%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : REL030-3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:57 PM UTC 2026
% Result : Unsatisfiable 10.85s 2.17s
% Output : Refutation 11.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 55
% Number of leaves : 26
% Syntax : Number of formulae : 282 ( 282 unt; 12 def)
% Number of atoms : 282 ( 281 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 18 con; 0-2 aty)
% Number of variables : 212 ( 212 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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(f8,negated_conjecture,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',composition_distributivity_7) ).
fof(f10,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_idempotence_8) ).
fof(f11,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_additivity_9) ).
fof(f12,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox2/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/sandbox2/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,negated_conjecture,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_top_12) ).
fof(f16,negated_conjecture,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_zero_13) ).
fof(f23,negated_conjecture,
join(sk1,one) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_17) ).
fof(f24,plain,
one = join(sk1,one),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
meet(composition(sk1,sk2),complement(sk3)) != meet(composition(sk1,sk2),complement(composition(sk1,sk3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_18) ).
fof(f26,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f16,f6]) ).
fof(f30,plain,
complement(join(complement(composition(sk1,sk2)),complement(complement(sk3)))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),
inference(definition_unfolding,[],[f25,f6,f6]) ).
fof(f31,definition,
sF0 = join(sk1,one),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f32,plain,
join(sk1,one) = sF0,
inference(reorient_equations,[],[f31]) ).
fof(f33,plain,
one = sF0,
inference(definition_folding,[],[f24,f32]) ).
fof(f34,definition,
sF1 = composition(sk1,sk2),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f35,plain,
composition(sk1,sk2) = sF1,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF2 = complement(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f37,plain,
complement(sF1) = sF2,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF3 = complement(sk3),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f39,plain,
complement(sk3) = sF3,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF4 = complement(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f41,plain,
complement(sF3) = sF4,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF5 = join(sF2,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f43,plain,
join(sF2,sF4) = sF5,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF6 = complement(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f45,plain,
complement(sF5) = sF6,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF7 = composition(sk1,sk3),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f47,plain,
composition(sk1,sk3) = sF7,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF8 = complement(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f49,plain,
complement(sF7) = sF8,
inference(reorient_equations,[],[f48]) ).
fof(f50,definition,
sF9 = complement(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f51,plain,
complement(sF8) = sF9,
inference(reorient_equations,[],[f50]) ).
fof(f52,definition,
sF10 = join(sF2,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f53,plain,
join(sF2,sF9) = sF10,
inference(reorient_equations,[],[f52]) ).
fof(f54,definition,
sF11 = complement(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f55,plain,
complement(sF10) = sF11,
inference(reorient_equations,[],[f54]) ).
fof(f56,plain,
sF6 != sF11,
inference(definition_folding,[],[f30,f55,f53,f51,f49,f47,f37,f35,f45,f43,f41,f39,f37,f35]) ).
fof(f57,plain,
zero = complement(top),
inference(backward_demodulation,[],[f26,f15]) ).
fof(f58,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(backward_demodulation,[],[f4,f1]) ).
fof(f61,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(converse(X0),complement(composition(X0,X1)))),
inference(backward_demodulation,[],[f14,f1]) ).
fof(f62,plain,
one = join(sk1,one),
inference(forward_demodulation,[],[f32,f33]) ).
fof(f63,plain,
one = join(one,sk1),
inference(forward_demodulation,[],[f62,f1]) ).
fof(f119,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(complement(complement(X0)))))) = X0,
inference(superposition,[],[f58,f15]) ).
fof(f120,plain,
! [X0] : join(zero,complement(join(complement(X0),complement(complement(complement(X0)))))) = X0,
inference(forward_demodulation,[],[f119,f57]) ).
fof(f141,plain,
! [X0,X1] : join(complement(join(complement(X1),X0)),complement(join(complement(X0),complement(X1)))) = X1,
inference(superposition,[],[f58,f1]) ).
fof(f158,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(X0,complement(composition(converse(X0),X1)))),
inference(superposition,[],[f61,f10]) ).
fof(f160,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(superposition,[],[f2,f1]) ).
fof(f163,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f2,f15]) ).
fof(f168,plain,
! [X0] : join(sF2,join(sF4,X0)) = join(sF5,X0),
inference(superposition,[],[f2,f43]) ).
fof(f169,plain,
! [X0] : join(sF2,join(sF9,X0)) = join(sF10,X0),
inference(superposition,[],[f2,f53]) ).
fof(f175,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f258,plain,
! [X0,X1] : composition(converse(X1),X0) = converse(composition(converse(X0),X1)),
inference(superposition,[],[f12,f10]) ).
fof(f260,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(f267,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = join(converse(composition(X0,X2)),converse(composition(X0,X1))),
inference(superposition,[],[f260,f12]) ).
fof(f273,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = converse(join(composition(X0,X2),composition(X0,X1))),
inference(forward_demodulation,[],[f267,f11]) ).
fof(f276,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = composition(converse(join(X2,X1)),converse(X0)),
inference(forward_demodulation,[],[f273,f11]) ).
fof(f278,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = converse(composition(X0,join(X2,X1))),
inference(forward_demodulation,[],[f276,f12]) ).
fof(f289,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X0,X2)) = converse(converse(composition(X0,join(X1,X2)))),
inference(superposition,[],[f10,f278]) ).
fof(f300,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = join(composition(X0,X1),composition(X0,X2)),
inference(forward_demodulation,[],[f289,f10]) ).
fof(f318,plain,
! [X0] : composition(sk1,join(sk3,X0)) = join(sF7,composition(sk1,X0)),
inference(superposition,[],[f300,f47]) ).
fof(f320,plain,
! [X0] : composition(sk1,join(X0,sk2)) = join(composition(sk1,X0),sF1),
inference(superposition,[],[f300,f35]) ).
fof(f321,plain,
! [X0] : composition(sk1,join(X0,sk3)) = join(composition(sk1,X0),sF7),
inference(superposition,[],[f300,f47]) ).
fof(f330,plain,
! [X0] : join(sF7,composition(sk1,X0)) = composition(sk1,join(X0,sk3)),
inference(forward_demodulation,[],[f321,f1]) ).
fof(f331,plain,
! [X0] : join(sF1,composition(sk1,X0)) = composition(sk1,join(X0,sk2)),
inference(forward_demodulation,[],[f320,f1]) ).
fof(f534,plain,
! [X0] : complement(X0) = join(complement(join(complement(complement(X0)),X0)),complement(top)),
inference(superposition,[],[f141,f15]) ).
fof(f550,plain,
! [X0] : complement(X0) = join(complement(top),complement(join(complement(complement(X0)),X0))),
inference(forward_demodulation,[],[f534,f1]) ).
fof(f577,plain,
! [X0] : complement(X0) = join(complement(top),complement(join(X0,complement(complement(X0))))),
inference(forward_demodulation,[],[f550,f1]) ).
fof(f591,plain,
! [X0] : complement(X0) = join(zero,complement(join(X0,complement(complement(X0))))),
inference(forward_demodulation,[],[f577,f57]) ).
fof(f601,plain,
! [X0] : complement(complement(X0)) = X0,
inference(backward_demodulation,[],[f120,f591]) ).
fof(f612,plain,
! [X0] : complement(X0) = join(zero,complement(join(X0,X0))),
inference(backward_demodulation,[],[f591,f601]) ).
fof(f625,plain,
! [X0,X1] : complement(join(X1,X0)) = join(zero,complement(join(X0,join(join(X1,X0),X1)))),
inference(superposition,[],[f612,f175]) ).
fof(f634,plain,
! [X0,X1] : complement(join(X1,X0)) = join(zero,complement(join(X0,join(X1,join(X0,X1))))),
inference(forward_demodulation,[],[f625,f2]) ).
fof(f636,plain,
sk3 = complement(sF3),
inference(superposition,[],[f601,f39]) ).
fof(f637,plain,
sF1 = complement(sF2),
inference(superposition,[],[f601,f37]) ).
fof(f638,plain,
sF3 = complement(sF4),
inference(superposition,[],[f601,f41]) ).
fof(f639,plain,
sF5 = complement(sF6),
inference(superposition,[],[f601,f45]) ).
fof(f640,plain,
sF7 = complement(sF8),
inference(superposition,[],[f601,f49]) ).
fof(f642,plain,
sF10 = complement(sF11),
inference(superposition,[],[f601,f55]) ).
fof(f644,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(X0,complement(X1)))),
inference(superposition,[],[f58,f601]) ).
fof(f648,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(complement(X1),X0))),
inference(superposition,[],[f141,f601]) ).
fof(f675,plain,
sF7 = sF9,
inference(backward_demodulation,[],[f51,f640]) ).
fof(f676,plain,
sk3 = sF4,
inference(forward_demodulation,[],[f636,f41]) ).
fof(f681,plain,
sF10 = join(sF2,sF7),
inference(backward_demodulation,[],[f53,f675]) ).
fof(f685,plain,
! [X0] : join(sF10,X0) = join(sF2,join(sF7,X0)),
inference(backward_demodulation,[],[f169,f675]) ).
fof(f690,plain,
sF7 = composition(sk1,sF4),
inference(backward_demodulation,[],[f47,f676]) ).
fof(f698,plain,
! [X0] : join(sF7,composition(sk1,X0)) = composition(sk1,join(sF4,X0)),
inference(backward_demodulation,[],[f318,f676]) ).
fof(f699,plain,
! [X0] : join(sF7,composition(sk1,X0)) = composition(sk1,join(X0,sF4)),
inference(backward_demodulation,[],[f330,f676]) ).
fof(f716,plain,
! [X0,X1] : complement(X1) = join(complement(join(X0,X1)),complement(join(X1,complement(X0)))),
inference(superposition,[],[f644,f1]) ).
fof(f789,plain,
! [X0,X1] : complement(X1) = join(complement(join(X0,X1)),complement(join(complement(X0),X1))),
inference(superposition,[],[f648,f1]) ).
fof(f826,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(complement(complement(X0)),complement(join(complement(join(X0,X1)),complement(complement(join(complement(X1),X0)))))),
inference(superposition,[],[f644,f648]) ).
fof(f827,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(complement(complement(X0)),complement(join(complement(join(X0,X1)),join(complement(X1),X0)))),
inference(forward_demodulation,[],[f826,f601]) ).
fof(f852,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(complement(complement(X0)),complement(join(X0,join(complement(join(X0,X1)),complement(X1))))),
inference(forward_demodulation,[],[f827,f175]) ).
fof(f866,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(complement(complement(X0)),complement(join(X0,join(complement(X1),complement(join(X0,X1)))))),
inference(forward_demodulation,[],[f852,f1]) ).
fof(f878,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(X0,complement(join(X0,join(complement(X1),complement(join(X0,X1)))))),
inference(forward_demodulation,[],[f866,f601]) ).
fof(f888,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,join(complement(X1),complement(join(X0,X1)))))),
inference(forward_demodulation,[],[f878,f601]) ).
fof(f897,plain,
! [X0] : join(sF10,X0) = join(sF2,join(X0,sF7)),
inference(superposition,[],[f685,f1]) ).
fof(f982,plain,
! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(complement(join(complement(join(X0,complement(X1))),join(X1,X0))),complement(complement(X0))),
inference(superposition,[],[f648,f716]) ).
fof(f994,plain,
! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(complement(complement(X0)),complement(join(complement(join(X0,complement(X1))),join(X1,X0)))),
inference(forward_demodulation,[],[f982,f1]) ).
fof(f1017,plain,
! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(complement(complement(X0)),complement(join(join(X1,X0),complement(join(X0,complement(X1)))))),
inference(forward_demodulation,[],[f994,f1]) ).
fof(f1034,plain,
! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(complement(complement(X0)),complement(join(X1,join(X0,complement(join(X0,complement(X1))))))),
inference(forward_demodulation,[],[f1017,f2]) ).
fof(f1049,plain,
! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(X0,complement(join(X1,join(X0,complement(join(X0,complement(X1))))))),
inference(forward_demodulation,[],[f1034,f601]) ).
fof(f1063,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X1,join(X0,complement(join(X0,complement(X1))))))),
inference(forward_demodulation,[],[f1049,f601]) ).
fof(f1084,plain,
! [X0,X1] : join(top,X1) = join(complement(X0),join(X0,X1)),
inference(superposition,[],[f160,f15]) ).
fof(f1135,plain,
! [X0,X1] : join(top,X1) = join(X0,join(X1,complement(X0))),
inference(forward_demodulation,[],[f1084,f175]) ).
fof(f1192,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f258,f8]) ).
fof(f1210,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f1192,f10]) ).
fof(f1229,plain,
! [X0] : complement(X0) = join(complement(X0),composition(one,complement(X0))),
inference(superposition,[],[f158,f1210]) ).
fof(f1232,plain,
! [X0,X1] : join(X0,composition(X1,X0)) = composition(join(converse(one),X1),X0),
inference(superposition,[],[f9,f1210]) ).
fof(f1239,plain,
one = converse(one),
inference(superposition,[],[f8,f1210]) ).
fof(f1244,plain,
! [X0] : composition(one,X0) = X0,
inference(backward_demodulation,[],[f1210,f1239]) ).
fof(f1252,plain,
! [X0,X1] : join(X0,composition(X1,X0)) = composition(join(one,X1),X0),
inference(forward_demodulation,[],[f1232,f1239]) ).
fof(f1257,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(backward_demodulation,[],[f1229,f1244]) ).
fof(f1292,plain,
! [X0] : join(X0,X0) = X0,
inference(superposition,[],[f1257,f601]) ).
fof(f1303,plain,
! [X0] : complement(complement(X0)) = join(zero,complement(complement(X0))),
inference(superposition,[],[f612,f1257]) ).
fof(f1314,plain,
! [X0] : join(zero,X0) = X0,
inference(forward_demodulation,[],[f1303,f601]) ).
fof(f1339,plain,
! [X0,X1] : complement(join(X1,X0)) = complement(join(X0,join(X1,join(X0,X1)))),
inference(backward_demodulation,[],[f634,f1314]) ).
fof(f1380,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f1,f1314]) ).
fof(f1429,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X0,X1)),
inference(superposition,[],[f175,f1292]) ).
fof(f1430,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(superposition,[],[f175,f1292]) ).
fof(f1440,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,join(X0,X1))),
inference(superposition,[],[f2,f1292]) ).
fof(f1450,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(backward_demodulation,[],[f1339,f1440]) ).
fof(f1535,plain,
! [X0] : composition(one,X0) = join(X0,composition(sk1,X0)),
inference(superposition,[],[f1252,f63]) ).
fof(f1567,plain,
! [X0] : join(X0,composition(sk1,X0)) = X0,
inference(forward_demodulation,[],[f1535,f1244]) ).
fof(f1589,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(composition(sk1,X0),X1)),
inference(superposition,[],[f2,f1567]) ).
fof(f1590,plain,
! [X0,X1] : join(X0,X1) = join(composition(sk1,X0),join(X0,X1)),
inference(superposition,[],[f160,f1567]) ).
fof(f1591,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(composition(sk1,X0),X1)),
inference(superposition,[],[f175,f1567]) ).
fof(f1598,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(complement(join(composition(sk1,complement(X0)),X0)),complement(complement(X0))),
inference(superposition,[],[f648,f1567]) ).
fof(f1607,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(complement(complement(X0)),complement(join(composition(sk1,complement(X0)),X0))),
inference(forward_demodulation,[],[f1598,f1]) ).
fof(f1613,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,composition(sk1,X0))),
inference(forward_demodulation,[],[f1590,f175]) ).
fof(f1622,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(complement(complement(X0)),complement(join(X0,composition(sk1,complement(X0))))),
inference(forward_demodulation,[],[f1607,f1450]) ).
fof(f1628,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(X0,complement(join(X0,composition(sk1,complement(X0))))),
inference(forward_demodulation,[],[f1622,f601]) ).
fof(f1641,plain,
! [X0,X1] : join(X0,composition(sk1,join(X0,X1))) = join(X0,composition(sk1,X1)),
inference(superposition,[],[f1589,f300]) ).
fof(f1714,plain,
! [X0,X1] : join(X0,composition(sk1,join(X0,X1))) = join(composition(sk1,X1),X0),
inference(superposition,[],[f1591,f300]) ).
fof(f1801,plain,
! [X0,X1] : join(X1,composition(sk1,join(X0,X1))) = join(composition(sk1,X0),X1),
inference(superposition,[],[f1714,f1]) ).
fof(f1812,plain,
! [X0] : join(composition(sk1,complement(X0)),X0) = join(X0,composition(sk1,top)),
inference(superposition,[],[f1714,f15]) ).
fof(f1826,plain,
join(composition(sk1,sF4),sF2) = join(sF2,composition(sk1,sF5)),
inference(superposition,[],[f1714,f43]) ).
fof(f1873,plain,
join(sF2,composition(sk1,sF5)) = join(sF2,composition(sk1,sF4)),
inference(forward_demodulation,[],[f1826,f1]) ).
fof(f1884,plain,
! [X0] : join(X0,composition(sk1,complement(X0))) = join(X0,composition(sk1,top)),
inference(forward_demodulation,[],[f1812,f1]) ).
fof(f1903,plain,
join(sF2,sF7) = join(sF2,composition(sk1,sF5)),
inference(forward_demodulation,[],[f1873,f690]) ).
fof(f1912,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(X0,complement(join(X0,composition(sk1,top)))),
inference(backward_demodulation,[],[f1628,f1884]) ).
fof(f1920,plain,
sF10 = join(sF2,composition(sk1,sF5)),
inference(forward_demodulation,[],[f1903,f681]) ).
fof(f1932,plain,
complement(sF2) = join(complement(sF10),complement(join(sF2,complement(composition(sk1,sF5))))),
inference(superposition,[],[f644,f1920]) ).
fof(f1939,plain,
complement(sF2) = join(sF11,complement(join(sF2,complement(composition(sk1,sF5))))),
inference(forward_demodulation,[],[f1932,f55]) ).
fof(f1945,plain,
sF1 = join(sF11,complement(join(sF2,complement(composition(sk1,sF5))))),
inference(forward_demodulation,[],[f1939,f637]) ).
fof(f1968,plain,
! [X0] : join(sF4,X0) = join(sF4,join(X0,sF7)),
inference(superposition,[],[f1613,f690]) ).
fof(f3484,plain,
join(sF2,sF4) = join(sF5,sF4),
inference(superposition,[],[f168,f1292]) ).
fof(f3549,plain,
join(sF2,sF4) = join(sF4,sF5),
inference(forward_demodulation,[],[f3484,f1]) ).
fof(f3570,plain,
sF5 = join(sF4,sF5),
inference(forward_demodulation,[],[f3549,f43]) ).
fof(f3608,plain,
! [X0] : join(X0,complement(X0)) = join(top,complement(X0)),
inference(superposition,[],[f163,f1292]) ).
fof(f3618,plain,
! [X0,X1] : join(top,complement(join(X0,complement(X1)))) = join(join(X0,X1),complement(X0)),
inference(superposition,[],[f163,f644]) ).
fof(f3702,plain,
! [X0,X1] : join(X0,join(X1,complement(X0))) = join(top,complement(join(X0,complement(X1)))),
inference(forward_demodulation,[],[f3618,f2]) ).
fof(f3708,plain,
! [X0] : top = join(top,complement(X0)),
inference(forward_demodulation,[],[f3608,f15]) ).
fof(f3729,plain,
! [X0,X1] : join(top,X1) = join(top,complement(join(X0,complement(X1)))),
inference(forward_demodulation,[],[f3702,f1135]) ).
fof(f3744,plain,
! [X1] : top = join(top,X1),
inference(forward_demodulation,[],[f3729,f3708]) ).
fof(f4481,plain,
join(sF2,sF5) = join(sF5,sF5),
inference(superposition,[],[f168,f3570]) ).
fof(f4486,plain,
complement(sF4) = join(complement(sF5),complement(join(sF4,complement(sF5)))),
inference(superposition,[],[f644,f3570]) ).
fof(f4492,plain,
complement(sF4) = join(sF6,complement(join(sF4,sF6))),
inference(forward_demodulation,[],[f4486,f45]) ).
fof(f4495,plain,
sF5 = join(sF2,sF5),
inference(forward_demodulation,[],[f4481,f1292]) ).
fof(f4498,plain,
sF3 = join(sF6,complement(join(sF4,sF6))),
inference(forward_demodulation,[],[f4492,f638]) ).
fof(f4650,plain,
composition(sk1,top) = join(sF1,composition(sk1,top)),
inference(superposition,[],[f331,f3744]) ).
fof(f5097,plain,
join(sF4,sF2) = join(sF4,sF10),
inference(superposition,[],[f1968,f681]) ).
fof(f5136,plain,
join(sF2,sF4) = join(sF4,sF10),
inference(forward_demodulation,[],[f5097,f1]) ).
fof(f5147,plain,
sF5 = join(sF4,sF10),
inference(forward_demodulation,[],[f5136,f43]) ).
fof(f5159,plain,
complement(sF10) = join(complement(sF5),complement(join(sF10,complement(sF4)))),
inference(superposition,[],[f716,f5147]) ).
fof(f5163,plain,
complement(sF10) = join(complement(sF5),complement(join(sF10,sF3))),
inference(forward_demodulation,[],[f5159,f638]) ).
fof(f5169,plain,
complement(sF10) = join(complement(sF5),complement(join(sF3,sF10))),
inference(forward_demodulation,[],[f5163,f1450]) ).
fof(f5172,plain,
complement(sF10) = join(sF6,complement(join(sF3,sF10))),
inference(forward_demodulation,[],[f5169,f45]) ).
fof(f5175,plain,
sF11 = join(sF6,complement(join(sF3,sF10))),
inference(forward_demodulation,[],[f5172,f55]) ).
fof(f5455,plain,
complement(sF2) = join(complement(sF5),complement(join(sF2,complement(sF5)))),
inference(superposition,[],[f644,f4495]) ).
fof(f5461,plain,
complement(sF2) = join(sF6,complement(join(sF2,sF6))),
inference(forward_demodulation,[],[f5455,f45]) ).
fof(f5466,plain,
sF1 = join(sF6,complement(join(sF2,sF6))),
inference(forward_demodulation,[],[f5461,f637]) ).
fof(f5491,plain,
! [X0,X1] : join(complement(join(complement(X1),X0)),complement(join(X0,X1))) = join(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f1429,f648]) ).
fof(f5492,plain,
! [X0,X1] : join(complement(join(X0,complement(X1))),complement(join(X1,X0))) = join(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f1429,f716]) ).
fof(f5647,plain,
! [X0,X1] : join(complement(X0),complement(join(X1,X0))) = join(complement(join(X0,complement(X1))),complement(join(X1,X0))),
inference(forward_demodulation,[],[f5492,f1]) ).
fof(f5648,plain,
! [X0,X1] : join(complement(join(complement(X1),X0)),complement(join(X0,X1))) = join(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f5491,f1]) ).
fof(f5719,plain,
! [X0,X1] : join(complement(X0),complement(join(X1,X0))) = join(complement(join(X1,X0)),complement(join(X0,complement(X1)))),
inference(forward_demodulation,[],[f5647,f1]) ).
fof(f5720,plain,
! [X0,X1] : join(complement(join(X0,X1)),complement(join(complement(X1),X0))) = join(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f5648,f1]) ).
fof(f5749,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f5719,f716]) ).
fof(f5750,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f5720,f648]) ).
fof(f5770,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,complement(X1)))),
inference(backward_demodulation,[],[f888,f5749]) ).
fof(f5777,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X1,join(X0,X1)))),
inference(backward_demodulation,[],[f1063,f5770]) ).
fof(f5783,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f5777,f1430]) ).
fof(f5795,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(X0,complement(composition(sk1,top))),
inference(backward_demodulation,[],[f1912,f5783]) ).
fof(f5827,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(X1,complement(X0)),
inference(superposition,[],[f5783,f1]) ).
fof(f5864,plain,
join(sF2,complement(composition(sk1,sF5))) = join(sF2,complement(sF10)),
inference(superposition,[],[f5783,f1920]) ).
fof(f5880,plain,
join(sF4,complement(sF5)) = join(sF4,complement(sF10)),
inference(superposition,[],[f5783,f5147]) ).
fof(f5897,plain,
! [X0,X1] : join(X0,composition(sk1,complement(join(X0,X1)))) = join(X0,composition(sk1,join(X0,complement(X1)))),
inference(superposition,[],[f1641,f5783]) ).
fof(f5937,plain,
! [X0,X1] : join(X0,composition(sk1,complement(X1))) = join(X0,composition(sk1,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f5897,f1641]) ).
fof(f5954,plain,
join(sF4,complement(sF5)) = join(sF4,sF11),
inference(forward_demodulation,[],[f5880,f55]) ).
fof(f5969,plain,
join(sF2,complement(composition(sk1,sF5))) = join(sF2,sF11),
inference(forward_demodulation,[],[f5864,f55]) ).
fof(f6009,plain,
sF1 = join(sF6,complement(sF2)),
inference(backward_demodulation,[],[f5466,f5827]) ).
fof(f6010,plain,
sF3 = join(sF6,complement(sF4)),
inference(backward_demodulation,[],[f4498,f5827]) ).
fof(f6037,plain,
join(sF4,sF6) = join(sF4,sF11),
inference(forward_demodulation,[],[f5954,f45]) ).
fof(f6051,plain,
sF1 = join(sF11,complement(join(sF2,sF11))),
inference(backward_demodulation,[],[f1945,f5969]) ).
fof(f6078,plain,
sF3 = join(sF6,sF3),
inference(forward_demodulation,[],[f6010,f638]) ).
fof(f6079,plain,
sF1 = join(sF6,sF1),
inference(forward_demodulation,[],[f6009,f637]) ).
fof(f6104,plain,
sF1 = join(sF11,complement(sF2)),
inference(forward_demodulation,[],[f6051,f5827]) ).
fof(f6127,plain,
sF3 = join(sF3,sF6),
inference(forward_demodulation,[],[f6078,f1]) ).
fof(f6128,plain,
sF1 = join(sF1,sF6),
inference(forward_demodulation,[],[f6079,f1]) ).
fof(f6137,plain,
sF1 = join(sF11,sF1),
inference(forward_demodulation,[],[f6104,f637]) ).
fof(f6153,plain,
sF1 = join(sF1,sF11),
inference(forward_demodulation,[],[f6137,f1]) ).
fof(f6184,plain,
join(sF1,complement(sF1)) = join(sF1,complement(sF11)),
inference(superposition,[],[f5783,f6153]) ).
fof(f6185,plain,
join(sF1,complement(sF1)) = join(sF1,sF10),
inference(forward_demodulation,[],[f6184,f642]) ).
fof(f6192,plain,
top = join(sF1,sF10),
inference(forward_demodulation,[],[f6185,f15]) ).
fof(f6281,plain,
join(composition(sk1,sF5),complement(sF2)) = join(composition(sk1,sF5),complement(sF10)),
inference(superposition,[],[f5827,f1920]) ).
fof(f6286,plain,
join(sF4,complement(sF2)) = join(sF4,complement(sF5)),
inference(superposition,[],[f5827,f43]) ).
fof(f6289,plain,
join(sF7,complement(sF2)) = join(sF7,complement(sF10)),
inference(superposition,[],[f5827,f681]) ).
fof(f6294,plain,
join(sF10,complement(sF5)) = join(sF10,complement(sF4)),
inference(superposition,[],[f5827,f5147]) ).
fof(f6371,plain,
join(sF10,complement(sF5)) = join(sF10,sF3),
inference(forward_demodulation,[],[f6294,f638]) ).
fof(f6376,plain,
join(sF7,complement(sF2)) = join(sF7,sF11),
inference(forward_demodulation,[],[f6289,f55]) ).
fof(f6379,plain,
join(sF4,complement(sF2)) = join(sF4,sF6),
inference(forward_demodulation,[],[f6286,f45]) ).
fof(f6383,plain,
join(composition(sk1,sF5),complement(sF2)) = join(complement(sF10),composition(sk1,sF5)),
inference(forward_demodulation,[],[f6281,f1]) ).
fof(f6436,plain,
join(sF10,complement(sF5)) = join(sF3,sF10),
inference(forward_demodulation,[],[f6371,f1]) ).
fof(f6441,plain,
join(sF7,sF1) = join(sF7,sF11),
inference(forward_demodulation,[],[f6376,f637]) ).
fof(f6444,plain,
join(sF4,sF1) = join(sF4,sF6),
inference(forward_demodulation,[],[f6379,f637]) ).
fof(f6448,plain,
join(composition(sk1,sF5),complement(sF2)) = join(sF11,composition(sk1,sF5)),
inference(forward_demodulation,[],[f6383,f55]) ).
fof(f6485,plain,
join(sF10,sF6) = join(sF3,sF10),
inference(forward_demodulation,[],[f6436,f45]) ).
fof(f6490,plain,
join(sF1,sF7) = join(sF7,sF11),
inference(forward_demodulation,[],[f6441,f1]) ).
fof(f6493,plain,
join(sF1,sF4) = join(sF4,sF6),
inference(forward_demodulation,[],[f6444,f1]) ).
fof(f6496,plain,
join(complement(sF2),composition(sk1,sF5)) = join(sF11,composition(sk1,sF5)),
inference(forward_demodulation,[],[f6448,f1]) ).
fof(f6519,plain,
join(sF1,sF4) = join(sF4,sF11),
inference(backward_demodulation,[],[f6037,f6493]) ).
fof(f6520,plain,
join(sF1,composition(sk1,sF5)) = join(sF11,composition(sk1,sF5)),
inference(forward_demodulation,[],[f6496,f637]) ).
fof(f6998,plain,
join(sF7,composition(sk1,sF11)) = join(sF7,composition(sk1,join(sF1,sF7))),
inference(superposition,[],[f1641,f6490]) ).
fof(f7007,plain,
join(sF7,composition(sk1,sF11)) = join(composition(sk1,sF1),sF7),
inference(forward_demodulation,[],[f6998,f1801]) ).
fof(f7021,plain,
join(sF7,composition(sk1,sF11)) = join(sF7,composition(sk1,sF1)),
inference(forward_demodulation,[],[f7007,f1]) ).
fof(f7062,plain,
join(sF4,composition(sk1,sF6)) = join(sF4,composition(sk1,join(sF1,sF4))),
inference(superposition,[],[f1641,f6493]) ).
fof(f7071,plain,
join(sF4,composition(sk1,sF6)) = join(composition(sk1,sF1),sF4),
inference(forward_demodulation,[],[f7062,f1801]) ).
fof(f7084,plain,
join(sF4,composition(sk1,sF6)) = join(sF4,composition(sk1,sF1)),
inference(forward_demodulation,[],[f7071,f1]) ).
fof(f7177,plain,
join(sF3,composition(sk1,sF3)) = join(sF3,composition(sk1,sF6)),
inference(superposition,[],[f1641,f6127]) ).
fof(f7182,plain,
sF3 = join(sF3,composition(sk1,sF6)),
inference(forward_demodulation,[],[f7177,f1567]) ).
fof(f7643,plain,
join(sF4,composition(sk1,join(sF1,sF4))) = join(sF4,composition(sk1,sF11)),
inference(superposition,[],[f1641,f6519]) ).
fof(f7654,plain,
join(composition(sk1,sF1),sF4) = join(sF4,composition(sk1,sF11)),
inference(forward_demodulation,[],[f7643,f1801]) ).
fof(f7668,plain,
join(sF4,composition(sk1,sF1)) = join(sF4,composition(sk1,sF11)),
inference(forward_demodulation,[],[f7654,f1]) ).
fof(f10039,plain,
composition(sk1,join(sF1,sF4)) = join(sF7,composition(sk1,sF6)),
inference(superposition,[],[f698,f6493]) ).
fof(f10086,plain,
join(sF7,composition(sk1,sF1)) = join(sF7,composition(sk1,sF6)),
inference(forward_demodulation,[],[f10039,f699]) ).
fof(f10404,plain,
complement(sF11) = join(complement(sF11),complement(join(sF1,composition(sk1,sF5)))),
inference(superposition,[],[f5750,f6520]) ).
fof(f10499,plain,
sF10 = join(sF10,complement(join(sF1,composition(sk1,sF5)))),
inference(forward_demodulation,[],[f10404,f642]) ).
fof(f12368,plain,
join(sF1,composition(sk1,complement(sF1))) = join(sF1,composition(sk1,complement(sF6))),
inference(superposition,[],[f5937,f6128]) ).
fof(f12505,plain,
join(sF1,composition(sk1,sF5)) = join(sF1,composition(sk1,complement(sF1))),
inference(forward_demodulation,[],[f12368,f639]) ).
fof(f12605,plain,
join(sF1,composition(sk1,sF5)) = join(sF1,composition(sk1,top)),
inference(forward_demodulation,[],[f12505,f1884]) ).
fof(f12669,plain,
composition(sk1,top) = join(sF1,composition(sk1,sF5)),
inference(forward_demodulation,[],[f12605,f4650]) ).
fof(f12712,plain,
sF10 = join(sF10,complement(composition(sk1,top))),
inference(backward_demodulation,[],[f10499,f12669]) ).
fof(f12735,plain,
sF10 = complement(composition(sk1,complement(sF10))),
inference(forward_demodulation,[],[f12712,f5795]) ).
fof(f12743,plain,
sF10 = complement(composition(sk1,sF11)),
inference(forward_demodulation,[],[f12735,f55]) ).
fof(f12781,plain,
complement(sF10) = composition(sk1,sF11),
inference(superposition,[],[f601,f12743]) ).
fof(f12798,plain,
sF11 = composition(sk1,sF11),
inference(forward_demodulation,[],[f12781,f55]) ).
fof(f12816,plain,
join(sF7,sF11) = join(sF7,composition(sk1,sF1)),
inference(backward_demodulation,[],[f7021,f12798]) ).
fof(f12817,plain,
join(sF4,sF11) = join(sF4,composition(sk1,sF1)),
inference(backward_demodulation,[],[f7668,f12798]) ).
fof(f12851,plain,
join(sF1,sF4) = join(sF4,composition(sk1,sF1)),
inference(forward_demodulation,[],[f12817,f6519]) ).
fof(f12852,plain,
join(sF1,sF7) = join(sF7,composition(sk1,sF1)),
inference(forward_demodulation,[],[f12816,f6490]) ).
fof(f12861,plain,
join(sF1,sF4) = join(sF4,composition(sk1,sF6)),
inference(backward_demodulation,[],[f7084,f12851]) ).
fof(f12862,plain,
join(sF1,sF7) = join(sF7,composition(sk1,sF6)),
inference(backward_demodulation,[],[f10086,f12852]) ).
fof(f13333,plain,
complement(composition(sk1,sF6)) = join(complement(join(sF1,sF4)),complement(join(complement(sF4),composition(sk1,sF6)))),
inference(superposition,[],[f789,f12861]) ).
fof(f13359,plain,
complement(composition(sk1,sF6)) = join(complement(join(sF1,sF4)),complement(join(sF3,composition(sk1,sF6)))),
inference(forward_demodulation,[],[f13333,f638]) ).
fof(f13380,plain,
join(complement(join(sF1,sF4)),complement(sF3)) = complement(composition(sk1,sF6)),
inference(forward_demodulation,[],[f13359,f7182]) ).
fof(f13395,plain,
join(complement(sF3),complement(join(sF1,sF4))) = complement(composition(sk1,sF6)),
inference(forward_demodulation,[],[f13380,f1]) ).
fof(f13404,plain,
join(sF4,complement(join(sF1,sF4))) = complement(composition(sk1,sF6)),
inference(forward_demodulation,[],[f13395,f41]) ).
fof(f13411,plain,
join(sF4,complement(sF1)) = complement(composition(sk1,sF6)),
inference(forward_demodulation,[],[f13404,f5827]) ).
fof(f13416,plain,
join(sF4,sF2) = complement(composition(sk1,sF6)),
inference(forward_demodulation,[],[f13411,f37]) ).
fof(f13419,plain,
join(sF2,sF4) = complement(composition(sk1,sF6)),
inference(forward_demodulation,[],[f13416,f1]) ).
fof(f13421,plain,
sF5 = complement(composition(sk1,sF6)),
inference(forward_demodulation,[],[f13419,f43]) ).
fof(f13458,plain,
complement(sF5) = composition(sk1,sF6),
inference(superposition,[],[f601,f13421]) ).
fof(f13475,plain,
sF6 = composition(sk1,sF6),
inference(forward_demodulation,[],[f13458,f45]) ).
fof(f13500,plain,
join(sF1,sF7) = join(sF7,sF6),
inference(backward_demodulation,[],[f12862,f13475]) ).
fof(f13587,plain,
join(sF10,sF6) = join(sF2,join(sF1,sF7)),
inference(superposition,[],[f685,f13500]) ).
fof(f13629,plain,
join(sF10,sF6) = join(sF10,sF1),
inference(forward_demodulation,[],[f13587,f897]) ).
fof(f13646,plain,
join(sF10,sF6) = join(sF1,sF10),
inference(forward_demodulation,[],[f13629,f1]) ).
fof(f13661,plain,
top = join(sF10,sF6),
inference(forward_demodulation,[],[f13646,f6192]) ).
fof(f13673,plain,
top = join(sF3,sF10),
inference(backward_demodulation,[],[f6485,f13661]) ).
fof(f13685,plain,
sF11 = join(sF6,complement(top)),
inference(backward_demodulation,[],[f5175,f13673]) ).
fof(f13692,plain,
sF11 = join(sF6,zero),
inference(forward_demodulation,[],[f13685,f57]) ).
fof(f13700,plain,
sF6 = sF11,
inference(forward_demodulation,[],[f13692,f1380]) ).
fof(f13860,plain,
$false,
inference(forward_subsumption_resolution,[],[f13700,f56]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL030-3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n001.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 23:00:46 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.85/2.17 % (4062215)Detected a unit-equality problem, will run specialized UEQ schedule.
% 10.85/2.17 % (4062222)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=1597153263:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 10.85/2.17 % (4062223)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3269469910:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 10.85/2.17 % (4062225)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1274367712:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 10.85/2.17 % (4062224)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=252217324:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 10.85/2.17 % (4062221)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1169987469:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 10.85/2.17 % (4062226)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1611136914:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 10.85/2.17 % (4062220)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=3289883725:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 10.85/2.17 % (4062223)Instruction limit reached!
% 10.85/2.17 % (4062223)------------------------------
% 10.85/2.17 % (4062223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.85/2.17 % (4062223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.17 % (4062223)CaDiCaL version: 2.1.3
% 10.85/2.17 % (4062223)Termination reason: Instruction limit
% 10.85/2.17 % (4062223)Termination phase: Saturation
% 10.85/2.17 % (4062223)Time elapsed: 0.082 s
% 10.85/2.17 % (4062223)Peak memory usage: 89 MB
% 10.85/2.17 % (4062223)Instructions burned: 136 (million)
% 10.85/2.17 % (4062224)Instruction limit reached!
% 10.85/2.17 % (4062224)------------------------------
% 10.85/2.17 % (4062224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.85/2.17 % (4062224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.17 % (4062224)CaDiCaL version: 2.1.3
% 10.85/2.17 % (4062224)Termination reason: Instruction limit
% 10.85/2.17 % (4062224)Termination phase: Saturation
% 10.85/2.17 % (4062224)Time elapsed: 0.103 s
% 10.85/2.17 % (4062224)Peak memory usage: 89 MB
% 10.85/2.17 % (4062224)Instructions burned: 182 (million)
% 10.85/2.17 % (4062225)Instruction limit reached!
% 10.85/2.17 % (4062225)------------------------------
% 10.85/2.17 % (4062225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.85/2.17 % (4062225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.17 % (4062225)CaDiCaL version: 2.1.3
% 10.85/2.17 % (4062225)Termination reason: Instruction limit
% 10.85/2.17 % (4062225)Termination phase: Saturation
% 10.85/2.17 % (4062225)Time elapsed: 0.170 s
% 10.85/2.17 % (4062225)Peak memory usage: 90 MB
% 10.85/2.17 % (4062225)Instructions burned: 258 (million)
% 10.85/2.17 % (4062234)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1221876876:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 10.85/2.17 % (4062235)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3181317100:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 10.85/2.17 % (4062236)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=2698212211:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 10.85/2.17 % (4062236)Instruction limit reached!
% 10.85/2.17 % (4062236)------------------------------
% 10.85/2.17 % (4062236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.85/2.17 % (4062236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.17 % (4062236)CaDiCaL version: 2.1.3
% 10.85/2.17 % (4062236)Termination reason: Instruction limit
% 10.85/2.17 % (4062236)Termination phase: Saturation
% 10.85/2.17 % (4062236)Time elapsed: 0.126 s
% 10.85/2.17 % (4062236)Peak memory usage: 92 MB
% 10.85/2.17 % (4062236)Instructions burned: 216 (million)
% 10.85/2.17 % (4062240)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=1195624908:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2993 on theBenchmark for (2993ds/317Mi)
% 10.85/2.17 % (4062226)Instruction limit reached!
% 10.85/2.17 % (4062226)------------------------------
% 10.85/2.17 % (4062226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.85/2.17 % (4062226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.17 % (4062226)CaDiCaL version: 2.1.3
% 10.85/2.17 % (4062226)Termination reason: Instruction limit
% 10.85/2.17 % (4062226)Termination phase: Saturation
% 10.85/2.17 % (4062226)Time elapsed: 0.651 s
% 10.85/2.17 % (4062226)Peak memory usage: 100 MB
% 10.85/2.17 % (4062226)Instructions burned: 1188 (million)
% 10.85/2.17 % (4062242)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=2106585588:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 10.85/2.17 % (4062240)Instruction limit reached!
% 10.85/2.17 % (4062240)------------------------------
% 10.85/2.17 % (4062240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.85/2.17 % (4062240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.17 % (4062240)CaDiCaL version: 2.1.3
% 10.85/2.17 % (4062240)Termination reason: Instruction limit
% 10.85/2.17 % (4062240)Termination phase: Saturation
% 10.85/2.17 % (4062240)Time elapsed: 0.198 s
% 10.85/2.17 % (4062240)Peak memory usage: 94 MB
% 10.85/2.17 % (4062240)Instructions burned: 318 (million)
% 10.85/2.17 % (4062244)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3949308079:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2989 on theBenchmark for (2989ds/2836Mi)
% 10.85/2.17 % (4062222)First to succeed.
% 10.85/2.17 % (4062222)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4062215"
% 10.85/2.17 % (4062221)Also succeeded, but the first one will report.
% 10.85/2.17 % (4062234)Instruction limit reached!
% 10.85/2.17 % (4062234)------------------------------
% 10.85/2.17 % (4062234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.85/2.17 % (4062234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.17 % (4062234)CaDiCaL version: 2.1.3
% 10.85/2.17 % (4062234)Termination reason: Instruction limit
% 10.85/2.17 % (4062234)Termination phase: Saturation
% 10.85/2.17 % (4062234)Time elapsed: 1.090 s
% 10.85/2.17 % (4062234)Peak memory usage: 140 MB
% 10.85/2.17 % (4062234)Instructions burned: 2052 (million)
% 10.85/2.17 % (4062222)Refutation found. Thanks to Tanya!
% 10.85/2.17 % SZS status Unsatisfiable for theBenchmark
% 10.85/2.17 % SZS output start Proof for theBenchmark
% See solution above
% 11.29/2.37 % (4062222)------------------------------
% 11.29/2.37 % (4062222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.29/2.37 % (4062222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.29/2.37 % (4062222)CaDiCaL version: 2.1.3
% 11.29/2.37 % (4062222)Termination reason: Refutation
% 11.29/2.37 % (4062222)Time elapsed: 1.191 s
% 11.29/2.37 % (4062222)Peak memory usage: 145 MB
% 11.29/2.37 % (4062222)Instructions burned: 2785 (million)
% 11.29/2.37 % (4062222)------------------------------
% 11.29/2.37 % (4062222)------------------------------
% 11.29/2.37 % (4062215)Success in time 1.553 s
% 11.29/2.37 % Vampire exiting
%------------------------------------------------------------------------------