%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT065-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.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:45:56 AM UTC 2026
% Result : Unsatisfiable 33.03s 9.92s
% Output : Refutation 64.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 78
% Number of leaves : 17
% Syntax : Number of formulae : 395 ( 351 unt; 5 def)
% Number of atoms : 448 ( 447 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 108 ( 55 ~; 53 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 12 ( 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 : 968 ( 968 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0] : join(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_of_join) ).
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)) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',top) ).
fof(f10,axiom,
! [X0] : meet(X0,complement(X0)) = n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bottom) ).
fof(f11,axiom,
! [X0,X1] :
( join(X0,X1) != n1
| meet(X0,X1) != n0
| complement(X0) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complements_are_unique) ).
fof(f12,axiom,
! [X2,X0,X1] : meet(X0,join(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1)))) = join(meet(X0,X1),meet(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c94_37) ).
fof(f13,negated_conjecture,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_distributivity) ).
fof(f14,definition,
sF0 = join(b,c),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f15,plain,
join(b,c) = sF0,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF1 = meet(a,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f17,plain,
meet(a,sF0) = sF1,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF2 = meet(a,b),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f19,plain,
meet(a,b) = sF2,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF3 = meet(a,c),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f21,plain,
meet(a,c) = sF3,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF4 = join(sF2,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f23,plain,
join(sF2,sF3) = sF4,
inference(reorient_equations,[],[f22]) ).
fof(f24,plain,
sF1 != sF4,
inference(definition_folding,[],[f13,f23,f21,f19,f17,f15]) ).
fof(f25,plain,
sF2 = meet(b,a),
inference(forward_demodulation,[],[f19,f5]) ).
fof(f26,plain,
sF3 = meet(c,a),
inference(forward_demodulation,[],[f21,f5]) ).
fof(f32,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f34,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f35,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f32,f3]) ).
fof(f41,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f35,f6]) ).
fof(f43,plain,
! [X2,X0,X1] : join(X0,join(meet(X0,X1),X2)) = join(X0,X2),
inference(superposition,[],[f8,f4]) ).
fof(f44,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f32]) ).
fof(f46,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(superposition,[],[f8,f6]) ).
fof(f53,plain,
! [X2,X0,X1] : join(X0,X1) = join(X0,join(X1,meet(join(X0,X1),X2))),
inference(superposition,[],[f4,f8]) ).
fof(f56,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f60,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f34,f4]) ).
fof(f61,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f34,f32]) ).
fof(f66,plain,
! [X0,X1] : join(X1,X0) = join(join(X1,X0),X0),
inference(superposition,[],[f32,f34]) ).
fof(f68,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f66,f6]) ).
fof(f69,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f61,f5]) ).
fof(f70,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f60,f5]) ).
fof(f76,plain,
! [X0,X1] :
( join(X0,X1) != n1
| meet(X1,X0) != n0
| complement(X1) = X0 ),
inference(superposition,[],[f11,f6]) ).
fof(f111,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f112,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f34]) ).
fof(f125,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f128,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,meet(X1,join(X2,meet(X0,X1)))),
inference(superposition,[],[f34,f7]) ).
fof(f135,plain,
! [X2,X0,X1] : meet(X1,join(meet(X0,join(X2,meet(X0,X1))),meet(X2,join(X1,X0)))) = join(meet(X0,X1),meet(X1,X2)),
inference(superposition,[],[f12,f5]) ).
fof(f143,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X1,join(meet(X0,X1),X2)),meet(X2,join(X0,X1)))),
inference(superposition,[],[f12,f6]) ).
fof(f147,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(meet(X0,X1),join(X2,meet(X0,meet(X0,X1)))),meet(X2,X0))),
inference(superposition,[],[f12,f4]) ).
fof(f150,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,X2)) = meet(X1,join(meet(X0,join(X2,meet(X1,X0))),meet(X2,join(X0,X1)))),
inference(superposition,[],[f12,f6]) ).
fof(f158,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X1,join(X2,meet(X0,X1))),meet(join(X0,X1),X2))),
inference(superposition,[],[f12,f5]) ).
fof(f161,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X1,X0)) = meet(X1,join(meet(X0,join(X1,X2)),meet(X2,join(X0,meet(X1,X2))))),
inference(superposition,[],[f12,f6]) ).
fof(f164,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1))) = join(join(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1))),join(meet(X0,X1),meet(X0,X2))),
inference(superposition,[],[f32,f12]) ).
fof(f169,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1))) = join(join(meet(X0,X1),meet(X0,X2)),join(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f164,f6]) ).
fof(f173,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(join(X0,X1),X2),meet(X1,join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f158,f6]) ).
fof(f181,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,X2)) = meet(X1,join(meet(X2,join(X0,X1)),meet(X0,join(X2,meet(X1,X0))))),
inference(forward_demodulation,[],[f150,f6]) ).
fof(f184,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(meet(X0,X1),join(X2,meet(X0,meet(X0,X1)))))),
inference(forward_demodulation,[],[f147,f6]) ).
fof(f188,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X2,join(X0,X1)),meet(X1,join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f143,f6]) ).
fof(f196,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X2)) = meet(X1,join(meet(X2,join(X1,X0)),meet(X0,join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f135,f6]) ).
fof(f202,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1))) = join(meet(X2,join(X0,X1)),join(join(meet(X0,X1),meet(X0,X2)),meet(X1,join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f169,f56]) ).
fof(f208,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X0,meet(X1,join(X2,meet(X0,meet(X0,X1))))))),
inference(forward_demodulation,[],[f184,f7]) ).
fof(f216,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1))) = join(meet(X2,join(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X1,join(X2,meet(X0,X1)))))),
inference(forward_demodulation,[],[f202,f8]) ).
fof(f221,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X0,meet(X1,join(X2,meet(X0,X1)))))),
inference(forward_demodulation,[],[f208,f70]) ).
fof(f228,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1))) = join(meet(X0,X1),join(join(meet(X0,X2),meet(X1,join(X2,meet(X0,X1)))),meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f216,f56]) ).
fof(f231,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X0,X1))),
inference(forward_demodulation,[],[f221,f128]) ).
fof(f233,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1))) = join(meet(X0,X1),join(meet(X2,join(X0,X1)),join(meet(X0,X2),meet(X1,join(X2,meet(X0,X1)))))),
inference(forward_demodulation,[],[f228,f6]) ).
fof(f235,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1))) = join(meet(X0,X1),join(meet(X0,X2),join(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1))))),
inference(forward_demodulation,[],[f233,f56]) ).
fof(f237,plain,
! [X2,X0,X1] : join(meet(X2,join(X0,X1)),meet(X1,join(X2,meet(X0,X1)))) = join(meet(X0,X1),join(meet(X0,X2),join(meet(X2,join(X0,X1)),meet(X1,join(X2,meet(X0,X1)))))),
inference(forward_demodulation,[],[f235,f6]) ).
fof(f246,plain,
! [X0] : meet(X0,n1) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f248,plain,
! [X0,X1] : join(meet(X0,complement(X0)),meet(X0,X1)) = meet(X0,join(meet(complement(X0),join(X1,meet(X0,complement(X0)))),meet(X1,n1))),
inference(superposition,[],[f12,f9]) ).
fof(f250,plain,
! [X0,X1] : n1 = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f252,plain,
! [X0,X1] : join(meet(X0,complement(X0)),meet(X0,X1)) = meet(X0,join(meet(X1,n1),meet(complement(X0),join(X1,meet(X0,complement(X0)))))),
inference(forward_demodulation,[],[f248,f6]) ).
fof(f253,plain,
! [X0,X1] : join(n0,meet(X0,X1)) = meet(X0,join(meet(X1,n1),meet(complement(X0),join(X1,n0)))),
inference(forward_demodulation,[],[f252,f10]) ).
fof(f254,plain,
! [X0,X1] : join(n0,meet(X0,X1)) = meet(X0,join(X1,meet(complement(X0),join(X1,n0)))),
inference(forward_demodulation,[],[f253,f246]) ).
fof(f262,plain,
! [X0] : meet(n1,X0) = X0,
inference(superposition,[],[f5,f246]) ).
fof(f281,plain,
! [X0] : n1 = join(X0,n1),
inference(superposition,[],[f34,f262]) ).
fof(f369,plain,
! [X0] : join(X0,n0) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f370,plain,
! [X0,X1] : n0 = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f373,plain,
! [X0,X1] : join(n0,meet(X0,X1)) = meet(X0,join(X1,meet(complement(X0),X1))),
inference(backward_demodulation,[],[f254,f369]) ).
fof(f375,plain,
! [X0,X1] : meet(X0,X1) = join(n0,meet(X0,X1)),
inference(forward_demodulation,[],[f373,f32]) ).
fof(f388,plain,
! [X0] : join(n0,X0) = X0,
inference(superposition,[],[f375,f262]) ).
fof(f394,plain,
! [X0] : n0 = meet(n0,X0),
inference(superposition,[],[f4,f375]) ).
fof(f395,plain,
! [X0] : n0 = meet(X0,n0),
inference(superposition,[],[f32,f375]) ).
fof(f424,plain,
! [X0,X1] : join(meet(X0,n0),meet(X0,X1)) = meet(X0,join(meet(n0,join(X1,meet(X0,n0))),meet(X1,X0))),
inference(superposition,[],[f12,f369]) ).
fof(f427,plain,
! [X0,X1] : join(meet(X0,n0),meet(X0,X1)) = meet(X0,join(meet(X1,X0),meet(n0,join(X1,meet(X0,n0))))),
inference(forward_demodulation,[],[f424,f6]) ).
fof(f429,plain,
! [X0,X1] : join(meet(X0,n0),meet(X0,X1)) = meet(X0,join(meet(X1,X0),n0)),
inference(forward_demodulation,[],[f427,f394]) ).
fof(f430,plain,
! [X0,X1] : join(meet(X0,n0),meet(X0,X1)) = meet(X0,join(n0,meet(X1,X0))),
inference(forward_demodulation,[],[f429,f6]) ).
fof(f431,plain,
! [X0,X1] : meet(X0,meet(X1,X0)) = join(meet(X0,n0),meet(X0,X1)),
inference(forward_demodulation,[],[f430,f388]) ).
fof(f432,plain,
! [X0,X1] : meet(X0,meet(X1,X0)) = join(n0,meet(X0,X1)),
inference(forward_demodulation,[],[f431,f395]) ).
fof(f433,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f432,f388]) ).
fof(f446,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f111,f5]) ).
fof(f451,plain,
! [X0,X1] : meet(X0,n0) = meet(X0,complement(join(X0,X1))),
inference(superposition,[],[f111,f10]) ).
fof(f467,plain,
! [X0,X1] : n0 = meet(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f451,f395]) ).
fof(f479,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(meet(join(X0,X2),X1),meet(X0,X1)),
inference(superposition,[],[f433,f111]) ).
fof(f487,plain,
meet(a,c) = meet(a,sF3),
inference(superposition,[],[f433,f26]) ).
fof(f493,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(meet(X1,X0),X2)),
inference(superposition,[],[f7,f433]) ).
fof(f502,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f493,f7]) ).
fof(f506,plain,
meet(c,a) = meet(a,sF3),
inference(forward_demodulation,[],[f487,f5]) ).
fof(f513,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(meet(X0,X1),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f479,f5]) ).
fof(f516,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f502,f7]) ).
fof(f518,plain,
sF3 = meet(a,sF3),
inference(forward_demodulation,[],[f506,f26]) ).
fof(f524,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(X1,meet(meet(X0,X1),join(X0,X2))),
inference(forward_demodulation,[],[f513,f125]) ).
fof(f529,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(X1,meet(X0,meet(X1,join(X0,X2)))),
inference(forward_demodulation,[],[f524,f7]) ).
fof(f531,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(X1,meet(X0,join(X0,X2))),
inference(forward_demodulation,[],[f529,f516]) ).
fof(f532,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(meet(join(X0,X2),X1),X0),
inference(forward_demodulation,[],[f531,f3]) ).
fof(f533,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X0,meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f532,f5]) ).
fof(f599,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f43,f6]) ).
fof(f603,plain,
! [X0,X1] : join(X0,n1) = join(X0,complement(meet(X0,X1))),
inference(superposition,[],[f43,f9]) ).
fof(f623,plain,
! [X0,X1] : n1 = join(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f603,f281]) ).
fof(f669,plain,
! [X0,X1] : n0 = meet(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f370,f5]) ).
fof(f750,plain,
! [X0,X1] : n1 = join(X1,complement(meet(X0,X1))),
inference(superposition,[],[f623,f5]) ).
fof(f756,plain,
! [X2,X0,X1] : n1 = join(X0,complement(join(meet(X0,X1),meet(X0,X2)))),
inference(superposition,[],[f623,f12]) ).
fof(f772,plain,
! [X2,X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,X2)) = meet(X0,join(meet(complement(meet(X0,X1)),join(X2,meet(X0,complement(meet(X0,X1))))),meet(X2,n1))),
inference(superposition,[],[f12,f623]) ).
fof(f781,plain,
! [X2,X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,X2)) = meet(X0,join(meet(X2,n1),meet(complement(meet(X0,X1)),join(X2,meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f772,f6]) ).
fof(f788,plain,
! [X2,X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,X2)) = meet(X0,join(X2,meet(complement(meet(X0,X1)),join(X2,meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f781,f246]) ).
fof(f869,plain,
! [X0,X1] :
( n1 != n1
| n0 != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(superposition,[],[f11,f250]) ).
fof(f876,plain,
! [X0,X1] :
( n0 != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f869]) ).
fof(f924,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f44,f6]) ).
fof(f942,plain,
! [X2,X0,X1] : join(meet(X2,X0),X1) = meet(join(meet(X2,X0),X1),join(X0,X1)),
inference(superposition,[],[f34,f44]) ).
fof(f945,plain,
! [X2,X3,X0,X1] : join(X0,join(meet(X0,X1),X2)) = join(X0,join(meet(X3,meet(X0,X1)),X2)),
inference(superposition,[],[f43,f44]) ).
fof(f950,plain,
! [X2,X3,X0,X1] : join(X0,X2) = join(X0,join(meet(X3,meet(X0,X1)),X2)),
inference(forward_demodulation,[],[f945,f43]) ).
fof(f952,plain,
! [X2,X0,X1] : join(meet(X2,X0),X1) = meet(join(X0,X1),join(meet(X2,X0),X1)),
inference(forward_demodulation,[],[f942,f5]) ).
fof(f1010,plain,
! [X2,X0,X1] : join(meet(X0,complement(meet(X1,X0))),meet(X0,X2)) = meet(X0,join(meet(complement(meet(X1,X0)),join(X2,meet(X0,complement(meet(X1,X0))))),meet(X2,n1))),
inference(superposition,[],[f12,f750]) ).
fof(f1023,plain,
! [X2,X0,X1] : join(meet(X0,complement(meet(X1,X0))),meet(X0,X2)) = meet(X0,join(meet(X2,n1),meet(complement(meet(X1,X0)),join(X2,meet(X0,complement(meet(X1,X0))))))),
inference(forward_demodulation,[],[f1010,f6]) ).
fof(f1034,plain,
! [X2,X0,X1] : join(meet(X0,complement(meet(X1,X0))),meet(X0,X2)) = meet(X0,join(X2,meet(complement(meet(X1,X0)),join(X2,meet(X0,complement(meet(X1,X0))))))),
inference(forward_demodulation,[],[f1023,f246]) ).
fof(f1349,plain,
! [X0,X1] : n0 = meet(X1,complement(join(X0,X1))),
inference(superposition,[],[f467,f6]) ).
fof(f1567,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(meet(X0,X1),meet(X0,X2)),
inference(superposition,[],[f112,f4]) ).
fof(f1661,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f1567,f125]) ).
fof(f1678,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X2,X1)),
inference(forward_demodulation,[],[f1661,f516]) ).
fof(f1943,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = meet(X0,join(meet(complement(meet(X0,X1)),join(X0,X1)),meet(X1,n1))),
inference(superposition,[],[f188,f9]) ).
fof(f2001,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = meet(X0,join(meet(X1,n1),meet(complement(meet(X0,X1)),join(X0,X1)))),
inference(forward_demodulation,[],[f1943,f6]) ).
fof(f2074,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = meet(X0,join(meet(X1,n1),meet(join(X0,X1),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f2001,f5]) ).
fof(f2130,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = meet(X0,join(X1,meet(join(X0,X1),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f2074,f246]) ).
fof(f2264,plain,
! [X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,complement(meet(X0,meet(X1,X0))))) = meet(X0,join(meet(X1,X0),meet(X0,complement(meet(X0,meet(X1,X0)))))),
inference(superposition,[],[f2130,f32]) ).
fof(f2270,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = meet(X0,join(complement(meet(X0,X1)),meet(n1,complement(meet(X0,complement(meet(X0,X1))))))),
inference(superposition,[],[f2130,f623]) ).
fof(f2399,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = meet(X0,join(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f2270,f262]) ).
fof(f2405,plain,
! [X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,complement(meet(X0,meet(X1,X0))))) = join(meet(X0,complement(meet(X0,meet(X1,X0)))),meet(X0,X1)),
inference(forward_demodulation,[],[f2264,f231]) ).
fof(f2449,plain,
! [X0,X1] : meet(X0,n1) = join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f2399,f750]) ).
fof(f2453,plain,
! [X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,complement(meet(X0,meet(X1,X0))))) = join(meet(X0,X1),meet(X0,complement(meet(X0,meet(X1,X0))))),
inference(forward_demodulation,[],[f2405,f6]) ).
fof(f2479,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = X0,
inference(forward_demodulation,[],[f2449,f246]) ).
fof(f2483,plain,
! [X0,X1] : join(meet(X1,X0),meet(X0,complement(meet(X1,X0)))) = join(meet(X0,X1),meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f2453,f69]) ).
fof(f3303,plain,
! [X2,X3,X0,X1] : meet(X2,meet(X0,X1)) = meet(X2,meet(X0,meet(X1,join(X2,X3)))),
inference(superposition,[],[f111,f125]) ).
fof(f3773,plain,
! [X2,X3,X0,X1] : join(X1,join(X3,X0)) = join(X1,join(X0,join(meet(X1,X2),X3))),
inference(superposition,[],[f43,f56]) ).
fof(f4048,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X1,X0))),meet(meet(X1,join(X2,meet(X0,X1))),X0)) = meet(meet(X1,join(X2,meet(X0,X1))),join(join(meet(X0,X1),meet(X0,X2)),meet(meet(X2,join(X1,X0)),join(X0,meet(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X1,X0))))))),
inference(superposition,[],[f181,f181]) ).
fof(f4209,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X1,X0))),meet(meet(X1,join(X2,meet(X0,X1))),X0)) = meet(X1,meet(join(X2,meet(X0,X1)),join(join(meet(X0,X1),meet(X0,X2)),meet(meet(X2,join(X1,X0)),join(X0,meet(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X1,X0)))))))),
inference(forward_demodulation,[],[f4048,f7]) ).
fof(f4295,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X1,X0))),meet(meet(X1,join(X2,meet(X0,X1))),X0)) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(meet(X2,join(X1,X0)),join(X0,meet(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X1,X0))))))))),
inference(forward_demodulation,[],[f4209,f8]) ).
fof(f4354,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X1,X0))),meet(meet(X1,join(X2,meet(X0,X1))),X0)) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X1,X0),join(X0,meet(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X1,X0)))))))))),
inference(forward_demodulation,[],[f4295,f7]) ).
fof(f4398,plain,
! [X2,X0,X1] : join(meet(meet(X2,join(X1,X0)),meet(X1,join(X2,meet(X0,X1)))),meet(meet(X1,join(X2,meet(X0,X1))),X0)) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X1,X0),join(X0,meet(meet(X2,join(X1,X0)),meet(X1,join(X2,meet(X0,X1))))))))))),
inference(forward_demodulation,[],[f4354,f5]) ).
fof(f4425,plain,
! [X2,X0,X1] : join(meet(join(X2,meet(X0,X1)),meet(meet(X2,join(X1,X0)),X1)),meet(meet(X1,join(X2,meet(X0,X1))),X0)) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X1,X0),join(X0,meet(join(X2,meet(X0,X1)),meet(meet(X2,join(X1,X0)),X1))))))))),
inference(forward_demodulation,[],[f4398,f125]) ).
fof(f4442,plain,
! [X2,X0,X1] : join(meet(X1,meet(join(X2,meet(X0,X1)),meet(X2,join(X1,X0)))),meet(meet(X1,join(X2,meet(X0,X1))),X0)) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X1,X0),join(X0,meet(X1,meet(join(X2,meet(X0,X1)),meet(X2,join(X1,X0))))))))))),
inference(forward_demodulation,[],[f4425,f125]) ).
fof(f4453,plain,
! [X2,X0,X1] : join(meet(X1,meet(join(X2,meet(X0,X1)),X2)),meet(meet(X1,join(X2,meet(X0,X1))),X0)) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X1,X0),join(X0,meet(X1,meet(join(X2,meet(X0,X1)),X2))))))))),
inference(forward_demodulation,[],[f4442,f3303]) ).
fof(f4461,plain,
! [X2,X0,X1] : join(meet(X1,meet(X2,join(X2,meet(X0,X1)))),meet(meet(X1,join(X2,meet(X0,X1))),X0)) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X1,X0),join(X0,meet(X1,meet(X2,join(X2,meet(X0,X1))))))))))),
inference(forward_demodulation,[],[f4453,f5]) ).
fof(f4468,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(meet(X1,join(X2,meet(X0,X1))),X0)) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X1,X0),join(X0,meet(X1,X2)))))))),
inference(forward_demodulation,[],[f4461,f3]) ).
fof(f4475,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X0,meet(X1,join(X2,meet(X0,X1))))) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X1,X0),join(X0,meet(X1,X2)))))))),
inference(forward_demodulation,[],[f4468,f5]) ).
fof(f4481,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X0,X1)) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X1,X0),join(X0,meet(X1,X2)))))))),
inference(forward_demodulation,[],[f4475,f128]) ).
fof(f4534,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(meet(X2,join(join(X0,X1),X0)),meet(X0,join(X2,X0)))),
inference(superposition,[],[f196,f3]) ).
fof(f4677,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(meet(X0,join(X2,X0)),meet(X2,join(join(X0,X1),X0)))),
inference(forward_demodulation,[],[f4534,f6]) ).
fof(f4771,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(meet(X0,join(X2,X0)),meet(X2,join(X0,join(X0,X1))))),
inference(forward_demodulation,[],[f4677,f6]) ).
fof(f4849,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(meet(X0,join(X2,X0)),meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f4771,f41]) ).
fof(f4905,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(X0,meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f4849,f34]) ).
fof(f6750,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X1,meet(X0,X2)),join(X0,X1)),
inference(superposition,[],[f34,f599]) ).
fof(f6796,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X0,X1),join(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f6750,f5]) ).
fof(f6830,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X0,X1)) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,join(X0,meet(X1,X2))))))),
inference(backward_demodulation,[],[f4481,f6796]) ).
fof(f7064,plain,
! [X2,X0,X1] : meet(meet(X1,join(X2,meet(X0,X1))),X0) = meet(meet(X1,join(X2,meet(X0,X1))),join(meet(X0,X1),meet(X0,X2))),
inference(superposition,[],[f446,f12]) ).
fof(f7092,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = join(meet(X1,join(X0,X2)),meet(X0,X1)),
inference(superposition,[],[f32,f446]) ).
fof(f7147,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = join(meet(X0,X1),meet(X1,join(X0,X2))),
inference(forward_demodulation,[],[f7092,f6]) ).
fof(f7168,plain,
! [X2,X0,X1] : meet(meet(X1,join(X2,meet(X0,X1))),X0) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),meet(X0,X2)))),
inference(forward_demodulation,[],[f7064,f7]) ).
fof(f7187,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X0,X1)) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),meet(X2,join(X0,meet(X1,X2)))))),
inference(backward_demodulation,[],[f6830,f7147]) ).
fof(f7209,plain,
! [X2,X0,X1] : meet(X0,meet(X1,join(X2,meet(X0,X1)))) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),meet(X0,X2)))),
inference(forward_demodulation,[],[f7168,f5]) ).
fof(f7228,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X0,X1)) = meet(X1,join(meet(X0,X1),meet(X2,join(X0,meet(X1,X2))))),
inference(forward_demodulation,[],[f7187,f6796]) ).
fof(f7235,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),meet(X0,X2)))),
inference(forward_demodulation,[],[f7209,f128]) ).
fof(f7450,plain,
! [X2,X3,X0,X1] : join(meet(X1,join(X0,X2)),X3) = join(meet(X1,join(X0,X2)),join(X3,meet(X0,X1))),
inference(superposition,[],[f924,f446]) ).
fof(f7513,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X1,meet(X2,X0)),join(X0,X1)),
inference(superposition,[],[f34,f924]) ).
fof(f7562,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X0,X1),join(X1,meet(X2,X0))),
inference(forward_demodulation,[],[f7513,f5]) ).
fof(f7599,plain,
! [X2,X3,X0,X1] : join(meet(X1,join(X0,X2)),X3) = join(meet(X0,X1),join(meet(X1,join(X0,X2)),X3)),
inference(forward_demodulation,[],[f7450,f56]) ).
fof(f7606,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X1,join(meet(X0,X1),meet(X0,X2))),
inference(backward_demodulation,[],[f7235,f7562]) ).
fof(f7622,plain,
! [X2,X0,X1] : join(meet(X2,join(X0,X1)),meet(X1,join(X2,meet(X0,X1)))) = join(meet(X0,X1),join(meet(X2,join(X0,X1)),meet(X1,join(X2,meet(X0,X1))))),
inference(backward_demodulation,[],[f237,f7599]) ).
fof(f7941,plain,
! [X2,X0,X1] : join(meet(join(X0,X1),X1),meet(join(X0,X1),X2)) = meet(join(X0,X1),join(meet(X2,join(X0,X1)),meet(X1,join(X2,meet(join(X0,X1),X1))))),
inference(superposition,[],[f181,f68]) ).
fof(f7971,plain,
! [X2,X0,X1] : join(meet(join(X0,X1),X1),meet(join(X0,X1),X2)) = join(meet(join(X0,X1),X1),meet(X2,join(X0,X1))),
inference(forward_demodulation,[],[f7941,f7228]) ).
fof(f8010,plain,
! [X2,X0,X1] : join(meet(X1,join(X0,X1)),meet(join(X0,X1),X2)) = join(meet(X1,join(X0,X1)),meet(X2,join(X0,X1))),
inference(forward_demodulation,[],[f7971,f5]) ).
fof(f8034,plain,
! [X2,X0,X1] : join(X1,meet(join(X0,X1),X2)) = join(X1,meet(X2,join(X0,X1))),
inference(forward_demodulation,[],[f8010,f34]) ).
fof(f8366,plain,
! [X0] :
( n1 != n1
| n0 != meet(complement(X0),X0)
| complement(complement(X0)) = X0 ),
inference(superposition,[],[f76,f9]) ).
fof(f8386,plain,
! [X0] :
( n0 != meet(complement(X0),X0)
| complement(complement(X0)) = X0 ),
inference(trivial_inequality_removal,[],[f8366]) ).
fof(f8398,plain,
! [X0] :
( meet(X0,complement(X0)) != n0
| complement(complement(X0)) = X0 ),
inference(forward_demodulation,[],[f8386,f5]) ).
fof(f8415,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_subsumption_resolution,[],[f8398,f10]) ).
fof(f8637,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(join(X1,X2),X0),meet(X0,X1)),
inference(superposition,[],[f32,f533]) ).
fof(f8644,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X1,X3)) = meet(X1,join(meet(X3,join(X1,meet(join(X1,X2),X0))),meet(meet(join(X1,X2),X0),join(X3,meet(X0,X1))))),
inference(superposition,[],[f161,f533]) ).
fof(f8690,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X1,X3)) = meet(X1,join(meet(X3,join(X1,meet(join(X1,X2),X0))),meet(join(X1,X2),meet(X0,join(X3,meet(X0,X1)))))),
inference(forward_demodulation,[],[f8644,f7]) ).
fof(f8695,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(X0,X1),meet(join(X1,X2),X0)),
inference(forward_demodulation,[],[f8637,f6]) ).
fof(f10584,plain,
! [X2,X0,X1] : join(X1,X0) = join(X0,join(X1,meet(X2,join(X1,X0)))),
inference(superposition,[],[f32,f46]) ).
fof(f10786,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,[],[f44,f2479]) ).
fof(f10861,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,[],[f10786,f6]) ).
fof(f10913,plain,
! [X0,X1] : n1 = join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f10861,f623]) ).
fof(f11140,plain,
! [X0,X1] :
( n1 != n1
| n0 != 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,f10913]) ).
fof(f11169,plain,
! [X0,X1] :
( n0 != 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,[],[f11140]) ).
fof(f11194,plain,
! [X0,X1] : meet(X0,complement(meet(X0,complement(meet(X0,X1))))) = complement(complement(meet(X0,X1))),
inference(forward_subsumption_resolution,[],[f11169,f669]) ).
fof(f11249,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f11194,f8415]) ).
fof(f11283,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,X1)) = X0,
inference(backward_demodulation,[],[f2479,f11249]) ).
fof(f11324,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = X0,
inference(forward_demodulation,[],[f11283,f6]) ).
fof(f11365,plain,
! [X0,X1] : meet(X0,join(X1,meet(join(X0,X1),complement(meet(X0,X1))))) = X0,
inference(backward_demodulation,[],[f2130,f11324]) ).
fof(f11570,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,complement(meet(X0,X1)))) = X1,
inference(superposition,[],[f11324,f7606]) ).
fof(f11608,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f44,f11324]) ).
fof(f11640,plain,
! [X0,X1] :
( n0 != 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,[],[f876,f11324]) ).
fof(f11649,plain,
! [X0,X1] :
( n0 != 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,[],[f11640,f7]) ).
fof(f11734,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X1,X0)))) = X0,
inference(backward_demodulation,[],[f2483,f11570]) ).
fof(f11792,plain,
! [X0,X1] :
( n0 != 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,[],[f11649,f6]) ).
fof(f11868,plain,
! [X0,X1] :
( complement(meet(X0,X1)) = join(complement(X0),meet(X0,complement(meet(X0,X1))))
| n0 != meet(X0,meet(X1,join(complement(X0),meet(X0,complement(meet(X0,X1)))))) ),
inference(forward_demodulation,[],[f11792,f6]) ).
fof(f11990,plain,
! [X0,X1] : join(meet(X1,X0),X0) = join(meet(X1,X0),meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f11608,f433]) ).
fof(f12185,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = join(meet(X1,X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f11990,f6]) ).
fof(f12249,plain,
! [X0,X1] : join(meet(X1,X0),meet(X0,complement(meet(X0,X1)))) = X0,
inference(forward_demodulation,[],[f12185,f32]) ).
fof(f12356,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,complement(meet(X1,complement(meet(X0,X1))))),
inference(superposition,[],[f11249,f7606]) ).
fof(f12401,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),X2)),
inference(superposition,[],[f7,f11249]) ).
fof(f12411,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(join(X0,complement(meet(X0,complement(meet(X0,X1))))),X2),meet(complement(meet(X0,complement(meet(X0,X1)))),join(X2,meet(X0,X1))))),
inference(superposition,[],[f173,f11249]) ).
fof(f12459,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(n1,X2),meet(complement(meet(X0,complement(meet(X0,X1)))),join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f12411,f623]) ).
fof(f12466,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),X2)),
inference(forward_demodulation,[],[f12401,f7]) ).
fof(f12503,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(X2,meet(complement(meet(X0,complement(meet(X0,X1)))),join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f12459,f262]) ).
fof(f12657,plain,
! [X0,X1] : join(X1,meet(join(X0,X1),complement(meet(X0,X1)))) = join(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),X0),
inference(superposition,[],[f32,f11365]) ).
fof(f12717,plain,
! [X0,X1] : join(X1,meet(join(X0,X1),complement(meet(X0,X1)))) = join(X0,join(X1,meet(join(X0,X1),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f12657,f6]) ).
fof(f12829,plain,
! [X0,X1] : join(X0,X1) = join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f12717,f53]) ).
fof(f13083,plain,
! [X0,X1] : join(X1,X0) = join(X0,meet(join(X1,X0),complement(meet(X0,X1)))),
inference(superposition,[],[f12829,f5]) ).
fof(f13696,plain,
! [X0,X1] :
( n0 != 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,[],[f876,f11734]) ).
fof(f13705,plain,
! [X0,X1] :
( n0 != 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,[],[f13696,f7]) ).
fof(f13845,plain,
! [X0,X1] :
( n0 != 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,[],[f13705,f6]) ).
fof(f13966,plain,
! [X0,X1] :
( complement(meet(X0,X1)) = join(complement(X0),meet(X0,complement(meet(X1,X0))))
| n0 != meet(X0,meet(X1,join(complement(X0),meet(X0,complement(meet(X1,X0)))))) ),
inference(forward_demodulation,[],[f13845,f6]) ).
fof(f15005,plain,
! [X0,X1] : meet(join(X1,X0),complement(meet(join(X1,X0),complement(X0)))) = X0,
inference(superposition,[],[f12356,f34]) ).
fof(f15066,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X2)) = meet(X1,join(meet(join(X1,complement(meet(X1,complement(meet(X0,X1))))),X2),meet(complement(meet(X1,complement(meet(X0,X1)))),join(X2,meet(X0,X1))))),
inference(superposition,[],[f173,f12356]) ).
fof(f15123,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X2)) = meet(X1,join(meet(n1,X2),meet(complement(meet(X1,complement(meet(X0,X1)))),join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f15066,f623]) ).
fof(f15169,plain,
! [X0,X1] : meet(join(X1,X0),complement(meet(complement(X0),join(X1,X0)))) = X0,
inference(forward_demodulation,[],[f15005,f5]) ).
fof(f15198,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X2)) = meet(X1,join(X2,meet(complement(meet(X1,complement(meet(X0,X1)))),join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f15123,f262]) ).
fof(f15728,plain,
! [X0,X1] :
( n0 != 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,[],[f876,f12249]) ).
fof(f15739,plain,
! [X0,X1] :
( n0 != 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,[],[f15728,f7]) ).
fof(f15879,plain,
! [X0,X1] :
( n0 != meet(X1,meet(X0,join(complement(X0),meet(X0,complement(meet(X0,X1))))))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(forward_demodulation,[],[f15739,f6]) ).
fof(f15996,plain,
! [X0,X1] :
( complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X0,X1))))
| n0 != meet(X1,meet(X0,join(complement(X0),meet(X0,complement(meet(X0,X1)))))) ),
inference(forward_demodulation,[],[f15879,f6]) ).
fof(f16315,plain,
! [X0,X1] :
( n0 != meet(meet(X1,X0),join(meet(X0,complement(meet(X1,X0))),complement(X0)))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X1,X0))),complement(X0)) ),
inference(superposition,[],[f876,f11570]) ).
fof(f16326,plain,
! [X0,X1] :
( n0 != meet(X1,meet(X0,join(meet(X0,complement(meet(X1,X0))),complement(X0))))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X1,X0))),complement(X0)) ),
inference(forward_demodulation,[],[f16315,f7]) ).
fof(f16402,plain,
! [X0,X1] :
( n0 != meet(X1,meet(X0,join(complement(X0),meet(X0,complement(meet(X1,X0))))))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X1,X0))),complement(X0)) ),
inference(forward_demodulation,[],[f16326,f6]) ).
fof(f16449,plain,
! [X0,X1] :
( complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X1,X0))))
| n0 != meet(X1,meet(X0,join(complement(X0),meet(X0,complement(meet(X1,X0)))))) ),
inference(forward_demodulation,[],[f16402,f6]) ).
fof(f24121,plain,
! [X2,X0,X1] : join(join(meet(X2,join(X1,X0)),meet(X1,join(X2,meet(X0,X1)))),X0) = join(X0,meet(join(join(meet(X2,join(X1,X0)),meet(X1,join(X2,meet(X0,X1)))),X0),complement(join(meet(X0,X1),meet(X0,X2))))),
inference(superposition,[],[f13083,f181]) ).
fof(f24316,plain,
! [X2,X0,X1] : join(join(meet(X2,join(X1,X0)),meet(X1,join(X2,meet(X0,X1)))),X0) = join(X0,meet(complement(join(meet(X0,X1),meet(X0,X2))),join(join(meet(X2,join(X1,X0)),meet(X1,join(X2,meet(X0,X1)))),X0))),
inference(forward_demodulation,[],[f24121,f8034]) ).
fof(f24455,plain,
! [X2,X0,X1] : join(X0,join(meet(X2,join(X1,X0)),meet(X1,join(X2,meet(X0,X1))))) = join(X0,meet(complement(join(meet(X0,X1),meet(X0,X2))),join(X0,join(meet(X2,join(X1,X0)),meet(X1,join(X2,meet(X0,X1))))))),
inference(forward_demodulation,[],[f24316,f6]) ).
fof(f27390,plain,
! [X2,X0,X1] : join(meet(X0,n1),meet(complement(meet(X1,X2)),join(X0,meet(X1,complement(meet(X1,X2)))))) = join(meet(X1,complement(meet(X1,X2))),join(meet(X0,n1),meet(complement(meet(X1,X2)),join(X0,meet(X1,complement(meet(X1,X2))))))),
inference(superposition,[],[f7622,f623]) ).
fof(f27391,plain,
! [X2,X0,X1] : join(meet(X0,n1),meet(complement(meet(X2,X1)),join(X0,meet(X1,complement(meet(X2,X1)))))) = join(meet(X1,complement(meet(X2,X1))),join(meet(X0,n1),meet(complement(meet(X2,X1)),join(X0,meet(X1,complement(meet(X2,X1))))))),
inference(superposition,[],[f7622,f750]) ).
fof(f27485,plain,
! [X2,X0,X1] : join(meet(X2,join(X0,complement(meet(X0,complement(meet(X0,X1)))))),meet(complement(meet(X0,complement(meet(X0,X1)))),join(X2,meet(X0,X1)))) = join(meet(X0,X1),join(meet(X2,join(X0,complement(meet(X0,complement(meet(X0,X1)))))),meet(complement(meet(X0,complement(meet(X0,X1)))),join(X2,meet(X0,X1))))),
inference(superposition,[],[f7622,f11249]) ).
fof(f27486,plain,
! [X2,X0,X1] : join(meet(X2,join(X1,complement(meet(X1,complement(meet(X0,X1)))))),meet(complement(meet(X1,complement(meet(X0,X1)))),join(X2,meet(X0,X1)))) = join(meet(X0,X1),join(meet(X2,join(X1,complement(meet(X1,complement(meet(X0,X1)))))),meet(complement(meet(X1,complement(meet(X0,X1)))),join(X2,meet(X0,X1))))),
inference(superposition,[],[f7622,f12356]) ).
fof(f27675,plain,
! [X2,X0,X1] : join(meet(X2,n1),meet(complement(meet(X1,complement(meet(X0,X1)))),join(X2,meet(X0,X1)))) = join(meet(X0,X1),join(meet(X2,n1),meet(complement(meet(X1,complement(meet(X0,X1)))),join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f27486,f623]) ).
fof(f27676,plain,
! [X2,X0,X1] : join(meet(X2,n1),meet(complement(meet(X0,complement(meet(X0,X1)))),join(X2,meet(X0,X1)))) = join(meet(X0,X1),join(meet(X2,n1),meet(complement(meet(X0,complement(meet(X0,X1)))),join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f27485,f623]) ).
fof(f27748,plain,
! [X2,X0,X1] : join(X0,meet(complement(meet(X2,X1)),join(X0,meet(X1,complement(meet(X2,X1)))))) = join(meet(X1,complement(meet(X2,X1))),join(X0,meet(complement(meet(X2,X1)),join(X0,meet(X1,complement(meet(X2,X1))))))),
inference(forward_demodulation,[],[f27391,f246]) ).
fof(f27749,plain,
! [X2,X0,X1] : join(X0,meet(complement(meet(X1,X2)),join(X0,meet(X1,complement(meet(X1,X2)))))) = join(meet(X1,complement(meet(X1,X2))),join(X0,meet(complement(meet(X1,X2)),join(X0,meet(X1,complement(meet(X1,X2))))))),
inference(forward_demodulation,[],[f27390,f246]) ).
fof(f27817,plain,
! [X2,X0,X1] : join(X2,meet(complement(meet(X1,complement(meet(X0,X1)))),join(X2,meet(X0,X1)))) = join(meet(X0,X1),join(X2,meet(complement(meet(X1,complement(meet(X0,X1)))),join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f27675,f246]) ).
fof(f27818,plain,
! [X2,X0,X1] : join(X2,meet(complement(meet(X0,complement(meet(X0,X1)))),join(X2,meet(X0,X1)))) = join(meet(X0,X1),join(X2,meet(complement(meet(X0,complement(meet(X0,X1)))),join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f27676,f246]) ).
fof(f27870,plain,
! [X2,X0,X1] : join(X0,meet(X1,complement(meet(X2,X1)))) = join(X0,meet(complement(meet(X2,X1)),join(X0,meet(X1,complement(meet(X2,X1)))))),
inference(forward_demodulation,[],[f27748,f10584]) ).
fof(f27871,plain,
! [X2,X0,X1] : join(X0,meet(X1,complement(meet(X1,X2)))) = join(X0,meet(complement(meet(X1,X2)),join(X0,meet(X1,complement(meet(X1,X2)))))),
inference(forward_demodulation,[],[f27749,f10584]) ).
fof(f27926,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(complement(meet(X1,complement(meet(X0,X1)))),join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f27817,f10584]) ).
fof(f27927,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(complement(meet(X0,complement(meet(X0,X1)))),join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f27818,f10584]) ).
fof(f27969,plain,
! [X2,X0,X1] : join(meet(X0,complement(meet(X1,X0))),meet(X0,X2)) = meet(X0,join(X2,meet(X0,complement(meet(X1,X0))))),
inference(backward_demodulation,[],[f1034,f27870]) ).
fof(f27970,plain,
! [X2,X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,X2)) = meet(X0,join(X2,meet(X0,complement(meet(X0,X1))))),
inference(backward_demodulation,[],[f788,f27871]) ).
fof(f28007,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,X1))) = join(meet(X0,X1),meet(X1,X2)),
inference(backward_demodulation,[],[f15198,f27926]) ).
fof(f28008,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(X2,meet(X0,X1))),
inference(backward_demodulation,[],[f12503,f27927]) ).
fof(f28035,plain,
! [X0,X1] :
( n0 != meet(X1,join(meet(X0,complement(meet(X1,X0))),meet(X0,complement(X0))))
| complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X1,X0)))) ),
inference(backward_demodulation,[],[f16449,f27969]) ).
fof(f28039,plain,
! [X0,X1] :
( n0 != meet(X1,join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(X0))))
| complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))) ),
inference(backward_demodulation,[],[f15996,f27970]) ).
fof(f28164,plain,
! [X2,X0,X1] : join(X0,join(meet(X2,join(X1,X0)),join(meet(X0,X1),meet(X1,X2)))) = join(X0,meet(complement(join(meet(X0,X1),meet(X0,X2))),join(X0,join(meet(X2,join(X1,X0)),join(meet(X0,X1),meet(X1,X2)))))),
inference(backward_demodulation,[],[f24455,f28007]) ).
fof(f28262,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = join(meet(X2,join(X0,X1)),meet(join(X0,X1),X0)),
inference(backward_demodulation,[],[f4905,f28007]) ).
fof(f28367,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X1,X3)) = meet(X1,join(meet(X3,join(X1,meet(join(X1,X2),X0))),meet(join(X1,X2),join(meet(X0,X1),meet(X0,X3))))),
inference(backward_demodulation,[],[f8690,f28008]) ).
fof(f28436,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,X1),meet(X0,meet(X2,X0))),
inference(backward_demodulation,[],[f231,f28008]) ).
fof(f28506,plain,
! [X0,X1] :
( n0 != meet(X1,join(meet(X0,complement(X0)),meet(X0,complement(meet(X1,X0)))))
| complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X1,X0)))) ),
inference(forward_demodulation,[],[f28035,f6]) ).
fof(f28511,plain,
! [X0,X1] :
( n0 != meet(X1,join(meet(X0,complement(X0)),meet(X0,complement(meet(X0,X1)))))
| complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f28039,f6]) ).
fof(f28576,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = join(meet(X2,join(X0,X1)),meet(X0,join(X0,X1))),
inference(forward_demodulation,[],[f28262,f5]) ).
fof(f28632,plain,
! [X2,X0,X1] : join(X0,join(meet(X1,X2),meet(X2,join(X1,X0)))) = join(X0,meet(complement(join(meet(X0,X1),meet(X0,X2))),join(X0,join(meet(X1,X2),meet(X2,join(X1,X0)))))),
inference(forward_demodulation,[],[f28164,f3773]) ).
fof(f28766,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,X1),meet(X2,X0)),
inference(forward_demodulation,[],[f28436,f69]) ).
fof(f28842,plain,
! [X0,X1] :
( n0 != meet(X1,join(n0,meet(X0,complement(meet(X1,X0)))))
| complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X1,X0)))) ),
inference(forward_demodulation,[],[f28506,f10]) ).
fof(f28846,plain,
! [X0,X1] :
( n0 != meet(X1,join(n0,meet(X0,complement(meet(X0,X1)))))
| complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f28511,f10]) ).
fof(f28896,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = join(meet(X2,join(X0,X1)),X0),
inference(forward_demodulation,[],[f28576,f3]) ).
fof(f28946,plain,
! [X2,X0,X1] : join(X0,meet(X2,join(X1,X0))) = join(X0,meet(complement(join(meet(X0,X1),meet(X0,X2))),join(X0,meet(X2,join(X1,X0))))),
inference(forward_demodulation,[],[f28632,f7147]) ).
fof(f29118,plain,
! [X0,X1] :
( n0 != meet(X1,meet(X0,complement(meet(X1,X0))))
| complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X1,X0)))) ),
inference(forward_demodulation,[],[f28842,f388]) ).
fof(f29122,plain,
! [X0,X1] :
( n0 != meet(X1,meet(X0,complement(meet(X0,X1))))
| complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f28846,f388]) ).
fof(f29148,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = join(X0,meet(X2,join(X0,X1))),
inference(forward_demodulation,[],[f28896,f6]) ).
fof(f29175,plain,
! [X2,X0,X1] : join(X0,meet(X2,join(X1,X0))) = join(X0,meet(join(X0,meet(X2,join(X1,X0))),complement(join(meet(X0,X1),meet(X0,X2))))),
inference(forward_demodulation,[],[f28946,f5]) ).
fof(f29298,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X1,X0)))),
inference(forward_subsumption_resolution,[],[f29118,f370]) ).
fof(f29302,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_subsumption_resolution,[],[f29122,f669]) ).
fof(f29378,plain,
! [X0,X1] :
( n0 != meet(X0,meet(X1,complement(meet(X1,X0))))
| complement(meet(X0,X1)) = join(complement(X0),meet(X0,complement(meet(X1,X0)))) ),
inference(backward_demodulation,[],[f13966,f29298]) ).
fof(f29383,plain,
! [X0,X1] :
( n0 != meet(X0,meet(X1,complement(meet(X1,X0))))
| complement(meet(X0,X1)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))) ),
inference(backward_demodulation,[],[f11868,f29302]) ).
fof(f29431,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),meet(X0,complement(meet(X1,X0)))),
inference(forward_subsumption_resolution,[],[f29378,f669]) ).
fof(f29435,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_subsumption_resolution,[],[f29383,f669]) ).
fof(f29636,plain,
! [X0] : meet(a,join(X0,sF3)) = join(sF3,meet(a,X0)),
inference(superposition,[],[f28008,f518]) ).
fof(f29680,plain,
! [X2,X3,X0,X1] : join(meet(X2,X3),meet(X2,join(X0,X1))) = meet(X2,join(X0,join(X1,meet(X2,X3)))),
inference(superposition,[],[f28008,f8]) ).
fof(f32068,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,join(meet(X0,X1),meet(X0,X2))),
inference(superposition,[],[f44,f28766]) ).
fof(f32128,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,meet(X0,X2)),
inference(forward_demodulation,[],[f32068,f44]) ).
fof(f32314,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = complement(meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f29435,f11249]) ).
fof(f32434,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(join(complement(X0),meet(X0,X1)),X2)),
inference(backward_demodulation,[],[f12466,f32314]) ).
fof(f32964,plain,
! [X2,X3,X0,X1] : meet(meet(join(X1,X2),X0),join(X3,meet(X0,X1))) = join(meet(X0,X1),meet(meet(join(X1,X2),X0),X3)),
inference(superposition,[],[f28007,f533]) ).
fof(f32968,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X2,X0)) = join(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f28007,f3]) ).
fof(f32969,plain,
! [X2,X0,X1] : join(X0,meet(join(X1,X0),X2)) = meet(join(X1,X0),join(X2,X0)),
inference(superposition,[],[f28007,f34]) ).
fof(f33035,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,join(X1,meet(X2,X3)))) = join(meet(X2,X3),meet(X3,join(X0,X1))),
inference(superposition,[],[f28007,f8]) ).
fof(f33107,plain,
! [X2,X3,X0,X1] : meet(X1,join(meet(X0,join(X1,X2)),meet(join(X1,X2),X3))) = meet(X1,join(X3,meet(X0,join(X1,X2)))),
inference(superposition,[],[f111,f28007]) ).
fof(f33267,plain,
! [X2,X0,X1] : join(meet(X2,X0),X1) = join(X1,meet(join(X0,X1),meet(X2,X0))),
inference(backward_demodulation,[],[f952,f32969]) ).
fof(f33306,plain,
! [X2,X3,X0,X1] : meet(meet(join(X1,X2),X0),join(X3,meet(X0,X1))) = join(meet(X0,X1),meet(join(X1,X2),meet(X0,X3))),
inference(forward_demodulation,[],[f32964,f7]) ).
fof(f33443,plain,
! [X2,X0,X1] : join(meet(X2,X0),X1) = join(X1,meet(X0,meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f33267,f125]) ).
fof(f33452,plain,
! [X2,X3,X0,X1] : meet(join(X1,X2),meet(X0,join(X3,meet(X0,X1)))) = join(meet(X0,X1),meet(join(X1,X2),meet(X0,X3))),
inference(forward_demodulation,[],[f33306,f7]) ).
fof(f33551,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = join(meet(X2,X0),X1),
inference(forward_demodulation,[],[f33443,f111]) ).
fof(f33559,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(join(X1,X2),meet(X0,X3))) = meet(join(X1,X2),join(meet(X0,X1),meet(X0,X3))),
inference(forward_demodulation,[],[f33452,f28008]) ).
fof(f33665,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X1,X3)) = meet(X1,join(meet(X3,join(X1,meet(join(X1,X2),X0))),join(meet(X0,X1),meet(join(X1,X2),meet(X0,X3))))),
inference(backward_demodulation,[],[f28367,f33559]) ).
fof(f33720,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X1,X3)) = meet(X1,join(meet(join(X1,X2),meet(X0,X3)),join(meet(X3,join(X1,meet(join(X1,X2),X0))),meet(X0,X1)))),
inference(forward_demodulation,[],[f33665,f56]) ).
fof(f33750,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X1,X3)) = join(meet(X0,X1),meet(X1,join(meet(join(X1,X2),meet(X0,X3)),meet(X3,join(X1,meet(join(X1,X2),X0)))))),
inference(forward_demodulation,[],[f33720,f33035]) ).
fof(f33919,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X0,meet(join(X0,X1),X2))),
inference(superposition,[],[f112,f32968]) ).
fof(f33930,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X2,X0),join(X0,X1)),
inference(superposition,[],[f5,f32968]) ).
fof(f34857,plain,
! [X2,X3,X0,X1] : join(join(X1,meet(X0,X2)),meet(join(X0,X1),X3)) = meet(join(X0,X1),join(X3,join(X1,meet(X0,X2)))),
inference(superposition,[],[f32969,f599]) ).
fof(f34927,plain,
! [X2,X3,X0,X1] : join(join(X1,meet(X0,X2)),meet(join(X3,join(X1,meet(X0,X2))),X0)) = meet(join(X3,join(X1,meet(X0,X2))),join(X0,X1)),
inference(superposition,[],[f32969,f599]) ).
fof(f34987,plain,
! [X2,X0,X1] : join(X0,meet(join(X1,X0),X2)) = join(meet(join(X2,X0),X1),join(X0,meet(join(X1,X0),X2))),
inference(superposition,[],[f8695,f32969]) ).
fof(f35022,plain,
! [X2,X3,X0,X1] : meet(join(X0,meet(join(X1,X0),X2)),X3) = meet(join(X1,X0),meet(X3,join(X2,X0))),
inference(superposition,[],[f1678,f32969]) ).
fof(f35096,plain,
! [X2,X0,X1] : join(X0,meet(join(X1,X0),X2)) = join(X0,join(meet(join(X1,X0),X2),meet(join(X2,X0),X1))),
inference(forward_demodulation,[],[f34987,f56]) ).
fof(f35155,plain,
! [X2,X3,X0,X1] : meet(join(X0,X1),join(X3,join(X1,meet(X0,X2)))) = join(join(X1,meet(X0,X2)),meet(join(X3,join(X1,meet(X0,X2))),X0)),
inference(forward_demodulation,[],[f34927,f5]) ).
fof(f35205,plain,
! [X2,X3,X0,X1] : meet(join(X0,X1),join(X3,join(X1,meet(X0,X2)))) = join(X1,join(meet(X0,X2),meet(join(X0,X1),X3))),
inference(forward_demodulation,[],[f34857,f8]) ).
fof(f35253,plain,
! [X2,X0,X1] : join(X0,meet(join(X1,X0),X2)) = join(X0,join(meet(X1,join(X2,X0)),meet(join(X1,X0),X2))),
inference(forward_demodulation,[],[f35096,f33551]) ).
fof(f35302,plain,
! [X2,X3,X0,X1] : meet(join(X0,X1),join(X3,join(X1,meet(X0,X2)))) = join(join(X1,meet(X0,X2)),meet(X0,join(X3,join(X1,meet(X0,X2))))),
inference(forward_demodulation,[],[f35155,f32128]) ).
fof(f35420,plain,
! [X2,X3,X0,X1] : meet(join(X0,X1),join(X3,join(X1,meet(X0,X2)))) = join(X1,join(meet(X0,X2),meet(X0,join(X3,join(X1,meet(X0,X2)))))),
inference(forward_demodulation,[],[f35302,f8]) ).
fof(f35500,plain,
! [X2,X3,X0,X1] : join(X1,join(meet(X0,X2),join(meet(X0,X2),meet(X0,join(X3,X1))))) = meet(join(X0,X1),join(X3,join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f35420,f29680]) ).
fof(f35523,plain,
! [X2,X3,X0,X1] : join(X1,join(meet(X0,X2),join(meet(X0,X2),meet(X0,join(X3,X1))))) = join(X1,join(meet(X0,X2),meet(join(X0,X1),X3))),
inference(forward_demodulation,[],[f35500,f35205]) ).
fof(f35537,plain,
! [X2,X3,X0,X1] : join(X1,join(meet(X0,X2),meet(X0,join(X3,X1)))) = join(X1,join(meet(X0,X2),meet(join(X0,X1),X3))),
inference(forward_demodulation,[],[f35523,f41]) ).
fof(f35554,plain,
! [X2,X0,X1] : join(X0,meet(join(X1,X0),X2)) = join(X0,join(meet(X1,join(X2,X0)),meet(X1,join(X2,X0)))),
inference(backward_demodulation,[],[f35253,f35537]) ).
fof(f35562,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X2,X0))) = join(X0,meet(join(X1,X0),X2)),
inference(forward_demodulation,[],[f35554,f2]) ).
fof(f35588,plain,
! [X2,X3,X0,X1] : meet(join(X0,meet(X1,join(X2,X0))),X3) = meet(join(X1,X0),meet(X3,join(X2,X0))),
inference(backward_demodulation,[],[f35022,f35562]) ).
fof(f35691,plain,
! [X2,X0,X1] : join(X0,meet(X2,join(X1,X0))) = join(X0,meet(join(X2,X0),meet(complement(join(meet(X0,X1),meet(X0,X2))),join(X1,X0)))),
inference(backward_demodulation,[],[f29175,f35588]) ).
fof(f35722,plain,
! [X2,X0,X1] : join(X0,meet(X2,join(X1,X0))) = join(X0,meet(X2,join(meet(complement(join(meet(X0,X1),meet(X0,X2))),join(X1,X0)),X0))),
inference(forward_demodulation,[],[f35691,f35562]) ).
fof(f35742,plain,
! [X2,X0,X1] : join(X0,meet(X2,join(X1,X0))) = join(X0,meet(X2,join(X0,meet(complement(join(meet(X0,X1),meet(X0,X2))),join(X1,X0))))),
inference(forward_demodulation,[],[f35722,f6]) ).
fof(f35753,plain,
! [X2,X0,X1] : join(X0,meet(X2,join(X1,X0))) = join(X0,meet(X2,join(X0,meet(join(X1,X0),complement(join(meet(X0,X1),meet(X0,X2))))))),
inference(forward_demodulation,[],[f35742,f8034]) ).
fof(f35757,plain,
! [X2,X0,X1] : join(X0,meet(X2,join(X1,X0))) = join(X0,meet(X2,join(X0,meet(X1,join(complement(join(meet(X0,X1),meet(X0,X2))),X0))))),
inference(forward_demodulation,[],[f35753,f35562]) ).
fof(f35759,plain,
! [X2,X0,X1] : join(X0,meet(X2,join(X1,X0))) = join(X0,meet(X2,join(X0,meet(X1,join(X0,complement(join(meet(X0,X1),meet(X0,X2)))))))),
inference(forward_demodulation,[],[f35757,f6]) ).
fof(f35761,plain,
! [X2,X0,X1] : join(X0,meet(X2,join(X1,X0))) = join(X0,meet(X2,join(X0,meet(X1,n1)))),
inference(forward_demodulation,[],[f35759,f756]) ).
fof(f35763,plain,
! [X2,X0,X1] : join(X0,meet(X2,join(X1,X0))) = join(X0,meet(X2,join(X0,X1))),
inference(forward_demodulation,[],[f35761,f246]) ).
fof(f36137,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = join(meet(X0,complement(meet(X1,X0))),meet(X0,complement(X0))),
inference(superposition,[],[f28008,f29431]) ).
fof(f36189,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = join(meet(X0,complement(X0)),meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f36137,f6]) ).
fof(f36276,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = join(n0,meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f36189,f10]) ).
fof(f36350,plain,
! [X0,X1] : meet(X0,complement(meet(X1,X0))) = meet(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f36276,f388]) ).
fof(f36552,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = complement(meet(X0,complement(meet(X1,X0)))),
inference(superposition,[],[f32314,f36350]) ).
fof(f36909,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(superposition,[],[f29435,f29302]) ).
fof(f36918,plain,
! [X0,X1] : complement(X1) = meet(complement(X1),complement(meet(X0,X1))),
inference(superposition,[],[f3,f29302]) ).
fof(f37363,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f36918,f3]) ).
fof(f37508,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f37363,f5]) ).
fof(f38062,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f4,f37508]) ).
fof(f38693,plain,
! [X0,X1] : complement(X1) = join(complement(X1),complement(join(X0,X1))),
inference(superposition,[],[f38062,f68]) ).
fof(f39098,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(join(X1,X0)),join(complement(X0),X2)),
inference(superposition,[],[f46,f38693]) ).
fof(f39137,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(X0),join(X2,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f39098,f56]) ).
fof(f39256,plain,
! [X0,X1] : complement(meet(join(X1,X0),complement(X0))) = join(complement(join(X1,X0)),meet(join(X1,X0),X0)),
inference(superposition,[],[f36552,f34]) ).
fof(f39445,plain,
! [X0,X1] : complement(meet(join(X1,X0),complement(X0))) = join(complement(join(X1,X0)),meet(X0,join(X1,X0))),
inference(forward_demodulation,[],[f39256,f32128]) ).
fof(f39539,plain,
! [X0,X1] : join(complement(join(X1,X0)),X0) = complement(meet(join(X1,X0),complement(X0))),
inference(forward_demodulation,[],[f39445,f34]) ).
fof(f39623,plain,
! [X0,X1] : join(complement(join(X1,X0)),X0) = complement(meet(complement(X0),join(X1,X0))),
inference(forward_demodulation,[],[f39539,f36909]) ).
fof(f39691,plain,
! [X0,X1] : join(X0,complement(join(X1,X0))) = complement(meet(complement(X0),join(X1,X0))),
inference(forward_demodulation,[],[f39623,f6]) ).
fof(f39743,plain,
! [X0,X1] : meet(join(X1,X0),join(X0,complement(join(X1,X0)))) = X0,
inference(backward_demodulation,[],[f15169,f39691]) ).
fof(f39779,plain,
! [X0,X1] : join(X0,meet(join(X0,complement(join(X1,X0))),X1)) = X0,
inference(forward_demodulation,[],[f39743,f33930]) ).
fof(f39801,plain,
! [X0,X1] : join(X0,meet(X1,join(X0,complement(join(X1,X0))))) = X0,
inference(forward_demodulation,[],[f39779,f29148]) ).
fof(f39937,plain,
! [X0,X1] : meet(X1,join(X0,complement(join(X1,X0)))) = meet(meet(X1,join(X0,complement(join(X1,X0)))),X0),
inference(superposition,[],[f34,f39801]) ).
fof(f40014,plain,
! [X0,X1] : meet(X1,join(X0,complement(join(X1,X0)))) = meet(X0,meet(X1,join(X0,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f39937,f5]) ).
fof(f40098,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(X0,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f40014,f446]) ).
fof(f40157,plain,
! [X0,X1] :
( complement(X0) = join(X1,complement(join(X0,X1)))
| meet(X1,X0) != n0 ),
inference(backward_demodulation,[],[f876,f40098]) ).
fof(f40330,plain,
! [X0,X1] :
( complement(X1) = join(complement(join(X0,X1)),complement(complement(X0)))
| n0 != meet(complement(join(X0,X1)),X1)
| meet(X1,X0) != n0 ),
inference(superposition,[],[f40157,f40157]) ).
fof(f40497,plain,
! [X0,X1] :
( complement(X1) = join(complement(complement(X0)),complement(join(X0,X1)))
| n0 != meet(complement(join(X0,X1)),X1)
| meet(X1,X0) != n0 ),
inference(forward_demodulation,[],[f40330,f6]) ).
fof(f40557,plain,
! [X0,X1] :
( complement(X1) = join(X0,complement(join(X0,X1)))
| n0 != meet(complement(join(X0,X1)),X1)
| meet(X1,X0) != n0 ),
inference(forward_demodulation,[],[f40497,f8415]) ).
fof(f40598,plain,
! [X0,X1] :
( n0 != meet(X1,complement(join(X0,X1)))
| complement(X1) = join(X0,complement(join(X0,X1)))
| meet(X1,X0) != n0 ),
inference(forward_demodulation,[],[f40557,f5]) ).
fof(f40623,plain,
! [X0,X1] :
( complement(X1) = join(X0,complement(join(X0,X1)))
| meet(X1,X0) != n0 ),
inference(forward_subsumption_resolution,[],[f40598,f1349]) ).
fof(f41798,plain,
! [X0,X1] :
( join(X0,complement(join(X0,X1))) = complement(meet(X1,complement(meet(X1,X0))))
| n0 != meet(meet(X1,complement(meet(X1,X0))),X0) ),
inference(superposition,[],[f40623,f11608]) ).
fof(f42028,plain,
! [X0,X1] :
( join(X0,complement(join(X0,X1))) = join(complement(X1),meet(X1,X0))
| n0 != meet(meet(X1,complement(meet(X1,X0))),X0) ),
inference(forward_demodulation,[],[f41798,f32314]) ).
fof(f42088,plain,
! [X0,X1] :
( n0 != meet(X0,meet(X1,complement(meet(X1,X0))))
| join(X0,complement(join(X0,X1))) = join(complement(X1),meet(X1,X0)) ),
inference(forward_demodulation,[],[f42028,f5]) ).
fof(f42125,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = join(complement(X1),meet(X1,X0)),
inference(forward_subsumption_resolution,[],[f42088,f669]) ).
fof(f42169,plain,
! [X0,X1] : join(X0,meet(complement(X0),X1)) = join(X1,complement(join(X1,complement(X0)))),
inference(superposition,[],[f42125,f8415]) ).
fof(f42195,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = join(X1,join(complement(X0),meet(X0,X1))),
inference(superposition,[],[f41,f42125]) ).
fof(f42258,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = join(complement(X1),join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f41,f42125]) ).
fof(f42308,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = join(complement(X1),X0),
inference(forward_demodulation,[],[f42258,f39137]) ).
fof(f42349,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),meet(X0,X1)),
inference(forward_demodulation,[],[f42195,f924]) ).
fof(f42446,plain,
! [X0,X1] : join(X0,meet(complement(X0),X1)) = join(complement(complement(X0)),X1),
inference(backward_demodulation,[],[f42169,f42308]) ).
fof(f42495,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(join(X1,complement(X0)),X2)),
inference(backward_demodulation,[],[f32434,f42349]) ).
fof(f42654,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(complement(X0),X1)),
inference(forward_demodulation,[],[f42446,f8415]) ).
fof(f61089,plain,
! [X2,X0,X1] : join(X0,meet(complement(X0),meet(X1,X2))) = join(X0,meet(join(X1,complement(complement(X0))),X2)),
inference(superposition,[],[f42654,f42495]) ).
fof(f61114,plain,
! [X2,X0,X1] : join(X0,meet(join(X1,X0),X2)) = join(X0,meet(complement(X0),meet(X1,X2))),
inference(forward_demodulation,[],[f61089,f8415]) ).
fof(f61220,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(join(X1,X0),X2)),
inference(forward_demodulation,[],[f61114,f42654]) ).
fof(f61290,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(X1,join(X2,X0))),
inference(backward_demodulation,[],[f35562,f61220]) ).
fof(f61347,plain,
! [X2,X0,X1] : join(X0,meet(X2,X1)) = join(X0,meet(X2,join(X0,X1))),
inference(backward_demodulation,[],[f35763,f61290]) ).
fof(f61430,plain,
! [X2,X0,X1] : join(X0,meet(X2,X1)) = join(X0,meet(join(X0,X1),X2)),
inference(backward_demodulation,[],[f29148,f61347]) ).
fof(f61611,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X1,X3)) = join(meet(X0,X1),meet(X1,join(meet(join(X1,X2),meet(X0,X3)),meet(X3,join(X1,meet(X0,X2)))))),
inference(backward_demodulation,[],[f33750,f61430]) ).
fof(f61613,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X0,meet(X2,X1))),
inference(backward_demodulation,[],[f33919,f61430]) ).
fof(f61823,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X2)) = meet(X1,join(X0,X2)),
inference(backward_demodulation,[],[f28007,f61613]) ).
fof(f61974,plain,
! [X2,X3,X0,X1] : meet(X1,join(X0,X3)) = join(meet(X0,X1),meet(X1,join(meet(join(X1,X2),meet(X0,X3)),meet(X3,join(X1,meet(X0,X2)))))),
inference(backward_demodulation,[],[f61611,f61823]) ).
fof(f62019,plain,
! [X2,X3,X0,X1] : meet(X1,join(X3,meet(X0,join(X1,X2)))) = meet(X1,meet(join(X1,X2),join(X0,X3))),
inference(backward_demodulation,[],[f33107,f61823]) ).
fof(f62289,plain,
! [X2,X3,X0,X1] : meet(X1,join(X0,X3)) = meet(X1,join(X3,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f62019,f111]) ).
fof(f62317,plain,
! [X2,X3,X0,X1] : meet(X1,join(X0,X3)) = meet(X1,join(X0,join(meet(join(X1,X2),meet(X0,X3)),meet(X3,join(X1,meet(X0,X2)))))),
inference(forward_demodulation,[],[f61974,f61823]) ).
fof(f62859,plain,
! [X2,X3,X0,X1] : meet(X1,join(X0,X3)) = meet(X1,join(X0,meet(X3,join(X1,meet(X0,X2))))),
inference(forward_demodulation,[],[f62317,f950]) ).
fof(f63401,plain,
! [X3,X0,X1] : meet(X1,join(X0,X3)) = meet(X1,join(X3,X0)),
inference(forward_demodulation,[],[f62859,f62289]) ).
fof(f65321,plain,
! [X0] : join(sF2,meet(a,X0)) = meet(a,join(b,X0)),
inference(superposition,[],[f61823,f25]) ).
fof(f65330,plain,
! [X0] : join(sF3,meet(a,X0)) = meet(a,join(c,X0)),
inference(superposition,[],[f61823,f26]) ).
fof(f65628,plain,
! [X0] : meet(a,join(X0,sF3)) = meet(a,join(c,X0)),
inference(backward_demodulation,[],[f29636,f65330]) ).
fof(f66558,plain,
join(sF2,sF3) = meet(a,join(b,sF3)),
inference(superposition,[],[f65321,f518]) ).
fof(f66707,plain,
join(sF2,sF3) = meet(a,join(c,b)),
inference(forward_demodulation,[],[f66558,f65628]) ).
fof(f66755,plain,
meet(a,join(b,c)) = join(sF2,sF3),
inference(forward_demodulation,[],[f66707,f63401]) ).
fof(f66789,plain,
meet(a,join(b,c)) = sF4,
inference(forward_demodulation,[],[f66755,f23]) ).
fof(f66815,plain,
meet(a,sF0) = sF4,
inference(forward_demodulation,[],[f66789,f15]) ).
fof(f66828,plain,
sF1 = sF4,
inference(forward_demodulation,[],[f66815,f17]) ).
fof(f66832,plain,
$false,
inference(forward_subsumption_resolution,[],[f66828,f24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT065-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/0.40 % Computer : n011.cluster.edu
% 0.15/0.40 % Model : x86_64 x86_64
% 0.15/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.40 % Memory : 8046.5625MB
% 0.15/0.40 % OS : Linux 6.8.0-71-generic
% 0.15/0.40 % CPULimit : 300
% 0.15/0.40 % WCLimit : 300
% 0.15/0.40 % DateTime : Sun Sep 27 13:59:00 UTC 2026
% 0.15/0.40 % CPUTime :
% 0.15/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/0.46 Running first-order theorem proving
% 0.15/0.46 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.15/3.58 % (2432294)Input is clausal, will run a generic CNF schedule.
% 18.15/3.58 % (2432304)lrs+10_1_sil=8000:sp=occurrence:random_seed=1260363541:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 18.15/3.58 % (2432304)Instruction limit reached!
% 18.15/3.58 % (2432304)------------------------------
% 18.15/3.58 % (2432304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.15/3.58 % (2432304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.15/3.58 % (2432304)CaDiCaL version: 2.1.3
% 18.15/3.58 % (2432304)Termination reason: Instruction limit
% 18.15/3.58 % (2432304)Termination phase: Saturation
% 18.15/3.58 % (2432304)Time elapsed: 0.055 s
% 18.15/3.58 % (2432304)Peak memory usage: 89 MB
% 18.15/3.58 % (2432304)Instructions burned: 107 (million)
% 18.15/3.58 % (2432305)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2651149322:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 18.15/3.58 % (2432301)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=704169018:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 18.15/3.58 % (2432306)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3401322252:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 18.15/3.58 % (2432302)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=268136631:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 18.15/3.58 % (2432307)dis-21_1_sil=8000:lcm=predicate:random_seed=1513116398: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.58 % (2432303)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=78525048:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 18.15/3.58 % (2432307)Refutation not found, incomplete strategy
% 18.15/3.58 % (2432307)------------------------------
% 18.15/3.58 % (2432307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.15/3.58 % (2432307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.15/3.58 % (2432307)CaDiCaL version: 2.1.3
% 18.15/3.58 % (2432307)Termination reason: Refutation not found, incomplete strategy
% 18.15/3.58 % (2432307)Time elapsed: 0.003 s
% 18.15/3.58 % (2432307)Peak memory usage: 88 MB
% 18.15/3.58 % (2432307)Instructions burned: 1 (million)
% 18.15/3.58 % (2432305)Instruction limit reached!
% 18.15/3.58 % (2432305)------------------------------
% 18.15/3.58 % (2432305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.15/3.58 % (2432305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.15/3.58 % (2432305)CaDiCaL version: 2.1.3
% 18.15/3.58 % (2432305)Termination reason: Instruction limit
% 18.15/3.58 % (2432305)Termination phase: Saturation
% 18.15/3.58 % (2432305)Time elapsed: 0.112 s
% 18.15/3.58 % (2432305)Peak memory usage: 89 MB
% 18.15/3.58 % (2432305)Instructions burned: 114 (million)
% 18.15/3.58 % (2432306)Instruction limit reached!
% 18.15/3.58 % (2432306)------------------------------
% 18.15/3.58 % (2432306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.15/3.58 % (2432306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.15/3.58 % (2432306)CaDiCaL version: 2.1.3
% 18.15/3.58 % (2432306)Termination reason: Instruction limit
% 18.15/3.58 % (2432306)Termination phase: Saturation
% 18.15/3.58 % (2432306)Time elapsed: 0.169 s
% 18.15/3.58 % (2432306)Peak memory usage: 89 MB
% 18.15/3.58 % (2432306)Instructions burned: 180 (million)
% 18.15/3.58 % (2432316)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=1027599122:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 18.15/3.58 % (2432316)Refutation not found, incomplete strategy
% 18.15/3.58 % (2432316)------------------------------
% 18.15/3.58 % (2432316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.15/3.58 % (2432316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.15/3.58 % (2432316)CaDiCaL version: 2.1.3
% 18.15/3.58 % (2432316)Termination reason: Refutation not found, incomplete strategy
% 18.15/3.58 % (2432316)Time elapsed: 0.001 s
% 18.15/3.58 % (2432316)Peak memory usage: 88 MB
% 18.15/3.58 % (2432307)------------------------------
% 18.15/3.58 % (2432307)------------------------------
% 32.74/5.66 % (2432317)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1506331098:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 32.74/5.66 % (2432317)Refutation not found, incomplete strategy
% 32.74/5.66 % (2432317)------------------------------
% 32.74/5.66 % (2432317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.74/5.66 % (2432317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.74/5.66 % (2432317)CaDiCaL version: 2.1.3
% 32.74/5.66 % (2432317)Termination reason: Refutation not found, incomplete strategy
% 32.74/5.66 % (2432317)Time elapsed: 0.003 s
% 32.74/5.66 % (2432317)Peak memory usage: 88 MB
% 32.74/5.66 % (2432317)Instructions burned: 1 (million)
% 32.74/5.66 % (2432316)------------------------------
% 32.74/5.66 % (2432316)------------------------------
% 32.74/5.66 % (2432318)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1764888218:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 32.74/5.66 % (2432318)Refutation not found, incomplete strategy
% 32.74/5.66 % (2432318)------------------------------
% 32.74/5.66 % (2432318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.74/5.66 % (2432318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.74/5.66 % (2432318)CaDiCaL version: 2.1.3
% 32.74/5.66 % (2432318)Termination reason: Refutation not found, incomplete strategy
% 32.74/5.66 % (2432318)Time elapsed: 0.002 s
% 32.74/5.66 % (2432318)Peak memory usage: 88 MB
% 32.74/5.66 % (2432321)lrs+10_64_to=lpo:sil=8000:random_seed=307383351:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 32.74/5.66 % (2432322)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2151910150:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 32.74/5.66 % (2432321)Instruction limit reached!
% 32.74/5.66 % (2432321)------------------------------
% 32.74/5.66 % (2432321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.74/5.66 % (2432321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.74/5.66 % (2432321)CaDiCaL version: 2.1.3
% 32.74/5.66 % (2432321)Termination reason: Instruction limit
% 32.74/5.66 % (2432321)Termination phase: Saturation
% 32.74/5.66 % (2432321)Time elapsed: 0.121 s
% 32.74/5.66 % (2432321)Peak memory usage: 88 MB
% 32.74/5.66 % (2432321)Instructions burned: 126 (million)
% 32.74/5.66 % (2432322)Instruction limit reached!
% 32.74/5.66 % (2432322)------------------------------
% 32.74/5.66 % (2432322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.74/5.66 % (2432322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.74/5.66 % (2432322)CaDiCaL version: 2.1.3
% 32.74/5.66 % (2432322)Termination reason: Instruction limit
% 32.74/5.66 % (2432322)Termination phase: Saturation
% 32.74/5.66 % (2432322)Time elapsed: 0.102 s
% 32.74/5.66 % (2432322)Peak memory usage: 89 MB
% 32.74/5.66 % (2432322)Instructions burned: 195 (million)
% 32.74/5.66 % (2432317)------------------------------
% 32.74/5.66 % (2432317)------------------------------
% 32.74/5.66 % (2432318)------------------------------
% 32.74/5.66 % (2432318)------------------------------
% 32.74/5.66 % (2432327)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1408544772:i=157:gtg=all_2989 on theBenchmark for (2989ds/157Mi)
% 32.74/5.66 % (2432329)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=295759224:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2989 on theBenchmark for (2989ds/106Mi)
% 32.74/5.66 % (2432328)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=269001619:i=3394:sd=4:ss=included:sgt=64_2989 on theBenchmark for (2989ds/3394Mi)
% 32.74/5.66 % (2432327)Instruction limit reached!
% 32.74/5.66 % (2432327)------------------------------
% 32.74/5.66 % (2432327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.74/5.66 % (2432327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.74/5.66 % (2432327)CaDiCaL version: 2.1.3
% 32.74/5.66 % (2432327)Termination reason: Instruction limit
% 32.74/5.66 % (2432327)Termination phase: Saturation
% 32.74/5.66 % (2432327)Time elapsed: 0.082 s
% 32.74/5.66 % (2432327)Peak memory usage: 90 MB
% 32.74/5.66 % (2432327)Instructions burned: 159 (million)
% 32.74/5.66 % (2432329)Instruction limit reached!
% 32.74/5.66 % (2432329)------------------------------
% 52.54/8.31 % (2432329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.54/8.31 % (2432329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.54/8.31 % (2432329)CaDiCaL version: 2.1.3
% 52.54/8.31 % (2432329)Termination reason: Instruction limit
% 52.54/8.31 % (2432329)Termination phase: Saturation
% 52.54/8.31 % (2432329)Time elapsed: 0.090 s
% 52.54/8.31 % (2432329)Peak memory usage: 89 MB
% 52.54/8.31 % (2432329)Instructions burned: 107 (million)
% 52.54/8.31 % (2432331)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1812583400:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 52.54/8.31 % (2432331)Refutation not found, incomplete strategy
% 52.54/8.31 % (2432331)------------------------------
% 52.54/8.31 % (2432331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.54/8.31 % (2432331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.54/8.31 % (2432331)CaDiCaL version: 2.1.3
% 52.54/8.31 % (2432331)Termination reason: Refutation not found, incomplete strategy
% 52.54/8.31 % (2432331)Time elapsed: 0.002 s
% 52.54/8.31 % (2432331)Peak memory usage: 87 MB
% 52.54/8.31 % (2432335)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3920332207:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2986 on theBenchmark for (2986ds/242Mi)
% 52.54/8.31 % (2432336)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1326728432:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi)
% 52.54/8.31 % (2432335)Instruction limit reached!
% 52.54/8.31 % (2432335)------------------------------
% 52.54/8.31 % (2432335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.54/8.31 % (2432335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.54/8.31 % (2432335)CaDiCaL version: 2.1.3
% 52.54/8.31 % (2432335)Termination reason: Instruction limit
% 52.54/8.31 % (2432335)Termination phase: Saturation
% 52.54/8.31 % (2432335)Time elapsed: 0.210 s
% 52.54/8.31 % (2432335)Peak memory usage: 90 MB
% 52.54/8.31 % (2432335)Instructions burned: 242 (million)
% 52.54/8.31 % (2432331)------------------------------
% 52.54/8.31 % (2432331)------------------------------
% 52.54/8.31 % (2432340)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3979783853:i=134:sd=2:doe=on:ss=axioms:sgt=14_2982 on theBenchmark for (2982ds/134Mi)
% 52.54/8.31 % (2432341)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=352245572:i=499:bd=all_2981 on theBenchmark for (2981ds/499Mi)
% 52.54/8.31 % (2432340)Instruction limit reached!
% 52.54/8.31 % (2432340)------------------------------
% 52.54/8.31 % (2432340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.54/8.31 % (2432340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.54/8.31 % (2432340)CaDiCaL version: 2.1.3
% 52.54/8.31 % (2432340)Termination reason: Instruction limit
% 52.54/8.31 % (2432340)Termination phase: Saturation
% 52.54/8.31 % (2432340)Time elapsed: 0.131 s
% 52.54/8.31 % (2432340)Peak memory usage: 89 MB
% 52.54/8.31 % (2432340)Instructions burned: 134 (million)
% 52.54/8.31 % (2432344)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1675514800:i=191:fgj=on:bd=all_2978 on theBenchmark for (2978ds/191Mi)
% 52.54/8.31 % (2432344)Instruction limit reached!
% 52.54/8.31 % (2432344)------------------------------
% 52.54/8.31 % (2432344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.54/8.31 % (2432344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.54/8.31 % (2432344)CaDiCaL version: 2.1.3
% 52.54/8.31 % (2432344)Termination reason: Instruction limit
% 52.54/8.31 % (2432344)Termination phase: Saturation
% 52.54/8.31 % (2432344)Time elapsed: 0.197 s
% 52.54/8.31 % (2432344)Peak memory usage: 91 MB
% 52.54/8.31 % (2432344)Instructions burned: 191 (million)
% 52.54/8.31 % (2432341)Instruction limit reached!
% 52.54/8.31 % (2432341)------------------------------
% 52.54/8.31 % (2432341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.54/8.31 % (2432341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.54/8.31 % (2432341)CaDiCaL version: 2.1.3
% 52.54/8.31 % (2432341)Termination reason: Instruction limit
% 52.54/8.31 % (2432341)Termination phase: Saturation
% 52.54/8.31 % (2432341)Time elapsed: 0.513 s
% 52.54/8.31 % (2432341)Peak memory usage: 94 MB
% 52.54/8.31 % (2432341)Instructions burned: 499 (million)
% 33.03/9.92 % (2432346)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2734036357:i=264:kws=precedence:fsr=off_2973 on theBenchmark for (2973ds/264Mi)
% 33.03/9.92 % (2432347)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1911379548:cond=on:i=156:bs=on:gtg=exists_all:er=known_2973 on theBenchmark for (2973ds/156Mi)
% 33.03/9.92 % (2432347)Instruction limit reached!
% 33.03/9.92 % (2432347)------------------------------
% 33.03/9.92 % (2432347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.03/9.92 % (2432347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.03/9.92 % (2432347)CaDiCaL version: 2.1.3
% 33.03/9.92 % (2432347)Termination reason: Instruction limit
% 33.03/9.92 % (2432347)Termination phase: Saturation
% 33.03/9.92 % (2432347)Time elapsed: 0.153 s
% 33.03/9.92 % (2432347)Peak memory usage: 89 MB
% 33.03/9.92 % (2432347)Instructions burned: 156 (million)
% 33.03/9.92 % (2432346)Instruction limit reached!
% 33.03/9.92 % (2432346)------------------------------
% 33.03/9.92 % (2432346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.03/9.92 % (2432346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.03/9.92 % (2432346)CaDiCaL version: 2.1.3
% 33.03/9.92 % (2432346)Termination reason: Instruction limit
% 33.03/9.92 % (2432346)Termination phase: Saturation
% 33.03/9.92 % (2432346)Time elapsed: 0.260 s
% 33.03/9.92 % (2432346)Peak memory usage: 91 MB
% 33.03/9.92 % (2432346)Instructions burned: 264 (million)
% 33.03/9.92 % (2432351)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3663234461:i=537:av=off:ss=included_2968 on theBenchmark for (2968ds/537Mi)
% 33.03/9.92 % (2432350)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=425575337:i=3256:kws=precedence:bd=preordered:av=off_2969 on theBenchmark for (2969ds/3256Mi)
% 33.03/9.92 % (2432351)Instruction limit reached!
% 33.03/9.92 % (2432351)------------------------------
% 33.03/9.92 % (2432351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.03/9.92 % (2432351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.03/9.92 % (2432351)CaDiCaL version: 2.1.3
% 33.03/9.92 % (2432351)Termination reason: Instruction limit
% 33.03/9.92 % (2432351)Termination phase: Saturation
% 33.03/9.92 % (2432351)Time elapsed: 0.492 s
% 33.03/9.92 % (2432351)Peak memory usage: 92 MB
% 33.03/9.92 % (2432351)Instructions burned: 537 (million)
% 33.03/9.92 % (2432354)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=893704898:i=180:bd=preordered:av=off_2961 on theBenchmark for (2961ds/180Mi)
% 33.03/9.92 % (2432354)Instruction limit reached!
% 33.03/9.92 % (2432354)------------------------------
% 33.03/9.92 % (2432354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.03/9.92 % (2432354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.03/9.92 % (2432354)CaDiCaL version: 2.1.3
% 33.03/9.92 % (2432354)Termination reason: Instruction limit
% 33.03/9.92 % (2432354)Termination phase: Saturation
% 33.03/9.92 % (2432354)Time elapsed: 0.170 s
% 33.03/9.92 % (2432354)Peak memory usage: 88 MB
% 33.03/9.92 % (2432354)Instructions burned: 180 (million)
% 33.03/9.92 % (2432336)Instruction limit reached!
% 33.03/9.92 % (2432336)------------------------------
% 33.03/9.92 % (2432336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.03/9.92 % (2432336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.03/9.92 % (2432336)CaDiCaL version: 2.1.3
% 33.03/9.92 % (2432336)Termination reason: Instruction limit
% 33.03/9.92 % (2432336)Termination phase: Saturation
% 33.03/9.92 % (2432336)Time elapsed: 2.826 s
% 33.03/9.92 % (2432336)Peak memory usage: 170 MB
% 33.03/9.92 % (2432336)Instructions burned: 5209 (million)
% 33.03/9.92 % (2432356)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=1877473150:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2957 on theBenchmark for (2957ds/10307Mi)
% 33.03/9.92 % (2432357)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=48829135:i=412:gtgl=4:gtg=exists_all_2956 on theBenchmark for (2956ds/412Mi)
% 33.03/9.92 % (2432328)Instruction limit reached!
% 33.03/9.92 % (2432328)------------------------------
% 33.03/9.92 % (2432328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.03/9.92 % (2432328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.03/9.92 % (2432328)CaDiCaL version: 2.1.3
% 33.03/9.92 % (2432328)Termination reason: Instruction limit
% 33.03/9.92 % (2432328)Termination phase: Saturation
% 33.03/9.92 % (2432328)Time elapsed: 3.458 s
% 33.03/9.92 % (2432328)Peak memory usage: 150 MB
% 33.03/9.92 % (2432328)Instructions burned: 3395 (million)
% 33.03/9.92 % (2432360)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=158613109:s2pl=no:i=8478:s2at=4:nm=6_2952 on theBenchmark for (2952ds/8478Mi)
% 33.03/9.92 % (2432357)Instruction limit reached!
% 33.03/9.92 % (2432357)------------------------------
% 33.03/9.92 % (2432357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.03/9.92 % (2432357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.03/9.92 % (2432357)CaDiCaL version: 2.1.3
% 33.03/9.92 % (2432357)Termination reason: Instruction limit
% 33.03/9.92 % (2432357)Termination phase: Saturation
% 33.03/9.92 % (2432357)Time elapsed: 0.404 s
% 33.03/9.92 % (2432357)Peak memory usage: 94 MB
% 33.03/9.92 % (2432357)Instructions burned: 412 (million)
% 33.03/9.92 % (2432362)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=4117838351:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2949 on theBenchmark for (2949ds/303Mi)
% 33.03/9.92 % (2432362)Refutation not found, incomplete strategy
% 33.03/9.92 % (2432362)------------------------------
% 33.03/9.92 % (2432362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.03/9.92 % (2432362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.03/9.92 % (2432362)CaDiCaL version: 2.1.3
% 33.03/9.92 % (2432362)Termination reason: Refutation not found, incomplete strategy
% 33.03/9.92 % (2432362)Time elapsed: 0.003 s
% 33.03/9.92 % (2432362)Peak memory usage: 88 MB
% 33.03/9.92 % (2432362)Instructions burned: 1 (million)
% 33.03/9.92 % (2432362)------------------------------
% 33.03/9.92 % (2432362)------------------------------
% 33.03/9.92 % (2432365)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3010337858:st=4:i=720:sd=3:fsr=off:ss=axioms_2942 on theBenchmark for (2942ds/720Mi)
% 33.03/9.92 % (2432365)Refutation not found, incomplete strategy
% 33.03/9.92 % (2432365)------------------------------
% 33.03/9.92 % (2432365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.03/9.92 % (2432365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.03/9.92 % (2432365)CaDiCaL version: 2.1.3
% 33.03/9.92 % (2432365)Termination reason: Refutation not found, incomplete strategy
% 33.03/9.92 % (2432365)Time elapsed: 0.002 s
% 33.03/9.92 % (2432365)Peak memory usage: 88 MB
% 33.03/9.92 % (2432365)------------------------------
% 33.03/9.92 % (2432365)------------------------------
% 33.03/9.92 % (2432368)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=684490059:i=598:bs=on:bd=preordered:av=off:ss=axioms_2935 on theBenchmark for (2935ds/598Mi)
% 33.03/9.92 % (2432350)Instruction limit reached!
% 33.03/9.92 % (2432350)------------------------------
% 33.03/9.92 % (2432350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.03/9.92 % (2432350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.03/9.92 % (2432350)CaDiCaL version: 2.1.3
% 33.03/9.92 % (2432350)Termination reason: Instruction limit
% 33.03/9.92 % (2432350)Termination phase: Saturation
% 33.03/9.92 % (2432350)Time elapsed: 3.382 s
% 33.03/9.92 % (2432350)Peak memory usage: 149 MB
% 33.03/9.92 % (2432350)Instructions burned: 3257 (million)
% 33.03/9.92 % (2432370)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3297096228:i=2989:sd=3:ss=axioms:sgt=60_2932 on theBenchmark for (2932ds/2989Mi)
% 33.03/9.92 % (2432368)Instruction limit reached!
% 33.03/9.92 % (2432368)------------------------------
% 33.03/9.92 % (2432368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.03/9.92 % (2432368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.03/9.92 % (2432368)CaDiCaL version: 2.1.3
% 33.03/9.92 % (2432368)Termination reason: Instruction limit
% 33.03/9.92 % (2432368)Termination phase: Saturation
% 33.03/9.92 % (2432368)Time elapsed: 0.620 s
% 33.03/9.92 % (2432368)Peak memory usage: 94 MB
% 33.03/9.92 % (2432368)Instructions burned: 598 (million)
% 33.03/9.92 % (2432372)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=2576651769:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2926 on theBenchmark for (2926ds/1997Mi)
% 33.03/9.92 % (2432303)First to succeed.
% 33.03/9.92 % (2432303)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2432294"
% 33.03/9.92 % (2432356)Also succeeded, but the first one will report.
% 33.03/9.92 % (2432303)Refutation found. Thanks to Tanya!
% 33.03/9.92 % SZS status Unsatisfiable for theBenchmark
% 33.03/9.92 % SZS output start Proof for theBenchmark
% See solution above
% 64.24/10.19 % (2432303)------------------------------
% 64.24/10.19 % (2432303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.24/10.19 % (2432303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.24/10.19 % (2432303)CaDiCaL version: 2.1.3
% 64.24/10.19 % (2432303)Termination reason: Refutation
% 64.24/10.19 % (2432303)Time elapsed: 8.244 s
% 64.24/10.19 % (2432303)Peak memory usage: 184 MB
% 64.24/10.19 % (2432303)Instructions burned: 7873 (million)
% 64.24/10.19 % (2432303)------------------------------
% 64.24/10.19 % (2432303)------------------------------
% 64.24/10.19 % (2432294)Success in time 8.979 s
% 64.24/10.19 % Vampire exiting
%------------------------------------------------------------------------------