%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT190-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 : n016.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:12 AM UTC 2026
% Result : Unsatisfiable 31.00s 6.34s
% Output : Refutation 36.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 93
% Number of leaves : 16
% Syntax : Number of formulae : 403 ( 364 unt; 5 def)
% Number of atoms : 449 ( 448 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 94 ( 48 ~; 46 |; 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 : 689 ( 689 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_meet) ).
fof(f8,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f9,axiom,
! [X0] : join(X0,complement(X0)) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement_join) ).
fof(f10,axiom,
! [X0] : meet(X0,complement(X0)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement_meet) ).
fof(f11,axiom,
! [X0,X1] :
( join(X0,X1) != one
| meet(X0,X1) != zero
| complement(X0) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f12,axiom,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),join(meet(X0,X2),meet(X1,join(X0,X2))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equation_H18) ).
fof(f13,negated_conjecture,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_distributivity) ).
fof(f14,definition,
sF0 = join(b,c),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f15,plain,
join(b,c) = sF0,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF1 = meet(a,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f17,plain,
meet(a,sF0) = sF1,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF2 = meet(a,b),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f19,plain,
meet(a,b) = sF2,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF3 = meet(a,c),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f21,plain,
meet(a,c) = sF3,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF4 = join(sF2,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f23,plain,
join(sF2,sF3) = sF4,
inference(reorient_equations,[],[f22]) ).
fof(f24,plain,
sF1 != sF4,
inference(definition_folding,[],[f13,f23,f21,f19,f17,f15]) ).
fof(f25,plain,
sF2 = meet(b,a),
inference(forward_demodulation,[],[f19,f5]) ).
fof(f26,plain,
sF3 = meet(c,a),
inference(forward_demodulation,[],[f21,f5]) ).
fof(f30,plain,
c = join(c,sF3),
inference(superposition,[],[f4,f26]) ).
fof(f32,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f33,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f32,f3]) ).
fof(f37,plain,
a = join(a,sF3),
inference(superposition,[],[f32,f26]) ).
fof(f39,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f33,f6]) ).
fof(f41,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f46,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X2)) = meet(X1,join(meet(X0,X1),join(meet(X1,X2),meet(X0,join(X1,X2))))),
inference(superposition,[],[f12,f5]) ).
fof(f64,plain,
! [X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X1)) = meet(X0,join(meet(X0,meet(X0,X1)),meet(X0,X1))),
inference(superposition,[],[f12,f4]) ).
fof(f68,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,meet(X0,X1))) = meet(X0,join(meet(X0,X1),meet(X0,meet(X0,X1)))),
inference(forward_demodulation,[],[f64,f6]) ).
fof(f78,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f68,f32]) ).
fof(f92,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f8,f4]) ).
fof(f93,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f32]) ).
fof(f96,plain,
! [X0] : join(b,join(c,X0)) = join(sF0,X0),
inference(superposition,[],[f8,f15]) ).
fof(f106,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f121,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f41,f32]) ).
fof(f129,plain,
! [X0,X1] : join(X1,X0) = join(join(X1,X0),X0),
inference(superposition,[],[f32,f41]) ).
fof(f131,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f129,f6]) ).
fof(f135,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f121,f5]) ).
fof(f140,plain,
sF3 = meet(sF3,sF4),
inference(superposition,[],[f41,f23]) ).
fof(f141,plain,
! [X0] : join(sF2,join(sF3,X0)) = join(sF4,X0),
inference(superposition,[],[f8,f23]) ).
fof(f147,plain,
! [X0,X1] :
( join(X0,X1) != one
| meet(X1,X0) != zero
| complement(X1) = X0 ),
inference(superposition,[],[f11,f6]) ).
fof(f179,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f181,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f41]) ).
fof(f183,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)),
inference(superposition,[],[f7,f5]) ).
fof(f185,plain,
! [X0] : meet(a,meet(sF0,X0)) = meet(sF1,X0),
inference(superposition,[],[f7,f17]) ).
fof(f186,plain,
! [X0] : meet(sF2,X0) = meet(b,meet(a,X0)),
inference(superposition,[],[f7,f25]) ).
fof(f187,plain,
! [X0] : meet(c,meet(a,X0)) = meet(sF3,X0),
inference(superposition,[],[f7,f26]) ).
fof(f195,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f248,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f252,plain,
! [X0,X1] : join(X0,complement(meet(X0,X1))) = join(X0,one),
inference(superposition,[],[f92,f9]) ).
fof(f253,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f265,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f248]) ).
fof(f291,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f41,f265]) ).
fof(f294,plain,
! [X0,X1] : one = join(X0,complement(meet(X0,X1))),
inference(backward_demodulation,[],[f252,f291]) ).
fof(f356,plain,
! [X0,X1] : one = join(X1,complement(meet(X0,X1))),
inference(superposition,[],[f294,f5]) ).
fof(f367,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X2)))) = meet(X0,join(meet(X0,X1),join(meet(X0,complement(meet(X0,X2))),meet(X1,one)))),
inference(superposition,[],[f12,f294]) ).
fof(f373,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X2)))) = meet(X0,join(meet(X0,X1),join(meet(X0,complement(meet(X0,X2))),X1))),
inference(forward_demodulation,[],[f367,f248]) ).
fof(f376,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X2)))) = meet(X0,join(X1,join(meet(X0,X1),meet(X0,complement(meet(X0,X2)))))),
inference(forward_demodulation,[],[f373,f106]) ).
fof(f377,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X2)))) = meet(X0,join(X1,meet(X0,complement(meet(X0,X2))))),
inference(forward_demodulation,[],[f376,f93]) ).
fof(f384,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(X0))) = meet(X0,join(X1,meet(X0,complement(X0)))),
inference(superposition,[],[f377,f248]) ).
fof(f395,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,complement(meet(X0,X1)))) = meet(X0,join(meet(X0,complement(meet(X0,X1))),X2)),
inference(superposition,[],[f377,f6]) ).
fof(f396,plain,
! [X2,X3,X0,X1] : join(meet(X2,join(X0,X1)),meet(X2,complement(meet(X2,X3)))) = meet(X2,join(X0,join(X1,meet(X2,complement(meet(X2,X3)))))),
inference(superposition,[],[f377,f8]) ).
fof(f404,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(X1,meet(X0,complement(meet(X0,X2)))),X3)) = meet(join(meet(X0,X1),meet(X0,complement(meet(X0,X2)))),X3),
inference(superposition,[],[f7,f377]) ).
fof(f430,plain,
! [X0,X1] : join(meet(X0,X1),zero) = meet(X0,join(X1,zero)),
inference(forward_demodulation,[],[f384,f10]) ).
fof(f446,plain,
! [X0,X1] : join(zero,meet(X0,X1)) = meet(X0,join(X1,zero)),
inference(forward_demodulation,[],[f430,f6]) ).
fof(f456,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f464,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f470,plain,
! [X0,X1] : meet(X0,X1) = join(zero,meet(X0,X1)),
inference(backward_demodulation,[],[f446,f456]) ).
fof(f490,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f470,f265]) ).
fof(f497,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f32,f470]) ).
fof(f606,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f179,f5]) ).
fof(f612,plain,
! [X0,X1] : meet(X0,zero) = meet(X0,complement(join(X0,X1))),
inference(superposition,[],[f179,f10]) ).
fof(f632,plain,
! [X0,X1] : zero = meet(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f612,f497]) ).
fof(f653,plain,
one = join(sF0,complement(sF1)),
inference(superposition,[],[f356,f17]) ).
fof(f702,plain,
! [X0,X1] : zero = meet(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f464,f5]) ).
fof(f864,plain,
! [X0] : join(a,X0) = join(a,join(sF2,X0)),
inference(superposition,[],[f93,f25]) ).
fof(f867,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f93,f6]) ).
fof(f961,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,f253]) ).
fof(f969,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f961]) ).
fof(f1297,plain,
! [X0,X1] : zero = meet(X1,complement(join(X0,X1))),
inference(superposition,[],[f632,f6]) ).
fof(f1532,plain,
! [X0,X1] : meet(X0,one) = join(meet(X0,complement(meet(X0,complement(meet(X0,X1))))),meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f395,f9]) ).
fof(f1586,plain,
! [X0,X1] : meet(X0,one) = join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f1532,f6]) ).
fof(f1623,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = X0,
inference(forward_demodulation,[],[f1586,f248]) ).
fof(f1673,plain,
meet(sF3,sF0) = meet(c,sF1),
inference(superposition,[],[f187,f17]) ).
fof(f1729,plain,
meet(c,sF1) = meet(sF0,sF3),
inference(forward_demodulation,[],[f1673,f5]) ).
fof(f1985,plain,
join(b,c) = join(sF0,sF3),
inference(superposition,[],[f96,f30]) ).
fof(f2002,plain,
sF0 = join(sF0,sF3),
inference(forward_demodulation,[],[f1985,f15]) ).
fof(f2292,plain,
! [X2,X3,X0,X1] : meet(X1,meet(X3,X0)) = meet(X1,meet(X0,meet(join(X1,X2),X3))),
inference(superposition,[],[f179,f195]) ).
fof(f2912,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,complement(meet(X1,X2)))) = meet(X1,join(meet(X0,X1),join(meet(X1,complement(meet(X1,X2))),meet(X0,one)))),
inference(superposition,[],[f46,f294]) ).
fof(f3017,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,complement(meet(X1,X2)))) = meet(X1,join(meet(X0,X1),join(meet(X1,complement(meet(X1,X2))),X0))),
inference(forward_demodulation,[],[f2912,f248]) ).
fof(f3106,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,complement(meet(X1,X2)))) = meet(X1,join(X0,join(meet(X0,X1),meet(X1,complement(meet(X1,X2)))))),
inference(forward_demodulation,[],[f3017,f106]) ).
fof(f3174,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,complement(meet(X1,X2)))) = join(meet(X1,join(X0,meet(X0,X1))),meet(X1,complement(meet(X1,X2)))),
inference(forward_demodulation,[],[f3106,f396]) ).
fof(f3215,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,complement(meet(X1,X2)))) = join(meet(X0,X1),meet(X1,complement(meet(X1,X2)))),
inference(forward_demodulation,[],[f3174,f4]) ).
fof(f3350,plain,
! [X2,X3,X0,X1] : meet(meet(X1,X0),X3) = meet(meet(X1,X0),meet(join(meet(X0,X1),meet(X0,complement(meet(X0,X2)))),X3)),
inference(superposition,[],[f179,f3215]) ).
fof(f3358,plain,
! [X2,X3,X0,X1] : meet(meet(X1,X0),X3) = meet(X1,meet(X0,meet(join(meet(X0,X1),meet(X0,complement(meet(X0,X2)))),X3))),
inference(forward_demodulation,[],[f3350,f7]) ).
fof(f3403,plain,
! [X2,X3,X0,X1] : meet(meet(X1,X0),X3) = meet(X1,meet(X0,meet(X0,meet(join(X1,meet(X0,complement(meet(X0,X2)))),X3)))),
inference(forward_demodulation,[],[f3358,f404]) ).
fof(f3442,plain,
! [X2,X3,X0,X1] : meet(meet(X1,X0),X3) = meet(X1,meet(X0,meet(join(X1,meet(X0,complement(meet(X0,X2)))),X3))),
inference(forward_demodulation,[],[f3403,f78]) ).
fof(f3467,plain,
! [X3,X0,X1] : meet(X1,meet(X3,X0)) = meet(meet(X1,X0),X3),
inference(forward_demodulation,[],[f3442,f2292]) ).
fof(f4344,plain,
! [X2,X3,X0,X1] : join(X2,join(X3,X0)) = join(X2,join(X0,join(meet(X1,X2),X3))),
inference(superposition,[],[f93,f106]) ).
fof(f4500,plain,
meet(sF2,sF0) = meet(b,sF1),
inference(superposition,[],[f186,f17]) ).
fof(f4503,plain,
! [X0] : meet(sF2,X0) = meet(b,meet(X0,a)),
inference(superposition,[],[f186,f5]) ).
fof(f4542,plain,
! [X0] : meet(sF2,X0) = meet(b,meet(sF2,X0)),
inference(superposition,[],[f78,f186]) ).
fof(f4586,plain,
meet(b,sF1) = meet(sF0,sF2),
inference(forward_demodulation,[],[f4500,f5]) ).
fof(f4673,plain,
sF0 = join(b,sF0),
inference(superposition,[],[f39,f15]) ).
fof(f5398,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X2,X1)),
inference(superposition,[],[f7,f3467]) ).
fof(f6190,plain,
meet(sF2,c) = meet(b,sF3),
inference(superposition,[],[f4503,f26]) ).
fof(f6246,plain,
meet(b,sF3) = meet(c,sF2),
inference(forward_demodulation,[],[f6190,f5]) ).
fof(f6575,plain,
! [X2,X0,X1] : join(complement(meet(X0,X2)),meet(X1,X0)) = join(complement(meet(X0,X2)),join(meet(X0,X1),meet(X0,complement(meet(X0,X2))))),
inference(superposition,[],[f867,f3215]) ).
fof(f6648,plain,
! [X2,X0,X1] : join(complement(meet(X0,X2)),meet(X1,X0)) = join(complement(meet(X0,X2)),meet(X0,X1)),
inference(forward_demodulation,[],[f6575,f867]) ).
fof(f6745,plain,
meet(b,sF3) = meet(sF2,meet(b,sF3)),
inference(superposition,[],[f135,f6246]) ).
fof(f6825,plain,
meet(b,sF3) = meet(b,meet(sF3,sF2)),
inference(forward_demodulation,[],[f6745,f195]) ).
fof(f6862,plain,
meet(b,sF3) = meet(b,meet(sF2,sF3)),
inference(forward_demodulation,[],[f6825,f5398]) ).
fof(f6881,plain,
meet(sF2,sF3) = meet(b,sF3),
inference(forward_demodulation,[],[f6862,f4542]) ).
fof(f7766,plain,
! [X0,X1] :
( one != one
| zero != meet(join(X1,complement(join(X0,X1))),X0)
| complement(join(X1,complement(join(X0,X1)))) = X0 ),
inference(superposition,[],[f147,f253]) ).
fof(f7771,plain,
! [X0] :
( one != one
| zero != meet(complement(X0),X0)
| complement(complement(X0)) = X0 ),
inference(superposition,[],[f147,f9]) ).
fof(f7793,plain,
! [X0] :
( zero != meet(complement(X0),X0)
| complement(complement(X0)) = X0 ),
inference(trivial_inequality_removal,[],[f7771]) ).
fof(f7796,plain,
! [X0,X1] :
( zero != meet(join(X1,complement(join(X0,X1))),X0)
| complement(join(X1,complement(join(X0,X1)))) = X0 ),
inference(trivial_inequality_removal,[],[f7766]) ).
fof(f7807,plain,
! [X0] :
( meet(X0,complement(X0)) != zero
| complement(complement(X0)) = X0 ),
inference(forward_demodulation,[],[f7793,f5]) ).
fof(f7812,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(join(X1,complement(join(X0,X1)))) = X0 ),
inference(forward_demodulation,[],[f7796,f5]) ).
fof(f7826,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_subsumption_resolution,[],[f7807,f10]) ).
fof(f7886,plain,
! [X0,X1] : join(complement(X0),meet(X1,X0)) = join(complement(X0),meet(X0,X1)),
inference(superposition,[],[f6648,f248]) ).
fof(f8037,plain,
! [X0,X1] : join(X0,meet(complement(X0),X1)) = join(X0,meet(X1,complement(X0))),
inference(superposition,[],[f7886,f7826]) ).
fof(f9353,plain,
join(a,sF3) = join(a,sF4),
inference(superposition,[],[f864,f23]) ).
fof(f9450,plain,
a = join(a,sF4),
inference(forward_demodulation,[],[f9353,f37]) ).
fof(f9482,plain,
sF4 = meet(sF4,a),
inference(superposition,[],[f41,f9450]) ).
fof(f9505,plain,
sF4 = meet(a,sF4),
inference(forward_demodulation,[],[f9482,f5]) ).
fof(f9508,plain,
meet(sF3,sF4) = meet(c,sF4),
inference(superposition,[],[f187,f9505]) ).
fof(f9544,plain,
sF3 = meet(c,sF4),
inference(forward_demodulation,[],[f9508,f140]) ).
fof(f10323,plain,
! [X0,X1] : join(complement(meet(X0,X1)),X0) = join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(superposition,[],[f93,f1623]) ).
fof(f10372,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,[],[f10323,f6]) ).
fof(f10415,plain,
! [X0,X1] : one = join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f10372,f294]) ).
fof(f10539,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,f10415]) ).
fof(f10559,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,[],[f10539]) ).
fof(f10575,plain,
! [X0,X1] : meet(X0,complement(meet(X0,complement(meet(X0,X1))))) = complement(complement(meet(X0,X1))),
inference(forward_subsumption_resolution,[],[f10559,f702]) ).
fof(f10619,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f10575,f7826]) ).
fof(f10641,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,X1)) = X0,
inference(backward_demodulation,[],[f1623,f10619]) ).
fof(f10667,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = X0,
inference(forward_demodulation,[],[f10641,f6]) ).
fof(f10751,plain,
! [X0,X1] : join(meet(X1,X0),meet(X0,complement(meet(X0,X1)))) = X0,
inference(superposition,[],[f3215,f10667]) ).
fof(f10752,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f93,f10667]) ).
fof(f10776,plain,
! [X0,X1] :
( zero != meet(meet(X0,X1),join(meet(X0,complement(meet(X0,X1))),complement(X0)))
| complement(meet(X0,X1)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(superposition,[],[f969,f10667]) ).
fof(f10785,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,join(meet(X0,complement(meet(X0,X1))),complement(X0))))
| complement(meet(X0,X1)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(forward_demodulation,[],[f10776,f7]) ).
fof(f10850,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,join(complement(X0),meet(X0,complement(meet(X0,X1))))))
| complement(meet(X0,X1)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(forward_demodulation,[],[f10785,f6]) ).
fof(f10894,plain,
! [X0,X1] :
( complement(meet(X0,X1)) = join(complement(X0),meet(X0,complement(meet(X0,X1))))
| zero != meet(X0,meet(X1,join(complement(X0),meet(X0,complement(meet(X0,X1)))))) ),
inference(forward_demodulation,[],[f10850,f6]) ).
fof(f10918,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f10752,f5]) ).
fof(f11257,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = meet(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f395,f10619]) ).
fof(f11259,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = join(meet(X2,X0),meet(X0,X1)),
inference(superposition,[],[f3215,f10619]) ).
fof(f11268,plain,
! [X2,X0,X1] : join(meet(X2,X0),meet(X0,X1)) = meet(X0,join(meet(X2,X0),join(meet(X0,X1),meet(X2,join(X0,complement(meet(X0,complement(meet(X0,X1))))))))),
inference(superposition,[],[f46,f10619]) ).
fof(f11325,plain,
! [X2,X0,X1] : join(meet(X2,X0),meet(X0,X1)) = meet(X0,join(meet(X2,X0),join(meet(X0,X1),meet(X2,one)))),
inference(forward_demodulation,[],[f11268,f294]) ).
fof(f11484,plain,
! [X2,X0,X1] : join(meet(X2,X0),meet(X0,X1)) = meet(X0,join(meet(X2,X0),join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f11325,f248]) ).
fof(f11614,plain,
! [X2,X0,X1] : join(meet(X2,X0),meet(X0,X1)) = meet(X0,join(X2,join(meet(X2,X0),meet(X0,X1)))),
inference(forward_demodulation,[],[f11484,f106]) ).
fof(f11687,plain,
! [X2,X0,X1] : join(meet(X2,X0),meet(X0,X1)) = meet(X0,join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f11614,f92]) ).
fof(f13414,plain,
! [X0,X1] :
( zero != meet(meet(X1,X0),join(meet(X0,complement(meet(X0,X1))),complement(X0)))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(superposition,[],[f969,f10751]) ).
fof(f13421,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,join(meet(X0,complement(meet(X0,X1))),complement(X0))))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(forward_demodulation,[],[f13414,f7]) ).
fof(f13529,plain,
! [X0,X1] :
( zero != meet(X1,join(meet(X0,complement(X0)),meet(X0,complement(meet(X0,X1)))))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(forward_demodulation,[],[f13421,f11257]) ).
fof(f13615,plain,
! [X0,X1] :
( zero != meet(X1,join(zero,meet(X0,complement(meet(X0,X1)))))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(forward_demodulation,[],[f13529,f10]) ).
fof(f13661,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,complement(meet(X0,X1))))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(forward_demodulation,[],[f13615,f490]) ).
fof(f13692,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)),
inference(forward_subsumption_resolution,[],[f13661,f702]) ).
fof(f13711,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f13692,f6]) ).
fof(f13727,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,complement(meet(X1,X0))))
| complement(meet(X0,X1)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))) ),
inference(backward_demodulation,[],[f10894,f13711]) ).
fof(f13729,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_subsumption_resolution,[],[f13727,f702]) ).
fof(f13733,plain,
! [X0,X1] : complement(meet(X1,complement(X0))) = join(X0,meet(complement(X0),complement(meet(complement(X0),X1)))),
inference(superposition,[],[f13711,f7826]) ).
fof(f13749,plain,
! [X2,X0,X1] : join(complement(X0),meet(X0,complement(meet(X0,X1)))) = complement(meet(meet(join(X2,X0),X1),X0)),
inference(superposition,[],[f13711,f181]) ).
fof(f13784,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = complement(meet(complement(meet(X0,X1)),X0)),
inference(superposition,[],[f13711,f10619]) ).
fof(f13795,plain,
! [X0,X1] : complement(X1) = meet(complement(X1),complement(meet(X0,X1))),
inference(superposition,[],[f3,f13711]) ).
fof(f13796,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(complement(X1),join(meet(X1,complement(meet(X1,X0))),X2)),
inference(superposition,[],[f8,f13711]) ).
fof(f13835,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = complement(meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f13784,f5]) ).
fof(f13870,plain,
! [X2,X0,X1] : complement(meet(X0,meet(join(X2,X0),X1))) = join(complement(X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f13749,f5]) ).
fof(f13948,plain,
! [X2,X0,X1] : complement(meet(X1,X0)) = complement(meet(X0,meet(join(X2,X0),X1))),
inference(forward_demodulation,[],[f13870,f13711]) ).
fof(f13982,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(forward_demodulation,[],[f13948,f181]) ).
fof(f14037,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,X1))) = join(meet(X2,X1),meet(X0,X1)),
inference(superposition,[],[f11687,f135]) ).
fof(f14079,plain,
! [X0] : join(meet(X0,sF0),meet(c,sF1)) = meet(sF0,join(X0,meet(c,sF1))),
inference(superposition,[],[f11687,f1729]) ).
fof(f14084,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,complement(X0))) = meet(X1,join(X0,meet(complement(X0),X1))),
inference(superposition,[],[f11687,f8037]) ).
fof(f14101,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = join(meet(complement(X1),X1),meet(X1,complement(meet(X1,X0)))),
inference(superposition,[],[f11687,f13711]) ).
fof(f14197,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = join(meet(X1,complement(X1)),meet(X1,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f14101,f3215]) ).
fof(f14267,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,complement(X0))) = join(meet(X0,X1),meet(complement(X0),X1)),
inference(backward_demodulation,[],[f14084,f14037]) ).
fof(f14323,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = join(zero,meet(X1,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f14197,f10]) ).
fof(f14417,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(X1,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f14323,f490]) ).
fof(f14560,plain,
! [X2,X0,X1] : meet(X0,meet(complement(meet(X0,X1)),X2)) = meet(X2,meet(X0,complement(meet(X1,X0)))),
inference(superposition,[],[f195,f14417]) ).
fof(f14617,plain,
! [X0,X1] : join(complement(X0),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = complement(meet(complement(meet(X1,X0)),X0)),
inference(superposition,[],[f13711,f14417]) ).
fof(f14636,plain,
! [X0,X1] : complement(meet(X0,complement(meet(X1,X0)))) = join(complement(X0),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f14617,f13982]) ).
fof(f14683,plain,
! [X0,X1] : complement(meet(X0,complement(meet(X1,X0)))) = complement(meet(complement(meet(X0,X1)),X0)),
inference(forward_demodulation,[],[f14636,f13711]) ).
fof(f14709,plain,
! [X0,X1] : complement(meet(X0,complement(meet(X0,X1)))) = complement(meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f14683,f13982]) ).
fof(f14723,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = complement(meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f14709,f13835]) ).
fof(f14768,plain,
! [X0,X1] : join(complement(join(X0,X1)),meet(join(X0,X1),X0)) = complement(meet(join(X0,X1),complement(X0))),
inference(superposition,[],[f14723,f3]) ).
fof(f14770,plain,
! [X0,X1] : join(complement(join(X1,X0)),meet(join(X1,X0),X0)) = complement(meet(join(X1,X0),complement(X0))),
inference(superposition,[],[f14723,f41]) ).
fof(f14827,plain,
! [X0,X1] : meet(X0,complement(meet(X1,X0))) = complement(join(complement(X0),meet(X0,X1))),
inference(superposition,[],[f7826,f14723]) ).
fof(f14888,plain,
! [X0,X1] : join(complement(join(X1,X0)),meet(join(X1,X0),X0)) = complement(meet(complement(X0),join(X1,X0))),
inference(forward_demodulation,[],[f14770,f13982]) ).
fof(f14890,plain,
! [X0,X1] : join(complement(join(X0,X1)),meet(join(X0,X1),X0)) = complement(meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f14768,f13982]) ).
fof(f14958,plain,
! [X0,X1] : join(complement(join(X1,X0)),meet(X0,join(X1,X0))) = complement(meet(complement(X0),join(X1,X0))),
inference(forward_demodulation,[],[f14888,f7886]) ).
fof(f14960,plain,
! [X0,X1] : join(complement(join(X0,X1)),meet(X0,join(X0,X1))) = complement(meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f14890,f7886]) ).
fof(f15018,plain,
! [X0,X1] : complement(meet(complement(X0),join(X1,X0))) = join(complement(join(X1,X0)),X0),
inference(forward_demodulation,[],[f14958,f41]) ).
fof(f15020,plain,
! [X0,X1] : join(complement(join(X0,X1)),X0) = complement(meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f14960,f3]) ).
fof(f15061,plain,
! [X0,X1] : join(X0,complement(join(X1,X0))) = complement(meet(complement(X0),join(X1,X0))),
inference(forward_demodulation,[],[f15018,f6]) ).
fof(f15063,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = complement(meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f15020,f6]) ).
fof(f15130,plain,
! [X0,X1] : join(X0,join(X1,X0)) = join(X0,meet(join(X1,X0),complement(X0))),
inference(superposition,[],[f10918,f41]) ).
fof(f15193,plain,
! [X0,X1] :
( zero != meet(X0,join(meet(X1,complement(meet(X0,X1))),complement(join(X0,X1))))
| complement(X0) = join(meet(X1,complement(meet(X0,X1))),complement(join(X0,X1))) ),
inference(superposition,[],[f969,f10918]) ).
fof(f15224,plain,
! [X0,X1] :
( zero != meet(X0,join(complement(join(X0,X1)),meet(X1,complement(meet(X0,X1)))))
| complement(X0) = join(meet(X1,complement(meet(X0,X1))),complement(join(X0,X1))) ),
inference(forward_demodulation,[],[f15193,f6]) ).
fof(f15265,plain,
! [X0,X1] : join(X0,join(X1,X0)) = join(X0,meet(complement(X0),join(X1,X0))),
inference(forward_demodulation,[],[f15130,f8037]) ).
fof(f15290,plain,
! [X0,X1] :
( complement(X0) = join(complement(join(X0,X1)),meet(X1,complement(meet(X0,X1))))
| zero != meet(X0,join(complement(join(X0,X1)),meet(X1,complement(meet(X0,X1))))) ),
inference(forward_demodulation,[],[f15224,f6]) ).
fof(f15310,plain,
! [X0,X1] : join(X1,X0) = join(X0,meet(complement(X0),join(X1,X0))),
inference(forward_demodulation,[],[f15265,f131]) ).
fof(f15904,plain,
! [X2,X0,X1] : meet(complement(X0),X2) = meet(complement(X0),meet(X2,complement(meet(X0,X1)))),
inference(superposition,[],[f606,f13729]) ).
fof(f16083,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = complement(join(complement(X0),meet(X0,X1))),
inference(superposition,[],[f7826,f13835]) ).
fof(f16282,plain,
! [X0,X1] : meet(X0,complement(meet(X1,complement(X0)))) = X0,
inference(superposition,[],[f13795,f7826]) ).
fof(f16302,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f13795,f3]) ).
fof(f16304,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f13795,f41]) ).
fof(f16418,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f16304,f5]) ).
fof(f16419,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f16302,f5]) ).
fof(f16543,plain,
! [X0,X1] : complement(meet(X1,complement(X0))) = join(X0,meet(complement(meet(X1,complement(X0))),complement(meet(complement(meet(X1,complement(X0))),X0)))),
inference(superposition,[],[f10751,f16282]) ).
fof(f16545,plain,
! [X0,X1] : join(X0,meet(complement(meet(X1,complement(X0))),complement(X0))) = join(X0,complement(meet(X1,complement(X0)))),
inference(superposition,[],[f10918,f16282]) ).
fof(f16575,plain,
! [X0,X1] : join(X0,meet(complement(X0),complement(meet(X1,complement(X0))))) = join(X0,complement(meet(X1,complement(X0)))),
inference(forward_demodulation,[],[f16545,f8037]) ).
fof(f16577,plain,
! [X0,X1] : complement(meet(X1,complement(X0))) = join(X0,complement(meet(X1,complement(X0)))),
inference(forward_demodulation,[],[f16543,f10752]) ).
fof(f16616,plain,
! [X0,X1] : complement(meet(X1,complement(X0))) = join(X0,meet(complement(X0),complement(meet(X1,complement(X0))))),
inference(backward_demodulation,[],[f16575,f16577]) ).
fof(f17351,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f4,f16419]) ).
fof(f17370,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),meet(complement(X0),complement(complement(join(X0,X1))))),
inference(superposition,[],[f10667,f16419]) ).
fof(f17393,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f17370,f7826]) ).
fof(f17633,plain,
! [X0,X1] : complement(X1) = join(complement(X1),complement(join(X0,X1))),
inference(superposition,[],[f17351,f131]) ).
fof(f18889,plain,
! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),meet(complement(complement(join(X1,X0))),complement(X0))),
inference(superposition,[],[f15310,f17633]) ).
fof(f18893,plain,
! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),meet(complement(X0),complement(complement(join(X1,X0))))),
inference(forward_demodulation,[],[f18889,f8037]) ).
fof(f18945,plain,
! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),meet(complement(X0),join(X1,X0))),
inference(forward_demodulation,[],[f18893,f7826]) ).
fof(f20253,plain,
! [X2,X0,X1] : join(X1,meet(complement(X1),complement(meet(X0,meet(complement(X1),X2))))) = complement(meet(meet(X2,X0),complement(X1))),
inference(superposition,[],[f13733,f195]) ).
fof(f20397,plain,
! [X2,X0,X1] : complement(meet(X2,meet(X0,complement(X1)))) = join(X1,meet(complement(X1),complement(meet(X0,meet(complement(X1),X2))))),
inference(forward_demodulation,[],[f20253,f7]) ).
fof(f21348,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),meet(X2,meet(X1,X0))) = join(complement(meet(X1,X0)),meet(X0,meet(X1,X2))),
inference(superposition,[],[f7886,f183]) ).
fof(f21367,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),meet(X0,meet(X1,X2))) = complement(meet(meet(X1,X0),complement(meet(X0,meet(X1,X2))))),
inference(superposition,[],[f13835,f183]) ).
fof(f21461,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),meet(X0,meet(X1,X2))) = complement(meet(X1,meet(X0,complement(meet(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f21367,f7]) ).
fof(f22018,plain,
! [X0,X1] : meet(complement(X0),complement(meet(X1,complement(X0)))) = complement(join(X0,meet(complement(X0),X1))),
inference(superposition,[],[f14827,f7826]) ).
fof(f22056,plain,
! [X0,X1] : meet(complement(X0),complement(meet(complement(join(X0,X1)),complement(X0)))) = complement(join(complement(complement(X0)),complement(join(X0,X1)))),
inference(superposition,[],[f14827,f16419]) ).
fof(f22057,plain,
! [X0,X1] : meet(complement(X1),complement(meet(complement(join(X0,X1)),complement(X1)))) = complement(join(complement(complement(X1)),complement(join(X0,X1)))),
inference(superposition,[],[f14827,f16418]) ).
fof(f22189,plain,
! [X0,X1] : complement(join(X1,complement(join(X0,X1)))) = meet(complement(X1),complement(meet(complement(join(X0,X1)),complement(X1)))),
inference(forward_demodulation,[],[f22057,f7826]) ).
fof(f22190,plain,
! [X0,X1] : complement(join(X0,complement(join(X0,X1)))) = meet(complement(X0),complement(meet(complement(join(X0,X1)),complement(X0)))),
inference(forward_demodulation,[],[f22056,f7826]) ).
fof(f22227,plain,
! [X0,X1] : complement(meet(X1,complement(X0))) = join(X0,complement(join(X0,meet(complement(X0),X1)))),
inference(backward_demodulation,[],[f16616,f22018]) ).
fof(f22280,plain,
! [X0,X1] : complement(join(X1,complement(join(X0,X1)))) = meet(complement(X1),complement(meet(complement(X1),complement(join(X0,X1))))),
inference(forward_demodulation,[],[f22189,f14417]) ).
fof(f22281,plain,
! [X0,X1] : complement(join(X0,complement(join(X0,X1)))) = meet(complement(X0),complement(meet(complement(X0),complement(join(X0,X1))))),
inference(forward_demodulation,[],[f22190,f14417]) ).
fof(f22343,plain,
! [X0,X1] : complement(join(X1,complement(join(X0,X1)))) = meet(complement(X1),complement(complement(join(X0,X1)))),
inference(forward_demodulation,[],[f22280,f16418]) ).
fof(f22344,plain,
! [X0,X1] : complement(join(X0,complement(join(X0,X1)))) = meet(complement(X0),complement(complement(join(X0,X1)))),
inference(forward_demodulation,[],[f22281,f16419]) ).
fof(f22383,plain,
! [X0,X1] : meet(complement(X1),join(X0,X1)) = complement(join(X1,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f22343,f7826]) ).
fof(f22384,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = complement(join(X0,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f22344,f7826]) ).
fof(f22413,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| meet(complement(X1),join(X0,X1)) = X0 ),
inference(backward_demodulation,[],[f7812,f22383]) ).
fof(f23081,plain,
! [X0,X1] :
( zero != meet(X0,join(meet(X1,complement(meet(X0,X1))),complement(join(X0,X1))))
| meet(complement(meet(X1,complement(meet(X0,X1)))),join(X0,X1)) = X0 ),
inference(superposition,[],[f22413,f10918]) ).
fof(f23143,plain,
! [X0,X1] :
( zero != meet(X0,join(complement(join(X0,X1)),meet(complement(X0),join(X0,X1))))
| meet(complement(complement(join(X0,X1))),join(X0,complement(join(X0,X1)))) = X0 ),
inference(superposition,[],[f22413,f22384]) ).
fof(f23144,plain,
! [X0,X1] :
( zero != meet(X0,join(complement(join(X1,X0)),meet(complement(X0),join(X1,X0))))
| meet(complement(complement(join(X1,X0))),join(X0,complement(join(X1,X0)))) = X0 ),
inference(superposition,[],[f22413,f22383]) ).
fof(f23169,plain,
! [X0,X1] :
( meet(X0,complement(X0)) != zero
| meet(complement(complement(join(X1,X0))),join(X0,complement(join(X1,X0)))) = X0 ),
inference(forward_demodulation,[],[f23144,f18945]) ).
fof(f23170,plain,
! [X0,X1] :
( meet(X0,complement(X0)) != zero
| meet(complement(complement(join(X0,X1))),join(X0,complement(join(X0,X1)))) = X0 ),
inference(forward_demodulation,[],[f23143,f17393]) ).
fof(f23220,plain,
! [X0,X1] :
( zero != meet(X0,join(complement(join(X0,X1)),meet(X1,complement(meet(X0,X1)))))
| meet(complement(meet(X1,complement(meet(X0,X1)))),join(X0,X1)) = X0 ),
inference(forward_demodulation,[],[f23081,f6]) ).
fof(f23233,plain,
! [X0,X1] : meet(complement(complement(join(X1,X0))),join(X0,complement(join(X1,X0)))) = X0,
inference(forward_subsumption_resolution,[],[f23169,f10]) ).
fof(f23234,plain,
! [X0,X1] : meet(complement(complement(join(X0,X1))),join(X0,complement(join(X0,X1)))) = X0,
inference(forward_subsumption_resolution,[],[f23170,f10]) ).
fof(f23278,plain,
! [X0,X1] :
( meet(join(X0,X1),complement(meet(X1,complement(meet(X0,X1))))) = X0
| zero != meet(X0,join(complement(join(X0,X1)),meet(X1,complement(meet(X0,X1))))) ),
inference(forward_demodulation,[],[f23220,f5]) ).
fof(f23290,plain,
! [X0,X1] : meet(join(X1,X0),join(X0,complement(join(X1,X0)))) = X0,
inference(forward_demodulation,[],[f23233,f7826]) ).
fof(f23291,plain,
! [X0,X1] : meet(join(X0,X1),join(X0,complement(join(X0,X1)))) = X0,
inference(forward_demodulation,[],[f23234,f7826]) ).
fof(f23333,plain,
! [X0,X1] :
( meet(join(X0,X1),join(complement(X1),meet(X1,X0))) = X0
| zero != meet(X0,join(complement(join(X0,X1)),meet(X1,complement(meet(X0,X1))))) ),
inference(forward_demodulation,[],[f23278,f14723]) ).
fof(f23535,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f181,f23291]) ).
fof(f23813,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f23535,f6]) ).
fof(f24318,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(join(X0,X1),join(meet(X1,complement(meet(X0,X1))),complement(join(X0,X1)))),
inference(superposition,[],[f23290,f10918]) ).
fof(f24525,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(join(X0,X1),join(complement(join(X0,X1)),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f24318,f6]) ).
fof(f24762,plain,
! [X0,X1] : meet(X0,meet(X1,complement(meet(X0,X1)))) = meet(X0,join(meet(X1,complement(meet(X0,X1))),complement(join(X0,X1)))),
inference(superposition,[],[f23813,f10918]) ).
fof(f25013,plain,
! [X0,X1] : meet(X0,meet(X1,complement(meet(X0,X1)))) = meet(X0,join(complement(join(X0,X1)),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f24762,f6]) ).
fof(f25130,plain,
! [X0,X1] : zero = meet(X0,join(complement(join(X0,X1)),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f25013,f464]) ).
fof(f25197,plain,
! [X0,X1] :
( zero != zero
| meet(join(X0,X1),join(complement(X1),meet(X1,X0))) = X0 ),
inference(backward_demodulation,[],[f23333,f25130]) ).
fof(f25198,plain,
! [X0,X1] :
( zero != zero
| complement(X0) = join(complement(join(X0,X1)),meet(X1,complement(meet(X0,X1)))) ),
inference(backward_demodulation,[],[f15290,f25130]) ).
fof(f25199,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),meet(X1,complement(meet(X0,X1)))),
inference(trivial_inequality_removal,[],[f25198]) ).
fof(f25200,plain,
! [X0,X1] : meet(join(X0,X1),join(complement(X1),meet(X1,X0))) = X0,
inference(trivial_inequality_removal,[],[f25197]) ).
fof(f25249,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(join(X0,X1),complement(X0)),
inference(backward_demodulation,[],[f24525,f25199]) ).
fof(f25272,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f25249,f5]) ).
fof(f25391,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(join(complement(join(X0,X1)),X1),join(complement(X1),zero)),
inference(superposition,[],[f25200,f1297]) ).
fof(f25427,plain,
sF3 = meet(join(sF3,sF0),join(complement(sF0),meet(c,sF1))),
inference(superposition,[],[f25200,f1729]) ).
fof(f25441,plain,
! [X0,X1] : meet(complement(X1),join(X0,X1)) = meet(complement(X1),X0),
inference(superposition,[],[f606,f25200]) ).
fof(f25444,plain,
! [X0,X1] : join(complement(X1),meet(X1,X0)) = join(join(complement(X1),meet(X1,X0)),X0),
inference(superposition,[],[f32,f25200]) ).
fof(f25448,plain,
! [X0,X1] : meet(join(complement(X1),meet(X1,X0)),X0) = X0,
inference(superposition,[],[f135,f25200]) ).
fof(f25457,plain,
! [X2,X0,X1] : join(join(complement(X1),meet(X1,X0)),X2) = join(join(complement(X1),meet(X1,X0)),join(X2,X0)),
inference(superposition,[],[f867,f25200]) ).
fof(f25478,plain,
! [X0,X1] : complement(join(complement(X1),meet(X1,X0))) = meet(complement(join(complement(X1),meet(X1,X0))),complement(X0)),
inference(superposition,[],[f13795,f25200]) ).
fof(f25491,plain,
! [X0,X1] : complement(join(complement(X1),meet(X1,X0))) = meet(complement(X0),complement(join(complement(X1),meet(X1,X0)))),
inference(forward_demodulation,[],[f25478,f5]) ).
fof(f25508,plain,
! [X2,X0,X1] : join(join(complement(X1),meet(X1,X0)),X2) = join(X0,join(join(complement(X1),meet(X1,X0)),X2)),
inference(forward_demodulation,[],[f25457,f106]) ).
fof(f25516,plain,
! [X0,X1] : meet(X0,join(complement(X1),meet(X1,X0))) = X0,
inference(forward_demodulation,[],[f25448,f5]) ).
fof(f25520,plain,
! [X0,X1] : join(complement(X1),meet(X1,X0)) = join(X0,join(complement(X1),meet(X1,X0))),
inference(forward_demodulation,[],[f25444,f6]) ).
fof(f25523,plain,
! [X0,X1] : join(X0,complement(join(X1,X0))) = complement(meet(complement(X0),X1)),
inference(backward_demodulation,[],[f15061,f25441]) ).
fof(f25524,plain,
! [X0,X1] : join(X1,X0) = join(X0,meet(complement(X0),X1)),
inference(backward_demodulation,[],[f15310,f25441]) ).
fof(f25576,plain,
sF3 = meet(join(sF0,sF3),join(complement(sF0),meet(c,sF1))),
inference(forward_demodulation,[],[f25427,f6]) ).
fof(f25609,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(join(complement(X1),zero),join(complement(join(X0,X1)),X1)),
inference(forward_demodulation,[],[f25391,f5]) ).
fof(f25703,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f25491,f14827]) ).
fof(f25715,plain,
! [X2,X0,X1] : join(complement(X1),join(meet(X1,X0),X2)) = join(X0,join(complement(X1),join(meet(X1,X0),X2))),
inference(forward_demodulation,[],[f25508,f8]) ).
fof(f25720,plain,
! [X0,X1] : join(meet(complement(X1),X0),meet(X1,X0)) = X0,
inference(forward_demodulation,[],[f25516,f14037]) ).
fof(f25723,plain,
! [X0,X1] : join(X0,complement(X1)) = join(complement(X1),meet(X1,X0)),
inference(forward_demodulation,[],[f25520,f867]) ).
fof(f25777,plain,
! [X0,X1] : join(X1,X0) = join(X0,meet(X1,complement(X0))),
inference(backward_demodulation,[],[f8037,f25524]) ).
fof(f25785,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(meet(X1,complement(X0)))),
inference(backward_demodulation,[],[f22018,f25524]) ).
fof(f25787,plain,
! [X0,X1] : join(X0,complement(join(X1,X0))) = complement(meet(X1,complement(X0))),
inference(backward_demodulation,[],[f22227,f25524]) ).
fof(f25805,plain,
! [X2,X0,X1] : complement(meet(X2,meet(X0,complement(X1)))) = join(complement(meet(X0,meet(complement(X1),X2))),X1),
inference(backward_demodulation,[],[f20397,f25524]) ).
fof(f25898,plain,
sF3 = meet(sF0,join(complement(sF0),meet(c,sF1))),
inference(forward_demodulation,[],[f25576,f2002]) ).
fof(f25921,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(join(complement(X1),zero),join(X1,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f25609,f6]) ).
fof(f26004,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),X1),
inference(forward_demodulation,[],[f25703,f15904]) ).
fof(f26014,plain,
! [X2,X0,X1] : join(complement(X1),join(meet(X1,X0),X2)) = join(X0,join(X2,complement(X1))),
inference(forward_demodulation,[],[f25715,f4344]) ).
fof(f26017,plain,
! [X0,X1] : join(meet(X1,X0),meet(complement(X1),X0)) = X0,
inference(forward_demodulation,[],[f25720,f6]) ).
fof(f26019,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),meet(X1,X0)),
inference(backward_demodulation,[],[f7886,f25723]) ).
fof(f26034,plain,
! [X0,X1] : join(X1,complement(X0)) = complement(meet(X0,complement(meet(X1,X0)))),
inference(backward_demodulation,[],[f14723,f25723]) ).
fof(f26037,plain,
! [X0,X1] : meet(X0,complement(meet(X1,X0))) = complement(join(X1,complement(X0))),
inference(backward_demodulation,[],[f14827,f25723]) ).
fof(f26044,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = complement(join(X1,complement(X0))),
inference(backward_demodulation,[],[f16083,f25723]) ).
fof(f26228,plain,
! [X2,X0,X1] : complement(meet(X2,meet(X0,complement(X1)))) = join(X1,complement(meet(X0,meet(complement(X1),X2)))),
inference(forward_demodulation,[],[f25805,f6]) ).
fof(f26335,plain,
sF3 = join(meet(complement(sF0),sF0),meet(c,sF1)),
inference(forward_demodulation,[],[f25898,f14079]) ).
fof(f26348,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(join(complement(X1),zero),complement(meet(complement(X1),X0))),
inference(forward_demodulation,[],[f25921,f25523]) ).
fof(f26453,plain,
! [X2,X0,X1] : meet(X0,meet(complement(meet(X0,X1)),X2)) = meet(X2,meet(complement(X1),X0)),
inference(backward_demodulation,[],[f14560,f26004]) ).
fof(f26484,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X0,X1)),
inference(backward_demodulation,[],[f25272,f26004]) ).
fof(f26514,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X1),complement(X0)),
inference(backward_demodulation,[],[f25785,f26004]) ).
fof(f26540,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(complement(meet(X1,X0)),join(X2,complement(X1))),
inference(backward_demodulation,[],[f13796,f26014]) ).
fof(f26545,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,complement(X0))) = X1,
inference(backward_demodulation,[],[f14267,f26017]) ).
fof(f26725,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),meet(X0,meet(X1,X2))) = complement(meet(X1,complement(join(meet(X1,X2),complement(X0))))),
inference(backward_demodulation,[],[f21461,f26044]) ).
fof(f26770,plain,
! [X0,X1] : meet(complement(X1),X0) = complement(join(X1,complement(X0))),
inference(forward_demodulation,[],[f26037,f26004]) ).
fof(f26773,plain,
! [X0,X1] : join(X1,complement(X0)) = complement(meet(complement(X1),X0)),
inference(forward_demodulation,[],[f26034,f26004]) ).
fof(f26793,plain,
! [X2,X0,X1] : join(X2,complement(meet(X1,X0))) = join(complement(meet(X1,X0)),meet(X0,meet(X1,X2))),
inference(backward_demodulation,[],[f21348,f26019]) ).
fof(f26910,plain,
sF3 = join(meet(c,sF1),meet(complement(sF0),sF0)),
inference(forward_demodulation,[],[f26335,f6]) ).
fof(f26922,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(join(zero,complement(X1)),complement(meet(complement(X1),X0))),
inference(forward_demodulation,[],[f26348,f6]) ).
fof(f27061,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = complement(meet(complement(X0),X1)),
inference(backward_demodulation,[],[f15063,f26484]) ).
fof(f27115,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(complement(X1),join(complement(meet(X1,X0)),X2)),
inference(forward_demodulation,[],[f26540,f106]) ).
fof(f27374,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),meet(X0,meet(X1,X2))) = complement(meet(X1,meet(complement(meet(X1,X2)),X0))),
inference(backward_demodulation,[],[f26725,f26770]) ).
fof(f27407,plain,
! [X0,X1] : join(X0,complement(join(X1,X0))) = join(X0,complement(X1)),
inference(backward_demodulation,[],[f25523,f26773]) ).
fof(f27540,plain,
sF3 = join(meet(c,sF1),meet(sF0,complement(sF0))),
inference(forward_demodulation,[],[f26910,f5]) ).
fof(f27549,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(join(zero,complement(X1)),join(X1,complement(X0))),
inference(forward_demodulation,[],[f26922,f26773]) ).
fof(f27630,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f27061,f26773]) ).
fof(f27791,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),meet(X0,meet(X1,X2))) = complement(meet(X0,meet(complement(X2),X1))),
inference(forward_demodulation,[],[f27374,f26453]) ).
fof(f27833,plain,
! [X0,X1] : join(X0,complement(X1)) = complement(meet(X1,complement(X0))),
inference(backward_demodulation,[],[f25787,f27407]) ).
fof(f27904,plain,
sF3 = join(meet(c,sF1),zero),
inference(forward_demodulation,[],[f27540,f10]) ).
fof(f27913,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),join(X1,complement(X0))),
inference(forward_demodulation,[],[f27549,f490]) ).
fof(f28137,plain,
! [X2,X0,X1] : join(X2,complement(meet(X1,X0))) = complement(meet(X0,meet(complement(X2),X1))),
inference(forward_demodulation,[],[f27791,f26793]) ).
fof(f28259,plain,
sF3 = join(zero,meet(c,sF1)),
inference(forward_demodulation,[],[f27904,f6]) ).
fof(f28263,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f27913,f26484]) ).
fof(f28379,plain,
! [X2,X0,X1] : complement(meet(X2,meet(X0,complement(X1)))) = join(X1,join(X1,complement(meet(X2,X0)))),
inference(backward_demodulation,[],[f26228,f28137]) ).
fof(f28465,plain,
sF3 = meet(c,sF1),
inference(forward_demodulation,[],[f28259,f490]) ).
fof(f28532,plain,
! [X2,X0,X1] : join(X1,complement(meet(X2,X0))) = complement(meet(X2,meet(X0,complement(X1)))),
inference(forward_demodulation,[],[f28379,f39]) ).
fof(f28976,plain,
! [X0,X1] : meet(complement(X1),X0) = complement(join(complement(X0),X1)),
inference(superposition,[],[f26770,f6]) ).
fof(f29210,plain,
join(sF3,complement(sF2)) = join(complement(sF2),meet(b,sF3)),
inference(superposition,[],[f25723,f6881]) ).
fof(f29218,plain,
! [X0,X1] : meet(X1,join(X0,complement(X1))) = join(meet(complement(X1),X1),meet(X1,X0)),
inference(superposition,[],[f11687,f25723]) ).
fof(f29253,plain,
! [X0,X1] : join(meet(X1,complement(X1)),meet(X1,X0)) = meet(X1,join(X0,complement(X1))),
inference(forward_demodulation,[],[f29218,f11259]) ).
fof(f29305,plain,
! [X0,X1] : join(zero,meet(X1,X0)) = meet(X1,join(X0,complement(X1))),
inference(forward_demodulation,[],[f29253,f10]) ).
fof(f29344,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(X0,complement(X1))),
inference(forward_demodulation,[],[f29305,f490]) ).
fof(f29851,plain,
join(complement(sF2),meet(b,sF3)) = join(c,complement(sF2)),
inference(superposition,[],[f26019,f6246]) ).
fof(f29853,plain,
join(complement(sF4),sF3) = join(c,complement(sF4)),
inference(superposition,[],[f26019,f9544]) ).
fof(f29893,plain,
join(sF3,complement(sF4)) = join(c,complement(sF4)),
inference(forward_demodulation,[],[f29853,f6]) ).
fof(f29895,plain,
join(sF3,complement(sF2)) = join(c,complement(sF2)),
inference(backward_demodulation,[],[f29210,f29851]) ).
fof(f30357,plain,
! [X0,X1] : meet(X0,complement(X1)) = complement(join(complement(X0),X1)),
inference(superposition,[],[f26514,f7826]) ).
fof(f30373,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(complement(X0),X1),
inference(superposition,[],[f25777,f26514]) ).
fof(f30572,plain,
! [X0,X1] : join(complement(X0),X1) = complement(meet(X0,complement(X1))),
inference(superposition,[],[f7826,f30357]) ).
fof(f30667,plain,
! [X2,X0,X1] : complement(meet(X2,meet(X0,complement(X1)))) = join(complement(X2),join(complement(X0),X1)),
inference(superposition,[],[f30572,f30357]) ).
fof(f30668,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X1),complement(X0)),
inference(superposition,[],[f30572,f7826]) ).
fof(f30728,plain,
! [X2,X0,X1] : join(X1,complement(meet(X2,X0))) = join(complement(X2),join(complement(X0),X1)),
inference(forward_demodulation,[],[f30667,f28532]) ).
fof(f30753,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(X2,complement(meet(X1,meet(X1,X0)))),
inference(backward_demodulation,[],[f27115,f30728]) ).
fof(f30778,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(X2,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f30753,f78]) ).
fof(f32620,plain,
join(sF3,complement(sF4)) = join(complement(sF2),sF3),
inference(superposition,[],[f30373,f23]) ).
fof(f32710,plain,
join(sF3,complement(sF4)) = join(sF3,complement(sF2)),
inference(forward_demodulation,[],[f32620,f6]) ).
fof(f32761,plain,
join(sF3,complement(sF4)) = join(c,complement(sF2)),
inference(forward_demodulation,[],[f32710,f29895]) ).
fof(f32804,plain,
join(c,complement(sF2)) = join(c,complement(sF4)),
inference(backward_demodulation,[],[f29893,f32761]) ).
fof(f33109,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(X1,complement(X0)),
inference(superposition,[],[f29344,f30668]) ).
fof(f34491,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(X1))) = X0,
inference(superposition,[],[f26545,f5]) ).
fof(f38172,plain,
join(c,complement(sF1)) = join(complement(sF1),sF3),
inference(superposition,[],[f26019,f28465]) ).
fof(f38186,plain,
join(c,complement(sF1)) = join(sF3,complement(sF1)),
inference(forward_demodulation,[],[f38172,f6]) ).
fof(f38950,plain,
! [X2,X0,X1] : join(X2,complement(meet(complement(X0),complement(X1)))) = join(complement(complement(join(X0,X1))),X2),
inference(superposition,[],[f30778,f28263]) ).
fof(f39174,plain,
! [X2,X0,X1] : meet(complement(complement(meet(X1,X0))),X2) = complement(join(complement(meet(X0,X1)),complement(X2))),
inference(superposition,[],[f28976,f30778]) ).
fof(f39180,plain,
! [X2,X0,X1] : meet(complement(complement(meet(X1,X0))),X2) = meet(complement(complement(X2)),meet(X0,X1)),
inference(forward_demodulation,[],[f39174,f28976]) ).
fof(f39351,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X2,complement(meet(complement(X0),complement(X1)))),
inference(forward_demodulation,[],[f38950,f7826]) ).
fof(f39384,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(complement(complement(meet(X1,X0))),X2),
inference(forward_demodulation,[],[f39180,f7826]) ).
fof(f39507,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X2,join(X1,complement(complement(X0)))),
inference(forward_demodulation,[],[f39351,f27833]) ).
fof(f39537,plain,
! [X2,X0,X1] : meet(meet(X1,X0),X2) = meet(X2,meet(X0,X1)),
inference(forward_demodulation,[],[f39384,f7826]) ).
fof(f39586,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X2,join(X1,X0)),
inference(forward_demodulation,[],[f39507,f7826]) ).
fof(f39813,plain,
! [X0] : meet(X0,sF2) = meet(meet(a,b),X0),
inference(superposition,[],[f39537,f25]) ).
fof(f40036,plain,
! [X0] : meet(X0,sF2) = meet(a,meet(b,X0)),
inference(forward_demodulation,[],[f39813,f7]) ).
fof(f40203,plain,
! [X0] : meet(X0,sF2) = meet(b,meet(X0,a)),
inference(forward_demodulation,[],[f40036,f195]) ).
fof(f40505,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,X1)),
inference(superposition,[],[f6,f39586]) ).
fof(f41720,plain,
join(sF4,complement(sF1)) = join(sF2,join(c,complement(sF1))),
inference(superposition,[],[f141,f38186]) ).
fof(f41776,plain,
join(sF4,complement(sF1)) = join(c,join(complement(sF1),sF2)),
inference(forward_demodulation,[],[f41720,f106]) ).
fof(f41802,plain,
join(sF4,complement(sF1)) = join(c,join(sF2,complement(sF1))),
inference(forward_demodulation,[],[f41776,f40505]) ).
fof(f46825,plain,
sF0 = join(meet(b,sF1),meet(sF0,complement(sF2))),
inference(superposition,[],[f34491,f4586]) ).
fof(f52488,plain,
join(c,complement(complement(sF4))) = join(c,complement(join(c,complement(sF2)))),
inference(superposition,[],[f27630,f32804]) ).
fof(f52509,plain,
join(c,complement(complement(sF4))) = join(c,complement(complement(sF2))),
inference(forward_demodulation,[],[f52488,f27630]) ).
fof(f52537,plain,
join(c,sF2) = join(c,complement(complement(sF4))),
inference(forward_demodulation,[],[f52509,f7826]) ).
fof(f52567,plain,
join(c,sF2) = join(c,sF4),
inference(forward_demodulation,[],[f52537,f7826]) ).
fof(f52606,plain,
join(sF0,sF4) = join(b,join(c,sF2)),
inference(superposition,[],[f96,f52567]) ).
fof(f52663,plain,
join(sF0,sF2) = join(sF0,sF4),
inference(forward_demodulation,[],[f52606,f96]) ).
fof(f52683,plain,
sF4 = meet(sF4,join(sF0,sF2)),
inference(superposition,[],[f41,f52663]) ).
fof(f56087,plain,
! [X0] : meet(b,a) = meet(join(b,X0),sF2),
inference(superposition,[],[f179,f40203]) ).
fof(f56165,plain,
! [X0] : sF2 = meet(join(b,X0),sF2),
inference(forward_demodulation,[],[f56087,f25]) ).
fof(f56221,plain,
sF2 = meet(sF0,sF2),
inference(superposition,[],[f56165,f4673]) ).
fof(f56357,plain,
sF2 = meet(b,sF1),
inference(backward_demodulation,[],[f4586,f56221]) ).
fof(f56392,plain,
sF0 = join(sF2,meet(sF0,complement(sF2))),
inference(backward_demodulation,[],[f46825,f56357]) ).
fof(f56401,plain,
sF0 = join(sF0,sF2),
inference(forward_demodulation,[],[f56392,f25777]) ).
fof(f56414,plain,
sF4 = meet(sF4,sF0),
inference(backward_demodulation,[],[f52683,f56401]) ).
fof(f56426,plain,
sF4 = meet(sF0,sF4),
inference(forward_demodulation,[],[f56414,f5]) ).
fof(f56428,plain,
meet(a,sF4) = meet(sF1,sF4),
inference(superposition,[],[f185,f56426]) ).
fof(f56496,plain,
sF4 = meet(sF1,sF4),
inference(forward_demodulation,[],[f56428,f9505]) ).
fof(f56551,plain,
meet(sF4,complement(sF4)) = meet(sF4,complement(sF1)),
inference(superposition,[],[f33109,f56496]) ).
fof(f56564,plain,
zero = meet(sF4,complement(sF1)),
inference(forward_demodulation,[],[f56551,f10]) ).
fof(f56682,plain,
join(complement(sF1),sF2) = join(b,complement(sF1)),
inference(superposition,[],[f26019,f56357]) ).
fof(f56720,plain,
join(sF2,complement(sF1)) = join(b,complement(sF1)),
inference(forward_demodulation,[],[f56682,f6]) ).
fof(f56740,plain,
join(sF4,complement(sF1)) = join(c,join(b,complement(sF1))),
inference(backward_demodulation,[],[f41802,f56720]) ).
fof(f56743,plain,
join(sF4,complement(sF1)) = join(b,join(complement(sF1),c)),
inference(forward_demodulation,[],[f56740,f106]) ).
fof(f56745,plain,
join(sF4,complement(sF1)) = join(b,join(c,complement(sF1))),
inference(forward_demodulation,[],[f56743,f40505]) ).
fof(f56747,plain,
join(sF0,complement(sF1)) = join(sF4,complement(sF1)),
inference(forward_demodulation,[],[f56745,f96]) ).
fof(f56748,plain,
one = join(sF4,complement(sF1)),
inference(forward_demodulation,[],[f56747,f653]) ).
fof(f64035,plain,
( one != one
| zero != meet(complement(sF1),sF4)
| sF4 = complement(complement(sF1)) ),
inference(superposition,[],[f147,f56748]) ).
fof(f64062,plain,
( zero != meet(complement(sF1),sF4)
| sF4 = complement(complement(sF1)) ),
inference(trivial_inequality_removal,[],[f64035]) ).
fof(f64089,plain,
( zero != meet(sF4,complement(sF1))
| sF4 = complement(complement(sF1)) ),
inference(forward_demodulation,[],[f64062,f5]) ).
fof(f64123,plain,
sF4 = complement(complement(sF1)),
inference(forward_subsumption_resolution,[],[f64089,f56564]) ).
fof(f64225,plain,
sF1 = sF4,
inference(forward_demodulation,[],[f64123,f7826]) ).
fof(f64275,plain,
$false,
inference(forward_subsumption_resolution,[],[f64225,f24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT190-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.21/0.48 % Computer : n016.cluster.edu
% 0.21/0.48 % Model : x86_64 x86_64
% 0.21/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/0.48 % Memory : 8046.5625MB
% 0.21/0.48 % OS : Linux 6.8.0-71-generic
% 0.21/0.48 % CPULimit : 300
% 0.21/0.48 % WCLimit : 300
% 0.21/0.48 % DateTime : Sun Sep 27 14:10:02 UTC 2026
% 0.21/0.49 % CPUTime :
% 0.21/0.49 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.54 Running first-order theorem proving
% 0.25/0.54 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.52/3.40 % (2675304)Input is clausal, will run a generic CNF schedule.
% 15.52/3.40 % (2675310)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4034772635:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 15.52/3.40 % (2675309)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=1796608961:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 15.52/3.40 % (2675315)dis-21_1_sil=8000:lcm=predicate:random_seed=2973437168: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)
% 15.52/3.40 % (2675313)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4175342379:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 15.52/3.40 % (2675312)lrs+10_1_sil=8000:sp=occurrence:random_seed=430269581:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 15.52/3.40 % (2675314)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1420956233:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 15.52/3.40 % (2675311)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2676415335:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 15.52/3.40 % (2675315)Refutation not found, incomplete strategy
% 15.52/3.40 % (2675315)------------------------------
% 15.52/3.40 % (2675315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.52/3.40 % (2675315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.52/3.40 % (2675315)CaDiCaL version: 2.1.3
% 15.52/3.40 % (2675315)Termination reason: Refutation not found, incomplete strategy
% 15.52/3.40 % (2675315)Time elapsed: 0.003 s
% 15.52/3.40 % (2675315)Peak memory usage: 88 MB
% 15.52/3.40 % (2675315)Instructions burned: 1 (million)
% 15.52/3.40 % (2675312)Instruction limit reached!
% 15.52/3.40 % (2675312)------------------------------
% 15.52/3.40 % (2675312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.52/3.40 % (2675312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.52/3.40 % (2675312)CaDiCaL version: 2.1.3
% 15.52/3.40 % (2675312)Termination reason: Instruction limit
% 15.52/3.40 % (2675312)Termination phase: Saturation
% 15.52/3.40 % (2675312)Time elapsed: 0.105 s
% 15.52/3.40 % (2675312)Peak memory usage: 89 MB
% 15.52/3.40 % (2675312)Instructions burned: 107 (million)
% 15.52/3.40 % (2675313)Instruction limit reached!
% 15.52/3.40 % (2675313)------------------------------
% 15.52/3.40 % (2675313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.52/3.40 % (2675313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.52/3.40 % (2675313)CaDiCaL version: 2.1.3
% 15.52/3.40 % (2675313)Termination reason: Instruction limit
% 15.52/3.40 % (2675313)Termination phase: Saturation
% 15.52/3.40 % (2675313)Time elapsed: 0.110 s
% 15.52/3.40 % (2675313)Peak memory usage: 89 MB
% 15.52/3.40 % (2675313)Instructions burned: 114 (million)
% 15.52/3.40 % (2675314)Instruction limit reached!
% 15.52/3.40 % (2675314)------------------------------
% 15.52/3.40 % (2675314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.52/3.40 % (2675314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.52/3.40 % (2675314)CaDiCaL version: 2.1.3
% 15.52/3.40 % (2675314)Termination reason: Instruction limit
% 15.52/3.40 % (2675314)Termination phase: Saturation
% 15.52/3.40 % (2675314)Time elapsed: 0.167 s
% 15.52/3.40 % (2675314)Peak memory usage: 90 MB
% 15.52/3.40 % (2675314)Instructions burned: 181 (million)
% 15.52/3.40 % (2675315)------------------------------
% 15.52/3.40 % (2675315)------------------------------
% 15.52/3.40 % (2675325)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=1901801837:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 15.52/3.40 % (2675326)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2366869024: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)
% 15.52/3.40 % (2675325)Refutation not found, incomplete strategy
% 15.52/3.40 % (2675325)------------------------------
% 15.52/3.40 % (2675325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.52/3.40 % (2675325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.31/4.92 % (2675325)CaDiCaL version: 2.1.3
% 25.31/4.92 % (2675325)Termination reason: Refutation not found, incomplete strategy
% 25.31/4.92 % (2675325)Time elapsed: 0.002 s
% 25.31/4.92 % (2675325)Peak memory usage: 88 MB
% 25.31/4.92 % (2675326)Refutation not found, incomplete strategy
% 25.31/4.92 % (2675326)------------------------------
% 25.31/4.92 % (2675326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.31/4.92 % (2675326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.31/4.92 % (2675326)CaDiCaL version: 2.1.3
% 25.31/4.92 % (2675326)Termination reason: Refutation not found, incomplete strategy
% 25.31/4.92 % (2675326)Time elapsed: 0.002 s
% 25.31/4.92 % (2675326)Peak memory usage: 88 MB
% 25.31/4.92 % (2675326)Instructions burned: 1 (million)
% 25.31/4.92 % (2675327)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2854741136:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 25.31/4.92 % (2675327)Refutation not found, incomplete strategy
% 25.31/4.92 % (2675327)------------------------------
% 25.31/4.92 % (2675327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.31/4.92 % (2675327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.31/4.92 % (2675327)CaDiCaL version: 2.1.3
% 25.31/4.92 % (2675327)Termination reason: Refutation not found, incomplete strategy
% 25.31/4.92 % (2675327)Time elapsed: 0.002 s
% 25.31/4.92 % (2675327)Peak memory usage: 87 MB
% 25.31/4.92 % (2675330)lrs+10_64_to=lpo:sil=8000:random_seed=3813615512:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 25.31/4.92 % (2675326)------------------------------
% 25.31/4.92 % (2675326)------------------------------
% 25.31/4.92 % (2675325)------------------------------
% 25.31/4.92 % (2675325)------------------------------
% 25.31/4.92 % (2675330)Instruction limit reached!
% 25.31/4.92 % (2675330)------------------------------
% 25.31/4.92 % (2675330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.31/4.92 % (2675330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.31/4.92 % (2675330)CaDiCaL version: 2.1.3
% 25.31/4.92 % (2675330)Termination reason: Instruction limit
% 25.31/4.92 % (2675330)Termination phase: Saturation
% 25.31/4.92 % (2675330)Time elapsed: 0.073 s
% 25.31/4.92 % (2675330)Peak memory usage: 88 MB
% 25.31/4.92 % (2675330)Instructions burned: 127 (million)
% 25.31/4.92 % (2675327)------------------------------
% 25.31/4.92 % (2675327)------------------------------
% 25.31/4.92 % (2675352)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3063822181:i=157:gtg=all_2990 on theBenchmark for (2990ds/157Mi)
% 25.31/4.92 % (2675350)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2726485278:avsq=on:i=194:fgj=on:bd=preordered_2990 on theBenchmark for (2990ds/194Mi)
% 25.31/4.92 % (2675356)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3613310091:i=3394:sd=4:ss=included:sgt=64_2989 on theBenchmark for (2989ds/3394Mi)
% 25.31/4.92 % (2675371)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=2954473638:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2989 on theBenchmark for (2989ds/106Mi)
% 25.31/4.92 % (2675352)Instruction limit reached!
% 25.31/4.92 % (2675352)------------------------------
% 25.31/4.92 % (2675352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.31/4.92 % (2675352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.31/4.92 % (2675352)CaDiCaL version: 2.1.3
% 25.31/4.92 % (2675352)Termination reason: Instruction limit
% 25.31/4.92 % (2675352)Termination phase: Saturation
% 25.31/4.92 % (2675352)Time elapsed: 0.096 s
% 25.31/4.92 % (2675352)Peak memory usage: 90 MB
% 25.31/4.92 % (2675352)Instructions burned: 159 (million)
% 25.31/4.92 % (2675350)Instruction limit reached!
% 25.31/4.92 % (2675350)------------------------------
% 25.31/4.92 % (2675350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.31/4.92 % (2675350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.31/4.92 % (2675350)CaDiCaL version: 2.1.3
% 25.31/4.92 % (2675350)Termination reason: Instruction limit
% 25.31/4.92 % (2675350)Termination phase: Saturation
% 25.31/4.92 % (2675350)Time elapsed: 0.117 s
% 25.31/4.92 % (2675350)Peak memory usage: 89 MB
% 25.31/4.92 % (2675350)Instructions burned: 195 (million)
% 25.31/4.92 % (2675371)Instruction limit reached!
% 25.31/4.92 % (2675371)------------------------------
% 31.00/6.33 % (2675371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.00/6.33 % (2675371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.00/6.33 % (2675371)CaDiCaL version: 2.1.3
% 31.00/6.33 % (2675371)Termination reason: Instruction limit
% 31.00/6.33 % (2675371)Termination phase: Saturation
% 31.00/6.33 % (2675371)Time elapsed: 0.067 s
% 31.00/6.33 % (2675371)Peak memory usage: 89 MB
% 31.00/6.33 % (2675371)Instructions burned: 106 (million)
% 31.00/6.33 % (2675437)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2611150236:i=107_2987 on theBenchmark for (2987ds/107Mi)
% 31.00/6.33 % (2675437)Refutation not found, incomplete strategy
% 31.00/6.33 % (2675437)------------------------------
% 31.00/6.33 % (2675437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.00/6.33 % (2675437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.00/6.33 % (2675437)CaDiCaL version: 2.1.3
% 31.00/6.33 % (2675437)Termination reason: Refutation not found, incomplete strategy
% 31.00/6.33 % (2675437)Time elapsed: 0.001 s
% 31.00/6.33 % (2675437)Peak memory usage: 87 MB
% 31.00/6.33 % (2675441)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3658755433:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi)
% 31.00/6.33 % (2675442)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1994430443:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi)
% 31.00/6.33 % (2675441)Instruction limit reached!
% 31.00/6.33 % (2675441)------------------------------
% 31.00/6.33 % (2675441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.00/6.33 % (2675441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.00/6.33 % (2675441)CaDiCaL version: 2.1.3
% 31.00/6.33 % (2675441)Termination reason: Instruction limit
% 31.00/6.33 % (2675441)Termination phase: Saturation
% 31.00/6.33 % (2675441)Time elapsed: 0.142 s
% 31.00/6.33 % (2675441)Peak memory usage: 90 MB
% 31.00/6.33 % (2675441)Instructions burned: 244 (million)
% 31.00/6.33 % (2675437)------------------------------
% 31.00/6.33 % (2675437)------------------------------
% 31.00/6.33 % (2675501)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3376870108:i=134:sd=2:doe=on:ss=axioms:sgt=14_2984 on theBenchmark for (2984ds/134Mi)
% 31.00/6.33 % (2675502)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=435246827:i=499:bd=all_2983 on theBenchmark for (2983ds/499Mi)
% 31.00/6.33 % (2675501)Instruction limit reached!
% 31.00/6.33 % (2675501)------------------------------
% 31.00/6.33 % (2675501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.00/6.33 % (2675501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.00/6.33 % (2675501)CaDiCaL version: 2.1.3
% 31.00/6.33 % (2675501)Termination reason: Instruction limit
% 31.00/6.33 % (2675501)Termination phase: Saturation
% 31.00/6.33 % (2675501)Time elapsed: 0.080 s
% 31.00/6.33 % (2675501)Peak memory usage: 89 MB
% 31.00/6.33 % (2675501)Instructions burned: 134 (million)
% 31.00/6.33 % (2675505)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2949729469:i=191:fgj=on:bd=all_2982 on theBenchmark for (2982ds/191Mi)
% 31.00/6.33 % (2675505)Instruction limit reached!
% 31.00/6.33 % (2675505)------------------------------
% 31.00/6.33 % (2675505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.00/6.33 % (2675505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.00/6.33 % (2675505)CaDiCaL version: 2.1.3
% 31.00/6.33 % (2675505)Termination reason: Instruction limit
% 31.00/6.33 % (2675505)Termination phase: Saturation
% 31.00/6.33 % (2675505)Time elapsed: 0.121 s
% 31.00/6.33 % (2675505)Peak memory usage: 91 MB
% 31.00/6.33 % (2675505)Instructions burned: 192 (million)
% 31.00/6.33 % (2675502)Instruction limit reached!
% 31.00/6.33 % (2675502)------------------------------
% 31.00/6.33 % (2675502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.00/6.33 % (2675502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.00/6.33 % (2675502)CaDiCaL version: 2.1.3
% 31.00/6.33 % (2675502)Termination reason: Instruction limit
% 31.00/6.33 % (2675502)Termination phase: Saturation
% 31.00/6.33 % (2675502)Time elapsed: 0.310 s
% 31.00/6.33 % (2675502)Peak memory usage: 94 MB
% 31.00/6.33 % (2675502)Instructions burned: 499 (million)
% 31.00/6.34 % (2675507)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=528161214:i=264:kws=precedence:fsr=off_2979 on theBenchmark for (2979ds/264Mi)
% 31.00/6.34 % (2675508)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=835779610:cond=on:i=156:bs=on:gtg=exists_all:er=known_2979 on theBenchmark for (2979ds/156Mi)
% 31.00/6.34 % (2675508)Instruction limit reached!
% 31.00/6.34 % (2675508)------------------------------
% 31.00/6.34 % (2675508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.00/6.34 % (2675508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.00/6.34 % (2675508)CaDiCaL version: 2.1.3
% 31.00/6.34 % (2675508)Termination reason: Instruction limit
% 31.00/6.34 % (2675508)Termination phase: Saturation
% 31.00/6.34 % (2675508)Time elapsed: 0.094 s
% 31.00/6.34 % (2675508)Peak memory usage: 89 MB
% 31.00/6.34 % (2675508)Instructions burned: 157 (million)
% 31.00/6.34 % (2675507)Instruction limit reached!
% 31.00/6.34 % (2675507)------------------------------
% 31.00/6.34 % (2675507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.00/6.34 % (2675507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.00/6.34 % (2675507)CaDiCaL version: 2.1.3
% 31.00/6.34 % (2675507)Termination reason: Instruction limit
% 31.00/6.34 % (2675507)Termination phase: Saturation
% 31.00/6.34 % (2675507)Time elapsed: 0.158 s
% 31.00/6.34 % (2675507)Peak memory usage: 92 MB
% 31.00/6.34 % (2675507)Instructions burned: 264 (million)
% 31.00/6.34 % (2675511)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=1163026161:i=3256:kws=precedence:bd=preordered:av=off_2976 on theBenchmark for (2976ds/3256Mi)
% 31.00/6.34 % (2675512)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3779721074:i=537:av=off:ss=included_2976 on theBenchmark for (2976ds/537Mi)
% 31.00/6.34 % (2675512)Instruction limit reached!
% 31.00/6.34 % (2675512)------------------------------
% 31.00/6.34 % (2675512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.00/6.34 % (2675512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.00/6.34 % (2675512)CaDiCaL version: 2.1.3
% 31.00/6.34 % (2675512)Termination reason: Instruction limit
% 31.00/6.34 % (2675512)Termination phase: Saturation
% 31.00/6.34 % (2675512)Time elapsed: 0.290 s
% 31.00/6.34 % (2675512)Peak memory usage: 93 MB
% 31.00/6.34 % (2675512)Instructions burned: 539 (million)
% 31.00/6.34 % (2675515)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=132359104:i=180:bd=preordered:av=off_2971 on theBenchmark for (2971ds/180Mi)
% 31.00/6.34 % (2675515)Instruction limit reached!
% 31.00/6.34 % (2675515)------------------------------
% 31.00/6.34 % (2675515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.00/6.34 % (2675515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.00/6.34 % (2675515)CaDiCaL version: 2.1.3
% 31.00/6.34 % (2675515)Termination reason: Instruction limit
% 31.00/6.34 % (2675515)Termination phase: Saturation
% 31.00/6.34 % (2675515)Time elapsed: 0.102 s
% 31.00/6.34 % (2675515)Peak memory usage: 88 MB
% 31.00/6.34 % (2675515)Instructions burned: 180 (million)
% 31.00/6.34 % (2675356)Instruction limit reached!
% 31.00/6.34 % (2675356)------------------------------
% 31.00/6.34 % (2675356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.00/6.34 % (2675356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.00/6.34 % (2675356)CaDiCaL version: 2.1.3
% 31.00/6.34 % (2675356)Termination reason: Instruction limit
% 31.00/6.34 % (2675356)Termination phase: Saturation
% 31.00/6.34 % (2675356)Time elapsed: 2.040 s
% 31.00/6.34 % (2675356)Peak memory usage: 151 MB
% 31.00/6.34 % (2675356)Instructions burned: 3395 (million)
% 31.00/6.34 % (2675517)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=2189726877:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2968 on theBenchmark for (2968ds/10307Mi)
% 31.00/6.34 % (2675518)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=379886538:i=412:gtgl=4:gtg=exists_all_2967 on theBenchmark for (2967ds/412Mi)
% 31.00/6.34 % (2675518)Instruction limit reached!
% 31.00/6.34 % (2675518)------------------------------
% 31.00/6.34 % (2675518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.00/6.34 % (2675518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.00/6.34 % (2675518)CaDiCaL version: 2.1.3
% 31.00/6.34 % (2675518)Termination reason: Instruction limit
% 31.00/6.34 % (2675518)Termination phase: Saturation
% 31.00/6.34 % (2675518)Time elapsed: 0.241 s
% 31.00/6.34 % (2675518)Peak memory usage: 94 MB
% 31.00/6.34 % (2675518)Instructions burned: 413 (million)
% 31.00/6.34 % (2675521)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=1744161718:s2pl=no:i=8478:s2at=4:nm=6_2963 on theBenchmark for (2963ds/8478Mi)
% 31.00/6.34 % (2675511)Instruction limit reached!
% 31.00/6.34 % (2675511)------------------------------
% 31.00/6.34 % (2675511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.00/6.34 % (2675511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.00/6.34 % (2675511)CaDiCaL version: 2.1.3
% 31.00/6.34 % (2675511)Termination reason: Instruction limit
% 31.00/6.34 % (2675511)Termination phase: Saturation
% 31.00/6.34 % (2675511)Time elapsed: 2.002 s
% 31.00/6.34 % (2675511)Peak memory usage: 148 MB
% 31.00/6.34 % (2675511)Instructions burned: 3257 (million)
% 31.00/6.34 % (2675442)Instruction limit reached!
% 31.00/6.34 % (2675442)------------------------------
% 31.00/6.34 % (2675442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.00/6.34 % (2675442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.00/6.34 % (2675442)CaDiCaL version: 2.1.3
% 31.00/6.34 % (2675442)Termination reason: Instruction limit
% 31.00/6.34 % (2675442)Termination phase: Saturation
% 31.00/6.34 % (2675442)Time elapsed: 3.107 s
% 31.00/6.34 % (2675442)Peak memory usage: 168 MB
% 31.00/6.34 % (2675442)Instructions burned: 5209 (million)
% 31.00/6.34 % (2675523)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=1949079784:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2954 on theBenchmark for (2954ds/303Mi)
% 31.00/6.34 % (2675524)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3905973314:st=4:i=720:sd=3:fsr=off:ss=axioms_2954 on theBenchmark for (2954ds/720Mi)
% 31.00/6.34 % (2675524)Refutation not found, incomplete strategy
% 31.00/6.34 % (2675524)------------------------------
% 31.00/6.34 % (2675524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.00/6.34 % (2675524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.00/6.34 % (2675524)CaDiCaL version: 2.1.3
% 31.00/6.34 % (2675524)Termination reason: Refutation not found, incomplete strategy
% 31.00/6.34 % (2675524)Time elapsed: 0.001 s
% 31.00/6.34 % (2675524)Peak memory usage: 88 MB
% 31.00/6.34 % (2675523)Refutation not found, incomplete strategy
% 31.00/6.34 % (2675523)------------------------------
% 31.00/6.34 % (2675523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.00/6.34 % (2675523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.00/6.34 % (2675523)CaDiCaL version: 2.1.3
% 31.00/6.34 % (2675523)Termination reason: Refutation not found, incomplete strategy
% 31.00/6.34 % (2675523)Time elapsed: 0.002 s
% 31.00/6.34 % (2675523)Peak memory usage: 88 MB
% 31.00/6.34 % (2675523)Instructions burned: 1 (million)
% 31.00/6.34 % (2675311)First to succeed.
% 31.00/6.34 % (2675311)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2675304"
% 31.00/6.34 % (2675523)------------------------------
% 31.00/6.34 % (2675523)------------------------------
% 31.00/6.34 % (2675524)------------------------------
% 31.00/6.34 % (2675524)------------------------------
% 31.00/6.34 % (2675311)Refutation found. Thanks to Tanya!
% 31.00/6.34 % SZS status Unsatisfiable for theBenchmark
% 31.00/6.34 % SZS output start Proof for theBenchmark
% See solution above
% 36.51/6.56 % (2675311)------------------------------
% 36.51/6.56 % (2675311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.51/6.56 % (2675311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.51/6.56 % (2675311)CaDiCaL version: 2.1.3
% 36.51/6.56 % (2675311)Termination reason: Refutation
% 36.51/6.56 % (2675311)Time elapsed: 4.446 s
% 36.51/6.56 % (2675311)Peak memory usage: 175 MB
% 36.51/6.56 % (2675311)Instructions burned: 6752 (million)
% 36.51/6.56 % (2675311)------------------------------
% 36.51/6.56 % (2675311)------------------------------
% 36.51/6.56 % (2675304)Success in time 5.015 s
% 36.51/6.56 % Vampire exiting
%------------------------------------------------------------------------------