%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT214-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 : n009.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:16 AM UTC 2026
% Result : Unsatisfiable 13.95s 2.88s
% Output : Refutation 14.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 98
% Number of leaves : 12
% Syntax : Number of formulae : 424 ( 410 unt; 0 def)
% Number of atoms : 441 ( 440 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 36 ( 19 ~; 17 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 9 ( 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 : 1122 (1122 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0] : join(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_of_join) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_meet) ).
fof(f8,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f9,axiom,
! [X0] : join(X0,complement(X0)) = 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,X3,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,X3)))) = meet(X0,join(meet(X0,join(X1,meet(X0,X2))),meet(X2,X3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equation_H79) ).
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(f29,plain,
! [X0,X1] : join(X1,X0) = join(join(X1,X0),X0),
inference(superposition,[],[f17,f15]) ).
fof(f31,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f29,f6]) ).
fof(f33,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f27,f5]) ).
fof(f36,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f37,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f15]) ).
fof(f46,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f52,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(X0,join(X1,X3)))) = meet(X1,join(meet(X1,join(X2,meet(X0,X1))),meet(X0,X3))),
inference(superposition,[],[f12,f5]) ).
fof(f58,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X0,join(X1,X2)))) = meet(X1,join(meet(X1,X0),meet(X0,X2))),
inference(superposition,[],[f12,f17]) ).
fof(f60,plain,
! [X2,X3,X0,X1] : meet(X0,join(X2,meet(X1,join(X0,X3)))) = meet(X0,join(meet(X0,join(meet(X0,X1),X2)),meet(X1,X3))),
inference(superposition,[],[f12,f6]) ).
fof(f65,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(X1,join(X2,X0)))) = meet(X2,join(meet(X2,join(X3,meet(X2,X1))),meet(X0,X1))),
inference(superposition,[],[f12,f5]) ).
fof(f70,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,meet(X0,join(X1,meet(X0,X2))))))) = meet(X0,meet(X0,join(X1,meet(X0,X2)))),
inference(superposition,[],[f12,f17]) ).
fof(f86,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,join(X1,meet(X2,join(X0,meet(X0,join(X1,meet(X0,X2))))))),
inference(forward_demodulation,[],[f70,f33]) ).
fof(f94,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,join(meet(X1,X0),meet(X0,X2))),
inference(forward_demodulation,[],[f58,f4]) ).
fof(f103,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,join(X1,meet(X2,X0))),
inference(forward_demodulation,[],[f86,f4]) ).
fof(f121,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f8,f4]) ).
fof(f122,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f17]) ).
fof(f128,plain,
! [X2,X0,X1] : meet(X2,join(X0,join(X1,X2))) = X2,
inference(superposition,[],[f15,f8]) ).
fof(f131,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f144,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f36,f5]) ).
fof(f146,plain,
! [X2,X0,X1] : meet(X0,join(X0,X1)) = meet(X0,join(X2,join(X0,X1))),
inference(superposition,[],[f36,f15]) ).
fof(f164,plain,
! [X2,X0,X1] : meet(X0,join(X2,join(X0,X1))) = X0,
inference(forward_demodulation,[],[f146,f3]) ).
fof(f179,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f121,f6]) ).
fof(f200,plain,
! [X0,X1] : join(X0,complement(meet(X0,X1))) = join(X0,one),
inference(superposition,[],[f121,f9]) ).
fof(f202,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(one,X1),
inference(superposition,[],[f8,f9]) ).
fof(f204,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f205,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f207,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f211,plain,
! [X0] : complement(X0) = join(complement(X0),zero),
inference(superposition,[],[f17,f10]) ).
fof(f213,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f215,plain,
! [X0] : complement(X0) = join(zero,complement(X0)),
inference(forward_demodulation,[],[f211,f6]) ).
fof(f222,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f204]) ).
fof(f226,plain,
! [X0] : one = join(one,X0),
inference(superposition,[],[f17,f204]) ).
fof(f243,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f6,f226]) ).
fof(f270,plain,
zero = complement(one),
inference(superposition,[],[f10,f222]) ).
fof(f321,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f207]) ).
fof(f324,plain,
! [X0] : zero = meet(zero,X0),
inference(superposition,[],[f15,f207]) ).
fof(f336,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f5,f324]) ).
fof(f369,plain,
one = complement(zero),
inference(superposition,[],[f9,f321]) ).
fof(f500,plain,
! [X0,X1] : meet(X0,zero) = meet(X0,complement(join(X1,X0))),
inference(superposition,[],[f37,f10]) ).
fof(f531,plain,
! [X0,X1] : zero = meet(X0,complement(join(X1,X0))),
inference(forward_demodulation,[],[f500,f336]) ).
fof(f725,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(join(X0,X1),join(X0,X2)),
inference(superposition,[],[f122,f3]) ).
fof(f769,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X2,join(X0,X1))),
inference(forward_demodulation,[],[f725,f131]) ).
fof(f777,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,join(X0,X1))),
inference(forward_demodulation,[],[f769,f8]) ).
fof(f1055,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(X0),join(X0,X2)))) = meet(X0,join(meet(X0,join(X1,zero)),meet(X2,complement(X0)))),
inference(superposition,[],[f65,f10]) ).
fof(f1101,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(meet(X0,X1),join(X2,meet(X1,join(meet(X0,X1),X0)))),
inference(superposition,[],[f15,f65]) ).
fof(f1134,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,meet(X1,join(X2,meet(X1,join(meet(X0,X1),X0))))),
inference(forward_demodulation,[],[f1101,f7]) ).
fof(f1172,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(X0),join(X0,X2)))) = meet(X0,join(meet(X0,X1),meet(X2,complement(X0)))),
inference(forward_demodulation,[],[f1055,f207]) ).
fof(f1188,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,meet(X1,join(X2,meet(X1,join(X0,meet(X0,X1)))))),
inference(forward_demodulation,[],[f1134,f6]) ).
fof(f1224,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,meet(X1,join(X2,meet(X1,X0)))),
inference(forward_demodulation,[],[f1188,f4]) ).
fof(f1287,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(complement(X0),join(X0,X1)))) = meet(X0,join(zero,meet(X1,complement(X0)))),
inference(superposition,[],[f1172,f10]) ).
fof(f1296,plain,
! [X0,X1] : meet(X0,join(X1,meet(complement(X0),join(X0,one)))) = meet(X0,join(meet(X0,X1),complement(X0))),
inference(superposition,[],[f1172,f222]) ).
fof(f1307,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,complement(X0))))) = meet(X0,join(join(X1,meet(X0,X2)),meet(complement(X0),join(X0,X2)))),
inference(superposition,[],[f12,f1172]) ).
fof(f1349,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,complement(X0))))) = meet(X0,join(X1,join(meet(X0,X2),meet(complement(X0),join(X0,X2))))),
inference(forward_demodulation,[],[f1307,f8]) ).
fof(f1357,plain,
! [X0,X1] : meet(X0,join(X1,meet(complement(X0),join(X0,one)))) = meet(X0,join(complement(X0),meet(X0,X1))),
inference(forward_demodulation,[],[f1296,f6]) ).
fof(f1363,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(complement(X0),join(X0,X1)))) = meet(X0,meet(X1,complement(X0))),
inference(forward_demodulation,[],[f1287,f321]) ).
fof(f1383,plain,
! [X2,X0,X1] : meet(X0,join(X1,join(meet(X0,X2),meet(complement(X0),join(X0,X2))))) = meet(X0,join(X1,meet(X2,one))),
inference(forward_demodulation,[],[f1349,f9]) ).
fof(f1391,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X0,X1))) = meet(X0,join(X1,meet(complement(X0),one))),
inference(forward_demodulation,[],[f1357,f243]) ).
fof(f1396,plain,
! [X0,X1] : meet(X0,complement(X0)) = meet(X0,meet(X1,complement(X0))),
inference(forward_demodulation,[],[f1363,f4]) ).
fof(f1408,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X1,join(meet(X0,X2),meet(complement(X0),join(X0,X2))))),
inference(forward_demodulation,[],[f1383,f204]) ).
fof(f1414,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X0,X1))) = meet(X0,join(X1,meet(one,complement(X0)))),
inference(forward_demodulation,[],[f1391,f5]) ).
fof(f1417,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(X0))),
inference(forward_demodulation,[],[f1396,f10]) ).
fof(f1427,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X0,X1))) = meet(X0,join(X1,complement(X0))),
inference(forward_demodulation,[],[f1414,f222]) ).
fof(f1479,plain,
! [X2,X0,X1] : meet(X0,zero) = meet(X0,meet(X1,complement(join(X0,X2)))),
inference(superposition,[],[f36,f1417]) ).
fof(f1482,plain,
! [X2,X0,X1] : zero = meet(X0,meet(X1,complement(join(X0,X2)))),
inference(forward_demodulation,[],[f1479,f336]) ).
fof(f1872,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = join(meet(X1,join(X2,meet(X1,X0))),meet(X0,X1)),
inference(superposition,[],[f17,f1224]) ).
fof(f1905,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = join(meet(X0,X1),meet(X1,join(X2,meet(X1,X0)))),
inference(forward_demodulation,[],[f1872,f6]) ).
fof(f2073,plain,
! [X2,X3,X0,X1] : join(X2,join(X0,X1)) = join(X2,join(X0,join(X1,meet(X2,X3)))),
inference(superposition,[],[f121,f131]) ).
fof(f2158,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,f205]) ).
fof(f2170,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f2158]) ).
fof(f2214,plain,
! [X0,X1] :
( zero != meet(X1,join(X0,complement(join(X0,X1))))
| complement(X1) = join(X0,complement(join(X0,X1))) ),
inference(superposition,[],[f2170,f6]) ).
fof(f2329,plain,
! [X0,X1] : zero = meet(X0,complement(join(X0,X1))),
inference(superposition,[],[f37,f1482]) ).
fof(f2921,plain,
! [X0,X1] :
( one != join(one,X0)
| zero != meet(X1,join(complement(X1),X0))
| complement(X1) = join(complement(X1),X0) ),
inference(superposition,[],[f11,f202]) ).
fof(f2928,plain,
! [X2,X0,X1] : meet(X1,join(X2,join(complement(X1),X0))) = meet(X1,join(X2,join(meet(X1,join(complement(X1),X0)),meet(complement(X1),join(one,X0))))),
inference(superposition,[],[f1408,f202]) ).
fof(f2945,plain,
! [X2,X0,X1] : meet(X1,join(X2,join(complement(X1),X0))) = meet(X1,join(X2,join(meet(X1,join(complement(X1),X0)),meet(complement(X1),one)))),
inference(forward_demodulation,[],[f2928,f226]) ).
fof(f2952,plain,
! [X0,X1] :
( zero != meet(X1,join(complement(X1),X0))
| complement(X1) = join(complement(X1),X0) ),
inference(forward_subsumption_resolution,[],[f2921,f226]) ).
fof(f2979,plain,
! [X2,X0,X1] : meet(X1,join(X2,join(complement(X1),X0))) = meet(X1,join(X2,join(meet(complement(X1),one),meet(X1,join(complement(X1),X0))))),
inference(forward_demodulation,[],[f2945,f6]) ).
fof(f2990,plain,
! [X2,X0,X1] : meet(X1,join(X2,join(complement(X1),X0))) = meet(X1,join(X2,join(meet(one,complement(X1)),meet(X1,join(complement(X1),X0))))),
inference(forward_demodulation,[],[f2979,f5]) ).
fof(f2996,plain,
! [X2,X0,X1] : meet(X1,join(X2,join(complement(X1),X0))) = meet(X1,join(X2,join(complement(X1),meet(X1,join(complement(X1),X0))))),
inference(forward_demodulation,[],[f2990,f222]) ).
fof(f4080,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = join(meet(X1,join(X0,X2)),meet(X0,X1)),
inference(superposition,[],[f17,f144]) ).
fof(f4125,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = join(meet(X0,X1),meet(X1,join(X0,X2))),
inference(forward_demodulation,[],[f4080,f6]) ).
fof(f4205,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,join(X2,meet(X1,X0))),
inference(superposition,[],[f103,f6]) ).
fof(f4288,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(join(X1,meet(X2,X0)),meet(X0,join(X1,meet(X0,X2)))),
inference(superposition,[],[f17,f103]) ).
fof(f4331,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,join(meet(X2,X0),meet(X0,join(X1,meet(X0,X2))))),
inference(forward_demodulation,[],[f4288,f8]) ).
fof(f4381,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,meet(X0,join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f4331,f1905]) ).
fof(f4424,plain,
! [X2,X3,X0,X1] : join(X2,meet(meet(X1,join(X0,X3)),X0)) = join(X2,meet(X0,join(X2,meet(X0,X1)))),
inference(superposition,[],[f4381,f144]) ).
fof(f4563,plain,
! [X2,X3,X0,X1] : join(X2,meet(X1,X0)) = join(X2,meet(meet(X1,join(X0,X3)),X0)),
inference(forward_demodulation,[],[f4424,f4381]) ).
fof(f4614,plain,
! [X2,X3,X0,X1] : join(X2,meet(X1,X0)) = join(X2,meet(X0,meet(X1,join(X0,X3)))),
inference(forward_demodulation,[],[f4563,f5]) ).
fof(f4649,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f4614,f144]) ).
fof(f4969,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,meet(X1,X2))) = join(X3,meet(X2,meet(X0,X1))),
inference(superposition,[],[f4649,f7]) ).
fof(f5040,plain,
! [X2,X3,X0,X1] : join(X3,join(X0,meet(X1,X2))) = join(meet(X2,X1),join(X3,X0)),
inference(superposition,[],[f131,f4649]) ).
fof(f5187,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,complement(X2))))) = meet(X0,join(meet(X0,join(meet(X0,X2),X1)),zero)),
inference(superposition,[],[f60,f10]) ).
fof(f5258,plain,
! [X2,X0,X1] : meet(one,join(X0,meet(X1,join(one,X2)))) = join(meet(one,join(meet(one,X1),X0)),meet(X1,X2)),
inference(superposition,[],[f222,f60]) ).
fof(f5260,plain,
! [X2,X0,X1] : meet(one,join(X0,meet(X1,join(one,X2)))) = join(join(meet(one,X1),X0),meet(X1,X2)),
inference(forward_demodulation,[],[f5258,f222]) ).
fof(f5310,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,complement(X2))))) = meet(X0,join(zero,meet(join(meet(X0,X2),X1),X0))),
inference(forward_demodulation,[],[f5187,f4205]) ).
fof(f5389,plain,
! [X2,X0,X1] : meet(one,join(X0,meet(X1,join(one,X2)))) = join(meet(one,X1),join(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f5260,f8]) ).
fof(f5425,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,complement(X2))))) = meet(X0,join(zero,meet(X0,join(meet(X0,X2),X1)))),
inference(forward_demodulation,[],[f5310,f103]) ).
fof(f5477,plain,
! [X2,X0,X1] : join(X1,join(X0,meet(X1,X2))) = meet(one,join(X0,meet(X1,join(one,X2)))),
inference(forward_demodulation,[],[f5389,f222]) ).
fof(f5504,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,complement(X2))))) = meet(X0,meet(X0,join(meet(X0,X2),X1))),
inference(forward_demodulation,[],[f5425,f321]) ).
fof(f5542,plain,
! [X2,X0,X1] : join(X1,join(X0,meet(X1,X2))) = join(X0,meet(X1,join(one,X2))),
inference(forward_demodulation,[],[f5477,f222]) ).
fof(f5559,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,complement(X2))))) = meet(X0,join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f5504,f33]) ).
fof(f5580,plain,
! [X2,X0,X1] : join(X1,join(X0,meet(X1,X2))) = join(X0,meet(X1,one)),
inference(forward_demodulation,[],[f5542,f226]) ).
fof(f5599,plain,
! [X2,X0,X1] : join(X0,X1) = join(X1,join(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f5580,f204]) ).
fof(f5669,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),complement(X0))) = meet(X0,join(complement(X0),X1)),
inference(superposition,[],[f1408,f5599]) ).
fof(f5716,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X1,X0))) = meet(X0,join(complement(X0),X1)),
inference(forward_demodulation,[],[f5669,f4205]) ).
fof(f5779,plain,
! [X0] : meet(complement(X0),join(complement(complement(X0)),X0)) = meet(complement(X0),join(complement(complement(X0)),zero)),
inference(superposition,[],[f5716,f10]) ).
fof(f5826,plain,
! [X2,X0,X1] : meet(X0,join(X2,join(complement(X0),meet(X1,X0)))) = meet(X0,join(X2,join(meet(X0,join(complement(X0),X1)),meet(complement(X0),join(X0,join(complement(X0),meet(X1,X0))))))),
inference(superposition,[],[f1408,f5716]) ).
fof(f5845,plain,
! [X2,X0,X1] : meet(X0,join(X2,join(complement(X0),meet(X1,X0)))) = meet(X0,join(X2,join(meet(X0,join(complement(X0),X1)),complement(X0)))),
inference(forward_demodulation,[],[f5826,f164]) ).
fof(f5870,plain,
! [X0] : meet(complement(X0),join(complement(complement(X0)),X0)) = meet(complement(X0),join(zero,complement(complement(X0)))),
inference(forward_demodulation,[],[f5779,f6]) ).
fof(f5898,plain,
! [X2,X0,X1] : meet(X0,join(X2,join(complement(X0),meet(X1,X0)))) = meet(X0,join(X2,join(complement(X0),meet(X0,join(complement(X0),X1))))),
inference(forward_demodulation,[],[f5845,f6]) ).
fof(f5911,plain,
! [X0] : meet(complement(X0),complement(complement(X0))) = meet(complement(X0),join(complement(complement(X0)),X0)),
inference(forward_demodulation,[],[f5870,f215]) ).
fof(f5935,plain,
! [X2,X0,X1] : meet(X0,join(X2,join(complement(X0),meet(X1,X0)))) = meet(X0,join(X2,join(complement(X0),X1))),
inference(forward_demodulation,[],[f5898,f2996]) ).
fof(f5947,plain,
! [X0] : meet(complement(X0),complement(complement(X0))) = meet(complement(X0),join(X0,complement(complement(X0)))),
inference(forward_demodulation,[],[f5911,f6]) ).
fof(f5966,plain,
! [X0] : zero = meet(complement(X0),join(X0,complement(complement(X0)))),
inference(forward_demodulation,[],[f5947,f10]) ).
fof(f7562,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,complement(one)))
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(superposition,[],[f2214,f9]) ).
fof(f7594,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,zero))
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(forward_demodulation,[],[f7562,f270]) ).
fof(f7618,plain,
! [X0] :
( zero != meet(complement(X0),X0)
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(forward_demodulation,[],[f7594,f207]) ).
fof(f7633,plain,
! [X0] :
( meet(X0,complement(X0)) != zero
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(forward_demodulation,[],[f7618,f5]) ).
fof(f7644,plain,
! [X0] : complement(complement(X0)) = join(X0,complement(one)),
inference(forward_subsumption_resolution,[],[f7633,f10]) ).
fof(f7653,plain,
! [X0] : join(X0,zero) = complement(complement(X0)),
inference(forward_demodulation,[],[f7644,f270]) ).
fof(f7659,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f7653,f207]) ).
fof(f9013,plain,
! [X0,X1] : meet(X0,join(complement(X0),zero)) = meet(X0,join(meet(X1,complement(meet(X0,X1))),complement(X0))),
inference(superposition,[],[f1427,f213]) ).
fof(f9077,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = join(join(complement(X0),meet(X0,X1)),meet(X0,join(X1,complement(X0)))),
inference(superposition,[],[f17,f1427]) ).
fof(f9141,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = join(meet(X0,join(X1,complement(X0))),join(complement(X0),meet(X0,X1))),
inference(forward_demodulation,[],[f9077,f6]) ).
fof(f9188,plain,
! [X0,X1] : meet(X0,join(complement(X0),zero)) = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f9013,f6]) ).
fof(f9214,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = join(meet(X1,X0),join(meet(X0,join(X1,complement(X0))),complement(X0))),
inference(forward_demodulation,[],[f9141,f5040]) ).
fof(f9257,plain,
! [X0,X1] : meet(X0,join(zero,complement(X0))) = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f9188,f6]) ).
fof(f9272,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = join(complement(X0),join(meet(X1,X0),meet(X0,join(X1,complement(X0))))),
inference(forward_demodulation,[],[f9214,f131]) ).
fof(f9306,plain,
! [X0,X1] : meet(X0,complement(X0)) = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f9257,f215]) ).
fof(f9312,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = join(complement(X0),meet(X0,join(X1,complement(X0)))),
inference(forward_demodulation,[],[f9272,f4125]) ).
fof(f9329,plain,
! [X0,X1] : zero = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f9306,f10]) ).
fof(f9347,plain,
! [X0,X1] : join(X0,meet(complement(X0),X1)) = join(X0,meet(complement(X0),join(X1,X0))),
inference(superposition,[],[f9312,f7659]) ).
fof(f9735,plain,
! [X0,X1] :
( zero != zero
| complement(X0) = join(complement(X0),meet(X1,complement(meet(X0,X1)))) ),
inference(superposition,[],[f2952,f9329]) ).
fof(f9786,plain,
! [X0,X1] : complement(X0) = join(complement(X0),meet(X1,complement(meet(X0,X1)))),
inference(trivial_inequality_removal,[],[f9735]) ).
fof(f10046,plain,
! [X0,X1] : complement(X0) = join(complement(X0),meet(complement(join(X0,X1)),complement(zero))),
inference(superposition,[],[f9786,f2329]) ).
fof(f10047,plain,
! [X0,X1] : complement(X0) = join(complement(X0),meet(complement(join(X1,X0)),complement(zero))),
inference(superposition,[],[f9786,f531]) ).
fof(f10074,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(meet(X1,complement(meet(X0,X1))),complement(X0)),
inference(superposition,[],[f15,f9786]) ).
fof(f10104,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f10074,f5]) ).
fof(f10120,plain,
! [X0,X1] : complement(X0) = join(complement(X0),meet(complement(zero),complement(join(X1,X0)))),
inference(forward_demodulation,[],[f10047,f4649]) ).
fof(f10121,plain,
! [X0,X1] : complement(X0) = join(complement(X0),meet(complement(zero),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f10046,f4649]) ).
fof(f10159,plain,
! [X0,X1] : complement(X0) = join(complement(X0),meet(one,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f10120,f369]) ).
fof(f10160,plain,
! [X0,X1] : complement(X0) = join(complement(X0),meet(one,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f10121,f369]) ).
fof(f10176,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f10159,f222]) ).
fof(f10177,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f10160,f222]) ).
fof(f10229,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f15,f10177]) ).
fof(f10259,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f10229,f5]) ).
fof(f10285,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),X1))),
inference(superposition,[],[f10259,f7659]) ).
fof(f10303,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(join(X0,X1))),
inference(superposition,[],[f10259,f5599]) ).
fof(f10433,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),complement(X0)),
inference(superposition,[],[f10176,f4]) ).
fof(f10434,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(meet(X1,X0)),complement(X0)),
inference(superposition,[],[f10176,f17]) ).
fof(f10523,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f10434,f6]) ).
fof(f10524,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f10433,f6]) ).
fof(f10557,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(meet(complement(X0),X1))),
inference(superposition,[],[f10524,f7659]) ).
fof(f10614,plain,
! [X0,X1] : complement(X0) = meet(complement(X0),complement(meet(X0,X1))),
inference(superposition,[],[f3,f10524]) ).
fof(f10629,plain,
! [X2,X0,X1] : meet(complement(X0),join(X2,complement(meet(X0,X1)))) = meet(complement(X0),join(X2,join(meet(complement(X0),complement(meet(X0,X1))),meet(complement(complement(X0)),complement(meet(X0,X1)))))),
inference(superposition,[],[f1408,f10524]) ).
fof(f10647,plain,
! [X2,X0,X1] : meet(complement(X0),join(X2,complement(meet(X0,X1)))) = meet(complement(X0),join(X2,join(meet(complement(X0),complement(meet(X0,X1))),meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f10629,f7659]) ).
fof(f10679,plain,
! [X2,X0,X1] : meet(complement(X0),join(X2,complement(meet(X0,X1)))) = meet(complement(X0),join(X2,join(meet(X0,complement(meet(X0,X1))),meet(complement(X0),complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f10647,f6]) ).
fof(f10692,plain,
! [X2,X0,X1] : meet(complement(X0),join(X2,complement(meet(X0,X1)))) = meet(complement(X0),join(X2,join(meet(X0,complement(meet(X0,X1))),complement(X0)))),
inference(forward_demodulation,[],[f10679,f10614]) ).
fof(f10702,plain,
! [X2,X0,X1] : complement(X0) = meet(complement(X0),join(X2,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f10692,f128]) ).
fof(f10717,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X1,X0)),complement(X0)),
inference(superposition,[],[f10303,f17]) ).
fof(f10840,plain,
! [X0,X1] : complement(X0) = meet(complement(X0),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f10717,f5]) ).
fof(f10905,plain,
! [X0,X1] : meet(X0,complement(meet(X1,complement(X0)))) = X0,
inference(superposition,[],[f10840,f7659]) ).
fof(f10992,plain,
! [X2,X0,X1] : meet(complement(X0),join(X1,complement(meet(X2,X0)))) = meet(complement(X0),join(X1,join(complement(X0),meet(complement(complement(X0)),join(complement(X0),complement(meet(X2,X0))))))),
inference(superposition,[],[f1408,f10840]) ).
fof(f11006,plain,
! [X2,X0,X1] : complement(X0) = meet(complement(X0),join(X1,complement(meet(X2,X0)))),
inference(forward_demodulation,[],[f10992,f164]) ).
fof(f11345,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(X2,complement(meet(complement(X0),X1)))),
inference(superposition,[],[f144,f10557]) ).
fof(f11511,plain,
! [X2,X0,X1] : meet(complement(X1),X2) = meet(complement(X1),meet(X2,complement(meet(X0,X1)))),
inference(superposition,[],[f144,f10523]) ).
fof(f11809,plain,
! [X2,X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),join(X2,complement(X0))),
inference(superposition,[],[f11006,f3]) ).
fof(f12113,plain,
! [X2,X3,X0,X1] : join(X2,complement(join(X0,X1))) = join(X2,meet(join(X3,complement(X0)),complement(join(X0,X1)))),
inference(superposition,[],[f4649,f11809]) ).
fof(f13001,plain,
! [X0,X1] : meet(X1,complement(meet(complement(X0),X1))) = meet(X0,meet(X1,complement(meet(complement(X0),X1)))),
inference(superposition,[],[f10104,f7659]) ).
fof(f13004,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = meet(complement(X1),meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f10104,f5]) ).
fof(f13192,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f13004,f11511]) ).
fof(f13194,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,complement(meet(complement(X0),X1))),
inference(forward_demodulation,[],[f13001,f11345]) ).
fof(f13286,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),X1),
inference(superposition,[],[f13192,f5]) ).
fof(f13389,plain,
! [X2,X0,X1] : meet(X1,join(X2,complement(meet(X1,X0)))) = meet(X1,join(X2,join(meet(complement(X0),X1),meet(complement(X1),join(X1,complement(meet(X1,X0))))))),
inference(superposition,[],[f1408,f13192]) ).
fof(f13390,plain,
! [X0,X1] : meet(X1,join(complement(meet(X1,X0)),complement(X1))) = meet(X1,join(complement(X1),meet(complement(X0),X1))),
inference(superposition,[],[f1427,f13192]) ).
fof(f13431,plain,
! [X0,X1] : meet(X1,join(complement(meet(X1,X0)),complement(X1))) = meet(X1,join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f13390,f5716]) ).
fof(f13432,plain,
! [X2,X0,X1] : meet(X1,join(X2,complement(meet(X1,X0)))) = meet(X1,join(X2,join(meet(complement(X0),X1),complement(X1)))),
inference(forward_demodulation,[],[f13389,f10702]) ).
fof(f13513,plain,
! [X0,X1] : meet(X1,join(complement(X1),complement(meet(X1,X0)))) = meet(X1,join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f13431,f6]) ).
fof(f13514,plain,
! [X2,X0,X1] : meet(X1,join(X2,complement(meet(X1,X0)))) = meet(X1,join(X2,join(complement(X1),meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f13432,f6]) ).
fof(f13577,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(X1,join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f13513,f10524]) ).
fof(f13578,plain,
! [X2,X0,X1] : meet(X1,join(X2,complement(meet(X1,X0)))) = meet(X1,join(X2,join(complement(X1),complement(X0)))),
inference(forward_demodulation,[],[f13514,f5935]) ).
fof(f13621,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(X1,join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f13577,f13192]) ).
fof(f13760,plain,
! [X0,X1] : meet(X1,join(complement(X1),meet(X0,X1))) = meet(X1,join(complement(meet(complement(X0),X1)),complement(X1))),
inference(superposition,[],[f1427,f13194]) ).
fof(f13805,plain,
! [X0,X1] : meet(X1,join(complement(X1),meet(X0,X1))) = meet(X1,join(complement(X1),complement(meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f13760,f6]) ).
fof(f13910,plain,
! [X0,X1] : meet(X1,join(complement(X1),meet(X0,X1))) = meet(complement(meet(complement(X0),X1)),X1),
inference(forward_demodulation,[],[f13805,f13621]) ).
fof(f13974,plain,
! [X0,X1] : meet(X1,complement(meet(complement(X0),X1))) = meet(X1,join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[],[f13910,f5]) ).
fof(f14009,plain,
! [X0,X1] : meet(X1,complement(meet(complement(X0),X1))) = meet(X1,join(complement(X1),X0)),
inference(forward_demodulation,[],[f13974,f5716]) ).
fof(f14026,plain,
! [X0,X1] : meet(X1,join(complement(X1),X0)) = meet(complement(complement(X0)),X1),
inference(forward_demodulation,[],[f14009,f13286]) ).
fof(f14038,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(complement(X1),X0)),
inference(forward_demodulation,[],[f14026,f7659]) ).
fof(f14047,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(X1,complement(X0)),
inference(superposition,[],[f14038,f7659]) ).
fof(f14057,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(X0,complement(X1))),
inference(superposition,[],[f14038,f6]) ).
fof(f14069,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(X2,join(X0,join(X1,complement(X2)))),
inference(superposition,[],[f14038,f131]) ).
fof(f14070,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = meet(X1,join(X0,join(complement(X1),X2))),
inference(superposition,[],[f14038,f131]) ).
fof(f14153,plain,
! [X2,X0,X1] : meet(X1,join(X2,join(complement(X1),X0))) = meet(X1,join(X2,join(meet(X0,X1),meet(complement(X1),join(X1,join(complement(X1),X0)))))),
inference(superposition,[],[f1408,f14038]) ).
fof(f14170,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(join(complement(X1),X0)),X1),
inference(superposition,[],[f13192,f14038]) ).
fof(f14193,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(X1,complement(join(complement(X1),X0))),
inference(forward_demodulation,[],[f14170,f5]) ).
fof(f14204,plain,
! [X2,X0,X1] : meet(X1,join(X2,join(complement(X1),X0))) = meet(X1,join(X2,join(meet(X0,X1),complement(X1)))),
inference(forward_demodulation,[],[f14153,f164]) ).
fof(f14279,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = complement(join(complement(X1),X0)),
inference(forward_demodulation,[],[f14193,f10285]) ).
fof(f14286,plain,
! [X2,X0,X1] : meet(X1,join(X2,join(complement(X1),X0))) = meet(join(X2,meet(X0,X1)),X1),
inference(forward_demodulation,[],[f14204,f14069]) ).
fof(f14349,plain,
! [X0,X1] : meet(complement(X0),X1) = complement(join(complement(X1),X0)),
inference(forward_demodulation,[],[f14279,f13286]) ).
fof(f14352,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,X1))) = meet(X1,join(X2,join(complement(X1),X0))),
inference(forward_demodulation,[],[f14286,f5]) ).
fof(f14380,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,X1))) = meet(join(X0,X2),X1),
inference(forward_demodulation,[],[f14352,f14070]) ).
fof(f14414,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,X1)) = meet(join(meet(X0,X2),X1),complement(X0)),
inference(superposition,[],[f14047,f121]) ).
fof(f14415,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,X1)) = meet(join(meet(X2,X0),X1),complement(X0)),
inference(superposition,[],[f14047,f122]) ).
fof(f14493,plain,
! [X2,X0,X1] : meet(complement(X1),meet(join(X1,X0),X2)) = meet(X2,meet(X0,complement(X1))),
inference(superposition,[],[f46,f14047]) ).
fof(f14533,plain,
! [X0,X1] : meet(complement(X1),complement(meet(X0,complement(X1)))) = meet(complement(join(X1,X0)),complement(X1)),
inference(superposition,[],[f13192,f14047]) ).
fof(f14534,plain,
! [X0,X1] : meet(complement(X1),complement(meet(X0,complement(X1)))) = meet(complement(X1),complement(join(X1,X0))),
inference(forward_demodulation,[],[f14533,f5]) ).
fof(f14618,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),join(meet(X2,X0),X1)),
inference(forward_demodulation,[],[f14415,f5]) ).
fof(f14619,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f14414,f5]) ).
fof(f14627,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X1),complement(meet(X0,complement(X1)))),
inference(forward_demodulation,[],[f14534,f10259]) ).
fof(f14693,plain,
! [X2,X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(meet(X2,X0),X1)),
inference(forward_demodulation,[],[f14618,f14047]) ).
fof(f14694,plain,
! [X2,X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f14619,f14047]) ).
fof(f14702,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(X1)),
inference(forward_demodulation,[],[f14627,f13286]) ).
fof(f14818,plain,
! [X0,X1] : meet(X0,complement(X1)) = complement(join(X1,complement(X0))),
inference(superposition,[],[f14702,f7659]) ).
fof(f14874,plain,
! [X2,X0,X1] : meet(X2,complement(join(X0,X1))) = meet(complement(X0),meet(X2,complement(X1))),
inference(superposition,[],[f46,f14702]) ).
fof(f14899,plain,
! [X0,X1] : meet(complement(X1),join(complement(complement(X1)),complement(join(X0,X1)))) = meet(complement(X1),join(complement(X0),complement(complement(X1)))),
inference(superposition,[],[f1427,f14702]) ).
fof(f14934,plain,
! [X0,X1] : meet(complement(X0),complement(X1)) = meet(complement(X1),join(complement(complement(X1)),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f14899,f14057]) ).
fof(f14998,plain,
! [X0,X1] : meet(complement(X0),complement(X1)) = meet(complement(join(X0,X1)),complement(X1)),
inference(forward_demodulation,[],[f14934,f13621]) ).
fof(f15042,plain,
! [X0,X1] : meet(complement(X1),complement(join(X0,X1))) = meet(complement(X0),complement(X1)),
inference(forward_demodulation,[],[f14998,f5]) ).
fof(f15065,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X1),complement(join(X0,X1))),
inference(forward_demodulation,[],[f15042,f14702]) ).
fof(f15079,plain,
! [X0,X1] : complement(join(X1,X0)) = complement(join(join(X0,X1),X1)),
inference(forward_demodulation,[],[f15065,f14702]) ).
fof(f15087,plain,
! [X0,X1] : complement(join(X1,X0)) = complement(join(X1,join(X0,X1))),
inference(forward_demodulation,[],[f15079,f6]) ).
fof(f15090,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f15087,f31]) ).
fof(f15440,plain,
! [X2,X0,X1] : meet(join(X1,complement(X0)),complement(X2)) = complement(join(X2,meet(X0,complement(X1)))),
inference(superposition,[],[f14818,f14818]) ).
fof(f15490,plain,
! [X0,X1] : join(X1,complement(X0)) = complement(meet(X0,complement(X1))),
inference(superposition,[],[f7659,f14818]) ).
fof(f15517,plain,
! [X2,X0,X1] : complement(join(join(X1,complement(X0)),X2)) = meet(complement(X2),meet(X0,complement(X1))),
inference(superposition,[],[f14702,f14818]) ).
fof(f15520,plain,
! [X2,X0,X1] : complement(join(join(X1,complement(X0)),X2)) = meet(X0,complement(join(X2,X1))),
inference(forward_demodulation,[],[f15517,f14874]) ).
fof(f15576,plain,
! [X2,X0,X1] : complement(join(X1,join(complement(X0),X2))) = meet(X0,complement(join(X2,X1))),
inference(forward_demodulation,[],[f15520,f8]) ).
fof(f16037,plain,
! [X2,X0,X1] : meet(X1,join(X2,join(complement(X1),complement(X0)))) = meet(X1,join(X2,join(meet(complement(X0),X1),meet(complement(X1),join(X1,join(complement(X1),complement(X0))))))),
inference(superposition,[],[f1408,f13621]) ).
fof(f16090,plain,
! [X2,X0,X1] : meet(X1,join(X2,join(meet(complement(X0),X1),complement(X1)))) = meet(X1,join(X2,join(complement(X1),complement(X0)))),
inference(forward_demodulation,[],[f16037,f164]) ).
fof(f16132,plain,
! [X2,X0,X1] : meet(X1,join(X2,complement(meet(X1,X0)))) = meet(X1,join(X2,join(meet(complement(X0),X1),complement(X1)))),
inference(forward_demodulation,[],[f16090,f13578]) ).
fof(f16159,plain,
! [X2,X0,X1] : meet(join(X2,meet(complement(X0),X1)),X1) = meet(X1,join(X2,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f16132,f14069]) ).
fof(f16173,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(complement(X0),X1))) = meet(X1,join(X2,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f16159,f5]) ).
fof(f16177,plain,
! [X2,X0,X1] : meet(join(complement(X0),X2),X1) = meet(X1,join(X2,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f16173,f14380]) ).
fof(f16183,plain,
! [X2,X0,X1] : meet(join(complement(X0),X2),X1) = meet(X1,join(X2,complement(meet(X0,X1)))),
inference(superposition,[],[f16177,f5]) ).
fof(f16226,plain,
! [X2,X0,X1] : meet(X1,join(X2,complement(meet(complement(X0),X1)))) = meet(join(complement(complement(meet(X1,X0))),X2),X1),
inference(superposition,[],[f16177,f13192]) ).
fof(f16227,plain,
! [X2,X0,X1] : meet(X1,join(X2,complement(meet(X0,X1)))) = meet(join(complement(complement(meet(complement(X0),X1))),X2),X1),
inference(superposition,[],[f16177,f13194]) ).
fof(f16251,plain,
! [X0,X1] : meet(X1,one) = meet(join(complement(X0),meet(X1,X0)),X1),
inference(superposition,[],[f16177,f9]) ).
fof(f16400,plain,
! [X0,X1] : meet(X1,one) = meet(X1,join(complement(X0),meet(X1,X0))),
inference(forward_demodulation,[],[f16251,f5]) ).
fof(f16424,plain,
! [X2,X0,X1] : meet(X1,join(X2,complement(meet(X0,X1)))) = meet(X1,join(complement(complement(meet(complement(X0),X1))),X2)),
inference(forward_demodulation,[],[f16227,f5]) ).
fof(f16425,plain,
! [X2,X0,X1] : meet(X1,join(X2,complement(meet(complement(X0),X1)))) = meet(X1,join(complement(complement(meet(X1,X0))),X2)),
inference(forward_demodulation,[],[f16226,f5]) ).
fof(f16517,plain,
! [X0,X1] : meet(X1,join(complement(X0),meet(X1,X0))) = X1,
inference(forward_demodulation,[],[f16400,f204]) ).
fof(f16540,plain,
! [X2,X0,X1] : meet(X1,join(X2,complement(meet(X0,X1)))) = meet(X1,join(meet(complement(X0),X1),X2)),
inference(forward_demodulation,[],[f16424,f7659]) ).
fof(f16541,plain,
! [X2,X0,X1] : meet(X1,join(meet(X1,X0),X2)) = meet(X1,join(X2,complement(meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f16425,f7659]) ).
fof(f16627,plain,
! [X2,X0,X1] : meet(join(complement(X0),X2),X1) = meet(X1,join(meet(complement(X0),X1),X2)),
inference(forward_demodulation,[],[f16540,f16183]) ).
fof(f16628,plain,
! [X2,X0,X1] : meet(X1,join(meet(X1,X0),X2)) = meet(join(complement(complement(X0)),X2),X1),
inference(forward_demodulation,[],[f16541,f16183]) ).
fof(f16683,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = meet(X1,join(meet(X1,X0),X2)),
inference(forward_demodulation,[],[f16628,f7659]) ).
fof(f16859,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(X1),meet(X1,X0)),
inference(superposition,[],[f4381,f16517]) ).
fof(f16872,plain,
! [X0,X1] : join(complement(X1),meet(X0,X1)) = join(join(complement(X1),meet(X0,X1)),X0),
inference(superposition,[],[f17,f16517]) ).
fof(f16888,plain,
! [X2,X0,X1] : join(join(complement(X1),meet(X0,X1)),X2) = join(join(complement(X1),meet(X0,X1)),join(X0,X2)),
inference(superposition,[],[f122,f16517]) ).
fof(f16911,plain,
! [X0,X1] : complement(join(complement(X1),meet(X0,X1))) = meet(complement(join(complement(X1),meet(X0,X1))),complement(X0)),
inference(superposition,[],[f10840,f16517]) ).
fof(f16940,plain,
! [X0,X1] : complement(join(complement(X1),meet(X0,X1))) = meet(complement(X0),complement(join(complement(X1),meet(X0,X1)))),
inference(forward_demodulation,[],[f16911,f5]) ).
fof(f16953,plain,
! [X2,X0,X1] : join(join(complement(X1),meet(X0,X1)),X2) = join(X0,join(X2,join(complement(X1),meet(X0,X1)))),
inference(forward_demodulation,[],[f16888,f131]) ).
fof(f16965,plain,
! [X0,X1] : join(complement(X1),meet(X0,X1)) = join(X0,join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[],[f16872,f6]) ).
fof(f17048,plain,
! [X0,X1] : complement(join(complement(X1),meet(X0,X1))) = complement(join(join(complement(X1),meet(X0,X1)),X0)),
inference(forward_demodulation,[],[f16940,f14702]) ).
fof(f17057,plain,
! [X2,X0,X1] : join(join(complement(X1),meet(X0,X1)),X2) = join(X0,join(X2,complement(X1))),
inference(forward_demodulation,[],[f16953,f2073]) ).
fof(f17067,plain,
! [X0,X1] : join(X0,complement(X1)) = join(complement(X1),meet(X0,X1)),
inference(forward_demodulation,[],[f16965,f179]) ).
fof(f17142,plain,
! [X0,X1] : complement(join(complement(X1),meet(X0,X1))) = complement(join(X0,join(complement(X1),meet(X0,X1)))),
inference(forward_demodulation,[],[f17048,f15090]) ).
fof(f17147,plain,
! [X2,X0,X1] : join(complement(X1),join(meet(X0,X1),X2)) = join(X0,join(X2,complement(X1))),
inference(forward_demodulation,[],[f17057,f8]) ).
fof(f17205,plain,
! [X0,X1] : complement(join(complement(X1),meet(X0,X1))) = meet(X1,complement(join(meet(X0,X1),X0))),
inference(forward_demodulation,[],[f17142,f15576]) ).
fof(f17242,plain,
! [X0,X1] : complement(join(complement(X1),meet(X0,X1))) = meet(X1,complement(join(X0,meet(X0,X1)))),
inference(forward_demodulation,[],[f17205,f15090]) ).
fof(f17268,plain,
! [X0,X1] : meet(X1,complement(X0)) = complement(join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[],[f17242,f4]) ).
fof(f17288,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),X1) = meet(X1,complement(X0)),
inference(forward_demodulation,[],[f17268,f14349]) ).
fof(f17295,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(X1,complement(X0)),
inference(forward_demodulation,[],[f17288,f5]) ).
fof(f17299,plain,
! [X0,X1] : join(X1,X0) = join(X0,meet(X1,complement(X0))),
inference(superposition,[],[f17067,f7659]) ).
fof(f17416,plain,
! [X0,X1] :
( zero != meet(complement(X1),join(meet(X0,X1),complement(join(X0,complement(X1)))))
| complement(complement(X1)) = join(meet(X0,X1),complement(join(X0,complement(X1)))) ),
inference(superposition,[],[f2170,f17067]) ).
fof(f17435,plain,
! [X0,X1] :
( zero != meet(complement(join(X0,complement(X1))),complement(X1))
| complement(complement(X1)) = join(meet(X0,X1),complement(join(X0,complement(X1)))) ),
inference(forward_demodulation,[],[f17416,f14693]) ).
fof(f17515,plain,
! [X0,X1] :
( zero != meet(complement(X1),complement(join(X0,complement(X1))))
| complement(complement(X1)) = join(meet(X0,X1),complement(join(X0,complement(X1)))) ),
inference(forward_demodulation,[],[f17435,f5]) ).
fof(f17574,plain,
! [X0,X1] : complement(complement(X1)) = join(meet(X0,X1),complement(join(X0,complement(X1)))),
inference(forward_subsumption_resolution,[],[f17515,f531]) ).
fof(f17612,plain,
! [X0,X1] : complement(complement(X1)) = join(meet(X0,X1),meet(X1,complement(X0))),
inference(forward_demodulation,[],[f17574,f14818]) ).
fof(f17635,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,complement(X0))) = X1,
inference(forward_demodulation,[],[f17612,f7659]) ).
fof(f17663,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(X0,X1),meet(meet(join(X0,X2),X1),complement(X0))),
inference(superposition,[],[f17635,f36]) ).
fof(f17689,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X2)) = join(meet(X0,X1),meet(join(meet(X0,X1),meet(X1,X2)),complement(X0))),
inference(superposition,[],[f17635,f94]) ).
fof(f17753,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(X1))),
inference(superposition,[],[f121,f17635]) ).
fof(f17884,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X2)) = join(meet(X0,X1),meet(complement(X0),join(meet(X0,X1),meet(X1,X2)))),
inference(forward_demodulation,[],[f17689,f4649]) ).
fof(f17910,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(X0,X1),meet(complement(X0),meet(join(X0,X2),X1))),
inference(forward_demodulation,[],[f17663,f4649]) ).
fof(f17976,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X2)) = join(meet(X0,X1),meet(meet(X1,X2),complement(X0))),
inference(forward_demodulation,[],[f17884,f14694]) ).
fof(f17998,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(X0,X1),meet(X1,meet(X2,complement(X0)))),
inference(forward_demodulation,[],[f17910,f14493]) ).
fof(f18049,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X2)) = join(meet(X0,X1),meet(X1,meet(X2,complement(X0)))),
inference(forward_demodulation,[],[f17976,f7]) ).
fof(f18095,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X2)) = meet(join(X0,X2),X1),
inference(forward_demodulation,[],[f18049,f17998]) ).
fof(f19418,plain,
! [X0,X1] : meet(X0,complement(meet(X1,complement(X0)))) = meet(complement(meet(X1,complement(X0))),complement(meet(complement(X0),complement(X1)))),
inference(superposition,[],[f13194,f17295]) ).
fof(f19427,plain,
! [X0,X1] : meet(X0,complement(meet(X1,complement(X0)))) = complement(join(meet(complement(X0),complement(X1)),meet(X1,complement(X0)))),
inference(forward_demodulation,[],[f19418,f14702]) ).
fof(f19539,plain,
! [X0,X1] : meet(X0,complement(meet(X1,complement(X0)))) = meet(join(X0,complement(X1)),complement(meet(complement(X0),complement(X1)))),
inference(forward_demodulation,[],[f19427,f15440]) ).
fof(f19635,plain,
! [X0,X1] : meet(X0,complement(meet(X1,complement(X0)))) = meet(join(X0,complement(X1)),join(X1,complement(complement(X0)))),
inference(forward_demodulation,[],[f19539,f15490]) ).
fof(f19706,plain,
! [X0,X1] : meet(X0,complement(meet(X1,complement(X0)))) = meet(join(X0,complement(X1)),join(X1,X0)),
inference(forward_demodulation,[],[f19635,f7659]) ).
fof(f19760,plain,
! [X0,X1] : meet(X0,complement(meet(X1,complement(X0)))) = meet(join(X1,X0),join(X0,complement(X1))),
inference(forward_demodulation,[],[f19706,f5]) ).
fof(f19795,plain,
! [X0,X1] : meet(join(X1,X0),join(X0,complement(X1))) = X0,
inference(forward_demodulation,[],[f19760,f10905]) ).
fof(f19833,plain,
! [X2,X0,X1] : join(meet(X2,X0),X1) = meet(join(X0,X1),join(join(meet(X2,X0),X1),complement(X0))),
inference(superposition,[],[f19795,f122]) ).
fof(f19902,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(join(X3,X0),join(X1,join(X0,complement(X3)))))) = meet(X1,join(meet(X1,join(meet(X1,join(X3,X0)),X2)),X0)),
inference(superposition,[],[f60,f19795]) ).
fof(f19920,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X2,join(X0,complement(X1)))) = meet(join(X1,X0),join(X2,join(X0,meet(complement(join(X1,X0)),join(join(X1,X0),join(X0,complement(X1))))))),
inference(superposition,[],[f1408,f19795]) ).
fof(f19966,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X2,join(X0,complement(X1)))) = meet(join(X1,X0),join(X2,join(X0,meet(join(X0,complement(X1)),complement(join(X1,X0)))))),
inference(forward_demodulation,[],[f19920,f14047]) ).
fof(f19983,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(join(X3,X0),join(X1,join(X0,complement(X3)))))) = meet(X1,join(X0,meet(join(meet(X1,join(X3,X0)),X2),X1))),
inference(forward_demodulation,[],[f19902,f4205]) ).
fof(f20036,plain,
! [X2,X0,X1] : join(meet(X2,X0),X1) = meet(join(X0,X1),join(complement(X0),join(meet(X2,X0),X1))),
inference(forward_demodulation,[],[f19833,f6]) ).
fof(f20059,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X2,join(X0,complement(X1)))) = meet(join(X1,X0),join(X2,join(X0,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f19966,f12113]) ).
fof(f20074,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(join(X3,X0),join(X1,join(X0,complement(X3)))))) = meet(X1,join(X0,meet(X1,join(meet(X1,join(X3,X0)),X2)))),
inference(forward_demodulation,[],[f19983,f103]) ).
fof(f20103,plain,
! [X2,X0,X1] : join(meet(X2,X0),X1) = meet(join(X0,X1),join(X2,join(X1,complement(X0)))),
inference(forward_demodulation,[],[f20036,f17147]) ).
fof(f20120,plain,
! [X2,X0,X1] : meet(join(X2,X0),join(X1,X0)) = meet(join(X1,X0),join(X2,join(X0,complement(X1)))),
inference(forward_demodulation,[],[f20059,f14069]) ).
fof(f20130,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(join(X3,X0),join(X1,join(X0,complement(X3)))))) = meet(X1,join(X0,meet(join(join(X3,X0),X2),X1))),
inference(forward_demodulation,[],[f20074,f16683]) ).
fof(f20160,plain,
! [X2,X0,X1] : meet(join(X2,X0),join(X1,X0)) = join(meet(X2,X1),X0),
inference(forward_demodulation,[],[f20120,f20103]) ).
fof(f20168,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(join(X3,X0),join(X1,join(X0,complement(X3)))))) = meet(join(join(join(X3,X0),X2),X0),X1),
inference(forward_demodulation,[],[f20130,f14380]) ).
fof(f20186,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(join(X3,X0),join(X1,join(X0,complement(X3)))))) = meet(join(X0,join(join(X3,X0),X2)),X1),
inference(forward_demodulation,[],[f20168,f6]) ).
fof(f20192,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(join(X3,X0),join(X1,join(X0,complement(X3)))))) = meet(join(X0,join(X3,join(X0,X2))),X1),
inference(forward_demodulation,[],[f20186,f8]) ).
fof(f20196,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(join(X3,X0),join(X1,join(X0,complement(X3)))))) = meet(join(X0,join(X2,X3)),X1),
inference(forward_demodulation,[],[f20192,f777]) ).
fof(f20200,plain,
! [X2,X3,X0,X1] : meet(join(X0,join(X2,X3)),X1) = meet(X1,join(X2,join(meet(X1,X3),X0))),
inference(forward_demodulation,[],[f20196,f20103]) ).
fof(f20209,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = join(meet(X0,X2),meet(X0,X1)),
inference(superposition,[],[f20160,f4]) ).
fof(f20210,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X1,X0))) = join(meet(X0,X2),meet(X1,X0)),
inference(superposition,[],[f20160,f17]) ).
fof(f20255,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = meet(join(X1,meet(X0,X2)),X0),
inference(superposition,[],[f20160,f4]) ).
fof(f20256,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X2,X0)) = meet(join(X1,meet(X2,X0)),X0),
inference(superposition,[],[f20160,f17]) ).
fof(f20345,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,X2)) = meet(X3,join(meet(X3,join(X0,X2)),join(meet(X0,X1),X2))),
inference(superposition,[],[f94,f20160]) ).
fof(f20417,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,X2)) = meet(join(join(X0,X2),join(meet(X0,X1),X2)),X3),
inference(forward_demodulation,[],[f20345,f16683]) ).
fof(f20486,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,X0))) = join(meet(X1,X0),meet(X2,X0)),
inference(forward_demodulation,[],[f20256,f5]) ).
fof(f20487,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = join(meet(X1,X0),meet(X0,X2)),
inference(forward_demodulation,[],[f20255,f5]) ).
fof(f20516,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(X0,X2),meet(X1,X0)),
inference(forward_demodulation,[],[f20210,f14380]) ).
fof(f20542,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,X2)) = meet(join(X2,join(join(X0,X2),meet(X0,X1))),X3),
inference(forward_demodulation,[],[f20417,f131]) ).
fof(f20599,plain,
! [X2,X0,X1] : meet(join(X2,X1),X0) = join(meet(X1,X0),meet(X2,X0)),
inference(forward_demodulation,[],[f20486,f14380]) ).
fof(f20600,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(join(X1,X2),X0),
inference(forward_demodulation,[],[f20487,f18095]) ).
fof(f20636,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,X2)) = meet(join(X2,join(X0,join(X2,meet(X0,X1)))),X3),
inference(forward_demodulation,[],[f20542,f8]) ).
fof(f20702,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,X2)) = meet(join(X2,join(meet(X0,X1),X0)),X3),
inference(forward_demodulation,[],[f20636,f777]) ).
fof(f20747,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,X2)) = meet(join(X2,join(X0,meet(X0,X1))),X3),
inference(forward_demodulation,[],[f20702,f6]) ).
fof(f20775,plain,
! [X2,X3,X0] : meet(join(X2,X0),X3) = meet(X3,join(X0,X2)),
inference(forward_demodulation,[],[f20747,f4]) ).
fof(f20890,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,join(X2,meet(X0,X1))))) = meet(X1,join(X2,meet(X0,join(X1,complement(meet(X1,join(X2,meet(X0,X1)))))))),
inference(superposition,[],[f52,f17299]) ).
fof(f20918,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X1,one)))) = meet(X1,join(X0,meet(X1,join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f20890,f200]) ).
fof(f20972,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X1,one)))) = meet(join(X0,join(X2,meet(X0,X1))),X1),
inference(forward_demodulation,[],[f20918,f20600]) ).
fof(f21006,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X1,one)))) = meet(X1,join(X0,join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f20972,f5]) ).
fof(f21031,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = meet(X1,join(X2,meet(X0,join(X1,one)))),
inference(forward_demodulation,[],[f21006,f179]) ).
fof(f21046,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = meet(X1,join(X2,meet(X0,one))),
inference(forward_demodulation,[],[f21031,f243]) ).
fof(f21056,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = meet(X1,join(X2,X0)),
inference(forward_demodulation,[],[f21046,f204]) ).
fof(f21333,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),meet(X0,join(X1,X2)))) = meet(X0,join(join(X2,X1),complement(X0))),
inference(superposition,[],[f1427,f21056]) ).
fof(f21334,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,join(X3,meet(X0,join(X1,X2))))) = join(X3,meet(join(X2,X1),X0)),
inference(superposition,[],[f4381,f21056]) ).
fof(f21398,plain,
! [X2,X3,X0,X1] : join(X3,meet(join(X1,X2),X0)) = join(X3,meet(join(X2,X1),X0)),
inference(forward_demodulation,[],[f21334,f4381]) ).
fof(f21399,plain,
! [X2,X0,X1] : meet(join(X2,X1),X0) = meet(X0,join(complement(X0),meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f21333,f14057]) ).
fof(f21500,plain,
! [X2,X0,X1] : meet(join(X2,X1),X0) = meet(join(complement(X0),join(X1,X2)),X0),
inference(forward_demodulation,[],[f21399,f20600]) ).
fof(f21550,plain,
! [X2,X0,X1] : meet(join(X2,X1),X0) = meet(X0,join(complement(X0),join(X1,X2))),
inference(forward_demodulation,[],[f21500,f5]) ).
fof(f21582,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = meet(join(X2,X1),X0),
inference(forward_demodulation,[],[f21550,f14038]) ).
fof(f21645,plain,
! [X2,X0,X1] : join(complement(X0),meet(X0,join(X1,X2))) = join(complement(X0),join(X2,X1)),
inference(superposition,[],[f16859,f21056]) ).
fof(f21857,plain,
! [X2,X0,X1] : join(complement(X0),join(X1,X2)) = join(complement(X0),join(X2,X1)),
inference(forward_demodulation,[],[f21645,f16859]) ).
fof(f23092,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,X1)),
inference(superposition,[],[f21857,f7659]) ).
fof(f23444,plain,
! [X2,X3,X0,X1] : join(X3,join(X0,meet(X1,X2))) = join(X3,join(meet(X2,X1),X0)),
inference(superposition,[],[f23092,f4649]) ).
fof(f25007,plain,
! [X0,X1] : meet(join(complement(X0),X1),join(X0,complement(complement(X0)))) = meet(join(X0,complement(complement(X0))),join(zero,X1)),
inference(superposition,[],[f16627,f5966]) ).
fof(f25165,plain,
! [X2,X0,X1] : join(meet(complement(X0),X2),X1) = join(join(meet(complement(X0),X2),X1),meet(join(complement(X0),X1),X2)),
inference(superposition,[],[f17,f16627]) ).
fof(f25286,plain,
! [X2,X0,X1] : join(meet(complement(X0),X2),X1) = join(meet(join(complement(X0),X1),X2),join(meet(complement(X0),X2),X1)),
inference(forward_demodulation,[],[f25165,f6]) ).
fof(f25412,plain,
! [X0,X1] : meet(join(X0,complement(complement(X0))),X1) = meet(join(complement(X0),X1),join(X0,complement(complement(X0)))),
inference(forward_demodulation,[],[f25007,f321]) ).
fof(f25458,plain,
! [X2,X0,X1] : join(meet(complement(X0),X2),X1) = join(X1,join(meet(join(complement(X0),X1),X2),meet(complement(X0),X2))),
inference(forward_demodulation,[],[f25286,f131]) ).
fof(f25554,plain,
! [X0,X1] : meet(join(X0,X0),X1) = meet(join(complement(X0),X1),join(X0,X0)),
inference(forward_demodulation,[],[f25412,f7659]) ).
fof(f25591,plain,
! [X2,X0,X1] : join(meet(complement(X0),X2),X1) = join(X1,join(meet(X2,complement(X0)),meet(join(complement(X0),X1),X2))),
inference(forward_demodulation,[],[f25458,f23444]) ).
fof(f25652,plain,
! [X0,X1] : meet(X0,X1) = meet(join(complement(X0),X1),X0),
inference(forward_demodulation,[],[f25554,f2]) ).
fof(f25679,plain,
! [X2,X0,X1] : join(meet(complement(X0),X2),X1) = join(X1,meet(join(join(complement(X0),X1),complement(X0)),X2)),
inference(forward_demodulation,[],[f25591,f20516]) ).
fof(f25723,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),X1)),
inference(forward_demodulation,[],[f25652,f5]) ).
fof(f25745,plain,
! [X2,X0,X1] : join(meet(complement(X0),X2),X1) = join(X1,meet(join(complement(X0),join(complement(X0),X1)),X2)),
inference(forward_demodulation,[],[f25679,f21398]) ).
fof(f25790,plain,
! [X2,X0,X1] : join(meet(complement(X0),X2),X1) = join(X1,meet(join(complement(X0),X1),X2)),
inference(forward_demodulation,[],[f25745,f24]) ).
fof(f25964,plain,
! [X2,X3,X0,X1] : meet(X2,join(meet(X2,join(X3,meet(X0,X2))),meet(X0,X1))) = meet(X2,join(X3,meet(X0,join(X2,join(complement(X0),X1))))),
inference(superposition,[],[f52,f25723]) ).
fof(f25966,plain,
! [X2,X3,X0,X1] : meet(X2,join(meet(X2,join(meet(X2,X0),X3)),meet(X0,X1))) = meet(X2,join(X3,meet(X0,join(X2,join(complement(X0),X1))))),
inference(superposition,[],[f60,f25723]) ).
fof(f26073,plain,
! [X2,X3,X0,X1] : meet(X2,join(meet(X2,join(meet(X2,X0),X3)),meet(X0,X1))) = meet(X2,join(X3,meet(join(X1,X2),X0))),
inference(forward_demodulation,[],[f25966,f14070]) ).
fof(f26075,plain,
! [X2,X3,X0,X1] : meet(X2,join(meet(X2,join(X3,meet(X0,X2))),meet(X0,X1))) = meet(X2,join(X3,meet(join(X1,X2),X0))),
inference(forward_demodulation,[],[f25964,f14070]) ).
fof(f26187,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(join(X1,X2),X0))) = meet(join(join(meet(X2,X0),X3),meet(X0,X1)),X2),
inference(forward_demodulation,[],[f26073,f16683]) ).
fof(f26189,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(join(X1,X2),X0))) = meet(join(join(X3,meet(X0,X2)),meet(X0,X1)),X2),
inference(forward_demodulation,[],[f26075,f16683]) ).
fof(f26259,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(join(X1,X2),X0))) = meet(X2,join(join(meet(X2,X0),X3),meet(X0,X1))),
inference(forward_demodulation,[],[f26187,f5]) ).
fof(f26261,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(join(X1,X2),X0))) = meet(X2,join(join(X3,meet(X0,X2)),meet(X0,X1))),
inference(forward_demodulation,[],[f26189,f5]) ).
fof(f26303,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(join(X1,X2),X0))) = meet(X2,join(meet(X2,X0),join(X3,meet(X0,X1)))),
inference(forward_demodulation,[],[f26259,f8]) ).
fof(f26305,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(join(X1,X2),X0))) = meet(X2,join(X3,join(meet(X0,X2),meet(X0,X1)))),
inference(forward_demodulation,[],[f26261,f8]) ).
fof(f26331,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(join(X1,X2),X0))) = meet(join(X0,join(X3,meet(X0,X1))),X2),
inference(forward_demodulation,[],[f26303,f16683]) ).
fof(f26333,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(X0,join(X2,meet(X0,X1))))) = meet(X2,join(X3,meet(join(X1,X2),X0))),
inference(forward_demodulation,[],[f26305,f20209]) ).
fof(f26348,plain,
! [X2,X3,X0,X1] : meet(join(X0,X3),X2) = meet(X2,join(X3,meet(join(X1,X2),X0))),
inference(forward_demodulation,[],[f26331,f179]) ).
fof(f26350,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(join(X1,X2),X0))) = meet(X2,join(X3,meet(join(X2,X1),X0))),
inference(forward_demodulation,[],[f26333,f20600]) ).
fof(f26360,plain,
! [X2,X3,X0,X1] : meet(join(X0,X3),X2) = meet(X2,join(X3,meet(join(X2,X1),X0))),
inference(forward_demodulation,[],[f26350,f26348]) ).
fof(f27114,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(join(X0,X2),X1)),
inference(superposition,[],[f25790,f7659]) ).
fof(f27887,plain,
! [X2,X0,X1] : join(meet(X1,X2),X0) = join(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f27114,f21582]) ).
fof(f27911,plain,
! [X2,X3,X0,X1] : join(meet(X0,join(X3,meet(X2,join(join(X0,X1),complement(X2))))),X1) = join(X1,meet(join(X0,X1),join(meet(join(X0,X1),X2),X3))),
inference(superposition,[],[f27114,f5559]) ).
fof(f27948,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X2,X0))) = join(meet(X2,join(X0,meet(join(X2,X0),X1))),X0),
inference(superposition,[],[f27114,f4381]) ).
fof(f27968,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(X1,join(X0,X2))),
inference(superposition,[],[f4649,f27114]) ).
fof(f28103,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X2,X0))) = join(X0,meet(X2,join(X0,meet(join(X2,X0),X1)))),
inference(forward_demodulation,[],[f27948,f6]) ).
fof(f28138,plain,
! [X2,X3,X0,X1] : join(meet(X0,join(X3,meet(X2,join(join(X0,X1),complement(X2))))),X1) = join(meet(X0,join(meet(join(X0,X1),X2),X3)),X1),
inference(forward_demodulation,[],[f27911,f27114]) ).
fof(f28242,plain,
! [X2,X0,X1] : join(X0,meet(join(X1,X0),X2)) = join(X0,meet(X1,join(X2,X0))),
inference(forward_demodulation,[],[f28103,f26360]) ).
fof(f28271,plain,
! [X2,X3,X0,X1] : join(meet(X0,join(X3,meet(X2,join(join(X0,X1),complement(X2))))),X1) = join(X1,meet(X0,join(meet(join(X0,X1),X2),X3))),
inference(forward_demodulation,[],[f28138,f6]) ).
fof(f28337,plain,
! [X2,X0,X1] : join(meet(X2,X1),X0) = join(X0,meet(join(X1,X0),X2)),
inference(forward_demodulation,[],[f28242,f27968]) ).
fof(f28358,plain,
! [X2,X3,X0,X1] : join(X1,meet(X0,join(meet(join(X0,X1),X2),X3))) = join(X1,meet(X0,join(X3,meet(X2,join(join(X0,X1),complement(X2)))))),
inference(forward_demodulation,[],[f28271,f6]) ).
fof(f28412,plain,
! [X2,X3,X0,X1] : join(X1,meet(X0,join(meet(join(X0,X1),X2),X3))) = join(X1,meet(X0,join(X3,meet(join(X0,X1),X2)))),
inference(forward_demodulation,[],[f28358,f14057]) ).
fof(f28444,plain,
! [X2,X3,X0,X1] : join(X1,meet(X0,join(meet(join(X0,X1),X2),X3))) = join(X1,meet(join(X2,X3),X0)),
inference(forward_demodulation,[],[f28412,f26360]) ).
fof(f29059,plain,
! [X2,X0,X1] : meet(join(X0,X2),join(X0,X1)) = join(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f18095,f3]) ).
fof(f29145,plain,
! [X2,X3,X0,X1] : join(meet(X3,X0),meet(X0,join(meet(X0,X1),X2))) = meet(join(X3,join(X2,meet(X1,join(X0,complement(X1))))),X0),
inference(superposition,[],[f18095,f5559]) ).
fof(f29409,plain,
! [X2,X3,X0,X1] : meet(X0,join(X3,join(X2,meet(X1,join(X0,complement(X1)))))) = join(meet(X3,X0),meet(X0,join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f29145,f5]) ).
fof(f29476,plain,
! [X2,X0,X1] : join(meet(X1,X2),X0) = meet(join(X0,X2),join(X0,X1)),
inference(forward_demodulation,[],[f29059,f27887]) ).
fof(f29597,plain,
! [X2,X3,X0,X1] : meet(X0,join(X3,join(X2,meet(X1,join(X0,complement(X1)))))) = meet(join(X3,join(meet(X0,X1),X2)),X0),
inference(forward_demodulation,[],[f29409,f18095]) ).
fof(f29726,plain,
! [X2,X3,X0,X1] : meet(X0,join(X3,join(X2,meet(X1,join(X0,complement(X1)))))) = meet(X0,join(X3,join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f29597,f5]) ).
fof(f29807,plain,
! [X2,X3,X0,X1] : meet(X0,join(X3,join(X2,meet(X1,join(X0,complement(X1)))))) = meet(join(X2,join(X3,X1)),X0),
inference(forward_demodulation,[],[f29726,f20200]) ).
fof(f29849,plain,
! [X2,X3,X0,X1] : meet(join(X2,join(X3,X1)),X0) = meet(X0,join(X3,join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f29807,f14057]) ).
fof(f29955,plain,
! [X2,X0,X1] : meet(join(X0,X2),join(X0,X1)) = join(meet(meet(X1,complement(X0)),X2),X0),
inference(superposition,[],[f29476,f17753]) ).
fof(f30273,plain,
! [X2,X0,X1] : meet(join(X0,X2),join(X0,X1)) = join(X0,meet(meet(X1,complement(X0)),X2)),
inference(forward_demodulation,[],[f29955,f6]) ).
fof(f30459,plain,
! [X2,X0,X1] : meet(join(X0,X2),join(X0,X1)) = join(X0,meet(X1,meet(complement(X0),X2))),
inference(forward_demodulation,[],[f30273,f7]) ).
fof(f30613,plain,
! [X2,X0,X1] : join(meet(X1,X2),X0) = join(X0,meet(X1,meet(complement(X0),X2))),
inference(forward_demodulation,[],[f30459,f29476]) ).
fof(f40550,plain,
! [X2,X3,X0,X1] : join(X1,meet(join(X0,X1),X2)) = join(meet(join(meet(join(X0,X1),X2),meet(X2,X3)),X0),X1),
inference(superposition,[],[f28337,f94]) ).
fof(f40794,plain,
! [X2,X3,X0,X1] : join(X1,meet(join(X0,X1),X2)) = join(X1,meet(join(meet(join(X0,X1),X2),meet(X2,X3)),X0)),
inference(forward_demodulation,[],[f40550,f6]) ).
fof(f40962,plain,
! [X2,X3,X0,X1] : join(X1,meet(join(X0,X1),X2)) = join(X1,meet(X0,join(meet(join(X0,X1),X2),meet(X2,X3)))),
inference(forward_demodulation,[],[f40794,f4649]) ).
fof(f41099,plain,
! [X2,X3,X0,X1] : join(X1,meet(join(X0,X1),X2)) = join(X1,meet(join(X2,meet(X2,X3)),X0)),
inference(forward_demodulation,[],[f40962,f28444]) ).
fof(f41189,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,meet(join(X0,X1),X2)),
inference(forward_demodulation,[],[f41099,f4]) ).
fof(f54099,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(complement(meet(X0,X2)),meet(X1,X2))) = join(meet(X0,X2),meet(complement(meet(X0,X2)),meet(join(X0,X1),X2))),
inference(superposition,[],[f9347,f20599]) ).
fof(f54184,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(complement(meet(X0,X2)),meet(X1,X2))) = join(meet(X0,X2),meet(X2,meet(complement(meet(X0,X2)),join(X0,X1)))),
inference(forward_demodulation,[],[f54099,f4969]) ).
fof(f54429,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(complement(meet(X0,X2)),meet(X1,X2))) = join(meet(X2,join(X0,X1)),meet(X0,X2)),
inference(forward_demodulation,[],[f54184,f30613]) ).
fof(f54624,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(complement(meet(X0,X2)),meet(X1,X2))) = join(meet(X0,X2),meet(X2,join(X0,X1))),
inference(forward_demodulation,[],[f54429,f6]) ).
fof(f54753,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = join(meet(X0,X2),meet(complement(meet(X0,X2)),meet(X1,X2))),
inference(forward_demodulation,[],[f54624,f4125]) ).
fof(f54822,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = join(meet(X0,X2),meet(X2,meet(complement(meet(X0,X2)),X1))),
inference(forward_demodulation,[],[f54753,f4969]) ).
fof(f54864,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = join(meet(X2,X1),meet(X0,X2)),
inference(forward_demodulation,[],[f54822,f30613]) ).
fof(f55165,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = meet(X0,join(join(X1,meet(X0,X2)),X2)),
inference(superposition,[],[f41189,f54864]) ).
fof(f55308,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = meet(X0,join(X2,join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f55165,f21056]) ).
fof(f55574,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = meet(join(X1,join(X2,X2)),X0),
inference(forward_demodulation,[],[f55308,f29849]) ).
fof(f55755,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(X0,X2),meet(X0,X1)),
inference(forward_demodulation,[],[f55574,f2]) ).
fof(f60138,plain,
meet(a,join(b,c)) != meet(join(c,b),a),
inference(superposition,[],[f13,f55755]) ).
fof(f60366,plain,
$false,
inference(forward_subsumption_resolution,[],[f60138,f20775]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT214-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n009.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 14:07:00 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 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
% 10.72/2.49 % (2066800)Input is clausal, will run a generic CNF schedule.
% 10.72/2.49 % (2066806)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3671490202:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.72/2.49 % (2066808)lrs+10_1_sil=8000:sp=occurrence:random_seed=2556360164:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.72/2.49 % (2066805)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=824101123:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.72/2.49 % (2066811)dis-21_1_sil=8000:lcm=predicate:random_seed=2140128822: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)
% 10.72/2.49 % (2066807)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3650889428:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.72/2.49 % (2066809)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1451675784:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.72/2.50 % (2066810)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2698597755:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.72/2.50 % (2066811)Refutation not found, incomplete strategy
% 10.72/2.50 % (2066811)------------------------------
% 10.72/2.50 % (2066811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.50 % (2066811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.50 % (2066811)CaDiCaL version: 2.1.3
% 10.72/2.50 % (2066811)Termination reason: Refutation not found, incomplete strategy
% 10.72/2.50 % (2066811)Time elapsed: 0.002 s
% 10.72/2.50 % (2066811)Peak memory usage: 88 MB
% 10.72/2.50 % (2066811)Instructions burned: 1 (million)
% 10.72/2.50 % (2066808)Instruction limit reached!
% 10.72/2.50 % (2066808)------------------------------
% 10.72/2.50 % (2066808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.50 % (2066808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.50 % (2066808)CaDiCaL version: 2.1.3
% 10.72/2.50 % (2066808)Termination reason: Instruction limit
% 10.72/2.50 % (2066808)Termination phase: Saturation
% 10.72/2.50 % (2066808)Time elapsed: 0.064 s
% 10.72/2.50 % (2066808)Peak memory usage: 89 MB
% 10.72/2.50 % (2066808)Instructions burned: 108 (million)
% 10.72/2.50 % (2066809)Instruction limit reached!
% 10.72/2.50 % (2066809)------------------------------
% 10.72/2.50 % (2066809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.50 % (2066809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.50 % (2066809)CaDiCaL version: 2.1.3
% 10.72/2.50 % (2066809)Termination reason: Instruction limit
% 10.72/2.50 % (2066809)Termination phase: Saturation
% 10.72/2.50 % (2066809)Time elapsed: 0.070 s
% 10.72/2.50 % (2066809)Peak memory usage: 89 MB
% 10.72/2.50 % (2066809)Instructions burned: 116 (million)
% 10.72/2.50 % (2066810)Instruction limit reached!
% 10.72/2.50 % (2066810)------------------------------
% 10.72/2.50 % (2066810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.50 % (2066810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.50 % (2066810)CaDiCaL version: 2.1.3
% 10.72/2.50 % (2066810)Termination reason: Instruction limit
% 10.72/2.50 % (2066810)Termination phase: Saturation
% 10.72/2.50 % (2066810)Time elapsed: 0.102 s
% 10.72/2.50 % (2066810)Peak memory usage: 89 MB
% 10.72/2.50 % (2066810)Instructions burned: 181 (million)
% 10.72/2.50 % (2066819)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=2905256963:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 10.72/2.50 % (2066819)Refutation not found, incomplete strategy
% 10.72/2.50 % (2066819)------------------------------
% 10.72/2.50 % (2066819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.50 % (2066819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.50 % (2066819)CaDiCaL version: 2.1.3
% 10.72/2.50 % (2066819)Termination reason: Refutation not found, incomplete strategy
% 10.72/2.50 % (2066819)Time elapsed: 0.001 s
% 10.72/2.50 % (2066819)Peak memory usage: 88 MB
% 10.72/2.50 % (2066820)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1203068819:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 13.95/2.88 % (2066820)Refutation not found, incomplete strategy
% 13.95/2.88 % (2066820)------------------------------
% 13.95/2.88 % (2066820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.95/2.88 % (2066820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.95/2.88 % (2066820)CaDiCaL version: 2.1.3
% 13.95/2.88 % (2066820)Termination reason: Refutation not found, incomplete strategy
% 13.95/2.88 % (2066820)Time elapsed: 0.002 s
% 13.95/2.88 % (2066820)Peak memory usage: 88 MB
% 13.95/2.88 % (2066820)Instructions burned: 1 (million)
% 13.95/2.88 % (2066821)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2770184755:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 13.95/2.88 % (2066821)Refutation not found, incomplete strategy
% 13.95/2.88 % (2066821)------------------------------
% 13.95/2.88 % (2066821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.95/2.88 % (2066821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.95/2.88 % (2066821)CaDiCaL version: 2.1.3
% 13.95/2.88 % (2066821)Termination reason: Refutation not found, incomplete strategy
% 13.95/2.88 % (2066821)Time elapsed: 0.001 s
% 13.95/2.88 % (2066821)Peak memory usage: 88 MB
% 13.95/2.88 % (2066811)------------------------------
% 13.95/2.88 % (2066811)------------------------------
% 13.95/2.88 % (2066825)lrs+10_64_to=lpo:sil=8000:random_seed=302238271:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 13.95/2.88 % (2066819)------------------------------
% 13.95/2.88 % (2066819)------------------------------
% 13.95/2.88 % (2066820)------------------------------
% 13.95/2.88 % (2066820)------------------------------
% 13.95/2.88 % (2066825)Instruction limit reached!
% 13.95/2.88 % (2066825)------------------------------
% 13.95/2.88 % (2066825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.95/2.88 % (2066825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.95/2.88 % (2066825)CaDiCaL version: 2.1.3
% 13.95/2.88 % (2066825)Termination reason: Instruction limit
% 13.95/2.88 % (2066825)Termination phase: Saturation
% 13.95/2.88 % (2066825)Time elapsed: 0.072 s
% 13.95/2.88 % (2066825)Peak memory usage: 88 MB
% 13.95/2.88 % (2066825)Instructions burned: 127 (million)
% 13.95/2.88 % (2066821)------------------------------
% 13.95/2.88 % (2066821)------------------------------
% 13.95/2.88 % (2066827)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3332929780:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 13.95/2.88 % (2066829)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=724423975:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 13.95/2.88 % (2066828)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1954051788:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 13.95/2.88 % (2066830)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=2600352664:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 13.95/2.88 % (2066828)Instruction limit reached!
% 13.95/2.88 % (2066828)------------------------------
% 13.95/2.88 % (2066828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.95/2.88 % (2066828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.95/2.88 % (2066828)CaDiCaL version: 2.1.3
% 13.95/2.88 % (2066828)Termination reason: Instruction limit
% 13.95/2.88 % (2066828)Termination phase: Saturation
% 13.95/2.88 % (2066828)Time elapsed: 0.095 s
% 13.95/2.88 % (2066828)Peak memory usage: 90 MB
% 13.95/2.88 % (2066828)Instructions burned: 158 (million)
% 13.95/2.88 % (2066827)Instruction limit reached!
% 13.95/2.88 % (2066827)------------------------------
% 13.95/2.88 % (2066827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.95/2.88 % (2066827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.95/2.88 % (2066827)CaDiCaL version: 2.1.3
% 13.95/2.88 % (2066827)Termination reason: Instruction limit
% 13.95/2.88 % (2066827)Termination phase: Saturation
% 13.95/2.88 % (2066827)Time elapsed: 0.116 s
% 13.95/2.88 % (2066827)Peak memory usage: 90 MB
% 13.95/2.88 % (2066827)Instructions burned: 194 (million)
% 13.95/2.88 % (2066830)Instruction limit reached!
% 13.95/2.88 % (2066830)------------------------------
% 13.95/2.88 % (2066830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.95/2.88 % (2066830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.95/2.88 % (2066830)CaDiCaL version: 2.1.3
% 13.95/2.88 % (2066830)Termination reason: Instruction limit
% 13.95/2.88 % (2066830)Termination phase: Saturation
% 13.95/2.88 % (2066830)Time elapsed: 0.065 s
% 13.95/2.88 % (2066830)Peak memory usage: 89 MB
% 13.95/2.88 % (2066830)Instructions burned: 106 (million)
% 13.95/2.88 % (2066835)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3761856179:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 13.95/2.88 % (2066835)Refutation not found, incomplete strategy
% 13.95/2.88 % (2066835)------------------------------
% 13.95/2.88 % (2066835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.95/2.88 % (2066835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.95/2.88 % (2066835)CaDiCaL version: 2.1.3
% 13.95/2.88 % (2066835)Termination reason: Refutation not found, incomplete strategy
% 13.95/2.88 % (2066835)Time elapsed: 0.001 s
% 13.95/2.88 % (2066835)Peak memory usage: 87 MB
% 13.95/2.88 % (2066837)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2323692090:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 13.95/2.88 % (2066836)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=593261827:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 13.95/2.88 % (2066836)Instruction limit reached!
% 13.95/2.88 % (2066836)------------------------------
% 13.95/2.88 % (2066836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.95/2.88 % (2066836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.95/2.88 % (2066836)CaDiCaL version: 2.1.3
% 13.95/2.88 % (2066836)Termination reason: Instruction limit
% 13.95/2.88 % (2066836)Termination phase: Saturation
% 13.95/2.88 % (2066836)Time elapsed: 0.143 s
% 13.95/2.88 % (2066836)Peak memory usage: 90 MB
% 13.95/2.88 % (2066836)Instructions burned: 243 (million)
% 13.95/2.88 % (2066835)------------------------------
% 13.95/2.88 % (2066835)------------------------------
% 13.95/2.88 % (2066841)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1149072323:i=134:sd=2:doe=on:ss=axioms:sgt=14_2988 on theBenchmark for (2988ds/134Mi)
% 13.95/2.88 % (2066842)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1488467387:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 13.95/2.88 % (2066841)Instruction limit reached!
% 13.95/2.88 % (2066841)------------------------------
% 13.95/2.88 % (2066841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.95/2.88 % (2066841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.95/2.88 % (2066841)CaDiCaL version: 2.1.3
% 13.95/2.88 % (2066841)Termination reason: Instruction limit
% 13.95/2.88 % (2066841)Termination phase: Saturation
% 13.95/2.88 % (2066841)Time elapsed: 0.079 s
% 13.95/2.88 % (2066841)Peak memory usage: 89 MB
% 13.95/2.88 % (2066841)Instructions burned: 135 (million)
% 13.95/2.88 % (2066845)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2817810328:i=191:fgj=on:bd=all_2986 on theBenchmark for (2986ds/191Mi)
% 13.95/2.88 % (2066845)Instruction limit reached!
% 13.95/2.88 % (2066845)------------------------------
% 13.95/2.88 % (2066845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.95/2.88 % (2066845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.95/2.88 % (2066845)CaDiCaL version: 2.1.3
% 13.95/2.88 % (2066845)Termination reason: Instruction limit
% 13.95/2.88 % (2066845)Termination phase: Saturation
% 13.95/2.88 % (2066845)Time elapsed: 0.119 s
% 13.95/2.88 % (2066845)Peak memory usage: 91 MB
% 13.95/2.88 % (2066845)Instructions burned: 192 (million)
% 13.95/2.88 % (2066842)Instruction limit reached!
% 13.95/2.88 % (2066842)------------------------------
% 13.95/2.88 % (2066842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.95/2.88 % (2066842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.95/2.88 % (2066842)CaDiCaL version: 2.1.3
% 13.95/2.88 % (2066842)Termination reason: Instruction limit
% 13.95/2.88 % (2066842)Termination phase: Saturation
% 13.95/2.88 % (2066842)Time elapsed: 0.315 s
% 13.95/2.88 % (2066842)Peak memory usage: 94 MB
% 13.95/2.88 % (2066842)Instructions burned: 500 (million)
% 13.95/2.88 % (2066847)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=551933893:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi)
% 13.95/2.88 % (2066848)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3148669977:cond=on:i=156:bs=on:gtg=exists_all:er=known_2983 on theBenchmark for (2983ds/156Mi)
% 13.95/2.88 % (2066806)First to succeed.
% 13.95/2.88 % (2066806)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2066800"
% 13.95/2.88 % (2066847)Instruction limit reached!
% 13.95/2.88 % (2066847)------------------------------
% 13.95/2.88 % (2066847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.95/2.88 % (2066847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.95/2.88 % (2066847)CaDiCaL version: 2.1.3
% 13.95/2.88 % (2066847)Termination reason: Instruction limit
% 13.95/2.88 % (2066847)Termination phase: Saturation
% 13.95/2.88 % (2066847)Time elapsed: 0.157 s
% 13.95/2.88 % (2066847)Peak memory usage: 92 MB
% 13.95/2.88 % (2066847)Instructions burned: 265 (million)
% 13.95/2.88 % (2066848)Instruction limit reached!
% 13.95/2.88 % (2066848)------------------------------
% 13.95/2.88 % (2066848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.95/2.88 % (2066848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.95/2.88 % (2066848)CaDiCaL version: 2.1.3
% 13.95/2.88 % (2066848)Termination reason: Instruction limit
% 13.95/2.88 % (2066848)Termination phase: Saturation
% 13.95/2.88 % (2066848)Time elapsed: 0.094 s
% 13.95/2.88 % (2066848)Peak memory usage: 89 MB
% 13.95/2.88 % (2066848)Instructions burned: 156 (million)
% 13.95/2.88 % (2066851)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=4270280546:i=3256:kws=precedence:bd=preordered:av=off_2981 on theBenchmark for (2981ds/3256Mi)
% 13.95/2.88 % (2066852)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=4244238872:i=537:av=off:ss=included_2981 on theBenchmark for (2981ds/537Mi)
% 13.95/2.88 % (2066806)Refutation found. Thanks to Tanya!
% 13.95/2.88 % SZS status Unsatisfiable for theBenchmark
% 13.95/2.88 % SZS output start Proof for theBenchmark
% See solution above
% 14.72/2.98 % (2066806)------------------------------
% 14.72/2.98 % (2066806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.72/2.98 % (2066806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.72/2.98 % (2066806)CaDiCaL version: 2.1.3
% 14.72/2.98 % (2066806)Termination reason: Refutation
% 14.72/2.98 % (2066806)Time elapsed: 1.731 s
% 14.72/2.98 % (2066806)Peak memory usage: 165 MB
% 14.72/2.98 % (2066806)Instructions burned: 5117 (million)
% 14.72/2.98 % (2066806)------------------------------
% 14.72/2.98 % (2066806)------------------------------
% 14.72/2.98 % (2066800)Success in time 2.019 s
% 14.72/2.98 % Vampire exiting
%------------------------------------------------------------------------------