%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : REL030-4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:33:57 PM UTC 2026
% Result : Unsatisfiable 10.30s 2.35s
% Output : Refutation 11.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 72
% Number of leaves : 15
% Syntax : Number of formulae : 171 ( 161 unt; 0 def)
% Number of atoms : 181 ( 180 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 40 ( 30 ~; 10 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 10 ( 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 : 276 ( 276 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux1_join_commutativity_1) ).
fof(f2,axiom,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux2_join_associativity_2) ).
fof(f3,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux3_a_kind_of_de_Morgan_3) ).
fof(f4,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(reorient_equations,[],[f3]) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux4_definiton_of_meet_4) ).
fof(f6,plain,
! [X0,X1] : complement(join(complement(X0),complement(X1))) = meet(X0,X1),
inference(reorient_equations,[],[f5]) ).
fof(f7,axiom,
! [X2,X0,X1] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',composition_associativity_5) ).
fof(f8,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',composition_identity_6) ).
fof(f9,axiom,
! [X2,X0,X1] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',composition_distributivity_7) ).
fof(f10,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_idempotence_8) ).
fof(f11,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_additivity_9) ).
fof(f12,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_multiplicativity_10) ).
fof(f13,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_cancellativity_11) ).
fof(f14,plain,
! [X0,X1] : complement(X1) = join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)),
inference(reorient_equations,[],[f13]) ).
fof(f15,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_top_12) ).
fof(f16,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_zero_13) ).
fof(f23,negated_conjecture,
join(sk1,one) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_17) ).
fof(f24,plain,
one = join(sk1,one),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( join(meet(composition(sk1,sk2),complement(sk3)),meet(composition(sk1,sk2),complement(composition(sk1,sk3)))) != meet(composition(sk1,sk2),complement(composition(sk1,sk3)))
| join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,sk2),complement(sk3))) != meet(composition(sk1,sk2),complement(sk3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_18) ).
fof(f26,plain,
( meet(composition(sk1,sk2),complement(composition(sk1,sk3))) != join(meet(composition(sk1,sk2),complement(sk3)),meet(composition(sk1,sk2),complement(composition(sk1,sk3))))
| meet(composition(sk1,sk2),complement(sk3)) != join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,sk2),complement(sk3))) ),
inference(reorient_equations,[],[f25]) ).
fof(f27,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f16,f6]) ).
fof(f31,plain,
( complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) != join(complement(join(complement(composition(sk1,sk2)),complement(complement(sk3)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))))
| complement(join(complement(composition(sk1,sk2)),complement(complement(sk3)))) != join(complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(sk3))))) ),
inference(definition_unfolding,[],[f26,f6,f6,f6,f6,f6,f6]) ).
fof(f39,plain,
( complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) != join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))))
| complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != join(complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),complement(join(complement(complement(sk3)),complement(composition(sk1,sk2))))) ),
inference(superposition,[],[f31,f1]) ).
fof(f40,plain,
( complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) != join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))))
| complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))) ),
inference(forward_demodulation,[],[f39,f1]) ).
fof(f44,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X1),X0))) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f45,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(join(complement(join(complement(X0),complement(X1))),complement(complement(join(complement(X0),X1))))),complement(X0)),
inference(superposition,[],[f4,f4]) ).
fof(f51,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(superposition,[],[f1,f4]) ).
fof(f54,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(X0),complement(join(complement(join(complement(X0),complement(X1))),complement(complement(join(complement(X0),X1)))))),
inference(forward_demodulation,[],[f45,f1]) ).
fof(f55,plain,
! [X0,X1] : join(complement(join(complement(X1),X0)),complement(join(complement(X0),complement(X1)))) = X1,
inference(forward_demodulation,[],[f44,f1]) ).
fof(f58,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(X0),complement(join(complement(complement(join(complement(X0),X1))),complement(join(complement(X0),complement(X1)))))),
inference(forward_demodulation,[],[f54,f1]) ).
fof(f61,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[],[f12,f10]) ).
fof(f63,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(f75,plain,
! [X2,X0,X1] : join(X0,X2) = join(complement(join(complement(X0),complement(X1))),join(complement(join(complement(X0),X1)),X2)),
inference(superposition,[],[f2,f4]) ).
fof(f82,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f83,plain,
! [X2,X0,X1] : join(X0,X2) = join(complement(join(complement(X0),X1)),join(X2,complement(join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f75,f82]) ).
fof(f177,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = join(converse(composition(X0,X2)),converse(composition(X0,X1))),
inference(superposition,[],[f63,f12]) ).
fof(f185,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = converse(join(composition(X0,X2),composition(X0,X1))),
inference(forward_demodulation,[],[f177,f11]) ).
fof(f188,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = composition(converse(join(X2,X1)),converse(X0)),
inference(forward_demodulation,[],[f185,f11]) ).
fof(f190,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = converse(composition(X0,join(X2,X1))),
inference(forward_demodulation,[],[f188,f12]) ).
fof(f192,plain,
! [X0,X1] : complement(X1) = join(composition(X0,complement(composition(converse(X0),X1))),complement(X1)),
inference(superposition,[],[f14,f10]) ).
fof(f208,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(X0,complement(composition(converse(X0),X1)))),
inference(forward_demodulation,[],[f192,f1]) ).
fof(f330,plain,
zero = complement(top),
inference(superposition,[],[f27,f15]) ).
fof(f429,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f61,f8]) ).
fof(f445,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f429,f10]) ).
fof(f463,plain,
! [X0,X1] : composition(join(converse(one),X1),X0) = join(X0,composition(X1,X0)),
inference(superposition,[],[f9,f445]) ).
fof(f465,plain,
one = converse(one),
inference(superposition,[],[f8,f445]) ).
fof(f469,plain,
! [X0,X1] : join(X0,composition(X1,X0)) = composition(join(one,X1),X0),
inference(forward_demodulation,[],[f463,f465]) ).
fof(f481,plain,
! [X0] : composition(one,X0) = X0,
inference(superposition,[],[f445,f465]) ).
fof(f502,plain,
! [X0] : complement(X0) = join(complement(X0),complement(composition(converse(one),X0))),
inference(superposition,[],[f208,f481]) ).
fof(f505,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(forward_demodulation,[],[f502,f445]) ).
fof(f524,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = join(X0,complement(join(complement(X0),complement(X1)))),
inference(superposition,[],[f83,f505]) ).
fof(f528,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f524,f51]) ).
fof(f570,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f528,f27]) ).
fof(f572,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),X0) = join(X0,X0),
inference(superposition,[],[f83,f528]) ).
fof(f592,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = join(X0,X0),
inference(forward_demodulation,[],[f572,f1]) ).
fof(f644,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f1,f570]) ).
fof(f702,plain,
! [X0] : join(top,top) = join(top,complement(join(zero,X0))),
inference(superposition,[],[f592,f330]) ).
fof(f710,plain,
! [X0,X1] : join(X1,X1) = join(X1,complement(join(X0,complement(X1)))),
inference(superposition,[],[f592,f1]) ).
fof(f725,plain,
! [X0] : join(X0,X0) = X0,
inference(superposition,[],[f528,f592]) ).
fof(f762,plain,
! [X0,X1] : join(X1,complement(join(X0,complement(X1)))) = X1,
inference(forward_demodulation,[],[f710,f725]) ).
fof(f770,plain,
! [X0] : join(top,complement(X0)) = join(top,top),
inference(forward_demodulation,[],[f702,f644]) ).
fof(f785,plain,
! [X0] : top = join(top,complement(X0)),
inference(forward_demodulation,[],[f770,f725]) ).
fof(f860,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),top) = join(X0,top),
inference(superposition,[],[f83,f785]) ).
fof(f866,plain,
! [X0,X1] : join(X0,top) = join(top,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f860,f1]) ).
fof(f868,plain,
! [X0] : top = join(X0,top),
inference(forward_demodulation,[],[f866,f785]) ).
fof(f1010,plain,
! [X0] : join(complement(top),complement(join(complement(top),complement(X0)))) = X0,
inference(superposition,[],[f55,f868]) ).
fof(f1015,plain,
! [X0] : join(zero,complement(join(zero,complement(X0)))) = X0,
inference(forward_demodulation,[],[f1010,f330]) ).
fof(f1026,plain,
! [X0] : complement(join(zero,complement(X0))) = X0,
inference(forward_demodulation,[],[f1015,f644]) ).
fof(f1032,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f1026,f644]) ).
fof(f1051,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(complement(X1),X0))),
inference(superposition,[],[f55,f1032]) ).
fof(f1062,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(superposition,[],[f762,f1032]) ).
fof(f1272,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(join(complement(join(complement(X1),X0)),join(X0,X1))),complement(complement(X0))),
inference(superposition,[],[f55,f1051]) ).
fof(f1274,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(complement(join(X0,X1)),join(complement(X1),X0)))),
inference(superposition,[],[f4,f1051]) ).
fof(f1297,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(X0,join(complement(join(X0,X1)),complement(X1))))),
inference(forward_demodulation,[],[f1274,f82]) ).
fof(f1299,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(complement(X0)),complement(join(complement(join(complement(X1),X0)),join(X0,X1)))),
inference(forward_demodulation,[],[f1272,f1]) ).
fof(f1346,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(X0,join(complement(X1),complement(join(X0,X1)))))),
inference(forward_demodulation,[],[f1297,f1]) ).
fof(f1348,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(complement(X0)),complement(join(join(X0,X1),complement(join(complement(X1),X0))))),
inference(forward_demodulation,[],[f1299,f1]) ).
fof(f1382,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(X0,complement(X1)))),
inference(forward_demodulation,[],[f1346,f1062]) ).
fof(f1384,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(complement(X0)),complement(join(X0,join(X1,complement(join(complement(X1),X0)))))),
inference(forward_demodulation,[],[f1348,f2]) ).
fof(f1409,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,complement(X1)))),
inference(forward_demodulation,[],[f1382,f1032]) ).
fof(f1411,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(complement(X0)),complement(join(X0,join(X1,X1)))),
inference(forward_demodulation,[],[f1384,f592]) ).
fof(f1431,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(complement(X0)),complement(join(X0,X1))),
inference(forward_demodulation,[],[f1411,f725]) ).
fof(f1444,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f1431,f1032]) ).
fof(f1495,plain,
! [X2,X0,X1] : join(X1,join(complement(join(X1,X0)),X2)) = join(X2,join(complement(X0),X1)),
inference(superposition,[],[f82,f1444]) ).
fof(f1812,plain,
! [X0,X1] : join(X1,complement(X0)) = join(X1,complement(join(X1,X0))),
inference(superposition,[],[f1409,f1032]) ).
fof(f1849,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X0,join(complement(join(X0,complement(X1))),X2)),
inference(superposition,[],[f82,f1409]) ).
fof(f1888,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X2,join(complement(complement(X1)),X0)),
inference(forward_demodulation,[],[f1849,f1495]) ).
fof(f1937,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X2,join(X1,X0)),
inference(forward_demodulation,[],[f1888,f1032]) ).
fof(f2964,plain,
! [X2,X0,X1] : join(X0,complement(join(X0,join(X1,X2)))) = join(X0,complement(join(X2,X1))),
inference(superposition,[],[f1812,f1937]) ).
fof(f2980,plain,
! [X2,X0,X1] : join(complement(join(X1,X2)),X0) = join(X0,complement(join(X2,X1))),
inference(forward_demodulation,[],[f2964,f1444]) ).
fof(f3127,plain,
! [X2,X3,X0,X1] : join(complement(join(X0,X1)),complement(join(X2,X3))) = join(complement(join(X1,X0)),complement(join(X3,X2))),
inference(superposition,[],[f2980,f2980]) ).
fof(f3148,plain,
! [X2,X0,X1] : join(X0,complement(join(X2,X1))) = join(X0,complement(join(X1,X2))),
inference(superposition,[],[f1,f2980]) ).
fof(f3170,plain,
! [X0,X1] : complement(join(X1,X0)) = join(zero,complement(join(X0,X1))),
inference(superposition,[],[f570,f2980]) ).
fof(f3192,plain,
! [X0,X1] : complement(join(X1,X0)) = join(complement(join(X0,X1)),complement(join(X1,X0))),
inference(superposition,[],[f505,f2980]) ).
fof(f3225,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f3170,f644]) ).
fof(f3662,plain,
! [X2,X3,X0,X1] : join(X3,complement(join(X2,join(X0,X1)))) = join(X3,complement(join(X0,join(X1,X2)))),
inference(superposition,[],[f3148,f2]) ).
fof(f6402,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X0,X2)) = converse(converse(composition(X0,join(X1,X2)))),
inference(superposition,[],[f10,f190]) ).
fof(f6418,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = join(composition(X0,X1),composition(X0,X2)),
inference(forward_demodulation,[],[f6402,f10]) ).
fof(f6448,plain,
! [X0,X1] : join(composition(X0,X1),X0) = composition(X0,join(X1,one)),
inference(superposition,[],[f6418,f8]) ).
fof(f6474,plain,
! [X2,X0,X1] : join(complement(composition(X0,X2)),composition(X0,X1)) = join(composition(X0,X1),complement(composition(X0,join(X1,X2)))),
inference(superposition,[],[f1444,f6418]) ).
fof(f6481,plain,
! [X2,X3,X0,X1] : join(complement(join(composition(X0,X2),composition(X0,X1))),X3) = join(X3,complement(composition(X0,join(X1,X2)))),
inference(superposition,[],[f2980,f6418]) ).
fof(f6490,plain,
! [X2,X3,X0,X1] : join(X3,complement(composition(X0,join(X1,X2)))) = join(complement(composition(X0,join(X2,X1))),X3),
inference(forward_demodulation,[],[f6481,f6418]) ).
fof(f6499,plain,
! [X0,X1] : join(X0,composition(X0,X1)) = composition(X0,join(X1,one)),
inference(forward_demodulation,[],[f6448,f1]) ).
fof(f6885,plain,
! [X0] : composition(X0,one) = join(X0,composition(X0,sk1)),
inference(superposition,[],[f6499,f24]) ).
fof(f6968,plain,
! [X0] : join(X0,composition(X0,sk1)) = X0,
inference(forward_demodulation,[],[f6885,f8]) ).
fof(f7043,plain,
! [X0] : composition(one,X0) = join(X0,composition(composition(one,sk1),X0)),
inference(superposition,[],[f469,f6968]) ).
fof(f7044,plain,
! [X0] : composition(one,X0) = join(X0,composition(one,composition(sk1,X0))),
inference(forward_demodulation,[],[f7043,f7]) ).
fof(f7075,plain,
! [X0] : composition(one,X0) = join(X0,composition(sk1,X0)),
inference(forward_demodulation,[],[f7044,f481]) ).
fof(f7095,plain,
! [X0] : join(X0,composition(sk1,X0)) = X0,
inference(forward_demodulation,[],[f7075,f481]) ).
fof(f7112,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(composition(sk1,X0),X1)),
inference(superposition,[],[f2,f7095]) ).
fof(f7136,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(complement(join(composition(sk1,complement(X0)),X0)),complement(complement(X0))),
inference(superposition,[],[f1051,f7095]) ).
fof(f7145,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(complement(complement(X0)),complement(join(X0,composition(sk1,complement(X0))))),
inference(forward_demodulation,[],[f7136,f2980]) ).
fof(f7172,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(X0,complement(join(X0,composition(sk1,complement(X0))))),
inference(forward_demodulation,[],[f7145,f1032]) ).
fof(f7188,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(complement(composition(sk1,complement(X0))),X0),
inference(forward_demodulation,[],[f7172,f1444]) ).
fof(f7194,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(X0,complement(composition(sk1,complement(X0)))),
inference(forward_demodulation,[],[f7188,f1]) ).
fof(f7803,plain,
! [X0,X1] : join(X0,composition(sk1,X1)) = join(X0,composition(sk1,join(X0,X1))),
inference(superposition,[],[f7112,f6418]) ).
fof(f7804,plain,
! [X0,X1] : join(X1,complement(composition(sk1,join(X1,X0)))) = join(X1,join(complement(composition(sk1,X0)),composition(sk1,X1))),
inference(superposition,[],[f7112,f6474]) ).
fof(f7845,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,composition(sk1,X0))),
inference(superposition,[],[f1937,f7112]) ).
fof(f7937,plain,
! [X0,X1] : join(X1,complement(composition(sk1,X0))) = join(X1,complement(composition(sk1,join(X1,X0)))),
inference(forward_demodulation,[],[f7804,f7845]) ).
fof(f8003,plain,
! [X0] : join(X0,composition(sk1,complement(X0))) = join(X0,composition(sk1,top)),
inference(superposition,[],[f7803,f15]) ).
fof(f8064,plain,
! [X0,X1] : join(complement(composition(sk1,join(X0,X1))),X0) = join(X0,complement(join(X0,composition(sk1,X1)))),
inference(superposition,[],[f1444,f7803]) ).
fof(f8106,plain,
! [X0,X1] : join(complement(composition(sk1,join(X0,X1))),X0) = join(complement(composition(sk1,X1)),X0),
inference(forward_demodulation,[],[f8064,f1444]) ).
fof(f8156,plain,
! [X0,X1] : join(complement(composition(sk1,X1)),X0) = join(X0,complement(composition(sk1,join(X1,X0)))),
inference(forward_demodulation,[],[f8106,f6490]) ).
fof(f8204,plain,
! [X0] : join(X0,complement(composition(sk1,complement(X0)))) = join(X0,complement(join(X0,composition(sk1,top)))),
inference(superposition,[],[f1812,f8003]) ).
fof(f8214,plain,
! [X0] : join(complement(X0),complement(composition(sk1,complement(complement(X0))))) = join(complement(X0),complement(join(complement(complement(join(complement(X0),composition(sk1,top)))),complement(join(complement(X0),complement(composition(sk1,complement(complement(X0))))))))),
inference(superposition,[],[f58,f8003]) ).
fof(f8235,plain,
! [X0] : complement(composition(sk1,complement(complement(X0)))) = join(complement(X0),complement(join(complement(complement(join(complement(X0),composition(sk1,top)))),complement(complement(composition(sk1,complement(complement(X0)))))))),
inference(forward_demodulation,[],[f8214,f7194]) ).
fof(f8245,plain,
! [X0] : join(X0,complement(composition(sk1,complement(X0)))) = join(complement(composition(sk1,top)),X0),
inference(forward_demodulation,[],[f8204,f1444]) ).
fof(f8267,plain,
! [X0] : complement(composition(sk1,complement(complement(X0)))) = join(complement(X0),complement(join(complement(complement(composition(sk1,complement(complement(X0))))),complement(complement(join(complement(X0),composition(sk1,top))))))),
inference(forward_demodulation,[],[f8235,f3148]) ).
fof(f8276,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(complement(composition(sk1,top)),X0),
inference(forward_demodulation,[],[f8245,f7194]) ).
fof(f8292,plain,
! [X0] : complement(composition(sk1,complement(complement(X0)))) = join(complement(X0),complement(join(complement(complement(composition(sk1,complement(complement(X0))))),join(complement(X0),composition(sk1,top))))),
inference(forward_demodulation,[],[f8267,f1032]) ).
fof(f8310,plain,
! [X0] : complement(composition(sk1,complement(complement(X0)))) = join(complement(X0),complement(join(complement(X0),join(composition(sk1,top),complement(complement(composition(sk1,complement(complement(X0))))))))),
inference(forward_demodulation,[],[f8292,f3662]) ).
fof(f8322,plain,
! [X0] : complement(composition(sk1,complement(complement(X0)))) = join(complement(join(composition(sk1,top),complement(complement(composition(sk1,complement(complement(X0))))))),complement(X0)),
inference(forward_demodulation,[],[f8310,f1444]) ).
fof(f8330,plain,
! [X0] : complement(composition(sk1,complement(complement(X0)))) = join(complement(X0),complement(join(complement(complement(composition(sk1,complement(complement(X0))))),composition(sk1,top)))),
inference(forward_demodulation,[],[f8322,f2980]) ).
fof(f8336,plain,
! [X0] : complement(composition(sk1,complement(complement(X0)))) = join(complement(X0),complement(join(composition(sk1,top),complement(complement(composition(sk1,complement(complement(X0)))))))),
inference(forward_demodulation,[],[f8330,f3148]) ).
fof(f8341,plain,
! [X0] : complement(composition(sk1,complement(complement(X0)))) = join(complement(X0),complement(join(composition(sk1,top),composition(sk1,complement(complement(X0)))))),
inference(forward_demodulation,[],[f8336,f1032]) ).
fof(f8345,plain,
! [X0] : complement(composition(sk1,complement(complement(X0)))) = join(complement(X0),complement(composition(sk1,join(top,complement(complement(X0)))))),
inference(forward_demodulation,[],[f8341,f6418]) ).
fof(f8347,plain,
! [X0] : complement(composition(sk1,complement(complement(X0)))) = join(complement(X0),complement(composition(sk1,top))),
inference(forward_demodulation,[],[f8345,f785]) ).
fof(f8348,plain,
! [X0] : complement(composition(sk1,X0)) = join(complement(X0),complement(composition(sk1,top))),
inference(forward_demodulation,[],[f8347,f1032]) ).
fof(f8386,plain,
! [X0,X1] : join(X1,complement(composition(sk1,X0))) = join(complement(X0),join(complement(composition(sk1,top)),X1)),
inference(superposition,[],[f82,f8348]) ).
fof(f8387,plain,
! [X0,X1] : join(X1,complement(composition(sk1,X0))) = join(complement(composition(sk1,top)),join(X1,complement(X0))),
inference(superposition,[],[f82,f8348]) ).
fof(f8428,plain,
! [X0,X1] : join(X1,complement(composition(sk1,X0))) = complement(composition(sk1,complement(join(X1,complement(X0))))),
inference(forward_demodulation,[],[f8387,f8276]) ).
fof(f8429,plain,
! [X0,X1] : join(X1,complement(composition(sk1,X0))) = join(complement(X0),complement(composition(sk1,complement(X1)))),
inference(forward_demodulation,[],[f8386,f8276]) ).
fof(f8588,plain,
! [X2,X0,X1] : join(complement(join(X2,X1)),complement(composition(sk1,X0))) = complement(composition(sk1,complement(join(complement(X0),complement(join(X1,X2)))))),
inference(superposition,[],[f8428,f2980]) ).
fof(f8601,plain,
! [X0,X1] : join(X1,complement(composition(sk1,X0))) = complement(composition(sk1,complement(join(complement(X0),X1)))),
inference(superposition,[],[f8428,f3225]) ).
fof(f8692,plain,
! [X2,X0,X1] : join(complement(join(X2,X1)),complement(composition(sk1,X0))) = join(complement(X0),complement(composition(sk1,join(X1,X2)))),
inference(forward_demodulation,[],[f8588,f8428]) ).
fof(f9062,plain,
! [X0,X1] : complement(composition(sk1,complement(join(complement(X0),complement(X1))))) = join(complement(join(complement(X1),X0)),complement(composition(sk1,X1))),
inference(superposition,[],[f8601,f1444]) ).
fof(f9184,plain,
! [X0,X1] : complement(composition(sk1,complement(join(complement(X0),complement(X1))))) = join(complement(X1),complement(composition(sk1,join(X0,complement(X1))))),
inference(forward_demodulation,[],[f9062,f8692]) ).
fof(f9266,plain,
! [X0,X1] : join(complement(composition(sk1,X0)),complement(X1)) = complement(composition(sk1,complement(join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f9184,f8156]) ).
fof(f9310,plain,
! [X0,X1] : join(complement(composition(sk1,X0)),complement(X1)) = join(complement(X0),complement(composition(sk1,X1))),
inference(forward_demodulation,[],[f9266,f8428]) ).
fof(f9409,plain,
( complement(join(complement(sk2),complement(composition(sk1,complement(composition(sk1,sk3)))))) != join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(sk2),complement(composition(sk1,complement(composition(sk1,sk3)))))))
| complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(sk2),complement(composition(sk1,complement(composition(sk1,sk3))))))) ),
inference(superposition,[],[f40,f9310]) ).
fof(f9446,plain,
! [X0,X1] : join(complement(composition(sk1,X0)),X1) = join(complement(X0),complement(composition(sk1,join(complement(composition(sk1,X0)),complement(X1))))),
inference(superposition,[],[f1409,f9310]) ).
fof(f9471,plain,
! [X2,X0,X1] : join(X2,complement(join(complement(X0),complement(composition(sk1,X1))))) = join(complement(join(complement(X1),complement(composition(sk1,X0)))),X2),
inference(superposition,[],[f2980,f9310]) ).
fof(f9475,plain,
! [X0,X1] : complement(join(complement(X1),complement(composition(sk1,X0)))) = complement(join(complement(X0),complement(composition(sk1,X1)))),
inference(superposition,[],[f3225,f9310]) ).
fof(f9495,plain,
! [X0,X1] : join(complement(composition(sk1,X0)),X1) = join(complement(X0),complement(composition(sk1,join(complement(X0),complement(composition(sk1,X1)))))),
inference(forward_demodulation,[],[f9446,f9310]) ).
fof(f9526,plain,
( complement(join(composition(sk1,sk3),complement(composition(sk1,sk2)))) != join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(composition(sk1,sk3),complement(composition(sk1,sk2)))))
| complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(sk2),complement(composition(sk1,complement(composition(sk1,sk3))))))) ),
inference(forward_demodulation,[],[f9409,f8429]) ).
fof(f9572,plain,
! [X0,X1] : join(complement(composition(sk1,X0)),X1) = join(complement(X0),complement(composition(sk1,complement(composition(sk1,X1))))),
inference(forward_demodulation,[],[f9495,f7937]) ).
fof(f9587,plain,
( complement(join(composition(sk1,sk3),complement(composition(sk1,sk2)))) != join(complement(join(complement(sk2),complement(composition(sk1,complement(sk3))))),complement(join(composition(sk1,sk3),complement(composition(sk1,sk2)))))
| complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(sk2),complement(composition(sk1,complement(composition(sk1,sk3))))))) ),
inference(forward_demodulation,[],[f9526,f9475]) ).
fof(f9612,plain,
! [X0,X1] : join(complement(composition(sk1,X0)),X1) = join(composition(sk1,X1),complement(composition(sk1,X0))),
inference(forward_demodulation,[],[f9572,f8429]) ).
fof(f9620,plain,
( complement(join(composition(sk1,sk3),complement(composition(sk1,sk2)))) != join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(composition(sk1,sk3),complement(composition(sk1,sk2)))))
| complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(sk2),complement(composition(sk1,complement(composition(sk1,sk3))))))) ),
inference(forward_demodulation,[],[f9587,f8429]) ).
fof(f9638,plain,
( complement(join(complement(composition(sk1,sk2)),sk3)) != join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),sk3)))
| complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(sk2),complement(composition(sk1,complement(composition(sk1,sk3))))))) ),
inference(forward_demodulation,[],[f9620,f9612]) ).
fof(f9648,plain,
complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(sk2),complement(composition(sk1,complement(composition(sk1,sk3))))))),
inference(forward_subsumption_resolution,[],[f9638,f3192]) ).
fof(f9655,plain,
complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(composition(sk1,sk3),complement(composition(sk1,sk2))))),
inference(forward_demodulation,[],[f9648,f8429]) ).
fof(f9662,plain,
complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),sk3))),
inference(forward_demodulation,[],[f9655,f9612]) ).
fof(f9666,plain,
complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != join(complement(join(complement(composition(sk1,sk2)),sk3)),complement(join(complement(sk2),complement(composition(sk1,complement(sk3)))))),
inference(forward_demodulation,[],[f9662,f9471]) ).
fof(f9670,plain,
complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,complement(sk3))),complement(sk2)))),
inference(forward_demodulation,[],[f9666,f3127]) ).
fof(f9674,plain,
complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(sk2),complement(composition(sk1,complement(sk3)))))),
inference(forward_demodulation,[],[f9670,f3148]) ).
fof(f9677,plain,
complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(sk3,complement(composition(sk1,sk2))))),
inference(forward_demodulation,[],[f9674,f8429]) ).
fof(f9680,plain,
complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != complement(join(sk3,complement(composition(sk1,sk2)))),
inference(forward_demodulation,[],[f9677,f505]) ).
fof(f9683,plain,
complement(join(sk3,complement(composition(sk1,sk2)))) != complement(join(complement(sk2),complement(composition(sk1,complement(sk3))))),
inference(forward_demodulation,[],[f9680,f9475]) ).
fof(f9686,plain,
complement(join(sk3,complement(composition(sk1,sk2)))) != complement(join(sk3,complement(composition(sk1,sk2)))),
inference(forward_demodulation,[],[f9683,f8429]) ).
fof(f9687,plain,
$false,
inference(trivial_inequality_removal,[],[f9686]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL030-4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n011.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 22:54:46 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.39/2.18 % (2855914)Input is clausal, will run a generic CNF schedule.
% 9.39/2.18 % (2855922)lrs+10_1_sil=8000:sp=occurrence:random_seed=1921370646:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.39/2.18 % (2855925)dis-21_1_sil=8000:lcm=predicate:random_seed=1926527129:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 9.39/2.18 % (2855925)Refutation not found, incomplete strategy
% 9.39/2.18 % (2855925)------------------------------
% 9.39/2.18 % (2855925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.39/2.18 % (2855925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.39/2.18 % (2855925)CaDiCaL version: 2.1.3
% 9.39/2.18 % (2855925)Termination reason: Refutation not found, incomplete strategy
% 9.39/2.18 % (2855925)Time elapsed: 0.002 s
% 9.39/2.18 % (2855925)Peak memory usage: 88 MB
% 9.39/2.18 % (2855925)Instructions burned: 1 (million)
% 9.39/2.18 % (2855920)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1505082500:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.39/2.18 % (2855924)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3559745142:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.39/2.18 % (2855921)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3475111563:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.39/2.18 % (2855919)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=4010822566:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.39/2.18 % (2855923)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=962010967:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.39/2.18 % (2855922)Instruction limit reached!
% 9.39/2.18 % (2855922)------------------------------
% 9.39/2.18 % (2855922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.39/2.18 % (2855922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.39/2.18 % (2855922)CaDiCaL version: 2.1.3
% 9.39/2.18 % (2855922)Termination reason: Instruction limit
% 9.39/2.18 % (2855922)Termination phase: Saturation
% 9.39/2.18 % (2855922)Time elapsed: 0.036 s
% 9.39/2.18 % (2855922)Peak memory usage: 89 MB
% 9.39/2.18 % (2855922)Instructions burned: 107 (million)
% 9.39/2.18 % (2855923)Instruction limit reached!
% 9.39/2.18 % (2855923)------------------------------
% 9.39/2.18 % (2855923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.39/2.18 % (2855923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.39/2.18 % (2855923)CaDiCaL version: 2.1.3
% 9.39/2.18 % (2855923)Termination reason: Instruction limit
% 9.39/2.18 % (2855923)Termination phase: Saturation
% 9.39/2.18 % (2855923)Time elapsed: 0.071 s
% 9.39/2.18 % (2855923)Peak memory usage: 89 MB
% 9.39/2.18 % (2855923)Instructions burned: 115 (million)
% 9.39/2.18 % (2855933)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=2390496313:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 9.39/2.18 % (2855924)Instruction limit reached!
% 9.39/2.18 % (2855924)------------------------------
% 9.39/2.18 % (2855924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.39/2.18 % (2855924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.39/2.18 % (2855924)CaDiCaL version: 2.1.3
% 9.39/2.18 % (2855924)Termination reason: Instruction limit
% 9.39/2.18 % (2855924)Termination phase: Saturation
% 9.39/2.18 % (2855924)Time elapsed: 0.113 s
% 9.39/2.18 % (2855924)Peak memory usage: 90 MB
% 9.39/2.18 % (2855924)Instructions burned: 180 (million)
% 9.39/2.18 % (2855933)Instruction limit reached!
% 9.39/2.18 % (2855933)------------------------------
% 9.39/2.18 % (2855933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.39/2.18 % (2855933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.39/2.18 % (2855933)CaDiCaL version: 2.1.3
% 9.39/2.18 % (2855933)Termination reason: Instruction limit
% 9.39/2.18 % (2855933)Termination phase: Saturation
% 9.39/2.18 % (2855933)Time elapsed: 0.042 s
% 9.39/2.18 % (2855933)Peak memory usage: 89 MB
% 9.39/2.18 % (2855933)Instructions burned: 144 (million)
% 9.39/2.18 % (2855934)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3821385777:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 10.30/2.35 % (2855936)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3732879861:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 10.30/2.35 % (2855925)------------------------------
% 10.30/2.35 % (2855925)------------------------------
% 10.30/2.35 % (2855937)lrs+10_64_to=lpo:sil=8000:random_seed=4093791857:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 10.30/2.35 % (2855937)Instruction limit reached!
% 10.30/2.35 % (2855937)------------------------------
% 10.30/2.35 % (2855937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.35 % (2855937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.35 % (2855937)CaDiCaL version: 2.1.3
% 10.30/2.35 % (2855937)Termination reason: Instruction limit
% 10.30/2.35 % (2855937)Termination phase: Saturation
% 10.30/2.35 % (2855937)Time elapsed: 0.041 s
% 10.30/2.35 % (2855937)Peak memory usage: 89 MB
% 10.30/2.35 % (2855937)Instructions burned: 127 (million)
% 10.30/2.35 % (2855934)Instruction limit reached!
% 10.30/2.35 % (2855934)------------------------------
% 10.30/2.35 % (2855934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.35 % (2855934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.35 % (2855934)CaDiCaL version: 2.1.3
% 10.30/2.35 % (2855934)Termination reason: Instruction limit
% 10.30/2.35 % (2855934)Termination phase: Saturation
% 10.30/2.35 % (2855934)Time elapsed: 0.125 s
% 10.30/2.35 % (2855934)Peak memory usage: 91 MB
% 10.30/2.35 % (2855934)Instructions burned: 190 (million)
% 10.30/2.35 % (2855936)Instruction limit reached!
% 10.30/2.35 % (2855936)------------------------------
% 10.30/2.35 % (2855936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.35 % (2855936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.35 % (2855936)CaDiCaL version: 2.1.3
% 10.30/2.35 % (2855936)Termination reason: Instruction limit
% 10.30/2.35 % (2855936)Termination phase: Saturation
% 10.30/2.35 % (2855936)Time elapsed: 0.121 s
% 10.30/2.35 % (2855936)Peak memory usage: 91 MB
% 10.30/2.35 % (2855936)Instructions burned: 219 (million)
% 10.30/2.35 % (2855941)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4102650139:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 10.30/2.35 % (2855942)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=214459854:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 10.30/2.35 % (2855942)Instruction limit reached!
% 10.30/2.35 % (2855942)------------------------------
% 10.30/2.35 % (2855942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.35 % (2855942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.35 % (2855942)CaDiCaL version: 2.1.3
% 10.30/2.35 % (2855942)Termination reason: Instruction limit
% 10.30/2.35 % (2855942)Termination phase: Saturation
% 10.30/2.35 % (2855942)Time elapsed: 0.050 s
% 10.30/2.35 % (2855942)Peak memory usage: 91 MB
% 10.30/2.35 % (2855942)Instructions burned: 159 (million)
% 10.30/2.35 % (2855943)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3375718143:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 10.30/2.35 % (2855944)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=79122932:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 10.30/2.35 % (2855941)Instruction limit reached!
% 10.30/2.35 % (2855941)------------------------------
% 10.30/2.35 % (2855941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.35 % (2855941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.35 % (2855941)CaDiCaL version: 2.1.3
% 10.30/2.35 % (2855941)Termination reason: Instruction limit
% 10.30/2.35 % (2855941)Termination phase: Saturation
% 10.30/2.35 % (2855941)Time elapsed: 0.124 s
% 10.30/2.35 % (2855941)Peak memory usage: 90 MB
% 10.30/2.35 % (2855941)Instructions burned: 194 (million)
% 10.30/2.35 % (2855947)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1935506527:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 10.30/2.35 % (2855944)Instruction limit reached!
% 10.30/2.35 % (2855944)------------------------------
% 10.30/2.35 % (2855944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.35 % (2855944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.35 % (2855944)CaDiCaL version: 2.1.3
% 10.30/2.35 % (2855944)Termination reason: Instruction limit
% 10.30/2.35 % (2855944)Termination phase: Saturation
% 10.30/2.35 % (2855944)Time elapsed: 0.066 s
% 10.30/2.35 % (2855944)Peak memory usage: 89 MB
% 10.30/2.35 % (2855944)Instructions burned: 107 (million)
% 10.30/2.35 % (2855947)Instruction limit reached!
% 10.30/2.35 % (2855947)------------------------------
% 10.30/2.35 % (2855947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.35 % (2855947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.35 % (2855947)CaDiCaL version: 2.1.3
% 10.30/2.35 % (2855947)Termination reason: Instruction limit
% 10.30/2.35 % (2855947)Termination phase: Saturation
% 10.30/2.35 % (2855947)Time elapsed: 0.033 s
% 10.30/2.35 % (2855947)Peak memory usage: 88 MB
% 10.30/2.35 % (2855947)Instructions burned: 109 (million)
% 10.30/2.35 % (2855950)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=477434281:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 10.30/2.35 % (2855952)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2686862029:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 10.30/2.35 % (2855953)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2774680414:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi)
% 10.30/2.35 % (2855953)Instruction limit reached!
% 10.30/2.35 % (2855953)------------------------------
% 10.30/2.35 % (2855953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.35 % (2855953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.35 % (2855953)CaDiCaL version: 2.1.3
% 10.30/2.35 % (2855953)Termination reason: Instruction limit
% 10.30/2.35 % (2855953)Termination phase: Saturation
% 10.30/2.35 % (2855953)Time elapsed: 0.042 s
% 10.30/2.35 % (2855953)Peak memory usage: 89 MB
% 10.30/2.35 % (2855953)Instructions burned: 137 (million)
% 10.30/2.35 % (2855950)Instruction limit reached!
% 10.30/2.35 % (2855950)------------------------------
% 10.30/2.35 % (2855950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.35 % (2855950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.35 % (2855950)CaDiCaL version: 2.1.3
% 10.30/2.35 % (2855950)Termination reason: Instruction limit
% 10.30/2.35 % (2855950)Termination phase: Saturation
% 10.30/2.35 % (2855950)Time elapsed: 0.139 s
% 10.30/2.35 % (2855950)Peak memory usage: 90 MB
% 10.30/2.35 % (2855950)Instructions burned: 243 (million)
% 10.30/2.35 % (2855957)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1057471840:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi)
% 10.30/2.35 % (2855958)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3670328203:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi)
% 10.30/2.35 % (2855958)Instruction limit reached!
% 10.30/2.35 % (2855958)------------------------------
% 10.30/2.35 % (2855958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.35 % (2855958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.35 % (2855958)CaDiCaL version: 2.1.3
% 10.30/2.35 % (2855958)Termination reason: Instruction limit
% 10.30/2.35 % (2855958)Termination phase: Saturation
% 10.30/2.35 % (2855958)Time elapsed: 0.124 s
% 10.30/2.35 % (2855958)Peak memory usage: 91 MB
% 10.30/2.35 % (2855958)Instructions burned: 192 (million)
% 10.30/2.35 % (2855920)First to succeed.
% 10.30/2.35 % (2855920)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2855914"
% 10.30/2.35 % (2855961)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3527540818:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi)
% 10.30/2.35 % (2855957)Instruction limit reached!
% 10.30/2.35 % (2855957)------------------------------
% 10.30/2.35 % (2855957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.35 % (2855957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.35 % (2855957)CaDiCaL version: 2.1.3
% 10.30/2.35 % (2855957)Termination reason: Instruction limit
% 10.30/2.35 % (2855957)Termination phase: Saturation
% 10.30/2.35 % (2855957)Time elapsed: 0.355 s
% 10.30/2.35 % (2855957)Peak memory usage: 94 MB
% 10.30/2.35 % (2855957)Instructions burned: 499 (million)
% 10.30/2.35 % (2855921)Also succeeded, but the first one will report.
% 10.30/2.35 % (2855963)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1112717247:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 10.30/2.35 % (2855961)Instruction limit reached!
% 10.30/2.35 % (2855961)------------------------------
% 10.30/2.35 % (2855961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.35 % (2855961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.35 % (2855961)CaDiCaL version: 2.1.3
% 10.30/2.35 % (2855961)Termination reason: Instruction limit
% 10.30/2.35 % (2855961)Termination phase: Saturation
% 10.30/2.35 % (2855961)Time elapsed: 0.162 s
% 10.30/2.35 % (2855961)Peak memory usage: 91 MB
% 10.30/2.35 % (2855961)Instructions burned: 264 (million)
% 10.30/2.35 % (2855920)Refutation found. Thanks to Tanya!
% 10.30/2.35 % SZS status Unsatisfiable for theBenchmark
% 10.30/2.35 % SZS output start Proof for theBenchmark
% See solution above
% 11.18/2.54 % (2855920)------------------------------
% 11.18/2.54 % (2855920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.54 % (2855920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.54 % (2855920)CaDiCaL version: 2.1.3
% 11.18/2.54 % (2855920)Termination reason: Refutation
% 11.18/2.54 % (2855920)Time elapsed: 1.092 s
% 11.18/2.54 % (2855920)Peak memory usage: 135 MB
% 11.18/2.54 % (2855920)Instructions burned: 1705 (million)
% 11.18/2.54 % (2855920)------------------------------
% 11.18/2.54 % (2855920)------------------------------
% 11.18/2.54 % (2855914)Success in time 1.506 s
% 11.18/2.54 % Vampire exiting
%------------------------------------------------------------------------------