%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : REL006-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n008.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:34:13 PM UTC 2026
% Result : Unsatisfiable 20.23s 7.60s
% Output : Refutation 20.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 64
% Number of leaves : 22
% Syntax : Number of formulae : 331 ( 331 unt; 10 def)
% Number of atoms : 331 ( 330 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 14 con; 0-2 aty)
% Number of variables : 421 ( 421 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001-0.ax',maddux1_join_commutativity_1) ).
fof(f2,axiom,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001-0.ax',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/sandbox2/benchmark/Axioms/REL001-0.ax',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/sandbox2/benchmark/Axioms/REL001-0.ax',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/sandbox2/benchmark/Axioms/REL001-0.ax',composition_associativity_5) ).
fof(f10,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/REL001-0.ax',converse_idempotence_8) ).
fof(f11,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001-0.ax',converse_additivity_9) ).
fof(f13,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001-0.ax',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/sandbox2/benchmark/Axioms/REL001-0.ax',def_top_12) ).
fof(f16,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001-0.ax',def_zero_13) ).
fof(f17,negated_conjecture,
meet(converse(sk1),sk2) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_14) ).
fof(f18,plain,
zero = meet(converse(sk1),sk2),
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
meet(sk1,converse(sk2)) != zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_15) ).
fof(f20,plain,
zero != meet(sk1,converse(sk2)),
inference(reorient_equations,[],[f19]) ).
fof(f21,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f16,f6]) ).
fof(f22,plain,
zero = complement(join(complement(converse(sk1)),complement(sk2))),
inference(definition_unfolding,[],[f18,f6]) ).
fof(f23,plain,
zero != complement(join(complement(sk1),complement(converse(sk2)))),
inference(definition_unfolding,[],[f20,f6]) ).
fof(f24,definition,
sF0 = converse(sk1),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f25,plain,
converse(sk1) = sF0,
inference(reorient_equations,[],[f24]) ).
fof(f26,definition,
sF1 = complement(sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f27,plain,
complement(sF0) = sF1,
inference(reorient_equations,[],[f26]) ).
fof(f28,definition,
sF2 = complement(sk2),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f29,plain,
complement(sk2) = sF2,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF3 = join(sF1,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f31,plain,
join(sF1,sF2) = sF3,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF4 = complement(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f33,plain,
complement(sF3) = sF4,
inference(reorient_equations,[],[f32]) ).
fof(f34,plain,
zero = sF4,
inference(definition_folding,[],[f22,f33,f31,f29,f27,f25]) ).
fof(f35,definition,
sF5 = complement(sk1),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f36,plain,
complement(sk1) = sF5,
inference(reorient_equations,[],[f35]) ).
fof(f37,definition,
sF6 = converse(sk2),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f38,plain,
converse(sk2) = sF6,
inference(reorient_equations,[],[f37]) ).
fof(f39,definition,
sF7 = complement(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f40,plain,
complement(sF6) = sF7,
inference(reorient_equations,[],[f39]) ).
fof(f41,definition,
sF8 = join(sF5,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f42,plain,
join(sF5,sF7) = sF8,
inference(reorient_equations,[],[f41]) ).
fof(f43,definition,
sF9 = complement(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f44,plain,
complement(sF8) = sF9,
inference(reorient_equations,[],[f43]) ).
fof(f45,plain,
zero != sF9,
inference(definition_folding,[],[f23,f44,f42,f40,f38,f36]) ).
fof(f46,plain,
zero = complement(sF3),
inference(forward_demodulation,[],[f33,f34]) ).
fof(f47,plain,
sk1 = converse(sF0),
inference(superposition,[],[f10,f25]) ).
fof(f54,plain,
top = join(sF3,zero),
inference(superposition,[],[f15,f46]) ).
fof(f57,plain,
top = join(zero,sF3),
inference(forward_demodulation,[],[f54,f1]) ).
fof(f65,plain,
zero = complement(top),
inference(superposition,[],[f21,f15]) ).
fof(f80,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[],[f11,f10]) ).
fof(f82,plain,
! [X0] : converse(join(sk2,X0)) = join(sF6,converse(X0)),
inference(superposition,[],[f11,f38]) ).
fof(f83,plain,
! [X0] : converse(join(sF0,X0)) = join(sk1,converse(X0)),
inference(superposition,[],[f11,f47]) ).
fof(f85,plain,
! [X0,X1] : converse(join(X1,converse(X0))) = join(converse(X1),X0),
inference(superposition,[],[f11,f10]) ).
fof(f108,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f2,f15]) ).
fof(f110,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(superposition,[],[f2,f1]) ).
fof(f113,plain,
! [X0] : join(zero,join(sF3,X0)) = join(top,X0),
inference(superposition,[],[f2,f57]) ).
fof(f117,plain,
! [X0] : join(sF5,join(sF7,X0)) = join(sF8,X0),
inference(superposition,[],[f2,f42]) ).
fof(f121,plain,
! [X0,X1] : top = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f15,f2]) ).
fof(f123,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f128,plain,
! [X0] : join(top,X0) = join(zero,join(X0,sF3)),
inference(superposition,[],[f113,f1]) ).
fof(f195,plain,
! [X2,X0,X1] : complement(X2) = join(composition(converse(composition(X0,X1)),complement(composition(X0,composition(X1,X2)))),complement(X2)),
inference(superposition,[],[f14,f7]) ).
fof(f218,plain,
! [X2,X0,X1] : complement(X2) = join(complement(X2),composition(converse(composition(X0,X1)),complement(composition(X0,composition(X1,X2))))),
inference(forward_demodulation,[],[f195,f1]) ).
fof(f240,plain,
! [X0] : join(complement(join(complement(X0),zero)),complement(join(complement(X0),sF3))) = X0,
inference(superposition,[],[f4,f46]) ).
fof(f247,plain,
! [X0] : join(zero,complement(join(complement(X0),complement(X0)))) = X0,
inference(superposition,[],[f4,f21]) ).
fof(f249,plain,
! [X0] : top = join(complement(join(zero,complement(X0))),complement(join(zero,X0))),
inference(superposition,[],[f4,f65]) ).
fof(f251,plain,
! [X0] : sk2 = join(complement(join(sF2,complement(X0))),complement(join(sF2,X0))),
inference(superposition,[],[f4,f29]) ).
fof(f252,plain,
! [X0] : sF0 = join(complement(join(sF1,complement(X0))),complement(join(sF1,X0))),
inference(superposition,[],[f4,f27]) ).
fof(f253,plain,
! [X0] : sF3 = join(complement(join(zero,complement(X0))),complement(join(zero,X0))),
inference(superposition,[],[f4,f46]) ).
fof(f256,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(f259,plain,
! [X0,X1] : join(complement(join(complement(X1),complement(X0))),complement(join(X0,complement(X1)))) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f260,plain,
! [X0] : join(complement(join(complement(X0),complement(complement(complement(X0))))),zero) = X0,
inference(superposition,[],[f4,f21]) ).
fof(f263,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(f265,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(superposition,[],[f1,f4]) ).
fof(f266,plain,
! [X2,X0,X1] : join(X0,X2) = join(complement(join(complement(X0),X1)),join(X2,complement(join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f263,f123]) ).
fof(f267,plain,
! [X0] : join(zero,complement(join(complement(X0),complement(complement(complement(X0)))))) = X0,
inference(forward_demodulation,[],[f260,f1]) ).
fof(f268,plain,
! [X0,X1] : join(complement(join(X0,complement(X1))),complement(join(complement(X1),complement(X0)))) = X1,
inference(forward_demodulation,[],[f259,f1]) ).
fof(f271,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,[],[f256,f1]) ).
fof(f274,plain,
! [X0] : sF3 = join(complement(join(zero,X0)),complement(join(zero,complement(X0)))),
inference(forward_demodulation,[],[f253,f1]) ).
fof(f275,plain,
! [X0] : sF0 = join(complement(join(sF1,X0)),complement(join(sF1,complement(X0)))),
inference(forward_demodulation,[],[f252,f1]) ).
fof(f276,plain,
! [X0] : sk2 = join(complement(join(sF2,X0)),complement(join(sF2,complement(X0)))),
inference(forward_demodulation,[],[f251,f1]) ).
fof(f278,plain,
! [X0] : top = join(complement(join(zero,X0)),complement(join(zero,complement(X0)))),
inference(forward_demodulation,[],[f249,f1]) ).
fof(f286,plain,
! [X0] : join(complement(join(complement(X0),zero)),complement(join(sF3,complement(X0)))) = X0,
inference(forward_demodulation,[],[f240,f1]) ).
fof(f293,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,[],[f271,f1]) ).
fof(f294,plain,
top = sF3,
inference(forward_demodulation,[],[f278,f274]) ).
fof(f299,plain,
! [X0] : join(complement(join(sF3,complement(X0))),complement(join(complement(X0),zero))) = X0,
inference(forward_demodulation,[],[f286,f1]) ).
fof(f308,plain,
! [X0] : join(complement(join(sF3,complement(X0))),complement(join(zero,complement(X0)))) = X0,
inference(forward_demodulation,[],[f299,f1]) ).
fof(f316,plain,
! [X0] : join(complement(join(zero,complement(X0))),complement(join(sF3,complement(X0)))) = X0,
inference(forward_demodulation,[],[f308,f1]) ).
fof(f338,plain,
! [X0] : sF3 = join(complement(join(X0,zero)),complement(join(zero,complement(X0)))),
inference(superposition,[],[f274,f1]) ).
fof(f348,plain,
! [X0] : join(zero,X0) = join(complement(sF3),complement(join(complement(join(zero,X0)),join(zero,complement(X0))))),
inference(superposition,[],[f4,f274]) ).
fof(f352,plain,
! [X0] : join(zero,X0) = join(complement(sF3),complement(join(complement(X0),join(complement(join(zero,X0)),zero)))),
inference(forward_demodulation,[],[f348,f123]) ).
fof(f363,plain,
! [X0] : join(zero,X0) = join(complement(sF3),complement(join(zero,join(complement(X0),complement(join(zero,X0)))))),
inference(forward_demodulation,[],[f352,f123]) ).
fof(f369,plain,
! [X0] : join(zero,X0) = join(zero,complement(join(zero,join(complement(X0),complement(join(zero,X0)))))),
inference(forward_demodulation,[],[f363,f46]) ).
fof(f396,plain,
! [X0,X1] : join(X0,X1) = join(complement(join(zero,complement(X0))),join(complement(join(sF3,complement(X0))),X1)),
inference(superposition,[],[f2,f316]) ).
fof(f823,plain,
! [X0] : converse(top) = join(X0,converse(complement(converse(X0)))),
inference(superposition,[],[f80,f15]) ).
fof(f843,plain,
! [X0] : converse(sF3) = join(X0,converse(complement(converse(X0)))),
inference(forward_demodulation,[],[f823,f294]) ).
fof(f1306,plain,
! [X0,X1] : join(top,complement(join(complement(X0),X1))) = join(join(complement(X0),complement(X1)),X0),
inference(superposition,[],[f108,f4]) ).
fof(f1307,plain,
! [X0] : join(top,complement(join(zero,complement(X0)))) = join(join(zero,X0),sF3),
inference(superposition,[],[f108,f274]) ).
fof(f1308,plain,
! [X0] : join(top,complement(join(sF3,complement(X0)))) = join(join(zero,complement(X0)),X0),
inference(superposition,[],[f108,f316]) ).
fof(f1310,plain,
! [X0,X1] : join(top,X0) = join(X1,join(X0,complement(X1))),
inference(superposition,[],[f108,f1]) ).
fof(f1313,plain,
! [X0] : join(X0,top) = join(top,complement(complement(X0))),
inference(superposition,[],[f108,f15]) ).
fof(f1364,plain,
! [X0] : join(X0,sF3) = join(sF3,complement(complement(X0))),
inference(forward_demodulation,[],[f1313,f294]) ).
fof(f1367,plain,
! [X0,X1] : join(sF3,X0) = join(X1,join(X0,complement(X1))),
inference(forward_demodulation,[],[f1310,f294]) ).
fof(f1369,plain,
! [X0] : join(top,complement(join(sF3,complement(X0)))) = join(X0,join(zero,complement(X0))),
inference(forward_demodulation,[],[f1308,f1]) ).
fof(f1370,plain,
! [X0] : join(sF3,join(zero,X0)) = join(top,complement(join(zero,complement(X0)))),
inference(forward_demodulation,[],[f1307,f1]) ).
fof(f1371,plain,
! [X0,X1] : join(top,complement(join(complement(X0),X1))) = join(X0,join(complement(X0),complement(X1))),
inference(forward_demodulation,[],[f1306,f1]) ).
fof(f1390,plain,
! [X0] : join(sF3,zero) = join(top,complement(join(sF3,complement(X0)))),
inference(forward_demodulation,[],[f1369,f1367]) ).
fof(f1391,plain,
! [X0] : join(sF3,join(zero,X0)) = join(sF3,complement(join(zero,complement(X0)))),
inference(forward_demodulation,[],[f1370,f294]) ).
fof(f1392,plain,
! [X0,X1] : join(top,complement(join(complement(X0),X1))) = join(top,complement(X1)),
inference(forward_demodulation,[],[f1371,f108]) ).
fof(f1401,plain,
! [X0] : join(sF3,zero) = join(sF3,complement(join(sF3,complement(X0)))),
inference(forward_demodulation,[],[f1390,f294]) ).
fof(f1402,plain,
! [X0] : join(zero,join(X0,sF3)) = join(sF3,complement(join(zero,complement(X0)))),
inference(forward_demodulation,[],[f1391,f123]) ).
fof(f1403,plain,
! [X0,X1] : join(sF3,complement(join(complement(X0),X1))) = join(sF3,complement(X1)),
inference(forward_demodulation,[],[f1392,f294]) ).
fof(f1406,plain,
! [X0] : join(zero,sF3) = join(sF3,complement(join(sF3,complement(X0)))),
inference(forward_demodulation,[],[f1401,f1]) ).
fof(f1407,plain,
! [X0] : join(top,X0) = join(sF3,complement(join(zero,complement(X0)))),
inference(forward_demodulation,[],[f1402,f128]) ).
fof(f1408,plain,
! [X0] : top = join(sF3,complement(join(sF3,complement(X0)))),
inference(forward_demodulation,[],[f1406,f57]) ).
fof(f1409,plain,
! [X0] : join(sF3,X0) = join(sF3,complement(join(zero,complement(X0)))),
inference(forward_demodulation,[],[f1407,f294]) ).
fof(f1410,plain,
! [X0] : sF3 = join(sF3,complement(join(sF3,complement(X0)))),
inference(forward_demodulation,[],[f1408,f294]) ).
fof(f1417,plain,
! [X0,X1] : top = join(X1,join(join(complement(X1),X0),complement(join(top,X0)))),
inference(superposition,[],[f121,f108]) ).
fof(f1481,plain,
! [X0,X1] : join(X0,top) = join(top,join(X1,complement(join(complement(X0),X1)))),
inference(superposition,[],[f108,f121]) ).
fof(f1519,plain,
! [X0,X1] : join(X0,sF3) = join(sF3,join(X1,complement(join(complement(X0),X1)))),
inference(forward_demodulation,[],[f1481,f294]) ).
fof(f1582,plain,
! [X0,X1] : top = join(X1,join(complement(join(top,X0)),join(complement(X1),X0))),
inference(forward_demodulation,[],[f1417,f1]) ).
fof(f1628,plain,
! [X0,X1] : top = join(X1,join(X0,join(complement(join(top,X0)),complement(X1)))),
inference(forward_demodulation,[],[f1582,f123]) ).
fof(f1650,plain,
! [X0,X1] : sF3 = join(X1,join(X0,join(complement(join(sF3,X0)),complement(X1)))),
inference(forward_demodulation,[],[f1628,f294]) ).
fof(f1668,plain,
! [X0] : join(complement(X0),complement(X0)) = join(complement(X0),complement(join(sF3,complement(join(complement(X0),complement(X0)))))),
inference(superposition,[],[f316,f247]) ).
fof(f1675,plain,
! [X0] : join(complement(X0),complement(X0)) = join(complement(X0),complement(join(sF3,complement(complement(X0))))),
inference(forward_demodulation,[],[f1668,f1403]) ).
fof(f1678,plain,
! [X0] : join(complement(X0),complement(X0)) = join(complement(X0),complement(join(X0,sF3))),
inference(forward_demodulation,[],[f1675,f1364]) ).
fof(f1692,plain,
! [X2,X3,X0,X1] : join(join(X0,join(X1,X2)),X3) = join(X2,join(join(X0,X1),X3)),
inference(superposition,[],[f110,f2]) ).
fof(f1819,plain,
! [X2,X3,X0,X1] : join(join(X0,join(X1,X2)),X3) = join(X2,join(X0,join(X1,X3))),
inference(forward_demodulation,[],[f1692,f2]) ).
fof(f1856,plain,
! [X2,X3,X0,X1] : join(X0,join(join(X1,X2),X3)) = join(X2,join(X0,join(X1,X3))),
inference(forward_demodulation,[],[f1819,f2]) ).
fof(f1870,plain,
! [X2,X3,X0,X1] : join(X0,join(X1,join(X2,X3))) = join(X2,join(X0,join(X1,X3))),
inference(forward_demodulation,[],[f1856,f2]) ).
fof(f2039,plain,
! [X0,X1] : sF3 = join(complement(join(X0,join(zero,X1))),complement(join(zero,complement(join(X1,X0))))),
inference(superposition,[],[f274,f123]) ).
fof(f2785,plain,
! [X0] : join(complement(X0),complement(complement(complement(X0)))) = join(complement(X0),complement(join(sF3,complement(join(complement(X0),complement(complement(complement(X0)))))))),
inference(superposition,[],[f316,f267]) ).
fof(f2797,plain,
! [X0] : join(complement(X0),complement(complement(complement(X0)))) = join(complement(X0),complement(join(sF3,complement(complement(complement(complement(X0))))))),
inference(forward_demodulation,[],[f2785,f1403]) ).
fof(f2801,plain,
! [X0] : join(complement(X0),complement(complement(complement(X0)))) = join(complement(X0),complement(join(complement(complement(X0)),sF3))),
inference(forward_demodulation,[],[f2797,f1364]) ).
fof(f2802,plain,
! [X0] : join(complement(X0),complement(complement(complement(X0)))) = join(complement(X0),complement(join(sF3,complement(complement(X0))))),
inference(forward_demodulation,[],[f2801,f1]) ).
fof(f2803,plain,
! [X0] : join(complement(X0),complement(complement(complement(X0)))) = join(complement(X0),complement(join(X0,sF3))),
inference(forward_demodulation,[],[f2802,f1364]) ).
fof(f2804,plain,
! [X0] : join(complement(X0),complement(X0)) = join(complement(X0),complement(complement(complement(X0)))),
inference(forward_demodulation,[],[f2803,f1678]) ).
fof(f3160,plain,
sk2 = join(complement(join(sF2,sF0)),complement(join(sF2,sF1))),
inference(superposition,[],[f276,f27]) ).
fof(f3183,plain,
sk2 = join(complement(join(sF2,sF0)),complement(join(sF1,sF2))),
inference(forward_demodulation,[],[f3160,f1]) ).
fof(f3200,plain,
sk2 = join(complement(join(sF1,sF2)),complement(join(sF2,sF0))),
inference(forward_demodulation,[],[f3183,f1]) ).
fof(f3209,plain,
sk2 = join(complement(join(sF1,sF2)),complement(join(sF0,sF2))),
inference(forward_demodulation,[],[f3200,f1]) ).
fof(f3216,plain,
sk2 = join(complement(join(sF0,sF2)),complement(join(sF1,sF2))),
inference(forward_demodulation,[],[f3209,f1]) ).
fof(f3220,plain,
sk2 = join(complement(join(sF0,sF2)),complement(sF3)),
inference(forward_demodulation,[],[f3216,f31]) ).
fof(f3223,plain,
sk2 = join(complement(sF3),complement(join(sF0,sF2))),
inference(forward_demodulation,[],[f3220,f1]) ).
fof(f3226,plain,
sk2 = join(zero,complement(join(sF0,sF2))),
inference(forward_demodulation,[],[f3223,f46]) ).
fof(f3513,plain,
! [X0] : sF3 = join(sF3,complement(join(X0,sF3))),
inference(superposition,[],[f1410,f1364]) ).
fof(f3871,plain,
! [X0] : top = join(X0,sF3),
inference(superposition,[],[f121,f3513]) ).
fof(f3880,plain,
! [X0] : sF3 = join(X0,sF3),
inference(forward_demodulation,[],[f3871,f294]) ).
fof(f3962,plain,
! [X0] : sF3 = join(sF3,X0),
inference(superposition,[],[f1,f3880]) ).
fof(f3964,plain,
! [X0,X1] : join(sF3,join(X0,X1)) = join(sF3,X1),
inference(superposition,[],[f110,f3880]) ).
fof(f3971,plain,
! [X0] : join(complement(join(complement(X0),complement(sF3))),complement(sF3)) = X0,
inference(superposition,[],[f4,f3880]) ).
fof(f4007,plain,
! [X0] : join(complement(sF3),complement(join(complement(X0),complement(sF3)))) = X0,
inference(forward_demodulation,[],[f3971,f1]) ).
fof(f4028,plain,
! [X0] : join(zero,complement(join(complement(X0),zero))) = X0,
inference(forward_demodulation,[],[f4007,f46]) ).
fof(f4035,plain,
! [X0] : join(zero,complement(join(zero,complement(X0)))) = X0,
inference(forward_demodulation,[],[f4028,f1]) ).
fof(f4148,plain,
sF3 = converse(sF3),
inference(superposition,[],[f843,f3962]) ).
fof(f4951,plain,
! [X0,X1] : join(top,complement(join(complement(X0),complement(X1)))) = join(join(X1,complement(X0)),X0),
inference(superposition,[],[f108,f268]) ).
fof(f4962,plain,
! [X0,X1] : join(X0,join(X1,complement(X0))) = join(top,complement(join(complement(X0),complement(X1)))),
inference(forward_demodulation,[],[f4951,f1]) ).
fof(f5028,plain,
! [X0,X1] : join(X0,join(X1,complement(X0))) = join(sF3,complement(join(complement(X0),complement(X1)))),
inference(forward_demodulation,[],[f4962,f294]) ).
fof(f5081,plain,
! [X0,X1] : join(X0,join(X1,complement(X0))) = join(sF3,complement(complement(X1))),
inference(forward_demodulation,[],[f5028,f1403]) ).
fof(f5103,plain,
! [X0,X1] : join(X1,sF3) = join(X0,join(X1,complement(X0))),
inference(forward_demodulation,[],[f5081,f1364]) ).
fof(f5117,plain,
! [X0,X1] : sF3 = join(X0,join(X1,complement(X0))),
inference(forward_demodulation,[],[f5103,f3880]) ).
fof(f5489,plain,
! [X0] : sF3 = join(complement(sF3),complement(join(zero,complement(join(X0,complement(zero)))))),
inference(superposition,[],[f274,f5117]) ).
fof(f5500,plain,
sF3 = join(sF8,complement(sF5)),
inference(superposition,[],[f117,f5117]) ).
fof(f5522,plain,
! [X0] : sF3 = join(zero,complement(join(zero,complement(join(X0,complement(zero)))))),
inference(forward_demodulation,[],[f5489,f46]) ).
fof(f5581,plain,
! [X0] : sF3 = join(X0,complement(zero)),
inference(forward_demodulation,[],[f5522,f4035]) ).
fof(f5840,plain,
sF3 = complement(zero),
inference(superposition,[],[f14,f5581]) ).
fof(f6815,plain,
! [X2,X0,X1] : join(X1,X2) = join(complement(join(top,X0)),join(X2,complement(join(complement(X1),complement(join(complement(complement(X1)),X0)))))),
inference(superposition,[],[f266,f108]) ).
fof(f6873,plain,
! [X0,X1] : join(X0,complement(join(X1,complement(X0)))) = join(complement(join(complement(X0),X1)),X0),
inference(superposition,[],[f266,f268]) ).
fof(f6888,plain,
! [X0,X1] : join(top,complement(join(complement(X0),complement(X1)))) = join(X0,complement(complement(join(complement(X0),X1)))),
inference(superposition,[],[f108,f266]) ).
fof(f6899,plain,
! [X0,X1] : join(sF3,complement(join(complement(X0),complement(X1)))) = join(X0,complement(complement(join(complement(X0),X1)))),
inference(forward_demodulation,[],[f6888,f294]) ).
fof(f6912,plain,
! [X0,X1] : join(X0,complement(join(X1,complement(X0)))) = join(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f6873,f1]) ).
fof(f6955,plain,
! [X2,X0,X1] : join(X1,X2) = join(complement(join(sF3,X0)),join(X2,complement(join(complement(X1),complement(join(complement(complement(X1)),X0)))))),
inference(forward_demodulation,[],[f6815,f294]) ).
fof(f6977,plain,
! [X0,X1] : join(sF3,complement(complement(X1))) = join(X0,complement(complement(join(complement(X0),X1)))),
inference(forward_demodulation,[],[f6899,f1403]) ).
fof(f7022,plain,
! [X2,X0,X1] : join(X1,X2) = join(complement(sF3),join(X2,complement(join(complement(X1),complement(join(complement(complement(X1)),X0)))))),
inference(forward_demodulation,[],[f6955,f3962]) ).
fof(f7032,plain,
! [X0,X1] : join(X1,sF3) = join(X0,complement(complement(join(complement(X0),X1)))),
inference(forward_demodulation,[],[f6977,f1364]) ).
fof(f7066,plain,
! [X2,X0,X1] : join(X1,X2) = join(zero,join(X2,complement(join(complement(X1),complement(join(complement(complement(X1)),X0)))))),
inference(forward_demodulation,[],[f7022,f46]) ).
fof(f7068,plain,
! [X0,X1] : sF3 = join(X0,complement(complement(join(complement(X0),X1)))),
inference(forward_demodulation,[],[f7032,f3880]) ).
fof(f7435,plain,
! [X0] : join(complement(join(zero,X0)),complement(complement(join(zero,complement(X0))))) = join(complement(join(zero,X0)),complement(join(complement(complement(sF3)),complement(join(complement(join(zero,X0)),complement(complement(join(zero,complement(X0))))))))),
inference(superposition,[],[f293,f274]) ).
fof(f7460,plain,
! [X0,X1] : join(complement(X1),complement(join(complement(complement(X1)),X0))) = join(complement(X1),complement(join(complement(complement(join(top,X0))),complement(join(complement(X1),complement(join(complement(complement(X1)),X0))))))),
inference(superposition,[],[f293,f108]) ).
fof(f7461,plain,
! [X0,X1] : join(complement(X0),complement(join(X1,complement(join(complement(X0),X1))))) = join(complement(X0),complement(join(complement(complement(top)),complement(join(complement(X0),complement(join(X1,complement(join(complement(X0),X1))))))))),
inference(superposition,[],[f293,f121]) ).
fof(f7588,plain,
! [X0,X1] : join(complement(X0),complement(join(X1,complement(join(complement(X0),X1))))) = join(complement(X0),complement(join(complement(zero),complement(join(complement(X0),complement(join(X1,complement(join(complement(X0),X1))))))))),
inference(forward_demodulation,[],[f7461,f65]) ).
fof(f7589,plain,
! [X0,X1] : join(complement(X1),complement(join(complement(complement(X1)),X0))) = join(complement(X1),complement(join(complement(complement(join(sF3,X0))),complement(join(complement(X1),complement(join(complement(complement(X1)),X0))))))),
inference(forward_demodulation,[],[f7460,f294]) ).
fof(f7596,plain,
! [X0] : join(complement(join(zero,X0)),complement(complement(join(zero,complement(X0))))) = join(complement(join(zero,X0)),complement(join(complement(zero),complement(join(complement(join(zero,X0)),complement(complement(join(zero,complement(X0))))))))),
inference(forward_demodulation,[],[f7435,f46]) ).
fof(f7642,plain,
! [X0,X1] : join(complement(X0),complement(join(X1,complement(join(complement(X0),X1))))) = join(complement(X0),complement(join(sF3,complement(join(complement(X0),complement(join(X1,complement(join(complement(X0),X1))))))))),
inference(forward_demodulation,[],[f7588,f5840]) ).
fof(f7643,plain,
! [X0,X1] : join(complement(X1),complement(join(complement(complement(X1)),X0))) = join(complement(X1),complement(join(complement(complement(sF3)),complement(join(complement(X1),complement(join(complement(complement(X1)),X0))))))),
inference(forward_demodulation,[],[f7589,f3962]) ).
fof(f7645,plain,
! [X0] : join(complement(join(zero,X0)),complement(complement(join(zero,complement(X0))))) = join(complement(join(zero,X0)),complement(join(sF3,complement(join(complement(join(zero,X0)),complement(complement(join(zero,complement(X0))))))))),
inference(forward_demodulation,[],[f7596,f5840]) ).
fof(f7681,plain,
! [X0,X1] : join(complement(X0),complement(join(X1,complement(join(complement(X0),X1))))) = join(complement(X0),complement(join(sF3,complement(complement(join(X1,complement(join(complement(X0),X1)))))))),
inference(forward_demodulation,[],[f7642,f1403]) ).
fof(f7682,plain,
! [X0,X1] : join(complement(X1),complement(join(complement(complement(X1)),X0))) = join(complement(X1),complement(join(complement(zero),complement(join(complement(X1),complement(join(complement(complement(X1)),X0))))))),
inference(forward_demodulation,[],[f7643,f46]) ).
fof(f7684,plain,
! [X0] : join(complement(join(zero,X0)),complement(complement(join(zero,complement(X0))))) = join(complement(join(zero,X0)),complement(join(sF3,complement(complement(complement(join(zero,complement(X0)))))))),
inference(forward_demodulation,[],[f7645,f1403]) ).
fof(f7703,plain,
! [X0,X1] : join(complement(X0),complement(join(X1,complement(join(complement(X0),X1))))) = join(complement(X0),complement(join(join(X1,complement(join(complement(X0),X1))),sF3))),
inference(forward_demodulation,[],[f7681,f1364]) ).
fof(f7704,plain,
! [X0,X1] : join(complement(X1),complement(join(complement(complement(X1)),X0))) = join(complement(X1),complement(join(sF3,complement(join(complement(X1),complement(join(complement(complement(X1)),X0))))))),
inference(forward_demodulation,[],[f7682,f5840]) ).
fof(f7706,plain,
! [X0] : join(complement(join(zero,X0)),complement(complement(join(zero,complement(X0))))) = join(complement(join(zero,X0)),complement(join(complement(join(zero,complement(X0))),sF3))),
inference(forward_demodulation,[],[f7684,f1364]) ).
fof(f7719,plain,
! [X0,X1] : join(complement(X0),complement(join(X1,complement(join(complement(X0),X1))))) = join(complement(X0),complement(join(sF3,join(X1,complement(join(complement(X0),X1)))))),
inference(forward_demodulation,[],[f7703,f1]) ).
fof(f7720,plain,
! [X0,X1] : join(complement(X1),complement(join(complement(complement(X1)),X0))) = join(complement(X1),complement(join(sF3,complement(complement(join(complement(complement(X1)),X0)))))),
inference(forward_demodulation,[],[f7704,f1403]) ).
fof(f7722,plain,
! [X0] : join(complement(join(zero,X0)),complement(complement(join(zero,complement(X0))))) = join(complement(join(zero,X0)),complement(join(sF3,complement(join(zero,complement(X0)))))),
inference(forward_demodulation,[],[f7706,f1]) ).
fof(f7732,plain,
! [X0,X1] : join(complement(X0),complement(join(X1,complement(join(complement(X0),X1))))) = join(complement(X0),complement(join(X0,sF3))),
inference(forward_demodulation,[],[f7719,f1519]) ).
fof(f7733,plain,
! [X0,X1] : join(complement(X1),complement(join(complement(complement(X1)),X0))) = join(complement(X1),complement(join(join(complement(complement(X1)),X0),sF3))),
inference(forward_demodulation,[],[f7720,f1364]) ).
fof(f7735,plain,
! [X0] : join(complement(join(zero,X0)),complement(complement(join(zero,complement(X0))))) = join(complement(join(zero,X0)),complement(join(sF3,X0))),
inference(forward_demodulation,[],[f7722,f1409]) ).
fof(f7744,plain,
! [X0,X1] : join(complement(X0),complement(X0)) = join(complement(X0),complement(join(X1,complement(join(complement(X0),X1))))),
inference(forward_demodulation,[],[f7732,f1678]) ).
fof(f7745,plain,
! [X0,X1] : join(complement(X1),complement(join(complement(complement(X1)),X0))) = join(complement(X1),complement(join(sF3,join(complement(complement(X1)),X0)))),
inference(forward_demodulation,[],[f7733,f1]) ).
fof(f7747,plain,
! [X0] : join(complement(join(zero,X0)),complement(complement(join(zero,complement(X0))))) = join(complement(join(zero,X0)),complement(sF3)),
inference(forward_demodulation,[],[f7735,f3962]) ).
fof(f7753,plain,
! [X0,X1] : join(complement(X1),complement(join(complement(complement(X1)),X0))) = join(complement(X1),complement(join(sF3,X0))),
inference(forward_demodulation,[],[f7745,f3964]) ).
fof(f7755,plain,
! [X0] : join(complement(join(zero,X0)),complement(complement(join(zero,complement(X0))))) = join(complement(sF3),complement(join(zero,X0))),
inference(forward_demodulation,[],[f7747,f1]) ).
fof(f7761,plain,
! [X0,X1] : join(complement(X1),complement(join(complement(complement(X1)),X0))) = join(complement(X1),complement(sF3)),
inference(forward_demodulation,[],[f7753,f3962]) ).
fof(f7762,plain,
! [X0] : join(complement(join(zero,X0)),complement(complement(join(zero,complement(X0))))) = join(zero,complement(join(zero,X0))),
inference(forward_demodulation,[],[f7755,f46]) ).
fof(f7768,plain,
! [X0,X1] : join(complement(X1),complement(join(complement(complement(X1)),X0))) = join(complement(X1),zero),
inference(forward_demodulation,[],[f7761,f46]) ).
fof(f7772,plain,
! [X0,X1] : join(zero,complement(X1)) = join(complement(X1),complement(join(complement(complement(X1)),X0))),
inference(forward_demodulation,[],[f7768,f1]) ).
fof(f10208,plain,
! [X0] : sF3 = join(X0,complement(complement(complement(X0)))),
inference(superposition,[],[f7068,f218]) ).
fof(f12339,plain,
! [X0] : complement(complement(X0)) = join(complement(sF3),complement(join(complement(complement(complement(X0))),complement(X0)))),
inference(superposition,[],[f268,f10208]) ).
fof(f12469,plain,
! [X0] : complement(complement(X0)) = join(complement(sF3),complement(join(complement(X0),complement(complement(complement(X0)))))),
inference(forward_demodulation,[],[f12339,f1]) ).
fof(f12519,plain,
! [X0] : complement(complement(X0)) = join(complement(sF3),complement(join(complement(X0),complement(X0)))),
inference(forward_demodulation,[],[f12469,f2804]) ).
fof(f12537,plain,
! [X0] : complement(complement(X0)) = join(zero,complement(join(complement(X0),complement(X0)))),
inference(forward_demodulation,[],[f12519,f46]) ).
fof(f12545,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f12537,f247]) ).
fof(f12731,plain,
sk1 = complement(sF5),
inference(superposition,[],[f12545,f36]) ).
fof(f12733,plain,
sF0 = complement(sF1),
inference(superposition,[],[f12545,f27]) ).
fof(f12735,plain,
sF6 = complement(sF7),
inference(superposition,[],[f12545,f40]) ).
fof(f12759,plain,
! [X0] : complement(X0) = join(zero,complement(join(X0,X0))),
inference(superposition,[],[f247,f12545]) ).
fof(f12779,plain,
! [X0] : complement(X0) = join(complement(join(zero,X0)),complement(join(sF3,X0))),
inference(superposition,[],[f316,f12545]) ).
fof(f12801,plain,
! [X0] : complement(X0) = join(complement(join(zero,X0)),complement(sF3)),
inference(forward_demodulation,[],[f12779,f3962]) ).
fof(f12823,plain,
! [X0] : complement(X0) = join(complement(sF3),complement(join(zero,X0))),
inference(forward_demodulation,[],[f12801,f1]) ).
fof(f12827,plain,
! [X0] : complement(X0) = join(zero,complement(join(zero,X0))),
inference(forward_demodulation,[],[f12823,f46]) ).
fof(f15220,plain,
! [X0] : join(zero,complement(X0)) = join(complement(sF3),complement(join(complement(join(zero,complement(X0))),complement(complement(join(X0,zero)))))),
inference(superposition,[],[f268,f338]) ).
fof(f15233,plain,
! [X0] : join(zero,complement(X0)) = join(complement(sF3),complement(join(complement(complement(join(X0,zero))),complement(join(zero,complement(X0)))))),
inference(forward_demodulation,[],[f15220,f1]) ).
fof(f15281,plain,
! [X0] : join(zero,complement(X0)) = join(complement(sF3),complement(join(join(X0,zero),complement(join(zero,complement(X0)))))),
inference(forward_demodulation,[],[f15233,f12545]) ).
fof(f15326,plain,
! [X0] : join(zero,complement(X0)) = join(complement(sF3),complement(join(X0,join(zero,complement(join(zero,complement(X0))))))),
inference(forward_demodulation,[],[f15281,f2]) ).
fof(f15358,plain,
! [X0] : join(zero,complement(X0)) = join(complement(sF3),complement(join(X0,X0))),
inference(forward_demodulation,[],[f15326,f4035]) ).
fof(f15383,plain,
! [X0] : join(zero,complement(X0)) = join(zero,complement(join(X0,X0))),
inference(forward_demodulation,[],[f15358,f46]) ).
fof(f15401,plain,
! [X0] : complement(X0) = join(zero,complement(X0)),
inference(forward_demodulation,[],[f15383,f12759]) ).
fof(f15417,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f15401,f12545]) ).
fof(f15420,plain,
sF5 = join(zero,sF5),
inference(superposition,[],[f15401,f36]) ).
fof(f15422,plain,
sF1 = join(zero,sF1),
inference(superposition,[],[f15401,f27]) ).
fof(f15427,plain,
sF7 = join(zero,sF7),
inference(superposition,[],[f15401,f40]) ).
fof(f15456,plain,
sk2 = complement(join(sF0,sF2)),
inference(superposition,[],[f3226,f15401]) ).
fof(f15468,plain,
! [X0,X1] : join(X0,zero) = join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))),
inference(superposition,[],[f266,f15401]) ).
fof(f15479,plain,
! [X0,X1] : join(X1,complement(X0)) = join(zero,join(complement(X0),X1)),
inference(superposition,[],[f123,f15401]) ).
fof(f15489,plain,
! [X0] : join(X0,zero) = X0,
inference(forward_demodulation,[],[f15468,f265]) ).
fof(f22998,plain,
! [X0,X1] : join(complement(X0),complement(join(X1,join(complement(join(sF3,X1)),complement(complement(X0)))))) = join(complement(X0),complement(join(complement(complement(sF3)),complement(join(complement(X0),complement(join(X1,join(complement(join(sF3,X1)),complement(complement(X0)))))))))),
inference(superposition,[],[f293,f1650]) ).
fof(f23086,plain,
! [X0,X1] : join(complement(X0),complement(join(X1,join(complement(join(sF3,X1)),X0)))) = join(complement(X0),complement(join(complement(complement(sF3)),complement(join(complement(X0),complement(join(X1,join(complement(join(sF3,X1)),X0)))))))),
inference(forward_demodulation,[],[f22998,f12545]) ).
fof(f23167,plain,
! [X0,X1] : join(complement(X0),complement(join(X1,join(complement(sF3),X0)))) = join(complement(X0),complement(join(complement(complement(sF3)),complement(join(complement(X0),complement(join(X1,join(complement(sF3),X0)))))))),
inference(forward_demodulation,[],[f23086,f3962]) ).
fof(f23229,plain,
! [X0,X1] : join(complement(X0),complement(join(X1,join(zero,X0)))) = join(complement(X0),complement(join(complement(zero),complement(join(complement(X0),complement(join(X1,join(zero,X0)))))))),
inference(forward_demodulation,[],[f23167,f46]) ).
fof(f23285,plain,
! [X0,X1] : join(complement(X0),complement(join(X1,X0))) = join(complement(X0),complement(join(complement(zero),complement(join(complement(X0),complement(join(X1,X0))))))),
inference(forward_demodulation,[],[f23229,f15417]) ).
fof(f23332,plain,
! [X0,X1] : join(complement(X0),complement(join(X1,X0))) = join(complement(X0),complement(join(sF3,complement(join(complement(X0),complement(join(X1,X0))))))),
inference(forward_demodulation,[],[f23285,f5840]) ).
fof(f23371,plain,
! [X0,X1] : join(complement(X0),complement(join(X1,X0))) = join(complement(X0),complement(join(sF3,complement(complement(join(X1,X0)))))),
inference(forward_demodulation,[],[f23332,f1403]) ).
fof(f23404,plain,
! [X0,X1] : join(complement(X0),complement(join(X1,X0))) = join(complement(X0),complement(join(join(X1,X0),sF3))),
inference(forward_demodulation,[],[f23371,f1364]) ).
fof(f23423,plain,
! [X0,X1] : join(complement(X0),complement(join(X1,X0))) = join(complement(X0),complement(join(sF3,join(X1,X0)))),
inference(forward_demodulation,[],[f23404,f1]) ).
fof(f23437,plain,
! [X0,X1] : join(complement(X0),complement(join(sF3,X0))) = join(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f23423,f3964]) ).
fof(f23444,plain,
! [X0,X1] : join(complement(X0),complement(sF3)) = join(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f23437,f3962]) ).
fof(f23450,plain,
! [X0,X1] : join(complement(X0),zero) = join(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f23444,f46]) ).
fof(f23454,plain,
! [X0,X1] : join(zero,complement(X0)) = join(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f23450,f1]) ).
fof(f23456,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f23454,f15401]) ).
fof(f23771,plain,
! [X0] : join(X0,X0) = join(X0,complement(join(complement(X0),sF3))),
inference(superposition,[],[f1678,f12545]) ).
fof(f23885,plain,
! [X0] : join(X0,complement(join(sF3,complement(X0)))) = join(X0,X0),
inference(forward_demodulation,[],[f23771,f6912]) ).
fof(f23938,plain,
! [X0] : join(X0,complement(sF3)) = join(X0,X0),
inference(forward_demodulation,[],[f23885,f3962]) ).
fof(f23987,plain,
! [X0] : join(X0,zero) = join(X0,X0),
inference(forward_demodulation,[],[f23938,f46]) ).
fof(f24029,plain,
! [X0] : join(X0,X0) = X0,
inference(forward_demodulation,[],[f23987,f15489]) ).
fof(f26262,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X0,X1)),
inference(superposition,[],[f123,f24029]) ).
fof(f26263,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(superposition,[],[f123,f24029]) ).
fof(f46692,plain,
! [X0,X1] : join(zero,X0) = join(X0,complement(join(complement(X0),X1))),
inference(superposition,[],[f7772,f12545]) ).
fof(f46695,plain,
! [X0] : join(zero,sF5) = join(sF5,complement(join(complement(sF5),X0))),
inference(superposition,[],[f7772,f36]) ).
fof(f46697,plain,
! [X0] : join(zero,sF1) = join(sF1,complement(join(complement(sF1),X0))),
inference(superposition,[],[f7772,f27]) ).
fof(f46702,plain,
! [X0] : join(zero,sF7) = join(sF7,complement(join(complement(sF7),X0))),
inference(superposition,[],[f7772,f40]) ).
fof(f46922,plain,
! [X0] : join(zero,sF7) = join(sF7,complement(join(sF6,X0))),
inference(forward_demodulation,[],[f46702,f12735]) ).
fof(f46927,plain,
! [X0] : join(zero,sF1) = join(sF1,complement(join(sF0,X0))),
inference(forward_demodulation,[],[f46697,f12733]) ).
fof(f46929,plain,
! [X0] : join(zero,sF5) = join(sF5,complement(join(sk1,X0))),
inference(forward_demodulation,[],[f46695,f12731]) ).
fof(f46932,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(forward_demodulation,[],[f46692,f15417]) ).
fof(f47027,plain,
! [X0] : sF7 = join(sF7,complement(join(sF6,X0))),
inference(forward_demodulation,[],[f46922,f15427]) ).
fof(f47032,plain,
! [X0] : sF1 = join(sF1,complement(join(sF0,X0))),
inference(forward_demodulation,[],[f46927,f15422]) ).
fof(f47034,plain,
! [X0] : sF5 = join(sF5,complement(join(sk1,X0))),
inference(forward_demodulation,[],[f46929,f15420]) ).
fof(f51436,plain,
! [X0] : sF7 = join(sF7,complement(join(X0,sF6))),
inference(superposition,[],[f47027,f1]) ).
fof(f52514,plain,
sF1 = join(sF1,sk2),
inference(superposition,[],[f47032,f15456]) ).
fof(f52582,plain,
sF1 = join(sk2,sF1),
inference(forward_demodulation,[],[f52514,f1]) ).
fof(f53101,plain,
converse(sF1) = join(sF6,converse(sF1)),
inference(superposition,[],[f82,f52582]) ).
fof(f53442,plain,
sF7 = join(sF7,complement(converse(sF1))),
inference(superposition,[],[f47027,f53101]) ).
fof(f54134,plain,
sF3 = join(converse(sF1),sF7),
inference(superposition,[],[f5117,f53442]) ).
fof(f54175,plain,
sF3 = join(sF7,converse(sF1)),
inference(forward_demodulation,[],[f54134,f1]) ).
fof(f54647,plain,
converse(sF3) = join(converse(sF7),sF1),
inference(superposition,[],[f85,f54175]) ).
fof(f54693,plain,
converse(sF3) = join(sF1,converse(sF7)),
inference(forward_demodulation,[],[f54647,f1]) ).
fof(f54712,plain,
sF3 = join(sF1,converse(sF7)),
inference(forward_demodulation,[],[f54693,f4148]) ).
fof(f56157,plain,
sF0 = join(complement(sF3),complement(join(sF1,complement(converse(sF7))))),
inference(superposition,[],[f275,f54712]) ).
fof(f56208,plain,
sF0 = join(zero,complement(join(sF1,complement(converse(sF7))))),
inference(forward_demodulation,[],[f56157,f46]) ).
fof(f56230,plain,
sF0 = complement(join(sF1,complement(converse(sF7)))),
inference(forward_demodulation,[],[f56208,f15401]) ).
fof(f64456,plain,
! [X0,X1] : join(X0,join(zero,X1)) = join(zero,complement(join(zero,join(complement(join(X1,X0)),complement(join(X0,join(zero,X1))))))),
inference(superposition,[],[f369,f123]) ).
fof(f64599,plain,
! [X0,X1] : join(X0,join(zero,X1)) = complement(join(complement(join(X1,X0)),complement(join(X0,join(zero,X1))))),
inference(forward_demodulation,[],[f64456,f12827]) ).
fof(f64706,plain,
! [X0,X1] : join(X0,X1) = complement(join(complement(join(X1,X0)),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f64599,f15417]) ).
fof(f70598,plain,
! [X0,X1] : join(complement(join(X0,join(zero,X1))),complement(complement(join(zero,complement(join(X1,X0)))))) = join(complement(join(X0,join(zero,X1))),complement(join(complement(complement(sF3)),complement(join(complement(join(X0,join(zero,X1))),complement(complement(join(zero,complement(join(X1,X0)))))))))),
inference(superposition,[],[f293,f2039]) ).
fof(f70663,plain,
! [X0,X1] : join(complement(join(X0,join(zero,X1))),join(zero,complement(join(X1,X0)))) = join(complement(join(X0,join(zero,X1))),complement(join(complement(complement(sF3)),complement(join(complement(join(X0,join(zero,X1))),join(zero,complement(join(X1,X0)))))))),
inference(forward_demodulation,[],[f70598,f12545]) ).
fof(f71195,plain,
! [X0,X1] : join(complement(join(X1,X0)),join(complement(join(X0,join(zero,X1))),zero)) = join(complement(join(X0,join(zero,X1))),complement(join(complement(complement(sF3)),complement(join(complement(join(X1,X0)),join(complement(join(X0,join(zero,X1))),zero)))))),
inference(forward_demodulation,[],[f70663,f123]) ).
fof(f71720,plain,
! [X0,X1] : join(zero,join(complement(join(X1,X0)),complement(join(X0,join(zero,X1))))) = join(complement(join(X0,join(zero,X1))),complement(join(complement(complement(sF3)),complement(join(zero,join(complement(join(X1,X0)),complement(join(X0,join(zero,X1))))))))),
inference(forward_demodulation,[],[f71195,f123]) ).
fof(f72241,plain,
! [X0,X1] : join(complement(join(X0,join(zero,X1))),complement(join(X1,X0))) = join(complement(join(X0,join(zero,X1))),complement(join(complement(complement(sF3)),complement(join(complement(join(X0,join(zero,X1))),complement(join(X1,X0))))))),
inference(forward_demodulation,[],[f71720,f15479]) ).
fof(f72711,plain,
! [X0,X1] : join(complement(join(X1,X0)),complement(join(X0,join(zero,X1)))) = join(complement(join(X0,join(zero,X1))),complement(join(complement(complement(sF3)),complement(join(complement(join(X1,X0)),complement(join(X0,join(zero,X1)))))))),
inference(forward_demodulation,[],[f72241,f1]) ).
fof(f73137,plain,
! [X0,X1] : join(complement(join(X1,X0)),complement(join(X0,X1))) = join(complement(join(X0,X1)),complement(join(complement(complement(sF3)),complement(join(complement(join(X1,X0)),complement(join(X0,X1))))))),
inference(forward_demodulation,[],[f72711,f15417]) ).
fof(f73514,plain,
! [X0,X1] : join(complement(join(X1,X0)),complement(join(X0,X1))) = join(complement(join(X0,X1)),complement(join(complement(complement(sF3)),join(X0,X1)))),
inference(forward_demodulation,[],[f73137,f64706]) ).
fof(f73759,plain,
! [X0,X1] : complement(join(X0,X1)) = join(complement(join(X1,X0)),complement(join(X0,X1))),
inference(forward_demodulation,[],[f73514,f23456]) ).
fof(f79811,plain,
! [X2,X0,X1] : join(X1,join(X2,X0)) = join(complement(join(zero,complement(X1))),join(X0,join(complement(join(sF3,complement(X1))),X2))),
inference(superposition,[],[f396,f123]) ).
fof(f80056,plain,
! [X2,X0,X1] : join(X1,join(X2,X0)) = join(complement(join(zero,complement(X1))),join(X0,join(complement(sF3),X2))),
inference(forward_demodulation,[],[f79811,f3962]) ).
fof(f80259,plain,
! [X2,X0,X1] : join(X1,join(X2,X0)) = join(complement(sF3),join(complement(join(zero,complement(X1))),join(X0,X2))),
inference(forward_demodulation,[],[f80056,f1870]) ).
fof(f80433,plain,
! [X2,X0,X1] : join(X1,join(X2,X0)) = join(complement(sF3),join(complement(complement(X1)),join(X0,X2))),
inference(forward_demodulation,[],[f80259,f15401]) ).
fof(f80589,plain,
! [X2,X0,X1] : join(X1,join(X2,X0)) = join(complement(sF3),join(X1,join(X0,X2))),
inference(forward_demodulation,[],[f80433,f12545]) ).
fof(f80729,plain,
! [X2,X0,X1] : join(X1,join(X2,X0)) = join(zero,join(X1,join(X0,X2))),
inference(forward_demodulation,[],[f80589,f46]) ).
fof(f80835,plain,
! [X2,X0,X1] : join(X1,join(X0,X2)) = join(X1,join(X2,X0)),
inference(forward_demodulation,[],[f80729,f15417]) ).
fof(f88216,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(join(complement(X1),join(complement(X0),complement(X1)))),join(complement(X0),complement(X0))),
inference(superposition,[],[f266,f7744]) ).
fof(f88281,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),join(complement(join(complement(X1),join(complement(X0),complement(X1)))),complement(X0))),
inference(forward_demodulation,[],[f88216,f123]) ).
fof(f88482,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),join(complement(X0),complement(join(complement(X1),join(complement(X0),complement(X1)))))),
inference(forward_demodulation,[],[f88281,f123]) ).
fof(f88646,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(join(complement(X1),join(complement(X0),complement(X1)))),complement(X0)),
inference(forward_demodulation,[],[f88482,f26262]) ).
fof(f88767,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),complement(join(complement(X1),join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f88646,f1]) ).
fof(f88864,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),complement(join(complement(X0),complement(X1)))),
inference(forward_demodulation,[],[f88767,f26263]) ).
fof(f91941,plain,
! [X2,X0,X1] : join(zero,complement(join(X0,X1))) = join(complement(join(X0,X1)),complement(complement(join(zero,complement(join(X1,complement(join(complement(X0),complement(join(complement(complement(X0)),X2)))))))))),
inference(superposition,[],[f7762,f7066]) ).
fof(f92288,plain,
! [X2,X0,X1] : join(zero,complement(join(X0,X1))) = join(complement(join(X0,X1)),join(zero,complement(join(X1,complement(join(complement(X0),complement(join(complement(complement(X0)),X2)))))))),
inference(forward_demodulation,[],[f91941,f12545]) ).
fof(f92445,plain,
! [X2,X0,X1] : join(zero,complement(join(X0,X1))) = join(zero,join(complement(join(X1,complement(join(complement(X0),complement(join(complement(complement(X0)),X2)))))),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f92288,f123]) ).
fof(f92599,plain,
! [X2,X0,X1] : join(zero,complement(join(X0,X1))) = join(zero,join(complement(join(X0,X1)),complement(join(X1,complement(join(complement(X0),complement(join(complement(complement(X0)),X2)))))))),
inference(forward_demodulation,[],[f92445,f80835]) ).
fof(f92739,plain,
! [X2,X0,X1] : join(zero,complement(join(X0,X1))) = join(complement(join(X1,complement(join(complement(X0),complement(join(complement(complement(X0)),X2)))))),complement(join(X0,X1))),
inference(forward_demodulation,[],[f92599,f15479]) ).
fof(f92867,plain,
! [X2,X0,X1] : join(zero,complement(join(X0,X1))) = join(complement(join(X0,X1)),complement(join(X1,complement(join(complement(X0),complement(join(complement(complement(X0)),X2))))))),
inference(forward_demodulation,[],[f92739,f1]) ).
fof(f92980,plain,
! [X0,X1] : join(zero,complement(join(X0,X1))) = join(complement(join(X0,X1)),complement(join(X1,complement(complement(X0))))),
inference(forward_demodulation,[],[f92867,f46932]) ).
fof(f93059,plain,
! [X0,X1] : join(zero,complement(join(X0,X1))) = join(complement(join(X0,X1)),complement(join(X1,X0))),
inference(forward_demodulation,[],[f92980,f12545]) ).
fof(f93118,plain,
! [X0,X1] : complement(join(X1,X0)) = join(zero,complement(join(X0,X1))),
inference(forward_demodulation,[],[f93059,f73759]) ).
fof(f93164,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f93118,f15401]) ).
fof(f99222,plain,
! [X0] : join(sF5,sF7) = join(sF8,complement(join(X0,sF6))),
inference(superposition,[],[f117,f51436]) ).
fof(f99277,plain,
! [X0] : sF8 = join(sF8,complement(join(X0,sF6))),
inference(forward_demodulation,[],[f99222,f42]) ).
fof(f150860,plain,
complement(sF0) = join(sF1,complement(converse(sF7))),
inference(superposition,[],[f12545,f56230]) ).
fof(f150865,plain,
sF1 = join(sF1,complement(converse(sF7))),
inference(forward_demodulation,[],[f150860,f27]) ).
fof(f151531,plain,
converse(sF7) = join(complement(sF1),complement(join(complement(converse(sF7)),complement(sF1)))),
inference(superposition,[],[f268,f150865]) ).
fof(f151583,plain,
converse(sF7) = join(complement(sF1),complement(join(complement(sF1),complement(converse(sF7))))),
inference(forward_demodulation,[],[f151531,f93164]) ).
fof(f151603,plain,
converse(sF7) = join(converse(sF7),complement(sF1)),
inference(forward_demodulation,[],[f151583,f88864]) ).
fof(f151615,plain,
converse(sF7) = join(complement(sF1),converse(sF7)),
inference(forward_demodulation,[],[f151603,f1]) ).
fof(f151619,plain,
converse(sF7) = join(sF0,converse(sF7)),
inference(forward_demodulation,[],[f151615,f12733]) ).
fof(f151907,plain,
converse(converse(sF7)) = join(sk1,converse(converse(sF7))),
inference(superposition,[],[f83,f151619]) ).
fof(f151971,plain,
sF7 = join(sk1,sF7),
inference(forward_demodulation,[],[f151907,f10]) ).
fof(f152292,plain,
sF5 = join(sF5,complement(sF7)),
inference(superposition,[],[f47034,f151971]) ).
fof(f152358,plain,
sF5 = join(sF5,sF6),
inference(forward_demodulation,[],[f152292,f12735]) ).
fof(f152674,plain,
sF8 = join(sF8,complement(sF5)),
inference(superposition,[],[f99277,f152358]) ).
fof(f152730,plain,
sF3 = sF8,
inference(forward_demodulation,[],[f152674,f5500]) ).
fof(f153053,plain,
complement(sF3) = sF9,
inference(superposition,[],[f44,f152730]) ).
fof(f153159,plain,
zero = sF9,
inference(forward_demodulation,[],[f153053,f46]) ).
fof(f153180,plain,
$false,
inference(forward_subsumption_resolution,[],[f153159,f45]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL006-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.39 % Computer : n008.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 22:50:25 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.42 Running first-order model finding
% 0.13/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.42/2.61 % (1691235)Will run a generic schedule for satisfiability detection.
% 15.42/2.61 % (1691241)% WARNING: option uhcvi not known.
% 15.42/2.61 % (1691241)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1315823122:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.42/2.61 % (1691240)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2390454529_2999 on theBenchmark for (2999ds/0Mi)
% 15.42/2.61 % (1691243)dis+10_1_sil=32000:sp=arity:random_seed=994440255:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.42/2.61 % (1691242)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1694054745:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.42/2.61 % (1691244)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1568700983:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.42/2.61 % (1691246)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=82719507:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.42/2.61 % (1691245)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2679607803:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.42/2.61 % TRYING [1]
% 15.42/2.61 % TRYING [2]
% 15.42/2.61 % TRYING [3]
% 15.42/2.61 % TRYING [4]
% 15.42/2.61 % (1691243)Instruction limit reached!
% 15.42/2.61 % (1691243)------------------------------
% 15.42/2.61 % (1691243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/2.61 % (1691243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/2.61 % (1691243)CaDiCaL version: 2.1.3
% 15.42/2.61 % (1691243)Termination reason: Instruction limit
% 15.42/2.61 % (1691243)Termination phase: Saturation
% 15.42/2.61 % (1691243)Time elapsed: 0.058 s
% 15.42/2.61 % (1691243)Peak memory usage: 12 MB
% 15.42/2.61 % (1691243)Instructions burned: 104 (million)
% 15.42/2.61 % TRYING [5]
% 15.42/2.61 % (1691244)Instruction limit reached!
% 15.42/2.61 % (1691244)------------------------------
% 15.42/2.61 % (1691244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/2.61 % (1691244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/2.61 % (1691244)CaDiCaL version: 2.1.3
% 15.42/2.61 % (1691244)Termination reason: Instruction limit
% 15.42/2.61 % (1691244)Termination phase: Saturation
% 15.42/2.61 % (1691244)Time elapsed: 0.070 s
% 15.42/2.61 % (1691244)Peak memory usage: 12 MB
% 15.42/2.61 % (1691244)Instructions burned: 117 (million)
% 15.42/2.61 % (1691254)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2668194833:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.42/2.61 % (1691245)Instruction limit reached!
% 15.42/2.61 % (1691245)------------------------------
% 15.42/2.61 % (1691245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/2.61 % (1691245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/2.61 % (1691245)CaDiCaL version: 2.1.3
% 15.42/2.61 % (1691245)Termination reason: Instruction limit
% 15.42/2.61 % (1691245)Termination phase: Saturation
% 15.42/2.61 % (1691245)Time elapsed: 0.079 s
% 15.42/2.61 % (1691245)Peak memory usage: 12 MB
% 15.42/2.61 % (1691245)Instructions burned: 136 (million)
% 15.42/2.61 % TRYING [1]
% 15.42/2.61 % TRYING [2]
% 15.42/2.61 % TRYING [3]
% 15.42/2.61 % (1691255)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1172419197:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 15.42/2.61 % TRYING [4]
% 15.42/2.61 % (1691246)Instruction limit reached!
% 15.42/2.61 % (1691246)------------------------------
% 15.42/2.61 % (1691246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/2.61 % (1691246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/2.61 % (1691246)CaDiCaL version: 2.1.3
% 15.42/2.61 % (1691246)Termination reason: Instruction limit
% 15.42/2.61 % (1691246)Termination phase: Saturation
% 15.42/2.61 % (1691246)Time elapsed: 0.096 s
% 15.42/2.61 % (1691246)Peak memory usage: 13 MB
% 15.42/2.61 % (1691246)Instructions burned: 159 (million)
% 15.42/2.61 % (1691257)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3274712296:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.42/2.61 % (1691259)ott-21_1_sil=16000:fs=off:random_seed=865030477:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.42/2.61 % TRYING [5]
% 15.42/2.61 % (1691255)Instruction limit reached!
% 15.42/2.61 % (1691255)------------------------------
% 15.42/2.61 % (1691255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.05/7.27 % (1691255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.05/7.27 % (1691255)CaDiCaL version: 2.1.3
% 48.05/7.27 % (1691255)Termination reason: Instruction limit
% 48.05/7.27 % (1691255)Termination phase: Saturation
% 48.05/7.27 % (1691255)Time elapsed: 0.085 s
% 48.05/7.27 % (1691255)Peak memory usage: 12 MB
% 48.05/7.27 % (1691255)Instructions burned: 132 (million)
% 48.05/7.27 % (1691262)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=405719036:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 48.05/7.27 % (1691259)Instruction limit reached!
% 48.05/7.27 % (1691259)------------------------------
% 48.05/7.27 % (1691259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.05/7.27 % (1691259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.05/7.27 % (1691259)CaDiCaL version: 2.1.3
% 48.05/7.27 % (1691259)Termination reason: Instruction limit
% 48.05/7.27 % (1691259)Termination phase: Saturation
% 48.05/7.27 % (1691259)Time elapsed: 0.083 s
% 48.05/7.27 % (1691259)Peak memory usage: 12 MB
% 48.05/7.27 % (1691259)Instructions burned: 181 (million)
% 48.05/7.27 % (1691264)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2078335334:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 48.05/7.27 % TRYING [1]
% 48.05/7.27 % TRYING [2]
% 48.05/7.27 % TRYING [3]
% 48.05/7.27 % TRYING [4]
% 48.05/7.27 % TRYING [6]
% 48.05/7.27 % TRYING [5]
% 48.05/7.27 % TRYING [6]
% 48.05/7.27 % (1691254)Instruction limit reached!
% 48.05/7.27 % (1691254)------------------------------
% 48.05/7.27 % (1691254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.05/7.27 % (1691254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.05/7.27 % (1691254)CaDiCaL version: 2.1.3
% 48.05/7.27 % (1691254)Termination reason: Instruction limit
% 48.05/7.27 % (1691254)Termination phase: Finite model building constraint generation
% 48.05/7.27 % (1691254)Time elapsed: 0.348 s
% 48.05/7.27 % (1691254)Peak memory usage: 24 MB
% 48.05/7.27 % (1691254)Instructions burned: 716 (million)
% 48.05/7.27 % (1691257)Instruction limit reached!
% 48.05/7.27 % (1691257)------------------------------
% 48.05/7.27 % (1691257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.05/7.27 % (1691257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.05/7.27 % (1691257)CaDiCaL version: 2.1.3
% 48.05/7.27 % (1691257)Termination reason: Instruction limit
% 48.05/7.27 % (1691257)Termination phase: Saturation
% 48.05/7.27 % (1691257)Time elapsed: 0.344 s
% 48.05/7.27 % (1691257)Peak memory usage: 16 MB
% 48.05/7.27 % (1691257)Instructions burned: 684 (million)
% 48.05/7.27 % (1691266)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1068264664:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 48.05/7.27 % TRYING [6]
% 48.05/7.27 % (1691262)Instruction limit reached!
% 48.05/7.27 % (1691262)------------------------------
% 48.05/7.27 % (1691262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.05/7.27 % (1691262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.05/7.27 % (1691262)CaDiCaL version: 2.1.3
% 48.05/7.27 % (1691262)Termination reason: Instruction limit
% 48.05/7.27 % (1691262)Termination phase: Saturation
% 48.05/7.27 % (1691262)Time elapsed: 0.264 s
% 48.05/7.27 % (1691262)Peak memory usage: 15 MB
% 48.05/7.27 % (1691262)Instructions burned: 478 (million)
% 48.05/7.27 % (1691267)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3503690408:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 48.05/7.27 % (1691269)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=510888659:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 48.05/7.27 % (1691264)Instruction limit reached!
% 48.05/7.27 % (1691264)------------------------------
% 48.05/7.27 % (1691264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.05/7.27 % (1691264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.05/7.27 % (1691264)CaDiCaL version: 2.1.3
% 48.05/7.27 % (1691264)Termination reason: Instruction limit
% 48.05/7.27 % (1691264)Termination phase: Finite model building SAT solving
% 48.05/7.27 % (1691264)Time elapsed: 0.342 s
% 48.05/7.27 % (1691264)Peak memory usage: 22 MB
% 48.05/7.27 % (1691264)Instructions burned: 866 (million)
% 48.05/7.27 % TRYING [14]
% 48.05/7.27 % (1691272)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2739076804:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 48.05/7.27 % (1691267)Instruction limit reached!
% 20.23/7.60 % (1691267)------------------------------
% 20.23/7.60 % (1691267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.23/7.60 % (1691267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.23/7.60 % (1691267)CaDiCaL version: 2.1.3
% 20.23/7.60 % (1691267)Termination reason: Instruction limit
% 20.23/7.60 % (1691267)Termination phase: Finite model building constraint generation
% 20.23/7.60 % (1691267)Time elapsed: 0.336 s
% 20.23/7.60 % (1691267)Peak memory usage: 82 MB
% 20.23/7.60 % (1691267)Instructions burned: 890 (million)
% 20.23/7.60 % (1691274)fmb+10_1_sil=64000:random_seed=801036076:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 20.23/7.60 % TRYING [1]
% 20.23/7.60 % TRYING [2]
% 20.23/7.60 % TRYING [3]
% 20.23/7.60 % TRYING [4]
% 20.23/7.60 % (1691269)Instruction limit reached!
% 20.23/7.60 % (1691269)------------------------------
% 20.23/7.60 % (1691269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.23/7.60 % (1691269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.23/7.60 % (1691269)CaDiCaL version: 2.1.3
% 20.23/7.60 % (1691269)Termination reason: Instruction limit
% 20.23/7.60 % (1691269)Termination phase: Saturation
% 20.23/7.60 % (1691269)Time elapsed: 0.386 s
% 20.23/7.60 % (1691269)Peak memory usage: 16 MB
% 20.23/7.60 % (1691269)Instructions burned: 692 (million)
% 20.23/7.60 % (1691276)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2452840369:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 20.23/7.60 % TRYING [20]
% 20.23/7.60 % TRYING [5]
% 20.23/7.60 % TRYING [7]
% 20.23/7.60 % (1691272)Instruction limit reached!
% 20.23/7.60 % (1691272)------------------------------
% 20.23/7.60 % (1691272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.23/7.60 % (1691272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.23/7.60 % (1691272)CaDiCaL version: 2.1.3
% 20.23/7.60 % (1691272)Termination reason: Instruction limit
% 20.23/7.60 % (1691272)Termination phase: Saturation
% 20.23/7.60 % (1691272)Time elapsed: 0.459 s
% 20.23/7.60 % (1691272)Peak memory usage: 18 MB
% 20.23/7.60 % (1691272)Instructions burned: 879 (million)
% 20.23/7.60 % (1691278)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1439800428:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 20.23/7.60 % TRYING [6]
% 20.23/7.60 % TRYING [8]
% 20.23/7.60 % (1691266)Instruction limit reached!
% 20.23/7.60 % (1691266)------------------------------
% 20.23/7.60 % (1691266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.23/7.60 % (1691266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.23/7.60 % (1691266)CaDiCaL version: 2.1.3
% 20.23/7.60 % (1691266)Termination reason: Instruction limit
% 20.23/7.60 % (1691266)Termination phase: Saturation
% 20.23/7.60 % (1691266)Time elapsed: 0.638 s
% 20.23/7.60 % (1691266)Peak memory usage: 20 MB
% 20.23/7.60 % (1691266)Instructions burned: 1180 (million)
% 20.23/7.60 % (1691280)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2330720540:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 20.23/7.60 % (1691278)Instruction limit reached!
% 20.23/7.60 % (1691278)------------------------------
% 20.23/7.60 % (1691278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.23/7.60 % (1691278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.23/7.60 % (1691278)CaDiCaL version: 2.1.3
% 20.23/7.60 % (1691278)Termination reason: Instruction limit
% 20.23/7.60 % (1691278)Termination phase: Finite model building SAT solving
% 20.23/7.60 % (1691278)Time elapsed: 0.369 s
% 20.23/7.60 % (1691278)Peak memory usage: 65 MB
% 20.23/7.60 % (1691278)Instructions burned: 922 (million)
% 20.23/7.60 % (1691282)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3008600364:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 20.23/7.60 % TRYING [7]
% 20.23/7.60 % (1691282)Instruction limit reached!
% 20.23/7.60 % (1691282)------------------------------
% 20.23/7.60 % (1691282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.23/7.60 % (1691282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.23/7.60 % (1691282)CaDiCaL version: 2.1.3
% 20.23/7.60 % (1691282)Termination reason: Instruction limit
% 20.23/7.60 % (1691282)Termination phase: Saturation
% 20.23/7.60 % (1691282)Time elapsed: 0.676 s
% 20.23/7.60 % (1691282)Peak memory usage: 24 MB
% 20.23/7.60 % (1691282)Instructions burned: 1472 (million)
% 20.23/7.60 % (1691285)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2519432460:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 20.23/7.60 % TRYING [77]
% 20.23/7.60 % TRYING [8]
% 20.23/7.60 % (1691280)Instruction limit reached!
% 20.23/7.60 % (1691280)------------------------------
% 20.23/7.60 % (1691280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.23/7.60 % (1691280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.23/7.60 % (1691280)CaDiCaL version: 2.1.3
% 20.23/7.60 % (1691280)Termination reason: Instruction limit
% 20.23/7.60 % (1691280)Termination phase: Saturation
% 20.23/7.60 % (1691280)Time elapsed: 2.730 s
% 20.23/7.60 % (1691280)Peak memory usage: 47 MB
% 20.23/7.60 % (1691280)Instructions burned: 5132 (million)
% 20.23/7.60 % (1691287)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2252184643:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 20.23/7.60 % TRYING [16]
% 20.23/7.60 % (1691276)Instruction limit reached!
% 20.23/7.60 % (1691276)------------------------------
% 20.23/7.60 % (1691276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.23/7.60 % (1691276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.23/7.60 % (1691276)CaDiCaL version: 2.1.3
% 20.23/7.60 % (1691276)Termination reason: Instruction limit
% 20.23/7.60 % (1691276)Termination phase: Finite model building constraint generation
% 20.23/7.60 % (1691276)Time elapsed: 3.449 s
% 20.23/7.60 % (1691276)Peak memory usage: 671 MB
% 20.23/7.60 % (1691276)Instructions burned: 9518 (million)
% 20.23/7.60 % (1691289)ott-2_1_sil=16000:newcnf=on:random_seed=2199678938:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2955 on theBenchmark for (2955ds/869Mi)
% 20.23/7.60 % (1691285)Instruction limit reached!
% 20.23/7.60 % (1691285)------------------------------
% 20.23/7.60 % (1691285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.23/7.60 % (1691285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.23/7.60 % (1691285)CaDiCaL version: 2.1.3
% 20.23/7.60 % (1691285)Termination reason: Instruction limit
% 20.23/7.60 % (1691285)Termination phase: Finite model building constraint generation
% 20.23/7.60 % (1691285)Time elapsed: 2.345 s
% 20.23/7.60 % (1691285)Peak memory usage: 515 MB
% 20.23/7.60 % (1691285)Instructions burned: 6326 (million)
% 20.23/7.60 % (1691291)ott+10_1_sil=32000:tgt=ground:random_seed=232292589:i=5114:av=off_2954 on theBenchmark for (2954ds/5114Mi)
% 20.23/7.60 % (1691287)Instruction limit reached!
% 20.23/7.60 % (1691287)------------------------------
% 20.23/7.60 % (1691287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.23/7.60 % (1691287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.23/7.60 % (1691287)CaDiCaL version: 2.1.3
% 20.23/7.60 % (1691287)Termination reason: Instruction limit
% 20.23/7.60 % (1691287)Termination phase: Finite model building constraint generation
% 20.23/7.60 % (1691287)Time elapsed: 0.731 s
% 20.23/7.60 % (1691287)Peak memory usage: 135 MB
% 20.23/7.60 % (1691287)Instructions burned: 2174 (million)
% 20.23/7.60 % TRYING [8]
% 20.23/7.60 % (1691293)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4077942737:i=54282_2953 on theBenchmark for (2953ds/54282Mi)
% 20.23/7.60 % TRYING [1]
% 20.23/7.60 % TRYING [2]
% 20.23/7.60 % TRYING [3]
% 20.23/7.60 % TRYING [4]
% 20.23/7.60 % TRYING [5]
% 20.23/7.60 % TRYING [6]
% 20.23/7.60 % (1691289)Instruction limit reached!
% 20.23/7.60 % (1691289)------------------------------
% 20.23/7.60 % (1691289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.23/7.60 % (1691289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.23/7.60 % (1691289)CaDiCaL version: 2.1.3
% 20.23/7.60 % (1691289)Termination reason: Instruction limit
% 20.23/7.60 % (1691289)Termination phase: Saturation
% 20.23/7.60 % (1691289)Time elapsed: 0.486 s
% 20.23/7.60 % (1691289)Peak memory usage: 18 MB
% 20.23/7.60 % (1691289)Instructions burned: 870 (million)
% 20.23/7.60 % (1691295)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1790594266:i=3512:aac=none_2950 on theBenchmark for (2950ds/3512Mi)
% 20.23/7.60 % TRYING [7]
% 20.23/7.60 % (1691295)Instruction limit reached!
% 20.23/7.60 % (1691295)------------------------------
% 20.23/7.60 % (1691295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.23/7.60 % (1691295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.23/7.60 % (1691295)CaDiCaL version: 2.1.3
% 20.23/7.60 % (1691295)Termination reason: Instruction limit
% 20.23/7.60 % (1691295)Termination phase: Saturation
% 20.23/7.60 % (1691295)Time elapsed: 1.849 s
% 20.23/7.60 % (1691295)Peak memory usage: 40 MB
% 20.23/7.60 % (1691295)Instructions burned: 3512 (million)
% 20.23/7.60 % (1691297)dis+21_1_sil=32000:sas=cadical:random_seed=1516631597:i=3773:amm=off_2931 on theBenchmark for (2931ds/3773Mi)
% 20.23/7.60 % (1691291) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1691235-1691291"...
% 20.23/7.60 % (1691291)...printing done.
% 20.23/7.60 % (1691291)Refutation found. Thanks to Tanya!
% 20.23/7.60 % SZS status Unsatisfiable for theBenchmark
% 20.23/7.60 % SZS output start Proof for theBenchmark
% See solution above
% 20.23/7.61 % (1691291)------------------------------
% 20.23/7.61 % (1691291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.23/7.61 % (1691291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.23/7.61 % (1691291)CaDiCaL version: 2.1.3
% 20.23/7.61 % (1691291)Termination reason: Refutation
% 20.23/7.61 % (1691291)Time elapsed: 2.546 s
% 20.23/7.61 % (1691291)Peak memory usage: 47 MB
% 20.23/7.61 % (1691291)Instructions burned: 4506 (million)
% 20.23/7.61 % (1691235)Success in time 7.176 s
% 20.23/7.61 % Vampire exiting
%------------------------------------------------------------------------------