%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT193-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.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 55.87s 8.67s
% Output : Refutation 56.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 90
% Number of leaves : 17
% Syntax : Number of formulae : 403 ( 357 unt; 5 def)
% Number of atoms : 457 ( 456 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 110 ( 56 ~; 54 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 10 con; 0-2 aty)
% Number of variables : 782 ( 782 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0] : join(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_join) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_meet) ).
fof(f8,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f9,axiom,
! [X0] : join(X0,complement(X0)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_join) ).
fof(f10,axiom,
! [X0] : meet(X0,complement(X0)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_meet) ).
fof(f11,axiom,
! [X0,X1] :
( join(X0,X1) != one
| meet(X0,X1) != zero
| complement(X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f12,axiom,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X2)) = join(meet(X0,X1),meet(X1,join(meet(X0,X1),meet(X2,join(X0,X1))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H24) ).
fof(f13,negated_conjecture,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_distributivity) ).
fof(f14,definition,
sF0 = join(b,c),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f15,plain,
join(b,c) = sF0,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF1 = meet(a,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f17,plain,
meet(a,sF0) = sF1,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF2 = meet(a,b),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f19,plain,
meet(a,b) = sF2,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF3 = meet(a,c),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f21,plain,
meet(a,c) = sF3,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF4 = join(sF2,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f23,plain,
join(sF2,sF3) = sF4,
inference(reorient_equations,[],[f22]) ).
fof(f24,plain,
sF1 != sF4,
inference(definition_folding,[],[f13,f23,f21,f19,f17,f15]) ).
fof(f25,plain,
sF2 = meet(b,a),
inference(forward_demodulation,[],[f19,f5]) ).
fof(f26,plain,
sF3 = meet(c,a),
inference(forward_demodulation,[],[f21,f5]) ).
fof(f29,plain,
b = join(b,sF2),
inference(superposition,[],[f4,f25]) ).
fof(f32,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f33,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f32,f3]) ).
fof(f39,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f33,f6]) ).
fof(f40,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = join(X0,meet(join(X0,X1),join(X0,meet(X2,join(X0,join(X0,X1)))))),
inference(superposition,[],[f12,f3]) ).
fof(f56,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = join(X0,meet(join(X0,X1),join(X0,meet(X2,join(X0,X1))))),
inference(forward_demodulation,[],[f40,f39]) ).
fof(f63,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = join(meet(X1,X0),meet(X0,join(meet(X1,X0),meet(X2,join(X0,X1))))),
inference(superposition,[],[f12,f6]) ).
fof(f64,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f66,plain,
b = meet(b,sF0),
inference(superposition,[],[f3,f15]) ).
fof(f70,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f8,f4]) ).
fof(f71,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f32]) ).
fof(f81,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f83,plain,
! [X2,X0,X1] : join(X0,X1) = meet(join(X0,X1),join(X0,join(X1,X2))),
inference(superposition,[],[f3,f8]) ).
fof(f90,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f64,f4]) ).
fof(f91,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f64,f32]) ).
fof(f96,plain,
! [X0,X1] : join(X1,X0) = join(join(X1,X0),X0),
inference(superposition,[],[f32,f64]) ).
fof(f98,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f96,f6]) ).
fof(f101,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f91,f5]) ).
fof(f102,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f90,f5]) ).
fof(f111,plain,
! [X0,X1] :
( join(X0,X1) != one
| meet(X1,X0) != zero
| complement(X1) = X0 ),
inference(superposition,[],[f11,f6]) ).
fof(f170,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(meet(X0,X2),X1),join(X0,X1)),
inference(superposition,[],[f64,f70]) ).
fof(f173,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(X0,X1),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f170,f5]) ).
fof(f183,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f184,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f64]) ).
fof(f186,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)),
inference(superposition,[],[f7,f5]) ).
fof(f188,plain,
! [X0] : meet(a,meet(sF0,X0)) = meet(sF1,X0),
inference(superposition,[],[f7,f17]) ).
fof(f189,plain,
! [X0] : meet(b,meet(a,X0)) = meet(sF2,X0),
inference(superposition,[],[f7,f25]) ).
fof(f197,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f215,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f219,plain,
! [X0,X1] : join(X0,complement(meet(X0,X1))) = join(X0,one),
inference(superposition,[],[f70,f9]) ).
fof(f220,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f229,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f215]) ).
fof(f252,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f64,f229]) ).
fof(f256,plain,
! [X0,X1] : one = join(X0,complement(meet(X0,X1))),
inference(backward_demodulation,[],[f219,f252]) ).
fof(f303,plain,
! [X0,X1] : one = join(X1,complement(meet(X0,X1))),
inference(superposition,[],[f256,f5]) ).
fof(f314,plain,
! [X2,X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(complement(meet(X0,X1)),X2)) = join(meet(X0,complement(meet(X0,X1))),meet(complement(meet(X0,X1)),join(meet(X0,complement(meet(X0,X1))),meet(X2,one)))),
inference(superposition,[],[f12,f256]) ).
fof(f320,plain,
! [X2,X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(complement(meet(X0,X1)),X2)) = join(meet(X0,complement(meet(X0,X1))),meet(complement(meet(X0,X1)),join(meet(X0,complement(meet(X0,X1))),X2))),
inference(forward_demodulation,[],[f314,f215]) ).
fof(f325,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f331,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f343,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f325]) ).
fof(f347,plain,
! [X0] : zero = meet(zero,X0),
inference(superposition,[],[f64,f325]) ).
fof(f368,plain,
! [X0,X1] : join(meet(zero,X0),meet(X0,X1)) = join(meet(zero,X0),meet(X0,join(meet(zero,X0),meet(X1,X0)))),
inference(superposition,[],[f12,f343]) ).
fof(f371,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f32,f343]) ).
fof(f379,plain,
! [X0,X1] : join(zero,meet(X0,X1)) = join(zero,meet(X0,join(zero,meet(X1,X0)))),
inference(forward_demodulation,[],[f368,f347]) ).
fof(f382,plain,
! [X0,X1] : join(zero,meet(X0,X1)) = meet(X0,join(zero,meet(X1,X0))),
inference(forward_demodulation,[],[f379,f343]) ).
fof(f384,plain,
! [X0,X1] : meet(X0,meet(X1,X0)) = join(zero,meet(X0,X1)),
inference(forward_demodulation,[],[f382,f343]) ).
fof(f385,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f384,f343]) ).
fof(f449,plain,
! [X0,X1] : meet(X0,zero) = meet(X0,complement(join(X0,X1))),
inference(superposition,[],[f183,f10]) ).
fof(f457,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(join(X0,X2),X1),meet(X0,X1)),
inference(superposition,[],[f32,f183]) ).
fof(f464,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(X0,X1),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f457,f6]) ).
fof(f469,plain,
! [X0,X1] : zero = meet(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f449,f371]) ).
fof(f531,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(join(X0,X1),join(X0,X2)),
inference(superposition,[],[f71,f3]) ).
fof(f583,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,join(X0,X2))),
inference(forward_demodulation,[],[f531,f8]) ).
fof(f592,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X1,join(X0,X2))),
inference(forward_demodulation,[],[f583,f8]) ).
fof(f610,plain,
! [X0,X1] : zero = meet(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f331,f5]) ).
fof(f707,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,f220]) ).
fof(f715,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f707]) ).
fof(f748,plain,
! [X0,X1] : zero = meet(X1,complement(join(X0,X1))),
inference(superposition,[],[f469,f6]) ).
fof(f1014,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(meet(X0,X1),meet(X0,X2)),
inference(superposition,[],[f184,f4]) ).
fof(f1030,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,X2))),
inference(superposition,[],[f184,f5]) ).
fof(f1097,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f1014,f197]) ).
fof(f1113,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f1097,f7]) ).
fof(f1140,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(meet(X1,X0),X2)),
inference(superposition,[],[f7,f385]) ).
fof(f1146,plain,
! [X0,X1] : one = join(meet(X1,X0),complement(meet(X0,X1))),
inference(superposition,[],[f303,f385]) ).
fof(f1160,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f1140,f7]) ).
fof(f1183,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X2,X1)),
inference(forward_demodulation,[],[f1160,f1113]) ).
fof(f1403,plain,
! [X0] : meet(sF2,X0) = meet(sF2,meet(b,X0)),
inference(superposition,[],[f184,f29]) ).
fof(f1410,plain,
! [X0] : meet(sF2,X0) = meet(b,meet(X0,sF2)),
inference(forward_demodulation,[],[f1403,f197]) ).
fof(f1429,plain,
meet(sF2,sF0) = meet(b,sF1),
inference(superposition,[],[f189,f17]) ).
fof(f1432,plain,
! [X0] : meet(sF2,X0) = meet(b,meet(X0,a)),
inference(superposition,[],[f189,f5]) ).
fof(f1486,plain,
meet(b,sF1) = meet(sF0,sF2),
inference(forward_demodulation,[],[f1429,f5]) ).
fof(f1743,plain,
sF4 = join(sF2,sF4),
inference(superposition,[],[f39,f23]) ).
fof(f2321,plain,
meet(sF2,sF0) = meet(sF2,meet(b,sF1)),
inference(superposition,[],[f385,f1486]) ).
fof(f2324,plain,
meet(sF2,sF0) = meet(sF1,meet(sF2,b)),
inference(forward_demodulation,[],[f2321,f197]) ).
fof(f2330,plain,
meet(sF2,sF0) = meet(b,meet(sF1,sF2)),
inference(forward_demodulation,[],[f2324,f197]) ).
fof(f2334,plain,
meet(sF2,sF0) = meet(sF2,sF1),
inference(forward_demodulation,[],[f2330,f1410]) ).
fof(f2336,plain,
meet(sF2,sF0) = meet(sF1,sF2),
inference(forward_demodulation,[],[f2334,f5]) ).
fof(f2337,plain,
meet(sF0,sF2) = meet(sF1,sF2),
inference(forward_demodulation,[],[f2336,f5]) ).
fof(f2338,plain,
meet(b,sF1) = meet(sF1,sF2),
inference(forward_demodulation,[],[f2337,f1486]) ).
fof(f3046,plain,
! [X2,X0,X1] : join(meet(meet(X0,X1),X0),meet(X0,X2)) = join(meet(meet(X0,X1),X0),meet(X0,join(meet(meet(X0,X1),X0),meet(X2,X0)))),
inference(superposition,[],[f63,f4]) ).
fof(f3149,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = join(meet(X0,meet(X0,X1)),meet(X0,join(meet(X0,meet(X0,X1)),meet(X2,X0)))),
inference(forward_demodulation,[],[f3046,f5]) ).
fof(f3213,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,X1),meet(X0,join(meet(X0,X1),meet(X2,X0)))),
inference(forward_demodulation,[],[f3149,f102]) ).
fof(f3803,plain,
meet(sF2,c) = meet(b,sF3),
inference(superposition,[],[f1432,f26]) ).
fof(f3852,plain,
meet(b,sF3) = meet(c,sF2),
inference(forward_demodulation,[],[f3803,f5]) ).
fof(f3898,plain,
meet(sF2,c) = meet(sF2,meet(b,sF3)),
inference(superposition,[],[f385,f3852]) ).
fof(f3905,plain,
meet(sF2,c) = meet(b,meet(sF3,sF2)),
inference(forward_demodulation,[],[f3898,f197]) ).
fof(f3914,plain,
meet(sF2,sF3) = meet(sF2,c),
inference(forward_demodulation,[],[f3905,f1410]) ).
fof(f3919,plain,
meet(sF2,sF3) = meet(c,sF2),
inference(forward_demodulation,[],[f3914,f5]) ).
fof(f3920,plain,
meet(sF2,sF3) = meet(b,sF3),
inference(forward_demodulation,[],[f3919,f3852]) ).
fof(f5105,plain,
! [X0,X1] :
( one != one
| zero != meet(join(X1,complement(join(X0,X1))),X0)
| complement(join(X1,complement(join(X0,X1)))) = X0 ),
inference(superposition,[],[f111,f220]) ).
fof(f5111,plain,
! [X0] :
( one != one
| zero != meet(complement(X0),X0)
| complement(complement(X0)) = X0 ),
inference(superposition,[],[f111,f9]) ).
fof(f5125,plain,
! [X0] :
( zero != meet(complement(X0),X0)
| complement(complement(X0)) = X0 ),
inference(trivial_inequality_removal,[],[f5111]) ).
fof(f5128,plain,
! [X0,X1] :
( zero != meet(join(X1,complement(join(X0,X1))),X0)
| complement(join(X1,complement(join(X0,X1)))) = X0 ),
inference(trivial_inequality_removal,[],[f5105]) ).
fof(f5138,plain,
! [X0] :
( meet(X0,complement(X0)) != zero
| complement(complement(X0)) = X0 ),
inference(forward_demodulation,[],[f5125,f5]) ).
fof(f5144,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(join(X1,complement(join(X0,X1)))) = X0 ),
inference(forward_demodulation,[],[f5128,f5]) ).
fof(f5163,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_subsumption_resolution,[],[f5138,f10]) ).
fof(f5441,plain,
! [X0] : meet(sF1,X0) = meet(a,meet(X0,sF0)),
inference(superposition,[],[f188,f5]) ).
fof(f7740,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X0)) = meet(X0,join(meet(X0,X1),meet(X2,X0))),
inference(superposition,[],[f173,f32]) ).
fof(f7969,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,X1),join(meet(X0,X1),meet(X2,X0))),
inference(backward_demodulation,[],[f3213,f7740]) ).
fof(f8021,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,X1),meet(X2,X0)),
inference(forward_demodulation,[],[f7969,f39]) ).
fof(f8071,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X2)) = join(meet(X0,X1),meet(X2,X1)),
inference(superposition,[],[f8021,f101]) ).
fof(f8151,plain,
! [X2,X3,X0,X1] : join(X3,join(meet(X0,X1),meet(X2,X0))) = join(meet(X0,X2),join(X3,meet(X0,X1))),
inference(superposition,[],[f81,f8021]) ).
fof(f8168,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,join(meet(X0,X1),meet(X0,X2))),
inference(superposition,[],[f71,f8021]) ).
fof(f8175,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X2,X0),meet(X0,X1)),
inference(superposition,[],[f6,f8021]) ).
fof(f8217,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = join(X1,meet(X2,X0)),
inference(forward_demodulation,[],[f8168,f71]) ).
fof(f8346,plain,
! [X2,X3,X0,X1] : join(X3,meet(X2,meet(X0,X1))) = join(X3,meet(X0,meet(X1,X2))),
inference(superposition,[],[f8217,f7]) ).
fof(f8418,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(X2,X1),X0),
inference(superposition,[],[f6,f8217]) ).
fof(f8453,plain,
! [X2,X3,X0,X1] : join(join(X0,X1),meet(X2,X3)) = join(X0,join(X1,meet(X3,X2))),
inference(superposition,[],[f8,f8217]) ).
fof(f8467,plain,
! [X2,X3,X0,X1] : join(X0,join(X1,meet(X2,X3))) = join(X0,join(X1,meet(X3,X2))),
inference(forward_demodulation,[],[f8453,f8]) ).
fof(f8738,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X2,X3)) = join(meet(X3,X2),meet(X1,X0)),
inference(superposition,[],[f8217,f8418]) ).
fof(f9678,plain,
meet(a,b) = meet(sF1,b),
inference(superposition,[],[f5441,f66]) ).
fof(f9757,plain,
meet(a,b) = meet(b,sF1),
inference(forward_demodulation,[],[f9678,f5]) ).
fof(f9783,plain,
meet(b,a) = meet(b,sF1),
inference(forward_demodulation,[],[f9757,f5]) ).
fof(f9795,plain,
sF2 = meet(b,sF1),
inference(forward_demodulation,[],[f9783,f25]) ).
fof(f9828,plain,
sF2 = meet(sF1,sF2),
inference(backward_demodulation,[],[f2338,f9795]) ).
fof(f10830,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,X2)) = join(X0,meet(join(X0,X1),join(X0,X2))),
inference(superposition,[],[f464,f3]) ).
fof(f11067,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(X0,meet(X2,join(X0,X1)))),
inference(backward_demodulation,[],[f56,f10830]) ).
fof(f11985,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,join(X1,X2)),join(X0,X1)),
inference(superposition,[],[f32,f83]) ).
fof(f12029,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(join(X1,X2),join(X0,X1))),
inference(forward_demodulation,[],[f11985,f8]) ).
fof(f12102,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(join(X1,X2),X1)),
inference(forward_demodulation,[],[f12029,f592]) ).
fof(f12122,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X1,join(X2,X1))),
inference(forward_demodulation,[],[f12102,f8]) ).
fof(f12131,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,X1)),
inference(forward_demodulation,[],[f12122,f98]) ).
fof(f12302,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X2,X1),X0),
inference(superposition,[],[f6,f12131]) ).
fof(f13824,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(complement(meet(X0,X1)),one)) = join(meet(X0,complement(meet(X0,X1))),meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))),
inference(superposition,[],[f320,f9]) ).
fof(f13897,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))) = join(meet(X0,complement(meet(X0,X1))),meet(one,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f13824,f8071]) ).
fof(f13970,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))) = join(meet(X0,complement(meet(X0,X1))),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f13897,f229]) ).
fof(f14019,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))) = join(complement(meet(X0,X1)),meet(complement(meet(X0,X1)),X0)),
inference(forward_demodulation,[],[f13970,f8418]) ).
fof(f14054,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(meet(X0,complement(meet(X0,X1))),meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f14019,f4]) ).
fof(f15376,plain,
! [X0,X1] :
( one != one
| zero != meet(meet(X0,X1),complement(meet(X1,X0)))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(superposition,[],[f11,f1146]) ).
fof(f15405,plain,
! [X0,X1] :
( zero != meet(meet(X0,X1),complement(meet(X1,X0)))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(trivial_inequality_removal,[],[f15376]) ).
fof(f15428,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,complement(meet(X1,X0))))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(forward_demodulation,[],[f15405,f7]) ).
fof(f15540,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(forward_subsumption_resolution,[],[f15428,f610]) ).
fof(f19637,plain,
! [X0,X1] : join(X0,complement(meet(X0,X1))) = join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))),
inference(superposition,[],[f70,f14054]) ).
fof(f19668,plain,
! [X0,X1] :
( zero != meet(meet(X0,complement(meet(X0,X1))),join(meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))),complement(complement(meet(X0,X1)))))
| meet(X0,complement(meet(X0,X1))) = complement(join(meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))),complement(complement(meet(X0,X1))))) ),
inference(superposition,[],[f5144,f14054]) ).
fof(f19676,plain,
! [X0,X1] :
( zero != meet(X0,meet(complement(meet(X0,X1)),join(meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))),complement(complement(meet(X0,X1))))))
| meet(X0,complement(meet(X0,X1))) = complement(join(meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))),complement(complement(meet(X0,X1))))) ),
inference(forward_demodulation,[],[f19668,f7]) ).
fof(f19704,plain,
! [X0,X1] : one = join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f19637,f256]) ).
fof(f19750,plain,
! [X0,X1] :
( zero != meet(X0,meet(complement(meet(X0,X1)),join(complement(complement(meet(X0,X1))),meet(complement(meet(X0,complement(meet(X0,X1)))),complement(meet(X0,X1))))))
| meet(X0,complement(meet(X0,X1))) = complement(join(meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))),complement(complement(meet(X0,X1))))) ),
inference(forward_demodulation,[],[f19676,f8418]) ).
fof(f19800,plain,
! [X0,X1] :
( zero != meet(X0,meet(complement(meet(X0,X1)),join(complement(complement(meet(X0,X1))),meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))))
| meet(X0,complement(meet(X0,X1))) = complement(join(meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))),complement(complement(meet(X0,X1))))) ),
inference(forward_demodulation,[],[f19750,f8217]) ).
fof(f19824,plain,
! [X0,X1] :
( zero != meet(X0,meet(complement(meet(X0,X1)),join(meet(X0,X1),meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))))
| meet(X0,complement(meet(X0,X1))) = complement(join(meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))),complement(complement(meet(X0,X1))))) ),
inference(forward_demodulation,[],[f19800,f5163]) ).
fof(f19837,plain,
! [X0,X1] :
( meet(X0,complement(meet(X0,X1))) = complement(join(complement(complement(meet(X0,X1))),meet(complement(meet(X0,complement(meet(X0,X1)))),complement(meet(X0,X1)))))
| zero != meet(X0,meet(complement(meet(X0,X1)),join(meet(X0,X1),meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))))) ),
inference(forward_demodulation,[],[f19824,f8418]) ).
fof(f19845,plain,
! [X0,X1] :
( meet(X0,complement(meet(X0,X1))) = complement(join(complement(complement(meet(X0,X1))),meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))))
| zero != meet(X0,meet(complement(meet(X0,X1)),join(meet(X0,X1),meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))))) ),
inference(forward_demodulation,[],[f19837,f8217]) ).
fof(f19851,plain,
! [X0,X1] :
( meet(X0,complement(meet(X0,X1))) = complement(join(meet(X0,X1),meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))))
| zero != meet(X0,meet(complement(meet(X0,X1)),join(meet(X0,X1),meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))))) ),
inference(forward_demodulation,[],[f19845,f5163]) ).
fof(f19975,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,f19704]) ).
fof(f20023,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,[],[f19975]) ).
fof(f20060,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_subsumption_resolution,[],[f20023,f331]) ).
fof(f20124,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)),
inference(backward_demodulation,[],[f14054,f20060]) ).
fof(f20132,plain,
! [X0,X1] :
( zero != meet(X0,meet(complement(meet(X0,X1)),join(meet(X0,X1),complement(X0))))
| meet(X0,complement(meet(X0,X1))) = complement(join(meet(X0,X1),meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))) ),
inference(backward_demodulation,[],[f19851,f20060]) ).
fof(f20188,plain,
! [X0,X1] :
( zero != meet(X0,meet(complement(meet(X0,X1)),join(complement(X0),meet(X1,X0))))
| meet(X0,complement(meet(X0,X1))) = complement(join(meet(X0,X1),meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))) ),
inference(forward_demodulation,[],[f20132,f8418]) ).
fof(f20195,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),meet(complement(meet(X0,X1)),X0)),
inference(forward_demodulation,[],[f20124,f8418]) ).
fof(f20225,plain,
! [X0,X1] :
( meet(X0,complement(meet(X0,X1))) = complement(join(meet(X0,X1),complement(X0)))
| zero != meet(X0,meet(complement(meet(X0,X1)),join(complement(X0),meet(X1,X0)))) ),
inference(forward_demodulation,[],[f20188,f20060]) ).
fof(f20231,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f20195,f8217]) ).
fof(f20252,plain,
! [X0,X1] :
( meet(X0,complement(meet(X0,X1))) = complement(join(complement(X0),meet(X1,X0)))
| zero != meet(X0,meet(complement(meet(X0,X1)),join(complement(X0),meet(X1,X0)))) ),
inference(forward_demodulation,[],[f20225,f8418]) ).
fof(f20274,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,meet(complement(X0),complement(meet(complement(X0),X1)))),
inference(superposition,[],[f20231,f5163]) ).
fof(f20349,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X1),meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f20231,f15540]) ).
fof(f20365,plain,
! [X0,X1] : complement(X0) = meet(complement(X0),complement(meet(X0,X1))),
inference(superposition,[],[f3,f20231]) ).
fof(f21169,plain,
! [X2,X0,X1] : join(X2,X0) = meet(join(X2,X0),join(X2,complement(meet(complement(X0),X1)))),
inference(superposition,[],[f83,f20274]) ).
fof(f21429,plain,
! [X0,X1] : complement(X1) = meet(complement(X1),complement(meet(X0,X1))),
inference(superposition,[],[f20365,f15540]) ).
fof(f21568,plain,
! [X0,X1] : meet(X0,complement(meet(X1,complement(X0)))) = X0,
inference(superposition,[],[f21429,f5163]) ).
fof(f21593,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f21429,f3]) ).
fof(f21665,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(meet(X1,X0)),complement(X0)),
inference(superposition,[],[f32,f21429]) ).
fof(f21667,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),X2) = join(complement(meet(X1,X0)),join(complement(X0),X2)),
inference(superposition,[],[f71,f21429]) ).
fof(f21731,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),X2) = join(complement(X0),join(X2,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f21667,f81]) ).
fof(f21732,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f21665,f6]) ).
fof(f21761,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f21593,f5]) ).
fof(f22182,plain,
! [X0,X1] : complement(meet(X1,complement(X0))) = join(X0,complement(meet(X1,complement(X0)))),
inference(superposition,[],[f21732,f5163]) ).
fof(f22207,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f21732,f3]) ).
fof(f22208,plain,
! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f21732,f64]) ).
fof(f22269,plain,
! [X0,X1] : join(complement(X1),X0) = meet(join(complement(X1),X0),complement(meet(complement(X0),X1))),
inference(superposition,[],[f21169,f21732]) ).
fof(f22339,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f22208,f6]) ).
fof(f22340,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f22207,f6]) ).
fof(f22399,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(superposition,[],[f22340,f5163]) ).
fof(f22620,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(complement(join(complement(X0),X1)),X0),
inference(superposition,[],[f64,f22399]) ).
fof(f22689,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f22620,f5]) ).
fof(f22840,plain,
! [X2,X0,X1] : meet(complement(join(X1,X0)),X2) = meet(complement(join(X1,X0)),meet(complement(X0),X2)),
inference(superposition,[],[f184,f22339]) ).
fof(f22867,plain,
! [X2,X0,X1] : meet(complement(join(X1,X0)),X2) = meet(complement(X0),meet(X2,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f22840,f197]) ).
fof(f25863,plain,
! [X0,X1] : complement(complement(X0)) = join(complement(complement(meet(X0,X1))),meet(complement(meet(X0,X1)),complement(complement(X0)))),
inference(superposition,[],[f20349,f20365]) ).
fof(f25864,plain,
! [X0,X1] : complement(complement(X0)) = join(complement(complement(meet(X1,X0))),meet(complement(meet(X1,X0)),complement(complement(X0)))),
inference(superposition,[],[f20349,f21429]) ).
fof(f26006,plain,
! [X0,X1] : complement(complement(X0)) = join(complement(complement(meet(X1,X0))),meet(complement(complement(X0)),complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f25864,f8217]) ).
fof(f26007,plain,
! [X0,X1] : complement(complement(X0)) = join(complement(complement(meet(X0,X1))),meet(complement(complement(X0)),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f25863,f8217]) ).
fof(f26067,plain,
! [X0,X1] : join(complement(complement(meet(X1,X0))),meet(X0,complement(meet(X1,X0)))) = X0,
inference(forward_demodulation,[],[f26006,f5163]) ).
fof(f26068,plain,
! [X0,X1] : join(complement(complement(meet(X0,X1))),meet(X0,complement(meet(X0,X1)))) = X0,
inference(forward_demodulation,[],[f26007,f5163]) ).
fof(f26107,plain,
! [X0,X1] : join(meet(X1,X0),meet(X0,complement(meet(X1,X0)))) = X0,
inference(forward_demodulation,[],[f26067,f5163]) ).
fof(f26108,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = X0,
inference(forward_demodulation,[],[f26068,f5163]) ).
fof(f26253,plain,
! [X0,X1] : join(meet(X1,X0),meet(X1,complement(meet(X0,X1)))) = X1,
inference(superposition,[],[f26108,f15540]) ).
fof(f26269,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f71,f26108]) ).
fof(f26303,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),meet(X2,X0))),
inference(superposition,[],[f11067,f26108]) ).
fof(f26504,plain,
! [X2,X0,X1] : join(X2,meet(X1,X0)) = join(X2,meet(meet(X1,X0),complement(meet(X0,meet(X1,X2))))),
inference(superposition,[],[f26269,f186]) ).
fof(f26552,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f26269,f15540]) ).
fof(f26761,plain,
! [X2,X0,X1] : join(X2,meet(X1,X0)) = join(X2,meet(X1,meet(X0,complement(meet(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f26504,f7]) ).
fof(f27088,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = meet(X0,join(meet(X1,X0),meet(X2,X0))),
inference(superposition,[],[f11067,f26107]) ).
fof(f27314,plain,
! [X2,X0,X1] : join(X0,meet(join(X2,X0),X1)) = join(X0,meet(meet(join(X2,X0),X1),complement(meet(X0,X1)))),
inference(superposition,[],[f26552,f184]) ).
fof(f27563,plain,
! [X2,X0,X1] : join(X0,meet(join(X2,X0),X1)) = join(X0,meet(complement(meet(X0,X1)),meet(join(X2,X0),X1))),
inference(forward_demodulation,[],[f27314,f8217]) ).
fof(f27653,plain,
! [X2,X0,X1] : join(X0,meet(join(X2,X0),X1)) = join(X0,meet(X1,meet(complement(meet(X0,X1)),join(X2,X0)))),
inference(forward_demodulation,[],[f27563,f8346]) ).
fof(f27943,plain,
! [X0,X1] :
( zero != meet(meet(X0,X1),join(meet(X0,complement(meet(X1,X0))),complement(X0)))
| complement(meet(X0,X1)) = join(meet(X0,complement(meet(X1,X0))),complement(X0)) ),
inference(superposition,[],[f715,f26253]) ).
fof(f27970,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,join(meet(X0,complement(meet(X1,X0))),complement(X0))))
| complement(meet(X0,X1)) = join(meet(X0,complement(meet(X1,X0))),complement(X0)) ),
inference(forward_demodulation,[],[f27943,f7]) ).
fof(f28157,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,join(complement(X0),meet(complement(meet(X1,X0)),X0))))
| complement(meet(X0,X1)) = join(meet(X0,complement(meet(X1,X0))),complement(X0)) ),
inference(forward_demodulation,[],[f27970,f8418]) ).
fof(f28307,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,join(complement(X0),meet(X0,complement(meet(X1,X0))))))
| complement(meet(X0,X1)) = join(meet(X0,complement(meet(X1,X0))),complement(X0)) ),
inference(forward_demodulation,[],[f28157,f8217]) ).
fof(f28398,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,complement(meet(X1,X0))))
| complement(meet(X0,X1)) = join(meet(X0,complement(meet(X1,X0))),complement(X0)) ),
inference(forward_demodulation,[],[f28307,f20349]) ).
fof(f28469,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(meet(X0,complement(meet(X1,X0))),complement(X0)),
inference(forward_subsumption_resolution,[],[f28398,f610]) ).
fof(f28519,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),meet(complement(meet(X1,X0)),X0)),
inference(forward_demodulation,[],[f28469,f8418]) ).
fof(f28553,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f28519,f8217]) ).
fof(f28740,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(X2,join(meet(X0,complement(meet(X1,X0))),complement(X0))),
inference(superposition,[],[f12302,f28553]) ).
fof(f28752,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(X2,join(complement(X0),meet(X0,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f28740,f12131]) ).
fof(f28872,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(X2,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f28752,f20349]) ).
fof(f30299,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = meet(join(complement(X1),complement(X0)),complement(meet(X0,X1))),
inference(superposition,[],[f22269,f5163]) ).
fof(f30350,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(meet(complement(X1),X0),complement(join(complement(X0),X1))),
inference(superposition,[],[f21568,f22269]) ).
fof(f30410,plain,
! [X0,X1] : complement(meet(complement(X1),X0)) = join(join(complement(X0),X1),meet(complement(meet(complement(X1),X0)),complement(join(complement(X0),X1)))),
inference(superposition,[],[f26107,f22269]) ).
fof(f30417,plain,
! [X0,X1] : join(join(complement(X0),X1),complement(meet(complement(X1),X0))) = join(join(complement(X0),X1),meet(complement(meet(complement(X1),X0)),complement(join(complement(X0),X1)))),
inference(superposition,[],[f26552,f22269]) ).
fof(f30420,plain,
! [X0,X1] : join(join(complement(X0),X1),complement(meet(complement(X1),X0))) = join(complement(X0),join(X1,meet(complement(meet(complement(X1),X0)),complement(join(complement(X0),X1))))),
inference(forward_demodulation,[],[f30417,f8]) ).
fof(f30425,plain,
! [X0,X1] : complement(meet(complement(X1),X0)) = join(complement(X0),join(X1,meet(complement(meet(complement(X1),X0)),complement(join(complement(X0),X1))))),
inference(forward_demodulation,[],[f30410,f8]) ).
fof(f30460,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(complement(X1),meet(X0,complement(join(complement(X0),X1)))),
inference(forward_demodulation,[],[f30350,f7]) ).
fof(f30504,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = meet(complement(meet(X0,X1)),join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f30299,f5]) ).
fof(f30533,plain,
! [X0,X1] : join(join(complement(X0),X1),complement(meet(complement(X1),X0))) = join(complement(X0),join(X1,meet(complement(join(complement(X0),X1)),complement(meet(complement(X1),X0))))),
inference(forward_demodulation,[],[f30420,f8467]) ).
fof(f30538,plain,
! [X0,X1] : complement(meet(complement(X1),X0)) = join(complement(X0),join(X1,meet(complement(join(complement(X0),X1)),complement(meet(complement(X1),X0))))),
inference(forward_demodulation,[],[f30425,f8467]) ).
fof(f30565,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(complement(join(complement(X0),X1)),X0),
inference(forward_demodulation,[],[f30460,f22867]) ).
fof(f30621,plain,
! [X0,X1] : join(complement(X0),join(X1,meet(complement(join(complement(X0),X1)),complement(meet(complement(X1),X0))))) = join(complement(X0),join(X1,complement(meet(complement(X1),X0)))),
inference(forward_demodulation,[],[f30533,f8]) ).
fof(f30645,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f30565,f5]) ).
fof(f30684,plain,
! [X0,X1] : join(complement(X0),join(X1,meet(complement(join(complement(X0),X1)),complement(meet(complement(X1),X0))))) = join(complement(meet(complement(X1),X0)),X1),
inference(forward_demodulation,[],[f30621,f21731]) ).
fof(f30698,plain,
! [X0,X1] : meet(complement(X1),X0) = complement(join(complement(X0),X1)),
inference(backward_demodulation,[],[f22689,f30645]) ).
fof(f30729,plain,
! [X0,X1] : join(X1,complement(meet(X0,complement(X1)))) = join(complement(X0),join(X1,meet(complement(join(complement(X0),X1)),complement(meet(complement(X1),X0))))),
inference(forward_demodulation,[],[f30684,f28872]) ).
fof(f30803,plain,
! [X0,X1] : complement(meet(complement(X1),X0)) = join(complement(X0),join(X1,meet(meet(complement(X1),X0),complement(meet(complement(X1),X0))))),
inference(backward_demodulation,[],[f30538,f30698]) ).
fof(f30848,plain,
! [X0,X1] :
( meet(X0,complement(meet(X0,X1))) = meet(complement(meet(X1,X0)),X0)
| zero != meet(X0,meet(complement(meet(X0,X1)),join(complement(X0),meet(X1,X0)))) ),
inference(backward_demodulation,[],[f20252,f30698]) ).
fof(f30869,plain,
! [X0,X1] : join(X1,complement(meet(X0,complement(X1)))) = join(complement(X0),join(X1,meet(meet(complement(X1),X0),complement(meet(complement(X1),X0))))),
inference(forward_demodulation,[],[f30729,f30698]) ).
fof(f30879,plain,
! [X0,X1] :
( meet(X0,complement(meet(X0,X1))) = meet(X0,complement(meet(X1,X0)))
| zero != meet(X0,meet(complement(meet(X0,X1)),join(complement(X0),meet(X1,X0)))) ),
inference(forward_demodulation,[],[f30848,f5]) ).
fof(f30895,plain,
! [X0,X1] : join(complement(X0),join(X1,zero)) = complement(meet(complement(X1),X0)),
inference(forward_demodulation,[],[f30803,f10]) ).
fof(f30941,plain,
! [X0,X1] : join(complement(X0),join(X1,zero)) = join(X1,complement(meet(X0,complement(X1)))),
inference(forward_demodulation,[],[f30869,f10]) ).
fof(f30950,plain,
! [X0,X1] : join(zero,join(complement(X0),X1)) = complement(meet(complement(X1),X0)),
inference(forward_demodulation,[],[f30895,f81]) ).
fof(f30957,plain,
! [X0,X1] : join(complement(X0),join(X1,zero)) = complement(meet(X0,complement(X1))),
inference(forward_demodulation,[],[f30941,f22182]) ).
fof(f30961,plain,
! [X0,X1] : join(complement(X0),X1) = complement(meet(complement(X1),X0)),
inference(forward_demodulation,[],[f30950,f343]) ).
fof(f30963,plain,
! [X0,X1] : join(zero,join(complement(X0),X1)) = complement(meet(X0,complement(X1))),
inference(forward_demodulation,[],[f30957,f81]) ).
fof(f31171,plain,
! [X0,X1] : join(complement(X0),X1) = complement(meet(X0,complement(X1))),
inference(forward_demodulation,[],[f30963,f343]) ).
fof(f31409,plain,
! [X2,X0,X1] : complement(join(meet(complement(X0),X1),X2)) = meet(complement(X2),join(complement(X1),X0)),
inference(superposition,[],[f30698,f30698]) ).
fof(f31410,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(X0)),
inference(superposition,[],[f30698,f5163]) ).
fof(f31415,plain,
! [X0,X1] : meet(complement(X0),X1) = complement(join(X0,complement(X1))),
inference(superposition,[],[f30698,f6]) ).
fof(f31418,plain,
! [X0,X1] : complement(complement(meet(X0,X1))) = meet(complement(meet(X1,complement(meet(X0,X1)))),X1),
inference(superposition,[],[f30698,f20349]) ).
fof(f31587,plain,
! [X0,X1] : complement(complement(meet(X0,X1))) = meet(X1,complement(meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f31418,f5]) ).
fof(f31621,plain,
! [X0,X1] :
( meet(complement(X1),join(X0,X1)) = X0
| zero != meet(X0,join(X1,complement(join(X0,X1)))) ),
inference(backward_demodulation,[],[f5144,f31415]) ).
fof(f31649,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(join(X0,X1),X0)),
inference(backward_demodulation,[],[f21761,f31410]) ).
fof(f31721,plain,
! [X0,X1] :
( zero != meet(X0,complement(join(meet(complement(meet(X1,X0)),X0),meet(X0,X1))))
| meet(X0,complement(meet(X0,X1))) = meet(X0,complement(meet(X1,X0))) ),
inference(backward_demodulation,[],[f30879,f31409]) ).
fof(f31725,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = complement(join(meet(complement(complement(X0)),X1),meet(X0,X1))),
inference(backward_demodulation,[],[f30504,f31409]) ).
fof(f31776,plain,
! [X0,X1] : complement(complement(meet(X0,X1))) = meet(X1,join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[],[f31587,f31171]) ).
fof(f31840,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X0,join(X1,X0))),
inference(forward_demodulation,[],[f31649,f8]) ).
fof(f31850,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = complement(join(meet(X1,X0),meet(X1,complement(complement(X0))))),
inference(forward_demodulation,[],[f31725,f8738]) ).
fof(f31854,plain,
! [X0,X1] :
( zero != meet(X0,complement(join(meet(X0,X1),meet(X0,complement(meet(X1,X0))))))
| meet(X0,complement(meet(X0,X1))) = meet(X0,complement(meet(X1,X0))) ),
inference(forward_demodulation,[],[f31721,f8175]) ).
fof(f31888,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[],[f31776,f5163]) ).
fof(f31917,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f31840,f98]) ).
fof(f31924,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = complement(join(meet(X1,X0),meet(X1,X0))),
inference(forward_demodulation,[],[f31850,f5163]) ).
fof(f31927,plain,
! [X0,X1] :
( meet(X0,complement(X0)) != zero
| meet(X0,complement(meet(X0,X1))) = meet(X0,complement(meet(X1,X0))) ),
inference(forward_demodulation,[],[f31854,f26253]) ).
fof(f31948,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f31924,f2]) ).
fof(f31949,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = meet(X0,complement(meet(X1,X0))),
inference(forward_subsumption_resolution,[],[f31927,f10]) ).
fof(f32153,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(meet(X0,complement(X1)),X1))),
inference(superposition,[],[f26552,f31410]) ).
fof(f32155,plain,
! [X0,X1] : complement(meet(X0,complement(X1))) = join(complement(complement(X1)),complement(join(meet(X0,complement(X1)),X1))),
inference(superposition,[],[f20349,f31410]) ).
fof(f32164,plain,
! [X0,X1] : join(X1,complement(X0)) = join(X1,complement(join(meet(complement(X0),X1),X0))),
inference(superposition,[],[f26269,f31410]) ).
fof(f32214,plain,
! [X2,X0,X1] : join(X2,complement(join(X0,X1))) = join(X2,meet(complement(X0),complement(X1))),
inference(superposition,[],[f8217,f31410]) ).
fof(f32216,plain,
! [X2,X0,X1] : join(complement(join(X0,X1)),X2) = join(X2,meet(complement(X0),complement(X1))),
inference(superposition,[],[f8418,f31410]) ).
fof(f32264,plain,
! [X2,X0,X1] : join(complement(join(X0,X1)),X2) = join(X2,complement(join(X1,X0))),
inference(forward_demodulation,[],[f32216,f31410]) ).
fof(f32266,plain,
! [X2,X0,X1] : join(X2,complement(join(X0,X1))) = join(X2,complement(join(X1,X0))),
inference(forward_demodulation,[],[f32214,f31410]) ).
fof(f32394,plain,
! [X0,X1] : join(X1,complement(X0)) = join(X1,complement(join(X0,meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f32164,f31917]) ).
fof(f32403,plain,
! [X0,X1] : complement(meet(X0,complement(X1))) = complement(meet(complement(X1),join(meet(X0,complement(X1)),X1))),
inference(forward_demodulation,[],[f32155,f31948]) ).
fof(f32405,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X1,meet(X0,complement(X1))))),
inference(forward_demodulation,[],[f32153,f31917]) ).
fof(f32562,plain,
! [X0,X1] : complement(meet(X0,complement(X1))) = join(complement(join(meet(X0,complement(X1)),X1)),X1),
inference(forward_demodulation,[],[f32403,f30961]) ).
fof(f32658,plain,
! [X0,X1] : complement(meet(X0,complement(X1))) = join(X1,complement(join(X1,meet(X0,complement(X1))))),
inference(forward_demodulation,[],[f32562,f32264]) ).
fof(f32698,plain,
! [X0,X1] : join(complement(X0),X1) = join(X1,complement(join(X1,meet(X0,complement(X1))))),
inference(forward_demodulation,[],[f32658,f31171]) ).
fof(f32749,plain,
! [X0,X1] : join(X0,complement(X1)) = complement(meet(complement(X0),X1)),
inference(superposition,[],[f31948,f5163]) ).
fof(f33121,plain,
! [X2,X0,X1] : complement(join(meet(complement(X0),X1),X2)) = meet(complement(X2),join(X0,complement(X1))),
inference(superposition,[],[f31410,f32749]) ).
fof(f34003,plain,
! [X0,X1] : meet(complement(X0),complement(complement(join(X0,X1)))) = meet(complement(X0),complement(meet(complement(X0),complement(X1)))),
inference(superposition,[],[f31949,f31410]) ).
fof(f34006,plain,
! [X0,X1] : meet(X1,join(X0,complement(X1))) = meet(X1,complement(meet(X1,complement(X0)))),
inference(superposition,[],[f31949,f32749]) ).
fof(f34117,plain,
! [X2,X0,X1] : meet(X0,meet(complement(meet(X1,X0)),X2)) = meet(X2,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f197,f31949]) ).
fof(f34287,plain,
! [X0,X1] : meet(X1,join(complement(X1),X0)) = meet(X1,join(X0,complement(X1))),
inference(forward_demodulation,[],[f34006,f31171]) ).
fof(f34288,plain,
! [X0,X1] : meet(complement(X0),complement(complement(join(X0,X1)))) = complement(join(meet(complement(X0),complement(X1)),X0)),
inference(forward_demodulation,[],[f34003,f31410]) ).
fof(f34387,plain,
! [X0,X1] : meet(complement(X0),complement(complement(join(X0,X1)))) = complement(join(X0,meet(complement(X0),complement(X1)))),
inference(forward_demodulation,[],[f34288,f31917]) ).
fof(f34454,plain,
! [X0,X1] : complement(join(X0,complement(join(X1,X0)))) = meet(complement(X0),complement(complement(join(X0,X1)))),
inference(forward_demodulation,[],[f34387,f31410]) ).
fof(f34487,plain,
! [X0,X1] : complement(join(X0,complement(join(X1,X0)))) = complement(join(complement(join(X0,X1)),X0)),
inference(forward_demodulation,[],[f34454,f31410]) ).
fof(f34508,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = complement(join(X0,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f34487,f30698]) ).
fof(f34523,plain,
! [X0,X1] : meet(complement(X0),join(X1,X0)) = meet(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f34508,f31415]) ).
fof(f34629,plain,
! [X2,X0,X1] : meet(complement(X0),meet(join(X1,X0),X2)) = meet(X2,meet(complement(X0),join(X0,X1))),
inference(superposition,[],[f197,f34523]) ).
fof(f35891,plain,
! [X0,X1] : meet(join(X0,X1),join(complement(join(X0,X1)),X0)) = X0,
inference(superposition,[],[f31888,f3]) ).
fof(f36126,plain,
! [X0,X1] : meet(join(X0,X1),join(X0,complement(join(X0,X1)))) = X0,
inference(forward_demodulation,[],[f35891,f34287]) ).
fof(f36451,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f184,f36126]) ).
fof(f36460,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,complement(join(X0,X1))),X2)) = join(X0,meet(join(X0,complement(join(X0,X1))),join(X0,meet(X2,join(join(X0,X1),join(X0,complement(join(X0,X1)))))))),
inference(superposition,[],[f12,f36126]) ).
fof(f36565,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,complement(join(X0,X1))),X2)) = meet(join(X0,complement(join(X0,X1))),join(X0,meet(X2,join(join(X0,X1),join(X0,complement(join(X0,X1))))))),
inference(forward_demodulation,[],[f36460,f10830]) ).
fof(f36642,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,complement(join(X0,X1))),X2)) = meet(join(X0,complement(join(X0,X1))),join(X0,meet(X2,join(X0,join(X1,join(X0,complement(join(X0,X1)))))))),
inference(forward_demodulation,[],[f36565,f8]) ).
fof(f36702,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,complement(join(X0,X1))),X2)) = meet(join(X0,complement(join(X0,X1))),join(X0,meet(X2,join(X0,join(X1,complement(join(X0,X1))))))),
inference(forward_demodulation,[],[f36642,f592]) ).
fof(f36723,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,complement(join(X0,X1))),X2)) = meet(join(X0,complement(join(X0,X1))),join(X0,meet(X2,one))),
inference(forward_demodulation,[],[f36702,f220]) ).
fof(f36730,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,complement(join(X0,X1))),X2)) = meet(join(X0,complement(join(X0,X1))),join(X0,X2)),
inference(forward_demodulation,[],[f36723,f215]) ).
fof(f36753,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f36451,f6]) ).
fof(f36905,plain,
! [X0,X1] : join(X1,complement(join(X1,X0))) = join(meet(X0,X1),meet(join(X1,complement(join(X1,X0))),complement(meet(X0,X1)))),
inference(superposition,[],[f26107,f36451]) ).
fof(f36957,plain,
! [X0,X1] : join(X1,complement(join(X1,X0))) = join(meet(X0,X1),meet(complement(meet(X0,X1)),join(X1,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f36905,f8217]) ).
fof(f37086,plain,
! [X0,X1] :
( complement(X0) = join(X1,complement(join(X0,X1)))
| meet(X0,X1) != zero ),
inference(backward_demodulation,[],[f715,f36753]) ).
fof(f37092,plain,
! [X0,X1] :
( meet(complement(X1),join(X0,X1)) = X0
| meet(X0,X1) != zero ),
inference(backward_demodulation,[],[f31621,f36753]) ).
fof(f37113,plain,
! [X0,X1] : join(X1,complement(join(X1,X0))) = join(meet(X0,X1),complement(join(meet(complement(X1),join(X1,X0)),meet(X0,X1)))),
inference(forward_demodulation,[],[f36957,f33121]) ).
fof(f37220,plain,
! [X0,X1] : join(X1,complement(join(X1,X0))) = join(meet(X0,X1),complement(join(meet(X0,X1),meet(complement(X1),join(X1,X0))))),
inference(forward_demodulation,[],[f37113,f32266]) ).
fof(f37963,plain,
! [X0,X1] :
( meet(complement(complement(join(X0,X1))),complement(X0)) = X1
| zero != meet(X1,complement(join(X0,X1)))
| meet(X0,X1) != zero ),
inference(superposition,[],[f37092,f37086]) ).
fof(f37991,plain,
! [X0,X1] :
( meet(complement(complement(join(X0,X1))),complement(X0)) = X1
| meet(X0,X1) != zero ),
inference(forward_subsumption_resolution,[],[f37963,f748]) ).
fof(f38086,plain,
! [X0,X1] :
( meet(complement(X0),complement(complement(join(X0,X1)))) = X1
| meet(X0,X1) != zero ),
inference(forward_demodulation,[],[f37991,f5]) ).
fof(f38147,plain,
! [X0,X1] :
( complement(join(complement(join(X0,X1)),X0)) = X1
| meet(X0,X1) != zero ),
inference(forward_demodulation,[],[f38086,f31410]) ).
fof(f38193,plain,
! [X0,X1] :
( meet(complement(X0),join(X0,X1)) = X1
| meet(X0,X1) != zero ),
inference(forward_demodulation,[],[f38147,f30698]) ).
fof(f38275,plain,
! [X0,X1] :
( meet(X1,complement(meet(X1,X0))) = meet(complement(X0),join(X0,X1))
| zero != meet(X0,meet(X1,complement(meet(X1,X0)))) ),
inference(superposition,[],[f38193,f26269]) ).
fof(f38502,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(complement(X0),join(X0,X1)),
inference(forward_subsumption_resolution,[],[f38275,f610]) ).
fof(f38729,plain,
! [X0,X1] : join(meet(X1,X0),meet(complement(X0),join(X0,X1))) = X1,
inference(superposition,[],[f26108,f38502]) ).
fof(f38743,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(X1,meet(complement(X0),join(X0,X1))),
inference(superposition,[],[f102,f38502]) ).
fof(f38766,plain,
! [X2,X0,X1] : meet(X1,meet(X2,complement(meet(X1,X0)))) = meet(meet(complement(X0),join(X0,X1)),X2),
inference(superposition,[],[f1183,f38502]) ).
fof(f38803,plain,
! [X0,X1] : complement(meet(complement(X0),join(X0,complement(X1)))) = join(X1,complement(complement(meet(complement(X1),X0)))),
inference(superposition,[],[f32749,f38502]) ).
fof(f38819,plain,
! [X0,X1] : meet(X0,complement(X1)) = meet(X0,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f1030,f38502]) ).
fof(f38835,plain,
! [X2,X0,X1] : meet(X2,meet(X0,complement(meet(X0,X1)))) = meet(complement(X1),meet(join(X1,X0),X2)),
inference(superposition,[],[f197,f38502]) ).
fof(f38932,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = meet(X0,complement(X1)),
inference(forward_demodulation,[],[f38819,f102]) ).
fof(f38941,plain,
! [X0,X1] : join(X1,meet(complement(X1),X0)) = complement(meet(complement(X0),join(X0,complement(X1)))),
inference(forward_demodulation,[],[f38803,f5163]) ).
fof(f38973,plain,
! [X2,X0,X1] : meet(X1,meet(X2,complement(meet(X1,X0)))) = meet(complement(X0),meet(join(X0,X1),X2)),
inference(forward_demodulation,[],[f38766,f7]) ).
fof(f38990,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f38743,f1030]) ).
fof(f39001,plain,
! [X0,X1] : join(meet(X0,X1),complement(X0)) = join(X1,complement(join(X1,X0))),
inference(backward_demodulation,[],[f37220,f38729]) ).
fof(f39135,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(X1))),
inference(backward_demodulation,[],[f26269,f38932]) ).
fof(f39179,plain,
! [X2,X0,X1] : meet(X0,meet(complement(meet(X1,X0)),X2)) = meet(X2,meet(X0,complement(X1))),
inference(backward_demodulation,[],[f34117,f38932]) ).
fof(f39219,plain,
! [X2,X0,X1] : meet(X2,meet(X0,complement(X1))) = meet(complement(X1),meet(join(X1,X0),X2)),
inference(backward_demodulation,[],[f38835,f38932]) ).
fof(f39243,plain,
! [X2,X0,X1] : join(X2,meet(X1,X0)) = join(X2,meet(X1,meet(X0,complement(meet(X1,X2))))),
inference(backward_demodulation,[],[f26761,f38932]) ).
fof(f39289,plain,
! [X0,X1] : join(X1,meet(complement(X1),X0)) = join(complement(join(X0,complement(X1))),X0),
inference(forward_demodulation,[],[f38941,f30961]) ).
fof(f39350,plain,
! [X2,X0,X1] : meet(X2,meet(X1,complement(X0))) = meet(complement(X0),meet(join(X1,X0),X2)),
inference(backward_demodulation,[],[f34629,f38990]) ).
fof(f39461,plain,
! [X0,X1] : join(X1,complement(join(X1,X0))) = join(complement(X0),meet(X1,X0)),
inference(forward_demodulation,[],[f39001,f8418]) ).
fof(f39687,plain,
! [X2,X0,X1] : meet(X2,meet(X1,complement(X0))) = meet(X1,meet(X2,complement(meet(X1,X0)))),
inference(backward_demodulation,[],[f38973,f39219]) ).
fof(f39800,plain,
! [X2,X0,X1] : join(X0,meet(join(X2,X0),X1)) = join(X0,meet(join(X2,X0),meet(X1,complement(X0)))),
inference(backward_demodulation,[],[f27653,f39179]) ).
fof(f39884,plain,
! [X0,X1] : join(X0,complement(join(X1,X0))) = join(X0,complement(X1)),
inference(backward_demodulation,[],[f32405,f39135]) ).
fof(f39885,plain,
! [X0,X1] : join(complement(X0),X1) = join(X1,complement(join(X1,X0))),
inference(backward_demodulation,[],[f32698,f39135]) ).
fof(f39931,plain,
! [X0,X1] : join(X1,meet(complement(X1),X0)) = join(X0,complement(join(complement(X1),X0))),
inference(forward_demodulation,[],[f39289,f32264]) ).
fof(f40151,plain,
! [X2,X0,X1] : join(X2,meet(X1,X0)) = join(X2,meet(X0,meet(X1,complement(X2)))),
inference(backward_demodulation,[],[f39243,f39687]) ).
fof(f40204,plain,
! [X2,X0,X1] : join(X0,meet(join(X2,X0),X1)) = join(X0,meet(complement(X0),meet(join(X2,X0),X1))),
inference(forward_demodulation,[],[f39800,f8346]) ).
fof(f40269,plain,
! [X2,X0,X1] : join(X0,meet(join(complement(X1),X0),X2)) = meet(join(complement(X1),X0),join(X0,X2)),
inference(backward_demodulation,[],[f36730,f39885]) ).
fof(f40287,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),meet(X1,X0)),
inference(backward_demodulation,[],[f39461,f39885]) ).
fof(f40375,plain,
! [X0,X1] : join(X1,meet(complement(X1),X0)) = join(X0,complement(complement(X1))),
inference(forward_demodulation,[],[f39931,f39884]) ).
fof(f40555,plain,
! [X2,X0,X1] : join(X0,meet(join(X2,X0),X1)) = join(X0,meet(X1,meet(X2,complement(X0)))),
inference(forward_demodulation,[],[f40204,f39350]) ).
fof(f40781,plain,
! [X0,X1] : join(X0,X1) = join(X1,meet(complement(X1),X0)),
inference(forward_demodulation,[],[f40375,f5163]) ).
fof(f40870,plain,
! [X2,X0,X1] : join(X0,meet(join(X2,X0),X1)) = join(X0,meet(X2,X1)),
inference(forward_demodulation,[],[f40555,f40151]) ).
fof(f40945,plain,
! [X0,X1] : join(X1,complement(X0)) = join(X1,complement(join(X1,X0))),
inference(backward_demodulation,[],[f32394,f40781]) ).
fof(f41053,plain,
! [X2,X0,X1] : join(X0,meet(complement(X1),X2)) = meet(join(complement(X1),X0),join(X0,X2)),
inference(backward_demodulation,[],[f40269,f40870]) ).
fof(f42346,plain,
join(complement(sF3),meet(b,sF3)) = join(complement(sF3),sF2),
inference(superposition,[],[f40287,f3920]) ).
fof(f42402,plain,
join(complement(sF3),meet(b,sF3)) = join(sF2,complement(sF3)),
inference(forward_demodulation,[],[f42346,f6]) ).
fof(f42472,plain,
join(sF2,complement(sF3)) = join(complement(sF3),b),
inference(forward_demodulation,[],[f42402,f40287]) ).
fof(f42526,plain,
join(sF2,complement(sF3)) = join(b,complement(sF3)),
inference(forward_demodulation,[],[f42472,f6]) ).
fof(f43474,plain,
join(sF2,complement(sF4)) = join(complement(sF3),sF2),
inference(superposition,[],[f39885,f23]) ).
fof(f43578,plain,
join(sF2,complement(sF4)) = join(sF2,complement(sF3)),
inference(forward_demodulation,[],[f43474,f6]) ).
fof(f43690,plain,
join(sF2,complement(sF4)) = join(b,complement(sF3)),
inference(forward_demodulation,[],[f43578,f42526]) ).
fof(f50995,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X0,X1),join(X1,X2)),
inference(superposition,[],[f41053,f5163]) ).
fof(f51729,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f50995,f4]) ).
fof(f51730,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = meet(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f50995,f32]) ).
fof(f51898,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = meet(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f183,f50995]) ).
fof(f51900,plain,
! [X2,X0,X1] : meet(X2,join(X1,X0)) = meet(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f1030,f50995]) ).
fof(f52038,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(X2,meet(X0,X1))),
inference(backward_demodulation,[],[f26303,f51900]) ).
fof(f52039,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X0)) = meet(X0,join(X2,meet(X0,X1))),
inference(backward_demodulation,[],[f7740,f51900]) ).
fof(f52040,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = meet(X0,join(X2,meet(X1,X0))),
inference(backward_demodulation,[],[f27088,f51900]) ).
fof(f52480,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X1,X0),meet(X0,X2)),
inference(forward_demodulation,[],[f52040,f51900]) ).
fof(f52481,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X0)) = meet(X0,join(X2,X1)),
inference(forward_demodulation,[],[f52039,f51898]) ).
fof(f52482,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(X2,X1)),
inference(forward_demodulation,[],[f52038,f51898]) ).
fof(f52815,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(meet(X1,X0),X2)),
inference(backward_demodulation,[],[f51730,f52480]) ).
fof(f52916,plain,
! [X2,X3,X0,X1] : join(meet(X0,X2),join(X3,meet(X0,X1))) = join(X3,meet(X0,join(X2,X1))),
inference(backward_demodulation,[],[f8151,f52481]) ).
fof(f52949,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,join(X2,X1)),
inference(backward_demodulation,[],[f51729,f52482]) ).
fof(f55260,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = join(join(meet(X0,X2),X1),meet(X0,join(X1,X2))),
inference(superposition,[],[f32,f52949]) ).
fof(f55354,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = join(meet(X0,X2),join(X1,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f55260,f8]) ).
fof(f55489,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = join(X1,meet(X0,join(X2,join(X1,X2)))),
inference(forward_demodulation,[],[f55354,f52916]) ).
fof(f55589,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = join(X1,meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f55489,f98]) ).
fof(f55986,plain,
! [X0] : join(b,meet(X0,sF0)) = join(meet(X0,c),b),
inference(superposition,[],[f55589,f15]) ).
fof(f56183,plain,
! [X0] : join(b,meet(X0,sF0)) = join(b,meet(c,X0)),
inference(forward_demodulation,[],[f55986,f8418]) ).
fof(f56503,plain,
! [X0] : meet(sF1,join(b,X0)) = meet(sF1,join(sF2,X0)),
inference(superposition,[],[f52815,f9795]) ).
fof(f58650,plain,
! [X0] : join(meet(sF1,X0),sF2) = meet(sF1,join(sF2,X0)),
inference(superposition,[],[f52482,f9828]) ).
fof(f58761,plain,
! [X0] : join(meet(sF1,X0),sF2) = meet(sF1,join(b,X0)),
inference(forward_demodulation,[],[f58650,f56503]) ).
fof(f58938,plain,
! [X0] : join(sF2,meet(X0,sF1)) = meet(sF1,join(b,X0)),
inference(forward_demodulation,[],[f58761,f8418]) ).
fof(f59882,plain,
join(b,sF1) = join(b,meet(c,a)),
inference(superposition,[],[f56183,f17]) ).
fof(f59972,plain,
join(b,sF1) = join(b,sF3),
inference(forward_demodulation,[],[f59882,f26]) ).
fof(f60049,plain,
join(b,complement(sF3)) = join(b,complement(join(b,sF1))),
inference(superposition,[],[f40945,f59972]) ).
fof(f60059,plain,
join(complement(sF1),b) = join(b,complement(sF3)),
inference(forward_demodulation,[],[f60049,f39885]) ).
fof(f60071,plain,
join(b,complement(sF1)) = join(b,complement(sF3)),
inference(forward_demodulation,[],[f60059,f6]) ).
fof(f60080,plain,
join(sF2,complement(sF4)) = join(b,complement(sF1)),
inference(backward_demodulation,[],[f43690,f60071]) ).
fof(f60113,plain,
join(sF2,complement(join(b,complement(sF1)))) = join(sF2,complement(complement(sF4))),
inference(superposition,[],[f40945,f60080]) ).
fof(f60123,plain,
join(sF2,sF4) = join(sF2,complement(join(b,complement(sF1)))),
inference(forward_demodulation,[],[f60113,f5163]) ).
fof(f60149,plain,
join(sF2,sF4) = join(sF2,meet(complement(b),sF1)),
inference(forward_demodulation,[],[f60123,f31415]) ).
fof(f60176,plain,
join(sF2,sF4) = meet(sF1,join(b,complement(b))),
inference(forward_demodulation,[],[f60149,f58938]) ).
fof(f60186,plain,
join(sF2,sF4) = meet(sF1,one),
inference(forward_demodulation,[],[f60176,f9]) ).
fof(f60199,plain,
join(sF2,sF4) = meet(one,sF1),
inference(forward_demodulation,[],[f60186,f5]) ).
fof(f60206,plain,
sF1 = join(sF2,sF4),
inference(forward_demodulation,[],[f60199,f229]) ).
fof(f60212,plain,
sF1 = sF4,
inference(backward_demodulation,[],[f1743,f60206]) ).
fof(f60217,plain,
$false,
inference(forward_subsumption_resolution,[],[f60212,f24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT193-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n006.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 14:04:40 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.15/3.21 % (3000578)Input is clausal, will run a generic CNF schedule.
% 18.15/3.21 % (3000620)dis-21_1_sil=8000:lcm=predicate:random_seed=734443483:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 18.15/3.21 % (3000620)Refutation not found, incomplete strategy
% 18.15/3.21 % (3000620)------------------------------
% 18.15/3.21 % (3000620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.15/3.21 % (3000620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.15/3.21 % (3000620)CaDiCaL version: 2.1.3
% 18.15/3.21 % (3000620)Termination reason: Refutation not found, incomplete strategy
% 18.15/3.21 % (3000620)Time elapsed: 0.001 s
% 18.15/3.21 % (3000620)Peak memory usage: 88 MB
% 18.15/3.21 % (3000620)Instructions burned: 1 (million)
% 18.15/3.21 % (3000615)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1859039999:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 18.15/3.21 % (3000614)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=3896703669:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 18.15/3.21 % (3000619)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=813207976:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 18.15/3.21 % (3000617)lrs+10_1_sil=8000:sp=occurrence:random_seed=1851584381:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 18.15/3.21 % (3000616)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=525303844:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 18.15/3.21 % (3000618)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2118667059:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 18.15/3.21 % (3000617)Instruction limit reached!
% 18.15/3.21 % (3000617)------------------------------
% 18.15/3.21 % (3000617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.15/3.21 % (3000617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.15/3.21 % (3000617)CaDiCaL version: 2.1.3
% 18.15/3.21 % (3000617)Termination reason: Instruction limit
% 18.15/3.21 % (3000617)Termination phase: Saturation
% 18.15/3.21 % (3000617)Time elapsed: 0.069 s
% 18.15/3.21 % (3000617)Peak memory usage: 88 MB
% 18.15/3.21 % (3000617)Instructions burned: 108 (million)
% 18.15/3.21 % (3000618)Instruction limit reached!
% 18.15/3.21 % (3000618)------------------------------
% 18.15/3.21 % (3000618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.15/3.21 % (3000618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.15/3.21 % (3000618)CaDiCaL version: 2.1.3
% 18.15/3.21 % (3000618)Termination reason: Instruction limit
% 18.15/3.21 % (3000618)Termination phase: Saturation
% 18.15/3.21 % (3000618)Time elapsed: 0.078 s
% 18.15/3.21 % (3000618)Peak memory usage: 89 MB
% 18.15/3.21 % (3000618)Instructions burned: 114 (million)
% 18.15/3.21 % (3000619)Instruction limit reached!
% 18.15/3.21 % (3000619)------------------------------
% 18.15/3.21 % (3000619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.15/3.21 % (3000619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.15/3.21 % (3000619)CaDiCaL version: 2.1.3
% 18.15/3.21 % (3000619)Termination reason: Instruction limit
% 18.15/3.21 % (3000619)Termination phase: Saturation
% 18.15/3.21 % (3000619)Time elapsed: 0.139 s
% 18.15/3.21 % (3000619)Peak memory usage: 89 MB
% 18.15/3.21 % (3000619)Instructions burned: 181 (million)
% 18.15/3.21 % (3000620)------------------------------
% 18.15/3.21 % (3000620)------------------------------
% 18.15/3.21 % (3000649)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=1643274282:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 18.15/3.21 % (3000649)Refutation not found, incomplete strategy
% 18.15/3.21 % (3000649)------------------------------
% 18.15/3.21 % (3000649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.15/3.21 % (3000649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.15/3.21 % (3000649)CaDiCaL version: 2.1.3
% 18.15/3.21 % (3000649)Termination reason: Refutation not found, incomplete strategy
% 18.15/3.21 % (3000649)Time elapsed: 0.002 s
% 18.15/3.21 % (3000649)Peak memory usage: 87 MB
% 35.39/5.79 % (3000651)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=416450929: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)
% 35.39/5.79 % (3000651)Refutation not found, incomplete strategy
% 35.39/5.79 % (3000651)------------------------------
% 35.39/5.79 % (3000651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.39/5.79 % (3000651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.39/5.79 % (3000651)CaDiCaL version: 2.1.3
% 35.39/5.79 % (3000651)Termination reason: Refutation not found, incomplete strategy
% 35.39/5.79 % (3000651)Time elapsed: 0.003 s
% 35.39/5.79 % (3000651)Peak memory usage: 88 MB
% 35.39/5.79 % (3000651)Instructions burned: 1 (million)
% 35.39/5.79 % (3000658)lrs+10_64_to=lpo:sil=8000:random_seed=1895059603:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 35.39/5.79 % (3000657)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1795740915:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 35.39/5.79 % (3000657)Refutation not found, incomplete strategy
% 35.39/5.79 % (3000657)------------------------------
% 35.39/5.79 % (3000657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.39/5.79 % (3000657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.39/5.79 % (3000657)CaDiCaL version: 2.1.3
% 35.39/5.79 % (3000657)Termination reason: Refutation not found, incomplete strategy
% 35.39/5.79 % (3000657)Time elapsed: 0.001 s
% 35.39/5.79 % (3000657)Peak memory usage: 88 MB
% 35.39/5.79 % (3000658)Instruction limit reached!
% 35.39/5.79 % (3000658)------------------------------
% 35.39/5.79 % (3000658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.39/5.79 % (3000658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.39/5.79 % (3000658)CaDiCaL version: 2.1.3
% 35.39/5.79 % (3000658)Termination reason: Instruction limit
% 35.39/5.79 % (3000658)Termination phase: Saturation
% 35.39/5.79 % (3000658)Time elapsed: 0.066 s
% 35.39/5.79 % (3000658)Peak memory usage: 88 MB
% 35.39/5.79 % (3000658)Instructions burned: 128 (million)
% 35.39/5.79 % (3000674)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1572069749:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 35.39/5.79 % (3000649)------------------------------
% 35.39/5.79 % (3000649)------------------------------
% 35.39/5.79 % (3000657)------------------------------
% 35.39/5.79 % (3000657)------------------------------
% 35.39/5.79 % (3000651)------------------------------
% 35.39/5.79 % (3000651)------------------------------
% 35.39/5.79 % (3000674)Instruction limit reached!
% 35.39/5.79 % (3000674)------------------------------
% 35.39/5.79 % (3000674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.39/5.79 % (3000674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.39/5.79 % (3000674)CaDiCaL version: 2.1.3
% 35.39/5.79 % (3000674)Termination reason: Instruction limit
% 35.39/5.79 % (3000674)Termination phase: Saturation
% 35.39/5.79 % (3000674)Time elapsed: 0.107 s
% 35.39/5.79 % (3000674)Peak memory usage: 90 MB
% 35.39/5.79 % (3000674)Instructions burned: 196 (million)
% 35.39/5.79 % (3000679)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1850127161:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 35.39/5.79 % (3000678)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3190240383:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 35.39/5.79 % (3000683)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2114067432:i=107_2990 on theBenchmark for (2990ds/107Mi)
% 35.39/5.79 % (3000683)Refutation not found, incomplete strategy
% 35.39/5.79 % (3000683)------------------------------
% 35.39/5.79 % (3000683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.39/5.79 % (3000683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.39/5.79 % (3000683)CaDiCaL version: 2.1.3
% 35.39/5.79 % (3000683)Termination reason: Refutation not found, incomplete strategy
% 35.39/5.79 % (3000683)Time elapsed: 0.002 s
% 35.39/5.79 % (3000683)Peak memory usage: 87 MB
% 35.39/5.79 % (3000681)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=1963730470:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi)
% 55.87/8.67 % (3000678)Instruction limit reached!
% 55.87/8.67 % (3000678)------------------------------
% 55.87/8.67 % (3000678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.87/8.67 % (3000678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.87/8.67 % (3000678)CaDiCaL version: 2.1.3
% 55.87/8.67 % (3000678)Termination reason: Instruction limit
% 55.87/8.67 % (3000678)Termination phase: Saturation
% 55.87/8.67 % (3000678)Time elapsed: 0.158 s
% 55.87/8.67 % (3000678)Peak memory usage: 90 MB
% 55.87/8.67 % (3000678)Instructions burned: 157 (million)
% 55.87/8.67 % (3000681)Instruction limit reached!
% 55.87/8.67 % (3000681)------------------------------
% 55.87/8.67 % (3000681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.87/8.67 % (3000681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.87/8.67 % (3000681)CaDiCaL version: 2.1.3
% 55.87/8.67 % (3000681)Termination reason: Instruction limit
% 55.87/8.67 % (3000681)Termination phase: Saturation
% 55.87/8.67 % (3000681)Time elapsed: 0.113 s
% 55.87/8.67 % (3000681)Peak memory usage: 89 MB
% 55.87/8.67 % (3000681)Instructions burned: 107 (million)
% 55.87/8.67 % (3000693)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2519068739:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi)
% 55.87/8.67 % (3000683)------------------------------
% 55.87/8.67 % (3000683)------------------------------
% 55.87/8.67 % (3000694)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1157089246:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi)
% 55.87/8.67 % (3000693)Instruction limit reached!
% 55.87/8.67 % (3000693)------------------------------
% 55.87/8.67 % (3000693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.87/8.67 % (3000693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.87/8.67 % (3000693)CaDiCaL version: 2.1.3
% 55.87/8.67 % (3000693)Termination reason: Instruction limit
% 55.87/8.67 % (3000693)Termination phase: Saturation
% 55.87/8.67 % (3000693)Time elapsed: 0.243 s
% 55.87/8.67 % (3000693)Peak memory usage: 90 MB
% 55.87/8.67 % (3000693)Instructions burned: 243 (million)
% 55.87/8.67 % (3000696)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=58416540:i=134:sd=2:doe=on:ss=axioms:sgt=14_2984 on theBenchmark for (2984ds/134Mi)
% 55.87/8.67 % (3000696)Instruction limit reached!
% 55.87/8.67 % (3000696)------------------------------
% 55.87/8.67 % (3000696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.87/8.67 % (3000696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.87/8.67 % (3000696)CaDiCaL version: 2.1.3
% 55.87/8.67 % (3000696)Termination reason: Instruction limit
% 55.87/8.67 % (3000696)Termination phase: Saturation
% 55.87/8.67 % (3000696)Time elapsed: 0.139 s
% 55.87/8.67 % (3000696)Peak memory usage: 89 MB
% 55.87/8.67 % (3000696)Instructions burned: 134 (million)
% 55.87/8.67 % (3000702)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=562154467:i=499:bd=all_2982 on theBenchmark for (2982ds/499Mi)
% 55.87/8.67 % (3000708)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2452503633:i=191:fgj=on:bd=all_2980 on theBenchmark for (2980ds/191Mi)
% 55.87/8.67 % (3000708)Instruction limit reached!
% 55.87/8.67 % (3000708)------------------------------
% 55.87/8.67 % (3000708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.87/8.67 % (3000708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.87/8.67 % (3000708)CaDiCaL version: 2.1.3
% 55.87/8.67 % (3000708)Termination reason: Instruction limit
% 55.87/8.67 % (3000708)Termination phase: Saturation
% 55.87/8.67 % (3000708)Time elapsed: 0.192 s
% 55.87/8.67 % (3000708)Peak memory usage: 91 MB
% 55.87/8.67 % (3000708)Instructions burned: 191 (million)
% 55.87/8.67 % (3000702)Instruction limit reached!
% 55.87/8.67 % (3000702)------------------------------
% 55.87/8.67 % (3000702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.87/8.67 % (3000702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.87/8.67 % (3000702)CaDiCaL version: 2.1.3
% 55.87/8.67 % (3000702)Termination reason: Instruction limit
% 55.87/8.67 % (3000702)Termination phase: Saturation
% 55.87/8.67 % (3000702)Time elapsed: 0.503 s
% 55.87/8.67 % (3000702)Peak memory usage: 94 MB
% 55.87/8.67 % (3000702)Instructions burned: 499 (million)
% 55.87/8.67 % (3000711)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=780717018:i=264:kws=precedence:fsr=off_2975 on theBenchmark for (2975ds/264Mi)
% 55.87/8.67 % (3000712)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=691600335:cond=on:i=156:bs=on:gtg=exists_all:er=known_2974 on theBenchmark for (2974ds/156Mi)
% 55.87/8.67 % (3000712)Instruction limit reached!
% 55.87/8.67 % (3000712)------------------------------
% 55.87/8.67 % (3000712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.87/8.67 % (3000712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.87/8.67 % (3000712)CaDiCaL version: 2.1.3
% 55.87/8.67 % (3000712)Termination reason: Instruction limit
% 55.87/8.67 % (3000712)Termination phase: Saturation
% 55.87/8.67 % (3000712)Time elapsed: 0.160 s
% 55.87/8.67 % (3000712)Peak memory usage: 89 MB
% 55.87/8.67 % (3000712)Instructions burned: 156 (million)
% 55.87/8.67 % (3000711)Instruction limit reached!
% 55.87/8.67 % (3000711)------------------------------
% 55.87/8.67 % (3000711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.87/8.67 % (3000711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.87/8.67 % (3000711)CaDiCaL version: 2.1.3
% 55.87/8.67 % (3000711)Termination reason: Instruction limit
% 55.87/8.67 % (3000711)Termination phase: Saturation
% 55.87/8.67 % (3000711)Time elapsed: 0.266 s
% 55.87/8.67 % (3000711)Peak memory usage: 92 MB
% 55.87/8.67 % (3000711)Instructions burned: 265 (million)
% 55.87/8.67 % (3000717)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=1496424433:i=3256:kws=precedence:bd=preordered:av=off_2969 on theBenchmark for (2969ds/3256Mi)
% 55.87/8.67 % (3000718)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3806012973:i=537:av=off:ss=included_2969 on theBenchmark for (2969ds/537Mi)
% 55.87/8.67 % (3000718)Instruction limit reached!
% 55.87/8.67 % (3000718)------------------------------
% 55.87/8.67 % (3000718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.87/8.67 % (3000718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.87/8.67 % (3000718)CaDiCaL version: 2.1.3
% 55.87/8.67 % (3000718)Termination reason: Instruction limit
% 55.87/8.67 % (3000718)Termination phase: Saturation
% 55.87/8.67 % (3000718)Time elapsed: 0.511 s
% 55.87/8.67 % (3000718)Peak memory usage: 93 MB
% 55.87/8.67 % (3000718)Instructions burned: 537 (million)
% 55.87/8.67 % (3000722)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1142762579:i=180:bd=preordered:av=off_2961 on theBenchmark for (2961ds/180Mi)
% 55.87/8.67 % (3000722)Instruction limit reached!
% 55.87/8.67 % (3000722)------------------------------
% 55.87/8.67 % (3000722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.87/8.67 % (3000722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.87/8.67 % (3000722)CaDiCaL version: 2.1.3
% 55.87/8.67 % (3000722)Termination reason: Instruction limit
% 55.87/8.67 % (3000722)Termination phase: Saturation
% 55.87/8.67 % (3000722)Time elapsed: 0.174 s
% 55.87/8.67 % (3000722)Peak memory usage: 88 MB
% 55.87/8.67 % (3000722)Instructions burned: 181 (million)
% 55.87/8.67 % (3000679)Instruction limit reached!
% 55.87/8.67 % (3000679)------------------------------
% 55.87/8.67 % (3000679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.87/8.67 % (3000679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.87/8.67 % (3000679)CaDiCaL version: 2.1.3
% 55.87/8.67 % (3000679)Termination reason: Instruction limit
% 55.87/8.67 % (3000679)Termination phase: Saturation
% 55.87/8.67 % (3000679)Time elapsed: 3.390 s
% 55.87/8.67 % (3000679)Peak memory usage: 149 MB
% 55.87/8.67 % (3000679)Instructions burned: 3395 (million)
% 55.87/8.67 % (3000726)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=933423324:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2956 on theBenchmark for (2956ds/10307Mi)
% 55.87/8.67 % (3000727)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=2949363753:i=412:gtgl=4:gtg=exists_all_2954 on theBenchmark for (2954ds/412Mi)
% 55.87/8.67 % (3000727)Instruction limit reached!
% 55.87/8.67 % (3000727)------------------------------
% 55.87/8.67 % (3000727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.87/8.67 % (3000727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.87/8.67 % (3000727)CaDiCaL version: 2.1.3
% 55.87/8.67 % (3000727)Termination reason: Instruction limit
% 55.87/8.67 % (3000727)Termination phase: Saturation
% 55.87/8.67 % (3000727)Time elapsed: 0.392 s
% 55.87/8.67 % (3000727)Peak memory usage: 94 MB
% 55.87/8.67 % (3000727)Instructions burned: 413 (million)
% 55.87/8.67 % (3000730)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=2472454310:s2pl=no:i=8478:s2at=4:nm=6_2948 on theBenchmark for (2948ds/8478Mi)
% 55.87/8.67 % (3000717)Instruction limit reached!
% 55.87/8.67 % (3000717)------------------------------
% 55.87/8.67 % (3000717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.87/8.67 % (3000717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.87/8.67 % (3000717)CaDiCaL version: 2.1.3
% 55.87/8.67 % (3000717)Termination reason: Instruction limit
% 55.87/8.67 % (3000717)Termination phase: Saturation
% 55.87/8.67 % (3000717)Time elapsed: 3.322 s
% 55.87/8.67 % (3000717)Peak memory usage: 149 MB
% 55.87/8.67 % (3000717)Instructions burned: 3256 (million)
% 55.87/8.67 % (3000694)Instruction limit reached!
% 55.87/8.67 % (3000694)------------------------------
% 55.87/8.67 % (3000694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.87/8.67 % (3000694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.87/8.67 % (3000694)CaDiCaL version: 2.1.3
% 55.87/8.67 % (3000694)Termination reason: Instruction limit
% 55.87/8.67 % (3000694)Termination phase: Saturation
% 55.87/8.67 % (3000694)Time elapsed: 5.121 s
% 55.87/8.67 % (3000694)Peak memory usage: 165 MB
% 55.87/8.67 % (3000694)Instructions burned: 5208 (million)
% 55.87/8.67 % (3000732)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=379267786:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2934 on theBenchmark for (2934ds/303Mi)
% 55.87/8.67 % (3000732)Refutation not found, incomplete strategy
% 55.87/8.67 % (3000732)------------------------------
% 55.87/8.67 % (3000732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.87/8.67 % (3000732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.87/8.67 % (3000732)CaDiCaL version: 2.1.3
% 55.87/8.67 % (3000732)Termination reason: Refutation not found, incomplete strategy
% 55.87/8.67 % (3000732)Time elapsed: 0.004 s
% 55.87/8.67 % (3000732)Peak memory usage: 88 MB
% 55.87/8.67 % (3000732)Instructions burned: 1 (million)
% 55.87/8.67 % (3000733)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2866366161:st=4:i=720:sd=3:fsr=off:ss=axioms_2932 on theBenchmark for (2932ds/720Mi)
% 55.87/8.67 % (3000733)Refutation not found, incomplete strategy
% 55.87/8.67 % (3000733)------------------------------
% 55.87/8.67 % (3000733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.87/8.67 % (3000733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.87/8.67 % (3000733)CaDiCaL version: 2.1.3
% 55.87/8.67 % (3000733)Termination reason: Refutation not found, incomplete strategy
% 55.87/8.67 % (3000733)Time elapsed: 0.002 s
% 55.87/8.67 % (3000733)Peak memory usage: 88 MB
% 55.87/8.67 % (3000732)------------------------------
% 55.87/8.67 % (3000732)------------------------------
% 55.87/8.67 % (3000733)------------------------------
% 55.87/8.67 % (3000733)------------------------------
% 55.87/8.67 % (3000738)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1253526957:i=598:bs=on:bd=preordered:av=off:ss=axioms_2928 on theBenchmark for (2928ds/598Mi)
% 55.87/8.67 % (3000616)First to succeed.
% 55.87/8.67 % (3000616)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3000578"
% 55.87/8.67 % (3000739)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1835487889:i=2989:sd=3:ss=axioms:sgt=60_2925 on theBenchmark for (2925ds/2989Mi)
% 55.87/8.67 % (3000616)Refutation found. Thanks to Tanya!
% 55.87/8.67 % SZS status Unsatisfiable for theBenchmark
% 55.87/8.67 % SZS output start Proof for theBenchmark
% See solution above
% 56.96/8.88 % (3000616)------------------------------
% 56.96/8.88 % (3000616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.96/8.88 % (3000616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.96/8.88 % (3000616)CaDiCaL version: 2.1.3
% 56.96/8.88 % (3000616)Termination reason: Refutation
% 56.96/8.88 % (3000616)Time elapsed: 7.399 s
% 56.96/8.88 % (3000616)Peak memory usage: 175 MB
% 56.96/8.88 % (3000616)Instructions burned: 6988 (million)
% 56.96/8.88 % (3000616)------------------------------
% 56.96/8.88 % (3000616)------------------------------
% 56.96/8.88 % (3000578)Success in time 8.027 s
% 56.96/8.88 % Vampire exiting
%------------------------------------------------------------------------------