%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT189-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:11 AM UTC 2026
% Result : Unsatisfiable 36.24s 9.73s
% Output : Refutation 62.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 149
% Number of leaves : 12
% Syntax : Number of formulae : 554 ( 524 unt; 0 def)
% Number of atoms : 587 ( 586 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 68 ( 35 ~; 33 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 1347 (1347 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : meet(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_of_meet) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_meet) ).
fof(f8,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f9,axiom,
! [X0] : join(X0,complement(X0)) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement_join) ).
fof(f10,axiom,
! [X0] : meet(X0,complement(X0)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement_meet) ).
fof(f11,axiom,
! [X0,X1] :
( join(X0,X1) != one
| meet(X0,X1) != zero
| complement(X0) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f12,axiom,
! [X2,X0,X1] : meet(X0,join(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_H17) ).
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(f15,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f17,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f22,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f17,f3]) ).
fof(f24,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f22,f6]) ).
fof(f27,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f15,f4]) ).
fof(f28,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f15,f17]) ).
fof(f32,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f28,f5]) ).
fof(f33,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f27,f5]) ).
fof(f35,plain,
! [X2,X0,X1] : meet(X2,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(f36,plain,
! [X2,X0,X1] : meet(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(f42,plain,
! [X2,X0,X1] : meet(X2,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(f46,plain,
! [X2,X0,X1] : meet(X1,join(meet(X1,X0),meet(X1,X2))) = meet(X1,join(meet(X0,join(X1,meet(X0,X2))),meet(X2,join(X0,X1)))),
inference(superposition,[],[f12,f6]) ).
fof(f47,plain,
! [X2,X0,X1] : meet(X0,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(f55,plain,
! [X2,X0,X1] : meet(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(f65,plain,
! [X2,X0,X1] : meet(X0,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,[],[f47,f6]) ).
fof(f66,plain,
! [X2,X0,X1] : meet(X1,join(meet(X1,X0),meet(X1,X2))) = meet(X1,join(meet(X2,join(X0,X1)),meet(X0,join(X1,meet(X0,X2))))),
inference(forward_demodulation,[],[f46,f6]) ).
fof(f70,plain,
! [X2,X0,X1] : meet(X2,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,[],[f42,f6]) ).
fof(f76,plain,
! [X2,X0,X1] : meet(X1,join(meet(X1,X0),meet(X1,join(X0,X2)))) = meet(X1,join(X0,meet(join(X0,X2),join(X1,X0)))),
inference(forward_demodulation,[],[f36,f15]) ).
fof(f77,plain,
! [X2,X0,X1] : meet(X2,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,[],[f35,f6]) ).
fof(f84,plain,
! [X2,X0,X1] : meet(X0,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,[],[f65,f7]) ).
fof(f92,plain,
! [X2,X0,X1] : meet(X0,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,[],[f84,f7]) ).
fof(f98,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,meet(X0,X1)),meet(X0,X2))) = meet(X0,join(meet(X2,X0),meet(X0,meet(X1,X0)))),
inference(forward_demodulation,[],[f92,f4]) ).
fof(f101,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,meet(X0,X1)),meet(X0,X2))) = meet(X0,join(meet(X2,X0),meet(X1,X0))),
inference(forward_demodulation,[],[f98,f32]) ).
fof(f104,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,X2))) = meet(X0,join(meet(X2,X0),meet(X1,X0))),
inference(forward_demodulation,[],[f101,f33]) ).
fof(f114,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)),
inference(superposition,[],[f7,f5]) ).
fof(f115,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f116,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f15]) ).
fof(f126,plain,
! [X2,X0,X1] : meet(X0,X1) = join(meet(X0,X1),meet(X0,meet(X1,X2))),
inference(superposition,[],[f4,f7]) ).
fof(f128,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f131,plain,
! [X2,X3,X0,X1] : meet(X2,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(f132,plain,
! [X2,X3,X0,X1] : meet(X2,join(meet(X2,X3),meet(X2,meet(X0,X1)))) = meet(X2,join(meet(X3,join(X2,meet(X3,meet(X0,X1)))),meet(X0,meet(X1,join(X2,X3))))),
inference(superposition,[],[f12,f7]) ).
fof(f135,plain,
! [X2,X3,X0,X1] : meet(X2,join(meet(X2,X3),meet(X2,meet(X0,X1)))) = meet(X2,join(meet(X0,meet(X1,join(X2,X3))),meet(X3,join(X2,meet(X3,meet(X0,X1)))))),
inference(forward_demodulation,[],[f132,f6]) ).
fof(f136,plain,
! [X2,X3,X0,X1] : meet(X2,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,[],[f131,f6]) ).
fof(f142,plain,
! [X2,X3,X0,X1] : meet(X2,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,[],[f136,f7]) ).
fof(f153,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f8,f4]) ).
fof(f154,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f17]) ).
fof(f164,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f180,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f115,f5]) ).
fof(f182,plain,
! [X2,X0,X1] : meet(X0,join(X0,X1)) = meet(X0,join(X2,join(X0,X1))),
inference(superposition,[],[f115,f15]) ).
fof(f188,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(join(X0,X2),X1),meet(X0,X1)),
inference(superposition,[],[f17,f115]) ).
fof(f192,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(X0,X1),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f188,f6]) ).
fof(f198,plain,
! [X2,X0,X1] : meet(X0,join(X2,join(X0,X1))) = X0,
inference(forward_demodulation,[],[f182,f3]) ).
fof(f214,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f153,f6]) ).
fof(f222,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(meet(X0,X2),X1),join(X0,X1)),
inference(superposition,[],[f15,f153]) ).
fof(f226,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(X0,X1),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f222,f5]) ).
fof(f237,plain,
! [X0,X1] : join(X0,complement(meet(X0,X1))) = join(X0,one),
inference(superposition,[],[f153,f9]) ).
fof(f238,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f241,plain,
! [X0] : complement(X0) = meet(complement(X0),one),
inference(superposition,[],[f15,f9]) ).
fof(f242,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(one,X1)),
inference(superposition,[],[f115,f9]) ).
fof(f243,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f244,plain,
! [X0] : complement(X0) = meet(one,complement(X0)),
inference(forward_demodulation,[],[f241,f5]) ).
fof(f249,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f250,plain,
! [X0,X1] : meet(X0,meet(complement(X0),X1)) = meet(zero,X1),
inference(superposition,[],[f7,f10]) ).
fof(f251,plain,
! [X0,X1] : meet(X0,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(f253,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(zero,X1)),
inference(superposition,[],[f153,f10]) ).
fof(f254,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f271,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f238]) ).
fof(f274,plain,
! [X0] : one = join(one,X0),
inference(superposition,[],[f17,f238]) ).
fof(f289,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f6,f274]) ).
fof(f335,plain,
zero = complement(one),
inference(superposition,[],[f10,f271]) ).
fof(f369,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f249]) ).
fof(f372,plain,
! [X0,X1] : meet(X0,join(meet(X0,zero),meet(X0,X1))) = meet(X0,join(meet(zero,join(X0,meet(zero,X1))),meet(X1,X0))),
inference(superposition,[],[f12,f249]) ).
fof(f373,plain,
! [X0] : zero = meet(zero,X0),
inference(superposition,[],[f15,f249]) ).
fof(f378,plain,
! [X0,X1] : meet(X0,join(meet(X0,zero),meet(X0,X1))) = meet(X0,join(meet(X1,X0),meet(zero,join(X0,meet(zero,X1))))),
inference(forward_demodulation,[],[f372,f6]) ).
fof(f379,plain,
! [X0,X1] : meet(X0,join(meet(X0,zero),meet(X0,X1))) = meet(X0,join(meet(X1,X0),zero)),
inference(forward_demodulation,[],[f378,f373]) ).
fof(f380,plain,
! [X0,X1] : meet(X0,join(meet(X0,zero),meet(X0,X1))) = meet(X0,join(zero,meet(X1,X0))),
inference(forward_demodulation,[],[f379,f6]) ).
fof(f381,plain,
! [X0,X1] : meet(X0,meet(X1,X0)) = meet(X0,join(meet(X0,zero),meet(X0,X1))),
inference(forward_demodulation,[],[f380,f369]) ).
fof(f382,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,join(meet(X0,zero),meet(X0,X1))),
inference(forward_demodulation,[],[f381,f32]) ).
fof(f390,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f5,f373]) ).
fof(f467,plain,
! [X0,X1] : meet(X0,meet(complement(X0),X1)) = meet(X1,zero),
inference(superposition,[],[f128,f10]) ).
fof(f515,plain,
! [X0,X1] : zero = meet(X0,meet(complement(X0),X1)),
inference(forward_demodulation,[],[f467,f390]) ).
fof(f555,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,X2))),
inference(superposition,[],[f116,f5]) ).
fof(f573,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = join(meet(join(X2,X0),X1),meet(X0,X1)),
inference(superposition,[],[f17,f116]) ).
fof(f585,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = join(meet(X0,X1),meet(join(X2,X0),X1)),
inference(forward_demodulation,[],[f573,f6]) ).
fof(f669,plain,
! [X2,X3,X0,X1] : join(meet(join(X2,X0),X1),X3) = join(meet(join(X2,X0),X1),join(meet(X0,X1),X3)),
inference(superposition,[],[f154,f116]) ).
fof(f687,plain,
! [X0,X1] : join(X0,one) = join(X0,complement(meet(X1,X0))),
inference(superposition,[],[f154,f9]) ).
fof(f711,plain,
! [X0,X1] : one = join(X0,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f687,f289]) ).
fof(f720,plain,
! [X2,X3,X0,X1] : join(meet(join(X2,X0),X1),X3) = join(meet(X0,X1),join(X3,meet(join(X2,X0),X1))),
inference(forward_demodulation,[],[f669,f164]) ).
fof(f930,plain,
! [X0,X1] : zero = meet(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f254,f5]) ).
fof(f1049,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,f243]) ).
fof(f1060,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f1049]) ).
fof(f1101,plain,
! [X0,X1] :
( zero != meet(X1,join(X0,complement(join(X0,X1))))
| complement(X1) = join(X0,complement(join(X0,X1))) ),
inference(superposition,[],[f1060,f6]) ).
fof(f1775,plain,
! [X2,X0,X1] : meet(X1,join(meet(X1,X0),meet(X1,join(X2,X0)))) = meet(X1,join(meet(join(X2,X0),join(X1,X0)),meet(X0,join(X1,X0)))),
inference(superposition,[],[f55,f15]) ).
fof(f1858,plain,
! [X2,X0,X1] : meet(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(forward_demodulation,[],[f1775,f6]) ).
fof(f1913,plain,
! [X2,X0,X1] : meet(X1,join(meet(X1,X0),meet(X1,join(X2,X0)))) = meet(X1,meet(join(X2,X0),join(X1,X0))),
inference(forward_demodulation,[],[f1858,f585]) ).
fof(f1957,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(meet(X1,X0),meet(X1,join(X2,X0)))),
inference(forward_demodulation,[],[f1913,f180]) ).
fof(f3060,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,complement(one)))
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(superposition,[],[f1101,f9]) ).
fof(f3089,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,zero))
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f3060,f335]) ).
fof(f3107,plain,
! [X0] :
( zero != meet(complement(X0),X0)
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f3089,f249]) ).
fof(f3119,plain,
! [X0] :
( meet(X0,complement(X0)) != zero
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f3107,f5]) ).
fof(f3128,plain,
! [X0] : join(X0,complement(one)) = complement(complement(X0)),
inference(forward_subsumption_resolution,[],[f3119,f10]) ).
fof(f3135,plain,
! [X0] : join(X0,zero) = complement(complement(X0)),
inference(forward_demodulation,[],[f3128,f335]) ).
fof(f3140,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f3135,f249]) ).
fof(f3772,plain,
! [X0,X1] : meet(complement(meet(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,[],[f70,f9]) ).
fof(f3854,plain,
! [X0,X1] : meet(complement(meet(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,[],[f3772,f6]) ).
fof(f3948,plain,
! [X0,X1] : meet(complement(meet(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,[],[f3854,f6]) ).
fof(f4024,plain,
! [X0,X1] : meet(complement(meet(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,one)))),
inference(forward_demodulation,[],[f3948,f237]) ).
fof(f4083,plain,
! [X0,X1] : meet(complement(meet(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,[],[f4024,f289]) ).
fof(f4128,plain,
! [X0,X1] : meet(complement(meet(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,[],[f4083,f238]) ).
fof(f4166,plain,
! [X0,X1] : meet(complement(meet(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,[],[f4128,f238]) ).
fof(f4201,plain,
! [X0,X1] : meet(complement(meet(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,[],[f4166,f5]) ).
fof(f4228,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(X0,X1))) = meet(complement(meet(X0,X1)),join(meet(complement(meet(X0,X1)),X0),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f4201,f5]) ).
fof(f4250,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(X0,X1))) = meet(complement(meet(X0,X1)),join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f4228,f5]) ).
fof(f4393,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1)))) = join(join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1)))),meet(join(X0,X1),complement(meet(X0,X1)))),
inference(superposition,[],[f17,f4250]) ).
fof(f4418,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1)))) = join(meet(join(X0,X1),complement(meet(X0,X1))),join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f4393,f6]) ).
fof(f4468,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1)))) = join(meet(X1,complement(meet(X0,X1))),join(meet(join(X0,X1),complement(meet(X0,X1))),meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f4418,f164]) ).
fof(f4509,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1)))) = join(meet(X1,complement(meet(X0,X1))),join(meet(X0,complement(meet(X0,X1))),meet(join(X0,X1),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f4468,f6]) ).
fof(f4546,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1)))) = join(meet(join(X0,X1),complement(meet(X0,X1))),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f4509,f720]) ).
fof(f4578,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1)))) = join(meet(X0,complement(meet(X0,X1))),meet(join(X0,X1),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f4546,f6]) ).
fof(f4599,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,[],[f4578,f192]) ).
fof(f4687,plain,
! [X0,X1] : join(X0,meet(X1,complement(meet(X0,X1)))) = join(X0,meet(join(X0,X1),complement(meet(X0,X1)))),
inference(superposition,[],[f153,f4599]) ).
fof(f4964,plain,
! [X0,X1] : join(X1,meet(X0,complement(meet(X1,X0)))) = join(X1,meet(join(X0,X1),complement(meet(X1,X0)))),
inference(superposition,[],[f4687,f6]) ).
fof(f4977,plain,
! [X0,X1] : join(X0,meet(complement(meet(X1,X0)),complement(meet(X0,complement(meet(X1,X0)))))) = join(X0,meet(one,complement(meet(X0,complement(meet(X1,X0)))))),
inference(superposition,[],[f4687,f711]) ).
fof(f5110,plain,
! [X0,X1] : join(X0,meet(complement(meet(X1,X0)),complement(meet(X0,complement(meet(X1,X0)))))) = join(X0,complement(meet(X0,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f4977,f244]) ).
fof(f5163,plain,
! [X0,X1] : join(X0,one) = join(X0,meet(complement(meet(X1,X0)),complement(meet(X0,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f5110,f237]) ).
fof(f5202,plain,
! [X0,X1] : one = join(X0,meet(complement(meet(X1,X0)),complement(meet(X0,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f5163,f289]) ).
fof(f7151,plain,
! [X2,X0,X1] : meet(X1,join(meet(X1,join(X0,X2)),meet(X1,X0))) = meet(X1,join(meet(X0,join(X1,join(X0,X2))),meet(join(X0,X2),join(X1,X0)))),
inference(superposition,[],[f77,f3]) ).
fof(f7304,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(join(X0,X2),join(X1,X0)))) = meet(X1,join(meet(X1,join(X0,X2)),meet(X1,X0))),
inference(forward_demodulation,[],[f7151,f198]) ).
fof(f7404,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(join(X0,X2),join(X1,X0)))) = meet(X1,join(meet(X0,X1),meet(join(X0,X2),X1))),
inference(forward_demodulation,[],[f7304,f104]) ).
fof(f7486,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(join(X0,X2),join(X1,X0)))) = meet(X1,meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f7404,f192]) ).
fof(f7552,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(join(X0,X2),join(X1,X0)))) = meet(join(X0,X2),X1),
inference(forward_demodulation,[],[f7486,f32]) ).
fof(f7825,plain,
! [X0,X1] : meet(complement(X0),join(meet(complement(X0),X0),meet(complement(X0),X1))) = meet(complement(X0),join(meet(X1,one),meet(X0,join(complement(X0),meet(X0,X1))))),
inference(superposition,[],[f66,f9]) ).
fof(f8069,plain,
! [X0,X1] : meet(complement(X0),join(meet(complement(X0),X0),meet(complement(X0),X1))) = meet(complement(X0),join(X1,meet(X0,join(complement(X0),meet(X0,X1))))),
inference(forward_demodulation,[],[f7825,f238]) ).
fof(f8172,plain,
! [X0,X1] : meet(complement(X0),join(meet(X0,complement(X0)),meet(complement(X0),X1))) = meet(complement(X0),join(X1,meet(X0,join(complement(X0),meet(X0,X1))))),
inference(forward_demodulation,[],[f8069,f5]) ).
fof(f8254,plain,
! [X0,X1] : meet(complement(X0),join(zero,meet(complement(X0),X1))) = meet(complement(X0),join(X1,meet(X0,join(complement(X0),meet(X0,X1))))),
inference(forward_demodulation,[],[f8172,f10]) ).
fof(f8320,plain,
! [X0,X1] : meet(complement(X0),meet(complement(X0),X1)) = meet(complement(X0),join(X1,meet(X0,join(complement(X0),meet(X0,X1))))),
inference(forward_demodulation,[],[f8254,f369]) ).
fof(f8376,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X1,meet(X0,join(complement(X0),meet(X0,X1))))),
inference(forward_demodulation,[],[f8320,f33]) ).
fof(f9023,plain,
! [X2,X0,X1] : meet(X1,X0) = join(meet(X1,X0),meet(X0,meet(X1,X2))),
inference(superposition,[],[f4,f114]) ).
fof(f9304,plain,
! [X2,X0,X1] : meet(X2,meet(X1,X0)) = meet(X2,meet(X0,meet(one,X1))),
inference(superposition,[],[f242,f128]) ).
fof(f9316,plain,
! [X2,X0,X1] : meet(X2,join(meet(one,X1),meet(one,join(X0,X1)))) = meet(X2,meet(one,join(X0,X1))),
inference(superposition,[],[f242,f1957]) ).
fof(f9442,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(meet(one,X1),meet(one,join(X0,X1)))),
inference(forward_demodulation,[],[f9316,f242]) ).
fof(f9452,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f9304,f242]) ).
fof(f9480,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(meet(one,X1),join(X0,X1))),
inference(forward_demodulation,[],[f9442,f271]) ).
fof(f9502,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X1,join(meet(one,X1),X0))),
inference(forward_demodulation,[],[f9480,f164]) ).
fof(f9514,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X1,X0)),
inference(forward_demodulation,[],[f9502,f154]) ).
fof(f9569,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,join(X1,X2))) = meet(X3,join(X2,join(X0,X1))),
inference(superposition,[],[f9514,f8]) ).
fof(f9668,plain,
! [X0,X1] : join(X0,X1) = meet(join(X0,X1),join(X1,X0)),
inference(superposition,[],[f1,f9514]) ).
fof(f9671,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X2,X1),X0),
inference(superposition,[],[f5,f9514]) ).
fof(f9683,plain,
! [X2,X3,X0,X1] : meet(X3,meet(X0,join(X1,X2))) = meet(X0,meet(join(X2,X1),X3)),
inference(superposition,[],[f128,f9514]) ).
fof(f9703,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),join(X2,X3)) = meet(X0,meet(X1,join(X3,X2))),
inference(superposition,[],[f7,f9514]) ).
fof(f9721,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,join(X2,X3))) = meet(X0,meet(X1,join(X3,X2))),
inference(forward_demodulation,[],[f9703,f7]) ).
fof(f9863,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(join(X1,X0),X2),
inference(superposition,[],[f5,f9671]) ).
fof(f10132,plain,
! [X2,X3,X0,X1] : meet(X3,meet(X0,join(X1,X2))) = meet(X3,meet(join(X2,X1),X0)),
inference(superposition,[],[f9452,f9514]) ).
fof(f10226,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X2,X1),X0),
inference(superposition,[],[f5,f9452]) ).
fof(f12143,plain,
! [X0,X1] : zero = meet(join(X0,X1),complement(join(X1,X0))),
inference(superposition,[],[f10,f9863]) ).
fof(f12927,plain,
! [X0,X1] : meet(X1,X0) = join(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f126,f32]) ).
fof(f13796,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,join(X2,X3))) = join(meet(X2,meet(X0,X1)),meet(X0,meet(X1,join(X2,X3)))),
inference(superposition,[],[f192,f128]) ).
fof(f14999,plain,
! [X0,X1] : join(complement(meet(X0,X1)),meet(X1,complement(meet(complement(meet(X0,X1)),X1)))) = join(complement(meet(X0,X1)),meet(one,complement(meet(complement(meet(X0,X1)),X1)))),
inference(superposition,[],[f4964,f711]) ).
fof(f15209,plain,
! [X0,X1] : join(complement(meet(X0,X1)),meet(X1,complement(meet(complement(meet(X0,X1)),X1)))) = join(complement(meet(X0,X1)),complement(meet(complement(meet(X0,X1)),X1))),
inference(forward_demodulation,[],[f14999,f244]) ).
fof(f15301,plain,
! [X0,X1] : join(complement(meet(X0,X1)),one) = join(complement(meet(X0,X1)),meet(X1,complement(meet(complement(meet(X0,X1)),X1)))),
inference(forward_demodulation,[],[f15209,f237]) ).
fof(f15371,plain,
! [X0,X1] : join(complement(meet(X0,X1)),one) = join(complement(meet(X0,X1)),meet(X1,complement(meet(X1,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f15301,f5]) ).
fof(f15428,plain,
! [X0,X1] : join(one,complement(meet(X0,X1))) = join(complement(meet(X0,X1)),meet(X1,complement(meet(X1,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f15371,f6]) ).
fof(f15463,plain,
! [X0,X1] : one = join(complement(meet(X0,X1)),meet(X1,complement(meet(X1,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f15428,f274]) ).
fof(f15689,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),meet(X0,X2))),
inference(superposition,[],[f226,f4]) ).
fof(f15690,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X0)) = meet(X0,join(meet(X0,X1),meet(X2,X0))),
inference(superposition,[],[f226,f17]) ).
fof(f16527,plain,
! [X2,X0,X1] : join(X2,join(X1,X0)) = join(X2,join(X0,join(zero,X1))),
inference(superposition,[],[f253,f164]) ).
fof(f16591,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(meet(X2,join(zero,X1)),meet(X2,join(X0,X1)))),
inference(superposition,[],[f1957,f253]) ).
fof(f16630,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = join(meet(X2,join(zero,X1)),meet(X2,join(X0,X1))),
inference(forward_demodulation,[],[f16591,f15689]) ).
fof(f16683,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X2,join(X1,X0)),
inference(forward_demodulation,[],[f16527,f253]) ).
fof(f16697,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = join(meet(X2,X1),meet(X2,join(X0,X1))),
inference(forward_demodulation,[],[f16630,f369]) ).
fof(f16783,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,join(meet(X1,X0),meet(X0,X1))),
inference(superposition,[],[f16683,f12927]) ).
fof(f16887,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X2,X1),X0),
inference(superposition,[],[f6,f16683]) ).
fof(f17008,plain,
! [X2,X0,X1] : join(X2,meet(X1,X0)) = join(X2,meet(X0,X1)),
inference(forward_demodulation,[],[f16783,f12927]) ).
fof(f17574,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,meet(X1,X2))) = join(X3,meet(X0,meet(X2,X1))),
inference(superposition,[],[f17008,f10226]) ).
fof(f17576,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,meet(X1,X2))) = join(X3,meet(X2,meet(X0,X1))),
inference(superposition,[],[f17008,f7]) ).
fof(f17579,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,join(X1,X2))) = join(X3,meet(X0,join(X2,X1))),
inference(superposition,[],[f17008,f9671]) ).
fof(f17684,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(X2,X1),X0),
inference(superposition,[],[f6,f17008]) ).
fof(f17722,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,meet(X1,X2))) = meet(X3,join(meet(X2,X1),X0)),
inference(superposition,[],[f9514,f17008]) ).
fof(f17997,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X2,X3)) = join(meet(X1,X0),meet(X3,X2)),
inference(superposition,[],[f17684,f17684]) ).
fof(f18019,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X1,X0),X2),
inference(superposition,[],[f6,f17684]) ).
fof(f18057,plain,
! [X2,X3,X0,X1] : meet(X3,join(meet(X0,X1),X2)) = meet(X3,join(meet(X1,X0),X2)),
inference(superposition,[],[f9514,f17684]) ).
fof(f18129,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,meet(X1,X2))) = meet(X3,join(X0,meet(X2,X1))),
inference(superposition,[],[f9514,f17684]) ).
fof(f20573,plain,
! [X2,X3,X0,X1] : join(meet(X0,meet(X1,X2)),X3) = join(meet(X2,meet(X0,X1)),X3),
inference(superposition,[],[f18019,f7]) ).
fof(f20842,plain,
! [X0,X1] : one = join(meet(X0,X1),complement(meet(X1,X0))),
inference(superposition,[],[f9,f18019]) ).
fof(f21973,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,join(X1,X2))) = meet(X3,join(X0,join(X2,X1))),
inference(superposition,[],[f9514,f16887]) ).
fof(f22449,plain,
! [X0,X1] : meet(X0,join(meet(X0,complement(meet(X1,X0))),meet(X0,complement(complement(meet(X1,X0)))))) = meet(X0,join(meet(complement(meet(X1,X0)),join(X0,zero)),meet(complement(complement(meet(X1,X0))),one))),
inference(superposition,[],[f251,f711]) ).
fof(f22661,plain,
! [X0,X1] : meet(X0,join(meet(X0,complement(meet(X1,X0))),meet(X0,complement(complement(meet(X1,X0)))))) = meet(X0,join(meet(complement(complement(meet(X1,X0))),one),meet(join(X0,zero),complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f22449,f17722]) ).
fof(f22817,plain,
! [X0,X1] : meet(X0,join(meet(X0,complement(meet(X1,X0))),meet(X0,complement(complement(meet(X1,X0)))))) = meet(X0,join(meet(one,complement(complement(meet(X1,X0)))),meet(join(X0,zero),complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f22661,f18057]) ).
fof(f22954,plain,
! [X0,X1] : meet(X0,join(meet(X0,complement(meet(X1,X0))),meet(X0,complement(complement(meet(X1,X0)))))) = meet(X0,join(meet(one,complement(complement(meet(X1,X0)))),meet(X0,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f22817,f249]) ).
fof(f23064,plain,
! [X0,X1] : meet(X0,join(meet(X0,complement(meet(X1,X0))),meet(X0,complement(complement(meet(X1,X0)))))) = meet(X0,join(complement(complement(meet(X1,X0))),meet(X0,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f22954,f244]) ).
fof(f23152,plain,
! [X0,X1] : meet(X0,join(meet(X0,complement(meet(X1,X0))),meet(X0,meet(X1,X0)))) = meet(X0,join(meet(X1,X0),meet(X0,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f23064,f3140]) ).
fof(f23223,plain,
! [X0,X1] : meet(X0,join(meet(X1,X0),meet(X0,complement(meet(X1,X0))))) = meet(X0,join(meet(X0,meet(X1,X0)),meet(complement(meet(X1,X0)),X0))),
inference(forward_demodulation,[],[f23152,f17722]) ).
fof(f23282,plain,
! [X0,X1] : meet(X0,join(meet(X1,X0),meet(X0,complement(meet(X1,X0))))) = join(meet(X0,meet(X1,X0)),meet(complement(meet(X1,X0)),X0)),
inference(forward_demodulation,[],[f23223,f15690]) ).
fof(f23332,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,[],[f23282,f17008]) ).
fof(f23372,plain,
! [X0,X1] : join(meet(X1,X0),meet(X0,complement(meet(X1,X0)))) = meet(X0,join(meet(X1,X0),meet(X0,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f23332,f32]) ).
fof(f25182,plain,
! [X0,X1] : meet(complement(X1),join(meet(X0,X1),meet(X1,complement(meet(X0,X1))))) = meet(complement(X1),join(join(meet(X0,X1),meet(X1,complement(meet(X0,X1)))),meet(X1,join(complement(X1),join(meet(X0,X1),meet(X1,complement(meet(X0,X1)))))))),
inference(superposition,[],[f8376,f23372]) ).
fof(f25187,plain,
! [X2,X0,X1] : meet(X1,join(X2,join(meet(X0,X1),meet(X1,complement(meet(X0,X1)))))) = join(join(meet(X0,X1),meet(X1,complement(meet(X0,X1)))),meet(X1,join(X2,join(meet(X0,X1),meet(X1,complement(meet(X0,X1))))))),
inference(superposition,[],[f16697,f23372]) ).
fof(f25213,plain,
! [X2,X0,X1] : meet(X1,join(X2,join(meet(X0,X1),meet(X1,complement(meet(X0,X1)))))) = join(meet(X0,X1),join(meet(X1,complement(meet(X0,X1))),meet(X1,join(X2,join(meet(X0,X1),meet(X1,complement(meet(X0,X1)))))))),
inference(forward_demodulation,[],[f25187,f8]) ).
fof(f25217,plain,
! [X0,X1] : meet(complement(X1),join(meet(X0,X1),meet(X1,complement(meet(X0,X1))))) = meet(complement(X1),join(meet(X0,X1),join(meet(X1,complement(meet(X0,X1))),meet(X1,join(complement(X1),join(meet(X0,X1),meet(X1,complement(meet(X0,X1))))))))),
inference(forward_demodulation,[],[f25182,f8]) ).
fof(f25323,plain,
! [X0,X1] : meet(complement(X1),join(meet(X0,X1),meet(X1,complement(meet(X0,X1))))) = meet(complement(X1),meet(X1,join(complement(X1),join(meet(X0,X1),meet(X1,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f25217,f25213]) ).
fof(f25401,plain,
! [X0,X1] : meet(complement(X1),join(meet(X0,X1),meet(X1,complement(meet(X0,X1))))) = meet(X1,meet(join(join(meet(X0,X1),meet(X1,complement(meet(X0,X1)))),complement(X1)),complement(X1))),
inference(forward_demodulation,[],[f25323,f9683]) ).
fof(f25460,plain,
! [X0,X1] : meet(complement(X1),join(meet(X0,X1),meet(X1,complement(meet(X0,X1))))) = meet(X1,meet(complement(X1),join(join(meet(X0,X1),meet(X1,complement(meet(X0,X1)))),complement(X1)))),
inference(forward_demodulation,[],[f25401,f9452]) ).
fof(f25509,plain,
! [X0,X1] : meet(complement(X1),join(meet(X0,X1),meet(X1,complement(meet(X0,X1))))) = meet(X1,meet(complement(X1),join(complement(X1),join(meet(X0,X1),meet(X1,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f25460,f9721]) ).
fof(f25551,plain,
! [X0,X1] : meet(complement(X1),join(meet(X0,X1),meet(X1,complement(meet(X0,X1))))) = meet(zero,join(complement(X1),join(meet(X0,X1),meet(X1,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f25509,f250]) ).
fof(f25580,plain,
! [X0,X1] : zero = meet(complement(X1),join(meet(X0,X1),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f25551,f373]) ).
fof(f25724,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X0,meet(X0,X1)),meet(X0,meet(X2,X3)))) = meet(X0,join(meet(X2,meet(X3,X0)),meet(meet(X0,X1),join(X0,meet(meet(X0,X1),meet(X2,X3)))))),
inference(superposition,[],[f135,f4]) ).
fof(f26338,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X0,meet(X0,X1)),meet(X0,meet(X2,X3)))) = meet(X0,join(meet(X2,meet(X3,X0)),meet(X0,meet(X1,join(X0,meet(meet(X0,X1),meet(X2,X3))))))),
inference(forward_demodulation,[],[f25724,f7]) ).
fof(f26551,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X0,meet(X0,X1)),meet(X0,meet(X2,X3)))) = meet(X0,join(meet(X2,meet(X3,X0)),meet(X0,X1))),
inference(forward_demodulation,[],[f26338,f180]) ).
fof(f26719,plain,
! [X2,X3,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,meet(X2,X3))) = meet(X0,join(meet(X2,meet(X3,X0)),meet(X0,X1))),
inference(forward_demodulation,[],[f26551,f15689]) ).
fof(f26830,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X0,meet(X2,X3))) = meet(X0,join(meet(X2,meet(X3,X0)),meet(X0,X1))),
inference(forward_demodulation,[],[f26719,f33]) ).
fof(f27542,plain,
! [X2,X0,X1] : meet(X0,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(superposition,[],[f142,f4]) ).
fof(f27757,plain,
! [X2,X0,X1] : meet(meet(X2,join(X0,meet(X0,X1))),join(meet(meet(X2,join(X0,meet(X0,X1))),X0),meet(meet(X2,join(X0,meet(X0,X1))),meet(X1,join(X0,meet(X0,meet(X1,X2))))))) = meet(meet(X2,join(X0,meet(X0,X1))),join(meet(X0,join(meet(X0,meet(X0,X1)),meet(X0,X2))),meet(meet(X1,join(X0,meet(X0,meet(X1,X2)))),join(meet(X2,join(X0,meet(X0,X1))),X0)))),
inference(superposition,[],[f12,f142]) ).
fof(f27902,plain,
! [X2,X0,X1] : meet(meet(X2,join(X0,meet(X0,X1))),join(meet(meet(X2,join(X0,meet(X0,X1))),X0),meet(meet(X2,join(X0,meet(X0,X1))),meet(X1,join(X0,meet(X0,meet(X1,X2))))))) = meet(X2,meet(join(X0,meet(X0,X1)),join(meet(X0,join(meet(X0,meet(X0,X1)),meet(X0,X2))),meet(meet(X1,join(X0,meet(X0,meet(X1,X2)))),join(meet(X2,join(X0,meet(X0,X1))),X0))))),
inference(forward_demodulation,[],[f27757,f7]) ).
fof(f28102,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,meet(X0,X1)),meet(X0,X2))) = meet(X0,join(meet(X2,X0),meet(X0,X1))),
inference(forward_demodulation,[],[f27542,f180]) ).
fof(f28228,plain,
! [X2,X0,X1] : meet(meet(X2,join(X0,meet(X0,X1))),join(meet(meet(X2,join(X0,meet(X0,X1))),X0),meet(meet(X2,join(X0,meet(X0,X1))),meet(X1,join(X0,meet(X0,meet(X1,X2))))))) = meet(X2,meet(join(X0,meet(X0,X1)),join(meet(X0,join(meet(X0,meet(X0,X1)),meet(X0,X2))),meet(meet(X1,join(X0,meet(X0,meet(X1,X2)))),join(X0,meet(X2,join(X0,meet(X0,X1)))))))),
inference(forward_demodulation,[],[f27902,f17579]) ).
fof(f28384,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,[],[f28102,f15689]) ).
fof(f28490,plain,
! [X2,X0,X1] : meet(meet(X2,join(X0,meet(X0,X1))),join(meet(meet(X2,join(X0,meet(X0,X1))),X0),meet(meet(X2,join(X0,meet(X0,X1))),meet(X1,join(X0,meet(X0,meet(X1,X2))))))) = meet(X2,meet(join(X0,meet(X0,X1)),join(meet(X0,join(meet(X0,meet(X0,X1)),meet(X0,X2))),meet(X1,meet(join(X0,meet(X0,meet(X1,X2))),join(X0,meet(X2,join(X0,meet(X0,X1))))))))),
inference(forward_demodulation,[],[f28228,f7]) ).
fof(f28601,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X0,X1))),
inference(forward_demodulation,[],[f28384,f33]) ).
fof(f28676,plain,
! [X2,X0,X1] : meet(meet(X2,X0),join(meet(meet(X2,X0),X0),meet(meet(X2,X0),meet(X1,join(X0,meet(X0,meet(X1,X2))))))) = meet(X2,meet(X0,join(meet(X0,join(meet(X0,meet(X0,X1)),meet(X0,X2))),meet(X1,meet(join(X0,meet(X0,meet(X1,X2))),join(X0,meet(X2,X0))))))),
inference(forward_demodulation,[],[f28490,f4]) ).
fof(f28819,plain,
! [X2,X0,X1] : meet(meet(X2,X0),join(meet(meet(X2,X0),X0),meet(meet(X2,X0),meet(X1,join(X0,meet(X0,meet(X1,X2))))))) = meet(X2,meet(X0,join(meet(X0,join(meet(X0,meet(X0,X1)),meet(X0,X2))),meet(X1,meet(join(X0,meet(X2,X0)),join(X0,meet(X0,meet(X1,X2)))))))),
inference(forward_demodulation,[],[f28676,f17574]) ).
fof(f28918,plain,
! [X2,X0,X1] : meet(meet(X2,X0),join(meet(meet(X2,X0),X0),meet(meet(X2,X0),meet(X1,X0)))) = meet(X2,meet(X0,join(meet(X0,join(meet(X0,meet(X0,X1)),meet(X0,X2))),meet(X1,meet(join(X0,meet(X2,X0)),X0))))),
inference(forward_demodulation,[],[f28819,f4]) ).
fof(f29004,plain,
! [X2,X0,X1] : meet(meet(X2,X0),join(meet(meet(X2,X0),X0),meet(meet(X2,X0),meet(X1,X0)))) = meet(X2,meet(X0,join(meet(X1,meet(join(X0,meet(X2,X0)),X0)),meet(X0,join(meet(X0,meet(X0,X1)),meet(X0,X2)))))),
inference(forward_demodulation,[],[f28918,f9721]) ).
fof(f29074,plain,
! [X2,X0,X1] : meet(meet(X2,X0),join(meet(meet(X2,X0),X0),meet(meet(X2,X0),meet(X1,X0)))) = meet(X2,join(meet(X0,join(meet(X0,meet(X0,X1)),meet(X0,X2))),meet(X0,meet(X1,join(X0,meet(X2,X0)))))),
inference(forward_demodulation,[],[f29004,f26830]) ).
fof(f29128,plain,
! [X2,X0,X1] : meet(meet(X2,X0),join(meet(meet(X2,X0),X0),meet(meet(X2,X0),meet(X1,X0)))) = meet(X2,join(meet(X0,meet(X1,join(X0,meet(X2,X0)))),meet(join(meet(X0,meet(X0,X1)),meet(X0,X2)),X0))),
inference(forward_demodulation,[],[f29074,f17722]) ).
fof(f29179,plain,
! [X2,X0,X1] : meet(meet(X2,X0),join(meet(meet(X2,X0),X0),meet(meet(X2,X0),meet(X1,X0)))) = meet(X2,join(meet(X0,meet(X1,join(X0,meet(X2,X0)))),meet(X0,join(meet(X0,meet(X0,X1)),meet(X0,X2))))),
inference(forward_demodulation,[],[f29128,f18129]) ).
fof(f29222,plain,
! [X2,X0,X1] : meet(meet(X2,X0),join(meet(meet(X2,X0),X0),meet(meet(X2,X0),meet(X1,X0)))) = meet(X2,join(meet(X0,meet(X1,join(X0,meet(X2,X0)))),join(meet(X0,meet(X0,X1)),meet(X0,X2)))),
inference(forward_demodulation,[],[f29179,f15689]) ).
fof(f29262,plain,
! [X2,X0,X1] : meet(meet(X2,X0),join(meet(meet(X2,X0),X0),meet(meet(X2,X0),meet(X1,X0)))) = meet(X2,join(meet(X0,X2),join(meet(X0,meet(X1,join(X0,meet(X2,X0)))),meet(X0,meet(X0,X1))))),
inference(forward_demodulation,[],[f29222,f9569]) ).
fof(f29298,plain,
! [X2,X0,X1] : meet(meet(X2,X0),join(meet(meet(X2,X0),X0),meet(meet(X2,X0),meet(X1,X0)))) = meet(X2,join(meet(X0,X2),join(meet(X0,meet(X0,X1)),meet(X0,meet(X1,join(X0,meet(X2,X0))))))),
inference(forward_demodulation,[],[f29262,f21973]) ).
fof(f29334,plain,
! [X2,X0,X1] : meet(meet(X2,X0),join(meet(meet(X2,X0),X0),meet(meet(X2,X0),meet(X1,X0)))) = meet(X2,join(meet(X0,X2),meet(X0,meet(X1,join(X0,meet(X2,X0)))))),
inference(forward_demodulation,[],[f29298,f13796]) ).
fof(f29368,plain,
! [X2,X0,X1] : meet(meet(X2,X0),join(meet(meet(X2,X0),X0),meet(meet(X2,X0),meet(X1,X0)))) = meet(X2,join(meet(X0,X2),meet(X0,X1))),
inference(forward_demodulation,[],[f29334,f180]) ).
fof(f29400,plain,
! [X2,X0,X1] : meet(X2,join(meet(X0,X2),meet(X0,X1))) = meet(meet(X2,X0),join(meet(X0,meet(X2,X0)),meet(meet(X2,X0),meet(X1,X0)))),
inference(forward_demodulation,[],[f29368,f18057]) ).
fof(f29428,plain,
! [X2,X0,X1] : join(meet(meet(X2,X0),meet(X1,X0)),meet(meet(X2,X0),X0)) = meet(X2,join(meet(X0,X2),meet(X0,X1))),
inference(forward_demodulation,[],[f29400,f28601]) ).
fof(f29454,plain,
! [X2,X0,X1] : join(meet(meet(X2,X0),X0),meet(meet(X2,X0),meet(X1,X0))) = meet(X2,join(meet(X0,X2),meet(X0,X1))),
inference(forward_demodulation,[],[f29428,f6]) ).
fof(f29476,plain,
! [X2,X0,X1] : meet(X2,join(meet(X0,X2),meet(X0,X1))) = join(meet(meet(X2,X0),X0),meet(X0,meet(meet(X2,X0),X1))),
inference(forward_demodulation,[],[f29454,f17576]) ).
fof(f29492,plain,
! [X2,X0,X1] : meet(meet(X2,X0),X0) = meet(X2,join(meet(X0,X2),meet(X0,X1))),
inference(forward_demodulation,[],[f29476,f9023]) ).
fof(f29505,plain,
! [X2,X0,X1] : meet(X0,meet(X2,X0)) = meet(X2,join(meet(X0,X2),meet(X0,X1))),
inference(forward_demodulation,[],[f29492,f5]) ).
fof(f29517,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,join(meet(X0,X2),meet(X0,X1))),
inference(forward_demodulation,[],[f29505,f32]) ).
fof(f38019,plain,
! [X0,X1] :
( one != one
| zero != meet(meet(X0,X1),complement(meet(X1,X0)))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(superposition,[],[f11,f20842]) ).
fof(f38068,plain,
! [X0,X1] :
( zero != meet(meet(X0,X1),complement(meet(X1,X0)))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(trivial_inequality_removal,[],[f38019]) ).
fof(f38108,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,complement(meet(X1,X0))))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(forward_demodulation,[],[f38068,f7]) ).
fof(f38248,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(forward_subsumption_resolution,[],[f38108,f930]) ).
fof(f38649,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(meet(join(X1,X0),join(X0,X1))),
inference(superposition,[],[f38248,f9668]) ).
fof(f38740,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f38649,f9668]) ).
fof(f45829,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X1,X0)),complement(meet(X0,complement(meet(X1,X0))))),
inference(unit_resulting_resolution,[],[f11,f254,f5202]) ).
fof(f53760,plain,
! [X2,X0,X1] : meet(X2,join(meet(X2,X1),meet(join(X0,X1),X2))) = meet(X2,join(X1,meet(join(X1,X0),join(X2,X1)))),
inference(superposition,[],[f76,f9671]) ).
fof(f53762,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X2),meet(X0,join(X1,X2)))) = meet(X0,join(X2,meet(join(X2,X1),join(X0,X2)))),
inference(superposition,[],[f76,f9514]) ).
fof(f54544,plain,
! [X2,X0,X1] : meet(join(X2,X1),X0) = meet(X0,join(meet(X0,X2),meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f53762,f7552]) ).
fof(f54546,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = meet(X2,join(meet(X2,X1),meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f53760,f7552]) ).
fof(f54893,plain,
! [X2,X0,X1] : meet(join(X2,X1),X0) = join(meet(X0,X2),meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f54544,f15689]) ).
fof(f54895,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = join(meet(X2,X1),meet(join(X0,X1),X2)),
inference(forward_demodulation,[],[f54546,f15690]) ).
fof(f58316,plain,
! [X2,X0,X1] : meet(join(X1,X0),meet(one,X2)) = join(meet(meet(one,X2),X1),meet(join(X0,X1),X2)),
inference(superposition,[],[f54895,f242]) ).
fof(f58591,plain,
! [X2,X0,X1] : meet(join(X1,X0),meet(one,X2)) = join(meet(one,meet(X2,X1)),meet(join(X0,X1),X2)),
inference(forward_demodulation,[],[f58316,f7]) ).
fof(f58828,plain,
! [X2,X0,X1] : join(meet(X2,X1),meet(join(X0,X1),X2)) = meet(join(X1,X0),meet(one,X2)),
inference(forward_demodulation,[],[f58591,f271]) ).
fof(f59031,plain,
! [X2,X0,X1] : join(meet(X2,X1),meet(join(X0,X1),X2)) = meet(one,meet(X2,join(X1,X0))),
inference(forward_demodulation,[],[f58828,f128]) ).
fof(f59186,plain,
! [X2,X0,X1] : meet(X2,join(X1,X0)) = join(meet(X2,X1),meet(join(X0,X1),X2)),
inference(forward_demodulation,[],[f59031,f271]) ).
fof(f59730,plain,
! [X2,X0,X1] : meet(X1,join(meet(X2,X0),X0)) = join(meet(X1,meet(X2,X0)),meet(X0,X1)),
inference(superposition,[],[f59186,f17]) ).
fof(f60157,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,meet(X2,X0))) = meet(X1,join(meet(X2,X0),X0)),
inference(forward_demodulation,[],[f59730,f6]) ).
fof(f60390,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,meet(X2,X0))) = meet(X1,join(X0,meet(X0,X2))),
inference(forward_demodulation,[],[f60157,f17722]) ).
fof(f60578,plain,
! [X2,X0,X1] : meet(X1,X0) = join(meet(X0,X1),meet(X1,meet(X2,X0))),
inference(forward_demodulation,[],[f60390,f4]) ).
fof(f64745,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(meet(complement(meet(X0,X1)),X1),meet(complement(meet(X0,X1)),complement(meet(X1,complement(meet(X0,X1))))))) = meet(complement(meet(X0,X1)),join(meet(complement(meet(X1,complement(meet(X0,X1)))),join(X1,complement(meet(X0,X1)))),meet(X1,one))),
inference(superposition,[],[f66,f15463]) ).
fof(f64880,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(meet(complement(meet(X0,X1)),X1),meet(complement(meet(X0,X1)),complement(meet(X1,complement(meet(X0,X1))))))) = meet(complement(meet(X0,X1)),join(meet(X1,one),meet(join(X1,complement(meet(X0,X1))),complement(meet(X1,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f64745,f17722]) ).
fof(f65019,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(meet(complement(meet(X0,X1)),X1),meet(complement(meet(X0,X1)),complement(meet(X1,complement(meet(X0,X1))))))) = meet(complement(meet(X0,X1)),join(meet(X1,one),meet(one,complement(meet(X1,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f64880,f711]) ).
fof(f65123,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(meet(complement(meet(X0,X1)),X1),meet(complement(meet(X0,X1)),complement(meet(X1,complement(meet(X0,X1))))))) = meet(complement(meet(X0,X1)),join(meet(X1,one),complement(meet(X1,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f65019,f244]) ).
fof(f65203,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(meet(complement(meet(X0,X1)),X1),meet(complement(meet(X0,X1)),complement(meet(X1,complement(meet(X0,X1))))))) = meet(complement(meet(X0,X1)),join(X1,complement(meet(X1,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f65123,f238]) ).
fof(f65267,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(meet(complement(meet(X0,X1)),X1),meet(complement(meet(X0,X1)),complement(meet(X1,complement(meet(X0,X1))))))) = meet(complement(meet(X0,X1)),join(X1,one)),
inference(forward_demodulation,[],[f65203,f237]) ).
fof(f65313,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(meet(complement(meet(X0,X1)),X1),meet(complement(meet(X0,X1)),complement(meet(X1,complement(meet(X0,X1))))))) = meet(join(one,X1),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f65267,f9671]) ).
fof(f65349,plain,
! [X0,X1] : meet(one,complement(meet(X0,X1))) = meet(complement(meet(X0,X1)),join(meet(complement(meet(X0,X1)),X1),meet(complement(meet(X0,X1)),complement(meet(X1,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f65313,f274]) ).
fof(f65382,plain,
! [X0,X1] : meet(one,complement(meet(X0,X1))) = meet(complement(meet(X0,X1)),join(meet(X1,complement(meet(X0,X1))),meet(complement(meet(X0,X1)),complement(meet(X1,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f65349,f18057]) ).
fof(f65412,plain,
! [X0,X1] : meet(one,complement(meet(X0,X1))) = join(meet(complement(meet(X0,X1)),complement(meet(X1,complement(meet(X0,X1))))),meet(complement(meet(X0,X1)),X1)),
inference(forward_demodulation,[],[f65382,f28601]) ).
fof(f65438,plain,
! [X0,X1] : meet(one,complement(meet(X0,X1))) = join(meet(complement(meet(X0,X1)),X1),meet(complement(meet(X0,X1)),complement(meet(X1,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f65412,f6]) ).
fof(f65455,plain,
! [X0,X1] : meet(one,complement(meet(X0,X1))) = join(meet(X1,complement(meet(X0,X1))),meet(complement(meet(X1,complement(meet(X0,X1)))),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f65438,f17997]) ).
fof(f65469,plain,
! [X0,X1] : meet(one,complement(meet(X0,X1))) = join(meet(X1,complement(meet(X0,X1))),meet(complement(meet(X0,X1)),complement(meet(X1,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f65455,f17008]) ).
fof(f65480,plain,
! [X0,X1] : meet(one,complement(meet(X0,X1))) = join(meet(X1,complement(meet(X0,X1))),complement(X1)),
inference(forward_demodulation,[],[f65469,f45829]) ).
fof(f65491,plain,
! [X0,X1] : meet(one,complement(meet(X0,X1))) = join(complement(X1),meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f65480,f6]) ).
fof(f65502,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X1),meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f65491,f244]) ).
fof(f65546,plain,
! [X0,X1] : complement(meet(X1,complement(X0))) = join(X0,meet(complement(X0),complement(meet(X1,complement(X0))))),
inference(superposition,[],[f65502,f3140]) ).
fof(f65655,plain,
! [X0,X1] : complement(X1) = meet(complement(X1),complement(meet(X0,X1))),
inference(superposition,[],[f3,f65502]) ).
fof(f65689,plain,
! [X0,X1] :
( zero != meet(complement(X1),join(meet(X1,complement(meet(X0,X1))),complement(complement(meet(X0,X1)))))
| complement(complement(X1)) = join(meet(X1,complement(meet(X0,X1))),complement(complement(meet(X0,X1)))) ),
inference(superposition,[],[f1060,f65502]) ).
fof(f65746,plain,
! [X0,X1] :
( zero != meet(complement(X1),join(complement(complement(meet(X0,X1))),meet(complement(meet(X0,X1)),X1)))
| complement(complement(X1)) = join(meet(X1,complement(meet(X0,X1))),complement(complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f65689,f17722]) ).
fof(f65871,plain,
! [X0,X1] :
( zero != meet(complement(X1),join(complement(complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1)))))
| complement(complement(X1)) = join(meet(X1,complement(meet(X0,X1))),complement(complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f65746,f18129]) ).
fof(f65967,plain,
! [X0,X1] :
( zero != meet(complement(X1),join(meet(X0,X1),meet(X1,complement(meet(X0,X1)))))
| complement(complement(X1)) = join(meet(X1,complement(meet(X0,X1))),complement(complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f65871,f3140]) ).
fof(f66031,plain,
! [X0,X1] : complement(complement(X1)) = join(meet(X1,complement(meet(X0,X1))),complement(complement(meet(X0,X1)))),
inference(forward_subsumption_resolution,[],[f65967,f25580]) ).
fof(f66076,plain,
! [X0,X1] : complement(complement(X1)) = join(complement(complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f66031,f6]) ).
fof(f66109,plain,
! [X0,X1] : complement(complement(X1)) = join(meet(X0,X1),meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f66076,f3140]) ).
fof(f66137,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,complement(meet(X0,X1)))) = X1,
inference(forward_demodulation,[],[f66109,f3140]) ).
fof(f66296,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f65655,f3]) ).
fof(f66297,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f65655,f15]) ).
fof(f66305,plain,
! [X0,X1] : complement(join(meet(X1,zero),meet(X1,X0))) = meet(complement(join(meet(X1,zero),meet(X1,X0))),complement(meet(X0,X1))),
inference(superposition,[],[f65655,f382]) ).
fof(f66352,plain,
! [X0,X1] : complement(X0) = meet(complement(X0),complement(meet(X0,X1))),
inference(superposition,[],[f65655,f38248]) ).
fof(f66387,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),X2) = join(complement(meet(X1,X0)),join(complement(X0),X2)),
inference(superposition,[],[f154,f65655]) ).
fof(f66499,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),X2) = join(complement(X0),join(X2,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f66387,f164]) ).
fof(f66553,plain,
! [X0,X1] : complement(join(meet(X1,zero),meet(X1,X0))) = meet(complement(meet(X0,X1)),complement(join(meet(X1,zero),meet(X1,X0)))),
inference(forward_demodulation,[],[f66305,f5]) ).
fof(f66558,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f66297,f5]) ).
fof(f66559,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f66296,f5]) ).
fof(f66651,plain,
! [X0,X1] : complement(join(zero,meet(X1,X0))) = meet(complement(meet(X0,X1)),complement(join(zero,meet(X1,X0)))),
inference(forward_demodulation,[],[f66553,f390]) ).
fof(f66702,plain,
! [X0,X1] : complement(meet(X1,X0)) = meet(complement(meet(X0,X1)),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f66651,f369]) ).
fof(f66891,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),complement(X0)),
inference(superposition,[],[f17,f66352]) ).
fof(f66973,plain,
! [X0,X1] : complement(complement(X0)) = join(complement(complement(meet(X0,X1))),meet(complement(meet(X0,X1)),complement(complement(X0)))),
inference(superposition,[],[f65502,f66352]) ).
fof(f66976,plain,
! [X0,X1] : complement(complement(X0)) = join(complement(complement(meet(X0,X1))),meet(complement(complement(X0)),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f66973,f17008]) ).
fof(f67039,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f66891,f6]) ).
fof(f67070,plain,
! [X0,X1] : join(complement(complement(meet(X0,X1))),meet(X0,complement(meet(X0,X1)))) = X0,
inference(forward_demodulation,[],[f66976,f3140]) ).
fof(f67132,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = X0,
inference(forward_demodulation,[],[f67070,f3140]) ).
fof(f67542,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),X1))),
inference(superposition,[],[f66559,f3140]) ).
fof(f67627,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f4,f66559]) ).
fof(f67652,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(X0),join(X2,complement(join(X0,X1)))),
inference(superposition,[],[f214,f66559]) ).
fof(f68283,plain,
! [X0,X1] : complement(join(X1,complement(X0))) = meet(X0,complement(join(X1,complement(X0)))),
inference(superposition,[],[f66558,f3140]) ).
fof(f68372,plain,
! [X0,X1] : complement(X1) = join(complement(X1),complement(join(X0,X1))),
inference(superposition,[],[f4,f66558]) ).
fof(f68817,plain,
! [X2,X0,X1] : meet(X2,X0) = join(meet(X2,X0),meet(X2,complement(join(complement(X0),X1)))),
inference(superposition,[],[f126,f67542]) ).
fof(f69230,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(meet(X1,X0)),complement(meet(X0,X1))),
inference(superposition,[],[f67627,f60578]) ).
fof(f69474,plain,
! [X0,X1] : join(X0,complement(join(X1,complement(X0)))) = X0,
inference(superposition,[],[f68372,f3140]) ).
fof(f69907,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(meet(X1,X0)))),
inference(superposition,[],[f153,f66137]) ).
fof(f70733,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f69907,f38248]) ).
fof(f76516,plain,
! [X0,X1] : complement(meet(X1,X0)) = meet(complement(meet(X1,X0)),complement(meet(X0,X1))),
inference(superposition,[],[f15,f69230]) ).
fof(f76557,plain,
! [X2,X0,X1] : meet(X2,complement(meet(X0,X1))) = meet(X2,join(complement(meet(X1,X0)),complement(meet(X0,X1)))),
inference(superposition,[],[f9514,f69230]) ).
fof(f76561,plain,
! [X2,X0,X1] : meet(complement(meet(X0,X1)),X2) = meet(X2,join(complement(meet(X1,X0)),complement(meet(X0,X1)))),
inference(superposition,[],[f9671,f69230]) ).
fof(f76570,plain,
! [X2,X0,X1] : join(X2,complement(meet(X0,X1))) = join(X2,join(complement(meet(X1,X0)),complement(meet(X0,X1)))),
inference(superposition,[],[f16683,f69230]) ).
fof(f76573,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(X2,join(complement(meet(X1,X0)),complement(meet(X0,X1)))),
inference(superposition,[],[f16887,f69230]) ).
fof(f76601,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(X2,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f76573,f69230]) ).
fof(f76603,plain,
! [X2,X0,X1] : join(X2,complement(meet(X0,X1))) = join(X2,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f76570,f69230]) ).
fof(f76609,plain,
! [X2,X0,X1] : meet(complement(meet(X0,X1)),X2) = meet(X2,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f76561,f69230]) ).
fof(f76612,plain,
! [X2,X0,X1] : meet(X2,complement(meet(X0,X1))) = meet(X2,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f76557,f69230]) ).
fof(f78260,plain,
! [X2,X3,X0,X1] : meet(X3,complement(meet(X0,meet(X1,X2)))) = meet(X3,complement(meet(X2,meet(X0,X1)))),
inference(superposition,[],[f76612,f7]) ).
fof(f78264,plain,
! [X2,X0,X1] : meet(X2,complement(join(X0,X1))) = meet(X2,complement(meet(join(X1,X0),join(X0,X1)))),
inference(superposition,[],[f76612,f9668]) ).
fof(f78784,plain,
! [X2,X0,X1] : meet(X2,complement(join(X0,X1))) = meet(X2,complement(join(X1,X0))),
inference(forward_demodulation,[],[f78264,f9668]) ).
fof(f78927,plain,
! [X2,X0,X1] : join(X2,complement(join(X0,X1))) = join(X2,complement(meet(join(X1,X0),join(X0,X1)))),
inference(superposition,[],[f76603,f9668]) ).
fof(f79127,plain,
! [X2,X0,X1] : join(complement(meet(X2,X1)),X0) = meet(join(complement(meet(X2,X1)),X0),join(X0,complement(meet(X1,X2)))),
inference(superposition,[],[f9668,f76603]) ).
fof(f79265,plain,
! [X2,X0,X1] : join(X2,complement(join(X0,X1))) = join(X2,complement(join(X1,X0))),
inference(forward_demodulation,[],[f78927,f9668]) ).
fof(f88214,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(meet(complement(meet(X0,X1)),complement(meet(X1,X0))),X2),
inference(superposition,[],[f18019,f66702]) ).
fof(f88291,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),X2) = join(complement(meet(X0,X1)),X2),
inference(forward_demodulation,[],[f88214,f66702]) ).
fof(f89230,plain,
! [X0,X1] : meet(X1,X0) = join(meet(X1,X0),complement(join(complement(X0),complement(X1)))),
inference(superposition,[],[f68817,f68283]) ).
fof(f90031,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(join(complement(X1),complement(X0)),complement(meet(X0,X1))),
inference(superposition,[],[f69474,f89230]) ).
fof(f90153,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(meet(X1,X0)),join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f90031,f76601]) ).
fof(f90275,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),join(complement(meet(X1,X0)),complement(X1))),
inference(forward_demodulation,[],[f90153,f164]) ).
fof(f90362,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),join(complement(X1),complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f90275,f16683]) ).
fof(f90430,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(meet(X1,X0)),complement(X1)),
inference(forward_demodulation,[],[f90362,f66499]) ).
fof(f90480,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X1),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f90430,f6]) ).
fof(f90519,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f90480,f67039]) ).
fof(f90668,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(X1)),
inference(superposition,[],[f90519,f3140]) ).
fof(f90675,plain,
! [X0,X1] : join(complement(X1),X0) = complement(meet(X1,complement(X0))),
inference(superposition,[],[f90519,f3140]) ).
fof(f90734,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X1),complement(X0)),
inference(superposition,[],[f6,f90519]) ).
fof(f91053,plain,
! [X2,X0,X1] : join(X2,complement(meet(X0,X1))) = complement(meet(X0,meet(X1,complement(X2)))),
inference(superposition,[],[f90668,f128]) ).
fof(f91054,plain,
! [X2,X0,X1] : join(X1,complement(meet(X2,X0))) = complement(meet(X0,meet(complement(X1),X2))),
inference(superposition,[],[f90668,f128]) ).
fof(f91071,plain,
! [X2,X0,X1] : join(X2,complement(join(X1,X0))) = complement(meet(join(X0,X1),complement(X2))),
inference(superposition,[],[f90668,f9671]) ).
fof(f91183,plain,
! [X0,X1] : meet(complement(X0),X1) = complement(join(X0,complement(X1))),
inference(superposition,[],[f3140,f90668]) ).
fof(f91335,plain,
! [X2,X0,X1] : join(complement(join(X0,X1)),X2) = join(X2,complement(join(X1,X0))),
inference(forward_demodulation,[],[f91071,f90675]) ).
fof(f91543,plain,
! [X2,X0,X1] : complement(meet(X2,join(X0,complement(X1)))) = join(complement(X2),meet(complement(X0),X1)),
inference(superposition,[],[f90675,f90668]) ).
fof(f91544,plain,
! [X2,X0,X1] : join(complement(X2),meet(X0,complement(X1))) = complement(meet(X2,join(complement(X0),X1))),
inference(superposition,[],[f90675,f90675]) ).
fof(f91656,plain,
! [X0,X1] : meet(X0,complement(X1)) = complement(join(complement(X0),X1)),
inference(superposition,[],[f3140,f90675]) ).
fof(f91931,plain,
! [X2,X0,X1] : complement(join(X2,meet(complement(X0),X1))) = meet(complement(X2),join(X0,complement(X1))),
inference(superposition,[],[f91183,f91183]) ).
fof(f91932,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X1),complement(X0)),
inference(superposition,[],[f91183,f3140]) ).
fof(f91955,plain,
! [X2,X0,X1] : meet(complement(join(X0,X1)),X2) = complement(join(X0,join(X1,complement(X2)))),
inference(superposition,[],[f91183,f8]) ).
fof(f92227,plain,
! [X2,X0,X1] : complement(join(meet(X0,complement(X1)),X2)) = meet(join(complement(X0),X1),complement(X2)),
inference(superposition,[],[f91932,f90675]) ).
fof(f92237,plain,
! [X2,X0,X1] : meet(complement(X2),join(complement(X0),X1)) = complement(join(X2,meet(X0,complement(X1)))),
inference(superposition,[],[f91932,f90675]) ).
fof(f92334,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(X0)),
inference(superposition,[],[f5,f91932]) ).
fof(f92351,plain,
! [X2,X0,X1] : meet(X2,complement(join(X0,X1))) = meet(complement(X1),meet(X2,complement(X0))),
inference(superposition,[],[f128,f91932]) ).
fof(f92446,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(X0),meet(complement(X1),complement(complement(join(X0,X1))))),
inference(superposition,[],[f69907,f91932]) ).
fof(f92469,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(X0),complement(join(X1,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f92446,f91932]) ).
fof(f92637,plain,
! [X0,X1] : complement(meet(X0,join(X1,complement(join(X0,X1))))) = join(complement(X0),complement(X1)),
inference(forward_demodulation,[],[f92469,f90519]) ).
fof(f92742,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X0,join(X1,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f92637,f90519]) ).
fof(f92820,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),meet(complement(X1),join(X0,X1))),
inference(forward_demodulation,[],[f92742,f91543]) ).
fof(f93165,plain,
! [X2,X0,X1] : meet(complement(X0),complement(X1)) = join(complement(join(X0,X1)),meet(complement(X0),meet(X2,complement(X1)))),
inference(superposition,[],[f60578,f92334]) ).
fof(f93220,plain,
! [X2,X0,X1] : meet(complement(X0),complement(X1)) = join(complement(join(X0,X1)),meet(X2,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f93165,f92351]) ).
fof(f93389,plain,
! [X2,X0,X1] : complement(join(X0,X1)) = join(complement(join(X0,X1)),meet(X2,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f93220,f91932]) ).
fof(f94621,plain,
! [X0,X1] : complement(complement(meet(X0,complement(complement(X1))))) = meet(X1,complement(meet(complement(complement(X1)),complement(meet(X0,complement(complement(X1))))))),
inference(superposition,[],[f91656,f65546]) ).
fof(f94829,plain,
! [X0,X1] : complement(complement(meet(X0,complement(complement(X1))))) = meet(X1,join(complement(complement(complement(X1))),meet(X0,complement(complement(X1))))),
inference(forward_demodulation,[],[f94621,f90675]) ).
fof(f94940,plain,
! [X0,X1] : complement(complement(meet(X0,X1))) = meet(X1,join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[],[f94829,f3140]) ).
fof(f95000,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[],[f94940,f3140]) ).
fof(f95105,plain,
! [X0,X1] : meet(join(X0,X1),join(complement(join(X0,X1)),X0)) = X0,
inference(superposition,[],[f95000,f3]) ).
fof(f95170,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),join(complement(complement(X0)),complement(join(X0,X1)))),
inference(superposition,[],[f95000,f92334]) ).
fof(f95171,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),join(complement(complement(X1)),complement(join(X0,X1)))),
inference(superposition,[],[f95000,f91932]) ).
fof(f95482,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(meet(complement(X1),join(X0,X1)))),
inference(forward_demodulation,[],[f95171,f90519]) ).
fof(f95483,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(meet(complement(X0),join(X0,X1)))),
inference(forward_demodulation,[],[f95170,f90519]) ).
fof(f95527,plain,
! [X0,X1] : meet(join(X0,X1),join(X0,complement(join(X0,X1)))) = X0,
inference(forward_demodulation,[],[f95105,f9514]) ).
fof(f95657,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,meet(complement(X1),join(X0,X1)))),
inference(forward_demodulation,[],[f95482,f91932]) ).
fof(f95658,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X0,meet(complement(X0),join(X0,X1)))),
inference(forward_demodulation,[],[f95483,f91932]) ).
fof(f95779,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),join(X1,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f95657,f91931]) ).
fof(f95780,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),join(X0,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f95658,f91931]) ).
fof(f96142,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(meet(X0,X1),complement(X0))),
inference(superposition,[],[f95527,f67132]) ).
fof(f96201,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f116,f95527]) ).
fof(f96496,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),meet(X1,X0))),
inference(forward_demodulation,[],[f96142,f17722]) ).
fof(f96959,plain,
! [X0,X1] : meet(complement(X0),complement(X1)) = meet(complement(X0),join(complement(X1),complement(complement(meet(X0,X1))))),
inference(superposition,[],[f96201,f90734]) ).
fof(f96960,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = meet(complement(X1),join(complement(X0),complement(complement(meet(X0,X1))))),
inference(superposition,[],[f96201,f90519]) ).
fof(f97064,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(meet(join(X1,complement(join(X1,X0))),X0),X2),
inference(superposition,[],[f10226,f96201]) ).
fof(f97212,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(join(X1,complement(join(X1,X0))),meet(X0,X2)),
inference(forward_demodulation,[],[f97064,f7]) ).
fof(f97283,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = meet(complement(X1),complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f96960,f90519]) ).
fof(f97284,plain,
! [X0,X1] : meet(complement(X0),complement(X1)) = meet(complement(X0),complement(meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f96959,f90519]) ).
fof(f97419,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X0,meet(X2,join(X1,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f97212,f128]) ).
fof(f97474,plain,
! [X0,X1] : complement(join(X1,meet(X0,complement(meet(X0,X1))))) = meet(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f97283,f91932]) ).
fof(f97475,plain,
! [X0,X1] : complement(join(X0,meet(X1,complement(meet(X0,X1))))) = meet(complement(X0),complement(X1)),
inference(forward_demodulation,[],[f97284,f91932]) ).
fof(f97616,plain,
! [X0,X1] : complement(join(X1,X0)) = complement(join(X1,meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f97474,f91932]) ).
fof(f97617,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X0,meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f97475,f91932]) ).
fof(f97727,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X1),join(complement(X0),meet(X0,X1))),
inference(forward_demodulation,[],[f97616,f92237]) ).
fof(f97728,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[],[f97617,f92237]) ).
fof(f98131,plain,
! [X0,X1] : meet(join(complement(join(X0,X1)),X1),complement(X1)) = join(meet(complement(X1),complement(join(X0,X1))),complement(join(X0,X1))),
inference(superposition,[],[f54893,f95779]) ).
fof(f98328,plain,
! [X0,X1] : meet(join(complement(join(X0,X1)),X1),complement(X1)) = join(complement(join(X1,X0)),meet(complement(X1),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f98131,f91335]) ).
fof(f98515,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(join(complement(join(X0,X1)),X1),complement(X1)),
inference(forward_demodulation,[],[f98328,f93389]) ).
fof(f98652,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X1),join(complement(join(X0,X1)),X1)),
inference(forward_demodulation,[],[f98515,f5]) ).
fof(f98755,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X1),join(X1,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f98652,f9514]) ).
fof(f103383,plain,
! [X0,X1] : complement(meet(join(complement(X1),meet(X1,X0)),complement(X0))) = meet(complement(complement(join(X0,X1))),complement(meet(join(complement(X1),meet(X1,X0)),complement(X0)))),
inference(superposition,[],[f66702,f97727]) ).
fof(f103418,plain,
! [X0,X1] : complement(meet(join(complement(X1),meet(X1,X0)),complement(X0))) = meet(complement(complement(join(X0,X1))),complement(meet(complement(X0),join(complement(X1),meet(X1,X0))))),
inference(forward_demodulation,[],[f103383,f76612]) ).
fof(f103665,plain,
! [X0,X1] : complement(meet(join(complement(X1),meet(X1,X0)),complement(X0))) = complement(join(complement(join(X0,X1)),meet(complement(X0),join(complement(X1),meet(X1,X0))))),
inference(forward_demodulation,[],[f103418,f91932]) ).
fof(f103875,plain,
! [X0,X1] : complement(meet(join(complement(X1),meet(X1,X0)),complement(X0))) = meet(complement(complement(join(X0,X1))),join(X0,complement(join(complement(X1),meet(X1,X0))))),
inference(forward_demodulation,[],[f103665,f91931]) ).
fof(f104044,plain,
! [X0,X1] : complement(meet(join(complement(X1),meet(X1,X0)),complement(X0))) = meet(complement(complement(join(X0,X1))),join(X0,meet(X1,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f103875,f91656]) ).
fof(f104182,plain,
! [X0,X1] : meet(complement(complement(join(X0,X1))),join(X0,X1)) = complement(meet(join(complement(X1),meet(X1,X0)),complement(X0))),
inference(forward_demodulation,[],[f104044,f70733]) ).
fof(f104301,plain,
! [X0,X1] : meet(complement(complement(join(X0,X1))),join(X0,X1)) = complement(meet(complement(X0),join(complement(X1),meet(X1,X0)))),
inference(forward_demodulation,[],[f104182,f38248]) ).
fof(f104405,plain,
! [X0,X1] : meet(complement(complement(join(X0,X1))),join(X0,X1)) = join(complement(complement(X0)),meet(X1,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f104301,f91544]) ).
fof(f104490,plain,
! [X0,X1] : join(X0,meet(X1,complement(meet(X1,X0)))) = meet(complement(complement(join(X0,X1))),join(X0,X1)),
inference(forward_demodulation,[],[f104405,f3140]) ).
fof(f104560,plain,
! [X0,X1] : join(X0,meet(X1,complement(meet(X1,X0)))) = meet(join(X1,X0),complement(complement(join(X0,X1)))),
inference(forward_demodulation,[],[f104490,f9671]) ).
fof(f104619,plain,
! [X0,X1] : join(X0,meet(X1,complement(meet(X1,X0)))) = meet(join(X1,X0),join(X0,X1)),
inference(forward_demodulation,[],[f104560,f3140]) ).
fof(f104664,plain,
! [X0,X1] : join(X1,X0) = join(X0,meet(X1,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f104619,f9668]) ).
fof(f105003,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),meet(complement(X1),complement(complement(join(X0,X1))))),
inference(superposition,[],[f104664,f92334]) ).
fof(f105259,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),complement(join(X1,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f105003,f91932]) ).
fof(f105420,plain,
! [X0,X1] : complement(meet(X0,join(X1,complement(join(X0,X1))))) = join(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f105259,f90519]) ).
fof(f105538,plain,
! [X0,X1] : complement(meet(X1,X0)) = complement(meet(X0,join(X1,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f105420,f90519]) ).
fof(f105615,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),meet(complement(X1),join(X0,X1))),
inference(forward_demodulation,[],[f105538,f91543]) ).
fof(f111629,plain,
! [X2,X0,X1] : meet(complement(join(X0,X1)),X2) = meet(join(complement(X1),meet(X0,X1)),meet(complement(X0),X2)),
inference(superposition,[],[f114,f97728]) ).
fof(f111814,plain,
! [X2,X0,X1] : meet(complement(join(X0,X1)),X2) = meet(complement(X0),meet(X2,join(complement(X1),meet(X0,X1)))),
inference(forward_demodulation,[],[f111629,f128]) ).
fof(f116143,plain,
! [X0,X1] :
( zero != meet(meet(complement(X0),join(X1,X0)),join(complement(X1),complement(complement(meet(X0,X1)))))
| complement(meet(complement(X0),join(X1,X0))) = join(complement(X1),complement(complement(meet(X0,X1)))) ),
inference(superposition,[],[f1101,f105615]) ).
fof(f116239,plain,
! [X0,X1] :
( zero != meet(complement(X0),meet(join(X1,X0),join(complement(X1),complement(complement(meet(X0,X1))))))
| complement(meet(complement(X0),join(X1,X0))) = join(complement(X1),complement(complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f116143,f7]) ).
fof(f116444,plain,
! [X0,X1] :
( zero != meet(complement(X0),meet(join(X1,X0),complement(meet(X1,complement(meet(X0,X1))))))
| complement(meet(complement(X0),join(X1,X0))) = join(complement(X1),complement(complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f116239,f90519]) ).
fof(f116620,plain,
! [X0,X1] :
( zero != meet(join(X1,X0),complement(join(meet(X1,complement(meet(X0,X1))),X0)))
| complement(meet(complement(X0),join(X1,X0))) = join(complement(X1),complement(complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f116444,f92351]) ).
fof(f116752,plain,
! [X0,X1] :
( zero != meet(join(X1,X0),complement(join(X0,meet(X1,complement(meet(X0,X1))))))
| complement(meet(complement(X0),join(X1,X0))) = join(complement(X1),complement(complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f116620,f78784]) ).
fof(f116866,plain,
! [X0,X1] :
( zero != meet(join(X1,X0),meet(complement(X0),join(complement(X1),meet(X0,X1))))
| complement(meet(complement(X0),join(X1,X0))) = join(complement(X1),complement(complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f116752,f92237]) ).
fof(f116962,plain,
! [X0,X1] :
( zero != meet(complement(X0),meet(join(meet(X0,X1),complement(X1)),join(X1,X0)))
| complement(meet(complement(X0),join(X1,X0))) = join(complement(X1),complement(complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f116866,f9683]) ).
fof(f117043,plain,
! [X0,X1] :
( zero != meet(complement(X0),meet(join(X0,X1),join(meet(X0,X1),complement(X1))))
| complement(meet(complement(X0),join(X1,X0))) = join(complement(X1),complement(complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f116962,f10132]) ).
fof(f117109,plain,
! [X0,X1] :
( zero != meet(complement(X0),meet(join(X0,X1),join(complement(X1),meet(X0,X1))))
| complement(meet(complement(X0),join(X1,X0))) = join(complement(X1),complement(complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f117043,f9721]) ).
fof(f117162,plain,
! [X0,X1] :
( zero != meet(complement(join(X0,X1)),join(X0,X1))
| complement(meet(complement(X0),join(X1,X0))) = join(complement(X1),complement(complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f117109,f111814]) ).
fof(f117199,plain,
! [X0,X1] :
( zero != meet(join(X1,X0),complement(join(X0,X1)))
| complement(meet(complement(X0),join(X1,X0))) = join(complement(X1),complement(complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f117162,f9671]) ).
fof(f117228,plain,
! [X0,X1] : complement(meet(complement(X0),join(X1,X0))) = join(complement(X1),complement(complement(meet(X0,X1)))),
inference(forward_subsumption_resolution,[],[f117199,f12143]) ).
fof(f117246,plain,
! [X0,X1] : complement(meet(X1,complement(meet(X0,X1)))) = complement(meet(complement(X0),join(X1,X0))),
inference(forward_demodulation,[],[f117228,f90519]) ).
fof(f117259,plain,
! [X0,X1] : join(X0,complement(join(X1,X0))) = complement(meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f117246,f90668]) ).
fof(f117268,plain,
! [X0,X1] : join(X0,complement(join(X1,X0))) = join(complement(X1),meet(X0,X1)),
inference(forward_demodulation,[],[f117259,f90675]) ).
fof(f117468,plain,
! [X0,X1] : join(complement(join(X1,complement(join(X1,X0)))),meet(X0,X1)) = join(X0,complement(join(join(X1,complement(join(X1,X0))),X0))),
inference(superposition,[],[f117268,f96201]) ).
fof(f117473,plain,
! [X2,X0,X1] : join(complement(join(meet(X1,X0),meet(X1,X2))),meet(X0,X1)) = join(X0,complement(join(join(meet(X1,X0),meet(X1,X2)),X0))),
inference(superposition,[],[f117268,f29517]) ).
fof(f117538,plain,
! [X0,X1] : join(complement(complement(X0)),complement(join(X0,X1))) = join(complement(X1),complement(join(complement(X0),complement(X1)))),
inference(superposition,[],[f117268,f92334]) ).
fof(f117565,plain,
! [X0,X1] : join(complement(X0),meet(X1,X0)) = join(X1,join(complement(X0),meet(X1,X0))),
inference(superposition,[],[f24,f117268]) ).
fof(f117676,plain,
! [X0,X1] : complement(join(X0,complement(join(X1,X0)))) = meet(X1,complement(join(X0,complement(join(X1,X0))))),
inference(superposition,[],[f67542,f117268]) ).
fof(f117735,plain,
! [X0,X1] : join(complement(X1),meet(meet(X0,X1),complement(meet(complement(X1),meet(X0,X1))))) = join(complement(X1),meet(join(X0,complement(join(X1,X0))),complement(meet(complement(X1),meet(X0,X1))))),
inference(superposition,[],[f4687,f117268]) ).
fof(f117775,plain,
! [X0,X1] : complement(join(X0,complement(join(X1,X0)))) = meet(complement(complement(X1)),join(complement(X1),complement(join(X0,complement(join(X1,X0)))))),
inference(superposition,[],[f95780,f117268]) ).
fof(f117784,plain,
! [X0,X1] : complement(join(X0,complement(join(X1,X0)))) = meet(complement(complement(X1)),complement(meet(X1,join(X0,complement(join(X1,X0)))))),
inference(forward_demodulation,[],[f117775,f90519]) ).
fof(f117820,plain,
! [X0,X1] : join(complement(X1),meet(meet(X0,X1),complement(meet(complement(X1),meet(X0,X1))))) = join(complement(X1),meet(join(X0,complement(join(X1,X0))),complement(meet(X1,meet(complement(X1),X0))))),
inference(forward_demodulation,[],[f117735,f78260]) ).
fof(f117868,plain,
! [X0,X1] : meet(complement(X0),join(X1,X0)) = meet(X1,meet(complement(X0),join(X1,X0))),
inference(forward_demodulation,[],[f117676,f91183]) ).
fof(f117950,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),meet(X1,X0)),
inference(forward_demodulation,[],[f117565,f214]) ).
fof(f117964,plain,
! [X0,X1] : join(complement(complement(X0)),complement(join(X0,X1))) = complement(meet(X1,join(complement(X0),complement(X1)))),
inference(forward_demodulation,[],[f117538,f90519]) ).
fof(f118026,plain,
! [X2,X0,X1] : join(complement(join(meet(X1,X0),meet(X1,X2))),meet(X0,X1)) = join(X0,complement(join(X0,join(meet(X1,X0),meet(X1,X2))))),
inference(forward_demodulation,[],[f117473,f79265]) ).
fof(f118031,plain,
! [X0,X1] : join(X0,complement(join(X0,join(X1,complement(join(X1,X0)))))) = join(complement(join(X1,complement(join(X1,X0)))),meet(X0,X1)),
inference(forward_demodulation,[],[f117468,f79265]) ).
fof(f118174,plain,
! [X0,X1] : complement(join(X0,complement(join(X1,X0)))) = complement(join(complement(X1),meet(X1,join(X0,complement(join(X1,X0)))))),
inference(forward_demodulation,[],[f117784,f91932]) ).
fof(f118200,plain,
! [X0,X1] : join(complement(X1),meet(meet(X0,X1),complement(meet(complement(X1),meet(X0,X1))))) = join(complement(X1),meet(join(X0,complement(join(X1,X0))),join(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f117820,f91054]) ).
fof(f118232,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(X1,X0)),
inference(forward_demodulation,[],[f117868,f180]) ).
fof(f118303,plain,
! [X0,X1] : join(complement(complement(X0)),complement(join(X0,X1))) = join(complement(X1),meet(complement(complement(X0)),X1)),
inference(forward_demodulation,[],[f117964,f91543]) ).
fof(f118364,plain,
! [X2,X0,X1] : join(X0,complement(join(X0,meet(X1,X2)))) = join(complement(join(meet(X1,X0),meet(X1,X2))),meet(X0,X1)),
inference(forward_demodulation,[],[f118026,f154]) ).
fof(f118369,plain,
! [X0,X1] : join(X0,complement(join(X0,join(X1,complement(join(X1,X0)))))) = join(meet(X0,X1),complement(join(X1,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f118031,f6]) ).
fof(f118495,plain,
! [X0,X1] : complement(join(X0,complement(join(X1,X0)))) = meet(X1,complement(meet(X1,join(X0,complement(join(X1,X0)))))),
inference(forward_demodulation,[],[f118174,f91656]) ).
fof(f118516,plain,
! [X0,X1] : join(complement(X1),meet(meet(X0,X1),complement(meet(complement(X1),meet(X0,X1))))) = join(complement(X1),meet(join(X0,complement(join(X1,X0))),one)),
inference(forward_demodulation,[],[f118200,f711]) ).
fof(f118600,plain,
! [X0,X1] : join(complement(complement(X0)),complement(join(X0,X1))) = join(complement(complement(X0)),complement(X1)),
inference(forward_demodulation,[],[f118303,f117950]) ).
fof(f118660,plain,
! [X2,X0,X1] : join(X0,complement(join(X0,meet(X1,X2)))) = join(meet(X0,X1),complement(join(meet(X1,X0),meet(X1,X2)))),
inference(forward_demodulation,[],[f118364,f6]) ).
fof(f118665,plain,
! [X0,X1] : join(meet(X0,X1),meet(complement(X1),join(X1,X0))) = join(X0,complement(join(X0,join(X1,complement(join(X1,X0)))))),
inference(forward_demodulation,[],[f118369,f91183]) ).
fof(f118769,plain,
! [X0,X1] : complement(join(X0,complement(join(X1,X0)))) = meet(X1,join(complement(X1),meet(complement(X0),join(X1,X0)))),
inference(forward_demodulation,[],[f118495,f91543]) ).
fof(f118787,plain,
! [X0,X1] : join(complement(X1),meet(meet(X0,X1),complement(meet(complement(X1),meet(X0,X1))))) = join(complement(X1),meet(one,join(X0,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f118516,f17008]) ).
fof(f118856,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(complement(complement(X0)),complement(join(X0,X1))),
inference(forward_demodulation,[],[f118600,f90519]) ).
fof(f118915,plain,
! [X0,X1] : join(meet(X0,X1),meet(complement(X1),join(X1,X0))) = join(X0,meet(complement(join(X0,X1)),join(X1,X0))),
inference(forward_demodulation,[],[f118665,f91955]) ).
fof(f118994,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = complement(join(X0,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f118769,f92820]) ).
fof(f119010,plain,
! [X0,X1] : join(complement(X1),join(X0,complement(join(X1,X0)))) = join(complement(X1),meet(meet(X0,X1),complement(meet(complement(X1),meet(X0,X1))))),
inference(forward_demodulation,[],[f118787,f271]) ).
fof(f119061,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = complement(meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f118856,f90519]) ).
fof(f119105,plain,
! [X0,X1] : join(meet(X0,X1),meet(complement(X1),join(X1,X0))) = join(X0,meet(join(X1,X0),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f118915,f17008]) ).
fof(f119150,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(complement(X0),join(X1,X0)),
inference(forward_demodulation,[],[f118994,f91183]) ).
fof(f119165,plain,
! [X0,X1] : join(complement(X1),meet(X0,X1)) = join(complement(X1),join(X0,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f119010,f69907]) ).
fof(f119210,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = complement(meet(complement(X0),X1)),
inference(forward_demodulation,[],[f119061,f90668]) ).
fof(f119245,plain,
! [X0,X1] : join(X0,zero) = join(meet(X0,X1),meet(complement(X1),join(X1,X0))),
inference(forward_demodulation,[],[f119105,f12143]) ).
fof(f119279,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(X1,complement(X0)),
inference(forward_demodulation,[],[f119150,f118232]) ).
fof(f119292,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(X1),meet(X0,X1)),
inference(forward_demodulation,[],[f119165,f67652]) ).
fof(f119332,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = join(X0,complement(X1)),
inference(forward_demodulation,[],[f119210,f90668]) ).
fof(f119362,plain,
! [X0,X1] : join(meet(X0,X1),meet(complement(X1),join(X1,X0))) = X0,
inference(forward_demodulation,[],[f119245,f249]) ).
fof(f119729,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(X1,complement(X0))),
inference(superposition,[],[f119292,f3140]) ).
fof(f119771,plain,
! [X2,X0,X1] : join(complement(join(meet(X1,X0),meet(X1,X2))),meet(X0,X1)) = join(complement(join(meet(X1,X0),meet(X1,X2))),X0),
inference(superposition,[],[f119292,f29517]) ).
fof(f119841,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),X1)),
inference(superposition,[],[f96496,f119292]) ).
fof(f120105,plain,
! [X2,X0,X1] : join(complement(join(meet(X1,X0),meet(X1,X2))),meet(X0,X1)) = join(X0,complement(join(meet(X1,X0),meet(X1,X2)))),
inference(forward_demodulation,[],[f119771,f6]) ).
fof(f120258,plain,
! [X2,X0,X1] : join(meet(X0,X1),complement(join(meet(X1,X0),meet(X1,X2)))) = join(X0,complement(join(meet(X1,X0),meet(X1,X2)))),
inference(forward_demodulation,[],[f120105,f6]) ).
fof(f120393,plain,
! [X2,X0,X1] : join(X0,complement(join(X0,meet(X1,X2)))) = join(X0,complement(join(meet(X1,X0),meet(X1,X2)))),
inference(forward_demodulation,[],[f120258,f118660]) ).
fof(f120498,plain,
! [X2,X0,X1] : join(X0,complement(meet(X1,X2))) = join(X0,complement(join(meet(X1,X0),meet(X1,X2)))),
inference(forward_demodulation,[],[f120393,f119332]) ).
fof(f120948,plain,
! [X0,X1] :
( zero != meet(meet(X1,complement(X0)),join(X0,complement(join(X0,X1))))
| join(X0,complement(join(X0,X1))) = complement(meet(X1,complement(X0))) ),
inference(superposition,[],[f1101,f119729]) ).
fof(f121093,plain,
! [X0,X1] :
( zero != meet(X1,meet(complement(X0),join(X0,complement(join(X0,X1)))))
| join(X0,complement(join(X0,X1))) = complement(meet(X1,complement(X0))) ),
inference(forward_demodulation,[],[f120948,f7]) ).
fof(f121208,plain,
! [X0,X1] :
( zero != meet(complement(X0),meet(X1,X0))
| join(X0,complement(join(X0,X1))) = complement(meet(X1,complement(X0))) ),
inference(forward_demodulation,[],[f121093,f97419]) ).
fof(f121289,plain,
! [X0,X1] :
( zero != meet(X0,meet(complement(X0),X1))
| join(X0,complement(join(X0,X1))) = complement(meet(X1,complement(X0))) ),
inference(forward_demodulation,[],[f121208,f128]) ).
fof(f121348,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = complement(meet(X1,complement(X0))),
inference(forward_subsumption_resolution,[],[f121289,f515]) ).
fof(f121390,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f121348,f90675]) ).
fof(f121710,plain,
! [X0,X1] : complement(join(complement(join(X0,X1)),X0)) = meet(complement(complement(join(X0,X1))),join(complement(join(X0,X1)),complement(join(X0,complement(X1))))),
inference(superposition,[],[f98755,f119332]) ).
fof(f121719,plain,
! [X2,X0,X1] : join(meet(X1,X0),complement(join(meet(X0,X1),X2))) = join(meet(X0,X1),complement(X2)),
inference(superposition,[],[f18019,f119332]) ).
fof(f121754,plain,
! [X0,X1] : complement(join(complement(join(X0,X1)),X0)) = meet(complement(complement(join(X0,X1))),complement(meet(join(X0,X1),join(X0,complement(X1))))),
inference(forward_demodulation,[],[f121710,f90519]) ).
fof(f121925,plain,
! [X0,X1] : complement(join(complement(join(X0,X1)),X0)) = complement(join(complement(join(X0,X1)),meet(join(X0,X1),join(X0,complement(X1))))),
inference(forward_demodulation,[],[f121754,f91932]) ).
fof(f122049,plain,
! [X0,X1] : complement(join(complement(join(X0,X1)),X0)) = meet(join(X0,X1),complement(meet(join(X0,X1),join(X0,complement(X1))))),
inference(forward_demodulation,[],[f121925,f91656]) ).
fof(f122136,plain,
! [X0,X1] : complement(join(complement(join(X0,X1)),X0)) = meet(join(X0,X1),complement(join(X0,complement(X1)))),
inference(forward_demodulation,[],[f122049,f119279]) ).
fof(f122197,plain,
! [X0,X1] : complement(join(complement(join(X0,X1)),X0)) = meet(join(X0,X1),meet(complement(X0),X1)),
inference(forward_demodulation,[],[f122136,f91183]) ).
fof(f122236,plain,
! [X0,X1] : complement(join(complement(join(X0,X1)),X0)) = meet(X1,meet(join(X0,X1),complement(X0))),
inference(forward_demodulation,[],[f122197,f128]) ).
fof(f122265,plain,
! [X0,X1] : complement(join(complement(join(X0,X1)),X0)) = meet(X1,meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f122236,f9452]) ).
fof(f122289,plain,
! [X0,X1] : meet(X1,complement(X0)) = complement(join(complement(join(X0,X1)),X0)),
inference(forward_demodulation,[],[f122265,f555]) ).
fof(f122308,plain,
! [X0,X1] : meet(X1,complement(X0)) = complement(join(X0,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f122289,f38740]) ).
fof(f122320,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f122308,f91183]) ).
fof(f122466,plain,
! [X0,X1] : meet(complement(complement(X0)),complement(meet(X0,X1))) = meet(complement(X1),complement(complement(X0))),
inference(superposition,[],[f122320,f90519]) ).
fof(f122571,plain,
! [X2,X0,X1] : meet(X2,meet(X0,complement(X1))) = meet(complement(X1),meet(join(X1,X0),X2)),
inference(superposition,[],[f128,f122320]) ).
fof(f122823,plain,
! [X0,X1] : complement(join(X1,complement(X0))) = meet(complement(complement(X0)),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f122466,f91932]) ).
fof(f123027,plain,
! [X0,X1] : complement(join(X1,complement(X0))) = complement(join(complement(X0),meet(X0,X1))),
inference(forward_demodulation,[],[f122823,f91932]) ).
fof(f123192,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = complement(join(X1,complement(X0))),
inference(forward_demodulation,[],[f123027,f91656]) ).
fof(f123302,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f123192,f91183]) ).
fof(f127168,plain,
! [X2,X0,X1] : meet(X0,meet(complement(meet(X0,X1)),X2)) = meet(X2,meet(X0,complement(X1))),
inference(superposition,[],[f128,f119279]) ).
fof(f127208,plain,
! [X2,X0,X1] : meet(X2,meet(X0,complement(X1))) = meet(meet(complement(meet(X0,X1)),X0),X2),
inference(superposition,[],[f10226,f119279]) ).
fof(f127381,plain,
! [X2,X0,X1] : meet(X2,meet(X0,complement(X1))) = meet(complement(meet(X0,X1)),meet(X0,X2)),
inference(forward_demodulation,[],[f127208,f7]) ).
fof(f127604,plain,
! [X2,X0,X1] : meet(X2,meet(X0,complement(X1))) = meet(X0,meet(X2,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f127381,f128]) ).
fof(f128508,plain,
! [X2,X0,X1] : meet(complement(X0),meet(X1,X2)) = meet(X1,meet(X2,complement(meet(meet(X1,X2),X0)))),
inference(superposition,[],[f7,f123302]) ).
fof(f128569,plain,
! [X2,X0,X1] : meet(X1,meet(X2,complement(meet(X1,meet(X2,X0))))) = meet(complement(X0),meet(X1,X2)),
inference(forward_demodulation,[],[f128508,f7]) ).
fof(f128808,plain,
! [X2,X0,X1] : meet(complement(X0),meet(X1,X2)) = meet(X2,meet(X1,complement(meet(X2,X0)))),
inference(forward_demodulation,[],[f128569,f127604]) ).
fof(f142129,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),X1)) = meet(X0,join(meet(complement(X0),X2),X1)),
inference(superposition,[],[f119841,f153]) ).
fof(f142585,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,join(meet(complement(X0),X2),X1)),
inference(forward_demodulation,[],[f142129,f119841]) ).
fof(f147925,plain,
! [X2,X0,X1] : join(complement(join(meet(X1,X0),meet(X1,X2))),meet(X0,X1)) = join(X0,complement(join(meet(X1,X0),meet(X1,X2)))),
inference(superposition,[],[f117950,f29517]) ).
fof(f148333,plain,
! [X2,X0,X1] : join(X0,complement(meet(X1,X2))) = join(complement(join(meet(X1,X0),meet(X1,X2))),meet(X0,X1)),
inference(forward_demodulation,[],[f147925,f120498]) ).
fof(f148518,plain,
! [X2,X0,X1] : join(X0,complement(meet(X1,X2))) = join(meet(X0,X1),complement(join(meet(X1,X0),meet(X1,X2)))),
inference(forward_demodulation,[],[f148333,f6]) ).
fof(f148665,plain,
! [X2,X0,X1] : join(X0,complement(meet(X1,X2))) = join(meet(X1,X0),complement(meet(X1,X2))),
inference(forward_demodulation,[],[f148518,f121719]) ).
fof(f152708,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = join(meet(meet(join(X1,X0),X2),meet(X2,X0)),meet(complement(meet(X2,X0)),meet(join(X0,X1),X2))),
inference(superposition,[],[f119362,f54895]) ).
fof(f153055,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = join(meet(meet(join(X1,X0),X2),meet(X2,X0)),meet(X2,meet(complement(meet(X2,X0)),join(X0,X1)))),
inference(forward_demodulation,[],[f152708,f17576]) ).
fof(f153386,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = join(meet(meet(X2,X0),meet(join(X1,X0),X2)),meet(meet(complement(meet(X2,X0)),join(X0,X1)),X2)),
inference(forward_demodulation,[],[f153055,f17997]) ).
fof(f153666,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = join(meet(meet(X2,X0),meet(join(X1,X0),X2)),meet(X2,meet(complement(meet(X2,X0)),join(X0,X1)))),
inference(forward_demodulation,[],[f153386,f17008]) ).
fof(f153918,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = join(meet(X2,meet(meet(X2,X0),join(X1,X0))),meet(X2,meet(complement(meet(X2,X0)),join(X0,X1)))),
inference(forward_demodulation,[],[f153666,f20573]) ).
fof(f154124,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = join(meet(X2,meet(meet(X2,X0),join(X1,X0))),meet(join(X0,X1),meet(X2,complement(X0)))),
inference(forward_demodulation,[],[f153918,f127168]) ).
fof(f154300,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = join(meet(join(X0,X1),meet(X2,complement(X0))),meet(X2,meet(meet(X2,X0),join(X1,X0)))),
inference(forward_demodulation,[],[f154124,f6]) ).
fof(f154434,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = join(meet(complement(X0),meet(join(X0,X1),X2)),meet(X2,meet(meet(X2,X0),join(X1,X0)))),
inference(forward_demodulation,[],[f154300,f20573]) ).
fof(f154540,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = join(meet(complement(X0),meet(join(X0,X1),X2)),meet(X2,meet(X2,meet(X0,join(X1,X0))))),
inference(forward_demodulation,[],[f154434,f7]) ).
fof(f154622,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = join(meet(complement(X0),meet(join(X0,X1),X2)),meet(X2,meet(X0,join(X1,X0)))),
inference(forward_demodulation,[],[f154540,f33]) ).
fof(f154691,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = join(meet(X2,meet(X0,join(X1,X0))),meet(complement(X0),meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f154622,f6]) ).
fof(f154748,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = join(meet(X2,meet(X0,join(X1,X0))),meet(X2,meet(X1,complement(X0)))),
inference(forward_demodulation,[],[f154691,f122571]) ).
fof(f154797,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = join(meet(X2,meet(X1,complement(X0))),meet(X2,meet(X0,join(X1,X0)))),
inference(forward_demodulation,[],[f154748,f6]) ).
fof(f154839,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = join(meet(X2,meet(X1,complement(X0))),meet(X2,X0)),
inference(forward_demodulation,[],[f154797,f15]) ).
fof(f154875,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = join(meet(X2,X0),meet(X2,meet(X1,complement(X0)))),
inference(forward_demodulation,[],[f154839,f6]) ).
fof(f169749,plain,
! [X2,X0,X1] : complement(meet(meet(X1,complement(meet(X2,X0))),X2)) = meet(complement(meet(meet(X1,complement(meet(X2,X0))),X2)),complement(meet(complement(X0),meet(X1,X2)))),
inference(superposition,[],[f76516,f128808]) ).
fof(f169865,plain,
! [X2,X0,X1] : complement(meet(meet(X1,complement(meet(X2,X0))),X2)) = meet(complement(meet(meet(X1,X2),complement(X0))),complement(meet(meet(X1,complement(meet(X2,X0))),X2))),
inference(forward_demodulation,[],[f169749,f76609]) ).
fof(f170161,plain,
! [X2,X0,X1] : complement(meet(meet(X1,complement(meet(X2,X0))),X2)) = meet(complement(meet(meet(X1,X2),complement(X0))),complement(meet(X2,meet(X1,complement(meet(X2,X0)))))),
inference(forward_demodulation,[],[f169865,f76612]) ).
fof(f170407,plain,
! [X2,X0,X1] : complement(meet(meet(X1,complement(meet(X2,X0))),X2)) = complement(join(meet(meet(X1,X2),complement(X0)),meet(X2,meet(X1,complement(meet(X2,X0)))))),
inference(forward_demodulation,[],[f170161,f91932]) ).
fof(f170589,plain,
! [X2,X0,X1] : complement(meet(meet(X1,complement(meet(X2,X0))),X2)) = meet(join(complement(meet(X1,X2)),X0),complement(meet(X2,meet(X1,complement(meet(X2,X0)))))),
inference(forward_demodulation,[],[f170407,f92227]) ).
fof(f170737,plain,
! [X2,X0,X1] : complement(meet(meet(X1,complement(meet(X2,X0))),X2)) = meet(join(complement(meet(X1,X2)),X0),join(meet(X2,X0),complement(meet(X2,X1)))),
inference(forward_demodulation,[],[f170589,f91053]) ).
fof(f170853,plain,
! [X2,X0,X1] : complement(meet(meet(X1,complement(meet(X2,X0))),X2)) = meet(join(complement(meet(X1,X2)),X0),join(X0,complement(meet(X2,X1)))),
inference(forward_demodulation,[],[f170737,f148665]) ).
fof(f170940,plain,
! [X2,X0,X1] : join(complement(meet(X1,X2)),X0) = complement(meet(meet(X1,complement(meet(X2,X0))),X2)),
inference(forward_demodulation,[],[f170853,f79127]) ).
fof(f171004,plain,
! [X2,X0,X1] : join(complement(meet(X1,X2)),X0) = complement(meet(X2,meet(X1,complement(meet(X2,X0))))),
inference(forward_demodulation,[],[f170940,f38248]) ).
fof(f171056,plain,
! [X2,X0,X1] : join(complement(meet(X1,X2)),X0) = join(meet(X2,X0),complement(meet(X2,X1))),
inference(forward_demodulation,[],[f171004,f91053]) ).
fof(f187395,plain,
! [X2,X3,X0,X1] : join(meet(X0,X3),complement(meet(X0,X1))) = join(complement(meet(join(meet(complement(X0),X2),X1),X0)),X3),
inference(superposition,[],[f171056,f142585]) ).
fof(f187831,plain,
! [X2,X3,X0,X1] : join(meet(X0,X3),complement(meet(X0,X1))) = join(complement(meet(X0,join(meet(complement(X0),X2),X1))),X3),
inference(forward_demodulation,[],[f187395,f88291]) ).
fof(f188167,plain,
! [X3,X0,X1] : join(complement(meet(X0,X1)),X3) = join(meet(X0,X3),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f187831,f142585]) ).
fof(f189634,plain,
! [X2,X0,X1] : join(meet(X0,X2),complement(join(complement(meet(X0,X1)),X2))) = join(complement(complement(meet(X0,X1))),meet(X0,X2)),
inference(superposition,[],[f121390,f188167]) ).
fof(f189648,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,X2),complement(join(complement(meet(X0,X1)),X2))),
inference(forward_demodulation,[],[f189634,f3140]) ).
fof(f189928,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,X2),meet(meet(X0,X1),complement(X2))),
inference(forward_demodulation,[],[f189648,f91656]) ).
fof(f190123,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,X2),meet(X0,meet(X1,complement(X2)))),
inference(forward_demodulation,[],[f189928,f7]) ).
fof(f190261,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(join(X1,X2),X0),
inference(forward_demodulation,[],[f190123,f154875]) ).
fof(f190925,plain,
meet(a,join(b,c)) != meet(join(b,c),a),
inference(superposition,[],[f13,f190261]) ).
fof(f191301,plain,
$false,
inference(forward_subsumption_resolution,[],[f190925,f5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT189-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.43 % Computer : n011.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Sun Sep 27 14:05:15 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.43 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.20/0.49 Running first-order theorem proving
% 0.20/0.49 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.84/3.69 % (2441676)Input is clausal, will run a generic CNF schedule.
% 18.84/3.69 % (2441687)dis-21_1_sil=8000:lcm=predicate:random_seed=1271395097: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.84/3.69 % (2441687)Refutation not found, incomplete strategy
% 18.84/3.69 % (2441687)------------------------------
% 18.84/3.69 % (2441687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/3.69 % (2441687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/3.69 % (2441687)CaDiCaL version: 2.1.3
% 18.84/3.69 % (2441687)Termination reason: Refutation not found, incomplete strategy
% 18.84/3.69 % (2441687)Time elapsed: 0.002 s
% 18.84/3.69 % (2441687)Peak memory usage: 88 MB
% 18.84/3.69 % (2441687)Instructions burned: 1 (million)
% 18.84/3.69 % (2441681)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=3131864033:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 18.84/3.69 % (2441682)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3610568236:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 18.84/3.69 % (2441685)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=567761104:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 18.84/3.69 % (2441683)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2048509221:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 18.84/3.69 % (2441684)lrs+10_1_sil=8000:sp=occurrence:random_seed=71198307:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 18.84/3.69 % (2441686)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4161870088:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 18.84/3.69 % (2441684)Instruction limit reached!
% 18.84/3.69 % (2441684)------------------------------
% 18.84/3.69 % (2441684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/3.69 % (2441684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/3.69 % (2441684)CaDiCaL version: 2.1.3
% 18.84/3.69 % (2441684)Termination reason: Instruction limit
% 18.84/3.69 % (2441684)Termination phase: Saturation
% 18.84/3.69 % (2441684)Time elapsed: 0.109 s
% 18.84/3.69 % (2441684)Peak memory usage: 88 MB
% 18.84/3.69 % (2441684)Instructions burned: 107 (million)
% 18.84/3.69 % (2441685)Instruction limit reached!
% 18.84/3.69 % (2441685)------------------------------
% 18.84/3.69 % (2441685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/3.69 % (2441685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/3.69 % (2441685)CaDiCaL version: 2.1.3
% 18.84/3.69 % (2441685)Termination reason: Instruction limit
% 18.84/3.69 % (2441685)Termination phase: Saturation
% 18.84/3.69 % (2441685)Time elapsed: 0.116 s
% 18.84/3.69 % (2441685)Peak memory usage: 89 MB
% 18.84/3.69 % (2441685)Instructions burned: 115 (million)
% 18.84/3.69 % (2441687)------------------------------
% 18.84/3.69 % (2441687)------------------------------
% 18.84/3.69 % (2441686)Instruction limit reached!
% 18.84/3.69 % (2441686)------------------------------
% 18.84/3.69 % (2441686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/3.69 % (2441686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/3.69 % (2441686)CaDiCaL version: 2.1.3
% 18.84/3.69 % (2441686)Termination reason: Instruction limit
% 18.84/3.69 % (2441686)Termination phase: Saturation
% 18.84/3.69 % (2441686)Time elapsed: 0.165 s
% 18.84/3.69 % (2441686)Peak memory usage: 89 MB
% 18.84/3.69 % (2441686)Instructions burned: 180 (million)
% 18.84/3.69 % (2441697)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=455088845:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 18.84/3.69 % (2441697)Refutation not found, incomplete strategy
% 18.84/3.69 % (2441697)------------------------------
% 18.84/3.69 % (2441697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/3.69 % (2441697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/3.69 % (2441697)CaDiCaL version: 2.1.3
% 18.84/3.69 % (2441697)Termination reason: Refutation not found, incomplete strategy
% 18.84/3.69 % (2441697)Time elapsed: 0.001 s
% 18.84/3.69 % (2441697)Peak memory usage: 88 MB
% 18.84/3.69 % (2441695)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=2965780952:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 39.10/6.40 % (2441696)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3747001467:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 39.10/6.40 % (2441695)Refutation not found, incomplete strategy
% 39.10/6.40 % (2441695)------------------------------
% 39.10/6.40 % (2441695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.10/6.40 % (2441695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.10/6.40 % (2441695)CaDiCaL version: 2.1.3
% 39.10/6.40 % (2441695)Termination reason: Refutation not found, incomplete strategy
% 39.10/6.40 % (2441695)Time elapsed: 0.002 s
% 39.10/6.40 % (2441695)Peak memory usage: 88 MB
% 39.10/6.40 % (2441696)Refutation not found, incomplete strategy
% 39.10/6.40 % (2441696)------------------------------
% 39.10/6.40 % (2441696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.10/6.40 % (2441696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.10/6.40 % (2441696)CaDiCaL version: 2.1.3
% 39.10/6.40 % (2441696)Termination reason: Refutation not found, incomplete strategy
% 39.10/6.40 % (2441696)Time elapsed: 0.002 s
% 39.10/6.40 % (2441696)Peak memory usage: 88 MB
% 39.10/6.40 % (2441696)Instructions burned: 1 (million)
% 39.10/6.40 % (2441698)lrs+10_64_to=lpo:sil=8000:random_seed=3495279535:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 39.10/6.40 % (2441698)Instruction limit reached!
% 39.10/6.40 % (2441698)------------------------------
% 39.10/6.40 % (2441698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.10/6.40 % (2441698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.10/6.40 % (2441698)CaDiCaL version: 2.1.3
% 39.10/6.40 % (2441698)Termination reason: Instruction limit
% 39.10/6.40 % (2441698)Termination phase: Saturation
% 39.10/6.40 % (2441698)Time elapsed: 0.123 s
% 39.10/6.40 % (2441698)Peak memory usage: 88 MB
% 39.10/6.40 % (2441698)Instructions burned: 126 (million)
% 39.10/6.40 % (2441697)------------------------------
% 39.10/6.40 % (2441697)------------------------------
% 39.10/6.40 % (2441703)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4161320795:avsq=on:i=194:fgj=on:bd=preordered_2991 on theBenchmark for (2991ds/194Mi)
% 39.10/6.40 % (2441695)------------------------------
% 39.10/6.40 % (2441695)------------------------------
% 39.10/6.40 % (2441696)------------------------------
% 39.10/6.40 % (2441696)------------------------------
% 39.10/6.40 % (2441703)Instruction limit reached!
% 39.10/6.40 % (2441703)------------------------------
% 39.10/6.40 % (2441703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.10/6.40 % (2441703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.10/6.40 % (2441703)CaDiCaL version: 2.1.3
% 39.10/6.40 % (2441703)Termination reason: Instruction limit
% 39.10/6.40 % (2441703)Termination phase: Saturation
% 39.10/6.40 % (2441703)Time elapsed: 0.104 s
% 39.10/6.40 % (2441703)Peak memory usage: 89 MB
% 39.10/6.40 % (2441703)Instructions burned: 195 (million)
% 39.10/6.40 % (2441704)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3891640195:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 39.10/6.40 % (2441704)Instruction limit reached!
% 39.10/6.40 % (2441704)------------------------------
% 39.10/6.40 % (2441704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.10/6.40 % (2441704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.10/6.40 % (2441704)CaDiCaL version: 2.1.3
% 39.10/6.40 % (2441704)Termination reason: Instruction limit
% 39.10/6.40 % (2441704)Termination phase: Saturation
% 39.10/6.40 % (2441704)Time elapsed: 0.161 s
% 39.10/6.40 % (2441704)Peak memory usage: 90 MB
% 39.10/6.40 % (2441704)Instructions burned: 157 (million)
% 39.10/6.40 % (2441707)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=3138319150:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2989 on theBenchmark for (2989ds/106Mi)
% 39.10/6.40 % (2441706)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=219757236:i=3394:sd=4:ss=included:sgt=64_2989 on theBenchmark for (2989ds/3394Mi)
% 39.10/6.40 % (2441708)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2589563077:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 59.67/9.38 % (2441708)Refutation not found, incomplete strategy
% 59.67/9.38 % (2441708)------------------------------
% 59.67/9.38 % (2441708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.67/9.38 % (2441708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.67/9.38 % (2441708)CaDiCaL version: 2.1.3
% 59.67/9.38 % (2441708)Termination reason: Refutation not found, incomplete strategy
% 59.67/9.38 % (2441708)Time elapsed: 0.002 s
% 59.67/9.38 % (2441708)Peak memory usage: 87 MB
% 59.67/9.38 % (2441707)Instruction limit reached!
% 59.67/9.38 % (2441707)------------------------------
% 59.67/9.38 % (2441707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.67/9.38 % (2441707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.67/9.38 % (2441707)CaDiCaL version: 2.1.3
% 59.67/9.38 % (2441707)Termination reason: Instruction limit
% 59.67/9.38 % (2441707)Termination phase: Saturation
% 59.67/9.38 % (2441707)Time elapsed: 0.115 s
% 59.67/9.38 % (2441707)Peak memory usage: 89 MB
% 59.67/9.38 % (2441707)Instructions burned: 106 (million)
% 59.67/9.38 % (2441710)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1440993016:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2986 on theBenchmark for (2986ds/242Mi)
% 59.67/9.38 % (2441714)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2262688225:cond=fast:i=5208:av=off_2985 on theBenchmark for (2985ds/5208Mi)
% 59.67/9.38 % (2441708)------------------------------
% 59.67/9.38 % (2441708)------------------------------
% 59.67/9.38 % (2441710)Instruction limit reached!
% 59.67/9.38 % (2441710)------------------------------
% 59.67/9.38 % (2441710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.67/9.38 % (2441710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.67/9.38 % (2441710)CaDiCaL version: 2.1.3
% 59.67/9.38 % (2441710)Termination reason: Instruction limit
% 59.67/9.38 % (2441710)Termination phase: Saturation
% 59.67/9.38 % (2441710)Time elapsed: 0.240 s
% 59.67/9.38 % (2441710)Peak memory usage: 90 MB
% 59.67/9.38 % (2441710)Instructions burned: 242 (million)
% 59.67/9.38 % (2441717)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3121022229:i=134:sd=2:doe=on:ss=axioms:sgt=14_2981 on theBenchmark for (2981ds/134Mi)
% 59.67/9.38 % (2441718)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2128338881:i=499:bd=all_2981 on theBenchmark for (2981ds/499Mi)
% 59.67/9.38 % (2441717)Instruction limit reached!
% 59.67/9.38 % (2441717)------------------------------
% 59.67/9.38 % (2441717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.67/9.38 % (2441717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.67/9.38 % (2441717)CaDiCaL version: 2.1.3
% 59.67/9.38 % (2441717)Termination reason: Instruction limit
% 59.67/9.38 % (2441717)Termination phase: Saturation
% 59.67/9.38 % (2441717)Time elapsed: 0.132 s
% 59.67/9.38 % (2441717)Peak memory usage: 89 MB
% 59.67/9.38 % (2441717)Instructions burned: 134 (million)
% 59.67/9.38 % (2441721)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=139621281:i=191:fgj=on:bd=all_2977 on theBenchmark for (2977ds/191Mi)
% 59.67/9.38 % (2441718)Instruction limit reached!
% 59.67/9.38 % (2441718)------------------------------
% 59.67/9.38 % (2441718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.67/9.38 % (2441718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.67/9.38 % (2441718)CaDiCaL version: 2.1.3
% 59.67/9.38 % (2441718)Termination reason: Instruction limit
% 59.67/9.38 % (2441718)Termination phase: Saturation
% 59.67/9.38 % (2441718)Time elapsed: 0.523 s
% 59.67/9.38 % (2441718)Peak memory usage: 93 MB
% 59.67/9.38 % (2441718)Instructions burned: 500 (million)
% 59.67/9.38 % (2441721)Instruction limit reached!
% 59.67/9.38 % (2441721)------------------------------
% 59.67/9.38 % (2441721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.67/9.38 % (2441721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.67/9.38 % (2441721)CaDiCaL version: 2.1.3
% 59.67/9.38 % (2441721)Termination reason: Instruction limit
% 59.67/9.38 % (2441721)Termination phase: Saturation
% 59.67/9.38 % (2441721)Time elapsed: 0.199 s
% 59.67/9.38 % (2441721)Peak memory usage: 91 MB
% 59.67/9.38 % (2441721)Instructions burned: 191 (million)
% 36.24/9.73 % (2441723)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=929952769:i=264:kws=precedence:fsr=off_2972 on theBenchmark for (2972ds/264Mi)
% 36.24/9.73 % (2441724)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=197792259:cond=on:i=156:bs=on:gtg=exists_all:er=known_2972 on theBenchmark for (2972ds/156Mi)
% 36.24/9.73 % (2441724)Instruction limit reached!
% 36.24/9.73 % (2441724)------------------------------
% 36.24/9.73 % (2441724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.24/9.73 % (2441724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.24/9.73 % (2441724)CaDiCaL version: 2.1.3
% 36.24/9.73 % (2441724)Termination reason: Instruction limit
% 36.24/9.73 % (2441724)Termination phase: Saturation
% 36.24/9.73 % (2441724)Time elapsed: 0.156 s
% 36.24/9.73 % (2441724)Peak memory usage: 89 MB
% 36.24/9.73 % (2441724)Instructions burned: 156 (million)
% 36.24/9.73 % (2441723)Instruction limit reached!
% 36.24/9.73 % (2441723)------------------------------
% 36.24/9.73 % (2441723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.24/9.73 % (2441723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.24/9.73 % (2441723)CaDiCaL version: 2.1.3
% 36.24/9.73 % (2441723)Termination reason: Instruction limit
% 36.24/9.73 % (2441723)Termination phase: Saturation
% 36.24/9.73 % (2441723)Time elapsed: 0.262 s
% 36.24/9.73 % (2441723)Peak memory usage: 92 MB
% 36.24/9.73 % (2441723)Instructions burned: 264 (million)
% 36.24/9.73 % (2441729)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=2654086409:i=3256:kws=precedence:bd=preordered:av=off_2967 on theBenchmark for (2967ds/3256Mi)
% 36.24/9.73 % (2441730)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3326502990:i=537:av=off:ss=included_2967 on theBenchmark for (2967ds/537Mi)
% 36.24/9.73 % (2441730)Instruction limit reached!
% 36.24/9.73 % (2441730)------------------------------
% 36.24/9.73 % (2441730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.24/9.73 % (2441730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.24/9.73 % (2441730)CaDiCaL version: 2.1.3
% 36.24/9.73 % (2441730)Termination reason: Instruction limit
% 36.24/9.73 % (2441730)Termination phase: Saturation
% 36.24/9.73 % (2441730)Time elapsed: 0.445 s
% 36.24/9.73 % (2441730)Peak memory usage: 93 MB
% 36.24/9.73 % (2441730)Instructions burned: 537 (million)
% 36.24/9.73 % (2441735)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2150074245:i=180:bd=preordered:av=off_2959 on theBenchmark for (2959ds/180Mi)
% 36.24/9.73 % (2441735)Instruction limit reached!
% 36.24/9.73 % (2441735)------------------------------
% 36.24/9.73 % (2441735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.24/9.73 % (2441735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.24/9.73 % (2441735)CaDiCaL version: 2.1.3
% 36.24/9.73 % (2441735)Termination reason: Instruction limit
% 36.24/9.73 % (2441735)Termination phase: Saturation
% 36.24/9.73 % (2441735)Time elapsed: 0.174 s
% 36.24/9.73 % (2441735)Peak memory usage: 88 MB
% 36.24/9.73 % (2441735)Instructions burned: 180 (million)
% 36.24/9.73 % (2441706)Instruction limit reached!
% 36.24/9.73 % (2441706)------------------------------
% 36.24/9.73 % (2441706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.24/9.73 % (2441706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.24/9.73 % (2441706)CaDiCaL version: 2.1.3
% 36.24/9.73 % (2441706)Termination reason: Instruction limit
% 36.24/9.73 % (2441706)Termination phase: Saturation
% 36.24/9.73 % (2441706)Time elapsed: 3.370 s
% 36.24/9.73 % (2441706)Peak memory usage: 149 MB
% 36.24/9.73 % (2441706)Instructions burned: 3394 (million)
% 36.24/9.73 % (2441737)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=24022238:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2955 on theBenchmark for (2955ds/10307Mi)
% 36.24/9.73 % (2441738)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=3936095494:i=412:gtgl=4:gtg=exists_all_2952 on theBenchmark for (2952ds/412Mi)
% 36.24/9.73 % (2441738)Instruction limit reached!
% 36.24/9.73 % (2441738)------------------------------
% 36.24/9.73 % (2441738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.24/9.73 % (2441738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.24/9.73 % (2441738)CaDiCaL version: 2.1.3
% 36.24/9.73 % (2441738)Termination reason: Instruction limit
% 36.24/9.73 % (2441738)Termination phase: Saturation
% 36.24/9.73 % (2441738)Time elapsed: 0.403 s
% 36.24/9.73 % (2441738)Peak memory usage: 94 MB
% 36.24/9.73 % (2441738)Instructions burned: 412 (million)
% 36.24/9.73 % (2441741)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=4048814216:s2pl=no:i=8478:s2at=4:nm=6_2945 on theBenchmark for (2945ds/8478Mi)
% 36.24/9.73 % (2441729)Instruction limit reached!
% 36.24/9.73 % (2441729)------------------------------
% 36.24/9.73 % (2441729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.24/9.73 % (2441729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.24/9.73 % (2441729)CaDiCaL version: 2.1.3
% 36.24/9.73 % (2441729)Termination reason: Instruction limit
% 36.24/9.73 % (2441729)Termination phase: Saturation
% 36.24/9.73 % (2441729)Time elapsed: 3.463 s
% 36.24/9.73 % (2441729)Peak memory usage: 147 MB
% 36.24/9.73 % (2441729)Instructions burned: 3256 (million)
% 36.24/9.73 % (2441714)Instruction limit reached!
% 36.24/9.73 % (2441714)------------------------------
% 36.24/9.73 % (2441714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.24/9.73 % (2441714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.24/9.73 % (2441714)CaDiCaL version: 2.1.3
% 36.24/9.73 % (2441714)Termination reason: Instruction limit
% 36.24/9.73 % (2441714)Termination phase: Saturation
% 36.24/9.73 % (2441714)Time elapsed: 5.424 s
% 36.24/9.73 % (2441714)Peak memory usage: 167 MB
% 36.24/9.73 % (2441714)Instructions burned: 5208 (million)
% 36.24/9.73 % (2441743)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=2459817579:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2931 on theBenchmark for (2931ds/303Mi)
% 36.24/9.73 % (2441743)Refutation not found, incomplete strategy
% 36.24/9.73 % (2441743)------------------------------
% 36.24/9.73 % (2441743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.24/9.73 % (2441743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.24/9.73 % (2441743)CaDiCaL version: 2.1.3
% 36.24/9.73 % (2441743)Termination reason: Refutation not found, incomplete strategy
% 36.24/9.73 % (2441743)Time elapsed: 0.003 s
% 36.24/9.73 % (2441743)Peak memory usage: 88 MB
% 36.24/9.73 % (2441743)Instructions burned: 1 (million)
% 36.24/9.73 % (2441745)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2317540827:st=4:i=720:sd=3:fsr=off:ss=axioms_2928 on theBenchmark for (2928ds/720Mi)
% 36.24/9.73 % (2441745)Refutation not found, incomplete strategy
% 36.24/9.73 % (2441745)------------------------------
% 36.24/9.73 % (2441745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.24/9.73 % (2441745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.24/9.73 % (2441745)CaDiCaL version: 2.1.3
% 36.24/9.73 % (2441745)Termination reason: Refutation not found, incomplete strategy
% 36.24/9.73 % (2441745)Time elapsed: 0.002 s
% 36.24/9.73 % (2441745)Peak memory usage: 88 MB
% 36.24/9.73 % (2441743)------------------------------
% 36.24/9.73 % (2441743)------------------------------
% 36.24/9.73 % (2441745)------------------------------
% 36.24/9.73 % (2441745)------------------------------
% 36.24/9.73 % (2441747)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=4200722222:i=598:bs=on:bd=preordered:av=off:ss=axioms_2924 on theBenchmark for (2924ds/598Mi)
% 36.24/9.73 % (2441748)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1761318529:i=2989:sd=3:ss=axioms:sgt=60_2922 on theBenchmark for (2922ds/2989Mi)
% 36.24/9.73 % (2441747)Instruction limit reached!
% 36.24/9.73 % (2441747)------------------------------
% 36.24/9.73 % (2441747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.24/9.73 % (2441747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.24/9.73 % (2441747)CaDiCaL version: 2.1.3
% 36.24/9.73 % (2441747)Termination reason: Instruction limit
% 36.24/9.73 % (2441747)Termination phase: Saturation
% 36.24/9.73 % (2441747)Time elapsed: 0.630 s
% 36.24/9.73 % (2441747)Peak memory usage: 94 MB
% 36.24/9.73 % (2441747)Instructions burned: 599 (million)
% 36.24/9.73 % (2441682)First to succeed.
% 36.24/9.73 % (2441682)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2441676"
% 36.24/9.73 % (2441751)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=2681141996:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2915 on theBenchmark for (2915ds/1997Mi)
% 36.24/9.73 % (2441682)Refutation found. Thanks to Tanya!
% 36.24/9.73 % SZS status Unsatisfiable for theBenchmark
% 36.24/9.73 % SZS output start Proof for theBenchmark
% See solution above
% 62.86/9.93 % (2441682)------------------------------
% 62.86/9.93 % (2441682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.86/9.93 % (2441682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.86/9.93 % (2441682)CaDiCaL version: 2.1.3
% 62.86/9.93 % (2441682)Termination reason: Refutation
% 62.86/9.93 % (2441682)Time elapsed: 8.213 s
% 62.86/9.93 % (2441682)Peak memory usage: 230 MB
% 62.86/9.93 % (2441682)Instructions burned: 14271 (million)
% 62.86/9.93 % (2441682)------------------------------
% 62.86/9.93 % (2441682)------------------------------
% 62.86/9.93 % (2441676)Success in time 8.787 s
% 62.86/9.93 % Vampire exiting
%------------------------------------------------------------------------------