%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : REL047-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/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:40 PM UTC 2026
% Result : Unsatisfiable 188.89s 38.52s
% Output : Refutation 188.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 72
% Number of leaves : 14
% Syntax : Number of formulae : 225 ( 225 unt; 0 def)
% Number of atoms : 225 ( 224 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 : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 277 ( 277 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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(f8,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/REL001-0.ax',composition_identity_6) ).
fof(f10,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/REL001-0.ax',converse_additivity_9) ).
fof(f12,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/REL001-0.ax',converse_multiplicativity_10) ).
fof(f13,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox/benchmark/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/sandbox/benchmark/Axioms/REL001-0.ax',def_top_12) ).
fof(f16,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/REL001-0.ax',def_zero_13) ).
fof(f17,negated_conjecture,
join(sk1,sk2) = sk2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_14) ).
fof(f18,plain,
sk2 = join(sk1,sk2),
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
join(sk1,sk3) = sk3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_15) ).
fof(f20,plain,
sk3 = join(sk1,sk3),
inference(reorient_equations,[],[f19]) ).
fof(f21,negated_conjecture,
join(sk1,meet(sk2,sk3)) != meet(sk2,sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_16) ).
fof(f22,plain,
meet(sk2,sk3) != join(sk1,meet(sk2,sk3)),
inference(reorient_equations,[],[f21]) ).
fof(f23,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f16,f6]) ).
fof(f24,plain,
complement(join(complement(sk2),complement(sk3))) != join(sk1,complement(join(complement(sk2),complement(sk3)))),
inference(definition_unfolding,[],[f22,f6,f6]) ).
fof(f25,plain,
sk2 = join(sk2,sk1),
inference(superposition,[],[f1,f18]) ).
fof(f26,plain,
sk3 = join(sk3,sk1),
inference(superposition,[],[f1,f20]) ).
fof(f33,plain,
zero = complement(top),
inference(forward_demodulation,[],[f23,f15]) ).
fof(f34,plain,
top = join(top,zero),
inference(superposition,[],[f15,f33]) ).
fof(f35,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[],[f11,f10]) ).
fof(f36,plain,
! [X0,X1] : converse(join(X1,converse(X0))) = join(converse(X1),X0),
inference(superposition,[],[f11,f10]) ).
fof(f37,plain,
! [X0,X1] : join(converse(X0),converse(X1)) = converse(join(X1,X0)),
inference(superposition,[],[f11,f1]) ).
fof(f42,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[],[f12,f10]) ).
fof(f46,plain,
! [X0] : join(X0,converse(complement(converse(X0)))) = converse(top),
inference(superposition,[],[f35,f15]) ).
fof(f47,plain,
! [X0,X1] : join(X1,converse(X0)) = converse(join(X0,converse(X1))),
inference(superposition,[],[f35,f1]) ).
fof(f70,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(converse(X1),X0),
inference(superposition,[],[f36,f1]) ).
fof(f92,plain,
! [X0,X1] : converse(join(X0,X1)) = converse(join(X1,X0)),
inference(superposition,[],[f37,f11]) ).
fof(f202,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f42,f8]) ).
fof(f218,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f202,f10]) ).
fof(f223,plain,
one = converse(one),
inference(superposition,[],[f218,f8]) ).
fof(f230,plain,
! [X0] : composition(one,X0) = X0,
inference(superposition,[],[f218,f223]) ).
fof(f434,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f2,f15]) ).
fof(f435,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(superposition,[],[f2,f1]) ).
fof(f445,plain,
! [X0] : join(sk2,X0) = join(sk2,join(sk1,X0)),
inference(superposition,[],[f2,f25]) ).
fof(f446,plain,
! [X0] : join(sk3,X0) = join(sk3,join(sk1,X0)),
inference(superposition,[],[f2,f26]) ).
fof(f447,plain,
! [X0,X1] : top = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f2,f15]) ).
fof(f448,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X1,join(X2,X0)),
inference(superposition,[],[f2,f1]) ).
fof(f488,plain,
! [X0] : join(sk2,X0) = join(sk2,join(X0,sk1)),
inference(superposition,[],[f445,f1]) ).
fof(f499,plain,
! [X0] : join(sk3,X0) = join(sk3,join(X0,sk1)),
inference(superposition,[],[f446,f1]) ).
fof(f533,plain,
! [X0,X1] : join(join(sk2,X0),X1) = join(sk2,join(join(X0,sk1),X1)),
inference(superposition,[],[f2,f488]) ).
fof(f534,plain,
! [X0,X1] : join(join(sk2,X0),X1) = join(sk2,join(X0,join(sk1,X1))),
inference(forward_demodulation,[],[f533,f2]) ).
fof(f535,plain,
! [X0,X1] : join(sk2,join(X0,X1)) = join(sk2,join(X0,join(sk1,X1))),
inference(forward_demodulation,[],[f534,f2]) ).
fof(f540,plain,
! [X0,X1] : join(join(sk3,X0),X1) = join(sk3,join(join(X0,sk1),X1)),
inference(superposition,[],[f2,f499]) ).
fof(f541,plain,
! [X0,X1] : join(join(sk3,X0),X1) = join(sk3,join(X0,join(sk1,X1))),
inference(forward_demodulation,[],[f540,f2]) ).
fof(f542,plain,
! [X0,X1] : join(sk3,join(X0,X1)) = join(sk3,join(X0,join(sk1,X1))),
inference(forward_demodulation,[],[f541,f2]) ).
fof(f1051,plain,
! [X0,X1] : join(sk2,join(join(sk1,X0),X1)) = join(sk2,join(X1,X0)),
inference(superposition,[],[f535,f1]) ).
fof(f1076,plain,
! [X0,X1] : join(sk2,join(sk1,join(X0,X1))) = join(sk2,join(X1,X0)),
inference(forward_demodulation,[],[f1051,f2]) ).
fof(f1082,plain,
! [X0,X1] : join(sk2,join(X0,X1)) = join(sk2,join(X1,X0)),
inference(forward_demodulation,[],[f1076,f445]) ).
fof(f1099,plain,
! [X0,X1] : join(sk2,join(converse(X1),converse(X0))) = join(sk2,converse(join(X0,X1))),
inference(superposition,[],[f1082,f11]) ).
fof(f1146,plain,
! [X0,X1] : join(sk2,converse(join(X0,X1))) = join(sk2,converse(join(X1,X0))),
inference(forward_demodulation,[],[f1099,f11]) ).
fof(f1295,plain,
! [X0,X1] : join(sk3,join(join(sk1,X0),X1)) = join(sk3,join(X1,X0)),
inference(superposition,[],[f542,f1]) ).
fof(f1326,plain,
! [X0,X1] : join(sk3,join(sk1,join(X0,X1))) = join(sk3,join(X1,X0)),
inference(forward_demodulation,[],[f1295,f2]) ).
fof(f1333,plain,
! [X0,X1] : join(sk3,join(X0,X1)) = join(sk3,join(X1,X0)),
inference(forward_demodulation,[],[f1326,f446]) ).
fof(f1350,plain,
! [X0,X1] : join(sk3,join(converse(X1),converse(X0))) = join(sk3,converse(join(X0,X1))),
inference(superposition,[],[f1333,f11]) ).
fof(f1401,plain,
! [X0,X1] : join(sk3,converse(join(X0,X1))) = join(sk3,converse(join(X1,X0))),
inference(forward_demodulation,[],[f1350,f11]) ).
fof(f1842,plain,
! [X0,X1] : join(join(X1,X0),converse(sk2)) = converse(join(sk2,converse(join(X0,X1)))),
inference(superposition,[],[f47,f1146]) ).
fof(f1849,plain,
! [X0,X1] : join(join(X1,X0),converse(sk2)) = join(converse(sk2),join(X0,X1)),
inference(forward_demodulation,[],[f1842,f36]) ).
fof(f1861,plain,
! [X0,X1] : join(converse(sk2),join(X0,X1)) = join(X1,join(X0,converse(sk2))),
inference(forward_demodulation,[],[f1849,f2]) ).
fof(f1896,plain,
! [X0,X1] : join(join(X1,X0),converse(sk3)) = converse(join(sk3,converse(join(X0,X1)))),
inference(superposition,[],[f47,f1401]) ).
fof(f1903,plain,
! [X0,X1] : join(join(X1,X0),converse(sk3)) = join(converse(sk3),join(X0,X1)),
inference(forward_demodulation,[],[f1896,f36]) ).
fof(f1915,plain,
! [X0,X1] : join(converse(sk3),join(X0,X1)) = join(X1,join(X0,converse(sk3))),
inference(forward_demodulation,[],[f1903,f2]) ).
fof(f2186,plain,
! [X0,X1] : join(converse(sk2),join(X0,X1)) = join(X1,join(converse(sk2),X0)),
inference(superposition,[],[f1861,f1]) ).
fof(f2509,plain,
! [X0,X1] : join(converse(sk3),converse(join(X0,X1))) = join(converse(X1),join(converse(X0),converse(sk3))),
inference(superposition,[],[f1915,f11]) ).
fof(f2520,plain,
! [X0,X1] : join(converse(sk3),join(X0,X1)) = join(X1,join(converse(sk3),X0)),
inference(superposition,[],[f1915,f1]) ).
fof(f2621,plain,
! [X0,X1] : join(converse(sk3),converse(join(X0,X1))) = join(converse(X1),converse(join(X0,sk3))),
inference(forward_demodulation,[],[f2509,f11]) ).
fof(f2637,plain,
! [X0,X1] : join(converse(sk3),converse(join(X0,X1))) = converse(join(X1,join(X0,sk3))),
inference(forward_demodulation,[],[f2621,f11]) ).
fof(f2645,plain,
! [X0,X1] : converse(join(sk3,join(X0,X1))) = converse(join(X1,join(X0,sk3))),
inference(forward_demodulation,[],[f2637,f11]) ).
fof(f3764,plain,
! [X0] : join(X0,top) = join(converse(sk2),join(complement(converse(sk2)),X0)),
inference(superposition,[],[f2186,f15]) ).
fof(f3954,plain,
! [X0,X1] : join(X1,join(X0,top)) = join(converse(sk2),join(join(complement(converse(sk2)),X0),X1)),
inference(superposition,[],[f2186,f3764]) ).
fof(f3958,plain,
! [X0,X1] : join(join(X0,top),X1) = join(converse(sk2),join(join(complement(converse(sk2)),X0),X1)),
inference(superposition,[],[f2,f3764]) ).
fof(f3959,plain,
! [X0,X1] : join(join(X0,top),X1) = join(converse(sk2),join(complement(converse(sk2)),join(X0,X1))),
inference(forward_demodulation,[],[f3958,f2]) ).
fof(f3962,plain,
! [X0,X1] : join(X1,join(X0,top)) = join(converse(sk2),join(complement(converse(sk2)),join(X0,X1))),
inference(forward_demodulation,[],[f3954,f2]) ).
fof(f3983,plain,
! [X0,X1] : join(join(X0,X1),top) = join(join(X0,top),X1),
inference(forward_demodulation,[],[f3959,f3764]) ).
fof(f3985,plain,
! [X0,X1] : join(join(X0,X1),top) = join(X1,join(X0,top)),
inference(forward_demodulation,[],[f3962,f3764]) ).
fof(f3996,plain,
! [X0,X1] : join(join(X0,X1),top) = join(X0,join(top,X1)),
inference(forward_demodulation,[],[f3983,f2]) ).
fof(f3997,plain,
! [X0,X1] : join(X0,join(X1,top)) = join(X1,join(X0,top)),
inference(forward_demodulation,[],[f3985,f2]) ).
fof(f4001,plain,
! [X0,X1] : join(X0,join(X1,top)) = join(X0,join(top,X1)),
inference(forward_demodulation,[],[f3996,f2]) ).
fof(f4009,plain,
! [X0,X1] : join(X0,join(X1,top)) = join(X1,join(top,X0)),
inference(superposition,[],[f3997,f1]) ).
fof(f4430,plain,
! [X0,X1] : converse(join(X0,join(top,X1))) = converse(join(join(X1,top),X0)),
inference(superposition,[],[f92,f4001]) ).
fof(f4446,plain,
! [X0,X1] : join(converse(join(X1,top)),X0) = converse(join(converse(X0),join(top,X1))),
inference(superposition,[],[f70,f4001]) ).
fof(f4515,plain,
! [X0,X1] : converse(join(converse(X0),join(X1,top))) = join(converse(join(top,X1)),X0),
inference(superposition,[],[f70,f4001]) ).
fof(f4520,plain,
! [X0,X1] : join(X0,converse(join(X1,top))) = join(converse(join(top,X1)),X0),
inference(forward_demodulation,[],[f4515,f35]) ).
fof(f4565,plain,
! [X0,X1] : join(converse(join(X1,top)),X0) = join(X0,converse(join(top,X1))),
inference(forward_demodulation,[],[f4446,f35]) ).
fof(f4581,plain,
! [X0,X1] : converse(join(X0,join(top,X1))) = converse(join(X1,join(top,X0))),
inference(forward_demodulation,[],[f4430,f2]) ).
fof(f5045,plain,
! [X0] : join(X0,top) = join(zero,join(X0,top)),
inference(superposition,[],[f4009,f34]) ).
fof(f5403,plain,
! [X0] : join(top,X0) = join(zero,join(top,X0)),
inference(superposition,[],[f5045,f1]) ).
fof(f5472,plain,
converse(top) = join(zero,converse(top)),
inference(superposition,[],[f5403,f46]) ).
fof(f5515,plain,
converse(converse(top)) = join(top,converse(zero)),
inference(superposition,[],[f47,f5472]) ).
fof(f5521,plain,
top = join(top,converse(zero)),
inference(forward_demodulation,[],[f5515,f10]) ).
fof(f5537,plain,
! [X0] : join(top,X0) = join(top,join(converse(zero),X0)),
inference(superposition,[],[f2,f5521]) ).
fof(f22816,plain,
! [X0] : join(X0,top) = join(converse(sk3),join(complement(converse(sk3)),X0)),
inference(superposition,[],[f2520,f15]) ).
fof(f22817,plain,
! [X0] : join(X0,converse(top)) = join(converse(sk3),join(converse(complement(converse(converse(sk3)))),X0)),
inference(superposition,[],[f2520,f46]) ).
fof(f23007,plain,
! [X0] : join(X0,converse(top)) = join(converse(sk3),join(converse(complement(sk3)),X0)),
inference(forward_demodulation,[],[f22817,f10]) ).
fof(f23141,plain,
! [X0] : join(X0,top) = join(converse(sk3),join(X0,complement(converse(sk3)))),
inference(superposition,[],[f22816,f1]) ).
fof(f24556,plain,
! [X0,X1] : join(X1,join(X0,sk3)) = converse(converse(join(sk3,join(X0,X1)))),
inference(superposition,[],[f10,f2645]) ).
fof(f24583,plain,
! [X0,X1] : join(sk3,join(X0,X1)) = join(X1,join(X0,sk3)),
inference(forward_demodulation,[],[f24556,f10]) ).
fof(f24734,plain,
! [X0,X1] : join(sk3,join(X0,X1)) = join(X1,join(sk3,X0)),
inference(superposition,[],[f24583,f1]) ).
fof(f26566,plain,
! [X0] : join(X0,top) = join(sk3,join(complement(sk3),X0)),
inference(superposition,[],[f24734,f15]) ).
fof(f44120,plain,
join(converse(complement(sk3)),top) = join(complement(converse(sk3)),converse(top)),
inference(superposition,[],[f23141,f23007]) ).
fof(f44181,plain,
join(converse(complement(sk3)),top) = join(converse(top),complement(converse(sk3))),
inference(forward_demodulation,[],[f44120,f1]) ).
fof(f44296,plain,
join(top,converse(complement(sk3))) = join(converse(top),complement(converse(sk3))),
inference(forward_demodulation,[],[f44181,f1]) ).
fof(f44494,plain,
converse(join(top,converse(complement(sk3)))) = join(top,converse(complement(converse(sk3)))),
inference(superposition,[],[f35,f44296]) ).
fof(f44497,plain,
join(top,converse(complement(converse(sk3)))) = join(converse(top),complement(sk3)),
inference(forward_demodulation,[],[f44494,f36]) ).
fof(f44501,plain,
join(top,converse(complement(converse(sk3)))) = join(complement(sk3),converse(top)),
inference(forward_demodulation,[],[f44497,f1]) ).
fof(f62370,plain,
! [X0,X1] : join(converse(join(X0,top)),X1) = join(converse(join(top,X0)),X1),
inference(superposition,[],[f4520,f1]) ).
fof(f67415,plain,
! [X0] : converse(join(X0,converse(top))) = converse(join(converse(complement(converse(top))),join(top,X0))),
inference(superposition,[],[f4581,f46]) ).
fof(f67747,plain,
! [X0] : converse(join(X0,converse(top))) = join(complement(converse(top)),converse(join(top,X0))),
inference(forward_demodulation,[],[f67415,f35]) ).
fof(f68081,plain,
! [X0] : join(converse(X0),top) = join(complement(converse(top)),converse(join(top,X0))),
inference(forward_demodulation,[],[f67747,f36]) ).
fof(f68262,plain,
! [X0] : join(top,converse(X0)) = join(complement(converse(top)),converse(join(top,X0))),
inference(forward_demodulation,[],[f68081,f1]) ).
fof(f108951,plain,
! [X0] : top = join(converse(join(X0,top)),complement(converse(join(top,X0)))),
inference(superposition,[],[f62370,f15]) ).
fof(f117089,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(converse(X0),complement(composition(X0,X1)))),
inference(forward_demodulation,[],[f14,f1]) ).
fof(f123931,plain,
! [X0] : join(converse(sk3),complement(converse(sk3))) = join(composition(converse(X0),complement(composition(X0,converse(sk3)))),top),
inference(superposition,[],[f22816,f117089]) ).
fof(f123943,plain,
! [X0] : join(sk3,complement(sk3)) = join(composition(converse(X0),complement(composition(X0,sk3))),top),
inference(superposition,[],[f26566,f117089]) ).
fof(f123951,plain,
! [X0] : join(sk3,complement(sk3)) = join(top,composition(converse(X0),complement(composition(X0,sk3)))),
inference(forward_demodulation,[],[f123943,f1]) ).
fof(f123963,plain,
! [X0] : join(converse(sk3),complement(converse(sk3))) = join(top,composition(converse(X0),complement(composition(X0,converse(sk3))))),
inference(forward_demodulation,[],[f123931,f1]) ).
fof(f123977,plain,
! [X0] : top = join(top,composition(converse(X0),complement(composition(X0,sk3)))),
inference(forward_demodulation,[],[f123951,f15]) ).
fof(f123985,plain,
! [X0] : top = join(top,composition(converse(X0),complement(composition(X0,converse(sk3))))),
inference(forward_demodulation,[],[f123963,f15]) ).
fof(f124080,plain,
top = join(top,complement(composition(one,sk3))),
inference(superposition,[],[f123977,f218]) ).
fof(f124148,plain,
top = join(top,complement(sk3)),
inference(forward_demodulation,[],[f124080,f230]) ).
fof(f124228,plain,
top = join(converse(join(complement(sk3),top)),complement(converse(top))),
inference(superposition,[],[f108951,f124148]) ).
fof(f124258,plain,
top = join(complement(converse(top)),converse(join(top,complement(sk3)))),
inference(forward_demodulation,[],[f124228,f4565]) ).
fof(f124289,plain,
top = join(top,converse(complement(sk3))),
inference(forward_demodulation,[],[f124258,f68262]) ).
fof(f124422,plain,
converse(top) = join(complement(sk3),converse(top)),
inference(superposition,[],[f47,f124289]) ).
fof(f127531,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f4,f1]) ).
fof(f131764,plain,
! [X0,X1] : join(complement(join(X0,complement(X1))),complement(join(complement(X1),complement(X0)))) = X1,
inference(superposition,[],[f127531,f1]) ).
fof(f131869,plain,
! [X0] : join(complement(join(complement(X0),complement(X0))),complement(top)) = X0,
inference(superposition,[],[f127531,f15]) ).
fof(f131873,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(X0)))) = X0,
inference(forward_demodulation,[],[f131869,f1]) ).
fof(f131916,plain,
! [X0] : join(zero,complement(join(complement(X0),complement(X0)))) = X0,
inference(forward_demodulation,[],[f131873,f33]) ).
fof(f155382,plain,
top = join(top,complement(composition(one,converse(sk3)))),
inference(superposition,[],[f123985,f218]) ).
fof(f155457,plain,
top = join(top,complement(converse(sk3))),
inference(forward_demodulation,[],[f155382,f230]) ).
fof(f155542,plain,
join(complement(converse(top)),converse(top)) = join(top,converse(complement(converse(sk3)))),
inference(superposition,[],[f68262,f155457]) ).
fof(f155573,plain,
join(complement(converse(top)),converse(top)) = join(complement(sk3),converse(top)),
inference(forward_demodulation,[],[f155542,f44501]) ).
fof(f155608,plain,
converse(top) = join(complement(converse(top)),converse(top)),
inference(forward_demodulation,[],[f155573,f124422]) ).
fof(f155629,plain,
converse(top) = join(converse(top),complement(converse(top))),
inference(forward_demodulation,[],[f155608,f1]) ).
fof(f155642,plain,
top = converse(top),
inference(forward_demodulation,[],[f155629,f15]) ).
fof(f176814,plain,
! [X0] : top = join(X0,join(converse(complement(converse(X0))),complement(converse(top)))),
inference(superposition,[],[f447,f46]) ).
fof(f177713,plain,
! [X0,X1] : converse(top) = join(X0,converse(join(X1,complement(join(converse(X0),X1))))),
inference(superposition,[],[f35,f447]) ).
fof(f177723,plain,
! [X0,X1] : top = join(X0,converse(join(X1,complement(join(converse(X0),X1))))),
inference(forward_demodulation,[],[f177713,f155642]) ).
fof(f178528,plain,
! [X0] : top = join(X0,join(complement(converse(top)),converse(complement(converse(X0))))),
inference(forward_demodulation,[],[f176814,f1]) ).
fof(f179212,plain,
! [X0] : top = join(X0,join(complement(top),converse(complement(converse(X0))))),
inference(forward_demodulation,[],[f178528,f155642]) ).
fof(f179562,plain,
! [X0] : top = join(X0,join(zero,converse(complement(converse(X0))))),
inference(forward_demodulation,[],[f179212,f33]) ).
fof(f180347,plain,
! [X0] : converse(top) = join(X0,converse(join(zero,converse(complement(converse(converse(X0))))))),
inference(superposition,[],[f35,f179562]) ).
fof(f180357,plain,
! [X0] : converse(top) = join(X0,join(converse(zero),complement(converse(converse(X0))))),
inference(forward_demodulation,[],[f180347,f36]) ).
fof(f180640,plain,
! [X0] : converse(top) = join(X0,join(converse(zero),complement(X0))),
inference(forward_demodulation,[],[f180357,f10]) ).
fof(f180892,plain,
! [X0] : top = join(X0,join(converse(zero),complement(X0))),
inference(forward_demodulation,[],[f180640,f155642]) ).
fof(f181711,plain,
! [X0] : join(X0,top) = join(top,join(converse(zero),complement(complement(X0)))),
inference(superposition,[],[f434,f180892]) ).
fof(f181715,plain,
! [X0] : join(X0,top) = join(top,complement(complement(X0))),
inference(forward_demodulation,[],[f181711,f5537]) ).
fof(f207208,plain,
! [X0] : top = join(X0,converse(join(complement(converse(X0)),complement(top)))),
inference(superposition,[],[f177723,f15]) ).
fof(f207713,plain,
! [X0] : top = join(X0,converse(join(complement(top),complement(converse(X0))))),
inference(forward_demodulation,[],[f207208,f92]) ).
fof(f208172,plain,
! [X0] : top = join(X0,converse(join(zero,complement(converse(X0))))),
inference(forward_demodulation,[],[f207713,f33]) ).
fof(f209272,plain,
! [X0] : converse(top) = join(X0,converse(converse(join(zero,complement(converse(converse(X0))))))),
inference(superposition,[],[f35,f208172]) ).
fof(f209282,plain,
! [X0] : converse(top) = join(X0,join(zero,complement(converse(converse(X0))))),
inference(forward_demodulation,[],[f209272,f10]) ).
fof(f209563,plain,
! [X0] : converse(top) = join(X0,join(zero,complement(X0))),
inference(forward_demodulation,[],[f209282,f10]) ).
fof(f209802,plain,
! [X0] : top = join(X0,join(zero,complement(X0))),
inference(forward_demodulation,[],[f209563,f155642]) ).
fof(f210220,plain,
! [X0] : top = join(join(complement(X0),complement(X0)),X0),
inference(superposition,[],[f209802,f131916]) ).
fof(f210692,plain,
! [X0] : top = join(complement(X0),join(complement(X0),X0)),
inference(forward_demodulation,[],[f210220,f2]) ).
fof(f210871,plain,
! [X0] : top = join(complement(X0),join(X0,complement(X0))),
inference(forward_demodulation,[],[f210692,f1]) ).
fof(f211016,plain,
! [X0] : top = join(complement(X0),top),
inference(forward_demodulation,[],[f210871,f15]) ).
fof(f211123,plain,
! [X0] : top = join(top,complement(X0)),
inference(forward_demodulation,[],[f211016,f1]) ).
fof(f211211,plain,
! [X0] : top = join(X0,top),
inference(superposition,[],[f211123,f181715]) ).
fof(f211560,plain,
! [X0] : top = join(top,X0),
inference(superposition,[],[f211211,f1]) ).
fof(f211868,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(top)))) = X0,
inference(superposition,[],[f127531,f211211]) ).
fof(f211871,plain,
! [X0] : join(zero,complement(join(complement(X0),zero))) = X0,
inference(forward_demodulation,[],[f211868,f33]) ).
fof(f212098,plain,
! [X0] : join(zero,complement(join(zero,complement(X0)))) = X0,
inference(forward_demodulation,[],[f211871,f1]) ).
fof(f214482,plain,
zero = join(zero,complement(top)),
inference(superposition,[],[f212098,f15]) ).
fof(f214506,plain,
zero = join(zero,zero),
inference(forward_demodulation,[],[f214482,f33]) ).
fof(f214517,plain,
! [X0] : join(zero,X0) = join(zero,join(zero,X0)),
inference(superposition,[],[f2,f214506]) ).
fof(f214555,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f214517,f131916]) ).
fof(f215235,plain,
! [X0] : complement(join(zero,complement(X0))) = X0,
inference(superposition,[],[f212098,f214555]) ).
fof(f215613,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f215235,f214555]) ).
fof(f216674,plain,
! [X0] : complement(X0) = join(zero,complement(join(X0,X0))),
inference(superposition,[],[f131916,f215613]) ).
fof(f216690,plain,
! [X0] : complement(X0) = complement(join(X0,X0)),
inference(forward_demodulation,[],[f216674,f214555]) ).
fof(f217572,plain,
! [X0] : complement(complement(X0)) = join(X0,X0),
inference(superposition,[],[f215613,f216690]) ).
fof(f217573,plain,
! [X0] : join(X0,X0) = X0,
inference(forward_demodulation,[],[f217572,f215613]) ).
fof(f218192,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(superposition,[],[f2,f217573]) ).
fof(f220789,plain,
! [X2,X0,X1] : join(top,X2) = join(join(X1,complement(join(X0,X1))),join(X0,X2)),
inference(superposition,[],[f435,f447]) ).
fof(f220846,plain,
! [X0,X1] : join(top,X1) = join(complement(X0),join(X0,X1)),
inference(superposition,[],[f435,f15]) ).
fof(f222901,plain,
! [X0,X1] : top = join(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f220846,f211560]) ).
fof(f222958,plain,
! [X2,X0,X1] : join(top,X2) = join(X1,join(complement(join(X0,X1)),join(X0,X2))),
inference(forward_demodulation,[],[f220789,f2]) ).
fof(f223742,plain,
! [X2,X0,X1] : top = join(X1,join(complement(join(X0,X1)),join(X0,X2))),
inference(forward_demodulation,[],[f222958,f211560]) ).
fof(f226238,plain,
! [X0,X1] : join(complement(top),complement(join(complement(X0),complement(join(X0,X1))))) = X0,
inference(superposition,[],[f127531,f222901]) ).
fof(f226253,plain,
! [X0,X1] : join(zero,complement(join(complement(X0),complement(join(X0,X1))))) = X0,
inference(forward_demodulation,[],[f226238,f33]) ).
fof(f226776,plain,
! [X0,X1] : complement(join(complement(X0),complement(join(X0,X1)))) = X0,
inference(forward_demodulation,[],[f226253,f214555]) ).
fof(f245307,plain,
! [X0,X1] : join(X0,X1) = join(X1,join(X0,X1)),
inference(superposition,[],[f218192,f1]) ).
fof(f272077,plain,
sk1 = complement(join(complement(sk1),complement(sk2))),
inference(superposition,[],[f226776,f18]) ).
fof(f272078,plain,
sk1 = complement(join(complement(sk1),complement(sk3))),
inference(superposition,[],[f226776,f20]) ).
fof(f272222,plain,
! [X0,X1] : join(zero,complement(join(X0,X0))) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f131916,f226776]) ).
fof(f272256,plain,
! [X0,X1] : complement(join(X0,X0)) = join(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f272222,f214555]) ).
fof(f272326,plain,
sk1 = complement(join(complement(sk3),complement(sk1))),
inference(forward_demodulation,[],[f272078,f1]) ).
fof(f272327,plain,
sk1 = complement(join(complement(sk2),complement(sk1))),
inference(forward_demodulation,[],[f272077,f1]) ).
fof(f272729,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f272256,f216690]) ).
fof(f273885,plain,
join(complement(sk3),complement(sk1)) = join(zero,complement(join(sk1,sk1))),
inference(superposition,[],[f131916,f272326]) ).
fof(f273921,plain,
join(complement(sk3),complement(sk1)) = complement(join(sk1,sk1)),
inference(forward_demodulation,[],[f273885,f214555]) ).
fof(f273952,plain,
complement(sk1) = join(complement(sk3),complement(sk1)),
inference(forward_demodulation,[],[f273921,f216690]) ).
fof(f274027,plain,
join(complement(sk2),complement(sk1)) = join(zero,complement(join(sk1,sk1))),
inference(superposition,[],[f131916,f272327]) ).
fof(f274063,plain,
join(complement(sk2),complement(sk1)) = complement(join(sk1,sk1)),
inference(forward_demodulation,[],[f274027,f214555]) ).
fof(f274094,plain,
complement(sk1) = join(complement(sk2),complement(sk1)),
inference(forward_demodulation,[],[f274063,f216690]) ).
fof(f274167,plain,
! [X0] : join(complement(sk1),X0) = join(complement(sk3),join(complement(sk1),X0)),
inference(superposition,[],[f2,f273952]) ).
fof(f274276,plain,
! [X0] : join(complement(sk1),X0) = join(complement(sk2),join(complement(sk1),X0)),
inference(superposition,[],[f2,f274094]) ).
fof(f356998,plain,
! [X0,X1] : complement(join(X1,X0)) = complement(join(X0,join(join(X1,X0),X1))),
inference(superposition,[],[f216690,f448]) ).
fof(f357521,plain,
! [X0,X1] : complement(join(X1,X0)) = complement(join(X0,join(X1,join(X0,X1)))),
inference(forward_demodulation,[],[f356998,f2]) ).
fof(f359831,plain,
! [X0,X1] : complement(join(X1,X0)) = complement(join(X0,join(X0,X1))),
inference(forward_demodulation,[],[f357521,f245307]) ).
fof(f361328,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f359831,f218192]) ).
fof(f364498,plain,
! [X2,X0,X1] : top = join(X1,join(X0,join(X2,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f223742,f448]) ).
fof(f1121537,plain,
! [X0] : top = join(X0,join(complement(sk1),complement(join(complement(sk3),X0)))),
inference(superposition,[],[f364498,f274167]) ).
fof(f1198026,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(join(join(complement(X0),complement(X1)),complement(join(X1,complement(X0))))),complement(X0)),
inference(superposition,[],[f131764,f131764]) ).
fof(f1198364,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),complement(join(join(complement(X0),complement(X1)),complement(join(X1,complement(X0)))))),
inference(forward_demodulation,[],[f1198026,f1]) ).
fof(f1198765,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),complement(join(complement(X0),join(complement(X1),complement(join(X1,complement(X0))))))),
inference(forward_demodulation,[],[f1198364,f2]) ).
fof(f1199008,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),complement(join(complement(X0),complement(X1)))),
inference(forward_demodulation,[],[f1198765,f272729]) ).
fof(f1214204,plain,
! [X0,X1] : join(X1,X0) = join(X0,complement(join(X0,complement(X1)))),
inference(superposition,[],[f1199008,f226776]) ).
fof(f1215252,plain,
! [X0,X1] : join(X0,X1) = join(X1,complement(join(complement(X0),X1))),
inference(superposition,[],[f1214204,f1]) ).
fof(f1449454,plain,
top = join(complement(sk1),complement(join(complement(sk3),complement(sk2)))),
inference(superposition,[],[f274276,f1121537]) ).
fof(f1450656,plain,
top = join(complement(sk1),complement(join(complement(sk2),complement(sk3)))),
inference(forward_demodulation,[],[f1449454,f361328]) ).
fof(f1455090,plain,
join(sk1,complement(join(complement(sk2),complement(sk3)))) = join(complement(join(complement(sk2),complement(sk3))),complement(top)),
inference(superposition,[],[f1215252,f1450656]) ).
fof(f1455259,plain,
join(sk1,complement(join(complement(sk2),complement(sk3)))) = join(complement(top),complement(join(complement(sk2),complement(sk3)))),
inference(forward_demodulation,[],[f1455090,f1]) ).
fof(f1455391,plain,
join(sk1,complement(join(complement(sk2),complement(sk3)))) = join(zero,complement(join(complement(sk2),complement(sk3)))),
inference(forward_demodulation,[],[f1455259,f33]) ).
fof(f1455491,plain,
complement(join(complement(sk2),complement(sk3))) = join(sk1,complement(join(complement(sk2),complement(sk3)))),
inference(forward_demodulation,[],[f1455391,f214555]) ).
fof(f1455560,plain,
$false,
inference(forward_subsumption_resolution,[],[f1455491,f24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL047-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n008.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 22:57:54 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 23.94/3.89 % (1705183)Will run a generic schedule for satisfiability detection.
% 23.94/3.89 % (1705199)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=288448147:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 23.94/3.89 % (1705195)% WARNING: option uhcvi not known.
% 23.94/3.89 % (1705198)dis+10_1_sil=32000:sp=arity:random_seed=2267088792:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 23.94/3.89 % (1705195)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4130857439:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 23.94/3.89 % (1705194)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1503448795_2999 on theBenchmark for (2999ds/0Mi)
% 23.94/3.89 % (1705197)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=139545181:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 23.94/3.89 % (1705200)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3425871596:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 23.94/3.89 % TRYING [1]
% 23.94/3.89 % TRYING [2]
% 23.94/3.89 % TRYING [3]
% 23.94/3.89 % (1705201)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3666435276:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 23.94/3.89 % TRYING [4]
% 23.94/3.89 % (1705199)Instruction limit reached!
% 23.94/3.89 % (1705199)------------------------------
% 23.94/3.89 % (1705199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/3.89 % (1705199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/3.89 % (1705199)CaDiCaL version: 2.1.3
% 23.94/3.89 % (1705199)Termination reason: Instruction limit
% 23.94/3.89 % (1705199)Termination phase: Saturation
% 23.94/3.89 % (1705199)Time elapsed: 0.038 s
% 23.94/3.89 % (1705199)Peak memory usage: 12 MB
% 23.94/3.89 % (1705199)Instructions burned: 116 (million)
% 23.94/3.89 % (1705218)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4253082575:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 23.94/3.89 % TRYING [1]
% 23.94/3.89 % TRYING [2]
% 23.94/3.89 % TRYING [3]
% 23.94/3.89 % TRYING [4]
% 23.94/3.89 % (1705198)Instruction limit reached!
% 23.94/3.89 % (1705198)------------------------------
% 23.94/3.89 % (1705198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/3.89 % (1705198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/3.89 % (1705198)CaDiCaL version: 2.1.3
% 23.94/3.89 % (1705198)Termination reason: Instruction limit
% 23.94/3.89 % (1705198)Termination phase: Saturation
% 23.94/3.89 % (1705198)Time elapsed: 0.058 s
% 23.94/3.89 % (1705198)Peak memory usage: 12 MB
% 23.94/3.89 % (1705198)Instructions burned: 103 (million)
% 23.94/3.89 % TRYING [5]
% 23.94/3.89 % TRYING [5]
% 23.94/3.89 % (1705224)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=533266053:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 23.94/3.89 % (1705200)Instruction limit reached!
% 23.94/3.89 % (1705200)------------------------------
% 23.94/3.89 % (1705200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/3.89 % (1705200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/3.89 % (1705200)CaDiCaL version: 2.1.3
% 23.94/3.89 % (1705200)Termination reason: Instruction limit
% 23.94/3.89 % (1705200)Termination phase: Saturation
% 23.94/3.89 % (1705200)Time elapsed: 0.076 s
% 23.94/3.89 % (1705200)Peak memory usage: 12 MB
% 23.94/3.89 % (1705200)Instructions burned: 132 (million)
% 23.94/3.89 % (1705230)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=3863110961:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 23.94/3.89 % (1705201)Instruction limit reached!
% 23.94/3.89 % (1705201)------------------------------
% 23.94/3.89 % (1705201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/3.89 % (1705201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/3.89 % (1705201)CaDiCaL version: 2.1.3
% 23.94/3.89 % (1705201)Termination reason: Instruction limit
% 23.94/3.89 % (1705201)Termination phase: Saturation
% 23.94/3.89 % (1705201)Time elapsed: 0.103 s
% 23.94/3.89 % (1705201)Peak memory usage: 13 MB
% 23.94/3.89 % (1705201)Instructions burned: 159 (million)
% 23.94/3.89 % (1705233)ott-21_1_sil=16000:fs=off:random_seed=400533428:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 23.94/3.89 % (1705224)Instruction limit reached!
% 23.94/3.89 % (1705224)------------------------------
% 23.94/3.89 % (1705224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.11/11.19 % (1705224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.11/11.19 % (1705224)CaDiCaL version: 2.1.3
% 76.11/11.19 % (1705224)Termination reason: Instruction limit
% 76.11/11.19 % (1705224)Termination phase: Saturation
% 76.11/11.19 % (1705224)Time elapsed: 0.085 s
% 76.11/11.19 % (1705224)Peak memory usage: 13 MB
% 76.11/11.19 % (1705224)Instructions burned: 131 (million)
% 76.11/11.19 % (1705245)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2245197011:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 76.11/11.19 % TRYING [6]
% 76.11/11.19 % (1705233)Instruction limit reached!
% 76.11/11.19 % (1705233)------------------------------
% 76.11/11.19 % (1705233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.11/11.19 % (1705233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.11/11.19 % (1705233)CaDiCaL version: 2.1.3
% 76.11/11.19 % (1705233)Termination reason: Instruction limit
% 76.11/11.19 % (1705233)Termination phase: Saturation
% 76.11/11.19 % (1705233)Time elapsed: 0.084 s
% 76.11/11.19 % (1705233)Peak memory usage: 12 MB
% 76.11/11.19 % (1705233)Instructions burned: 181 (million)
% 76.11/11.19 % (1705218)Instruction limit reached!
% 76.11/11.19 % (1705218)------------------------------
% 76.11/11.19 % (1705218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.11/11.19 % (1705218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.11/11.19 % (1705218)CaDiCaL version: 2.1.3
% 76.11/11.19 % (1705218)Termination reason: Instruction limit
% 76.11/11.19 % (1705218)Termination phase: Finite model building constraint generation
% 76.11/11.19 % (1705218)Time elapsed: 0.186 s
% 76.11/11.19 % (1705218)Peak memory usage: 24 MB
% 76.11/11.19 % (1705218)Instructions burned: 718 (million)
% 76.11/11.19 % TRYING [6]
% 76.11/11.19 % (1705247)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=78970542:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 76.11/11.19 % (1705248)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3330168169:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 76.11/11.19 % TRYING [1]
% 76.11/11.19 % TRYING [2]
% 76.11/11.19 % TRYING [3]
% 76.11/11.19 % TRYING [4]
% 76.11/11.19 % TRYING [5]
% 76.11/11.19 % (1705245)Instruction limit reached!
% 76.11/11.19 % (1705245)------------------------------
% 76.11/11.19 % (1705245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.11/11.19 % (1705245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.11/11.19 % (1705245)CaDiCaL version: 2.1.3
% 76.11/11.19 % (1705245)Termination reason: Instruction limit
% 76.11/11.19 % (1705245)Termination phase: Saturation
% 76.11/11.19 % (1705245)Time elapsed: 0.259 s
% 76.11/11.19 % (1705245)Peak memory usage: 15 MB
% 76.11/11.19 % (1705245)Instructions burned: 478 (million)
% 76.11/11.19 % (1705271)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1726582064:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 76.11/11.19 % (1705230)Instruction limit reached!
% 76.11/11.19 % (1705230)------------------------------
% 76.11/11.19 % (1705230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.11/11.19 % (1705230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.11/11.19 % (1705230)CaDiCaL version: 2.1.3
% 76.11/11.19 % (1705230)Termination reason: Instruction limit
% 76.11/11.19 % (1705230)Termination phase: Saturation
% 76.11/11.19 % (1705230)Time elapsed: 0.396 s
% 76.11/11.19 % (1705230)Peak memory usage: 18 MB
% 76.11/11.19 % (1705230)Instructions burned: 685 (million)
% 76.11/11.19 % TRYING [6]
% 76.11/11.19 % (1705280)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=1858091441:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 76.11/11.19 % TRYING [14]
% 76.11/11.19 % (1705247)Instruction limit reached!
% 76.11/11.19 % (1705247)------------------------------
% 76.11/11.19 % (1705247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.11/11.19 % (1705247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.11/11.19 % (1705247)CaDiCaL version: 2.1.3
% 76.11/11.19 % (1705247)Termination reason: Instruction limit
% 76.11/11.19 % (1705247)Termination phase: Finite model building SAT solving
% 76.11/11.19 % (1705247)Time elapsed: 0.464 s
% 76.11/11.19 % (1705247)Peak memory usage: 22 MB
% 76.11/11.19 % (1705247)Instructions burned: 866 (million)
% 76.11/11.19 % (1705248)Instruction limit reached!
% 76.11/11.19 % (1705248)------------------------------
% 76.11/11.19 % (1705248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.70/22.25 % (1705248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.70/22.25 % (1705248)CaDiCaL version: 2.1.3
% 154.70/22.25 % (1705248)Termination reason: Instruction limit
% 154.70/22.25 % (1705248)Termination phase: Saturation
% 154.70/22.25 % (1705248)Time elapsed: 0.467 s
% 154.70/22.25 % (1705248)Peak memory usage: 21 MB
% 154.70/22.25 % (1705248)Instructions burned: 1181 (million)
% 154.70/22.25 % (1705291)fmb+10_1_sil=64000:random_seed=1709457638:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 154.70/22.25 % TRYING [1]
% 154.70/22.25 % TRYING [2]
% 154.70/22.25 % TRYING [3]
% 154.70/22.25 % (1705290)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3286655562:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 154.70/22.25 % TRYING [4]
% 154.70/22.25 % TRYING [5]
% 154.70/22.25 % TRYING [6]
% 154.70/22.25 % (1705280)Instruction limit reached!
% 154.70/22.25 % (1705280)------------------------------
% 154.70/22.25 % (1705280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.70/22.25 % (1705280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.70/22.25 % (1705280)CaDiCaL version: 2.1.3
% 154.70/22.25 % (1705280)Termination reason: Instruction limit
% 154.70/22.25 % (1705280)Termination phase: Saturation
% 154.70/22.25 % (1705280)Time elapsed: 0.619 s
% 154.70/22.25 % (1705280)Peak memory usage: 16 MB
% 154.70/22.25 % (1705280)Instructions burned: 692 (million)
% 154.70/22.25 % (1705271)Instruction limit reached!
% 154.70/22.25 % (1705271)------------------------------
% 154.70/22.25 % (1705271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.70/22.25 % (1705271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.70/22.25 % (1705271)CaDiCaL version: 2.1.3
% 154.70/22.25 % (1705271)Termination reason: Instruction limit
% 154.70/22.25 % (1705271)Termination phase: Finite model building constraint generation
% 154.70/22.25 % (1705271)Time elapsed: 0.694 s
% 154.70/22.25 % (1705271)Peak memory usage: 82 MB
% 154.70/22.25 % (1705271)Instructions burned: 889 (million)
% 154.70/22.25 % (1705298)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1075349677:i=9515:nm=5_2988 on theBenchmark for (2988ds/9515Mi)
% 154.70/22.25 % TRYING [20]
% 154.70/22.25 % (1705299)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2400233783:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 154.70/22.25 % TRYING [8]
% 154.70/22.25 % TRYING [7]
% 154.70/22.25 % TRYING [7]
% 154.70/22.25 % (1705290)Instruction limit reached!
% 154.70/22.25 % (1705290)------------------------------
% 154.70/22.25 % (1705290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.70/22.25 % (1705290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.70/22.25 % (1705290)CaDiCaL version: 2.1.3
% 154.70/22.25 % (1705290)Termination reason: Instruction limit
% 154.70/22.25 % (1705290)Termination phase: Saturation
% 154.70/22.25 % (1705290)Time elapsed: 0.802 s
% 154.70/22.25 % (1705290)Peak memory usage: 18 MB
% 154.70/22.25 % (1705290)Instructions burned: 879 (million)
% 154.70/22.25 % (1705310)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4271079821:i=5131_2984 on theBenchmark for (2984ds/5131Mi)
% 154.70/22.25 % (1705299)Instruction limit reached!
% 154.70/22.25 % (1705299)------------------------------
% 154.70/22.25 % (1705299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.70/22.25 % (1705299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.70/22.25 % (1705299)CaDiCaL version: 2.1.3
% 154.70/22.25 % (1705299)Termination reason: Instruction limit
% 154.70/22.25 % (1705299)Termination phase: Finite model building SAT solving
% 154.70/22.25 % (1705299)Time elapsed: 0.745 s
% 154.70/22.25 % (1705299)Peak memory usage: 65 MB
% 154.70/22.25 % (1705299)Instructions burned: 921 (million)
% 154.70/22.25 % (1705314)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3215265215:i=1472:ins=7:fdi=8:gsp=on_2979 on theBenchmark for (2979ds/1472Mi)
% 154.70/22.25 % TRYING [8]
% 154.70/22.25 % (1705314)Instruction limit reached!
% 154.70/22.25 % (1705314)------------------------------
% 154.70/22.25 % (1705314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.70/22.25 % (1705314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.70/22.25 % (1705314)CaDiCaL version: 2.1.3
% 154.70/22.25 % (1705314)Termination reason: Instruction limit
% 154.70/22.25 % (1705314)Termination phase: Saturation
% 154.70/22.25 % (1705314)Time elapsed: 1.392 s
% 154.70/22.25 % (1705314)Peak memory usage: 29 MB
% 154.70/22.25 % (1705314)Instructions burned: 1473 (million)
% 154.70/22.25 % (1705324)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1602383284:i=6324_2965 on theBenchmark for (2965ds/6324Mi)
% 188.89/38.52 % TRYING [77]
% 188.89/38.52 % (1705310)Instruction limit reached!
% 188.89/38.52 % (1705310)------------------------------
% 188.89/38.52 % (1705310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.89/38.52 % (1705310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.89/38.52 % (1705310)CaDiCaL version: 2.1.3
% 188.89/38.52 % (1705310)Termination reason: Instruction limit
% 188.89/38.52 % (1705310)Termination phase: Saturation
% 188.89/38.52 % (1705310)Time elapsed: 4.680 s
% 188.89/38.52 % (1705310)Peak memory usage: 51 MB
% 188.89/38.52 % (1705310)Instructions burned: 5131 (million)
% 188.89/38.52 % (1705328)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2092925985:fmbsr=2.30978:i=2174_2936 on theBenchmark for (2936ds/2174Mi)
% 188.89/38.52 % TRYING [16]
% 188.89/38.52 % TRYING [8]
% 188.89/38.52 % TRYING [9]
% 188.89/38.52 % (1705328)Instruction limit reached!
% 188.89/38.52 % (1705328)------------------------------
% 188.89/38.52 % (1705328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.89/38.52 % (1705328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.89/38.52 % (1705328)CaDiCaL version: 2.1.3
% 188.89/38.52 % (1705328)Termination reason: Instruction limit
% 188.89/38.52 % (1705328)Termination phase: Finite model building constraint generation
% 188.89/38.52 % (1705328)Time elapsed: 1.521 s
% 188.89/38.52 % (1705328)Peak memory usage: 135 MB
% 188.89/38.52 % (1705328)Instructions burned: 2175 (million)
% 188.89/38.52 % (1705332)ott-2_1_sil=16000:newcnf=on:random_seed=100595768:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2920 on theBenchmark for (2920ds/869Mi)
% 188.89/38.52 % (1705298)Instruction limit reached!
% 188.89/38.52 % (1705298)------------------------------
% 188.89/38.52 % (1705298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.89/38.52 % (1705298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.89/38.52 % (1705298)CaDiCaL version: 2.1.3
% 188.89/38.52 % (1705298)Termination reason: Instruction limit
% 188.89/38.52 % (1705298)Termination phase: Finite model building constraint generation
% 188.89/38.52 % (1705298)Time elapsed: 6.939 s
% 188.89/38.52 % (1705298)Peak memory usage: 670 MB
% 188.89/38.52 % (1705298)Instructions burned: 9515 (million)
% 188.89/38.52 % (1705324)Instruction limit reached!
% 188.89/38.52 % (1705324)------------------------------
% 188.89/38.52 % (1705324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.89/38.52 % (1705324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.89/38.52 % (1705324)CaDiCaL version: 2.1.3
% 188.89/38.52 % (1705324)Termination reason: Instruction limit
% 188.89/38.52 % (1705324)Termination phase: Finite model building constraint generation
% 188.89/38.52 % (1705324)Time elapsed: 4.758 s
% 188.89/38.52 % (1705324)Peak memory usage: 515 MB
% 188.89/38.52 % (1705324)Instructions burned: 6324 (million)
% 188.89/38.52 % (1705334)ott+10_1_sil=32000:tgt=ground:random_seed=1044733224:i=5114:av=off_2916 on theBenchmark for (2916ds/5114Mi)
% 188.89/38.52 % (1705335)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1691004499:i=54282_2916 on theBenchmark for (2916ds/54282Mi)
% 188.89/38.52 % TRYING [1]
% 188.89/38.52 % TRYING [2]
% 188.89/38.52 % TRYING [3]
% 188.89/38.52 % TRYING [4]
% 188.89/38.52 % TRYING [5]
% 188.89/38.52 % (1705332)Instruction limit reached!
% 188.89/38.52 % (1705332)------------------------------
% 188.89/38.52 % (1705332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.89/38.52 % (1705332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.89/38.52 % (1705332)CaDiCaL version: 2.1.3
% 188.89/38.52 % (1705332)Termination reason: Instruction limit
% 188.89/38.52 % (1705332)Termination phase: Saturation
% 188.89/38.52 % (1705332)Time elapsed: 0.797 s
% 188.89/38.52 % (1705332)Peak memory usage: 18 MB
% 188.89/38.52 % (1705332)Instructions burned: 869 (million)
% 188.89/38.52 % TRYING [6]
% 188.89/38.52 % (1705340)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4096132774:i=3512:aac=none_2912 on theBenchmark for (2912ds/3512Mi)
% 188.89/38.52 % TRYING [7]
% 188.89/38.52 % (1705291)Instruction limit reached!
% 188.89/38.52 % (1705291)------------------------------
% 188.89/38.52 % (1705291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.89/38.52 % (1705291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.89/38.52 % (1705291)CaDiCaL version: 2.1.3
% 188.89/38.52 % (1705291)Termination reason: Instruction limit
% 188.89/38.52 % (1705291)Termination phase: Finite model building SAT solving
% 188.89/38.52 % (1705291)Time elapsed: 10.008 s
% 188.89/38.52 % (1705291)Peak memory usage: 113 MB
% 188.89/38.52 % (1705291)Instructions burned: 22062 (million)
% 188.89/38.52 % (1705348)dis+21_1_sil=32000:sas=cadical:random_seed=2962831698:i=3773:amm=off_2892 on theBenchmark for (2892ds/3773Mi)
% 188.89/38.52 % (1705340)Instruction limit reached!
% 188.89/38.52 % (1705340)------------------------------
% 188.89/38.52 % (1705340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.89/38.52 % (1705340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.89/38.52 % (1705340)CaDiCaL version: 2.1.3
% 188.89/38.52 % (1705340)Termination reason: Instruction limit
% 188.89/38.52 % (1705340)Termination phase: Saturation
% 188.89/38.52 % (1705340)Time elapsed: 3.060 s
% 188.89/38.52 % (1705340)Peak memory usage: 40 MB
% 188.89/38.52 % (1705340)Instructions burned: 3512 (million)
% 188.89/38.52 % (1705350)ott+11_1_sil=16000:gs=on:random_seed=1131944204:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2881 on theBenchmark for (2881ds/2251Mi)
% 188.89/38.52 % (1705348)Instruction limit reached!
% 188.89/38.52 % (1705348)------------------------------
% 188.89/38.52 % (1705348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.89/38.52 % (1705348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.89/38.52 % (1705348)CaDiCaL version: 2.1.3
% 188.89/38.52 % (1705348)Termination reason: Instruction limit
% 188.89/38.52 % (1705348)Termination phase: Saturation
% 188.89/38.52 % (1705348)Time elapsed: 1.840 s
% 188.89/38.52 % (1705348)Peak memory usage: 42 MB
% 188.89/38.52 % (1705348)Instructions burned: 3775 (million)
% 188.89/38.52 % (1705352)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1130595922:fmbsr=1.6:i=67534_2873 on theBenchmark for (2873ds/67534Mi)
% 188.89/38.52 % TRYING [7]
% 188.89/38.52 % (1705334)Instruction limit reached!
% 188.89/38.52 % (1705334)------------------------------
% 188.89/38.52 % (1705334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.89/38.52 % (1705334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.89/38.52 % (1705334)CaDiCaL version: 2.1.3
% 188.89/38.52 % (1705334)Termination reason: Instruction limit
% 188.89/38.52 % (1705334)Termination phase: Saturation
% 188.89/38.52 % (1705334)Time elapsed: 4.847 s
% 188.89/38.52 % (1705334)Peak memory usage: 45 MB
% 188.89/38.52 % (1705334)Instructions burned: 5114 (million)
% 188.89/38.52 % (1705356)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1005796882:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2867 on theBenchmark for (2867ds/4591Mi)
% 188.89/38.52 % (1705350)Instruction limit reached!
% 188.89/38.52 % (1705350)------------------------------
% 188.89/38.52 % (1705350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.89/38.52 % (1705350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.89/38.52 % (1705350)CaDiCaL version: 2.1.3
% 188.89/38.52 % (1705350)Termination reason: Instruction limit
% 188.89/38.52 % (1705350)Termination phase: Saturation
% 188.89/38.52 % (1705350)Time elapsed: 2.064 s
% 188.89/38.52 % (1705350)Peak memory usage: 20 MB
% 188.89/38.52 % (1705350)Instructions burned: 2252 (million)
% 188.89/38.52 % (1705360)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3485192887:i=29340_2860 on theBenchmark for (2860ds/29340Mi)
% 188.89/38.52 % TRYING [8]
% 188.89/38.52 % (1705356)Instruction limit reached!
% 188.89/38.52 % (1705356)------------------------------
% 188.89/38.52 % (1705356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.89/38.52 % (1705356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.89/38.52 % (1705356)CaDiCaL version: 2.1.3
% 188.89/38.52 % (1705356)Termination reason: Instruction limit
% 188.89/38.52 % (1705356)Termination phase: Saturation
% 188.89/38.52 % (1705356)Time elapsed: 3.771 s
% 188.89/38.52 % (1705356)Peak memory usage: 31 MB
% 188.89/38.52 % (1705356)Instructions burned: 4592 (million)
% 188.89/38.52 % (1705366)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=444778897:i=5211_2829 on theBenchmark for (2829ds/5211Mi)
% 188.89/38.52 % TRYING [8]
% 188.89/38.52 % (1705366)Instruction limit reached!
% 188.89/38.52 % (1705366)------------------------------
% 188.89/38.52 % (1705366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.89/38.52 % (1705366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.89/38.52 % (1705366)CaDiCaL version: 2.1.3
% 188.89/38.52 % (1705366)Termination reason: Instruction limit
% 188.89/38.52 % (1705366)Termination phase: Saturation
% 188.89/38.52 % (1705366)Time elapsed: 4.721 s
% 188.89/38.52 % (1705366)Peak memory usage: 50 MB
% 188.89/38.52 % (1705366)Instructions burned: 5211 (million)
% 188.89/38.52 % (1705372)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3355727009:i=5497:nm=2_2782 on theBenchmark for (2782ds/5497Mi)
% 188.89/38.52 % TRYING [17]
% 188.89/38.52 % TRYING [9]
% 188.89/38.52 % (1705372)Instruction limit reached!
% 188.89/38.52 % (1705372)------------------------------
% 188.89/38.52 % (1705372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.89/38.52 % (1705372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.89/38.52 % (1705372)CaDiCaL version: 2.1.3
% 188.89/38.52 % (1705372)Termination reason: Instruction limit
% 188.89/38.52 % (1705372)Termination phase: Finite model building constraint generation
% 188.89/38.52 % (1705372)Time elapsed: 3.813 s
% 188.89/38.52 % (1705372)Peak memory usage: 392 MB
% 188.89/38.52 % (1705372)Instructions burned: 5498 (million)
% 188.89/38.52 % (1705376)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3140407999:fmbsr=2:i=46332_2742 on theBenchmark for (2742ds/46332Mi)
% 188.89/38.52 % TRYING [15]
% 188.89/38.52 % TRYING [9]
% 188.89/38.52 % TRYING [9]
% 188.89/38.52 % (1705197) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1705183-1705197"...
% 188.89/38.52 % (1705197)...printing done.
% 188.89/38.52 % (1705197)Refutation found. Thanks to Tanya!
% 188.89/38.52 % SZS status Unsatisfiable for theBenchmark
% 188.89/38.52 % SZS output start Proof for theBenchmark
% See solution above
% 188.89/38.53 % (1705197)------------------------------
% 188.89/38.53 % (1705197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.89/38.53 % (1705197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.89/38.53 % (1705197)CaDiCaL version: 2.1.3
% 188.89/38.53 % (1705197)Termination reason: Refutation
% 188.89/38.53 % (1705197)Time elapsed: 37.809 s
% 188.89/38.53 % (1705197)Peak memory usage: 283 MB
% 188.89/38.53 % (1705197)Instructions burned: 82111 (million)
% 188.89/38.53 % (1705183)Success in time 38.098 s
% 188.89/38.53 % Vampire exiting
%------------------------------------------------------------------------------