%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : REL029-4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.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 12:33:56 PM UTC 2026
% Result : Unsatisfiable 19.29s 4.17s
% Output : Refutation 22.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 102
% Number of leaves : 15
% Syntax : Number of formulae : 370 ( 352 unt; 0 def)
% Number of atoms : 388 ( 387 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 66 ( 48 ~; 18 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 555 ( 555 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux1_join_commutativity_1) ).
fof(f2,axiom,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux2_join_associativity_2) ).
fof(f3,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux3_a_kind_of_de_Morgan_3) ).
fof(f4,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(reorient_equations,[],[f3]) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux4_definiton_of_meet_4) ).
fof(f6,plain,
! [X0,X1] : complement(join(complement(X0),complement(X1))) = meet(X0,X1),
inference(reorient_equations,[],[f5]) ).
fof(f7,axiom,
! [X2,X0,X1] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',composition_associativity_5) ).
fof(f8,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',composition_identity_6) ).
fof(f9,axiom,
! [X2,X0,X1] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',composition_distributivity_7) ).
fof(f10,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_idempotence_8) ).
fof(f11,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_additivity_9) ).
fof(f12,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_multiplicativity_10) ).
fof(f13,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_cancellativity_11) ).
fof(f14,plain,
! [X0,X1] : complement(X1) = join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)),
inference(reorient_equations,[],[f13]) ).
fof(f15,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_top_12) ).
fof(f23,negated_conjecture,
join(sk1,one) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_17) ).
fof(f24,plain,
one = join(sk1,one),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
join(sk2,one) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_18) ).
fof(f26,plain,
one = join(sk2,one),
inference(reorient_equations,[],[f25]) ).
fof(f27,negated_conjecture,
( join(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))) != meet(composition(sk1,sk3),composition(sk2,sk3))
| join(meet(composition(sk1,sk3),composition(sk2,sk3)),composition(meet(sk1,sk2),sk3)) != composition(meet(sk1,sk2),sk3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_19) ).
fof(f28,plain,
( meet(composition(sk1,sk3),composition(sk2,sk3)) != join(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3)))
| composition(meet(sk1,sk2),sk3) != join(meet(composition(sk1,sk3),composition(sk2,sk3)),composition(meet(sk1,sk2),sk3)) ),
inference(reorient_equations,[],[f27]) ).
fof(f33,plain,
( complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) != join(composition(complement(join(complement(sk1),complement(sk2))),sk3),complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))))
| composition(complement(join(complement(sk1),complement(sk2))),sk3) != join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(join(complement(sk1),complement(sk2))),sk3)) ),
inference(definition_unfolding,[],[f28,f6,f6,f6,f6,f6,f6]) ).
fof(f34,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[],[f11,f10]) ).
fof(f41,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[],[f12,f10]) ).
fof(f42,plain,
! [X2,X0,X1] : composition(join(converse(X1),X2),converse(X0)) = join(converse(composition(X0,X1)),composition(X2,converse(X0))),
inference(superposition,[],[f9,f12]) ).
fof(f55,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = join(converse(composition(X0,X2)),converse(composition(X0,X1))),
inference(superposition,[],[f42,f12]) ).
fof(f60,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = converse(join(composition(X0,X2),composition(X0,X1))),
inference(forward_demodulation,[],[f55,f11]) ).
fof(f63,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = composition(converse(join(X2,X1)),converse(X0)),
inference(forward_demodulation,[],[f60,f11]) ).
fof(f65,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = converse(composition(X0,join(X2,X1))),
inference(forward_demodulation,[],[f63,f12]) ).
fof(f78,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f135,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f2,f15]) ).
fof(f141,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f41,f8]) ).
fof(f153,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f141,f10]) ).
fof(f165,plain,
one = converse(one),
inference(superposition,[],[f8,f153]) ).
fof(f180,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X1),X0))) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f181,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(join(complement(join(complement(X0),complement(X1))),complement(complement(join(complement(X0),X1))))),complement(X0)),
inference(superposition,[],[f4,f4]) ).
fof(f183,plain,
! [X0,X1] : join(complement(join(complement(X1),complement(X0))),complement(join(X0,complement(X1)))) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f191,plain,
! [X2,X0,X1] : join(X0,X2) = join(complement(join(complement(X0),complement(X1))),join(complement(join(complement(X0),X1)),X2)),
inference(superposition,[],[f2,f4]) ).
fof(f193,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(superposition,[],[f1,f4]) ).
fof(f194,plain,
! [X2,X0,X1] : join(X0,X2) = join(complement(join(complement(X0),X1)),join(X2,complement(join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f191,f78]) ).
fof(f199,plain,
! [X0,X1] : join(complement(join(X0,complement(X1))),complement(join(complement(X1),complement(X0)))) = X1,
inference(forward_demodulation,[],[f183,f1]) ).
fof(f201,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(X0),complement(join(complement(join(complement(X0),complement(X1))),complement(complement(join(complement(X0),X1)))))),
inference(forward_demodulation,[],[f181,f1]) ).
fof(f202,plain,
! [X0,X1] : join(complement(join(complement(X1),X0)),complement(join(complement(X0),complement(X1)))) = X1,
inference(forward_demodulation,[],[f180,f1]) ).
fof(f205,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(X0),complement(join(complement(complement(join(complement(X0),X1))),complement(join(complement(X0),complement(X1)))))),
inference(forward_demodulation,[],[f201,f1]) ).
fof(f263,plain,
! [X0,X1] : join(X1,complement(join(complement(X0),X1))) = join(complement(join(complement(X1),X0)),X0),
inference(superposition,[],[f194,f202]) ).
fof(f272,plain,
! [X0,X1] : join(X1,complement(join(complement(X0),X1))) = join(X0,complement(join(complement(X1),X0))),
inference(forward_demodulation,[],[f263,f1]) ).
fof(f383,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X0,X2)) = converse(converse(composition(X0,join(X1,X2)))),
inference(superposition,[],[f10,f65]) ).
fof(f395,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = join(composition(X0,X1),composition(X0,X2)),
inference(forward_demodulation,[],[f383,f10]) ).
fof(f419,plain,
! [X0,X1] : join(X0,composition(X0,X1)) = composition(X0,join(one,X1)),
inference(superposition,[],[f395,f8]) ).
fof(f423,plain,
! [X0,X1] : composition(X0,join(X1,one)) = join(composition(X0,X1),X0),
inference(superposition,[],[f395,f8]) ).
fof(f429,plain,
! [X0,X1] : composition(join(X0,X0),X1) = composition(X0,join(X1,X1)),
inference(superposition,[],[f9,f395]) ).
fof(f436,plain,
! [X0,X1] : join(X0,composition(X0,X1)) = composition(X0,join(X1,one)),
inference(forward_demodulation,[],[f423,f1]) ).
fof(f511,plain,
! [X0] : composition(X0,one) = join(X0,composition(X0,sk1)),
inference(superposition,[],[f436,f24]) ).
fof(f512,plain,
! [X0] : composition(X0,one) = join(X0,composition(X0,sk2)),
inference(superposition,[],[f436,f26]) ).
fof(f545,plain,
! [X0] : join(X0,composition(X0,sk2)) = X0,
inference(forward_demodulation,[],[f512,f8]) ).
fof(f546,plain,
! [X0] : join(X0,composition(X0,sk1)) = X0,
inference(forward_demodulation,[],[f511,f8]) ).
fof(f664,plain,
! [X2,X3,X0,X1] : composition(join(X3,composition(X0,X1)),X2) = join(composition(X3,X2),composition(X0,composition(X1,X2))),
inference(superposition,[],[f9,f7]) ).
fof(f698,plain,
! [X0] : composition(one,X0) = X0,
inference(superposition,[],[f153,f165]) ).
fof(f754,plain,
! [X0] : complement(X0) = join(complement(composition(one,X0)),complement(X0)),
inference(superposition,[],[f14,f153]) ).
fof(f766,plain,
! [X0] : complement(X0) = join(complement(X0),complement(composition(one,X0))),
inference(forward_demodulation,[],[f754,f1]) ).
fof(f779,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(forward_demodulation,[],[f766,f698]) ).
fof(f795,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = join(X0,complement(join(complement(X0),complement(X1)))),
inference(superposition,[],[f194,f779]) ).
fof(f801,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),join(X1,complement(X0))),
inference(superposition,[],[f78,f779]) ).
fof(f807,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f795,f193]) ).
fof(f833,plain,
! [X0] : join(X0,complement(top)) = X0,
inference(superposition,[],[f807,f15]) ).
fof(f836,plain,
! [X0,X1] : join(X1,complement(join(complement(X0),complement(X1)))) = X1,
inference(superposition,[],[f807,f1]) ).
fof(f842,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),X0) = join(X0,X0),
inference(superposition,[],[f194,f807]) ).
fof(f858,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = join(X0,X0),
inference(forward_demodulation,[],[f842,f1]) ).
fof(f1015,plain,
! [X0] : top = join(complement(X0),complement(join(complement(complement(join(complement(X0),complement(X0)))),complement(top)))),
inference(superposition,[],[f205,f15]) ).
fof(f1041,plain,
! [X0] : top = join(complement(X0),complement(complement(complement(join(complement(X0),complement(X0)))))),
inference(forward_demodulation,[],[f1015,f833]) ).
fof(f1051,plain,
! [X0] : top = join(complement(X0),complement(complement(complement(complement(X0))))),
inference(forward_demodulation,[],[f1041,f779]) ).
fof(f1082,plain,
! [X0,X1] : join(X1,X0) = join(complement(join(complement(X1),X0)),X0),
inference(superposition,[],[f194,f836]) ).
fof(f1099,plain,
! [X0,X1] : join(X1,X0) = join(X0,complement(join(complement(X1),X0))),
inference(forward_demodulation,[],[f1082,f1]) ).
fof(f1130,plain,
! [X0] : join(complement(join(complement(X0),complement(X0))),complement(top)) = X0,
inference(superposition,[],[f199,f15]) ).
fof(f1143,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),X0) = join(X0,complement(join(X1,complement(X0)))),
inference(superposition,[],[f194,f199]) ).
fof(f1156,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = join(X0,complement(join(X1,complement(X0)))),
inference(forward_demodulation,[],[f1143,f1]) ).
fof(f1167,plain,
! [X0] : complement(join(complement(X0),complement(X0))) = X0,
inference(forward_demodulation,[],[f1130,f833]) ).
fof(f1181,plain,
! [X0,X1] : join(X0,X0) = join(X0,complement(join(X1,complement(X0)))),
inference(forward_demodulation,[],[f1156,f858]) ).
fof(f1190,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f1167,f779]) ).
fof(f1228,plain,
! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),complement(join(X0,complement(X1)))),
inference(superposition,[],[f199,f1190]) ).
fof(f1230,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(complement(X1),X0))),
inference(superposition,[],[f202,f1190]) ).
fof(f1231,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(complement(complement(join(X0,X1))),complement(join(X0,complement(X1)))))),
inference(superposition,[],[f205,f1190]) ).
fof(f1235,plain,
! [X0] : join(X0,X0) = X0,
inference(superposition,[],[f779,f1190]) ).
fof(f1237,plain,
! [X0,X1] : join(X1,complement(join(complement(X1),X0))) = X1,
inference(superposition,[],[f807,f1190]) ).
fof(f1239,plain,
! [X0,X1] : join(X1,complement(join(X0,complement(X1)))) = X1,
inference(superposition,[],[f836,f1190]) ).
fof(f1242,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(join(X0,X1),complement(join(X0,complement(X1)))))),
inference(forward_demodulation,[],[f1231,f1190]) ).
fof(f1250,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,join(X1,complement(join(X0,complement(X1))))))),
inference(forward_demodulation,[],[f1242,f2]) ).
fof(f1251,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,join(X1,X1)))),
inference(forward_demodulation,[],[f1250,f1181]) ).
fof(f1252,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f1251,f1235]) ).
fof(f1253,plain,
! [X0,X1] : join(complement(X0),complement(X0)) = join(complement(X0),complement(join(X1,X0))),
inference(superposition,[],[f1181,f1190]) ).
fof(f1271,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X0))),complement(join(complement(X0),join(X1,complement(complement(X0)))))) = X0,
inference(superposition,[],[f4,f1181]) ).
fof(f1313,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X0))),complement(join(complement(X0),join(X1,X0)))) = X0,
inference(forward_demodulation,[],[f1271,f1190]) ).
fof(f1327,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f1253,f779]) ).
fof(f1343,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X0))),complement(join(X0,join(complement(X0),X1)))) = X0,
inference(forward_demodulation,[],[f1313,f78]) ).
fof(f1364,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X0))),complement(join(top,X1))) = X0,
inference(forward_demodulation,[],[f1343,f135]) ).
fof(f1381,plain,
! [X0,X1] : join(complement(complement(X0)),complement(join(top,X1))) = X0,
inference(forward_demodulation,[],[f1364,f779]) ).
fof(f1396,plain,
! [X0,X1] : join(X0,complement(join(top,X1))) = X0,
inference(forward_demodulation,[],[f1381,f1190]) ).
fof(f1416,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(X1,complement(X0)),
inference(superposition,[],[f1252,f1]) ).
fof(f1418,plain,
! [X2,X0,X1] : join(X1,complement(join(X2,X0))) = join(X1,complement(join(X0,join(X1,X2)))),
inference(superposition,[],[f1252,f78]) ).
fof(f1941,plain,
! [X0] : complement(composition(X0,sk2)) = join(complement(composition(X0,sk2)),complement(X0)),
inference(superposition,[],[f1327,f545]) ).
fof(f1974,plain,
! [X0,X1] : join(complement(X0),complement(complement(join(X1,X0)))) = join(complement(X0),complement(join(complement(complement(complement(X0))),complement(join(complement(X0),complement(complement(join(X1,X0)))))))),
inference(superposition,[],[f205,f1327]) ).
fof(f1989,plain,
! [X0,X1] : join(complement(X0),join(X1,X0)) = join(complement(X0),complement(join(complement(complement(complement(X0))),complement(join(complement(X0),join(X1,X0)))))),
inference(forward_demodulation,[],[f1974,f1190]) ).
fof(f2009,plain,
! [X0] : complement(composition(X0,sk2)) = join(complement(X0),complement(composition(X0,sk2))),
inference(forward_demodulation,[],[f1941,f1]) ).
fof(f2021,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(complement(X0),complement(join(complement(complement(complement(X0))),complement(join(X0,join(complement(X0),X1)))))),
inference(forward_demodulation,[],[f1989,f78]) ).
fof(f2045,plain,
! [X0,X1] : join(top,X1) = join(complement(X0),complement(join(complement(complement(complement(X0))),complement(join(top,X1))))),
inference(forward_demodulation,[],[f2021,f135]) ).
fof(f2054,plain,
! [X0,X1] : join(top,X1) = join(complement(X0),complement(complement(complement(complement(X0))))),
inference(forward_demodulation,[],[f2045,f1396]) ).
fof(f2059,plain,
! [X1] : top = join(top,X1),
inference(forward_demodulation,[],[f2054,f1051]) ).
fof(f2100,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(join(complement(X0),X2),complement(join(X0,X1))),
inference(superposition,[],[f1237,f194]) ).
fof(f2177,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(X0),join(X2,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f2100,f2]) ).
fof(f2236,plain,
! [X0] : complement(X0) = join(complement(top),complement(join(X0,complement(top)))),
inference(superposition,[],[f1228,f2059]) ).
fof(f2251,plain,
! [X0,X1] : complement(X1) = join(complement(join(X0,X1)),complement(join(complement(X0),X1))),
inference(superposition,[],[f1228,f1]) ).
fof(f2288,plain,
! [X0,X1] : join(complement(join(X1,X0)),complement(complement(X0))) = join(complement(join(X1,X0)),complement(complement(join(X0,complement(X1))))),
inference(superposition,[],[f1252,f1228]) ).
fof(f2293,plain,
! [X0,X1] : join(complement(join(X1,X0)),complement(complement(X0))) = join(complement(join(X1,X0)),join(X0,complement(X1))),
inference(forward_demodulation,[],[f2288,f1190]) ).
fof(f2334,plain,
! [X0] : complement(X0) = join(complement(top),complement(X0)),
inference(forward_demodulation,[],[f2236,f1416]) ).
fof(f2363,plain,
! [X0,X1] : join(complement(join(X1,X0)),complement(complement(X0))) = join(complement(X1),join(complement(join(X1,X0)),X0)),
inference(forward_demodulation,[],[f2293,f78]) ).
fof(f2408,plain,
! [X0,X1] : join(complement(join(X1,X0)),complement(complement(X0))) = join(complement(X1),join(X0,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f2363,f1]) ).
fof(f2445,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(join(X1,X0)),complement(complement(X0))),
inference(forward_demodulation,[],[f2408,f2177]) ).
fof(f2471,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(complement(X0)),complement(join(X1,X0))),
inference(forward_demodulation,[],[f2445,f1]) ).
fof(f2490,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(join(X1,X0))),
inference(forward_demodulation,[],[f2471,f1190]) ).
fof(f4011,plain,
! [X0,X1] : complement(join(complement(X1),X0)) = join(complement(join(top,X0)),complement(join(join(complement(X1),X0),complement(X1)))),
inference(superposition,[],[f1228,f135]) ).
fof(f4040,plain,
! [X0,X1] : complement(join(complement(X1),X0)) = join(complement(join(top,X0)),complement(join(complement(X1),join(X0,complement(X1))))),
inference(forward_demodulation,[],[f4011,f2]) ).
fof(f4102,plain,
! [X0,X1] : complement(join(complement(X1),X0)) = join(complement(join(top,X0)),complement(join(X0,complement(X1)))),
inference(forward_demodulation,[],[f4040,f801]) ).
fof(f4131,plain,
! [X0,X1] : complement(join(complement(X1),X0)) = join(complement(top),complement(join(X0,complement(X1)))),
inference(forward_demodulation,[],[f4102,f2059]) ).
fof(f4148,plain,
! [X0,X1] : complement(join(complement(X1),X0)) = complement(join(X0,complement(X1))),
inference(forward_demodulation,[],[f4131,f2334]) ).
fof(f5895,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(superposition,[],[f4148,f1190]) ).
fof(f6277,plain,
! [X2,X0,X1] : join(complement(X2),complement(join(X0,X1))) = join(complement(X2),complement(join(complement(complement(join(complement(X2),join(X1,X0)))),complement(join(complement(X2),complement(join(X0,X1))))))),
inference(superposition,[],[f205,f5895]) ).
fof(f6293,plain,
! [X2,X0,X1] : join(X1,X0) = join(join(X1,X0),complement(join(X2,complement(join(X0,X1))))),
inference(superposition,[],[f1239,f5895]) ).
fof(f6300,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,complement(join(X2,complement(join(X0,X1)))))),
inference(forward_demodulation,[],[f6293,f2]) ).
fof(f6311,plain,
! [X2,X0,X1] : join(complement(X2),complement(join(X0,X1))) = join(complement(X2),complement(join(join(complement(X2),join(X1,X0)),complement(join(complement(X2),complement(join(X0,X1))))))),
inference(forward_demodulation,[],[f6277,f1190]) ).
fof(f6370,plain,
! [X2,X0,X1] : join(complement(X2),complement(join(X0,X1))) = join(complement(X2),complement(join(complement(X2),join(join(X1,X0),complement(join(complement(X2),complement(join(X0,X1)))))))),
inference(forward_demodulation,[],[f6311,f2]) ).
fof(f6392,plain,
! [X2,X0,X1] : join(complement(X2),complement(join(X0,X1))) = join(complement(X2),complement(join(join(X1,X0),complement(join(complement(X2),complement(join(X0,X1))))))),
inference(forward_demodulation,[],[f6370,f1252]) ).
fof(f6405,plain,
! [X2,X0,X1] : join(complement(X2),complement(join(X0,X1))) = join(complement(X2),complement(join(X1,join(X0,complement(join(complement(X2),complement(join(X0,X1)))))))),
inference(forward_demodulation,[],[f6392,f2]) ).
fof(f6411,plain,
! [X2,X0,X1] : join(complement(X2),complement(join(X0,X1))) = join(complement(X2),complement(join(X1,X0))),
inference(forward_demodulation,[],[f6405,f6300]) ).
fof(f6453,plain,
! [X2,X0,X1] : join(X0,complement(join(X2,X1))) = join(X0,complement(join(X1,X2))),
inference(superposition,[],[f6411,f1190]) ).
fof(f6463,plain,
! [X2,X3,X0,X1] : join(complement(X3),complement(join(X2,join(X0,X1)))) = join(complement(X3),complement(join(X0,join(X1,X2)))),
inference(superposition,[],[f6411,f2]) ).
fof(f6609,plain,
! [X2,X0,X1] : join(complement(X0),complement(join(X1,X2))) = join(complement(join(X2,X1)),complement(X0)),
inference(superposition,[],[f1,f6411]) ).
fof(f6994,plain,
! [X2,X0,X1] : join(X0,complement(join(X1,X2))) = join(complement(join(X2,X1)),X0),
inference(superposition,[],[f1,f6453]) ).
fof(f7979,plain,
! [X0] : converse(converse(X0)) = join(X0,converse(composition(converse(X0),sk1))),
inference(superposition,[],[f34,f546]) ).
fof(f7980,plain,
! [X0] : converse(converse(X0)) = join(X0,converse(composition(converse(X0),sk2))),
inference(superposition,[],[f34,f545]) ).
fof(f7996,plain,
! [X0] : converse(converse(X0)) = join(X0,composition(converse(sk2),X0)),
inference(forward_demodulation,[],[f7980,f41]) ).
fof(f7997,plain,
! [X0] : converse(converse(X0)) = join(X0,composition(converse(sk1),X0)),
inference(forward_demodulation,[],[f7979,f41]) ).
fof(f8025,plain,
! [X0] : join(X0,composition(converse(sk2),X0)) = X0,
inference(forward_demodulation,[],[f7996,f10]) ).
fof(f8026,plain,
! [X0] : join(X0,composition(converse(sk1),X0)) = X0,
inference(forward_demodulation,[],[f7997,f10]) ).
fof(f8064,plain,
! [X0] : composition(X0,one) = join(X0,composition(X0,composition(converse(sk1),one))),
inference(superposition,[],[f419,f8026]) ).
fof(f8113,plain,
! [X0] : composition(X0,one) = join(X0,composition(X0,converse(sk1))),
inference(forward_demodulation,[],[f8064,f8]) ).
fof(f8131,plain,
! [X0] : join(X0,composition(X0,converse(sk1))) = X0,
inference(forward_demodulation,[],[f8113,f8]) ).
fof(f8187,plain,
! [X0] : converse(converse(X0)) = join(X0,converse(composition(converse(X0),converse(sk1)))),
inference(superposition,[],[f34,f8131]) ).
fof(f8190,plain,
! [X0] : converse(converse(X0)) = join(X0,composition(converse(converse(sk1)),X0)),
inference(forward_demodulation,[],[f8187,f41]) ).
fof(f8224,plain,
! [X0] : converse(converse(X0)) = join(X0,composition(sk1,X0)),
inference(forward_demodulation,[],[f8190,f10]) ).
fof(f8243,plain,
! [X0] : join(X0,composition(sk1,X0)) = X0,
inference(forward_demodulation,[],[f8224,f10]) ).
fof(f8265,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(composition(sk1,X0),X1)),
inference(superposition,[],[f2,f8243]) ).
fof(f8273,plain,
! [X0] : complement(composition(sk1,X0)) = join(complement(X0),complement(join(complement(X0),composition(sk1,X0)))),
inference(superposition,[],[f2251,f8243]) ).
fof(f8285,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(complement(join(composition(sk1,complement(X0)),X0)),complement(complement(X0))),
inference(superposition,[],[f1230,f8243]) ).
fof(f8293,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(complement(complement(X0)),complement(join(X0,composition(sk1,complement(X0))))),
inference(forward_demodulation,[],[f8285,f6609]) ).
fof(f8304,plain,
! [X0] : complement(composition(sk1,X0)) = join(complement(X0),complement(composition(sk1,X0))),
inference(forward_demodulation,[],[f8273,f1252]) ).
fof(f8321,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(X0,complement(join(X0,composition(sk1,complement(X0))))),
inference(forward_demodulation,[],[f8293,f1190]) ).
fof(f8337,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(X0,complement(composition(sk1,complement(X0)))),
inference(forward_demodulation,[],[f8321,f1252]) ).
fof(f8643,plain,
! [X0,X1] : join(X0,composition(sk1,X1)) = join(X0,composition(sk1,join(X0,X1))),
inference(superposition,[],[f8265,f395]) ).
fof(f8843,plain,
! [X0] : join(X0,composition(sk1,complement(X0))) = join(X0,composition(sk1,top)),
inference(superposition,[],[f8643,f15]) ).
fof(f8845,plain,
! [X0,X1] : join(X0,composition(sk1,complement(join(X1,X0)))) = join(X0,composition(sk1,join(X0,complement(X1)))),
inference(superposition,[],[f8643,f1416]) ).
fof(f8996,plain,
! [X0,X1] : join(X0,composition(sk1,complement(join(X1,X0)))) = join(X0,composition(sk1,complement(X1))),
inference(forward_demodulation,[],[f8845,f8643]) ).
fof(f9061,plain,
! [X0] : composition(X0,one) = join(X0,composition(X0,composition(converse(sk2),one))),
inference(superposition,[],[f419,f8025]) ).
fof(f9114,plain,
! [X0] : composition(X0,one) = join(X0,composition(X0,converse(sk2))),
inference(forward_demodulation,[],[f9061,f8]) ).
fof(f9132,plain,
! [X0] : join(X0,composition(X0,converse(sk2))) = X0,
inference(forward_demodulation,[],[f9114,f8]) ).
fof(f9190,plain,
! [X0] : converse(converse(X0)) = join(X0,converse(composition(converse(X0),converse(sk2)))),
inference(superposition,[],[f34,f9132]) ).
fof(f9193,plain,
! [X0] : converse(converse(X0)) = join(X0,composition(converse(converse(sk2)),X0)),
inference(forward_demodulation,[],[f9190,f41]) ).
fof(f9229,plain,
! [X0] : converse(converse(X0)) = join(X0,composition(sk2,X0)),
inference(forward_demodulation,[],[f9193,f10]) ).
fof(f9249,plain,
! [X0] : join(X0,composition(sk2,X0)) = X0,
inference(forward_demodulation,[],[f9229,f10]) ).
fof(f9271,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(composition(sk2,X0),X1)),
inference(superposition,[],[f2,f9249]) ).
fof(f9272,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(composition(sk2,X0),X1)),
inference(superposition,[],[f78,f9249]) ).
fof(f9279,plain,
! [X0] : complement(composition(sk2,X0)) = join(complement(X0),complement(join(complement(X0),composition(sk2,X0)))),
inference(superposition,[],[f2251,f9249]) ).
fof(f9292,plain,
! [X0] : complement(composition(sk2,complement(X0))) = join(complement(join(composition(sk2,complement(X0)),X0)),complement(complement(X0))),
inference(superposition,[],[f1230,f9249]) ).
fof(f9302,plain,
! [X0] : complement(composition(sk2,complement(X0))) = join(complement(complement(X0)),complement(join(X0,composition(sk2,complement(X0))))),
inference(forward_demodulation,[],[f9292,f6609]) ).
fof(f9314,plain,
! [X0] : complement(composition(sk2,X0)) = join(complement(X0),complement(composition(sk2,X0))),
inference(forward_demodulation,[],[f9279,f1252]) ).
fof(f9331,plain,
! [X0] : complement(composition(sk2,complement(X0))) = join(X0,complement(join(X0,composition(sk2,complement(X0))))),
inference(forward_demodulation,[],[f9302,f1190]) ).
fof(f9347,plain,
! [X0] : complement(composition(sk2,complement(X0))) = join(X0,complement(composition(sk2,complement(X0)))),
inference(forward_demodulation,[],[f9331,f1252]) ).
fof(f9653,plain,
! [X0,X1] : join(X0,composition(sk2,X1)) = join(X0,composition(sk2,join(X0,X1))),
inference(superposition,[],[f9271,f395]) ).
fof(f9869,plain,
! [X0] : join(X0,composition(sk2,complement(X0))) = join(X0,composition(sk2,top)),
inference(superposition,[],[f9653,f15]) ).
fof(f9871,plain,
! [X0,X1] : join(X0,composition(sk2,complement(join(X1,X0)))) = join(X0,composition(sk2,join(X0,complement(X1)))),
inference(superposition,[],[f9653,f1416]) ).
fof(f10034,plain,
! [X0,X1] : join(X0,composition(sk2,complement(join(X1,X0)))) = join(X0,composition(sk2,complement(X1))),
inference(forward_demodulation,[],[f9871,f9653]) ).
fof(f10109,plain,
! [X0] : join(X0,complement(composition(sk1,complement(X0)))) = join(X0,complement(join(X0,composition(sk1,top)))),
inference(superposition,[],[f1252,f8843]) ).
fof(f10155,plain,
! [X0] : join(X0,complement(composition(sk1,complement(X0)))) = join(X0,complement(composition(sk1,top))),
inference(forward_demodulation,[],[f10109,f1252]) ).
fof(f10189,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(X0,complement(composition(sk1,top))),
inference(forward_demodulation,[],[f10155,f8337]) ).
fof(f10294,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(complement(composition(sk1,top)),X0),
inference(superposition,[],[f1,f10189]) ).
fof(f10322,plain,
! [X0] : join(X0,complement(join(complement(complement(composition(sk1,top))),X0))) = join(complement(composition(sk1,top)),complement(complement(composition(sk1,complement(complement(X0)))))),
inference(superposition,[],[f272,f10189]) ).
fof(f10331,plain,
! [X0,X1] : complement(composition(sk1,complement(join(X0,X1)))) = join(X0,join(X1,complement(composition(sk1,top)))),
inference(superposition,[],[f2,f10189]) ).
fof(f10332,plain,
! [X0,X1] : complement(composition(sk1,complement(join(X0,X1)))) = join(X0,complement(composition(sk1,complement(X1)))),
inference(forward_demodulation,[],[f10331,f10189]) ).
fof(f10340,plain,
! [X0] : join(X0,complement(join(complement(complement(composition(sk1,top))),X0))) = join(complement(composition(sk1,top)),composition(sk1,complement(complement(X0)))),
inference(forward_demodulation,[],[f10322,f1190]) ).
fof(f10390,plain,
! [X0] : join(X0,complement(join(complement(complement(composition(sk1,top))),X0))) = complement(composition(sk1,complement(composition(sk1,complement(complement(X0)))))),
inference(forward_demodulation,[],[f10340,f10294]) ).
fof(f10431,plain,
! [X0] : complement(composition(sk1,complement(composition(sk1,X0)))) = join(X0,complement(join(complement(complement(composition(sk1,top))),X0))),
inference(forward_demodulation,[],[f10390,f1190]) ).
fof(f10453,plain,
! [X0] : complement(composition(sk1,complement(composition(sk1,X0)))) = join(complement(composition(sk1,top)),X0),
inference(forward_demodulation,[],[f10431,f1099]) ).
fof(f10468,plain,
! [X0] : complement(composition(sk1,complement(X0))) = complement(composition(sk1,complement(composition(sk1,X0)))),
inference(forward_demodulation,[],[f10453,f10294]) ).
fof(f10495,plain,
! [X0,X1] : complement(composition(sk1,complement(join(X1,complement(X0))))) = join(X1,complement(composition(sk1,X0))),
inference(superposition,[],[f10332,f1190]) ).
fof(f10535,plain,
! [X0] : complement(composition(sk1,complement(X0))) = complement(composition(sk1,complement(join(complement(composition(sk1,complement(X0))),X0)))),
inference(superposition,[],[f1235,f10332]) ).
fof(f10541,plain,
! [X0,X1] : complement(composition(sk1,complement(join(X0,X1)))) = join(complement(composition(sk1,complement(X1))),X0),
inference(superposition,[],[f1,f10332]) ).
fof(f10552,plain,
! [X0,X1] : join(complement(X0),complement(composition(sk1,complement(X1)))) = join(complement(composition(sk1,complement(X1))),complement(complement(composition(sk1,complement(join(X0,X1)))))),
inference(superposition,[],[f2490,f10332]) ).
fof(f10576,plain,
! [X0,X1] : join(X0,complement(composition(sk1,complement(X1)))) = join(X0,complement(composition(sk1,complement(join(composition(sk2,X0),X1))))),
inference(superposition,[],[f9271,f10332]) ).
fof(f10580,plain,
! [X0,X1] : join(X0,complement(composition(sk1,complement(X1)))) = complement(composition(sk1,complement(join(X0,join(composition(sk2,X0),X1))))),
inference(forward_demodulation,[],[f10576,f10332]) ).
fof(f10602,plain,
! [X0,X1] : join(complement(X0),complement(composition(sk1,complement(X1)))) = join(complement(composition(sk1,complement(X1))),composition(sk1,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f10552,f1190]) ).
fof(f10613,plain,
! [X0] : complement(composition(sk1,complement(X0))) = complement(composition(sk1,complement(join(X0,complement(composition(sk1,complement(X0))))))),
inference(forward_demodulation,[],[f10535,f4148]) ).
fof(f10647,plain,
! [X0,X1] : complement(composition(sk1,complement(join(X1,X0)))) = join(X0,complement(composition(sk1,complement(X1)))),
inference(forward_demodulation,[],[f10580,f9272]) ).
fof(f10668,plain,
! [X0,X1] : join(complement(X0),complement(composition(sk1,complement(X1)))) = complement(composition(sk1,complement(join(composition(sk1,complement(join(X0,X1))),X1)))),
inference(forward_demodulation,[],[f10602,f10541]) ).
fof(f10679,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(X0,complement(composition(sk1,composition(sk1,complement(X0))))),
inference(forward_demodulation,[],[f10613,f10495]) ).
fof(f10714,plain,
! [X0,X1] : join(complement(X0),complement(composition(sk1,complement(X1)))) = complement(composition(sk1,complement(join(X1,composition(sk1,complement(join(X0,X1))))))),
inference(forward_demodulation,[],[f10668,f5895]) ).
fof(f10742,plain,
! [X0,X1] : join(complement(X0),complement(composition(sk1,complement(X1)))) = complement(composition(sk1,complement(join(X1,composition(sk1,complement(X0)))))),
inference(forward_demodulation,[],[f10714,f8996]) ).
fof(f10760,plain,
! [X0,X1] : complement(composition(sk1,complement(join(complement(X0),X1)))) = complement(composition(sk1,complement(join(X1,composition(sk1,complement(X0)))))),
inference(forward_demodulation,[],[f10742,f10332]) ).
fof(f10799,plain,
! [X0,X1] : complement(composition(sk1,complement(join(X0,complement(X1))))) = join(X0,complement(composition(sk1,join(X1,X0)))),
inference(superposition,[],[f10495,f1416]) ).
fof(f10815,plain,
! [X0] : join(X0,complement(composition(sk1,composition(sk1,complement(X0))))) = complement(composition(sk1,complement(complement(composition(sk1,complement(X0)))))),
inference(superposition,[],[f10495,f8337]) ).
fof(f10837,plain,
! [X0] : join(complement(X0),complement(composition(sk1,composition(sk2,X0)))) = complement(composition(sk1,complement(complement(composition(sk2,X0))))),
inference(superposition,[],[f10495,f9314]) ).
fof(f10847,plain,
! [X0,X1] : complement(composition(sk1,complement(join(complement(X0),X1)))) = join(X1,complement(composition(sk1,X0))),
inference(superposition,[],[f10495,f5895]) ).
fof(f10897,plain,
! [X2,X0,X1] : complement(composition(sk1,complement(join(X2,composition(sk1,complement(join(X0,complement(X1)))))))) = join(X2,complement(composition(sk1,join(X0,complement(composition(sk1,X1)))))),
inference(superposition,[],[f10332,f10495]) ).
fof(f10898,plain,
! [X2,X0,X1] : join(X2,complement(composition(sk1,join(X0,complement(composition(sk1,X1)))))) = complement(composition(sk1,complement(join(complement(join(X0,complement(X1))),X2)))),
inference(forward_demodulation,[],[f10897,f10760]) ).
fof(f10941,plain,
! [X0] : complement(composition(sk1,composition(sk2,X0))) = join(complement(X0),complement(composition(sk1,composition(sk2,X0)))),
inference(forward_demodulation,[],[f10837,f1190]) ).
fof(f10956,plain,
! [X0] : complement(composition(sk1,composition(sk1,complement(X0)))) = join(X0,complement(composition(sk1,composition(sk1,complement(X0))))),
inference(forward_demodulation,[],[f10815,f1190]) ).
fof(f10967,plain,
! [X0,X1] : join(X0,complement(composition(sk1,X1))) = join(X0,complement(composition(sk1,join(X1,X0)))),
inference(forward_demodulation,[],[f10799,f10495]) ).
fof(f10977,plain,
! [X2,X0,X1] : join(X2,complement(composition(sk1,join(X0,complement(composition(sk1,X1)))))) = join(X2,complement(composition(sk1,join(X0,complement(X1))))),
inference(forward_demodulation,[],[f10898,f10847]) ).
fof(f11015,plain,
! [X0] : complement(composition(sk1,complement(X0))) = complement(composition(sk1,composition(sk1,complement(X0)))),
inference(forward_demodulation,[],[f10956,f10679]) ).
fof(f11150,plain,
! [X0,X1] : join(complement(X1),complement(composition(sk1,X0))) = join(complement(X0),complement(composition(sk1,X1))),
inference(superposition,[],[f10495,f10847]) ).
fof(f11507,plain,
! [X0] : join(complement(one),complement(composition(sk1,X0))) = join(complement(X0),complement(sk1)),
inference(superposition,[],[f11150,f8]) ).
fof(f11605,plain,
! [X0,X1] : join(complement(composition(sk1,X0)),complement(X1)) = join(complement(X0),complement(composition(sk1,X1))),
inference(superposition,[],[f1,f11150]) ).
fof(f12226,plain,
! [X0] : join(X0,complement(composition(sk2,complement(X0)))) = join(X0,complement(join(X0,composition(sk2,top)))),
inference(superposition,[],[f1252,f9869]) ).
fof(f12274,plain,
! [X0] : join(X0,complement(composition(sk2,complement(X0)))) = join(X0,complement(composition(sk2,top))),
inference(forward_demodulation,[],[f12226,f1252]) ).
fof(f12310,plain,
! [X0] : complement(composition(sk2,complement(X0))) = join(X0,complement(composition(sk2,top))),
inference(forward_demodulation,[],[f12274,f9347]) ).
fof(f12418,plain,
! [X0] : complement(composition(sk2,complement(X0))) = join(complement(composition(sk2,top)),X0),
inference(superposition,[],[f1,f12310]) ).
fof(f12446,plain,
! [X0] : join(X0,complement(join(complement(complement(composition(sk2,top))),X0))) = join(complement(composition(sk2,top)),complement(complement(composition(sk2,complement(complement(X0)))))),
inference(superposition,[],[f272,f12310]) ).
fof(f12452,plain,
! [X0] : complement(composition(sk1,complement(complement(composition(sk2,complement(complement(X0))))))) = join(complement(composition(sk2,top)),complement(composition(sk1,X0))),
inference(superposition,[],[f10847,f12310]) ).
fof(f12456,plain,
! [X0,X1] : complement(composition(sk2,complement(join(X0,X1)))) = join(X0,join(X1,complement(composition(sk2,top)))),
inference(superposition,[],[f2,f12310]) ).
fof(f12457,plain,
! [X0,X1] : complement(composition(sk2,complement(join(X0,X1)))) = join(X0,complement(composition(sk2,complement(X1)))),
inference(forward_demodulation,[],[f12456,f12310]) ).
fof(f12460,plain,
! [X0] : complement(composition(sk1,composition(sk2,complement(complement(X0))))) = join(complement(composition(sk2,top)),complement(composition(sk1,X0))),
inference(forward_demodulation,[],[f12452,f1190]) ).
fof(f12466,plain,
! [X0] : join(X0,complement(join(complement(complement(composition(sk2,top))),X0))) = join(complement(composition(sk2,top)),composition(sk2,complement(complement(X0)))),
inference(forward_demodulation,[],[f12446,f1190]) ).
fof(f12512,plain,
! [X0] : complement(composition(sk1,composition(sk2,complement(complement(X0))))) = complement(composition(sk2,complement(complement(composition(sk1,X0))))),
inference(forward_demodulation,[],[f12460,f12418]) ).
fof(f12518,plain,
! [X0] : join(X0,complement(join(complement(complement(composition(sk2,top))),X0))) = complement(composition(sk2,complement(composition(sk2,complement(complement(X0)))))),
inference(forward_demodulation,[],[f12466,f12418]) ).
fof(f12556,plain,
! [X0] : complement(composition(sk1,composition(sk2,complement(complement(X0))))) = complement(composition(sk2,composition(sk1,X0))),
inference(forward_demodulation,[],[f12512,f1190]) ).
fof(f12560,plain,
! [X0] : complement(composition(sk2,complement(composition(sk2,X0)))) = join(X0,complement(join(complement(complement(composition(sk2,top))),X0))),
inference(forward_demodulation,[],[f12518,f1190]) ).
fof(f12580,plain,
! [X0] : complement(composition(sk1,composition(sk2,X0))) = complement(composition(sk2,composition(sk1,X0))),
inference(forward_demodulation,[],[f12556,f1190]) ).
fof(f12583,plain,
! [X0] : complement(composition(sk2,complement(composition(sk2,X0)))) = join(complement(composition(sk2,top)),X0),
inference(forward_demodulation,[],[f12560,f1099]) ).
fof(f12598,plain,
! [X0] : complement(composition(sk2,complement(X0))) = complement(composition(sk2,complement(composition(sk2,X0)))),
inference(forward_demodulation,[],[f12583,f12418]) ).
fof(f12630,plain,
! [X0,X1] : complement(composition(sk2,complement(join(X1,complement(X0))))) = join(X1,complement(composition(sk2,X0))),
inference(superposition,[],[f12457,f1190]) ).
fof(f12668,plain,
! [X0] : complement(composition(sk2,complement(X0))) = complement(composition(sk2,complement(join(complement(composition(sk2,complement(X0))),X0)))),
inference(superposition,[],[f1235,f12457]) ).
fof(f12674,plain,
! [X0,X1] : complement(composition(sk2,complement(join(X0,X1)))) = join(complement(composition(sk2,complement(X1))),X0),
inference(superposition,[],[f1,f12457]) ).
fof(f12685,plain,
! [X0,X1] : join(complement(X0),complement(composition(sk2,complement(X1)))) = join(complement(composition(sk2,complement(X1))),complement(complement(composition(sk2,complement(join(X0,X1)))))),
inference(superposition,[],[f2490,f12457]) ).
fof(f12710,plain,
! [X0,X1] : join(X0,complement(composition(sk2,complement(X1)))) = join(X0,complement(composition(sk2,complement(join(composition(sk2,X0),X1))))),
inference(superposition,[],[f9271,f12457]) ).
fof(f12714,plain,
! [X0,X1] : join(X0,complement(composition(sk2,complement(X1)))) = complement(composition(sk2,complement(join(X0,join(composition(sk2,X0),X1))))),
inference(forward_demodulation,[],[f12710,f12457]) ).
fof(f12737,plain,
! [X0,X1] : join(complement(X0),complement(composition(sk2,complement(X1)))) = join(complement(composition(sk2,complement(X1))),composition(sk2,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f12685,f1190]) ).
fof(f12748,plain,
! [X0] : complement(composition(sk2,complement(X0))) = complement(composition(sk2,complement(join(X0,complement(composition(sk2,complement(X0))))))),
inference(forward_demodulation,[],[f12668,f4148]) ).
fof(f12784,plain,
! [X0,X1] : complement(composition(sk2,complement(join(X1,X0)))) = join(X0,complement(composition(sk2,complement(X1)))),
inference(forward_demodulation,[],[f12714,f9272]) ).
fof(f12806,plain,
! [X0,X1] : join(complement(X0),complement(composition(sk2,complement(X1)))) = complement(composition(sk2,complement(join(composition(sk2,complement(join(X0,X1))),X1)))),
inference(forward_demodulation,[],[f12737,f12674]) ).
fof(f12817,plain,
! [X0] : complement(composition(sk2,complement(X0))) = join(X0,complement(composition(sk2,composition(sk2,complement(X0))))),
inference(forward_demodulation,[],[f12748,f12630]) ).
fof(f12851,plain,
! [X0,X1] : join(complement(X0),complement(composition(sk2,complement(X1)))) = complement(composition(sk2,complement(join(X1,composition(sk2,complement(join(X0,X1))))))),
inference(forward_demodulation,[],[f12806,f5895]) ).
fof(f12879,plain,
! [X0,X1] : join(complement(X0),complement(composition(sk2,complement(X1)))) = complement(composition(sk2,complement(join(X1,composition(sk2,complement(X0)))))),
inference(forward_demodulation,[],[f12851,f10034]) ).
fof(f12897,plain,
! [X0,X1] : complement(composition(sk2,complement(join(complement(X0),X1)))) = complement(composition(sk2,complement(join(X1,composition(sk2,complement(X0)))))),
inference(forward_demodulation,[],[f12879,f12457]) ).
fof(f12938,plain,
! [X0,X1] : complement(composition(sk2,complement(join(X0,complement(X1))))) = join(X0,complement(composition(sk2,join(X1,X0)))),
inference(superposition,[],[f12630,f1416]) ).
fof(f12958,plain,
! [X0] : join(X0,complement(composition(sk2,composition(sk2,complement(X0))))) = complement(composition(sk2,complement(complement(composition(sk2,complement(X0)))))),
inference(superposition,[],[f12630,f9347]) ).
fof(f12991,plain,
! [X0,X1] : complement(composition(sk2,complement(join(complement(X0),X1)))) = join(X1,complement(composition(sk2,X0))),
inference(superposition,[],[f12630,f5895]) ).
fof(f13048,plain,
! [X2,X0,X1] : complement(composition(sk2,complement(join(X2,composition(sk2,complement(join(X0,complement(X1)))))))) = join(X2,complement(composition(sk2,join(X0,complement(composition(sk2,X1)))))),
inference(superposition,[],[f12457,f12630]) ).
fof(f13049,plain,
! [X2,X0,X1] : join(X2,complement(composition(sk2,join(X0,complement(composition(sk2,X1)))))) = complement(composition(sk2,complement(join(complement(join(X0,complement(X1))),X2)))),
inference(forward_demodulation,[],[f13048,f12897]) ).
fof(f13113,plain,
! [X0] : complement(composition(sk2,composition(sk2,complement(X0)))) = join(X0,complement(composition(sk2,composition(sk2,complement(X0))))),
inference(forward_demodulation,[],[f12958,f1190]) ).
fof(f13128,plain,
! [X0,X1] : join(X0,complement(composition(sk2,X1))) = join(X0,complement(composition(sk2,join(X1,X0)))),
inference(forward_demodulation,[],[f12938,f12630]) ).
fof(f13140,plain,
! [X2,X0,X1] : join(X2,complement(composition(sk2,join(X0,complement(composition(sk2,X1)))))) = join(X2,complement(composition(sk2,join(X0,complement(X1))))),
inference(forward_demodulation,[],[f13049,f12991]) ).
fof(f13186,plain,
! [X0] : complement(composition(sk2,complement(X0))) = complement(composition(sk2,composition(sk2,complement(X0)))),
inference(forward_demodulation,[],[f13113,f12817]) ).
fof(f13311,plain,
! [X0,X1] : complement(composition(sk2,complement(join(complement(X0),complement(X1))))) = join(complement(join(complement(X0),X1)),complement(composition(sk2,X0))),
inference(superposition,[],[f12991,f1252]) ).
fof(f13353,plain,
! [X0,X1] : join(complement(X1),complement(composition(sk2,X0))) = join(complement(X0),complement(composition(sk2,X1))),
inference(superposition,[],[f12630,f12991]) ).
fof(f13492,plain,
! [X0,X1] : complement(composition(sk2,complement(join(complement(X0),complement(X1))))) = join(complement(composition(sk2,X0)),complement(join(X1,complement(X0)))),
inference(forward_demodulation,[],[f13311,f6609]) ).
fof(f13599,plain,
! [X0,X1] : join(complement(X0),complement(composition(sk2,X1))) = join(complement(composition(sk2,X0)),complement(join(X1,complement(X0)))),
inference(forward_demodulation,[],[f13492,f12630]) ).
fof(f13778,plain,
! [X0] : join(complement(one),complement(composition(sk2,X0))) = join(complement(X0),complement(sk2)),
inference(superposition,[],[f13353,f8]) ).
fof(f13882,plain,
! [X0,X1] : join(complement(composition(sk2,X0)),complement(X1)) = join(complement(X0),complement(composition(sk2,X1))),
inference(superposition,[],[f1,f13353]) ).
fof(f14586,plain,
! [X0] : complement(complement(composition(sk1,complement(X0)))) = composition(sk1,composition(sk1,complement(X0))),
inference(superposition,[],[f1190,f11015]) ).
fof(f14605,plain,
! [X0,X1] : join(X1,complement(composition(sk1,complement(composition(sk1,complement(X0)))))) = complement(composition(sk1,complement(join(composition(sk1,composition(sk1,complement(X0))),X1)))),
inference(superposition,[],[f10647,f11015]) ).
fof(f14624,plain,
! [X0,X1] : complement(composition(sk1,complement(join(X1,composition(sk1,complement(X0)))))) = complement(composition(sk1,complement(join(composition(sk1,composition(sk1,complement(X0))),X1)))),
inference(forward_demodulation,[],[f14605,f10332]) ).
fof(f14638,plain,
! [X0] : composition(sk1,complement(X0)) = composition(sk1,composition(sk1,complement(X0))),
inference(forward_demodulation,[],[f14586,f1190]) ).
fof(f14670,plain,
! [X0,X1] : complement(composition(sk1,complement(join(complement(X0),X1)))) = complement(composition(sk1,complement(join(composition(sk1,composition(sk1,complement(X0))),X1)))),
inference(forward_demodulation,[],[f14624,f10760]) ).
fof(f14708,plain,
! [X0,X1] : complement(composition(sk1,complement(join(complement(X0),X1)))) = complement(composition(sk1,complement(join(composition(sk1,complement(X0)),X1)))),
inference(forward_demodulation,[],[f14670,f14638]) ).
fof(f14740,plain,
! [X0,X1] : join(X1,complement(composition(sk1,X0))) = complement(composition(sk1,complement(join(composition(sk1,complement(X0)),X1)))),
inference(forward_demodulation,[],[f14708,f10847]) ).
fof(f14799,plain,
! [X0,X1] : join(composition(sk1,X1),complement(composition(sk1,X0))) = complement(composition(sk1,complement(composition(sk1,join(complement(X0),X1))))),
inference(superposition,[],[f14740,f395]) ).
fof(f14856,plain,
! [X0,X1] : join(complement(X0),complement(composition(sk1,X1))) = join(composition(sk1,complement(X1)),complement(composition(sk1,X0))),
inference(superposition,[],[f10495,f14740]) ).
fof(f15030,plain,
! [X0,X1] : complement(composition(sk1,complement(join(complement(X0),X1)))) = join(composition(sk1,X1),complement(composition(sk1,X0))),
inference(forward_demodulation,[],[f14799,f10468]) ).
fof(f15136,plain,
! [X0,X1] : join(X1,complement(composition(sk1,X0))) = join(composition(sk1,X1),complement(composition(sk1,X0))),
inference(forward_demodulation,[],[f15030,f10847]) ).
fof(f15359,plain,
! [X0] : join(one,complement(composition(sk1,X0))) = join(sk1,complement(composition(sk1,X0))),
inference(superposition,[],[f15136,f8]) ).
fof(f15409,plain,
! [X2,X0,X1] : join(X2,complement(join(X0,complement(composition(sk1,X1))))) = join(X2,complement(join(complement(composition(sk1,X1)),composition(sk1,X0)))),
inference(superposition,[],[f6453,f15136]) ).
fof(f15689,plain,
! [X2,X0,X1] : join(X2,complement(join(complement(X0),complement(composition(sk1,X1))))) = join(X2,complement(join(complement(composition(sk1,X0)),composition(sk1,complement(X1))))),
inference(superposition,[],[f6453,f14856]) ).
fof(f15693,plain,
! [X2,X0,X1] : join(X2,complement(join(complement(X1),complement(composition(sk1,X0))))) = join(X2,complement(join(complement(X0),complement(composition(sk1,X1))))),
inference(forward_demodulation,[],[f15689,f15409]) ).
fof(f15896,plain,
! [X0] : complement(complement(composition(sk2,complement(X0)))) = composition(sk2,composition(sk2,complement(X0))),
inference(superposition,[],[f1190,f13186]) ).
fof(f15922,plain,
! [X0,X1] : join(X1,complement(composition(sk2,complement(composition(sk2,complement(X0)))))) = complement(composition(sk2,complement(join(composition(sk2,composition(sk2,complement(X0))),X1)))),
inference(superposition,[],[f12784,f13186]) ).
fof(f15933,plain,
! [X0,X1] : complement(composition(sk2,complement(join(X1,composition(sk2,complement(X0)))))) = complement(composition(sk2,complement(join(composition(sk2,composition(sk2,complement(X0))),X1)))),
inference(forward_demodulation,[],[f15922,f12457]) ).
fof(f15952,plain,
! [X0] : composition(sk2,complement(X0)) = composition(sk2,composition(sk2,complement(X0))),
inference(forward_demodulation,[],[f15896,f1190]) ).
fof(f15982,plain,
! [X0,X1] : complement(composition(sk2,complement(join(complement(X0),X1)))) = complement(composition(sk2,complement(join(composition(sk2,composition(sk2,complement(X0))),X1)))),
inference(forward_demodulation,[],[f15933,f12897]) ).
fof(f16021,plain,
! [X0,X1] : complement(composition(sk2,complement(join(complement(X0),X1)))) = complement(composition(sk2,complement(join(composition(sk2,complement(X0)),X1)))),
inference(forward_demodulation,[],[f15982,f15952]) ).
fof(f16055,plain,
! [X0,X1] : join(X1,complement(composition(sk2,X0))) = complement(composition(sk2,complement(join(composition(sk2,complement(X0)),X1)))),
inference(forward_demodulation,[],[f16021,f12991]) ).
fof(f16112,plain,
! [X0,X1] : join(composition(sk2,X1),complement(composition(sk2,X0))) = complement(composition(sk2,complement(composition(sk2,join(complement(X0),X1))))),
inference(superposition,[],[f16055,f395]) ).
fof(f16169,plain,
! [X0,X1] : join(complement(X0),complement(composition(sk2,X1))) = join(composition(sk2,complement(X1)),complement(composition(sk2,X0))),
inference(superposition,[],[f12630,f16055]) ).
fof(f16348,plain,
! [X0,X1] : complement(composition(sk2,complement(join(complement(X0),X1)))) = join(composition(sk2,X1),complement(composition(sk2,X0))),
inference(forward_demodulation,[],[f16112,f12598]) ).
fof(f16458,plain,
! [X0,X1] : join(X1,complement(composition(sk2,X0))) = join(composition(sk2,X1),complement(composition(sk2,X0))),
inference(forward_demodulation,[],[f16348,f12991]) ).
fof(f16695,plain,
! [X0] : join(one,complement(composition(sk2,X0))) = join(sk2,complement(composition(sk2,X0))),
inference(superposition,[],[f16458,f8]) ).
fof(f16741,plain,
! [X0,X1] : complement(join(X0,complement(composition(sk2,X1)))) = complement(join(complement(composition(sk2,X1)),composition(sk2,X0))),
inference(superposition,[],[f5895,f16458]) ).
fof(f16745,plain,
! [X2,X0,X1] : join(X2,complement(join(X0,complement(composition(sk2,X1))))) = join(X2,complement(join(complement(composition(sk2,X1)),composition(sk2,X0)))),
inference(superposition,[],[f6453,f16458]) ).
fof(f17019,plain,
! [X0,X1] : complement(join(complement(X0),complement(composition(sk2,X1)))) = complement(join(complement(composition(sk2,X0)),composition(sk2,complement(X1)))),
inference(superposition,[],[f5895,f16169]) ).
fof(f17023,plain,
! [X2,X0,X1] : join(X2,complement(join(complement(X0),complement(composition(sk2,X1))))) = join(X2,complement(join(complement(composition(sk2,X0)),composition(sk2,complement(X1))))),
inference(superposition,[],[f6453,f16169]) ).
fof(f17027,plain,
! [X2,X0,X1] : join(X2,complement(join(complement(X1),complement(composition(sk2,X0))))) = join(X2,complement(join(complement(X0),complement(composition(sk2,X1))))),
inference(forward_demodulation,[],[f17023,f16745]) ).
fof(f17031,plain,
! [X0,X1] : complement(join(complement(X1),complement(composition(sk2,X0)))) = complement(join(complement(X0),complement(composition(sk2,X1)))),
inference(forward_demodulation,[],[f17019,f16741]) ).
fof(f18126,plain,
! [X0,X1] : join(complement(join(X1,complement(X0))),complement(join(complement(X0),complement(composition(sk2,X1))))) = join(complement(complement(composition(sk2,X0))),complement(join(X1,complement(X0)))),
inference(superposition,[],[f2490,f13599]) ).
fof(f18133,plain,
! [X0,X1] : join(composition(sk2,X0),complement(join(X1,complement(X0)))) = join(complement(join(X1,complement(X0))),complement(join(complement(X0),complement(composition(sk2,X1))))),
inference(forward_demodulation,[],[f18126,f1190]) ).
fof(f20656,plain,
! [X0] : join(complement(one),complement(composition(sk2,X0))) = join(complement(composition(sk2,X0)),complement(join(sk2,complement(composition(sk2,X0))))),
inference(superposition,[],[f2490,f16695]) ).
fof(f20661,plain,
! [X0] : join(complement(one),complement(composition(sk2,X0))) = join(complement(X0),complement(composition(sk2,join(sk2,complement(composition(sk2,X0)))))),
inference(forward_demodulation,[],[f20656,f13882]) ).
fof(f20687,plain,
! [X0] : join(complement(one),complement(composition(sk2,X0))) = join(complement(X0),complement(composition(sk2,join(sk2,complement(X0))))),
inference(forward_demodulation,[],[f20661,f13140]) ).
fof(f20698,plain,
! [X0] : join(complement(one),complement(composition(sk2,X0))) = join(complement(X0),complement(composition(sk2,sk2))),
inference(forward_demodulation,[],[f20687,f13128]) ).
fof(f20708,plain,
! [X0] : join(complement(X0),complement(sk2)) = join(complement(X0),complement(composition(sk2,sk2))),
inference(forward_demodulation,[],[f20698,f13778]) ).
fof(f20727,plain,
! [X0] : join(X0,complement(sk2)) = join(X0,complement(composition(sk2,sk2))),
inference(superposition,[],[f20708,f1190]) ).
fof(f20752,plain,
! [X0] : composition(sk2,sk2) = join(complement(join(complement(composition(sk2,sk2)),X0)),complement(join(complement(X0),complement(sk2)))),
inference(superposition,[],[f202,f20708]) ).
fof(f20790,plain,
! [X0] : join(complement(X0),complement(complement(composition(sk2,sk2)))) = join(complement(X0),complement(join(complement(X0),complement(sk2)))),
inference(superposition,[],[f1252,f20708]) ).
fof(f20818,plain,
! [X0] : join(complement(X0),complement(complement(composition(sk2,sk2)))) = join(complement(X0),complement(complement(sk2))),
inference(forward_demodulation,[],[f20790,f1252]) ).
fof(f20849,plain,
! [X0] : composition(sk2,sk2) = join(complement(join(complement(X0),complement(sk2))),complement(join(X0,complement(composition(sk2,sk2))))),
inference(forward_demodulation,[],[f20752,f6609]) ).
fof(f20870,plain,
! [X0] : join(complement(X0),complement(complement(composition(sk2,sk2)))) = join(complement(X0),sk2),
inference(forward_demodulation,[],[f20818,f1190]) ).
fof(f20890,plain,
! [X0] : composition(sk2,sk2) = join(complement(join(complement(X0),complement(sk2))),complement(join(X0,complement(sk2)))),
inference(forward_demodulation,[],[f20849,f20727]) ).
fof(f20900,plain,
! [X0] : join(sk2,complement(X0)) = join(complement(X0),complement(complement(composition(sk2,sk2)))),
inference(forward_demodulation,[],[f20870,f1]) ).
fof(f20916,plain,
! [X0] : composition(sk2,sk2) = join(complement(join(X0,complement(sk2))),complement(join(complement(sk2),complement(X0)))),
inference(forward_demodulation,[],[f20890,f6609]) ).
fof(f20924,plain,
! [X0] : join(sk2,complement(X0)) = join(complement(X0),composition(sk2,sk2)),
inference(forward_demodulation,[],[f20900,f1190]) ).
fof(f20935,plain,
sk2 = composition(sk2,sk2),
inference(forward_demodulation,[],[f20916,f199]) ).
fof(f21252,plain,
! [X0] : join(complement(sk2),complement(composition(sk2,X0))) = join(complement(sk2),complement(join(X0,complement(sk2)))),
inference(superposition,[],[f13599,f20935]) ).
fof(f21277,plain,
! [X0] : join(complement(sk2),complement(composition(sk2,X0))) = join(complement(sk2),complement(X0)),
inference(forward_demodulation,[],[f21252,f1416]) ).
fof(f22387,plain,
! [X0] : join(complement(join(sk2,complement(X0))),complement(join(complement(X0),complement(composition(sk2,sk2))))) = X0,
inference(superposition,[],[f193,f20924]) ).
fof(f22448,plain,
! [X0] : join(composition(sk2,X0),complement(join(sk2,complement(X0)))) = X0,
inference(forward_demodulation,[],[f22387,f18133]) ).
fof(f22548,plain,
! [X0] : complement(composition(sk2,X0)) = join(complement(join(join(sk2,complement(X0)),composition(sk2,X0))),complement(X0)),
inference(superposition,[],[f1228,f22448]) ).
fof(f22587,plain,
! [X0] : complement(composition(sk2,X0)) = join(complement(X0),complement(join(composition(sk2,X0),join(sk2,complement(X0))))),
inference(forward_demodulation,[],[f22548,f6609]) ).
fof(f22644,plain,
! [X0] : complement(composition(sk2,X0)) = join(complement(X0),complement(join(sk2,join(complement(X0),composition(sk2,X0))))),
inference(forward_demodulation,[],[f22587,f6463]) ).
fof(f22693,plain,
! [X0] : complement(composition(sk2,X0)) = join(complement(X0),complement(join(composition(sk2,X0),sk2))),
inference(forward_demodulation,[],[f22644,f1418]) ).
fof(f22730,plain,
! [X0] : complement(composition(sk2,X0)) = join(complement(X0),complement(join(sk2,composition(sk2,X0)))),
inference(forward_demodulation,[],[f22693,f6411]) ).
fof(f22808,plain,
join(complement(sk1),complement(sk2)) = complement(composition(sk2,sk1)),
inference(superposition,[],[f22730,f546]) ).
fof(f23601,plain,
join(complement(sk1),complement(composition(sk1,sk2))) = complement(composition(sk1,complement(complement(composition(sk2,sk1))))),
inference(superposition,[],[f10495,f22808]) ).
fof(f23664,plain,
join(complement(sk1),complement(composition(sk1,sk2))) = complement(composition(sk1,composition(sk2,sk1))),
inference(forward_demodulation,[],[f23601,f1190]) ).
fof(f23704,plain,
complement(composition(sk1,sk2)) = complement(composition(sk1,composition(sk2,sk1))),
inference(forward_demodulation,[],[f23664,f2009]) ).
fof(f23841,plain,
! [X0] : join(complement(one),complement(composition(sk1,X0))) = join(complement(composition(sk1,X0)),complement(join(sk1,complement(composition(sk1,X0))))),
inference(superposition,[],[f2490,f15359]) ).
fof(f23846,plain,
! [X0] : join(complement(one),complement(composition(sk1,X0))) = join(complement(X0),complement(composition(sk1,join(sk1,complement(composition(sk1,X0)))))),
inference(forward_demodulation,[],[f23841,f11605]) ).
fof(f23872,plain,
! [X0] : join(complement(one),complement(composition(sk1,X0))) = join(complement(X0),complement(composition(sk1,join(sk1,complement(X0))))),
inference(forward_demodulation,[],[f23846,f10977]) ).
fof(f23883,plain,
! [X0] : join(complement(one),complement(composition(sk1,X0))) = join(complement(X0),complement(composition(sk1,sk1))),
inference(forward_demodulation,[],[f23872,f10967]) ).
fof(f23893,plain,
! [X0] : join(complement(X0),complement(sk1)) = join(complement(X0),complement(composition(sk1,sk1))),
inference(forward_demodulation,[],[f23883,f11507]) ).
fof(f23947,plain,
! [X0] : join(complement(X0),complement(composition(sk2,composition(sk1,sk1)))) = complement(composition(sk2,complement(join(complement(X0),complement(sk1))))),
inference(superposition,[],[f12630,f23893]) ).
fof(f24025,plain,
! [X0] : join(complement(X0),complement(composition(sk2,composition(sk1,sk1)))) = join(complement(X0),complement(composition(sk2,sk1))),
inference(forward_demodulation,[],[f23947,f12630]) ).
fof(f24068,plain,
! [X0] : join(complement(X0),complement(composition(sk1,composition(sk2,sk1)))) = join(complement(X0),complement(composition(sk2,sk1))),
inference(forward_demodulation,[],[f24025,f12580]) ).
fof(f24097,plain,
! [X0] : join(complement(X0),complement(composition(sk1,sk2))) = join(complement(X0),complement(composition(sk2,sk1))),
inference(forward_demodulation,[],[f24068,f23704]) ).
fof(f24197,plain,
join(complement(sk2),complement(sk1)) = join(complement(sk2),complement(composition(sk1,sk2))),
inference(superposition,[],[f21277,f24097]) ).
fof(f24291,plain,
join(complement(sk2),complement(sk1)) = complement(composition(sk1,sk2)),
inference(forward_demodulation,[],[f24197,f8304]) ).
fof(f24336,plain,
join(complement(sk1),complement(sk2)) = complement(composition(sk1,sk2)),
inference(forward_demodulation,[],[f24291,f1]) ).
fof(f26895,plain,
( complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) != join(composition(complement(complement(composition(sk1,sk2))),sk3),complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))))
| composition(complement(complement(composition(sk1,sk2))),sk3) != join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(complement(composition(sk1,sk2))),sk3)) ),
inference(superposition,[],[f33,f24336]) ).
fof(f26984,plain,
( complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) != join(composition(complement(complement(composition(sk1,sk2))),sk3),complement(join(complement(sk3),complement(composition(sk2,composition(sk1,sk3))))))
| composition(complement(complement(composition(sk1,sk2))),sk3) != join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(complement(composition(sk1,sk2))),sk3)) ),
inference(forward_demodulation,[],[f26895,f17027]) ).
fof(f27021,plain,
( complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) != join(composition(complement(complement(composition(sk1,sk2))),sk3),complement(join(complement(sk3),complement(composition(sk1,composition(sk2,sk3))))))
| composition(complement(complement(composition(sk1,sk2))),sk3) != join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(complement(composition(sk1,sk2))),sk3)) ),
inference(forward_demodulation,[],[f26984,f12580]) ).
fof(f27052,plain,
( complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) != join(composition(complement(complement(composition(sk1,sk2))),sk3),complement(complement(composition(sk1,composition(sk2,sk3)))))
| composition(complement(complement(composition(sk1,sk2))),sk3) != join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(complement(composition(sk1,sk2))),sk3)) ),
inference(forward_demodulation,[],[f27021,f10941]) ).
fof(f27072,plain,
( complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) != join(complement(complement(composition(sk1,composition(sk2,sk3)))),composition(complement(complement(composition(sk1,sk2))),sk3))
| composition(complement(complement(composition(sk1,sk2))),sk3) != join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(complement(composition(sk1,sk2))),sk3)) ),
inference(forward_demodulation,[],[f27052,f1]) ).
fof(f27083,plain,
( complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) != join(complement(complement(composition(sk1,composition(sk2,sk3)))),composition(composition(sk1,sk2),sk3))
| composition(complement(complement(composition(sk1,sk2))),sk3) != join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(complement(composition(sk1,sk2))),sk3)) ),
inference(forward_demodulation,[],[f27072,f1190]) ).
fof(f27091,plain,
( complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) != join(composition(composition(sk1,sk2),sk3),complement(complement(composition(sk1,composition(sk2,sk3)))))
| composition(complement(complement(composition(sk1,sk2))),sk3) != join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(complement(composition(sk1,sk2))),sk3)) ),
inference(forward_demodulation,[],[f27083,f1]) ).
fof(f27097,plain,
( complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) != join(composition(composition(sk1,sk2),sk3),composition(sk1,composition(sk2,sk3)))
| composition(complement(complement(composition(sk1,sk2))),sk3) != join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(complement(composition(sk1,sk2))),sk3)) ),
inference(forward_demodulation,[],[f27091,f1190]) ).
fof(f27103,plain,
( complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) != composition(join(composition(sk1,sk2),composition(sk1,sk2)),sk3)
| composition(complement(complement(composition(sk1,sk2))),sk3) != join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(complement(composition(sk1,sk2))),sk3)) ),
inference(forward_demodulation,[],[f27097,f664]) ).
fof(f27106,plain,
( complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) != composition(composition(sk1,sk2),join(sk3,sk3))
| composition(complement(complement(composition(sk1,sk2))),sk3) != join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(complement(composition(sk1,sk2))),sk3)) ),
inference(forward_demodulation,[],[f27103,f429]) ).
fof(f27108,plain,
( complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) != composition(sk1,composition(sk2,join(sk3,sk3)))
| composition(complement(complement(composition(sk1,sk2))),sk3) != join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(complement(composition(sk1,sk2))),sk3)) ),
inference(forward_demodulation,[],[f27106,f7]) ).
fof(f27109,plain,
( complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) != composition(sk1,composition(sk2,sk3))
| composition(complement(complement(composition(sk1,sk2))),sk3) != join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(complement(composition(sk1,sk2))),sk3)) ),
inference(forward_demodulation,[],[f27108,f1235]) ).
fof(f27110,plain,
( complement(join(complement(sk3),complement(composition(sk2,composition(sk1,sk3))))) != composition(sk1,composition(sk2,sk3))
| composition(complement(complement(composition(sk1,sk2))),sk3) != join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(complement(composition(sk1,sk2))),sk3)) ),
inference(forward_demodulation,[],[f27109,f17031]) ).
fof(f27111,plain,
( composition(sk1,composition(sk2,sk3)) != complement(join(complement(sk3),complement(composition(sk1,composition(sk2,sk3)))))
| composition(complement(complement(composition(sk1,sk2))),sk3) != join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(complement(composition(sk1,sk2))),sk3)) ),
inference(forward_demodulation,[],[f27110,f12580]) ).
fof(f27112,plain,
( composition(sk1,composition(sk2,sk3)) != complement(complement(composition(sk1,composition(sk2,sk3))))
| composition(complement(complement(composition(sk1,sk2))),sk3) != join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(complement(composition(sk1,sk2))),sk3)) ),
inference(forward_demodulation,[],[f27111,f10941]) ).
fof(f27113,plain,
composition(complement(complement(composition(sk1,sk2))),sk3) != join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(complement(composition(sk1,sk2))),sk3)),
inference(forward_subsumption_resolution,[],[f27112,f1190]) ).
fof(f27114,plain,
composition(complement(complement(composition(sk1,sk2))),sk3) != join(composition(complement(complement(composition(sk1,sk2))),sk3),complement(join(complement(composition(sk2,sk3)),complement(composition(sk1,sk3))))),
inference(forward_demodulation,[],[f27113,f6994]) ).
fof(f27115,plain,
composition(complement(complement(composition(sk1,sk2))),sk3) != join(composition(complement(complement(composition(sk1,sk2))),sk3),complement(join(complement(sk3),complement(composition(sk1,composition(sk2,sk3)))))),
inference(forward_demodulation,[],[f27114,f15693]) ).
fof(f27116,plain,
composition(complement(complement(composition(sk1,sk2))),sk3) != join(composition(complement(complement(composition(sk1,sk2))),sk3),complement(complement(composition(sk1,composition(sk2,sk3))))),
inference(forward_demodulation,[],[f27115,f10941]) ).
fof(f27117,plain,
composition(complement(complement(composition(sk1,sk2))),sk3) != join(complement(complement(composition(sk1,composition(sk2,sk3)))),composition(complement(complement(composition(sk1,sk2))),sk3)),
inference(forward_demodulation,[],[f27116,f1]) ).
fof(f27118,plain,
composition(composition(sk1,sk2),sk3) != join(complement(complement(composition(sk1,composition(sk2,sk3)))),composition(composition(sk1,sk2),sk3)),
inference(forward_demodulation,[],[f27117,f1190]) ).
fof(f27119,plain,
composition(composition(sk1,sk2),sk3) != join(composition(composition(sk1,sk2),sk3),complement(complement(composition(sk1,composition(sk2,sk3))))),
inference(forward_demodulation,[],[f27118,f1]) ).
fof(f27120,plain,
composition(composition(sk1,sk2),sk3) != join(composition(composition(sk1,sk2),sk3),composition(sk1,composition(sk2,sk3))),
inference(forward_demodulation,[],[f27119,f1190]) ).
fof(f27121,plain,
composition(composition(sk1,sk2),sk3) != composition(join(composition(sk1,sk2),composition(sk1,sk2)),sk3),
inference(forward_demodulation,[],[f27120,f664]) ).
fof(f27122,plain,
composition(composition(sk1,sk2),sk3) != composition(composition(sk1,sk2),join(sk3,sk3)),
inference(forward_demodulation,[],[f27121,f429]) ).
fof(f27123,plain,
composition(composition(sk1,sk2),sk3) != composition(sk1,composition(sk2,join(sk3,sk3))),
inference(forward_demodulation,[],[f27122,f7]) ).
fof(f27124,plain,
composition(sk1,composition(sk2,sk3)) != composition(composition(sk1,sk2),sk3),
inference(forward_demodulation,[],[f27123,f1235]) ).
fof(f27125,plain,
$false,
inference(forward_subsumption_resolution,[],[f27124,f7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : REL029-4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.44 % Computer : n017.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Sun Sep 27 22:49:35 UTC 2026
% 0.16/0.45 % CPUTime :
% 0.16/0.45 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.22/0.50 Running first-order theorem proving
% 0.22/0.50 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
% 19.76/3.81 % (3042200)Input is clausal, will run a generic CNF schedule.
% 19.76/3.81 % (3042206)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1023834021:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 19.76/3.81 % (3042207)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2723145035:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 19.76/3.81 % (3042205)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=3111973426:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 19.76/3.81 % (3042209)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2101860112:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 19.76/3.81 % (3042210)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=280512821:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 19.76/3.81 % (3042211)dis-21_1_sil=8000:lcm=predicate:random_seed=3583817573: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)
% 19.76/3.81 % (3042208)lrs+10_1_sil=8000:sp=occurrence:random_seed=1342551899:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 19.76/3.81 % (3042211)Refutation not found, incomplete strategy
% 19.76/3.81 % (3042211)------------------------------
% 19.76/3.81 % (3042211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/3.81 % (3042211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/3.81 % (3042211)CaDiCaL version: 2.1.3
% 19.76/3.81 % (3042211)Termination reason: Refutation not found, incomplete strategy
% 19.76/3.81 % (3042211)Time elapsed: 0.003 s
% 19.76/3.81 % (3042211)Peak memory usage: 88 MB
% 19.76/3.81 % (3042211)Instructions burned: 1 (million)
% 19.76/3.81 % (3042208)Instruction limit reached!
% 19.76/3.81 % (3042208)------------------------------
% 19.76/3.81 % (3042208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/3.81 % (3042208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/3.81 % (3042208)CaDiCaL version: 2.1.3
% 19.76/3.81 % (3042208)Termination reason: Instruction limit
% 19.76/3.81 % (3042208)Termination phase: Saturation
% 19.76/3.81 % (3042208)Time elapsed: 0.097 s
% 19.76/3.81 % (3042208)Peak memory usage: 89 MB
% 19.76/3.81 % (3042208)Instructions burned: 107 (million)
% 19.76/3.81 % (3042209)Instruction limit reached!
% 19.76/3.81 % (3042209)------------------------------
% 19.76/3.81 % (3042209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/3.81 % (3042209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/3.81 % (3042209)CaDiCaL version: 2.1.3
% 19.76/3.81 % (3042209)Termination reason: Instruction limit
% 19.76/3.81 % (3042209)Termination phase: Saturation
% 19.76/3.81 % (3042209)Time elapsed: 0.115 s
% 19.76/3.81 % (3042209)Peak memory usage: 89 MB
% 19.76/3.81 % (3042209)Instructions burned: 114 (million)
% 19.76/3.81 % (3042210)Instruction limit reached!
% 19.76/3.81 % (3042210)------------------------------
% 19.76/3.81 % (3042210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/3.81 % (3042210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/3.81 % (3042210)CaDiCaL version: 2.1.3
% 19.76/3.81 % (3042210)Termination reason: Instruction limit
% 19.76/3.81 % (3042210)Termination phase: Saturation
% 19.76/3.81 % (3042210)Time elapsed: 0.174 s
% 19.76/3.81 % (3042210)Peak memory usage: 90 MB
% 19.76/3.81 % (3042210)Instructions burned: 180 (million)
% 19.76/3.81 % (3042219)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=3234514683:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 19.76/3.81 % (3042211)------------------------------
% 19.76/3.81 % (3042211)------------------------------
% 19.76/3.81 % (3042220)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2400825671:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 19.76/3.81 % (3042221)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3239076499:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 19.76/3.81 % (3042219)Instruction limit reached!
% 19.76/3.81 % (3042219)------------------------------
% 19.29/4.17 % (3042219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/4.17 % (3042219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/4.17 % (3042219)CaDiCaL version: 2.1.3
% 19.29/4.17 % (3042219)Termination reason: Instruction limit
% 19.29/4.17 % (3042219)Termination phase: Saturation
% 19.29/4.17 % (3042219)Time elapsed: 0.116 s
% 19.29/4.17 % (3042219)Peak memory usage: 89 MB
% 19.29/4.17 % (3042219)Instructions burned: 144 (million)
% 19.29/4.17 % (3042223)lrs+10_64_to=lpo:sil=8000:random_seed=494549325:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 19.29/4.17 % (3042220)Instruction limit reached!
% 19.29/4.17 % (3042220)------------------------------
% 19.29/4.17 % (3042220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/4.17 % (3042220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/4.17 % (3042220)CaDiCaL version: 2.1.3
% 19.29/4.17 % (3042220)Termination reason: Instruction limit
% 19.29/4.17 % (3042220)Termination phase: Saturation
% 19.29/4.17 % (3042220)Time elapsed: 0.205 s
% 19.29/4.17 % (3042220)Peak memory usage: 90 MB
% 19.29/4.17 % (3042220)Instructions burned: 190 (million)
% 19.29/4.17 % (3042221)Instruction limit reached!
% 19.29/4.17 % (3042221)------------------------------
% 19.29/4.17 % (3042221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/4.17 % (3042221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/4.17 % (3042221)CaDiCaL version: 2.1.3
% 19.29/4.17 % (3042221)Termination reason: Instruction limit
% 19.29/4.17 % (3042221)Termination phase: Saturation
% 19.29/4.17 % (3042221)Time elapsed: 0.197 s
% 19.29/4.17 % (3042221)Peak memory usage: 90 MB
% 19.29/4.17 % (3042221)Instructions burned: 220 (million)
% 19.29/4.17 % (3042223)Instruction limit reached!
% 19.29/4.17 % (3042223)------------------------------
% 19.29/4.17 % (3042223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/4.17 % (3042223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/4.17 % (3042223)CaDiCaL version: 2.1.3
% 19.29/4.17 % (3042223)Termination reason: Instruction limit
% 19.29/4.17 % (3042223)Termination phase: Saturation
% 19.29/4.17 % (3042223)Time elapsed: 0.093 s
% 19.29/4.17 % (3042223)Peak memory usage: 89 MB
% 19.29/4.17 % (3042223)Instructions burned: 126 (million)
% 19.29/4.17 % (3042226)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=566405282:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 19.29/4.17 % (3042228)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=252244590:i=157:gtg=all_2990 on theBenchmark for (2990ds/157Mi)
% 19.29/4.17 % (3042226)Instruction limit reached!
% 19.29/4.17 % (3042226)------------------------------
% 19.29/4.17 % (3042226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/4.17 % (3042226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/4.17 % (3042226)CaDiCaL version: 2.1.3
% 19.29/4.17 % (3042226)Termination reason: Instruction limit
% 19.29/4.17 % (3042226)Termination phase: Saturation
% 19.29/4.17 % (3042226)Time elapsed: 0.171 s
% 19.29/4.17 % (3042226)Peak memory usage: 90 MB
% 19.29/4.17 % (3042226)Instructions burned: 194 (million)
% 19.29/4.17 % (3042229)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2371120834:i=3394:sd=4:ss=included:sgt=64_2990 on theBenchmark for (2990ds/3394Mi)
% 19.29/4.17 % (3042230)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=2134861552:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi)
% 19.29/4.17 % (3042228)Instruction limit reached!
% 19.29/4.17 % (3042228)------------------------------
% 19.29/4.17 % (3042228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/4.17 % (3042228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/4.17 % (3042228)CaDiCaL version: 2.1.3
% 19.29/4.17 % (3042228)Termination reason: Instruction limit
% 19.29/4.17 % (3042228)Termination phase: Saturation
% 19.29/4.17 % (3042228)Time elapsed: 0.167 s
% 19.29/4.17 % (3042228)Peak memory usage: 91 MB
% 19.29/4.17 % (3042228)Instructions burned: 157 (million)
% 19.29/4.17 % (3042230)Instruction limit reached!
% 19.29/4.17 % (3042230)------------------------------
% 19.29/4.17 % (3042230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/4.17 % (3042230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/4.17 % (3042230)CaDiCaL version: 2.1.3
% 19.29/4.17 % (3042230)Termination reason: Instruction limit
% 19.29/4.17 % (3042230)Termination phase: Saturation
% 19.29/4.17 % (3042230)Time elapsed: 0.113 s
% 19.29/4.17 % (3042230)Peak memory usage: 89 MB
% 19.29/4.17 % (3042230)Instructions burned: 108 (million)
% 19.29/4.17 % (3042233)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4233620549:i=107_2987 on theBenchmark for (2987ds/107Mi)
% 19.29/4.17 % (3042233)Instruction limit reached!
% 19.29/4.17 % (3042233)------------------------------
% 19.29/4.17 % (3042233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/4.17 % (3042233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/4.17 % (3042233)CaDiCaL version: 2.1.3
% 19.29/4.17 % (3042233)Termination reason: Instruction limit
% 19.29/4.17 % (3042233)Termination phase: Saturation
% 19.29/4.17 % (3042233)Time elapsed: 0.088 s
% 19.29/4.17 % (3042233)Peak memory usage: 88 MB
% 19.29/4.17 % (3042233)Instructions burned: 107 (million)
% 19.29/4.17 % (3042236)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3924304429:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2986 on theBenchmark for (2986ds/242Mi)
% 19.29/4.17 % (3042238)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3607612798:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi)
% 19.29/4.17 % (3042236)Instruction limit reached!
% 19.29/4.17 % (3042236)------------------------------
% 19.29/4.17 % (3042236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/4.17 % (3042236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/4.17 % (3042236)CaDiCaL version: 2.1.3
% 19.29/4.17 % (3042236)Termination reason: Instruction limit
% 19.29/4.17 % (3042236)Termination phase: Saturation
% 19.29/4.17 % (3042236)Time elapsed: 0.218 s
% 19.29/4.17 % (3042236)Peak memory usage: 89 MB
% 19.29/4.17 % (3042236)Instructions burned: 243 (million)
% 19.29/4.17 % (3042241)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=393455475:i=134:sd=2:doe=on:ss=axioms:sgt=14_2983 on theBenchmark for (2983ds/134Mi)
% 19.29/4.17 % (3042241)Instruction limit reached!
% 19.29/4.17 % (3042241)------------------------------
% 19.29/4.17 % (3042241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/4.17 % (3042241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/4.17 % (3042241)CaDiCaL version: 2.1.3
% 19.29/4.17 % (3042241)Termination reason: Instruction limit
% 19.29/4.17 % (3042241)Termination phase: Saturation
% 19.29/4.17 % (3042241)Time elapsed: 0.110 s
% 19.29/4.17 % (3042241)Peak memory usage: 89 MB
% 19.29/4.17 % (3042241)Instructions burned: 134 (million)
% 19.29/4.17 % (3042244)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1609214635:i=499:bd=all_2981 on theBenchmark for (2981ds/499Mi)
% 19.29/4.17 % (3042246)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=4190203231:i=191:fgj=on:bd=all_2979 on theBenchmark for (2979ds/191Mi)
% 19.29/4.17 % (3042246)Instruction limit reached!
% 19.29/4.17 % (3042246)------------------------------
% 19.29/4.17 % (3042246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/4.17 % (3042246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/4.17 % (3042246)CaDiCaL version: 2.1.3
% 19.29/4.17 % (3042246)Termination reason: Instruction limit
% 19.29/4.17 % (3042246)Termination phase: Saturation
% 19.29/4.17 % (3042246)Time elapsed: 0.180 s
% 19.29/4.17 % (3042246)Peak memory usage: 90 MB
% 19.29/4.17 % (3042246)Instructions burned: 191 (million)
% 19.29/4.17 % (3042206)First to succeed.
% 19.29/4.17 % (3042244)Instruction limit reached!
% 19.29/4.17 % (3042244)------------------------------
% 19.29/4.17 % (3042244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/4.17 % (3042244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/4.17 % (3042244)CaDiCaL version: 2.1.3
% 19.29/4.17 % (3042244)Termination reason: Instruction limit
% 19.29/4.17 % (3042244)Termination phase: Saturation
% 19.29/4.17 % (3042244)Time elapsed: 0.507 s
% 19.29/4.17 % (3042244)Peak memory usage: 93 MB
% 19.29/4.17 % (3042244)Instructions burned: 499 (million)
% 19.29/4.17 % (3042206)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3042200"
% 19.29/4.17 % (3042249)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3134856893:i=264:kws=precedence:fsr=off_2975 on theBenchmark for (2975ds/264Mi)
% 19.29/4.17 % (3042250)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1593102397:cond=on:i=156:bs=on:gtg=exists_all:er=known_2973 on theBenchmark for (2973ds/156Mi)
% 19.29/4.17 % (3042249)Instruction limit reached!
% 19.29/4.17 % (3042249)------------------------------
% 19.29/4.17 % (3042249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/4.17 % (3042249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/4.17 % (3042249)CaDiCaL version: 2.1.3
% 19.29/4.17 % (3042249)Termination reason: Instruction limit
% 19.29/4.17 % (3042249)Termination phase: Saturation
% 19.29/4.17 % (3042249)Time elapsed: 0.263 s
% 19.29/4.17 % (3042249)Peak memory usage: 91 MB
% 19.29/4.17 % (3042249)Instructions burned: 264 (million)
% 19.29/4.17 % (3042250)Instruction limit reached!
% 19.29/4.17 % (3042250)------------------------------
% 19.29/4.17 % (3042250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/4.17 % (3042250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/4.17 % (3042250)CaDiCaL version: 2.1.3
% 19.29/4.17 % (3042250)Termination reason: Instruction limit
% 19.29/4.17 % (3042250)Termination phase: Saturation
% 19.29/4.17 % (3042250)Time elapsed: 0.155 s
% 19.29/4.17 % (3042250)Peak memory usage: 90 MB
% 19.29/4.17 % (3042250)Instructions burned: 156 (million)
% 19.29/4.17 % (3042206)Refutation found. Thanks to Tanya!
% 19.29/4.17 % SZS status Unsatisfiable for theBenchmark
% 19.29/4.17 % SZS output start Proof for theBenchmark
% See solution above
% 22.91/4.45 % (3042206)------------------------------
% 22.91/4.45 % (3042206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.91/4.45 % (3042206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.91/4.45 % (3042206)CaDiCaL version: 2.1.3
% 22.91/4.45 % (3042206)Termination reason: Refutation
% 22.91/4.45 % (3042206)Time elapsed: 2.485 s
% 22.91/4.45 % (3042206)Peak memory usage: 145 MB
% 22.91/4.45 % (3042206)Instructions burned: 2882 (million)
% 22.91/4.45 % (3042206)------------------------------
% 22.91/4.45 % (3042206)------------------------------
% 22.91/4.45 % (3042200)Success in time 3.122 s
% 22.91/4.45 % Vampire exiting
%------------------------------------------------------------------------------