%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT198-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:13 AM UTC 2026
% Result : Unsatisfiable 20.88s 3.86s
% Output : Refutation 21.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 72
% Number of leaves : 12
% Syntax : Number of formulae : 267 ( 254 unt; 0 def)
% Number of atoms : 283 ( 282 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 34 ( 18 ~; 16 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 7 ( 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 : 597 ( 597 !; 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(X1,meet(X2,join(X1,join(X3,meet(X0,X2)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equation_H42) ).
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(f21,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f27,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f28,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f36,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f41,plain,
! [X2,X0,X1] : join(X0,join(meet(X0,X1),X2)) = join(X0,X2),
inference(superposition,[],[f8,f4]) ).
fof(f50,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f54,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f21,f3]) ).
fof(f59,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f21]) ).
fof(f62,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f54,f6]) ).
fof(f63,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f27,f4]) ).
fof(f70,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f27]) ).
fof(f75,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f63,f5]) ).
fof(f84,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f28,f5]) ).
fof(f104,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(one,X1),
inference(superposition,[],[f8,f9]) ).
fof(f105,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f106,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f109,plain,
! [X0,X1] : meet(X0,meet(complement(X0),X1)) = meet(zero,X1),
inference(superposition,[],[f7,f10]) ).
fof(f110,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f111,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f112,plain,
! [X0,X1] : meet(X0,complement(join(X0,X1))) = meet(X0,zero),
inference(superposition,[],[f28,f10]) ).
fof(f114,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(X0,join(X1,X3)))) = meet(X1,join(X2,meet(X0,join(X2,join(X3,meet(X0,X1)))))),
inference(superposition,[],[f12,f5]) ).
fof(f119,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(X0),join(X0,X2)))) = meet(X0,join(X1,meet(complement(X0),join(X1,join(X2,zero))))),
inference(superposition,[],[f12,f10]) ).
fof(f155,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(X0),join(X0,X2)))) = meet(X0,join(X1,meet(complement(X0),join(X1,X2)))),
inference(forward_demodulation,[],[f119,f110]) ).
fof(f176,plain,
! [X0] : one = join(one,X0),
inference(superposition,[],[f21,f105]) ).
fof(f179,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f105]) ).
fof(f184,plain,
! [X0,X1] : one = join(X0,join(complement(X0),X1)),
inference(backward_demodulation,[],[f104,f176]) ).
fof(f194,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f6,f176]) ).
fof(f214,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f110]) ).
fof(f217,plain,
! [X0] : zero = meet(zero,X0),
inference(superposition,[],[f27,f110]) ).
fof(f220,plain,
! [X0,X1] : zero = meet(X0,meet(complement(X0),X1)),
inference(backward_demodulation,[],[f109,f217]) ).
fof(f230,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f5,f217]) ).
fof(f237,plain,
! [X0,X1] : zero = meet(X0,complement(join(X0,X1))),
inference(backward_demodulation,[],[f112,f230]) ).
fof(f261,plain,
zero = complement(one),
inference(superposition,[],[f10,f179]) ).
fof(f282,plain,
! [X0,X1] : zero = meet(X1,meet(X0,complement(X1))),
inference(superposition,[],[f220,f5]) ).
fof(f339,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f41,f6]) ).
fof(f343,plain,
! [X0,X1] : join(X0,one) = join(X0,complement(meet(X0,X1))),
inference(superposition,[],[f41,f9]) ).
fof(f360,plain,
! [X0,X1] : one = join(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f343,f194]) ).
fof(f424,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,one))) = meet(X0,join(X1,meet(X2,join(X0,complement(X1))))),
inference(superposition,[],[f12,f184]) ).
fof(f428,plain,
! [X0,X1] :
( one != one
| zero != meet(X0,join(complement(X0),X1))
| complement(X0) = join(complement(X0),X1) ),
inference(superposition,[],[f11,f184]) ).
fof(f433,plain,
! [X0,X1] :
( zero != meet(X0,join(complement(X0),X1))
| complement(X0) = join(complement(X0),X1) ),
inference(trivial_inequality_removal,[],[f428]) ).
fof(f437,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X1,meet(X2,join(X0,complement(X1))))),
inference(forward_demodulation,[],[f424,f105]) ).
fof(f525,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(X0),join(X1,meet(X0,X2))))) = meet(X0,join(X1,meet(complement(X0),X0))),
inference(superposition,[],[f155,f4]) ).
fof(f549,plain,
! [X2,X0,X1] : meet(X2,join(X1,meet(complement(X2),join(X2,X0)))) = meet(X2,join(X1,meet(complement(X2),join(X0,X1)))),
inference(superposition,[],[f155,f6]) ).
fof(f635,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(X0),join(X1,meet(X0,X2))))) = meet(X0,join(X1,meet(X0,complement(X0)))),
inference(forward_demodulation,[],[f525,f5]) ).
fof(f659,plain,
! [X2,X0,X1] : meet(X0,join(X1,zero)) = meet(X0,join(X1,meet(complement(X0),join(X1,meet(X0,X2))))),
inference(forward_demodulation,[],[f635,f10]) ).
fof(f671,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,join(X1,meet(complement(X0),join(X1,meet(X0,X2))))),
inference(forward_demodulation,[],[f659,f110]) ).
fof(f803,plain,
! [X2,X0,X1] : meet(X1,join(join(X0,meet(X1,X2)),meet(X2,join(X1,X0)))) = meet(X1,join(join(X0,meet(X1,X2)),meet(X2,join(X0,meet(X1,X2))))),
inference(superposition,[],[f12,f2]) ).
fof(f804,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),join(X0,meet(X1,complement(X0)))),
inference(superposition,[],[f437,f2]) ).
fof(f805,plain,
! [X2,X0,X1] : meet(X1,join(join(X0,meet(X1,X2)),meet(X2,join(X1,X0)))) = meet(X1,join(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f803,f21]) ).
fof(f811,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(X1,join(X0,join(meet(X1,X2),meet(X2,join(X1,X0))))),
inference(forward_demodulation,[],[f805,f8]) ).
fof(f1045,plain,
! [X2,X0,X1] : join(join(X1,X0),X2) = join(join(X1,X0),join(X0,X2)),
inference(superposition,[],[f59,f27]) ).
fof(f1104,plain,
! [X2,X0,X1] : join(join(X1,X0),X2) = join(X0,join(X2,join(X1,X0))),
inference(forward_demodulation,[],[f1045,f50]) ).
fof(f1119,plain,
! [X2,X0,X1] : join(X1,join(X0,X2)) = join(X0,join(X2,join(X1,X0))),
inference(forward_demodulation,[],[f1104,f8]) ).
fof(f1140,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,X2))),
inference(superposition,[],[f70,f5]) ).
fof(f1311,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,f106]) ).
fof(f1324,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f1311]) ).
fof(f1701,plain,
! [X2,X0,X1] : meet(complement(X0),join(X1,meet(X0,join(complement(X0),X2)))) = meet(complement(X0),join(X1,meet(X0,join(X1,join(X2,zero))))),
inference(superposition,[],[f114,f10]) ).
fof(f1801,plain,
! [X2,X0,X1] : meet(complement(X0),join(X1,meet(X0,join(complement(X0),X2)))) = meet(complement(X0),join(X1,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f1701,f110]) ).
fof(f2104,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = join(meet(X1,join(X0,X2)),meet(X0,X1)),
inference(superposition,[],[f21,f84]) ).
fof(f2132,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = join(meet(X0,X1),meet(X1,join(X0,X2))),
inference(forward_demodulation,[],[f2104,f6]) ).
fof(f2153,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(X1,join(X0,meet(X2,join(X1,X0)))),
inference(backward_demodulation,[],[f811,f2132]) ).
fof(f2165,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(X1,join(X0,meet(X2,join(X0,X1)))),
inference(superposition,[],[f2153,f6]) ).
fof(f2170,plain,
! [X2,X0,X1] : meet(X0,join(join(complement(X0),X1),meet(X0,X2))) = meet(X0,join(join(complement(X0),X1),meet(X2,one))),
inference(superposition,[],[f2153,f184]) ).
fof(f2174,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X0,X1))) = meet(X0,join(complement(X0),meet(X1,one))),
inference(superposition,[],[f2153,f9]) ).
fof(f2265,plain,
! [X0,X1] : meet(X0,join(complement(X0),X1)) = meet(X0,join(complement(X0),meet(X0,X1))),
inference(forward_demodulation,[],[f2174,f105]) ).
fof(f2269,plain,
! [X2,X0,X1] : meet(X0,join(join(complement(X0),X1),meet(X0,X2))) = meet(X0,join(complement(X0),join(X1,meet(X2,one)))),
inference(forward_demodulation,[],[f2170,f8]) ).
fof(f2295,plain,
! [X2,X0,X1] : meet(X0,join(join(complement(X0),X1),meet(X0,X2))) = meet(X0,join(complement(X0),join(X1,X2))),
inference(forward_demodulation,[],[f2269,f105]) ).
fof(f2307,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(X1,X2))) = meet(X0,join(complement(X0),join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f2295,f8]) ).
fof(f2310,plain,
! [X0,X1] : meet(X1,join(complement(X1),X0)) = meet(X1,join(complement(X1),meet(X0,X1))),
inference(superposition,[],[f2265,f5]) ).
fof(f2314,plain,
! [X0,X1] : meet(X0,join(complement(X0),zero)) = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(superposition,[],[f2265,f111]) ).
fof(f2328,plain,
! [X0,X1] : meet(X0,join(complement(X0),zero)) = meet(X0,join(complement(X0),complement(join(X0,X1)))),
inference(superposition,[],[f2265,f237]) ).
fof(f2396,plain,
! [X0,X1] : meet(X0,join(zero,complement(X0))) = meet(X0,join(complement(X0),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f2328,f6]) ).
fof(f2410,plain,
! [X0,X1] : meet(X0,join(zero,complement(X0))) = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f2314,f6]) ).
fof(f2427,plain,
! [X0,X1] : meet(X0,complement(X0)) = meet(X0,join(complement(X0),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f2396,f214]) ).
fof(f2433,plain,
! [X0,X1] : meet(X0,complement(X0)) = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f2410,f214]) ).
fof(f2443,plain,
! [X0,X1] : zero = meet(X0,join(complement(X0),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f2427,f10]) ).
fof(f2444,plain,
! [X0,X1] : zero = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f2433,f10]) ).
fof(f2478,plain,
! [X0,X1] :
( zero != zero
| complement(X0) = join(complement(X0),complement(join(X0,X1))) ),
inference(superposition,[],[f433,f2443]) ).
fof(f2505,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(trivial_inequality_removal,[],[f2478]) ).
fof(f2581,plain,
! [X0,X1] : complement(X1) = join(complement(X1),complement(join(X0,X1))),
inference(superposition,[],[f2505,f6]) ).
fof(f2605,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f27,f2505]) ).
fof(f2623,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f2605,f5]) ).
fof(f2644,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(join(X0,X1))),
inference(superposition,[],[f2623,f6]) ).
fof(f2651,plain,
! [X2,X0,X1] : complement(join(X0,join(X1,X2))) = meet(complement(X2),complement(join(X0,join(X1,X2)))),
inference(superposition,[],[f2623,f50]) ).
fof(f2694,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),complement(X0)),
inference(superposition,[],[f2581,f4]) ).
fof(f2695,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(meet(X1,X0)),complement(X0)),
inference(superposition,[],[f2581,f21]) ).
fof(f2751,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f2695,f6]) ).
fof(f2752,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f2694,f6]) ).
fof(f2793,plain,
! [X2,X0,X1] : meet(complement(X0),join(meet(X0,X1),X2)) = meet(complement(X0),join(meet(X0,X1),meet(X2,complement(meet(X0,X1))))),
inference(superposition,[],[f437,f2752]) ).
fof(f2804,plain,
! [X2,X0,X1] : meet(complement(X0),X2) = meet(complement(X0),meet(X2,complement(meet(X0,X1)))),
inference(superposition,[],[f84,f2752]) ).
fof(f2875,plain,
! [X0,X1] :
( zero != zero
| complement(X0) = join(complement(X0),meet(X1,complement(meet(X0,X1)))) ),
inference(superposition,[],[f433,f2444]) ).
fof(f2900,plain,
! [X0,X1] : complement(X0) = join(complement(X0),meet(X1,complement(meet(X0,X1)))),
inference(trivial_inequality_removal,[],[f2875]) ).
fof(f3042,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(complement(meet(X0,X1)),join(X1,complement(X0))))) = meet(X1,join(X2,meet(complement(meet(X0,X1)),join(X2,complement(X0))))),
inference(superposition,[],[f12,f2900]) ).
fof(f3047,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(meet(X1,complement(meet(X0,X1))),complement(X0)),
inference(superposition,[],[f27,f2900]) ).
fof(f3069,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f3047,f5]) ).
fof(f3071,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(complement(meet(X0,X1)),join(X2,complement(X0))))) = meet(X1,join(X2,meet(join(X1,complement(X0)),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f3042,f5]) ).
fof(f3101,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),X1),
inference(forward_demodulation,[],[f3069,f2804]) ).
fof(f3155,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(X0,complement(meet(X0,X1))),
inference(superposition,[],[f3101,f5]) ).
fof(f3199,plain,
! [X0,X1] : meet(X1,join(complement(X1),complement(meet(X0,X1)))) = meet(X1,join(complement(X1),meet(complement(X0),X1))),
inference(superposition,[],[f2265,f3101]) ).
fof(f3212,plain,
! [X0,X1] : meet(X1,join(complement(X1),complement(meet(X0,X1)))) = meet(X1,join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f3199,f2310]) ).
fof(f3247,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(X1,join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f3212,f2751]) ).
fof(f3267,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(X1,join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f3247,f3101]) ).
fof(f3277,plain,
! [X0] : meet(X0,one) = meet(complement(complement(X0)),X0),
inference(superposition,[],[f3267,f9]) ).
fof(f3278,plain,
! [X0,X1] : meet(X0,one) = meet(complement(meet(complement(X0),X1)),X0),
inference(superposition,[],[f3267,f360]) ).
fof(f3310,plain,
! [X2,X0,X1] : meet(X2,meet(complement(X0),join(X1,X2))) = meet(X2,join(complement(join(X1,X2)),complement(X0))),
inference(superposition,[],[f70,f3267]) ).
fof(f3318,plain,
! [X2,X0,X1] : meet(X2,complement(X0)) = meet(X2,join(complement(join(X1,X2)),complement(X0))),
inference(forward_demodulation,[],[f3310,f1140]) ).
fof(f3332,plain,
! [X0,X1] : meet(X0,one) = meet(X0,complement(meet(complement(X0),X1))),
inference(forward_demodulation,[],[f3278,f5]) ).
fof(f3333,plain,
! [X0] : meet(X0,one) = meet(X0,complement(complement(X0))),
inference(forward_demodulation,[],[f3277,f5]) ).
fof(f3345,plain,
! [X0,X1] : meet(X0,complement(meet(complement(X0),X1))) = X0,
inference(forward_demodulation,[],[f3332,f105]) ).
fof(f3346,plain,
! [X0] : meet(X0,complement(complement(X0))) = X0,
inference(forward_demodulation,[],[f3333,f105]) ).
fof(f3358,plain,
! [X0] : complement(complement(X0)) = join(complement(complement(X0)),X0),
inference(superposition,[],[f21,f3346]) ).
fof(f3385,plain,
! [X0] : complement(complement(X0)) = join(X0,complement(complement(X0))),
inference(forward_demodulation,[],[f3358,f6]) ).
fof(f3409,plain,
! [X0,X1] : meet(complement(join(complement(X0),meet(X0,X1))),X0) = meet(X0,complement(meet(X0,join(complement(X0),X1)))),
inference(superposition,[],[f3155,f2265]) ).
fof(f3413,plain,
! [X0,X1] : meet(X1,complement(meet(complement(X0),X1))) = meet(complement(complement(meet(X1,X0))),X1),
inference(superposition,[],[f3155,f3155]) ).
fof(f3465,plain,
! [X0,X1] : meet(X1,complement(meet(complement(X0),X1))) = meet(X1,complement(complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f3413,f5]) ).
fof(f3469,plain,
! [X0,X1] : meet(complement(join(complement(X0),meet(X0,X1))),X0) = meet(complement(join(complement(X0),X1)),X0),
inference(forward_demodulation,[],[f3409,f3155]) ).
fof(f3493,plain,
! [X0,X1] : meet(complement(complement(X0)),X1) = meet(X1,complement(complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f3465,f3101]) ).
fof(f3497,plain,
! [X0,X1] : meet(complement(join(complement(X0),meet(X0,X1))),X0) = meet(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f3469,f5]) ).
fof(f3515,plain,
! [X0,X1] : meet(X0,complement(join(complement(X0),X1))) = meet(X0,complement(join(complement(X0),meet(X0,X1)))),
inference(forward_demodulation,[],[f3497,f5]) ).
fof(f3619,plain,
! [X0,X1] : join(X1,complement(complement(X0))) = join(X0,join(complement(complement(X0)),X1)),
inference(superposition,[],[f50,f3385]) ).
fof(f3725,plain,
! [X0,X1] : complement(X1) = meet(complement(X1),complement(meet(X0,X1))),
inference(superposition,[],[f3,f2751]) ).
fof(f4286,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(complement(meet(complement(X0),X1)),X0),
inference(superposition,[],[f21,f3345]) ).
fof(f4303,plain,
! [X0,X1] : complement(complement(meet(complement(X0),X1))) = meet(complement(complement(meet(complement(X0),X1))),complement(X0)),
inference(superposition,[],[f3725,f3345]) ).
fof(f4312,plain,
! [X0,X1] : complement(complement(meet(complement(X0),X1))) = meet(complement(X0),complement(complement(meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f4303,f5]) ).
fof(f4321,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(meet(complement(X0),X1))),
inference(forward_demodulation,[],[f4286,f6]) ).
fof(f4332,plain,
! [X0,X1] : complement(complement(meet(complement(X0),X1))) = meet(complement(complement(X1)),complement(X0)),
inference(forward_demodulation,[],[f4312,f3493]) ).
fof(f4529,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,join(X2,meet(complement(X0),join(meet(X0,X1),X2)))),
inference(superposition,[],[f671,f6]) ).
fof(f5746,plain,
! [X0,X1] : meet(complement(X0),join(X0,meet(complement(X0),X1))) = meet(complement(X0),join(X0,meet(X1,one))),
inference(superposition,[],[f2165,f9]) ).
fof(f5885,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),join(X0,meet(complement(X0),X1))),
inference(forward_demodulation,[],[f5746,f105]) ).
fof(f6011,plain,
! [X0,X1] : meet(complement(X0),join(X0,join(complement(complement(X0)),meet(complement(X0),X1)))) = meet(complement(X0),join(X0,meet(complement(X0),join(complement(complement(X0)),X1)))),
inference(superposition,[],[f5885,f2265]) ).
fof(f6018,plain,
! [X0,X1] : meet(complement(X1),join(X1,meet(complement(X0),complement(X1)))) = meet(complement(X1),join(X1,complement(meet(complement(X1),X0)))),
inference(superposition,[],[f5885,f3155]) ).
fof(f6110,plain,
! [X0,X1] : meet(complement(X1),complement(meet(complement(X1),X0))) = meet(complement(X1),join(X1,meet(complement(X0),complement(X1)))),
inference(forward_demodulation,[],[f6018,f4321]) ).
fof(f6117,plain,
! [X0,X1] : meet(complement(X0),join(X0,join(complement(complement(X0)),meet(complement(X0),X1)))) = meet(complement(X0),join(X0,join(complement(complement(X0)),X1))),
inference(forward_demodulation,[],[f6011,f5885]) ).
fof(f6161,plain,
! [X0,X1] : meet(complement(X1),join(X1,complement(X0))) = meet(complement(X1),complement(meet(complement(X1),X0))),
inference(forward_demodulation,[],[f6110,f804]) ).
fof(f6166,plain,
! [X0,X1] : meet(complement(X0),join(X1,complement(complement(X0)))) = meet(complement(X0),join(X0,join(complement(complement(X0)),meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f6117,f3619]) ).
fof(f6190,plain,
! [X0,X1] : meet(complement(X0),complement(X1)) = meet(complement(X1),join(X1,complement(X0))),
inference(forward_demodulation,[],[f6161,f3155]) ).
fof(f6195,plain,
! [X0,X1] : meet(complement(X0),join(X1,complement(complement(X0)))) = meet(complement(X0),join(meet(complement(X0),X1),complement(complement(X0)))),
inference(forward_demodulation,[],[f6166,f3619]) ).
fof(f6224,plain,
! [X0,X1] : meet(complement(X0),join(complement(complement(X0)),meet(complement(X0),X1))) = meet(complement(X0),join(X1,complement(complement(X0)))),
inference(forward_demodulation,[],[f6195,f6]) ).
fof(f6240,plain,
! [X0,X1] : meet(complement(X0),join(complement(complement(X0)),X1)) = meet(complement(X0),join(X1,complement(complement(X0)))),
inference(forward_demodulation,[],[f6224,f2265]) ).
fof(f6276,plain,
! [X0] :
( zero != meet(complement(join(complement(X0),X0)),complement(X0))
| complement(complement(X0)) = join(X0,complement(join(complement(X0),X0))) ),
inference(superposition,[],[f1324,f6190]) ).
fof(f6304,plain,
! [X0,X1] : meet(complement(join(X1,complement(X0))),complement(X1)) = meet(complement(X1),complement(meet(complement(X0),complement(X1)))),
inference(superposition,[],[f3155,f6190]) ).
fof(f6308,plain,
! [X0,X1] : meet(complement(complement(X0)),complement(X1)) = meet(complement(join(X1,complement(X0))),complement(X1)),
inference(forward_demodulation,[],[f6304,f3101]) ).
fof(f6321,plain,
! [X0] :
( zero != meet(complement(X0),complement(join(complement(X0),X0)))
| complement(complement(X0)) = join(X0,complement(join(complement(X0),X0))) ),
inference(forward_demodulation,[],[f6276,f5]) ).
fof(f6339,plain,
! [X0,X1] : meet(complement(complement(X0)),complement(X1)) = meet(complement(X1),complement(join(X1,complement(X0)))),
inference(forward_demodulation,[],[f6308,f5]) ).
fof(f6347,plain,
! [X0] : complement(complement(X0)) = join(X0,complement(join(complement(X0),X0))),
inference(forward_subsumption_resolution,[],[f6321,f237]) ).
fof(f6362,plain,
! [X0,X1] : complement(join(X1,complement(X0))) = meet(complement(complement(X0)),complement(X1)),
inference(forward_demodulation,[],[f6339,f2623]) ).
fof(f6365,plain,
! [X0] : complement(complement(X0)) = join(X0,complement(join(X0,complement(X0)))),
inference(forward_demodulation,[],[f6347,f6]) ).
fof(f6376,plain,
! [X0,X1] : complement(complement(meet(complement(X0),X1))) = complement(join(X0,complement(X1))),
inference(backward_demodulation,[],[f4332,f6362]) ).
fof(f6377,plain,
! [X0] : complement(complement(X0)) = join(X0,complement(one)),
inference(forward_demodulation,[],[f6365,f9]) ).
fof(f6397,plain,
! [X0] : join(X0,zero) = complement(complement(X0)),
inference(forward_demodulation,[],[f6377,f261]) ).
fof(f6414,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f6397,f110]) ).
fof(f6491,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),join(X1,X0)),
inference(backward_demodulation,[],[f6240,f6414]) ).
fof(f6513,plain,
! [X0,X1] : meet(complement(X0),X1) = complement(join(X0,complement(X1))),
inference(backward_demodulation,[],[f6376,f6414]) ).
fof(f6764,plain,
! [X0,X1] : meet(complement(join(X1,X0)),complement(X0)) = meet(complement(X0),complement(meet(complement(X0),join(X0,X1)))),
inference(superposition,[],[f3155,f6491]) ).
fof(f6766,plain,
! [X0,X1] : meet(complement(join(X0,X1)),complement(X0)) = meet(complement(join(X1,X0)),complement(X0)),
inference(forward_demodulation,[],[f6764,f3155]) ).
fof(f6793,plain,
! [X0,X1] : meet(complement(join(X0,X1)),complement(X0)) = meet(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f6766,f5]) ).
fof(f6805,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X0,X1)),complement(X0)),
inference(forward_demodulation,[],[f6793,f2644]) ).
fof(f6810,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f6805,f5]) ).
fof(f6822,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),join(X0,meet(complement(X0),X1))),
inference(superposition,[],[f2265,f6414]) ).
fof(f6826,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),X1))),
inference(superposition,[],[f2623,f6414]) ).
fof(f6831,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(complement(X1),X0)),
inference(superposition,[],[f3267,f6414]) ).
fof(f6840,plain,
! [X0,X1] : meet(X0,complement(X1)) = meet(complement(X1),join(X1,X0)),
inference(superposition,[],[f6190,f6414]) ).
fof(f6843,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(X0),join(X1,X2)))) = meet(X0,join(X1,meet(X2,complement(X0)))),
inference(backward_demodulation,[],[f155,f6840]) ).
fof(f6846,plain,
! [X2,X0,X1] : meet(X2,join(X1,meet(complement(X2),join(X0,X1)))) = meet(X2,join(X1,meet(X0,complement(X2)))),
inference(backward_demodulation,[],[f549,f6840]) ).
fof(f6954,plain,
! [X2,X0,X1] : meet(complement(X0),join(X1,meet(X2,X0))) = meet(complement(X0),join(X1,meet(X0,join(X1,X2)))),
inference(backward_demodulation,[],[f1801,f6831]) ).
fof(f6987,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(X1,X2))) = meet(join(X1,meet(X0,X2)),X0),
inference(backward_demodulation,[],[f2307,f6831]) ).
fof(f6996,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),meet(X0,X1)))),
inference(backward_demodulation,[],[f3515,f6826]) ).
fof(f6999,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(meet(complement(X0),X1),complement(X0)),
inference(forward_demodulation,[],[f6822,f6840]) ).
fof(f7060,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,join(X2,meet(meet(X0,X1),complement(X0)))),
inference(backward_demodulation,[],[f4529,f6846]) ).
fof(f7104,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,join(complement(X0),join(X1,X2))),
inference(forward_demodulation,[],[f6987,f5]) ).
fof(f7124,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = complement(join(complement(X0),meet(X0,X1))),
inference(forward_demodulation,[],[f6996,f6826]) ).
fof(f7127,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),meet(complement(X0),X1)),
inference(forward_demodulation,[],[f6999,f5]) ).
fof(f7169,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,join(X2,meet(complement(X0),meet(X0,X1)))),
inference(forward_demodulation,[],[f7060,f5]) ).
fof(f7199,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = meet(X0,join(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f7104,f6831]) ).
fof(f7222,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f7127,f75]) ).
fof(f7271,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,join(X2,meet(X0,meet(X1,complement(X0))))),
inference(forward_demodulation,[],[f7169,f36]) ).
fof(f7372,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(join(X2,meet(X1,complement(X0))),X0),
inference(forward_demodulation,[],[f7271,f7199]) ).
fof(f7437,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,join(X2,meet(X1,complement(X0)))),
inference(forward_demodulation,[],[f7372,f5]) ).
fof(f7464,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,join(X1,meet(complement(X0),join(X1,X2)))),
inference(backward_demodulation,[],[f6843,f7437]) ).
fof(f7588,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),join(X1,meet(X0,X2))),
inference(superposition,[],[f7222,f339]) ).
fof(f7590,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),join(meet(X0,X2),X1)),
inference(superposition,[],[f7222,f41]) ).
fof(f7635,plain,
! [X0,X1] : meet(complement(complement(X0)),join(X0,X1)) = meet(join(X0,X1),complement(meet(complement(X0),X1))),
inference(superposition,[],[f3101,f7222]) ).
fof(f7636,plain,
! [X0,X1] : meet(complement(join(X0,X1)),complement(X0)) = meet(complement(X0),complement(meet(complement(X0),X1))),
inference(superposition,[],[f3155,f7222]) ).
fof(f7638,plain,
! [X0,X1] : meet(complement(join(X0,X1)),complement(X0)) = meet(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f7636,f3155]) ).
fof(f7639,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = meet(join(X0,X1),complement(meet(complement(X0),X1))),
inference(forward_demodulation,[],[f7635,f6414]) ).
fof(f7667,plain,
! [X2,X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f7590,f6840]) ).
fof(f7669,plain,
! [X2,X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f7588,f6840]) ).
fof(f7672,plain,
! [X0,X1] : meet(complement(X0),complement(join(X0,X1))) = meet(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f7638,f5]) ).
fof(f7673,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(complement(X0),X1))) = X0,
inference(forward_demodulation,[],[f7639,f3]) ).
fof(f7687,plain,
! [X2,X0,X1] : meet(complement(X0),join(meet(X0,X1),X2)) = meet(meet(X2,complement(meet(X0,X1))),complement(X0)),
inference(backward_demodulation,[],[f2793,f7667]) ).
fof(f7693,plain,
! [X2,X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(X1,meet(X2,X0))),
inference(backward_demodulation,[],[f6954,f7669]) ).
fof(f7696,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f7672,f2623]) ).
fof(f7706,plain,
! [X2,X0,X1] : meet(complement(X0),join(meet(X0,X1),X2)) = meet(complement(X0),meet(X2,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f7687,f5]) ).
fof(f7721,plain,
! [X0,X1] : complement(join(X1,X0)) = complement(join(join(X0,X1),X0)),
inference(backward_demodulation,[],[f6810,f7696]) ).
fof(f7725,plain,
! [X2,X0,X1] : complement(join(X0,join(X1,X2))) = complement(join(join(X0,join(X1,X2)),X2)),
inference(backward_demodulation,[],[f2651,f7696]) ).
fof(f7752,plain,
! [X2,X0,X1] : meet(complement(X0),X2) = meet(complement(X0),join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f7706,f2804]) ).
fof(f7778,plain,
! [X2,X0,X1] : complement(join(X0,join(X1,X2))) = complement(join(X2,join(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f7725,f6]) ).
fof(f7782,plain,
! [X0,X1] : complement(join(X1,X0)) = complement(join(X0,join(X0,X1))),
inference(forward_demodulation,[],[f7721,f6]) ).
fof(f7804,plain,
! [X2,X0,X1] : complement(join(X0,join(X1,X2))) = complement(join(X1,join(X2,X0))),
inference(forward_demodulation,[],[f7778,f1119]) ).
fof(f7806,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f7782,f62]) ).
fof(f7860,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(X1,complement(X0))),
inference(superposition,[],[f7464,f27]) ).
fof(f8166,plain,
! [X0,X1] :
( zero != meet(complement(X0),complement(join(complement(X0),meet(X0,X1))))
| complement(complement(X0)) = join(meet(X0,X1),complement(join(complement(X0),meet(X0,X1)))) ),
inference(superposition,[],[f1324,f7752]) ).
fof(f8195,plain,
! [X0,X1] : complement(complement(X0)) = join(meet(X0,X1),complement(join(complement(X0),meet(X0,X1)))),
inference(forward_subsumption_resolution,[],[f8166,f237]) ).
fof(f8229,plain,
! [X0,X1] : complement(complement(X0)) = join(meet(X0,X1),complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f8195,f7124]) ).
fof(f8252,plain,
! [X0,X1] : join(meet(X0,X1),complement(join(complement(X0),X1))) = X0,
inference(forward_demodulation,[],[f8229,f6414]) ).
fof(f8349,plain,
! [X0,X1] :
( zero != meet(meet(X0,X1),join(complement(join(complement(X0),X1)),complement(X0)))
| complement(meet(X0,X1)) = join(complement(join(complement(X0),X1)),complement(X0)) ),
inference(superposition,[],[f1324,f8252]) ).
fof(f8353,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),X0) = meet(complement(meet(X0,X1)),complement(join(complement(X0),X1))),
inference(superposition,[],[f7222,f8252]) ).
fof(f8356,plain,
! [X0,X1] : join(X1,X0) = join(X1,complement(join(complement(X0),X1))),
inference(superposition,[],[f59,f8252]) ).
fof(f8360,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),X0) = complement(join(join(complement(X0),X1),meet(X0,X1))),
inference(forward_demodulation,[],[f8353,f7696]) ).
fof(f8364,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,join(complement(join(complement(X0),X1)),complement(X0))))
| complement(meet(X0,X1)) = join(complement(join(complement(X0),X1)),complement(X0)) ),
inference(forward_demodulation,[],[f8349,f7]) ).
fof(f8417,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),X0) = complement(join(meet(X0,X1),join(complement(X0),X1))),
inference(forward_demodulation,[],[f8360,f7806]) ).
fof(f8420,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,complement(X0)))
| complement(meet(X0,X1)) = join(complement(join(complement(X0),X1)),complement(X0)) ),
inference(forward_demodulation,[],[f8364,f3318]) ).
fof(f8459,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),X0) = complement(join(complement(X0),join(X1,meet(X0,X1)))),
inference(forward_demodulation,[],[f8417,f7804]) ).
fof(f8461,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(join(complement(X0),X1)),complement(X0)),
inference(forward_subsumption_resolution,[],[f8420,f282]) ).
fof(f8494,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(complement(meet(X0,X1)),X0),
inference(forward_demodulation,[],[f8459,f21]) ).
fof(f8496,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f8461,f6]) ).
fof(f8518,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f8494,f5]) ).
fof(f8527,plain,
! [X0,X1] : meet(complement(X1),X0) = complement(join(complement(X0),X1)),
inference(forward_demodulation,[],[f8518,f3155]) ).
fof(f8547,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(complement(X1),X0)),
inference(backward_demodulation,[],[f8356,f8527]) ).
fof(f8551,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),meet(complement(X1),X0)),
inference(backward_demodulation,[],[f8496,f8527]) ).
fof(f8589,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),meet(X0,X1)),
inference(superposition,[],[f8547,f6414]) ).
fof(f8982,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(X1),meet(X0,X1)),
inference(superposition,[],[f8589,f5]) ).
fof(f9083,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(X1)),
inference(backward_demodulation,[],[f8551,f8982]) ).
fof(f9225,plain,
! [X0,X1] : join(X0,complement(X1)) = complement(meet(complement(X0),X1)),
inference(superposition,[],[f9083,f6414]) ).
fof(f9226,plain,
! [X0,X1] : join(complement(X1),X0) = complement(meet(X1,complement(X0))),
inference(superposition,[],[f9083,f6414]) ).
fof(f9323,plain,
! [X0,X1] : meet(join(X0,X1),join(X0,complement(X1))) = X0,
inference(backward_demodulation,[],[f7673,f9225]) ).
fof(f9397,plain,
! [X0,X1] : meet(join(X0,X1),join(X1,complement(X0))) = X1,
inference(superposition,[],[f9323,f6]) ).
fof(f9738,plain,
! [X2,X0,X1] : meet(X1,complement(join(X0,X2))) = meet(complement(join(X0,X2)),join(X1,X0)),
inference(superposition,[],[f7693,f3]) ).
fof(f10029,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(X1,complement(X0)),
inference(superposition,[],[f7860,f9083]) ).
fof(f10056,plain,
! [X0,X1] : meet(complement(X0),join(X1,complement(X0))) = meet(join(X1,complement(X0)),complement(meet(X0,X1))),
inference(superposition,[],[f3101,f7860]) ).
fof(f10082,plain,
! [X0,X1] : complement(X0) = meet(join(X1,complement(X0)),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f10056,f27]) ).
fof(f10110,plain,
! [X2,X0,X1] : meet(X1,join(X2,complement(X0))) = meet(X1,join(X2,meet(complement(meet(X0,X1)),join(X2,complement(X0))))),
inference(backward_demodulation,[],[f3071,f10082]) ).
fof(f10180,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(join(X2,X1),X0),
inference(superposition,[],[f7199,f6]) ).
fof(f10221,plain,
! [X2,X0,X1] : join(complement(X2),join(X0,meet(X2,X1))) = join(complement(X2),meet(join(X0,X1),X2)),
inference(superposition,[],[f8589,f7199]) ).
fof(f10240,plain,
! [X2,X0,X1] : join(complement(X2),join(X0,X1)) = join(complement(X2),join(X0,meet(X2,X1))),
inference(forward_demodulation,[],[f10221,f8982]) ).
fof(f12574,plain,
! [X2,X0,X1] : meet(complement(X2),join(X0,complement(X1))) = complement(join(X2,meet(complement(X0),X1))),
inference(superposition,[],[f6513,f6513]) ).
fof(f12660,plain,
! [X2,X0,X1] : meet(X1,join(X2,complement(X0))) = meet(X1,join(X2,complement(join(meet(X0,X1),meet(complement(X2),X0))))),
inference(backward_demodulation,[],[f10110,f12574]) ).
fof(f13569,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X0,X1),join(join(X1,meet(X0,X2)),complement(X0))),
inference(superposition,[],[f9397,f339]) ).
fof(f13676,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X0,X1),join(complement(X0),join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f13569,f6]) ).
fof(f13713,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X0,X1),join(complement(X0),join(X1,X2))),
inference(forward_demodulation,[],[f13676,f10240]) ).
fof(f14099,plain,
! [X2,X0,X1] : join(X2,complement(join(X0,meet(complement(X2),X1)))) = complement(meet(join(X0,X1),complement(X2))),
inference(superposition,[],[f9225,f7199]) ).
fof(f14195,plain,
! [X2,X0,X1] : join(complement(join(X0,X1)),X2) = join(X2,complement(join(X0,meet(complement(X2),X1)))),
inference(forward_demodulation,[],[f14099,f9226]) ).
fof(f14243,plain,
! [X2,X0,X1] : meet(X1,join(X2,complement(X0))) = meet(X1,join(complement(join(meet(X0,X1),X0)),X2)),
inference(backward_demodulation,[],[f12660,f14195]) ).
fof(f14263,plain,
! [X2,X0,X1] : meet(X1,join(X2,complement(X0))) = meet(X1,join(complement(join(X0,meet(X0,X1))),X2)),
inference(forward_demodulation,[],[f14243,f7806]) ).
fof(f14274,plain,
! [X2,X0,X1] : meet(X1,join(X2,complement(X0))) = meet(X1,join(complement(X0),X2)),
inference(forward_demodulation,[],[f14263,f4]) ).
fof(f14299,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X0,X2)),
inference(superposition,[],[f14274,f6414]) ).
fof(f14656,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X2,X1),X0),
inference(superposition,[],[f5,f14299]) ).
fof(f21981,plain,
! [X2,X0,X1] : meet(join(X0,X1),complement(meet(X0,complement(join(X1,X2))))) = meet(join(X0,X1),complement(complement(join(X1,X2)))),
inference(superposition,[],[f10029,f9738]) ).
fof(f22000,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X1,X2)) = meet(join(X0,X1),complement(meet(X0,complement(join(X1,X2))))),
inference(forward_demodulation,[],[f21981,f6414]) ).
fof(f22087,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X1,X2)) = meet(join(X0,X1),join(complement(X0),join(X1,X2))),
inference(forward_demodulation,[],[f22000,f9226]) ).
fof(f22159,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X1,X2)) = join(X1,meet(X0,X2)),
inference(forward_demodulation,[],[f22087,f13713]) ).
fof(f22462,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = join(meet(X0,X1),meet(X0,X2)),
inference(superposition,[],[f22159,f4]) ).
fof(f22729,plain,
! [X2,X0,X1] : meet(join(X2,X1),X0) = join(meet(X0,X1),meet(X0,X2)),
inference(forward_demodulation,[],[f22462,f10180]) ).
fof(f22848,plain,
meet(a,join(b,c)) != meet(join(c,b),a),
inference(backward_demodulation,[],[f13,f22729]) ).
fof(f22912,plain,
$false,
inference(forward_subsumption_resolution,[],[f22848,f14656]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT198-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n011.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 14:05:30 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 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
% 11.22/2.44 % (2442302)Input is clausal, will run a generic CNF schedule.
% 11.22/2.44 % (2442311)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2717403337:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.22/2.44 % (2442311)Instruction limit reached!
% 11.22/2.44 % (2442311)------------------------------
% 11.22/2.44 % (2442311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.22/2.44 % (2442311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/2.44 % (2442311)CaDiCaL version: 2.1.3
% 11.22/2.44 % (2442311)Termination reason: Instruction limit
% 11.22/2.44 % (2442311)Termination phase: Saturation
% 11.22/2.44 % (2442311)Time elapsed: 0.038 s
% 11.22/2.44 % (2442311)Peak memory usage: 89 MB
% 11.22/2.44 % (2442311)Instructions burned: 115 (million)
% 11.22/2.44 % (2442307)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=860514676:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.22/2.44 % (2442308)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2551815192:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.22/2.44 % (2442313)dis-21_1_sil=8000:lcm=predicate:random_seed=3088332314: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)
% 11.22/2.44 % (2442309)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2048240386:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.22/2.44 % (2442312)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3575703505:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.22/2.44 % (2442310)lrs+10_1_sil=8000:sp=occurrence:random_seed=1222633522:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.22/2.44 % (2442313)Refutation not found, incomplete strategy
% 11.22/2.44 % (2442313)------------------------------
% 11.22/2.44 % (2442313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.22/2.44 % (2442313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/2.44 % (2442313)CaDiCaL version: 2.1.3
% 11.22/2.44 % (2442313)Termination reason: Refutation not found, incomplete strategy
% 11.22/2.44 % (2442313)Time elapsed: 0.002 s
% 11.22/2.44 % (2442313)Peak memory usage: 88 MB
% 11.22/2.44 % (2442313)Instructions burned: 1 (million)
% 11.22/2.44 % (2442310)Instruction limit reached!
% 11.22/2.44 % (2442310)------------------------------
% 11.22/2.44 % (2442310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.22/2.44 % (2442310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/2.44 % (2442310)CaDiCaL version: 2.1.3
% 11.22/2.44 % (2442310)Termination reason: Instruction limit
% 11.22/2.44 % (2442310)Termination phase: Saturation
% 11.22/2.44 % (2442310)Time elapsed: 0.064 s
% 11.22/2.44 % (2442310)Peak memory usage: 88 MB
% 11.22/2.44 % (2442310)Instructions burned: 107 (million)
% 11.22/2.44 % (2442312)Instruction limit reached!
% 11.22/2.44 % (2442312)------------------------------
% 11.22/2.44 % (2442312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.22/2.44 % (2442312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/2.44 % (2442312)CaDiCaL version: 2.1.3
% 11.22/2.44 % (2442312)Termination reason: Instruction limit
% 11.22/2.44 % (2442312)Termination phase: Saturation
% 11.22/2.44 % (2442312)Time elapsed: 0.101 s
% 11.22/2.44 % (2442312)Peak memory usage: 89 MB
% 11.22/2.44 % (2442312)Instructions burned: 181 (million)
% 11.22/2.44 % (2442315)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=1820956224:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 11.22/2.44 % (2442315)Refutation not found, incomplete strategy
% 11.22/2.44 % (2442315)------------------------------
% 11.22/2.44 % (2442315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.22/2.44 % (2442315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/2.44 % (2442315)CaDiCaL version: 2.1.3
% 11.22/2.44 % (2442315)Termination reason: Refutation not found, incomplete strategy
% 11.22/2.44 % (2442315)Time elapsed: 0.001 s
% 11.22/2.44 % (2442315)Peak memory usage: 88 MB
% 11.22/2.44 % (2442322)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3604610607: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)
% 20.88/3.86 % (2442322)Refutation not found, incomplete strategy
% 20.88/3.86 % (2442322)------------------------------
% 20.88/3.86 % (2442322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.86 % (2442322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.86 % (2442322)CaDiCaL version: 2.1.3
% 20.88/3.86 % (2442322)Termination reason: Refutation not found, incomplete strategy
% 20.88/3.86 % (2442322)Time elapsed: 0.002 s
% 20.88/3.86 % (2442322)Peak memory usage: 88 MB
% 20.88/3.86 % (2442322)Instructions burned: 1 (million)
% 20.88/3.86 % (2442313)------------------------------
% 20.88/3.86 % (2442313)------------------------------
% 20.88/3.86 % (2442323)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3980335584:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 20.88/3.86 % (2442323)Refutation not found, incomplete strategy
% 20.88/3.86 % (2442323)------------------------------
% 20.88/3.86 % (2442323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.86 % (2442323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.86 % (2442323)CaDiCaL version: 2.1.3
% 20.88/3.86 % (2442323)Termination reason: Refutation not found, incomplete strategy
% 20.88/3.86 % (2442323)Time elapsed: 0.001 s
% 20.88/3.86 % (2442323)Peak memory usage: 87 MB
% 20.88/3.86 % (2442315)------------------------------
% 20.88/3.86 % (2442315)------------------------------
% 20.88/3.86 % (2442328)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1046862244:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 20.88/3.86 % (2442326)lrs+10_64_to=lpo:sil=8000:random_seed=1120829456:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 20.88/3.86 % (2442322)------------------------------
% 20.88/3.86 % (2442322)------------------------------
% 20.88/3.86 % (2442328)Instruction limit reached!
% 20.88/3.86 % (2442328)------------------------------
% 20.88/3.86 % (2442328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.86 % (2442328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.86 % (2442328)CaDiCaL version: 2.1.3
% 20.88/3.86 % (2442328)Termination reason: Instruction limit
% 20.88/3.86 % (2442328)Termination phase: Saturation
% 20.88/3.86 % (2442328)Time elapsed: 0.062 s
% 20.88/3.86 % (2442328)Peak memory usage: 90 MB
% 20.88/3.86 % (2442328)Instructions burned: 195 (million)
% 20.88/3.86 % (2442326)Instruction limit reached!
% 20.88/3.86 % (2442326)------------------------------
% 20.88/3.86 % (2442326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.86 % (2442326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.86 % (2442326)CaDiCaL version: 2.1.3
% 20.88/3.86 % (2442326)Termination reason: Instruction limit
% 20.88/3.86 % (2442326)Termination phase: Saturation
% 20.88/3.86 % (2442326)Time elapsed: 0.072 s
% 20.88/3.86 % (2442326)Peak memory usage: 88 MB
% 20.88/3.86 % (2442326)Instructions burned: 126 (million)
% 20.88/3.86 % (2442323)------------------------------
% 20.88/3.86 % (2442323)------------------------------
% 20.88/3.86 % (2442331)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1601670807:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 20.88/3.86 % (2442332)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1268026977:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 20.88/3.86 % (2442333)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=2509092623:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 20.88/3.86 % (2442331)Instruction limit reached!
% 20.88/3.86 % (2442331)------------------------------
% 20.88/3.86 % (2442331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.86 % (2442331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.86 % (2442331)CaDiCaL version: 2.1.3
% 20.88/3.86 % (2442331)Termination reason: Instruction limit
% 20.88/3.86 % (2442331)Termination phase: Saturation
% 20.88/3.86 % (2442331)Time elapsed: 0.052 s
% 20.88/3.86 % (2442331)Peak memory usage: 90 MB
% 20.88/3.86 % (2442331)Instructions burned: 158 (million)
% 20.88/3.86 % (2442334)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3389845144:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 20.88/3.86 % (2442334)Refutation not found, incomplete strategy
% 20.88/3.86 % (2442334)------------------------------
% 20.88/3.86 % (2442334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.86 % (2442334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.86 % (2442334)CaDiCaL version: 2.1.3
% 20.88/3.86 % (2442334)Termination reason: Refutation not found, incomplete strategy
% 20.88/3.86 % (2442334)Time elapsed: 0.001 s
% 20.88/3.86 % (2442334)Peak memory usage: 87 MB
% 20.88/3.86 % (2442333)Instruction limit reached!
% 20.88/3.86 % (2442333)------------------------------
% 20.88/3.86 % (2442333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.86 % (2442333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.86 % (2442333)CaDiCaL version: 2.1.3
% 20.88/3.86 % (2442333)Termination reason: Instruction limit
% 20.88/3.86 % (2442333)Termination phase: Saturation
% 20.88/3.86 % (2442333)Time elapsed: 0.070 s
% 20.88/3.86 % (2442333)Peak memory usage: 89 MB
% 20.88/3.86 % (2442333)Instructions burned: 106 (million)
% 20.88/3.86 % (2442338)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=360261010:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 20.88/3.86 % (2442338)Instruction limit reached!
% 20.88/3.86 % (2442338)------------------------------
% 20.88/3.86 % (2442338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.86 % (2442338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.86 % (2442338)CaDiCaL version: 2.1.3
% 20.88/3.86 % (2442338)Termination reason: Instruction limit
% 20.88/3.86 % (2442338)Termination phase: Saturation
% 20.88/3.86 % (2442338)Time elapsed: 0.076 s
% 20.88/3.86 % (2442338)Peak memory usage: 90 MB
% 20.88/3.86 % (2442338)Instructions burned: 243 (million)
% 20.88/3.86 % (2442340)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1813437766:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 20.88/3.86 % (2442334)------------------------------
% 20.88/3.86 % (2442334)------------------------------
% 20.88/3.86 % (2442342)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3640060872:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 20.88/3.86 % (2442342)Instruction limit reached!
% 20.88/3.86 % (2442342)------------------------------
% 20.88/3.86 % (2442342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.86 % (2442342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.86 % (2442342)CaDiCaL version: 2.1.3
% 20.88/3.86 % (2442342)Termination reason: Instruction limit
% 20.88/3.86 % (2442342)Termination phase: Saturation
% 20.88/3.86 % (2442342)Time elapsed: 0.042 s
% 20.88/3.86 % (2442342)Peak memory usage: 89 MB
% 20.88/3.86 % (2442342)Instructions burned: 135 (million)
% 20.88/3.86 % (2442344)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1265002498:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 20.88/3.86 % (2442346)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1690497750:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 20.88/3.86 % (2442346)Instruction limit reached!
% 20.88/3.86 % (2442346)------------------------------
% 20.88/3.86 % (2442346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.86 % (2442346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.86 % (2442346)CaDiCaL version: 2.1.3
% 20.88/3.86 % (2442346)Termination reason: Instruction limit
% 20.88/3.86 % (2442346)Termination phase: Saturation
% 20.88/3.86 % (2442346)Time elapsed: 0.063 s
% 20.88/3.86 % (2442346)Peak memory usage: 91 MB
% 20.88/3.86 % (2442346)Instructions burned: 191 (million)
% 20.88/3.86 % (2442349)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2729850111:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 20.88/3.86 % (2442344)Instruction limit reached!
% 20.88/3.86 % (2442344)------------------------------
% 20.88/3.86 % (2442344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.86 % (2442344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.86 % (2442344)CaDiCaL version: 2.1.3
% 20.88/3.86 % (2442344)Termination reason: Instruction limit
% 20.88/3.86 % (2442344)Termination phase: Saturation
% 20.88/3.86 % (2442344)Time elapsed: 0.309 s
% 20.88/3.86 % (2442344)Peak memory usage: 93 MB
% 20.88/3.86 % (2442344)Instructions burned: 499 (million)
% 20.88/3.86 % (2442349)Instruction limit reached!
% 20.88/3.86 % (2442349)------------------------------
% 20.88/3.86 % (2442349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.86 % (2442349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.86 % (2442349)CaDiCaL version: 2.1.3
% 20.88/3.86 % (2442349)Termination reason: Instruction limit
% 20.88/3.86 % (2442349)Termination phase: Saturation
% 20.88/3.86 % (2442349)Time elapsed: 0.084 s
% 20.88/3.86 % (2442349)Peak memory usage: 92 MB
% 20.88/3.86 % (2442349)Instructions burned: 267 (million)
% 20.88/3.86 % (2442352)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=3320796192:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 20.88/3.86 % (2442351)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2471945695:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 20.88/3.86 % (2442351)Instruction limit reached!
% 20.88/3.86 % (2442351)------------------------------
% 20.88/3.86 % (2442351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.86 % (2442351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.86 % (2442351)CaDiCaL version: 2.1.3
% 20.88/3.86 % (2442351)Termination reason: Instruction limit
% 20.88/3.86 % (2442351)Termination phase: Saturation
% 20.88/3.86 % (2442351)Time elapsed: 0.094 s
% 20.88/3.86 % (2442351)Peak memory usage: 89 MB
% 20.88/3.86 % (2442351)Instructions burned: 156 (million)
% 20.88/3.86 % (2442355)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3712073877:i=537:av=off:ss=included_2981 on theBenchmark for (2981ds/537Mi)
% 20.88/3.86 % (2442355)Instruction limit reached!
% 20.88/3.86 % (2442355)------------------------------
% 20.88/3.86 % (2442355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.86 % (2442355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.86 % (2442355)CaDiCaL version: 2.1.3
% 20.88/3.86 % (2442355)Termination reason: Instruction limit
% 20.88/3.86 % (2442355)Termination phase: Saturation
% 20.88/3.86 % (2442355)Time elapsed: 0.286 s
% 20.88/3.86 % (2442355)Peak memory usage: 93 MB
% 20.88/3.86 % (2442355)Instructions burned: 538 (million)
% 20.88/3.86 % (2442357)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2211151341:i=180:bd=preordered:av=off_2977 on theBenchmark for (2977ds/180Mi)
% 20.88/3.86 % (2442357)Instruction limit reached!
% 20.88/3.86 % (2442357)------------------------------
% 20.88/3.86 % (2442357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.86 % (2442357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.86 % (2442357)CaDiCaL version: 2.1.3
% 20.88/3.86 % (2442357)Termination reason: Instruction limit
% 20.88/3.86 % (2442357)Termination phase: Saturation
% 20.88/3.86 % (2442357)Time elapsed: 0.101 s
% 20.88/3.86 % (2442357)Peak memory usage: 88 MB
% 20.88/3.86 % (2442357)Instructions burned: 181 (million)
% 20.88/3.86 % (2442359)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=788556038:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2974 on theBenchmark for (2974ds/10307Mi)
% 20.88/3.86 % (2442352)First to succeed.
% 20.88/3.86 % (2442352)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2442302"
% 20.88/3.86 % (2442332)Instruction limit reached!
% 20.88/3.86 % (2442332)------------------------------
% 20.88/3.86 % (2442332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.86 % (2442332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.86 % (2442332)CaDiCaL version: 2.1.3
% 20.88/3.86 % (2442332)Termination reason: Instruction limit
% 20.88/3.86 % (2442332)Termination phase: Saturation
% 20.88/3.86 % (2442332)Time elapsed: 2.093 s
% 20.88/3.86 % (2442332)Peak memory usage: 152 MB
% 20.88/3.86 % (2442332)Instructions burned: 3394 (million)
% 20.88/3.86 % (2442352)Refutation found. Thanks to Tanya!
% 20.88/3.86 % SZS status Unsatisfiable for theBenchmark
% 20.88/3.86 % SZS output start Proof for theBenchmark
% See solution above
% 21.89/4.06 % (2442352)------------------------------
% 21.89/4.06 % (2442352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.89/4.06 % (2442352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.89/4.06 % (2442352)CaDiCaL version: 2.1.3
% 21.89/4.06 % (2442352)Termination reason: Refutation
% 21.89/4.06 % (2442352)Time elapsed: 1.099 s
% 21.89/4.06 % (2442352)Peak memory usage: 147 MB
% 21.89/4.06 % (2442352)Instructions burned: 3215 (million)
% 21.89/4.06 % (2442352)------------------------------
% 21.89/4.06 % (2442352)------------------------------
% 21.89/4.06 % (2442302)Success in time 3.009 s
% 21.89/4.06 % Vampire exiting
%------------------------------------------------------------------------------