%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT191-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : 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:46:12 AM UTC 2026
% Result : Unsatisfiable 40.34s 11.22s
% Output : Refutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 93
% Number of leaves : 17
% Syntax : Number of formulae : 527 ( 465 unt; 5 def)
% Number of atoms : 598 ( 597 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 144 ( 73 ~; 71 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 11 ( 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 : 1223 (1223 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : meet(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_of_meet) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_meet) ).
fof(f8,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f9,axiom,
! [X0] : join(X0,complement(X0)) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement_join) ).
fof(f10,axiom,
! [X0] : meet(X0,complement(X0)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement_meet) ).
fof(f11,axiom,
! [X0,X1] :
( join(X0,X1) != one
| meet(X0,X1) != zero
| complement(X0) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f12,axiom,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X1,join(X0,meet(X1,X2))),meet(X2,join(X0,X1)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equation_H21) ).
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(f29,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,join(X0,X2))) = meet(X1,join(meet(X0,join(X1,X0)),meet(join(X0,X2),join(X1,X0)))),
inference(superposition,[],[f12,f3]) ).
fof(f34,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(meet(X0,X1),join(X0,meet(meet(X0,X1),X2))),meet(X2,X0))),
inference(superposition,[],[f12,f4]) ).
fof(f36,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,meet(X1,X2))),meet(X2,join(X0,X1))),meet(meet(X1,join(X0,meet(X1,X2))),X0)) = meet(meet(X1,join(X0,meet(X1,X2))),join(meet(meet(X2,join(X0,X1)),join(meet(X1,join(X0,meet(X1,X2))),meet(meet(X2,join(X0,X1)),X0))),join(meet(X0,X1),meet(X0,X2)))),
inference(superposition,[],[f12,f12]) ).
fof(f38,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,meet(X1,X2))),meet(X2,join(X0,X1))),meet(meet(X1,join(X0,meet(X1,X2))),X0)) = meet(X1,meet(join(X0,meet(X1,X2)),join(meet(meet(X2,join(X0,X1)),join(meet(X1,join(X0,meet(X1,X2))),meet(meet(X2,join(X0,X1)),X0))),join(meet(X0,X1),meet(X0,X2))))),
inference(forward_demodulation,[],[f36,f7]) ).
fof(f40,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(meet(X0,X1),join(X0,meet(meet(X0,X1),X2))))),
inference(forward_demodulation,[],[f34,f6]) ).
fof(f45,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,meet(X1,X2))),meet(X2,join(X0,X1))),meet(meet(X1,join(X0,meet(X1,X2))),X0)) = meet(X1,meet(join(X0,meet(X1,X2)),join(join(meet(X0,X1),meet(X0,X2)),meet(meet(X2,join(X0,X1)),join(meet(X1,join(X0,meet(X1,X2))),meet(meet(X2,join(X0,X1)),X0)))))),
inference(forward_demodulation,[],[f38,f6]) ).
fof(f47,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X0,meet(X1,join(X0,meet(meet(X0,X1),X2)))))),
inference(forward_demodulation,[],[f40,f7]) ).
fof(f51,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,meet(X1,X2))),meet(X2,join(X0,X1))),meet(meet(X1,join(X0,meet(X1,X2))),X0)) = meet(X1,meet(join(X0,meet(X1,X2)),join(meet(X0,X1),join(meet(X0,X2),meet(meet(X2,join(X0,X1)),join(meet(X1,join(X0,meet(X1,X2))),meet(meet(X2,join(X0,X1)),X0))))))),
inference(forward_demodulation,[],[f45,f8]) ).
fof(f53,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X0,meet(X1,join(X0,meet(X0,meet(X1,X2))))))),
inference(forward_demodulation,[],[f47,f7]) ).
fof(f56,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,meet(X1,X2))),meet(X2,join(X0,X1))),meet(meet(X1,join(X0,meet(X1,X2))),X0)) = meet(X1,meet(join(X0,meet(X1,X2)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(meet(X1,join(X0,meet(X1,X2))),meet(meet(X2,join(X0,X1)),X0)))))))),
inference(forward_demodulation,[],[f51,f7]) ).
fof(f58,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X0,meet(X1,X0)))),
inference(forward_demodulation,[],[f53,f4]) ).
fof(f60,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,meet(X1,X2))),meet(X2,join(X0,X1))),meet(meet(X1,join(X0,meet(X1,X2))),X0)) = meet(X1,meet(join(X0,meet(X1,X2)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(meet(X1,join(X0,meet(X1,X2))),meet(X0,meet(X2,join(X0,X1)))))))))),
inference(forward_demodulation,[],[f56,f5]) ).
fof(f62,plain,
! [X2,X0,X1] : meet(X1,meet(join(X0,meet(X1,X2)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(meet(X1,join(X0,meet(X1,X2))),meet(X0,meet(X2,join(X0,X1)))))))))) = join(meet(meet(X1,join(X0,meet(X1,X2))),X0),meet(meet(X1,join(X0,meet(X1,X2))),meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f60,f6]) ).
fof(f64,plain,
! [X2,X0,X1] : meet(X1,meet(join(X0,meet(X1,X2)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(meet(X1,join(X0,meet(X1,X2))),meet(X0,meet(X2,join(X0,X1)))))))))) = join(meet(meet(X1,join(X0,meet(X1,X2))),X0),meet(meet(X2,join(X0,X1)),meet(X1,join(X0,meet(X1,X2))))),
inference(forward_demodulation,[],[f62,f5]) ).
fof(f65,plain,
! [X2,X0,X1] : meet(X1,meet(join(X0,meet(X1,X2)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(meet(X1,join(X0,meet(X1,X2))),meet(X0,meet(X2,join(X0,X1)))))))))) = join(meet(meet(X1,join(X0,meet(X1,X2))),X0),meet(X2,meet(join(X0,X1),meet(X1,join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f64,f7]) ).
fof(f66,plain,
! [X2,X0,X1] : meet(X1,meet(join(X0,meet(X1,X2)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(meet(X1,join(X0,meet(X1,X2))),meet(X0,meet(X2,join(X0,X1)))))))))) = join(meet(X0,meet(X1,join(X0,meet(X1,X2)))),meet(X2,meet(join(X0,X1),meet(X1,join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f65,f5]) ).
fof(f76,plain,
! [X2,X0,X1] : join(meet(X2,X1),meet(X2,X0)) = meet(X2,join(meet(X1,join(X2,meet(X0,X1))),meet(X0,join(X2,X1)))),
inference(superposition,[],[f12,f5]) ).
fof(f77,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f78,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X1,join(X0,meet(X1,X2))),meet(join(X0,X1),X2))),
inference(superposition,[],[f12,f5]) ).
fof(f79,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(join(X0,X1),X2),meet(X1,join(X0,meet(X1,X2))))),
inference(forward_demodulation,[],[f78,f6]) ).
fof(f81,plain,
! [X2,X0,X1] : join(meet(X2,X1),meet(X2,X0)) = meet(X2,join(meet(X0,join(X2,X1)),meet(X1,join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f76,f6]) ).
fof(f92,plain,
! [X2,X0,X1] : join(meet(X2,X0),meet(X2,X1)) = meet(X2,join(meet(X0,join(meet(X0,X1),X2)),meet(X1,join(X2,X0)))),
inference(superposition,[],[f12,f6]) ).
fof(f94,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f95,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X1,X0)) = meet(X1,join(meet(X0,join(X1,X2)),meet(X2,join(X1,meet(X2,X0))))),
inference(superposition,[],[f12,f6]) ).
fof(f96,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,join(X0,X2))) = meet(X1,join(X0,meet(join(X0,X2),join(X1,X0)))),
inference(backward_demodulation,[],[f29,f94]) ).
fof(f98,plain,
! [X2,X0,X1] : join(meet(X2,X0),meet(X2,X1)) = meet(X2,join(meet(X1,join(X2,X0)),meet(X0,join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f92,f6]) ).
fof(f101,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f77,f3]) ).
fof(f104,plain,
a = join(a,sF3),
inference(superposition,[],[f77,f26]) ).
fof(f108,plain,
! [X2,X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,X2)) = meet(X0,join(meet(meet(X1,X0),join(X0,meet(meet(X1,X0),X2))),meet(X2,X0))),
inference(superposition,[],[f12,f77]) ).
fof(f110,plain,
! [X2,X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(meet(X1,X0),join(X0,meet(meet(X1,X0),X2))))),
inference(forward_demodulation,[],[f108,f6]) ).
fof(f113,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f101,f6]) ).
fof(f114,plain,
! [X2,X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X1,meet(X0,join(X0,meet(meet(X1,X0),X2)))))),
inference(forward_demodulation,[],[f110,f7]) ).
fof(f117,plain,
! [X2,X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X1,X0))),
inference(forward_demodulation,[],[f114,f3]) ).
fof(f124,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f8,f4]) ).
fof(f125,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f77]) ).
fof(f138,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f148,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f94,f4]) ).
fof(f149,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f94,f77]) ).
fof(f155,plain,
! [X0,X1] : join(X1,X0) = join(join(X1,X0),X0),
inference(superposition,[],[f77,f94]) ).
fof(f156,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,join(X2,X0))) = meet(X1,join(meet(X0,join(X1,X0)),meet(join(X2,X0),join(X1,X0)))),
inference(superposition,[],[f12,f94]) ).
fof(f158,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,join(X2,X0))) = meet(X1,join(X0,meet(join(X2,X0),join(X1,X0)))),
inference(forward_demodulation,[],[f156,f94]) ).
fof(f159,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f155,f6]) ).
fof(f161,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f149,f5]) ).
fof(f162,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f148,f5]) ).
fof(f164,plain,
! [X2,X0,X1] : meet(X0,join(meet(X2,X0),meet(X1,X0))) = join(meet(X1,X0),meet(X0,X2)),
inference(backward_demodulation,[],[f117,f161]) ).
fof(f166,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X1,X0))),
inference(backward_demodulation,[],[f58,f161]) ).
fof(f167,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X1,X0))),
inference(forward_demodulation,[],[f166,f162]) ).
fof(f171,plain,
! [X0,X1] :
( join(X0,X1) != one
| meet(X1,X0) != zero
| complement(X1) = X0 ),
inference(superposition,[],[f11,f6]) ).
fof(f215,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f217,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f94]) ).
fof(f219,plain,
! [X0] : meet(sF3,X0) = meet(c,meet(a,X0)),
inference(superposition,[],[f7,f26]) ).
fof(f228,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f232,plain,
! [X2,X3,X0,X1] : join(meet(X2,meet(X0,X1)),meet(X2,X3)) = meet(X2,join(meet(X0,meet(X1,join(X2,meet(meet(X0,X1),X3)))),meet(X3,join(X2,meet(X0,X1))))),
inference(superposition,[],[f12,f7]) ).
fof(f234,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,meet(X1,join(X2,meet(X0,X1)))),
inference(superposition,[],[f94,f7]) ).
fof(f238,plain,
! [X2,X3,X0,X1] : join(meet(X2,meet(X0,X1)),meet(X2,X3)) = meet(X2,join(meet(X3,join(X2,meet(X0,X1))),meet(X0,meet(X1,join(X2,meet(meet(X0,X1),X3)))))),
inference(forward_demodulation,[],[f232,f6]) ).
fof(f244,plain,
! [X2,X3,X0,X1] : join(meet(X2,meet(X0,X1)),meet(X2,X3)) = meet(X2,join(meet(X3,join(X2,meet(X0,X1))),meet(X0,meet(X1,join(X2,meet(X0,meet(X1,X3))))))),
inference(forward_demodulation,[],[f238,f7]) ).
fof(f262,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f124,f6]) ).
fof(f285,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f286,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(one,X1),
inference(superposition,[],[f8,f9]) ).
fof(f289,plain,
! [X0,X1] : join(X0,complement(meet(X0,X1))) = join(X0,one),
inference(superposition,[],[f124,f9]) ).
fof(f290,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f300,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f285]) ).
fof(f303,plain,
! [X0] : one = join(one,X0),
inference(superposition,[],[f77,f285]) ).
fof(f306,plain,
! [X0,X1] : one = join(X0,join(complement(X0),X1)),
inference(backward_demodulation,[],[f286,f303]) ).
fof(f328,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f94,f300]) ).
fof(f331,plain,
! [X0,X1] : one = join(X0,complement(meet(X0,X1))),
inference(backward_demodulation,[],[f289,f328]) ).
fof(f411,plain,
! [X0,X1] : one = join(X1,complement(meet(X0,X1))),
inference(superposition,[],[f331,f5]) ).
fof(f436,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f438,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(X1))) = meet(X0,join(meet(X1,join(X0,zero)),meet(complement(X1),join(X0,X1)))),
inference(superposition,[],[f12,f10]) ).
fof(f442,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f446,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(X1))) = meet(X0,join(meet(X1,X0),meet(complement(X1),join(X0,X1)))),
inference(backward_demodulation,[],[f438,f436]) ).
fof(f625,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f436]) ).
fof(f629,plain,
! [X0] : zero = meet(zero,X0),
inference(superposition,[],[f94,f436]) ).
fof(f663,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f77,f625]) ).
fof(f665,plain,
one = complement(zero),
inference(superposition,[],[f9,f625]) ).
fof(f695,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,zero)) = meet(X0,join(meet(X1,join(X0,zero)),meet(zero,join(X0,X1)))),
inference(superposition,[],[f12,f663]) ).
fof(f704,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,zero)) = meet(X0,join(meet(X1,join(X0,zero)),zero)),
inference(forward_demodulation,[],[f695,f629]) ).
fof(f708,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,zero)) = meet(X0,join(zero,meet(X1,join(X0,zero)))),
inference(forward_demodulation,[],[f704,f6]) ).
fof(f710,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,zero)) = meet(X0,meet(X1,join(X0,zero))),
inference(forward_demodulation,[],[f708,f625]) ).
fof(f711,plain,
! [X0,X1] : meet(X0,meet(X1,X0)) = join(meet(X0,X1),meet(X0,zero)),
inference(forward_demodulation,[],[f710,f436]) ).
fof(f712,plain,
! [X0,X1] : meet(X0,meet(X1,X0)) = join(meet(X0,X1),zero),
inference(forward_demodulation,[],[f711,f663]) ).
fof(f713,plain,
! [X0,X1] : meet(X0,meet(X1,X0)) = join(zero,meet(X0,X1)),
inference(forward_demodulation,[],[f712,f6]) ).
fof(f714,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f713,f625]) ).
fof(f725,plain,
meet(a,c) = meet(a,sF3),
inference(superposition,[],[f714,f26]) ).
fof(f730,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(meet(X1,X0),X2)),
inference(superposition,[],[f7,f714]) ).
fof(f732,plain,
! [X0,X1] : meet(X1,X0) = join(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f77,f714]) ).
fof(f741,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f730,f7]) ).
fof(f744,plain,
meet(c,a) = meet(a,sF3),
inference(forward_demodulation,[],[f725,f5]) ).
fof(f755,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f741,f7]) ).
fof(f758,plain,
sF3 = meet(a,sF3),
inference(forward_demodulation,[],[f744,f26]) ).
fof(f851,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f215,f5]) ).
fof(f868,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(join(X0,X2),X1),meet(X0,X1)),
inference(superposition,[],[f77,f215]) ).
fof(f872,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(meet(join(X0,X2),X1),meet(X0,X1)),
inference(superposition,[],[f714,f215]) ).
fof(f877,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(meet(X0,X1),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f872,f5]) ).
fof(f879,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(X0,X1),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f868,f6]) ).
fof(f893,plain,
! [X2,X0,X1] : meet(X1,meet(join(X0,meet(X1,X2)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(meet(X1,join(X0,meet(X1,X2))),meet(X0,meet(X2,join(X0,X1)))))))))) = join(meet(X0,X1),meet(X2,meet(join(X0,X1),meet(X1,join(X0,meet(X1,X2)))))),
inference(backward_demodulation,[],[f66,f851]) ).
fof(f896,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(X1,meet(meet(X0,X1),join(X0,X2))),
inference(forward_demodulation,[],[f877,f228]) ).
fof(f902,plain,
! [X2,X0,X1] : meet(X1,meet(join(X0,meet(X1,X2)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(meet(X1,join(X0,meet(X1,X2))),meet(X0,meet(X2,join(X0,X1)))))))))) = join(meet(X0,X1),meet(X2,meet(X1,meet(join(X0,meet(X1,X2)),join(X0,X1))))),
inference(forward_demodulation,[],[f893,f228]) ).
fof(f903,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(X1,meet(X0,meet(X1,join(X0,X2)))),
inference(forward_demodulation,[],[f896,f7]) ).
fof(f906,plain,
! [X2,X0,X1] : meet(X1,meet(join(X0,meet(X1,X2)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(meet(X1,join(X0,meet(X1,X2))),meet(X0,meet(X2,join(X0,X1)))))))))) = join(meet(X0,X1),meet(X2,meet(X1,meet(join(X0,X1),join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f902,f5]) ).
fof(f907,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(X1,meet(X0,join(X0,X2))),
inference(forward_demodulation,[],[f903,f755]) ).
fof(f909,plain,
! [X2,X0,X1] : meet(X1,meet(join(X0,meet(X1,X2)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(meet(X1,join(X0,meet(X1,X2))),meet(X0,meet(X2,join(X0,X1)))))))))) = join(meet(X0,X1),meet(X2,meet(X1,join(X0,meet(X1,X2))))),
inference(forward_demodulation,[],[f906,f217]) ).
fof(f910,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(meet(join(X0,X2),X1),X0),
inference(forward_demodulation,[],[f907,f3]) ).
fof(f912,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,meet(X1,join(X0,meet(X1,X2))))) = meet(X1,meet(join(X0,meet(X1,X2)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(meet(X1,join(X0,meet(X1,X2))),meet(X0,X2)))))))),
inference(forward_demodulation,[],[f909,f851]) ).
fof(f913,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X0,meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f910,f5]) ).
fof(f914,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,meet(X1,join(X0,meet(X1,X2))))) = meet(X1,meet(join(X0,meet(X1,X2)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(meet(X0,X2),meet(X1,join(X0,meet(X1,X2)))))))))),
inference(forward_demodulation,[],[f912,f6]) ).
fof(f950,plain,
! [X0,X1] : one = join(join(X0,X1),complement(X0)),
inference(superposition,[],[f411,f3]) ).
fof(f985,plain,
! [X0,X1] : one = join(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f950,f6]) ).
fof(f993,plain,
! [X0,X1] : one = join(X0,join(X1,complement(X0))),
inference(forward_demodulation,[],[f985,f138]) ).
fof(f1064,plain,
! [X0,X1] : zero = meet(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f442,f5]) ).
fof(f1153,plain,
! [X0,X1] : one = join(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f290,f6]) ).
fof(f1177,plain,
! [X0,X1] :
( one != one
| zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(superposition,[],[f11,f290]) ).
fof(f1185,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f1177]) ).
fof(f1218,plain,
! [X2,X0,X1] : join(meet(X1,X0),X2) = join(meet(X1,X0),join(meet(X0,X1),X2)),
inference(superposition,[],[f125,f714]) ).
fof(f1235,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f125,f6]) ).
fof(f1308,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(meet(X0,X1),join(X0,meet(meet(X0,X1),X2))))),
inference(superposition,[],[f95,f4]) ).
fof(f1324,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,meet(X1,X2))),meet(X2,join(X0,X1))),meet(meet(X1,join(X0,meet(X1,X2))),X0)) = meet(meet(X1,join(X0,meet(X1,X2))),join(join(meet(X0,X1),meet(X0,X2)),meet(meet(X2,join(X0,X1)),join(meet(X1,join(X0,meet(X1,X2))),meet(meet(X2,join(X0,X1)),X0))))),
inference(superposition,[],[f95,f12]) ).
fof(f1343,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,join(X0,X2))) = meet(X1,join(meet(join(X0,X2),join(X1,X0)),meet(X0,join(X1,X0)))),
inference(superposition,[],[f95,f3]) ).
fof(f1432,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,join(X0,X2))) = meet(X1,join(meet(X0,join(X1,X0)),meet(join(X0,X2),join(X1,X0)))),
inference(forward_demodulation,[],[f1343,f6]) ).
fof(f1446,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,meet(X1,X2))),meet(X2,join(X0,X1))),meet(meet(X1,join(X0,meet(X1,X2))),X0)) = meet(X1,meet(join(X0,meet(X1,X2)),join(join(meet(X0,X1),meet(X0,X2)),meet(meet(X2,join(X0,X1)),join(meet(X1,join(X0,meet(X1,X2))),meet(meet(X2,join(X0,X1)),X0)))))),
inference(forward_demodulation,[],[f1324,f7]) ).
fof(f1458,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X0,meet(X1,join(X0,meet(meet(X0,X1),X2)))))),
inference(forward_demodulation,[],[f1308,f7]) ).
fof(f1491,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,join(X0,X2))) = meet(X1,meet(join(X0,X2),join(X1,X0))),
inference(forward_demodulation,[],[f1432,f879]) ).
fof(f1503,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,meet(X1,X2))),meet(X2,join(X0,X1))),meet(meet(X1,join(X0,meet(X1,X2))),X0)) = meet(X1,meet(join(X0,meet(X1,X2)),join(meet(X0,X1),join(meet(X0,X2),meet(meet(X2,join(X0,X1)),join(meet(X1,join(X0,meet(X1,X2))),meet(meet(X2,join(X0,X1)),X0))))))),
inference(forward_demodulation,[],[f1446,f8]) ).
fof(f1510,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X0,X1))),
inference(forward_demodulation,[],[f1458,f851]) ).
fof(f1531,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = join(meet(X1,X0),meet(X1,join(X0,X2))),
inference(forward_demodulation,[],[f1491,f851]) ).
fof(f1541,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,meet(X1,X2))),meet(X2,join(X0,X1))),meet(meet(X1,join(X0,meet(X1,X2))),X0)) = meet(X1,meet(join(X0,meet(X1,X2)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(meet(X1,join(X0,meet(X1,X2))),meet(meet(X2,join(X0,X1)),X0)))))))),
inference(forward_demodulation,[],[f1503,f7]) ).
fof(f1548,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X0,X1))),
inference(forward_demodulation,[],[f1510,f162]) ).
fof(f1566,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = meet(X1,join(X0,meet(join(X0,X2),join(X1,X0)))),
inference(backward_demodulation,[],[f96,f1531]) ).
fof(f1573,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,meet(X1,X2))),meet(X2,join(X0,X1))),meet(meet(X1,join(X0,meet(X1,X2))),X0)) = meet(X1,meet(join(X0,meet(X1,X2)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(meet(X1,join(X0,meet(X1,X2))),meet(X0,meet(X2,join(X0,X1)))))))))),
inference(forward_demodulation,[],[f1541,f5]) ).
fof(f1596,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,meet(X1,X2))),meet(X2,join(X0,X1))),meet(meet(X1,join(X0,meet(X1,X2))),X0)) = meet(X1,meet(join(X0,meet(X1,X2)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(meet(X1,join(X0,meet(X1,X2))),meet(X0,X2)))))))),
inference(forward_demodulation,[],[f1573,f851]) ).
fof(f1615,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,meet(X1,X2))),meet(X2,join(X0,X1))),meet(meet(X1,join(X0,meet(X1,X2))),X0)) = meet(X1,meet(join(X0,meet(X1,X2)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(meet(X0,X2),meet(X1,join(X0,meet(X1,X2)))))))))),
inference(forward_demodulation,[],[f1596,f6]) ).
fof(f1626,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,meet(X1,X2))),meet(X2,join(X0,X1))),meet(meet(X1,join(X0,meet(X1,X2))),X0)) = join(meet(X0,X1),meet(X2,meet(X1,join(X0,meet(X1,X2))))),
inference(forward_demodulation,[],[f1615,f914]) ).
fof(f1636,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,meet(X1,X2))),X0),meet(meet(X1,join(X0,meet(X1,X2))),meet(X2,join(X0,X1)))) = join(meet(X0,X1),meet(X2,meet(X1,join(X0,meet(X1,X2))))),
inference(forward_demodulation,[],[f1626,f6]) ).
fof(f1645,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,meet(X1,X2))),X0),meet(meet(X2,join(X0,X1)),meet(X1,join(X0,meet(X1,X2))))) = join(meet(X0,X1),meet(X2,meet(X1,join(X0,meet(X1,X2))))),
inference(forward_demodulation,[],[f1636,f5]) ).
fof(f1653,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,meet(X1,join(X0,meet(X1,X2))))) = join(meet(meet(X1,join(X0,meet(X1,X2))),X0),meet(join(X0,meet(X1,X2)),meet(meet(X2,join(X0,X1)),X1))),
inference(forward_demodulation,[],[f1645,f228]) ).
fof(f1660,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,meet(X1,join(X0,meet(X1,X2))))) = join(meet(meet(X1,join(X0,meet(X1,X2))),X0),meet(X1,meet(join(X0,meet(X1,X2)),meet(X2,join(X0,X1))))),
inference(forward_demodulation,[],[f1653,f228]) ).
fof(f1667,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,meet(X1,join(X0,meet(X1,X2))))) = join(meet(meet(X1,join(X0,meet(X1,X2))),X0),meet(X1,meet(join(X0,X1),meet(join(X0,meet(X1,X2)),X2)))),
inference(forward_demodulation,[],[f1660,f228]) ).
fof(f1673,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,meet(X1,join(X0,meet(X1,X2))))) = join(meet(meet(X1,join(X0,meet(X1,X2))),X0),meet(X1,meet(join(X0,meet(X1,X2)),X2))),
inference(forward_demodulation,[],[f1667,f217]) ).
fof(f1677,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,meet(X1,join(X0,meet(X1,X2))))) = join(meet(meet(X1,join(X0,meet(X1,X2))),X0),meet(X1,meet(X2,join(X0,meet(X1,X2))))),
inference(forward_demodulation,[],[f1673,f5]) ).
fof(f1681,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,meet(X1,join(X0,meet(X1,X2))))) = join(meet(meet(X1,join(X0,meet(X1,X2))),X0),meet(X1,X2)),
inference(forward_demodulation,[],[f1677,f234]) ).
fof(f1685,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,meet(X1,join(X0,meet(X1,X2))))) = join(meet(X1,X2),meet(meet(X1,join(X0,meet(X1,X2))),X0)),
inference(forward_demodulation,[],[f1681,f6]) ).
fof(f1687,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,meet(X1,join(X0,meet(X1,X2))))) = join(meet(X1,X2),meet(X0,meet(X1,join(X0,meet(X1,X2))))),
inference(forward_demodulation,[],[f1685,f5]) ).
fof(f1688,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,meet(X1,join(X0,meet(X1,X2))))) = join(meet(X1,X2),meet(X0,X1)),
inference(forward_demodulation,[],[f1687,f851]) ).
fof(f2266,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(meet(X0,X1),meet(X0,X2)),
inference(superposition,[],[f217,f4]) ).
fof(f2282,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,X2))),
inference(superposition,[],[f217,f5]) ).
fof(f2361,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f2266,f228]) ).
fof(f2379,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X2,X1)),
inference(forward_demodulation,[],[f2361,f755]) ).
fof(f2741,plain,
! [X0,X1] : join(meet(complement(meet(X0,X1)),X0),meet(complement(meet(X0,X1)),X1)) = meet(complement(meet(X0,X1)),join(meet(X1,join(complement(meet(X0,X1)),X0)),meet(X0,one))),
inference(superposition,[],[f98,f9]) ).
fof(f2821,plain,
! [X0,X1] : join(meet(complement(meet(X0,X1)),X0),meet(complement(meet(X0,X1)),X1)) = meet(complement(meet(X0,X1)),join(meet(X0,one),meet(X1,join(complement(meet(X0,X1)),X0)))),
inference(forward_demodulation,[],[f2741,f6]) ).
fof(f2911,plain,
! [X0,X1] : join(meet(complement(meet(X0,X1)),X0),meet(complement(meet(X0,X1)),X1)) = meet(complement(meet(X0,X1)),join(meet(X0,one),meet(X1,join(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f2821,f6]) ).
fof(f2982,plain,
! [X0,X1] : join(meet(complement(meet(X0,X1)),X0),meet(complement(meet(X0,X1)),X1)) = meet(complement(meet(X0,X1)),join(meet(X0,one),meet(X1,one))),
inference(forward_demodulation,[],[f2911,f331]) ).
fof(f3036,plain,
! [X0,X1] : join(meet(complement(meet(X0,X1)),X0),meet(complement(meet(X0,X1)),X1)) = meet(complement(meet(X0,X1)),join(meet(X0,one),X1)),
inference(forward_demodulation,[],[f2982,f285]) ).
fof(f3078,plain,
! [X0,X1] : join(meet(complement(meet(X0,X1)),X0),meet(complement(meet(X0,X1)),X1)) = meet(complement(meet(X0,X1)),join(X0,X1)),
inference(forward_demodulation,[],[f3036,f285]) ).
fof(f3114,plain,
! [X0,X1] : join(meet(complement(meet(X0,X1)),X0),meet(complement(meet(X0,X1)),X1)) = meet(join(X0,X1),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f3078,f5]) ).
fof(f3144,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(X0,X1))) = join(meet(complement(meet(X0,X1)),X0),meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f3114,f5]) ).
fof(f3170,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(X0,X1))) = join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f3144,f5]) ).
fof(f3339,plain,
! [X0,X1] : join(X0,meet(X1,complement(meet(X0,X1)))) = join(X0,meet(join(X0,X1),complement(meet(X0,X1)))),
inference(superposition,[],[f124,f3170]) ).
fof(f3345,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(X0,X1))) = join(meet(X1,complement(meet(X0,X1))),meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f6,f3170]) ).
fof(f3347,plain,
! [X0,X1] :
( one != meet(join(X0,X1),complement(meet(X0,X1)))
| zero != meet(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1))))
| meet(X1,complement(meet(X0,X1))) = complement(meet(X0,complement(meet(X0,X1)))) ),
inference(superposition,[],[f11,f3170]) ).
fof(f3371,plain,
! [X0,X1] :
( zero != meet(complement(meet(X0,X1)),meet(meet(X0,complement(meet(X0,X1))),X1))
| one != meet(join(X0,X1),complement(meet(X0,X1)))
| meet(X1,complement(meet(X0,X1))) = complement(meet(X0,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f3347,f228]) ).
fof(f3421,plain,
! [X0,X1] :
( zero != meet(X1,meet(complement(meet(X0,X1)),meet(X0,complement(meet(X0,X1)))))
| one != meet(join(X0,X1),complement(meet(X0,X1)))
| meet(X1,complement(meet(X0,X1))) = complement(meet(X0,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f3371,f228]) ).
fof(f3464,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,complement(meet(X0,X1))))
| one != meet(join(X0,X1),complement(meet(X0,X1)))
| meet(X1,complement(meet(X0,X1))) = complement(meet(X0,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f3421,f161]) ).
fof(f3504,plain,
! [X0,X1] :
( meet(X1,complement(meet(X0,X1))) = complement(meet(X0,complement(meet(X0,X1))))
| one != meet(join(X0,X1),complement(meet(X0,X1))) ),
inference(forward_subsumption_resolution,[],[f3464,f1064]) ).
fof(f3615,plain,
! [X0,X1] : join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))) = join(X0,meet(one,complement(meet(X0,complement(meet(X0,X1)))))),
inference(superposition,[],[f3339,f331]) ).
fof(f3732,plain,
! [X0,X1] : join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))) = join(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f3615,f300]) ).
fof(f3783,plain,
! [X0,X1] : one = join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f3732,f331]) ).
fof(f4313,plain,
! [X0,X1] : join(meet(X0,join(X1,complement(join(X1,X0)))),meet(X0,complement(join(X1,complement(join(X1,X0)))))) = meet(X0,join(meet(join(X1,complement(join(X1,X0))),X0),meet(complement(join(X1,complement(join(X1,X0)))),one))),
inference(superposition,[],[f446,f1153]) ).
fof(f4334,plain,
! [X0,X1] : join(meet(X0,join(X1,complement(join(X1,X0)))),meet(X0,complement(join(X1,complement(join(X1,X0)))))) = meet(X0,join(meet(join(X1,complement(join(X1,X0))),X0),meet(one,complement(join(X1,complement(join(X1,X0))))))),
inference(forward_demodulation,[],[f4313,f5]) ).
fof(f4372,plain,
! [X0,X1] : join(meet(X0,join(X1,complement(join(X1,X0)))),meet(X0,complement(join(X1,complement(join(X1,X0)))))) = meet(X0,join(meet(join(X1,complement(join(X1,X0))),X0),complement(join(X1,complement(join(X1,X0)))))),
inference(forward_demodulation,[],[f4334,f300]) ).
fof(f4398,plain,
! [X0,X1] : join(meet(X0,join(X1,complement(join(X1,X0)))),meet(X0,complement(join(X1,complement(join(X1,X0)))))) = meet(X0,join(complement(join(X1,complement(join(X1,X0)))),meet(join(X1,complement(join(X1,X0))),X0))),
inference(forward_demodulation,[],[f4372,f6]) ).
fof(f4412,plain,
! [X0,X1] : join(meet(X0,join(X1,complement(join(X1,X0)))),meet(X0,complement(join(X1,complement(join(X1,X0)))))) = meet(X0,join(complement(join(X1,complement(join(X1,X0)))),meet(X0,join(X1,complement(join(X1,X0)))))),
inference(forward_demodulation,[],[f4398,f5]) ).
fof(f4872,plain,
! [X2,X0,X1] : join(X1,meet(meet(X2,X0),complement(meet(X0,meet(X1,X2))))) = join(X1,meet(join(X1,meet(X2,X0)),complement(meet(X0,meet(X1,X2))))),
inference(superposition,[],[f3339,f228]) ).
fof(f4905,plain,
! [X2,X3,X0,X1] : meet(X2,meet(X0,X1)) = meet(X2,meet(X0,meet(X1,join(X2,X3)))),
inference(superposition,[],[f215,f228]) ).
fof(f4929,plain,
! [X2,X0,X1] : join(X1,meet(join(X1,meet(X2,X0)),complement(meet(X0,meet(X1,X2))))) = join(X1,meet(X2,meet(X0,complement(meet(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f4872,f7]) ).
fof(f5744,plain,
! [X2,X0,X1] : join(meet(X0,join(X1,complement(join(X1,X0)))),meet(X0,X2)) = meet(X0,join(meet(X2,one),meet(join(X1,complement(join(X1,X0))),join(X0,meet(X2,join(X1,complement(join(X1,X0)))))))),
inference(superposition,[],[f81,f1153]) ).
fof(f5756,plain,
! [X0] : join(meet(a,sF3),meet(a,X0)) = meet(a,join(meet(X0,a),meet(sF3,join(a,meet(X0,sF3))))),
inference(superposition,[],[f81,f104]) ).
fof(f5801,plain,
! [X0,X1] : join(meet(X0,complement(X1)),meet(X0,X1)) = meet(X0,join(meet(X1,join(X0,complement(X1))),meet(complement(X1),join(X0,zero)))),
inference(superposition,[],[f81,f10]) ).
fof(f5921,plain,
! [X0,X1] : join(meet(X0,complement(X1)),meet(X0,X1)) = meet(X0,join(meet(X1,join(X0,complement(X1))),meet(complement(X1),X0))),
inference(forward_demodulation,[],[f5801,f436]) ).
fof(f5959,plain,
! [X0] : join(sF3,meet(a,X0)) = meet(a,join(meet(X0,a),meet(sF3,join(a,meet(X0,sF3))))),
inference(forward_demodulation,[],[f5756,f758]) ).
fof(f5971,plain,
! [X2,X0,X1] : join(meet(X0,join(X1,complement(join(X1,X0)))),meet(X0,X2)) = meet(X0,join(X2,meet(join(X1,complement(join(X1,X0))),join(X0,meet(X2,join(X1,complement(join(X1,X0)))))))),
inference(forward_demodulation,[],[f5744,f285]) ).
fof(f6023,plain,
! [X0,X1] : join(meet(X0,complement(X1)),meet(X0,X1)) = meet(X0,join(meet(complement(X1),X0),meet(X1,join(X0,complement(X1))))),
inference(forward_demodulation,[],[f5921,f6]) ).
fof(f6090,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(X1))) = meet(X0,join(meet(complement(X1),X0),meet(X1,join(X0,complement(X1))))),
inference(forward_demodulation,[],[f6023,f6]) ).
fof(f6385,plain,
! [X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,complement(meet(X1,X0)))) = meet(X0,join(meet(complement(meet(X1,X0)),X0),meet(meet(X1,X0),one))),
inference(superposition,[],[f6090,f411]) ).
fof(f6476,plain,
! [X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,complement(meet(X1,X0)))) = meet(X0,join(meet(meet(X1,X0),one),meet(complement(meet(X1,X0)),X0))),
inference(forward_demodulation,[],[f6385,f6]) ).
fof(f6534,plain,
! [X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,complement(meet(X1,X0)))) = meet(X0,join(meet(meet(X1,X0),one),meet(X0,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f6476,f5]) ).
fof(f6585,plain,
! [X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,complement(meet(X1,X0)))) = meet(X0,join(meet(one,meet(X1,X0)),meet(X0,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f6534,f5]) ).
fof(f6631,plain,
! [X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,complement(meet(X1,X0)))) = meet(X0,join(meet(X1,X0),meet(X0,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f6585,f300]) ).
fof(f6671,plain,
! [X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,complement(meet(X1,X0)))) = join(meet(X0,complement(meet(X1,X0))),meet(X0,X1)),
inference(forward_demodulation,[],[f6631,f1548]) ).
fof(f6707,plain,
! [X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,complement(meet(X1,X0)))) = join(meet(X0,X1),meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f6671,f6]) ).
fof(f6734,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,[],[f6707,f161]) ).
fof(f7284,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X1)) = join(meet(X1,X0),meet(X2,meet(X0,X1))),
inference(superposition,[],[f1218,f77]) ).
fof(f7305,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X1,X0),join(X2,meet(X0,X1))),
inference(superposition,[],[f138,f1218]) ).
fof(f7363,plain,
! [X2,X0,X1] : meet(X1,X0) = join(meet(X1,X0),meet(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f7284,f732]) ).
fof(f7913,plain,
! [X0] : meet(c,a) = meet(sF3,join(a,X0)),
inference(superposition,[],[f219,f3]) ).
fof(f8004,plain,
! [X0] : sF3 = meet(sF3,join(a,X0)),
inference(forward_demodulation,[],[f7913,f26]) ).
fof(f8041,plain,
! [X0] : join(sF3,meet(a,X0)) = meet(a,join(meet(X0,a),sF3)),
inference(backward_demodulation,[],[f5959,f8004]) ).
fof(f8059,plain,
! [X0] : join(sF3,meet(a,X0)) = meet(a,join(sF3,meet(X0,a))),
inference(forward_demodulation,[],[f8041,f6]) ).
fof(f8342,plain,
! [X2,X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,X2)) = meet(X0,join(meet(X0,X2),meet(meet(X1,X0),join(X0,meet(meet(X1,X0),X2))))),
inference(superposition,[],[f79,f77]) ).
fof(f8652,plain,
! [X2,X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,X2)) = meet(X0,join(meet(X0,X2),meet(X1,meet(X0,join(X0,meet(meet(X1,X0),X2)))))),
inference(forward_demodulation,[],[f8342,f7]) ).
fof(f8762,plain,
! [X2,X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,X2)) = meet(X0,join(meet(X0,X2),meet(X1,X0))),
inference(forward_demodulation,[],[f8652,f3]) ).
fof(f8844,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = meet(X0,join(meet(X0,X2),meet(X1,X0))),
inference(forward_demodulation,[],[f8762,f161]) ).
fof(f9371,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X1,meet(X0,join(X2,meet(X0,X1))))) = join(meet(X0,X2),join(meet(X0,X1),meet(X2,X0))),
inference(superposition,[],[f1218,f1688]) ).
fof(f9372,plain,
! [X2,X0,X1] : join(meet(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X2),meet(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X0)) = meet(meet(X1,meet(X0,join(X2,meet(X0,X1)))),join(meet(X0,join(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X2)),meet(X2,join(meet(X0,X1),meet(X2,X0))))),
inference(superposition,[],[f98,f1688]) ).
fof(f9374,plain,
! [X2,X0,X1] : join(X2,meet(X1,meet(X0,join(X2,meet(X0,X1))))) = join(X2,join(meet(X0,X1),meet(X2,X0))),
inference(superposition,[],[f124,f1688]) ).
fof(f9431,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(X1,meet(X0,join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f9374,f262]) ).
fof(f9433,plain,
! [X2,X0,X1] : join(meet(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X2),meet(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X0)) = meet(X1,meet(meet(X0,join(X2,meet(X0,X1))),join(meet(X0,join(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X2)),meet(X2,join(meet(X0,X1),meet(X2,X0)))))),
inference(forward_demodulation,[],[f9372,f7]) ).
fof(f9434,plain,
! [X2,X0,X1] : join(meet(X2,X0),meet(X0,X1)) = join(meet(X0,X2),meet(X1,meet(X0,join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f9371,f7305]) ).
fof(f9571,plain,
! [X2,X0,X1] : join(meet(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X2),meet(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X0)) = meet(X1,meet(X0,meet(join(X2,meet(X0,X1)),join(meet(X0,join(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X2)),meet(X2,join(meet(X0,X1),meet(X2,X0))))))),
inference(forward_demodulation,[],[f9433,f7]) ).
fof(f9688,plain,
! [X2,X0,X1] : join(meet(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X2),meet(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X0)) = meet(X1,meet(X0,meet(join(X2,meet(X0,X1)),join(meet(X2,join(meet(X0,X1),meet(X2,X0))),meet(X0,join(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X2)))))),
inference(forward_demodulation,[],[f9571,f6]) ).
fof(f9777,plain,
! [X2,X0,X1] : join(meet(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X2),meet(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X0)) = meet(X1,meet(X0,meet(join(X2,meet(X0,X1)),join(meet(X2,join(meet(X0,X1),meet(X2,X0))),meet(X0,join(X2,meet(X1,meet(X0,join(X2,meet(X0,X1)))))))))),
inference(forward_demodulation,[],[f9688,f6]) ).
fof(f9823,plain,
! [X2,X0,X1] : join(meet(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X2),meet(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X0)) = meet(X1,meet(X0,meet(join(X2,meet(X0,X1)),join(meet(X2,join(meet(X0,X1),meet(X2,X0))),meet(X0,join(X2,meet(X0,X1))))))),
inference(forward_demodulation,[],[f9777,f9431]) ).
fof(f9860,plain,
! [X2,X0,X1] : meet(X1,meet(X0,join(X2,meet(X0,X1)))) = join(meet(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X2),meet(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X0)),
inference(forward_demodulation,[],[f9823,f234]) ).
fof(f9887,plain,
! [X2,X0,X1] : meet(X1,meet(X0,join(X2,meet(X0,X1)))) = join(meet(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X2),meet(X0,meet(X1,meet(X0,join(X2,meet(X0,X1)))))),
inference(forward_demodulation,[],[f9860,f5]) ).
fof(f9910,plain,
! [X2,X0,X1] : meet(X1,meet(X0,join(X2,meet(X0,X1)))) = join(meet(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X2),meet(X0,meet(X1,join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f9887,f755]) ).
fof(f9930,plain,
! [X2,X0,X1] : meet(X1,meet(X0,join(X2,meet(X0,X1)))) = join(meet(X0,meet(X1,join(X2,meet(X0,X1)))),meet(meet(X1,meet(X0,join(X2,meet(X0,X1)))),X2)),
inference(forward_demodulation,[],[f9910,f6]) ).
fof(f9949,plain,
! [X2,X0,X1] : meet(X1,meet(X0,join(X2,meet(X0,X1)))) = join(meet(X0,meet(X1,join(X2,meet(X0,X1)))),meet(X2,meet(X1,meet(X0,join(X2,meet(X0,X1)))))),
inference(forward_demodulation,[],[f9930,f5]) ).
fof(f9962,plain,
! [X2,X0,X1] : meet(X1,meet(X0,join(X2,meet(X0,X1)))) = join(meet(X0,meet(X1,join(X2,meet(X0,X1)))),meet(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f9949,f4905]) ).
fof(f9969,plain,
! [X2,X0,X1] : meet(X1,meet(X0,join(X2,meet(X0,X1)))) = join(meet(X2,meet(X1,X0)),meet(X0,meet(X1,join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f9962,f6]) ).
fof(f9974,plain,
! [X2,X0,X1] : meet(X1,meet(X0,join(X2,meet(X0,X1)))) = join(meet(X2,meet(X1,X0)),meet(X0,X1)),
inference(forward_demodulation,[],[f9969,f234]) ).
fof(f9977,plain,
! [X2,X0,X1] : meet(X1,meet(X0,join(X2,meet(X0,X1)))) = join(meet(X0,X1),meet(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f9974,f6]) ).
fof(f9979,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X1,meet(X0,join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f9977,f7363]) ).
fof(f9987,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = join(meet(X2,X0),meet(X0,X1)),
inference(backward_demodulation,[],[f9434,f9979]) ).
fof(f10580,plain,
! [X2,X0,X1] : join(X1,meet(meet(join(X1,X2),X0),complement(meet(X0,X1)))) = join(X1,meet(join(X1,meet(join(X1,X2),X0)),complement(meet(X0,X1)))),
inference(superposition,[],[f3339,f913]) ).
fof(f10602,plain,
! [X2,X0,X1] : join(X1,meet(meet(join(X1,X2),X0),complement(meet(X0,X1)))) = join(X1,meet(complement(meet(X0,X1)),join(X1,meet(join(X1,X2),X0)))),
inference(forward_demodulation,[],[f10580,f5]) ).
fof(f10671,plain,
! [X2,X0,X1] : join(X1,meet(complement(meet(X0,X1)),join(X1,meet(join(X1,X2),X0)))) = join(X1,meet(complement(meet(X0,X1)),meet(join(X1,X2),X0))),
inference(forward_demodulation,[],[f10602,f5]) ).
fof(f10717,plain,
! [X2,X0,X1] : join(X1,meet(complement(meet(X0,X1)),join(X1,meet(join(X1,X2),X0)))) = join(X1,meet(X0,meet(complement(meet(X0,X1)),join(X1,X2)))),
inference(forward_demodulation,[],[f10671,f228]) ).
fof(f10804,plain,
! [X0,X1] : join(X1,meet(X0,complement(meet(X0,X1)))) = join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),
inference(superposition,[],[f262,f3170]) ).
fof(f11232,plain,
! [X2,X0,X1] : join(meet(X0,join(complement(X0),X1)),meet(X0,X2)) = meet(X0,join(meet(X2,one),meet(join(complement(X0),X1),join(X0,meet(join(complement(X0),X1),X2))))),
inference(superposition,[],[f95,f306]) ).
fof(f11280,plain,
! [X2,X0,X1] : join(meet(X0,join(complement(X0),X1)),meet(X0,X2)) = meet(X0,join(X2,meet(join(complement(X0),X1),join(X0,meet(join(complement(X0),X1),X2))))),
inference(forward_demodulation,[],[f11232,f285]) ).
fof(f11375,plain,
! [X0,X1] :
( meet(meet(X0,complement(meet(X1,X0))),complement(zero)) = complement(meet(X1,complement(zero)))
| one != meet(join(X1,meet(X0,complement(meet(X1,X0)))),complement(zero)) ),
inference(superposition,[],[f3504,f442]) ).
fof(f11376,plain,
! [X0,X1] :
( meet(meet(X0,complement(meet(X0,X1))),complement(zero)) = complement(meet(X1,complement(zero)))
| one != meet(join(X1,meet(X0,complement(meet(X0,X1)))),complement(zero)) ),
inference(superposition,[],[f3504,f1064]) ).
fof(f11553,plain,
! [X0,X1] :
( complement(meet(X1,one)) = meet(meet(X0,complement(meet(X0,X1))),one)
| one != meet(join(X1,meet(X0,complement(meet(X0,X1)))),complement(zero)) ),
inference(forward_demodulation,[],[f11376,f665]) ).
fof(f11554,plain,
! [X0,X1] :
( complement(meet(X1,one)) = meet(meet(X0,complement(meet(X1,X0))),one)
| one != meet(join(X1,meet(X0,complement(meet(X1,X0)))),complement(zero)) ),
inference(forward_demodulation,[],[f11375,f665]) ).
fof(f11650,plain,
! [X0,X1] :
( meet(one,meet(X0,complement(meet(X0,X1)))) = complement(meet(X1,one))
| one != meet(join(X1,meet(X0,complement(meet(X0,X1)))),complement(zero)) ),
inference(forward_demodulation,[],[f11553,f5]) ).
fof(f11651,plain,
! [X0,X1] :
( meet(one,meet(X0,complement(meet(X1,X0)))) = complement(meet(X1,one))
| one != meet(join(X1,meet(X0,complement(meet(X1,X0)))),complement(zero)) ),
inference(forward_demodulation,[],[f11554,f5]) ).
fof(f11691,plain,
! [X0,X1] :
( complement(X1) = meet(one,meet(X0,complement(meet(X0,X1))))
| one != meet(join(X1,meet(X0,complement(meet(X0,X1)))),complement(zero)) ),
inference(forward_demodulation,[],[f11650,f285]) ).
fof(f11692,plain,
! [X0,X1] :
( complement(X1) = meet(one,meet(X0,complement(meet(X1,X0))))
| one != meet(join(X1,meet(X0,complement(meet(X1,X0)))),complement(zero)) ),
inference(forward_demodulation,[],[f11651,f285]) ).
fof(f11742,plain,
! [X0,X1] :
( complement(X1) = meet(X0,complement(meet(X0,X1)))
| one != meet(join(X1,meet(X0,complement(meet(X0,X1)))),complement(zero)) ),
inference(forward_demodulation,[],[f11691,f300]) ).
fof(f11743,plain,
! [X0,X1] :
( complement(X1) = meet(X0,complement(meet(X1,X0)))
| one != meet(join(X1,meet(X0,complement(meet(X1,X0)))),complement(zero)) ),
inference(forward_demodulation,[],[f11692,f300]) ).
fof(f11764,plain,
! [X0,X1] :
( one != meet(complement(zero),join(X1,meet(X0,complement(meet(X0,X1)))))
| complement(X1) = meet(X0,complement(meet(X0,X1))) ),
inference(forward_demodulation,[],[f11742,f5]) ).
fof(f11765,plain,
! [X0,X1] :
( one != meet(complement(zero),join(X1,meet(X0,complement(meet(X1,X0)))))
| complement(X1) = meet(X0,complement(meet(X1,X0))) ),
inference(forward_demodulation,[],[f11743,f5]) ).
fof(f11780,plain,
! [X0,X1] :
( one != meet(one,join(X1,meet(X0,complement(meet(X0,X1)))))
| complement(X1) = meet(X0,complement(meet(X0,X1))) ),
inference(forward_demodulation,[],[f11764,f665]) ).
fof(f11781,plain,
! [X0,X1] :
( one != meet(one,join(X1,meet(X0,complement(meet(X1,X0)))))
| complement(X1) = meet(X0,complement(meet(X1,X0))) ),
inference(forward_demodulation,[],[f11765,f665]) ).
fof(f11792,plain,
! [X0,X1] :
( one != join(X1,meet(X0,complement(meet(X0,X1))))
| complement(X1) = meet(X0,complement(meet(X0,X1))) ),
inference(forward_demodulation,[],[f11780,f300]) ).
fof(f11793,plain,
! [X0,X1] :
( one != join(X1,meet(X0,complement(meet(X1,X0))))
| complement(X1) = meet(X0,complement(meet(X1,X0))) ),
inference(forward_demodulation,[],[f11781,f300]) ).
fof(f12430,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X2,join(X0,meet(X0,X1))),meet(X0,X1))),
inference(superposition,[],[f244,f851]) ).
fof(f12557,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X0,X1),meet(X2,join(X0,meet(X0,X1))))),
inference(forward_demodulation,[],[f12430,f6]) ).
fof(f12747,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X0,X1),meet(X2,X0))),
inference(forward_demodulation,[],[f12557,f4]) ).
fof(f12890,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = join(meet(X2,X0),meet(X0,X1)),
inference(forward_demodulation,[],[f12747,f8844]) ).
fof(f12991,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X2,X0),meet(X0,X1)),
inference(forward_demodulation,[],[f12890,f162]) ).
fof(f15251,plain,
! [X2,X0,X1] : join(X0,meet(meet(X1,join(X2,X0)),complement(meet(X0,X1)))) = join(X0,meet(join(X0,meet(X1,join(X2,X0))),complement(meet(X0,X1)))),
inference(superposition,[],[f3339,f2282]) ).
fof(f15286,plain,
! [X2,X0,X1] : join(X0,meet(meet(X1,join(X2,X0)),complement(meet(X0,X1)))) = join(X0,meet(complement(meet(X0,X1)),join(X0,meet(X1,join(X2,X0))))),
inference(forward_demodulation,[],[f15251,f5]) ).
fof(f15370,plain,
! [X2,X0,X1] : join(X0,meet(complement(meet(X0,X1)),meet(X1,join(X2,X0)))) = join(X0,meet(complement(meet(X0,X1)),join(X0,meet(X1,join(X2,X0))))),
inference(forward_demodulation,[],[f15286,f5]) ).
fof(f15417,plain,
! [X2,X0,X1] : join(X0,meet(complement(meet(X0,X1)),join(X0,meet(X1,join(X2,X0))))) = join(X0,meet(X1,meet(join(X2,X0),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f15370,f228]) ).
fof(f15488,plain,
! [X2,X3,X0,X1] : join(meet(X3,meet(join(X2,X0),X1)),meet(meet(join(X2,X0),X1),X0)) = meet(meet(join(X2,X0),X1),join(meet(X0,X1),meet(X3,meet(join(X2,X0),X1)))),
inference(superposition,[],[f164,f217]) ).
fof(f15516,plain,
! [X0] : meet(a,join(sF3,meet(X0,a))) = join(meet(X0,a),meet(a,c)),
inference(superposition,[],[f164,f26]) ).
fof(f15532,plain,
! [X2,X3,X0,X1] : join(meet(X0,meet(X1,X2)),meet(X2,X3)) = meet(X2,join(meet(X3,X2),meet(X0,meet(X1,X2)))),
inference(superposition,[],[f164,f7]) ).
fof(f15776,plain,
! [X0] : meet(a,join(sF3,meet(X0,a))) = join(meet(X0,a),meet(c,a)),
inference(forward_demodulation,[],[f15516,f5]) ).
fof(f15804,plain,
! [X2,X3,X0,X1] : join(meet(X3,meet(join(X2,X0),X1)),meet(meet(join(X2,X0),X1),X0)) = meet(join(X2,X0),meet(X1,join(meet(X0,X1),meet(X3,meet(join(X2,X0),X1))))),
inference(forward_demodulation,[],[f15488,f7]) ).
fof(f15909,plain,
! [X0] : join(meet(X0,a),sF3) = meet(a,join(sF3,meet(X0,a))),
inference(forward_demodulation,[],[f15776,f26]) ).
fof(f15936,plain,
! [X2,X3,X0,X1] : join(meet(X3,meet(join(X2,X0),X1)),meet(meet(join(X2,X0),X1),X0)) = meet(join(X2,X0),join(meet(X3,meet(join(X2,X0),X1)),meet(X1,X0))),
inference(forward_demodulation,[],[f15804,f15532]) ).
fof(f16021,plain,
! [X0] : join(sF3,meet(a,X0)) = join(meet(X0,a),sF3),
inference(forward_demodulation,[],[f15909,f8059]) ).
fof(f16047,plain,
! [X2,X3,X0,X1] : join(meet(X3,meet(join(X2,X0),X1)),meet(meet(join(X2,X0),X1),X0)) = meet(join(X2,X0),join(meet(X1,X0),meet(X3,meet(join(X2,X0),X1)))),
inference(forward_demodulation,[],[f15936,f6]) ).
fof(f16098,plain,
! [X0] : join(sF3,meet(a,X0)) = join(sF3,meet(X0,a)),
inference(forward_demodulation,[],[f16021,f6]) ).
fof(f16119,plain,
! [X2,X3,X0,X1] : join(meet(X3,meet(join(X2,X0),X1)),meet(X0,meet(join(X2,X0),X1))) = meet(join(X2,X0),join(meet(X1,X0),meet(X3,meet(join(X2,X0),X1)))),
inference(forward_demodulation,[],[f16047,f5]) ).
fof(f16170,plain,
! [X2,X3,X0,X1] : join(meet(X3,meet(join(X2,X0),X1)),meet(X0,X1)) = meet(join(X2,X0),join(meet(X1,X0),meet(X3,meet(join(X2,X0),X1)))),
inference(forward_demodulation,[],[f16119,f217]) ).
fof(f16212,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X3,meet(join(X2,X0),X1))) = meet(join(X2,X0),join(meet(X1,X0),meet(X3,meet(join(X2,X0),X1)))),
inference(forward_demodulation,[],[f16170,f6]) ).
fof(f17676,plain,
! [X2,X3,X0,X1] : meet(meet(join(X2,X0),X1),join(meet(X0,X1),meet(X3,meet(join(X2,X0),X1)))) = join(meet(meet(join(X2,X0),X1),X3),meet(meet(join(X2,X0),X1),X0)),
inference(superposition,[],[f167,f217]) ).
fof(f18011,plain,
! [X2,X3,X0,X1] : join(meet(meet(join(X2,X0),X1),X3),meet(X0,meet(join(X2,X0),X1))) = meet(meet(join(X2,X0),X1),join(meet(X0,X1),meet(X3,meet(join(X2,X0),X1)))),
inference(forward_demodulation,[],[f17676,f5]) ).
fof(f18166,plain,
! [X2,X3,X0,X1] : join(meet(meet(join(X2,X0),X1),X3),meet(X0,meet(join(X2,X0),X1))) = meet(join(X2,X0),meet(X1,join(meet(X0,X1),meet(X3,meet(join(X2,X0),X1))))),
inference(forward_demodulation,[],[f18011,f7]) ).
fof(f18304,plain,
! [X2,X3,X0,X1] : join(meet(meet(join(X2,X0),X1),X3),meet(X0,meet(join(X2,X0),X1))) = meet(join(X2,X0),join(meet(X3,meet(join(X2,X0),X1)),meet(X1,X0))),
inference(forward_demodulation,[],[f18166,f15532]) ).
fof(f18407,plain,
! [X2,X3,X0,X1] : join(meet(meet(join(X2,X0),X1),X3),meet(X0,meet(join(X2,X0),X1))) = meet(join(X2,X0),join(meet(X1,X0),meet(X3,meet(join(X2,X0),X1)))),
inference(forward_demodulation,[],[f18304,f6]) ).
fof(f18483,plain,
! [X2,X3,X0,X1] : join(meet(meet(join(X2,X0),X1),X3),meet(X0,meet(join(X2,X0),X1))) = join(meet(X0,X1),meet(X3,meet(join(X2,X0),X1))),
inference(forward_demodulation,[],[f18407,f16212]) ).
fof(f18527,plain,
! [X2,X3,X0,X1] : join(meet(meet(join(X2,X0),X1),X3),meet(X0,X1)) = join(meet(X0,X1),meet(X3,meet(join(X2,X0),X1))),
inference(forward_demodulation,[],[f18483,f217]) ).
fof(f18556,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(meet(join(X2,X0),X1),X3)) = join(meet(X0,X1),meet(X3,meet(join(X2,X0),X1))),
inference(forward_demodulation,[],[f18527,f6]) ).
fof(f18579,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(join(X2,X0),meet(X1,X3))) = join(meet(X0,X1),meet(X3,meet(join(X2,X0),X1))),
inference(forward_demodulation,[],[f18556,f7]) ).
fof(f18617,plain,
! [X0] :
( one != one
| zero != meet(complement(X0),X0)
| complement(complement(X0)) = X0 ),
inference(superposition,[],[f171,f9]) ).
fof(f18646,plain,
! [X0] :
( zero != meet(complement(X0),X0)
| complement(complement(X0)) = X0 ),
inference(trivial_inequality_removal,[],[f18617]) ).
fof(f18668,plain,
! [X0] :
( meet(X0,complement(X0)) != zero
| complement(complement(X0)) = X0 ),
inference(forward_demodulation,[],[f18646,f5]) ).
fof(f18696,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_subsumption_resolution,[],[f18668,f10]) ).
fof(f18779,plain,
! [X0,X1] :
( one != join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(zero)))
| meet(X1,complement(zero)) = complement(meet(X0,complement(meet(X0,X1)))) ),
inference(superposition,[],[f11792,f1064]) ).
fof(f18929,plain,
! [X0,X1] :
( one != join(meet(X1,complement(zero)),meet(X0,complement(meet(X0,X1))))
| meet(X1,complement(zero)) = complement(meet(X0,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f18779,f6]) ).
fof(f18952,plain,
! [X0,X1] :
( one != join(meet(X1,one),meet(X0,complement(meet(X0,X1))))
| meet(X1,complement(zero)) = complement(meet(X0,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f18929,f665]) ).
fof(f18970,plain,
! [X0,X1] :
( one != join(X1,meet(X0,complement(meet(X0,X1))))
| meet(X1,complement(zero)) = complement(meet(X0,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f18952,f285]) ).
fof(f18981,plain,
! [X0,X1] :
( meet(X1,one) = complement(meet(X0,complement(meet(X0,X1))))
| one != join(X1,meet(X0,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f18970,f665]) ).
fof(f18989,plain,
! [X0,X1] :
( complement(meet(X0,complement(meet(X0,X1)))) = X1
| one != join(X1,meet(X0,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f18981,f285]) ).
fof(f20671,plain,
! [X0,X1] : join(X0,meet(meet(join(X1,X0),complement(meet(X1,X0))),complement(meet(X0,meet(join(X1,X0),complement(meet(X1,X0))))))) = join(X0,meet(join(X0,meet(X1,complement(meet(X1,X0)))),complement(meet(X0,meet(join(X1,X0),complement(meet(X1,X0))))))),
inference(superposition,[],[f3339,f10804]) ).
fof(f20692,plain,
! [X0,X1] : join(X0,meet(meet(join(X1,X0),complement(meet(X1,X0))),complement(meet(X0,complement(meet(X1,X0)))))) = join(X0,meet(join(X0,meet(X1,complement(meet(X1,X0)))),complement(meet(X0,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f20671,f217]) ).
fof(f20812,plain,
! [X0,X1] : join(X0,meet(meet(join(X1,X0),complement(meet(X1,X0))),complement(meet(X0,complement(meet(X1,X0)))))) = join(X0,meet(complement(meet(X0,complement(meet(X1,X0)))),join(X0,meet(X1,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f20692,f5]) ).
fof(f20905,plain,
! [X0,X1] : join(X0,meet(complement(meet(X0,complement(meet(X1,X0)))),join(X0,meet(X1,complement(meet(X1,X0)))))) = join(X0,meet(complement(meet(X0,complement(meet(X1,X0)))),meet(join(X1,X0),complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f20812,f5]) ).
fof(f20971,plain,
! [X0,X1] : join(X0,meet(complement(meet(X0,complement(meet(X1,X0)))),join(X0,meet(X1,complement(meet(X1,X0)))))) = join(X0,meet(complement(meet(X1,X0)),meet(complement(meet(X0,complement(meet(X1,X0)))),join(X1,X0)))),
inference(forward_demodulation,[],[f20905,f228]) ).
fof(f21013,plain,
! [X0,X1] : join(X0,meet(complement(meet(X0,complement(meet(X1,X0)))),join(X0,meet(X1,complement(meet(X1,X0)))))) = join(X0,meet(join(X1,X0),meet(complement(meet(X1,X0)),complement(meet(X0,complement(meet(X1,X0))))))),
inference(forward_demodulation,[],[f20971,f228]) ).
fof(f22614,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = join(meet(X2,X1),meet(X2,join(X0,X1))),
inference(superposition,[],[f1531,f159]) ).
fof(f22788,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X0,meet(join(X2,X0),join(X1,X0)))),
inference(backward_demodulation,[],[f158,f22614]) ).
fof(f29260,plain,
! [X0,X1] :
( one != one
| complement(X0) = meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))) ),
inference(superposition,[],[f11793,f3783]) ).
fof(f29262,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = meet(X0,join(meet(join(X0,complement(meet(X0,X1))),complement(meet(X0,complement(meet(X0,X1))))),meet(complement(meet(X0,X1)),one))),
inference(superposition,[],[f79,f3783]) ).
fof(f29328,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))),
inference(trivial_inequality_removal,[],[f29260]) ).
fof(f29380,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = meet(X0,join(meet(complement(meet(X0,X1)),one),meet(join(X0,complement(meet(X0,X1))),complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f29262,f6]) ).
fof(f29476,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = meet(X0,join(meet(complement(meet(X0,X1)),one),meet(one,complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f29380,f331]) ).
fof(f29539,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = meet(X0,join(meet(one,complement(meet(X0,X1))),meet(one,complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f29476,f9987]) ).
fof(f29574,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = meet(X0,join(meet(one,complement(meet(X0,X1))),complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f29539,f300]) ).
fof(f29604,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,[],[f29574,f300]) ).
fof(f29623,plain,
! [X0,X1] : meet(X0,one) = join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f29604,f411]) ).
fof(f29637,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = X0,
inference(forward_demodulation,[],[f29623,f285]) ).
fof(f29678,plain,
! [X0,X1] : complement(X1) = meet(complement(meet(X0,X1)),complement(meet(X1,complement(meet(X0,X1))))),
inference(superposition,[],[f29328,f913]) ).
fof(f29712,plain,
! [X0,X1] : complement(complement(meet(X0,X1))) = meet(complement(complement(X0)),complement(meet(complement(meet(X0,X1)),complement(complement(X0))))),
inference(superposition,[],[f29328,f29328]) ).
fof(f29742,plain,
! [X0,X1] : meet(join(X0,complement(meet(X0,X1))),complement(meet(X0,complement(meet(X0,X1))))) = join(complement(X0),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(superposition,[],[f3345,f29328]) ).
fof(f29858,plain,
! [X0,X1] : meet(one,complement(meet(X0,complement(meet(X0,X1))))) = join(complement(X0),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f29742,f331]) ).
fof(f29884,plain,
! [X0,X1] : complement(complement(meet(X0,X1))) = meet(complement(complement(X0)),complement(meet(complement(complement(X0)),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f29712,f5]) ).
fof(f29901,plain,
! [X0,X1] : join(X0,meet(join(X1,X0),complement(X0))) = join(X0,meet(complement(meet(X0,complement(meet(X1,X0)))),join(X0,meet(X1,complement(meet(X1,X0)))))),
inference(backward_demodulation,[],[f21013,f29678]) ).
fof(f29952,plain,
! [X0,X1] : complement(meet(X0,complement(meet(X0,X1)))) = join(complement(X0),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f29858,f300]) ).
fof(f29968,plain,
! [X0,X1] : complement(complement(meet(X0,X1))) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f29884,f18696]) ).
fof(f29977,plain,
! [X0,X1] : join(X0,meet(complement(X0),join(X1,X0))) = join(X0,meet(complement(meet(X0,complement(meet(X1,X0)))),join(X0,meet(X1,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f29901,f5]) ).
fof(f30017,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f29968,f18696]) ).
fof(f30041,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,X1)) = X0,
inference(backward_demodulation,[],[f29637,f30017]) ).
fof(f30042,plain,
! [X0,X1] : complement(meet(X0,complement(meet(X0,X1)))) = join(complement(X0),meet(X0,X1)),
inference(backward_demodulation,[],[f29952,f30017]) ).
fof(f30095,plain,
! [X0,X1] :
( join(complement(X0),meet(X0,X1)) = X1
| one != join(X1,meet(X0,complement(meet(X0,X1)))) ),
inference(backward_demodulation,[],[f18989,f30042]) ).
fof(f30100,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X0,X1)),join(complement(X0),meet(X0,X1))),
inference(backward_demodulation,[],[f29328,f30042]) ).
fof(f30114,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),meet(X0,X1))),
inference(backward_demodulation,[],[f30017,f30042]) ).
fof(f30129,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = X0,
inference(forward_demodulation,[],[f30041,f6]) ).
fof(f30307,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X0,meet(complement(X0),X1))),
inference(superposition,[],[f30114,f18696]) ).
fof(f30330,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(complement(X1),meet(X0,X1))),
inference(superposition,[],[f30114,f913]) ).
fof(f30443,plain,
! [X0,X1] : meet(join(X0,join(complement(X0),meet(X0,X1))),complement(meet(X0,X1))) = join(meet(X0,complement(meet(X0,X1))),meet(join(complement(X0),meet(X0,X1)),complement(meet(X0,X1)))),
inference(superposition,[],[f3170,f30114]) ).
fof(f30495,plain,
! [X0,X1] : meet(join(X0,join(complement(X0),meet(X0,X1))),complement(meet(X0,X1))) = join(meet(X0,complement(meet(X0,X1))),meet(complement(meet(X0,X1)),join(complement(X0),meet(X0,X1)))),
inference(forward_demodulation,[],[f30443,f5]) ).
fof(f30659,plain,
! [X0,X1] : meet(join(X0,join(complement(X0),meet(X0,X1))),complement(meet(X0,X1))) = join(meet(X0,complement(meet(X0,X1))),complement(X0)),
inference(forward_demodulation,[],[f30495,f30100]) ).
fof(f30774,plain,
! [X0,X1] : meet(join(X0,join(complement(X0),meet(X0,X1))),complement(meet(X0,X1))) = join(complement(X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f30659,f6]) ).
fof(f30832,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(X0,join(complement(X0),meet(X0,X1)))) = join(complement(X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f30774,f5]) ).
fof(f30873,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(X0,complement(X0))) = join(complement(X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f30832,f262]) ).
fof(f30898,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),one) = join(complement(X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f30873,f9]) ).
fof(f30917,plain,
! [X0,X1] : meet(one,complement(meet(X0,X1))) = join(complement(X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f30898,f5]) ).
fof(f30928,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f30917,f300]) ).
fof(f30971,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,complement(meet(X0,X1)))) = X1,
inference(superposition,[],[f30129,f913]) ).
fof(f31027,plain,
! [X0,X1] : join(meet(X1,X0),X0) = join(meet(X1,X0),meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f1218,f30129]) ).
fof(f31029,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f125,f30129]) ).
fof(f31127,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),
inference(backward_demodulation,[],[f10804,f31029]) ).
fof(f31128,plain,
! [X0,X1] :
( complement(X1) = meet(X0,complement(meet(X0,X1)))
| join(X1,X0) != one ),
inference(backward_demodulation,[],[f11792,f31029]) ).
fof(f31148,plain,
! [X0,X1] : join(X0,meet(complement(X0),join(X1,X0))) = join(X0,meet(complement(meet(X0,complement(meet(X1,X0)))),join(X0,X1))),
inference(backward_demodulation,[],[f29977,f31029]) ).
fof(f31149,plain,
! [X0,X1] :
( join(complement(X0),meet(X0,X1)) = X1
| join(X1,X0) != one ),
inference(backward_demodulation,[],[f30095,f31029]) ).
fof(f31160,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = join(meet(X1,X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f31027,f6]) ).
fof(f31192,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X1,X0)))) = X0,
inference(backward_demodulation,[],[f6734,f30971]) ).
fof(f31238,plain,
! [X0,X1] : join(X0,meet(complement(X0),join(X1,X0))) = join(X0,meet(join(X0,X1),complement(meet(X0,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f31148,f5]) ).
fof(f31249,plain,
! [X0,X1] : join(meet(X1,X0),meet(X0,complement(meet(X0,X1)))) = X0,
inference(forward_demodulation,[],[f31160,f77]) ).
fof(f31459,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f31029,f5]) ).
fof(f31724,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(join(X0,X1),complement(meet(X0,X1)))),
inference(backward_demodulation,[],[f3339,f31459]) ).
fof(f31740,plain,
! [X0,X1] :
( complement(X1) = meet(X0,complement(meet(X1,X0)))
| join(X1,X0) != one ),
inference(backward_demodulation,[],[f11793,f31459]) ).
fof(f32115,plain,
! [X0,X1] : meet(X0,complement(X1)) = meet(complement(X1),join(X1,meet(X0,complement(X1)))),
inference(superposition,[],[f30307,f913]) ).
fof(f32909,plain,
! [X0,X1] :
( complement(X1) = meet(complement(meet(X0,X1)),complement(complement(X0)))
| one != join(X1,complement(meet(X0,X1)))
| join(X0,X1) != one ),
inference(superposition,[],[f31740,f31740]) ).
fof(f32995,plain,
! [X0,X1] :
( join(complement(X0),meet(X1,complement(complement(X0)))) = X1
| join(X0,X1) != one ),
inference(superposition,[],[f30129,f31740]) ).
fof(f33022,plain,
! [X0,X1] :
( join(complement(X0),meet(X1,X0)) = X1
| join(X0,X1) != one ),
inference(forward_demodulation,[],[f32995,f18696]) ).
fof(f33079,plain,
! [X0,X1] :
( complement(X1) = meet(complement(meet(X0,X1)),complement(complement(X0)))
| join(X0,X1) != one ),
inference(forward_subsumption_resolution,[],[f32909,f411]) ).
fof(f33155,plain,
! [X0,X1] :
( complement(X1) = meet(complement(complement(X0)),complement(meet(X0,X1)))
| join(X0,X1) != one ),
inference(forward_demodulation,[],[f33079,f5]) ).
fof(f33200,plain,
! [X0,X1] :
( complement(X1) = meet(X0,complement(meet(X0,X1)))
| join(X0,X1) != one ),
inference(forward_demodulation,[],[f33155,f18696]) ).
fof(f34521,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(join(X0,X1),complement(meet(X0,meet(join(X1,X0),complement(meet(X1,X0))))))),
inference(superposition,[],[f31724,f31127]) ).
fof(f34588,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,meet(join(X1,meet(X2,X0)),complement(meet(X0,meet(X1,X2))))),
inference(superposition,[],[f31724,f228]) ).
fof(f34590,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X2,X0))) = join(X0,meet(join(X0,meet(X1,join(X2,X0))),complement(meet(X0,X1)))),
inference(superposition,[],[f31724,f2282]) ).
fof(f34596,plain,
! [X2,X0,X1] : join(X1,meet(join(X1,X2),X0)) = join(X1,meet(join(X1,meet(join(X1,X2),X0)),complement(meet(X0,X1)))),
inference(superposition,[],[f31724,f913]) ).
fof(f34605,plain,
! [X0,X1] : join(X0,join(X0,X1)) = join(X0,meet(join(X0,join(X0,X1)),complement(X0))),
inference(superposition,[],[f31724,f3]) ).
fof(f34808,plain,
! [X0,X1] : join(X0,join(X0,X1)) = join(X0,meet(complement(X0),join(X0,join(X0,X1)))),
inference(forward_demodulation,[],[f34605,f5]) ).
fof(f34817,plain,
! [X2,X0,X1] : join(X1,meet(join(X1,X2),X0)) = join(X1,meet(complement(meet(X0,X1)),join(X1,meet(join(X1,X2),X0)))),
inference(forward_demodulation,[],[f34596,f5]) ).
fof(f34823,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X2,X0))) = join(X0,meet(complement(meet(X0,X1)),join(X0,meet(X1,join(X2,X0))))),
inference(forward_demodulation,[],[f34590,f5]) ).
fof(f34825,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,meet(X2,meet(X0,complement(meet(X0,meet(X1,X2)))))),
inference(backward_demodulation,[],[f4929,f34588]) ).
fof(f34867,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(join(X0,X1),complement(meet(X0,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f34521,f217]) ).
fof(f34950,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f34808,f113]) ).
fof(f34959,plain,
! [X2,X0,X1] : join(X1,meet(join(X1,X2),X0)) = join(X1,meet(X0,meet(complement(meet(X0,X1)),join(X1,X2)))),
inference(backward_demodulation,[],[f10717,f34817]) ).
fof(f34965,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X2,X0))) = join(X0,meet(X1,meet(join(X2,X0),complement(meet(X0,X1))))),
inference(backward_demodulation,[],[f15417,f34823]) ).
fof(f34992,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(complement(X0),join(X1,X0))),
inference(backward_demodulation,[],[f31238,f34867]) ).
fof(f35298,plain,
! [X2,X0,X1] : join(X0,join(meet(X0,X1),X2)) = join(X0,meet(complement(meet(X0,X1)),join(meet(X0,X1),X2))),
inference(superposition,[],[f124,f34950]) ).
fof(f35320,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,meet(complement(meet(X0,X1)),join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f35298,f124]) ).
fof(f35550,plain,
! [X0,X1] : complement(meet(X1,complement(meet(X0,X1)))) = join(complement(X1),meet(X0,X1)),
inference(superposition,[],[f30042,f913]) ).
fof(f36778,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(meet(X1,join(X2,X0)),X0),meet(meet(X1,join(X2,X0)),complement(meet(X0,X1)))),
inference(superposition,[],[f31192,f2282]) ).
fof(f37013,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X0,meet(X1,join(X2,X0))),meet(meet(X1,join(X2,X0)),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f36778,f9987]) ).
fof(f37180,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X0,meet(X1,join(X2,X0))),meet(complement(meet(X0,X1)),meet(X1,join(X2,X0)))),
inference(forward_demodulation,[],[f37013,f5]) ).
fof(f37321,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X0,meet(X1,join(X2,X0))),meet(X1,meet(join(X2,X0),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f37180,f228]) ).
fof(f37414,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X0,X1),meet(X1,meet(join(X2,X0),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f37321,f2282]) ).
fof(f37673,plain,
! [X0,X1] : meet(complement(X0),join(X1,X0)) = meet(complement(X0),join(X0,X1)),
inference(superposition,[],[f30307,f34992]) ).
fof(f38155,plain,
! [X0,X1] : meet(X0,join(complement(X0),X1)) = meet(X0,join(X1,complement(X0))),
inference(superposition,[],[f37673,f18696]) ).
fof(f38208,plain,
! [X2,X0,X1] : meet(complement(X0),meet(join(X1,X0),X2)) = meet(X2,meet(complement(X0),join(X0,X1))),
inference(superposition,[],[f228,f37673]) ).
fof(f38267,plain,
! [X2,X0,X1] : meet(complement(X0),meet(join(X0,X1),X2)) = meet(meet(complement(X0),join(X1,X0)),X2),
inference(superposition,[],[f7,f37673]) ).
fof(f38366,plain,
! [X2,X0,X1] : meet(complement(X0),meet(join(X0,X1),X2)) = meet(complement(X0),meet(join(X1,X0),X2)),
inference(forward_demodulation,[],[f38267,f7]) ).
fof(f38606,plain,
! [X2,X0,X1] : meet(X1,join(X0,join(complement(X1),X2))) = meet(X1,join(join(X2,X0),complement(X1))),
inference(superposition,[],[f38155,f138]) ).
fof(f38620,plain,
! [X2,X0,X1] : meet(X2,join(X0,join(X1,complement(X2)))) = meet(X2,join(complement(X2),join(X0,X1))),
inference(superposition,[],[f38155,f8]) ).
fof(f38923,plain,
! [X2,X0,X1] : meet(X1,join(X2,join(X0,complement(X1)))) = meet(X1,join(X0,join(complement(X1),X2))),
inference(forward_demodulation,[],[f38606,f8]) ).
fof(f40651,plain,
! [X0,X1] :
( zero != meet(meet(X1,X0),join(meet(X0,complement(meet(X0,X1))),complement(X0)))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(superposition,[],[f1185,f31249]) ).
fof(f40686,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,join(meet(X0,complement(meet(X0,X1))),complement(X0))))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(forward_demodulation,[],[f40651,f7]) ).
fof(f40878,plain,
! [X0,X1] :
( zero != 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,[],[f40686,f38155]) ).
fof(f41035,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,complement(meet(X0,X1))))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(forward_demodulation,[],[f40878,f30114]) ).
fof(f41144,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)),
inference(forward_subsumption_resolution,[],[f41035,f1064]) ).
fof(f41216,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f41144,f6]) ).
fof(f43195,plain,
! [X0,X1] :
( complement(meet(X0,X1)) = complement(meet(X1,X0))
| one != join(complement(meet(X1,X0)),X1) ),
inference(superposition,[],[f31149,f41216]) ).
fof(f43196,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(X1,complement(meet(X1,X0))),
inference(superposition,[],[f30114,f41216]) ).
fof(f43294,plain,
! [X0,X1] :
( one != join(X1,complement(meet(X1,X0)))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(forward_demodulation,[],[f43195,f6]) ).
fof(f43422,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(forward_subsumption_resolution,[],[f43294,f331]) ).
fof(f43946,plain,
! [X2,X0,X1] : meet(meet(X0,complement(meet(X0,X1))),X2) = meet(X0,meet(X2,complement(meet(X1,X0)))),
inference(superposition,[],[f2379,f43196]) ).
fof(f44023,plain,
! [X2,X0,X1] : meet(X0,meet(complement(meet(X0,X1)),X2)) = meet(X2,meet(X0,complement(meet(X1,X0)))),
inference(superposition,[],[f228,f43196]) ).
fof(f44074,plain,
! [X0,X1] : complement(meet(complement(meet(X0,X1)),X0)) = join(complement(X0),meet(X0,complement(meet(X0,complement(meet(X1,X0)))))),
inference(superposition,[],[f41216,f43196]) ).
fof(f44104,plain,
! [X0,X1] : complement(meet(X0,complement(meet(X1,X0)))) = complement(meet(complement(meet(X0,X1)),X0)),
inference(forward_demodulation,[],[f44074,f30928]) ).
fof(f44182,plain,
! [X2,X0,X1] : meet(X0,meet(complement(meet(X0,X1)),X2)) = meet(X0,meet(X2,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f43946,f7]) ).
fof(f44227,plain,
! [X0,X1] : complement(meet(X0,complement(meet(X0,X1)))) = complement(meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f44104,f43422]) ).
fof(f44305,plain,
! [X0,X1] : complement(meet(X0,complement(meet(X0,X1)))) = join(complement(X0),meet(X1,X0)),
inference(forward_demodulation,[],[f44227,f35550]) ).
fof(f46912,plain,
! [X0,X1] : meet(join(X0,X1),join(complement(join(X0,X1)),X0)) = X0,
inference(superposition,[],[f30330,f3]) ).
fof(f47060,plain,
! [X0,X1] :
( meet(X1,complement(meet(X0,X1))) = complement(join(complement(X1),meet(X0,X1)))
| one != join(X1,join(complement(X1),meet(X0,X1))) ),
inference(superposition,[],[f33200,f30330]) ).
fof(f47094,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = complement(join(complement(X1),meet(X0,X1))),
inference(forward_subsumption_resolution,[],[f47060,f306]) ).
fof(f47203,plain,
! [X0,X1] : meet(join(X0,X1),join(X0,complement(join(X0,X1)))) = X0,
inference(forward_demodulation,[],[f46912,f38155]) ).
fof(f47543,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f217,f47203]) ).
fof(f47605,plain,
! [X0,X1] : join(complement(join(X0,X1)),X0) = complement(meet(join(X0,X1),complement(X0))),
inference(superposition,[],[f30042,f47203]) ).
fof(f47624,plain,
! [X0,X1] :
( meet(join(X0,X1),complement(X0)) = complement(join(X0,complement(join(X0,X1))))
| one != join(join(X0,X1),join(X0,complement(join(X0,X1)))) ),
inference(superposition,[],[f33200,f47203]) ).
fof(f47631,plain,
! [X0,X1] : meet(join(X0,X1),complement(X0)) = complement(join(X0,complement(join(X0,X1)))),
inference(forward_subsumption_resolution,[],[f47624,f993]) ).
fof(f47649,plain,
! [X0,X1] : join(complement(join(X0,X1)),X0) = complement(meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f47605,f43422]) ).
fof(f47709,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(join(X1,complement(join(X1,X0)))))) = meet(X0,join(complement(join(X1,complement(join(X1,X0)))),meet(X0,X1))),
inference(backward_demodulation,[],[f4412,f47543]) ).
fof(f47711,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(X2,meet(join(X1,complement(join(X1,X0))),join(X0,meet(X2,join(X1,complement(join(X1,X0)))))))),
inference(backward_demodulation,[],[f5971,f47543]) ).
fof(f47748,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = complement(join(X0,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f47631,f5]) ).
fof(f47761,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = complement(meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f47649,f6]) ).
fof(f47801,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(join(X1,complement(join(X1,X0)))))) = meet(X0,join(meet(X0,X1),complement(join(X1,complement(join(X1,X0)))))),
inference(forward_demodulation,[],[f47709,f6]) ).
fof(f47858,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,meet(complement(X1),join(X1,X0)))) = meet(X0,join(meet(X0,X1),meet(complement(X1),join(X1,X0)))),
inference(forward_demodulation,[],[f47801,f47748]) ).
fof(f47892,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(X1))) = meet(X0,join(meet(X0,X1),meet(complement(X1),join(X1,X0)))),
inference(forward_demodulation,[],[f47858,f2282]) ).
fof(f48996,plain,
! [X0,X1] :
( meet(X0,complement(meet(X0,X1))) = complement(join(X1,complement(join(X1,X0))))
| one != join(join(X1,complement(join(X1,X0))),X0) ),
inference(superposition,[],[f31128,f47543]) ).
fof(f48997,plain,
! [X0,X1] :
( join(X1,complement(join(X1,X0))) = join(complement(X0),meet(X0,X1))
| one != join(join(X1,complement(join(X1,X0))),X0) ),
inference(superposition,[],[f31149,f47543]) ).
fof(f49005,plain,
! [X0,X1] :
( join(complement(join(X1,complement(join(X1,X0)))),meet(X0,X1)) = X0
| one != join(join(X1,complement(join(X1,X0))),X0) ),
inference(superposition,[],[f33022,f47543]) ).
fof(f49045,plain,
! [X0,X1] :
( join(meet(X0,X1),complement(join(X1,complement(join(X1,X0))))) = X0
| one != join(join(X1,complement(join(X1,X0))),X0) ),
inference(forward_demodulation,[],[f49005,f6]) ).
fof(f49053,plain,
! [X0,X1] :
( one != join(X0,join(X1,complement(join(X1,X0))))
| join(X1,complement(join(X1,X0))) = join(complement(X0),meet(X0,X1)) ),
inference(forward_demodulation,[],[f48997,f6]) ).
fof(f49054,plain,
! [X0,X1] :
( meet(X0,complement(meet(X0,X1))) = meet(complement(X1),join(X1,X0))
| one != join(join(X1,complement(join(X1,X0))),X0) ),
inference(forward_demodulation,[],[f48996,f47748]) ).
fof(f49200,plain,
! [X0,X1] :
( join(meet(X0,X1),meet(complement(X1),join(X1,X0))) = X0
| one != join(join(X1,complement(join(X1,X0))),X0) ),
inference(forward_demodulation,[],[f49045,f47748]) ).
fof(f49208,plain,
! [X0,X1] : join(X1,complement(join(X1,X0))) = join(complement(X0),meet(X0,X1)),
inference(forward_subsumption_resolution,[],[f49053,f1153]) ).
fof(f49209,plain,
! [X0,X1] :
( one != join(X0,join(X1,complement(join(X1,X0))))
| meet(X0,complement(meet(X0,X1))) = meet(complement(X1),join(X1,X0)) ),
inference(forward_demodulation,[],[f49054,f6]) ).
fof(f49313,plain,
! [X0,X1] :
( one != join(X0,join(X1,complement(join(X1,X0))))
| join(meet(X0,X1),meet(complement(X1),join(X1,X0))) = X0 ),
inference(forward_demodulation,[],[f49200,f6]) ).
fof(f49319,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = meet(complement(X1),join(X1,X0)),
inference(forward_subsumption_resolution,[],[f49209,f1153]) ).
fof(f49388,plain,
! [X0,X1] : join(meet(X0,X1),meet(complement(X1),join(X1,X0))) = X0,
inference(forward_subsumption_resolution,[],[f49313,f1153]) ).
fof(f49432,plain,
! [X0,X1] : meet(X0,X0) = join(meet(X0,X1),meet(X0,complement(X1))),
inference(backward_demodulation,[],[f47892,f49388]) ).
fof(f49469,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(X1))) = X0,
inference(forward_demodulation,[],[f49432,f1]) ).
fof(f49914,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(X1))),
inference(superposition,[],[f125,f49469]) ).
fof(f49923,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(X1),meet(X0,X1)),
inference(superposition,[],[f1235,f49469]) ).
fof(f50028,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(complement(X1),X0)),
inference(backward_demodulation,[],[f30330,f49923]) ).
fof(f50051,plain,
! [X0,X1] : join(complement(X0),X1) = complement(meet(X0,complement(meet(X0,X1)))),
inference(backward_demodulation,[],[f44305,f49923]) ).
fof(f50066,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = complement(join(complement(X1),X0)),
inference(backward_demodulation,[],[f47094,f49923]) ).
fof(f50103,plain,
! [X0,X1] : meet(X0,complement(X1)) = meet(complement(X1),join(X1,X0)),
inference(backward_demodulation,[],[f32115,f49914]) ).
fof(f50435,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = complement(join(complement(X1),X0)),
inference(backward_demodulation,[],[f43196,f50066]) ).
fof(f50448,plain,
! [X2,X0,X1] : meet(X0,meet(complement(meet(X0,X1)),X2)) = meet(X2,complement(join(complement(X0),X1))),
inference(backward_demodulation,[],[f44023,f50066]) ).
fof(f50540,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),meet(X0,X1)),
inference(backward_demodulation,[],[f30042,f50051]) ).
fof(f50549,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = meet(X0,join(X2,meet(join(complement(X0),X1),join(X0,meet(join(complement(X0),X1),X2))))),
inference(backward_demodulation,[],[f11280,f50028]) ).
fof(f50619,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(X2,join(X0,join(X1,complement(X2)))),
inference(backward_demodulation,[],[f38620,f50028]) ).
fof(f50688,plain,
! [X2,X0,X1] : meet(complement(X0),meet(join(X1,X0),X2)) = meet(X2,meet(X1,complement(X0))),
inference(backward_demodulation,[],[f38208,f50103]) ).
fof(f50711,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = complement(meet(X1,complement(X0))),
inference(backward_demodulation,[],[f47761,f50103]) ).
fof(f50714,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = meet(X0,complement(X1)),
inference(backward_demodulation,[],[f49319,f50103]) ).
fof(f50747,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,meet(X2,complement(meet(X0,X1)))),
inference(backward_demodulation,[],[f35320,f50103]) ).
fof(f50979,plain,
! [X2,X0,X1] : meet(X0,meet(X2,complement(meet(X1,X0)))) = meet(X2,complement(join(complement(X0),X1))),
inference(backward_demodulation,[],[f44182,f50448]) ).
fof(f50990,plain,
! [X2,X0,X1] : join(X1,meet(join(X1,X2),X0)) = join(X1,meet(join(X1,X2),complement(join(complement(X0),X1)))),
inference(backward_demodulation,[],[f34959,f50448]) ).
fof(f51173,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,meet(X2,complement(join(complement(X0),meet(X1,X2))))),
inference(backward_demodulation,[],[f34825,f50435]) ).
fof(f51349,plain,
! [X0,X1] : join(complement(X0),X1) = join(X1,complement(join(X1,X0))),
inference(backward_demodulation,[],[f49208,f50540]) ).
fof(f51408,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = meet(X1,join(X0,join(complement(X1),X2))),
inference(backward_demodulation,[],[f38923,f50619]) ).
fof(f51611,plain,
! [X0,X1] : meet(X1,complement(X0)) = complement(join(complement(X1),X0)),
inference(backward_demodulation,[],[f50435,f50714]) ).
fof(f51623,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(X2,meet(complement(meet(X0,complement(X1))),join(X0,meet(X2,complement(meet(X0,complement(X1)))))))),
inference(backward_demodulation,[],[f47711,f50711]) ).
fof(f51724,plain,
! [X2,X0,X1] : meet(complement(X0),meet(join(X0,X1),X2)) = meet(X2,meet(X1,complement(X0))),
inference(backward_demodulation,[],[f38366,f50688]) ).
fof(f51945,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X0,X1),meet(join(X2,X0),complement(join(complement(X1),X0)))),
inference(backward_demodulation,[],[f37414,f50979]) ).
fof(f51946,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X2,X0))) = join(X0,meet(join(X2,X0),complement(join(complement(X1),X0)))),
inference(backward_demodulation,[],[f34965,f50979]) ).
fof(f52218,plain,
! [X0,X1] : join(complement(X1),X0) = complement(meet(X1,complement(X0))),
inference(backward_demodulation,[],[f50711,f51349]) ).
fof(f52455,plain,
! [X2,X0,X1] : meet(X2,meet(X0,complement(X1))) = meet(X0,meet(X2,complement(meet(X1,X0)))),
inference(backward_demodulation,[],[f50979,f51611]) ).
fof(f52457,plain,
! [X2,X0,X1] : join(X1,meet(join(X1,X2),X0)) = join(X1,meet(join(X1,X2),meet(X0,complement(X1)))),
inference(backward_demodulation,[],[f50990,f51611]) ).
fof(f52554,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,meet(X2,meet(X0,complement(meet(X1,X2))))),
inference(backward_demodulation,[],[f51173,f51611]) ).
fof(f52662,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(X2,meet(complement(meet(X0,complement(X1))),join(X0,X2)))),
inference(forward_demodulation,[],[f51623,f50747]) ).
fof(f52841,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X2,X0))) = join(X0,meet(join(X2,X0),meet(X1,complement(X0)))),
inference(forward_demodulation,[],[f51946,f51611]) ).
fof(f52842,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X0,X1),meet(join(X2,X0),meet(X1,complement(X0)))),
inference(forward_demodulation,[],[f51945,f51611]) ).
fof(f53280,plain,
! [X2,X0,X1] : join(X1,meet(join(X1,X2),X0)) = join(X1,meet(complement(X1),meet(join(X1,X2),X0))),
inference(forward_demodulation,[],[f52457,f228]) ).
fof(f53283,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,meet(X0,meet(X2,complement(X1)))),
inference(backward_demodulation,[],[f52554,f52455]) ).
fof(f53345,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(X2,meet(join(complement(X0),X1),join(X0,X2)))),
inference(forward_demodulation,[],[f52662,f52218]) ).
fof(f53464,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X2,X0))) = join(X0,meet(complement(X0),meet(join(X2,X0),X1))),
inference(forward_demodulation,[],[f52841,f228]) ).
fof(f53465,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X0,X1),meet(complement(X0),meet(join(X2,X0),X1))),
inference(forward_demodulation,[],[f52842,f18579]) ).
fof(f53737,plain,
! [X2,X0,X1] : join(X1,meet(join(X1,X2),X0)) = join(X1,meet(X0,meet(X2,complement(X1)))),
inference(forward_demodulation,[],[f53280,f51724]) ).
fof(f53862,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X2,X0))) = join(X0,meet(X1,meet(X2,complement(X0)))),
inference(forward_demodulation,[],[f53464,f50688]) ).
fof(f53863,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X0,X1),meet(X1,meet(X2,complement(X0)))),
inference(forward_demodulation,[],[f53465,f50688]) ).
fof(f54029,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,meet(join(X1,X2),X0)),
inference(forward_demodulation,[],[f53737,f53283]) ).
fof(f54109,plain,
! [X2,X0,X1] : join(X0,meet(X2,X1)) = join(X0,meet(X1,join(X2,X0))),
inference(forward_demodulation,[],[f53862,f53283]) ).
fof(f54234,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = meet(X1,join(X0,meet(X2,join(X1,X0)))),
inference(backward_demodulation,[],[f1566,f54029]) ).
fof(f54320,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(X2,meet(X0,join(complement(X0),X1)))),
inference(backward_demodulation,[],[f53345,f54109]) ).
fof(f54322,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X0,meet(X1,join(X2,X0)))),
inference(backward_demodulation,[],[f22788,f54109]) ).
fof(f54542,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(X1,join(X0,X2)),
inference(forward_demodulation,[],[f54234,f54109]) ).
fof(f54596,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X0,meet(X2,X1))),
inference(forward_demodulation,[],[f54322,f54109]) ).
fof(f54598,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f54320,f50028]) ).
fof(f55228,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = meet(X0,join(X2,meet(join(complement(X0),X1),join(X0,X2)))),
inference(backward_demodulation,[],[f50549,f54542]) ).
fof(f55438,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(X1,X2)),
inference(forward_demodulation,[],[f54598,f54596]) ).
fof(f55812,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = meet(X0,join(X2,meet(X0,join(complement(X0),X1)))),
inference(forward_demodulation,[],[f55228,f54109]) ).
fof(f56197,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X2,X0),meet(X0,X1)),
inference(backward_demodulation,[],[f12991,f55438]) ).
fof(f56981,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = meet(X0,join(X2,join(complement(X0),X1))),
inference(forward_demodulation,[],[f55812,f54542]) ).
fof(f57634,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(meet(X2,complement(X0)),X0)),
inference(backward_demodulation,[],[f53863,f56197]) ).
fof(f57940,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = meet(join(X1,X2),X0),
inference(forward_demodulation,[],[f56981,f51408]) ).
fof(f58590,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X0,meet(X2,complement(X0)))),
inference(forward_demodulation,[],[f57634,f6]) ).
fof(f59298,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = meet(X1,join(X2,X0)),
inference(forward_demodulation,[],[f58590,f49914]) ).
fof(f62248,plain,
! [X0] : join(sF2,meet(a,X0)) = meet(join(b,X0),a),
inference(superposition,[],[f57940,f25]) ).
fof(f62249,plain,
! [X0] : join(sF3,meet(a,X0)) = meet(join(c,X0),a),
inference(superposition,[],[f57940,f26]) ).
fof(f62318,plain,
! [X0] : join(meet(X0,a),sF3) = meet(join(X0,sF3),a),
inference(superposition,[],[f57940,f758]) ).
fof(f62421,plain,
! [X0] : meet(a,join(X0,sF3)) = join(meet(X0,a),sF3),
inference(forward_demodulation,[],[f62318,f5]) ).
fof(f62500,plain,
! [X0] : join(sF3,meet(a,X0)) = meet(a,join(c,X0)),
inference(forward_demodulation,[],[f62249,f5]) ).
fof(f62501,plain,
! [X0] : join(sF2,meet(a,X0)) = meet(a,join(b,X0)),
inference(forward_demodulation,[],[f62248,f5]) ).
fof(f62665,plain,
! [X0] : meet(a,join(X0,sF3)) = join(sF3,meet(X0,a)),
inference(forward_demodulation,[],[f62421,f6]) ).
fof(f62753,plain,
! [X0] : meet(a,join(c,X0)) = join(sF3,meet(X0,a)),
inference(backward_demodulation,[],[f16098,f62500]) ).
fof(f63158,plain,
! [X0] : meet(a,join(X0,sF3)) = meet(a,join(c,X0)),
inference(backward_demodulation,[],[f62665,f62753]) ).
fof(f70494,plain,
join(sF2,sF3) = meet(a,join(b,sF3)),
inference(superposition,[],[f62501,f758]) ).
fof(f70562,plain,
join(sF2,sF3) = meet(a,join(c,b)),
inference(forward_demodulation,[],[f70494,f63158]) ).
fof(f70614,plain,
meet(a,join(b,c)) = join(sF2,sF3),
inference(forward_demodulation,[],[f70562,f59298]) ).
fof(f70651,plain,
meet(a,join(b,c)) = sF4,
inference(forward_demodulation,[],[f70614,f23]) ).
fof(f70674,plain,
meet(a,sF0) = sF4,
inference(forward_demodulation,[],[f70651,f15]) ).
fof(f70684,plain,
sF1 = sF4,
inference(forward_demodulation,[],[f70674,f17]) ).
fof(f70689,plain,
$false,
inference(forward_subsumption_resolution,[],[f70684,f24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT191-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.41 % Computer : n011.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Sun Sep 27 14:05:00 UTC 2026
% 0.16/0.41 % CPUTime :
% 0.16/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.47 Running first-order theorem proving
% 0.16/0.47 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.71/3.65 % (2441208)Input is clausal, will run a generic CNF schedule.
% 18.71/3.65 % (2441219)dis-21_1_sil=8000:lcm=predicate:random_seed=1661479192: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.71/3.65 % (2441219)Refutation not found, incomplete strategy
% 18.71/3.65 % (2441219)------------------------------
% 18.71/3.65 % (2441219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.71/3.65 % (2441219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.71/3.65 % (2441219)CaDiCaL version: 2.1.3
% 18.71/3.65 % (2441219)Termination reason: Refutation not found, incomplete strategy
% 18.71/3.65 % (2441219)Time elapsed: 0.002 s
% 18.71/3.65 % (2441219)Peak memory usage: 88 MB
% 18.71/3.65 % (2441219)Instructions burned: 1 (million)
% 18.71/3.65 % (2441215)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2002250271:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 18.71/3.65 % (2441218)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=955008858:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 18.71/3.65 % (2441216)lrs+10_1_sil=8000:sp=occurrence:random_seed=10705562:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 18.71/3.65 % (2441214)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=952378894:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 18.71/3.65 % (2441213)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=1823357424:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 18.71/3.65 % (2441217)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4193920182:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 18.71/3.65 % (2441216)Instruction limit reached!
% 18.71/3.65 % (2441216)------------------------------
% 18.71/3.65 % (2441216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.71/3.65 % (2441216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.71/3.65 % (2441216)CaDiCaL version: 2.1.3
% 18.71/3.65 % (2441216)Termination reason: Instruction limit
% 18.71/3.65 % (2441216)Termination phase: Saturation
% 18.71/3.65 % (2441216)Time elapsed: 0.109 s
% 18.71/3.65 % (2441216)Peak memory usage: 88 MB
% 18.71/3.65 % (2441216)Instructions burned: 107 (million)
% 18.71/3.65 % (2441217)Instruction limit reached!
% 18.71/3.65 % (2441217)------------------------------
% 18.71/3.65 % (2441217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.71/3.65 % (2441217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.71/3.65 % (2441217)CaDiCaL version: 2.1.3
% 18.71/3.65 % (2441217)Termination reason: Instruction limit
% 18.71/3.65 % (2441217)Termination phase: Saturation
% 18.71/3.65 % (2441217)Time elapsed: 0.114 s
% 18.71/3.65 % (2441217)Peak memory usage: 89 MB
% 18.71/3.65 % (2441217)Instructions burned: 115 (million)
% 18.71/3.65 % (2441218)Instruction limit reached!
% 18.71/3.65 % (2441218)------------------------------
% 18.71/3.65 % (2441218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.71/3.65 % (2441218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.71/3.65 % (2441218)CaDiCaL version: 2.1.3
% 18.71/3.65 % (2441218)Termination reason: Instruction limit
% 18.71/3.65 % (2441218)Termination phase: Saturation
% 18.71/3.65 % (2441218)Time elapsed: 0.167 s
% 18.71/3.65 % (2441218)Peak memory usage: 89 MB
% 18.71/3.65 % (2441218)Instructions burned: 180 (million)
% 18.71/3.65 % (2441219)------------------------------
% 18.71/3.65 % (2441219)------------------------------
% 18.71/3.65 % (2441227)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=1653203765:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 18.71/3.65 % (2441228)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3498369333:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 18.71/3.65 % (2441227)Refutation not found, incomplete strategy
% 18.71/3.65 % (2441227)------------------------------
% 18.71/3.65 % (2441227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.71/3.65 % (2441227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.62/5.58 % (2441227)CaDiCaL version: 2.1.3
% 32.62/5.58 % (2441227)Termination reason: Refutation not found, incomplete strategy
% 32.62/5.58 % (2441227)Time elapsed: 0.002 s
% 32.62/5.58 % (2441227)Peak memory usage: 87 MB
% 32.62/5.58 % (2441228)Refutation not found, incomplete strategy
% 32.62/5.58 % (2441228)------------------------------
% 32.62/5.58 % (2441228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.62/5.58 % (2441228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.62/5.58 % (2441228)CaDiCaL version: 2.1.3
% 32.62/5.58 % (2441228)Termination reason: Refutation not found, incomplete strategy
% 32.62/5.58 % (2441228)Time elapsed: 0.002 s
% 32.62/5.58 % (2441228)Peak memory usage: 88 MB
% 32.62/5.58 % (2441228)Instructions burned: 1 (million)
% 32.62/5.58 % (2441230)lrs+10_64_to=lpo:sil=8000:random_seed=2285417480:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 32.62/5.58 % (2441229)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=68279576:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 32.62/5.58 % (2441230)Instruction limit reached!
% 32.62/5.58 % (2441230)------------------------------
% 32.62/5.58 % (2441230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.62/5.58 % (2441230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.62/5.58 % (2441230)CaDiCaL version: 2.1.3
% 32.62/5.58 % (2441230)Termination reason: Instruction limit
% 32.62/5.58 % (2441230)Termination phase: Saturation
% 32.62/5.58 % (2441230)Time elapsed: 0.063 s
% 32.62/5.58 % (2441230)Peak memory usage: 88 MB
% 32.62/5.58 % (2441230)Instructions burned: 128 (million)
% 32.62/5.58 % (2441229)Refutation not found, incomplete strategy
% 32.62/5.58 % (2441229)------------------------------
% 32.62/5.58 % (2441229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.62/5.58 % (2441229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.62/5.58 % (2441229)CaDiCaL version: 2.1.3
% 32.62/5.58 % (2441229)Termination reason: Refutation not found, incomplete strategy
% 32.62/5.58 % (2441229)Time elapsed: 0.002 s
% 32.62/5.58 % (2441229)Peak memory usage: 88 MB
% 32.62/5.58 % (2441235)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3958646587:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 32.62/5.58 % (2441227)------------------------------
% 32.62/5.58 % (2441227)------------------------------
% 32.62/5.58 % (2441228)------------------------------
% 32.62/5.58 % (2441228)------------------------------
% 32.62/5.58 % (2441235)Instruction limit reached!
% 32.62/5.58 % (2441235)------------------------------
% 32.62/5.58 % (2441235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.62/5.58 % (2441235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.62/5.58 % (2441235)CaDiCaL version: 2.1.3
% 32.62/5.58 % (2441235)Termination reason: Instruction limit
% 32.62/5.58 % (2441235)Termination phase: Saturation
% 32.62/5.58 % (2441235)Time elapsed: 0.096 s
% 32.62/5.58 % (2441235)Peak memory usage: 90 MB
% 32.62/5.58 % (2441235)Instructions burned: 196 (million)
% 32.62/5.58 % (2441229)------------------------------
% 32.62/5.58 % (2441229)------------------------------
% 32.62/5.58 % (2441239)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=4131752387:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2988 on theBenchmark for (2988ds/106Mi)
% 32.62/5.58 % (2441237)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3496838187:i=157:gtg=all_2988 on theBenchmark for (2988ds/157Mi)
% 32.62/5.58 % (2441239)Instruction limit reached!
% 32.62/5.58 % (2441239)------------------------------
% 32.62/5.58 % (2441239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.62/5.58 % (2441239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.62/5.58 % (2441239)CaDiCaL version: 2.1.3
% 32.62/5.58 % (2441239)Termination reason: Instruction limit
% 32.62/5.58 % (2441239)Termination phase: Saturation
% 32.62/5.58 % (2441239)Time elapsed: 0.054 s
% 32.62/5.58 % (2441239)Peak memory usage: 89 MB
% 32.62/5.58 % (2441239)Instructions burned: 106 (million)
% 32.62/5.58 % (2441238)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1385101993:i=3394:sd=4:ss=included:sgt=64_2988 on theBenchmark for (2988ds/3394Mi)
% 32.62/5.58 % (2441240)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=150183874:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 58.94/9.24 % (2441240)Refutation not found, incomplete strategy
% 58.94/9.24 % (2441240)------------------------------
% 58.94/9.24 % (2441240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.94/9.24 % (2441240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.94/9.24 % (2441240)CaDiCaL version: 2.1.3
% 58.94/9.24 % (2441240)Termination reason: Refutation not found, incomplete strategy
% 58.94/9.24 % (2441240)Time elapsed: 0.002 s
% 58.94/9.24 % (2441240)Peak memory usage: 87 MB
% 58.94/9.24 % (2441237)Instruction limit reached!
% 58.94/9.24 % (2441237)------------------------------
% 58.94/9.24 % (2441237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.94/9.24 % (2441237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.94/9.24 % (2441237)CaDiCaL version: 2.1.3
% 58.94/9.24 % (2441237)Termination reason: Instruction limit
% 58.94/9.24 % (2441237)Termination phase: Saturation
% 58.94/9.24 % (2441237)Time elapsed: 0.157 s
% 58.94/9.24 % (2441237)Peak memory usage: 90 MB
% 58.94/9.24 % (2441237)Instructions burned: 157 (million)
% 58.94/9.24 % (2441243)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3086818945:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2986 on theBenchmark for (2986ds/242Mi)
% 58.94/9.24 % (2441246)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2608363046:cond=fast:i=5208:av=off_2985 on theBenchmark for (2985ds/5208Mi)
% 58.94/9.24 % (2441243)Instruction limit reached!
% 58.94/9.24 % (2441243)------------------------------
% 58.94/9.24 % (2441243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.94/9.24 % (2441243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.94/9.24 % (2441243)CaDiCaL version: 2.1.3
% 58.94/9.24 % (2441243)Termination reason: Instruction limit
% 58.94/9.24 % (2441243)Termination phase: Saturation
% 58.94/9.24 % (2441243)Time elapsed: 0.122 s
% 58.94/9.24 % (2441243)Peak memory usage: 90 MB
% 58.94/9.24 % (2441243)Instructions burned: 242 (million)
% 58.94/9.24 % (2441240)------------------------------
% 58.94/9.24 % (2441240)------------------------------
% 58.94/9.24 % (2441249)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3417343674:i=134:sd=2:doe=on:ss=axioms:sgt=14_2982 on theBenchmark for (2982ds/134Mi)
% 58.94/9.24 % (2441250)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=115293777:i=499:bd=all_2981 on theBenchmark for (2981ds/499Mi)
% 58.94/9.24 % (2441249)Instruction limit reached!
% 58.94/9.24 % (2441249)------------------------------
% 58.94/9.24 % (2441249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.94/9.24 % (2441249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.94/9.24 % (2441249)CaDiCaL version: 2.1.3
% 58.94/9.24 % (2441249)Termination reason: Instruction limit
% 58.94/9.24 % (2441249)Termination phase: Saturation
% 58.94/9.24 % (2441249)Time elapsed: 0.129 s
% 58.94/9.24 % (2441249)Peak memory usage: 89 MB
% 58.94/9.24 % (2441249)Instructions burned: 134 (million)
% 58.94/9.24 % (2441253)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1810939975:i=191:fgj=on:bd=all_2978 on theBenchmark for (2978ds/191Mi)
% 58.94/9.24 % (2441253)Instruction limit reached!
% 58.94/9.24 % (2441253)------------------------------
% 58.94/9.24 % (2441253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.94/9.24 % (2441253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.94/9.24 % (2441253)CaDiCaL version: 2.1.3
% 58.94/9.24 % (2441253)Termination reason: Instruction limit
% 58.94/9.24 % (2441253)Termination phase: Saturation
% 58.94/9.24 % (2441253)Time elapsed: 0.203 s
% 58.94/9.24 % (2441253)Peak memory usage: 91 MB
% 58.94/9.24 % (2441253)Instructions burned: 192 (million)
% 58.94/9.24 % (2441250)Instruction limit reached!
% 58.94/9.24 % (2441250)------------------------------
% 58.94/9.24 % (2441250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.94/9.24 % (2441250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.94/9.24 % (2441250)CaDiCaL version: 2.1.3
% 58.94/9.24 % (2441250)Termination reason: Instruction limit
% 58.94/9.24 % (2441250)Termination phase: Saturation
% 58.94/9.24 % (2441250)Time elapsed: 0.537 s
% 58.94/9.24 % (2441250)Peak memory usage: 94 MB
% 58.94/9.24 % (2441250)Instructions burned: 499 (million)
% 40.34/11.22 % (2441255)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1807392011:i=264:kws=precedence:fsr=off_2973 on theBenchmark for (2973ds/264Mi)
% 40.34/11.22 % (2441256)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=72195590:cond=on:i=156:bs=on:gtg=exists_all:er=known_2972 on theBenchmark for (2972ds/156Mi)
% 40.34/11.22 % (2441256)Instruction limit reached!
% 40.34/11.22 % (2441256)------------------------------
% 40.34/11.22 % (2441256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.34/11.22 % (2441256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.34/11.22 % (2441256)CaDiCaL version: 2.1.3
% 40.34/11.22 % (2441256)Termination reason: Instruction limit
% 40.34/11.22 % (2441256)Termination phase: Saturation
% 40.34/11.22 % (2441256)Time elapsed: 0.153 s
% 40.34/11.22 % (2441256)Peak memory usage: 89 MB
% 40.34/11.22 % (2441256)Instructions burned: 156 (million)
% 40.34/11.22 % (2441255)Instruction limit reached!
% 40.34/11.22 % (2441255)------------------------------
% 40.34/11.22 % (2441255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.34/11.22 % (2441255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.34/11.22 % (2441255)CaDiCaL version: 2.1.3
% 40.34/11.22 % (2441255)Termination reason: Instruction limit
% 40.34/11.22 % (2441255)Termination phase: Saturation
% 40.34/11.22 % (2441255)Time elapsed: 0.270 s
% 40.34/11.22 % (2441255)Peak memory usage: 91 MB
% 40.34/11.22 % (2441255)Instructions burned: 267 (million)
% 40.34/11.22 % (2441261)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=2743331832:i=3256:kws=precedence:bd=preordered:av=off_2968 on theBenchmark for (2968ds/3256Mi)
% 40.34/11.22 % (2441262)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3460138377:i=537:av=off:ss=included_2968 on theBenchmark for (2968ds/537Mi)
% 40.34/11.22 % (2441238)Instruction limit reached!
% 40.34/11.22 % (2441238)------------------------------
% 40.34/11.22 % (2441238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.34/11.22 % (2441238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.34/11.22 % (2441238)CaDiCaL version: 2.1.3
% 40.34/11.22 % (2441238)Termination reason: Instruction limit
% 40.34/11.22 % (2441238)Termination phase: Saturation
% 40.34/11.22 % (2441238)Time elapsed: 2.210 s
% 40.34/11.22 % (2441238)Peak memory usage: 150 MB
% 40.34/11.22 % (2441238)Instructions burned: 3395 (million)
% 40.34/11.22 % (2441265)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=4083363826:i=180:bd=preordered:av=off_2963 on theBenchmark for (2963ds/180Mi)
% 40.34/11.22 % (2441265)Instruction limit reached!
% 40.34/11.22 % (2441265)------------------------------
% 40.34/11.22 % (2441265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.34/11.22 % (2441265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.34/11.22 % (2441265)CaDiCaL version: 2.1.3
% 40.34/11.22 % (2441265)Termination reason: Instruction limit
% 40.34/11.22 % (2441265)Termination phase: Saturation
% 40.34/11.22 % (2441265)Time elapsed: 0.083 s
% 40.34/11.22 % (2441265)Peak memory usage: 88 MB
% 40.34/11.22 % (2441265)Instructions burned: 181 (million)
% 40.34/11.22 % (2441262)Instruction limit reached!
% 40.34/11.22 % (2441262)------------------------------
% 40.34/11.22 % (2441262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.34/11.22 % (2441262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.34/11.22 % (2441262)CaDiCaL version: 2.1.3
% 40.34/11.22 % (2441262)Termination reason: Instruction limit
% 40.34/11.22 % (2441262)Termination phase: Saturation
% 40.34/11.22 % (2441262)Time elapsed: 0.498 s
% 40.34/11.22 % (2441262)Peak memory usage: 93 MB
% 40.34/11.22 % (2441262)Instructions burned: 538 (million)
% 40.34/11.22 % (2441267)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=143536269:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2960 on theBenchmark for (2960ds/10307Mi)
% 40.34/11.22 % (2441268)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=402206039:i=412:gtgl=4:gtg=exists_all_2960 on theBenchmark for (2960ds/412Mi)
% 40.34/11.22 % (2441268)Instruction limit reached!
% 40.34/11.22 % (2441268)------------------------------
% 40.34/11.22 % (2441268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.34/11.22 % (2441268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.34/11.22 % (2441268)CaDiCaL version: 2.1.3
% 40.34/11.22 % (2441268)Termination reason: Instruction limit
% 40.34/11.22 % (2441268)Termination phase: Saturation
% 40.34/11.22 % (2441268)Time elapsed: 0.406 s
% 40.34/11.22 % (2441268)Peak memory usage: 94 MB
% 40.34/11.22 % (2441268)Instructions burned: 412 (million)
% 40.34/11.22 % (2441271)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=2695606919:s2pl=no:i=8478:s2at=4:nm=6_2953 on theBenchmark for (2953ds/8478Mi)
% 40.34/11.22 % (2441246)Instruction limit reached!
% 40.34/11.22 % (2441246)------------------------------
% 40.34/11.22 % (2441246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.34/11.22 % (2441246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.34/11.22 % (2441246)CaDiCaL version: 2.1.3
% 40.34/11.22 % (2441246)Termination reason: Instruction limit
% 40.34/11.22 % (2441246)Termination phase: Saturation
% 40.34/11.22 % (2441246)Time elapsed: 5.017 s
% 40.34/11.22 % (2441246)Peak memory usage: 169 MB
% 40.34/11.22 % (2441246)Instructions burned: 5209 (million)
% 40.34/11.22 % (2441261)Instruction limit reached!
% 40.34/11.22 % (2441261)------------------------------
% 40.34/11.22 % (2441261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.34/11.22 % (2441261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.34/11.22 % (2441261)CaDiCaL version: 2.1.3
% 40.34/11.22 % (2441261)Termination reason: Instruction limit
% 40.34/11.22 % (2441261)Termination phase: Saturation
% 40.34/11.22 % (2441261)Time elapsed: 3.382 s
% 40.34/11.22 % (2441261)Peak memory usage: 150 MB
% 40.34/11.22 % (2441261)Instructions burned: 3256 (million)
% 40.34/11.22 % (2441273)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=126134416:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2933 on theBenchmark for (2933ds/303Mi)
% 40.34/11.22 % (2441273)Refutation not found, incomplete strategy
% 40.34/11.22 % (2441273)------------------------------
% 40.34/11.22 % (2441273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.34/11.22 % (2441273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.34/11.22 % (2441273)CaDiCaL version: 2.1.3
% 40.34/11.22 % (2441273)Termination reason: Refutation not found, incomplete strategy
% 40.34/11.22 % (2441273)Time elapsed: 0.003 s
% 40.34/11.22 % (2441273)Peak memory usage: 88 MB
% 40.34/11.22 % (2441273)Instructions burned: 1 (million)
% 40.34/11.22 % (2441274)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1204579459:st=4:i=720:sd=3:fsr=off:ss=axioms_2932 on theBenchmark for (2932ds/720Mi)
% 40.34/11.22 % (2441274)Refutation not found, incomplete strategy
% 40.34/11.22 % (2441274)------------------------------
% 40.34/11.22 % (2441274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.34/11.22 % (2441274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.34/11.22 % (2441274)CaDiCaL version: 2.1.3
% 40.34/11.22 % (2441274)Termination reason: Refutation not found, incomplete strategy
% 40.34/11.22 % (2441274)Time elapsed: 0.002 s
% 40.34/11.22 % (2441274)Peak memory usage: 88 MB
% 40.34/11.22 % (2441273)------------------------------
% 40.34/11.22 % (2441273)------------------------------
% 40.34/11.22 % (2441274)------------------------------
% 40.34/11.22 % (2441274)------------------------------
% 40.34/11.22 % (2441279)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=675998722:i=598:bs=on:bd=preordered:av=off:ss=axioms_2926 on theBenchmark for (2926ds/598Mi)
% 40.34/11.22 % (2441280)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2423455030:i=2989:sd=3:ss=axioms:sgt=60_2925 on theBenchmark for (2925ds/2989Mi)
% 40.34/11.22 % (2441279)Instruction limit reached!
% 40.34/11.22 % (2441279)------------------------------
% 40.34/11.22 % (2441279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.34/11.22 % (2441279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.34/11.22 % (2441279)CaDiCaL version: 2.1.3
% 40.34/11.22 % (2441279)Termination reason: Instruction limit
% 40.34/11.22 % (2441279)Termination phase: Saturation
% 40.34/11.22 % (2441279)Time elapsed: 0.605 s
% 40.34/11.22 % (2441279)Peak memory usage: 94 MB
% 40.34/11.22 % (2441279)Instructions burned: 599 (million)
% 40.34/11.22 % (2441283)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=3740113905:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2917 on theBenchmark for (2917ds/1997Mi)
% 40.34/11.22 % (2441215)First to succeed.
% 40.34/11.22 % (2441215)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2441208"
% 40.34/11.22 % (2441267)Also succeeded, but the first one will report.
% 40.34/11.22 % (2441215)Refutation found. Thanks to Tanya!
% 40.34/11.22 % SZS status Unsatisfiable for theBenchmark
% 40.34/11.22 % SZS output start Proof for theBenchmark
% See solution above
% 0.23/11.51 % (2441215)------------------------------
% 0.23/11.51 % (2441215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.23/11.51 % (2441215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/11.51 % (2441215)CaDiCaL version: 2.1.3
% 0.23/11.51 % (2441215)Termination reason: Refutation
% 0.23/11.52 % (2441215)Time elapsed: 9.497 s
% 0.23/11.52 % (2441215)Peak memory usage: 188 MB
% 0.23/11.52 % (2441215)Instructions burned: 9163 (million)
% 0.23/11.52 % (2441215)------------------------------
% 0.23/11.52 % (2441215)------------------------------
% 0.23/11.52 % (2441208)Success in time 10.262 s
% 0.23/11.52 % Vampire exiting
%------------------------------------------------------------------------------