%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : REL030-2 : 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 : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:33:56 PM UTC 2026
% Result : Unsatisfiable 10.38s 2.34s
% Output : Refutation 11.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 17
% Syntax : Number of formulae : 193 ( 153 unt; 2 def)
% Number of atoms : 233 ( 189 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 84 ( 44 ~; 38 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 271 ( 0 sgn 271 !; 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(f17,negated_conjecture,
join(sk1,one) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_14) ).
fof(f18,plain,
one = join(sk1,one),
inference(reorient_equations,[],[f17]) ).
fof(f19,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_15) ).
fof(f20,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,[],[f19]) ).
fof(f21,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,[],[f20,f6,f6,f6,f6,f6,f6]) ).
fof(f22,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f16,f6]) ).
fof(f23,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f4,f1]) ).
fof(f24,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(converse(X0),complement(composition(X0,X1)))),
inference(forward_demodulation,[],[f14,f1]) ).
fof(f25,plain,
zero = complement(top),
inference(forward_demodulation,[],[f22,f15]) ).
fof(f26,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(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(forward_demodulation,[],[f21,f1]) ).
fof(f27,plain,
( complement(join(complement(composition(sk1,sk2)),complement(complement(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(composition(sk1,sk3))))) != join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))) ),
inference(forward_demodulation,[],[f26,f1]) ).
fof(f28,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)),complement(complement(composition(sk1,sk3))))))
| 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)))))) ),
inference(forward_demodulation,[],[f27,f1]) ).
fof(f30,definition,
( spl0_1
<=> 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)))))) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f32,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))))))
| spl0_1 ),
inference(avatar_component_clause,[],[f30]) ).
fof(f34,definition,
( spl0_2
<=> 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)))))) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f36,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)),complement(complement(composition(sk1,sk3))))))
| spl0_2 ),
inference(avatar_component_clause,[],[f34]) ).
fof(f37,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f28,f34,f30]) ).
fof(f41,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(join(complement(join(complement(X0),X1)),join(complement(X0),complement(X1)))),complement(X0)),
inference(superposition,[],[f23,f23]) ).
fof(f42,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(complement(join(complement(X0),X1)),join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f41,f1]) ).
fof(f50,plain,
! [X2,X0,X1] : join(X0,X2) = join(complement(join(complement(X0),X1)),join(complement(join(complement(X0),complement(X1))),X2)),
inference(superposition,[],[f2,f23]) ).
fof(f65,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X1,join(X2,X0)),
inference(superposition,[],[f2,f1]) ).
fof(f66,plain,
! [X0,X1] : join(complement(join(complement(X1),X0)),complement(join(complement(X0),complement(X1)))) = X1,
inference(superposition,[],[f23,f1]) ).
fof(f67,plain,
! [X0,X1] : join(complement(join(X0,complement(X1))),complement(join(complement(X1),complement(X0)))) = X1,
inference(superposition,[],[f23,f1]) ).
fof(f70,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(X0,complement(composition(converse(X0),X1)))),
inference(superposition,[],[f24,f10]) ).
fof(f90,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f2,f15]) ).
fof(f91,plain,
! [X0,X1] : top = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f2,f15]) ).
fof(f108,plain,
! [X0] : complement(X0) = join(complement(join(complement(complement(X0)),X0)),complement(top)),
inference(superposition,[],[f66,f15]) ).
fof(f115,plain,
! [X0] : complement(X0) = join(complement(top),complement(join(complement(complement(X0)),X0))),
inference(forward_demodulation,[],[f108,f1]) ).
fof(f126,plain,
! [X0] : complement(X0) = join(complement(top),complement(join(X0,complement(complement(X0))))),
inference(forward_demodulation,[],[f115,f1]) ).
fof(f131,plain,
! [X0] : complement(X0) = join(zero,complement(join(X0,complement(complement(X0))))),
inference(forward_demodulation,[],[f126,f25]) ).
fof(f136,plain,
! [X0,X1] : composition(converse(X1),X0) = converse(composition(converse(X0),X1)),
inference(superposition,[],[f12,f10]) ).
fof(f139,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(f145,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = join(converse(composition(X0,X2)),converse(composition(X0,X1))),
inference(superposition,[],[f139,f12]) ).
fof(f151,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = converse(join(composition(X0,X2),composition(X0,X1))),
inference(forward_demodulation,[],[f145,f11]) ).
fof(f154,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = composition(converse(join(X2,X1)),converse(X0)),
inference(forward_demodulation,[],[f151,f11]) ).
fof(f156,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = converse(composition(X0,join(X2,X1))),
inference(forward_demodulation,[],[f154,f12]) ).
fof(f165,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X0,X2)) = converse(converse(composition(X0,join(X1,X2)))),
inference(superposition,[],[f10,f156]) ).
fof(f177,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = join(composition(X0,X1),composition(X0,X2)),
inference(forward_demodulation,[],[f165,f10]) ).
fof(f190,plain,
! [X0,X1] : composition(X0,join(one,X1)) = join(X0,composition(X0,X1)),
inference(superposition,[],[f177,f8]) ).
fof(f192,plain,
! [X0,X1] : composition(X0,join(X1,one)) = join(composition(X0,X1),X0),
inference(superposition,[],[f177,f8]) ).
fof(f201,plain,
! [X0,X1] : join(X0,composition(X0,X1)) = composition(X0,join(X1,one)),
inference(forward_demodulation,[],[f192,f1]) ).
fof(f342,plain,
! [X0] : join(X0,X0) = composition(X0,join(one,one)),
inference(superposition,[],[f190,f8]) ).
fof(f650,plain,
! [X0,X1] : join(top,complement(join(complement(X0),complement(X1)))) = join(join(X1,complement(X0)),X0),
inference(superposition,[],[f90,f67]) ).
fof(f656,plain,
! [X0,X1] : join(top,X0) = join(X1,join(X0,complement(X1))),
inference(superposition,[],[f90,f1]) ).
fof(f694,plain,
! [X0,X1] : join(top,complement(join(complement(X0),complement(X1)))) = join(X0,join(X1,complement(X0))),
inference(forward_demodulation,[],[f650,f1]) ).
fof(f703,plain,
! [X0,X1] : join(top,X1) = join(top,complement(join(complement(X0),complement(X1)))),
inference(forward_demodulation,[],[f694,f656]) ).
fof(f901,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f136,f8]) ).
fof(f918,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f901,f10]) ).
fof(f937,plain,
! [X0,X1] : join(X0,composition(X1,X0)) = composition(join(converse(one),X1),X0),
inference(superposition,[],[f9,f918]) ).
fof(f946,plain,
one = converse(one),
inference(superposition,[],[f8,f918]) ).
fof(f957,plain,
! [X0,X1] : join(X0,composition(X1,X0)) = composition(join(one,X1),X0),
inference(forward_demodulation,[],[f937,f946]) ).
fof(f973,plain,
! [X0] : composition(one,X0) = X0,
inference(superposition,[],[f918,f946]) ).
fof(f1001,plain,
! [X0] : complement(X0) = join(complement(X0),complement(composition(converse(one),X0))),
inference(superposition,[],[f70,f973]) ).
fof(f1004,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(forward_demodulation,[],[f1001,f918]) ).
fof(f1030,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,[],[f50,f1004]) ).
fof(f1038,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f1030,f23]) ).
fof(f1097,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(superposition,[],[f1038,f42]) ).
fof(f1101,plain,
! [X0] : join(X0,complement(complement(X0))) = X0,
inference(superposition,[],[f1038,f1038]) ).
fof(f1120,plain,
! [X0,X1] : join(X0,complement(X0)) = join(top,complement(join(complement(complement(X0)),complement(X1)))),
inference(superposition,[],[f90,f1038]) ).
fof(f1140,plain,
! [X0,X1] : join(X0,complement(X0)) = join(top,X1),
inference(forward_demodulation,[],[f1120,f703]) ).
fof(f1161,plain,
! [X1] : top = join(top,X1),
inference(forward_demodulation,[],[f1140,f15]) ).
fof(f1205,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(join(complement(X0),X2),complement(join(X0,X1))),
inference(superposition,[],[f1097,f50]) ).
fof(f1207,plain,
! [X0,X1] : join(X1,complement(join(X0,complement(X1)))) = X1,
inference(superposition,[],[f1097,f1]) ).
fof(f1264,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(X0),join(X2,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f1205,f2]) ).
fof(f1319,plain,
! [X2,X0,X1] : join(X0,X1) = join(complement(join(complement(X0),join(X2,complement(complement(X0))))),join(complement(complement(X0)),X1)),
inference(superposition,[],[f50,f1207]) ).
fof(f1344,plain,
! [X2,X0,X1] : join(X0,X1) = join(complement(complement(X0)),join(X1,complement(join(complement(X0),join(X2,complement(complement(X0))))))),
inference(forward_demodulation,[],[f1319,f65]) ).
fof(f1367,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),X1),
inference(forward_demodulation,[],[f1344,f1264]) ).
fof(f1383,plain,
! [X0] : complement(X0) = join(zero,complement(X0)),
inference(superposition,[],[f131,f1101]) ).
fof(f1455,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(top)))) = X0,
inference(superposition,[],[f67,f1161]) ).
fof(f1458,plain,
! [X0] : join(zero,complement(join(complement(X0),zero))) = X0,
inference(forward_demodulation,[],[f1455,f25]) ).
fof(f1468,plain,
! [X0] : complement(join(complement(X0),zero)) = X0,
inference(forward_demodulation,[],[f1458,f1383]) ).
fof(f1470,plain,
! [X0] : complement(join(zero,complement(X0))) = X0,
inference(forward_demodulation,[],[f1468,f1]) ).
fof(f1471,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f1470,f1383]) ).
fof(f1479,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(X0,complement(X1)))),
inference(superposition,[],[f23,f1471]) ).
fof(f1484,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(complement(join(X0,X1)),join(X0,complement(X1))))),
inference(superposition,[],[f42,f1471]) ).
fof(f1490,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(complement(X1),X0))),
inference(superposition,[],[f66,f1471]) ).
fof(f1497,plain,
! [X0] : join(X0,X0) = X0,
inference(superposition,[],[f1004,f1471]) ).
fof(f1502,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(superposition,[],[f1207,f1471]) ).
fof(f1510,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,join(complement(X1),complement(join(X0,X1)))))),
inference(forward_demodulation,[],[f1484,f65]) ).
fof(f1520,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,complement(X1)))),
inference(forward_demodulation,[],[f1510,f1502]) ).
fof(f1598,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),complement(complement(X0))),
inference(superposition,[],[f1097,f1479]) ).
fof(f1601,plain,
! [X0,X1] : join(X0,complement(X1)) = join(complement(complement(X0)),complement(join(complement(join(X0,complement(X1))),complement(complement(join(X0,X1)))))),
inference(superposition,[],[f67,f1479]) ).
fof(f1608,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(complement(join(X0,complement(X1))),complement(complement(join(X0,X1)))))),
inference(forward_demodulation,[],[f1601,f1367]) ).
fof(f1611,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),join(X0,X1)),
inference(forward_demodulation,[],[f1598,f1]) ).
fof(f1659,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(complement(complement(join(X0,X1))),complement(join(X0,complement(X1)))))),
inference(forward_demodulation,[],[f1608,f1]) ).
fof(f1662,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,complement(complement(X0)))),
inference(forward_demodulation,[],[f1611,f65]) ).
fof(f1695,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(join(X0,X1),complement(join(X0,complement(X1)))))),
inference(forward_demodulation,[],[f1659,f1367]) ).
fof(f1698,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f1662,f1471]) ).
fof(f1725,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,join(X1,complement(join(X0,complement(X1))))))),
inference(forward_demodulation,[],[f1695,f2]) ).
fof(f1743,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f1725,f1207]) ).
fof(f1761,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(X1,complement(X0)),
inference(superposition,[],[f1743,f1]) ).
fof(f2686,plain,
! [X0,X1] : complement(X1) = join(complement(join(X0,X1)),complement(join(complement(X0),X1))),
inference(superposition,[],[f1490,f1]) ).
fof(f2743,plain,
! [X0,X1] : complement(join(X0,complement(join(complement(X1),X0)))) = join(complement(join(join(X0,complement(join(complement(X1),X0))),X1)),complement(top)),
inference(superposition,[],[f1490,f91]) ).
fof(f2820,plain,
! [X0,X1] : complement(join(X0,complement(join(complement(X1),X0)))) = join(complement(top),complement(join(join(X0,complement(join(complement(X1),X0))),X1))),
inference(forward_demodulation,[],[f2743,f1]) ).
fof(f2892,plain,
! [X0,X1] : complement(join(X0,complement(join(complement(X1),X0)))) = join(complement(top),complement(join(X1,join(X0,complement(join(complement(X1),X0)))))),
inference(forward_demodulation,[],[f2820,f1]) ).
fof(f2957,plain,
! [X0,X1] : complement(join(X0,complement(complement(X1)))) = join(complement(top),complement(join(X1,join(X0,complement(complement(X1)))))),
inference(forward_demodulation,[],[f2892,f1761]) ).
fof(f3007,plain,
! [X0,X1] : complement(join(X0,X1)) = join(complement(top),complement(join(X1,join(X0,X1)))),
inference(forward_demodulation,[],[f2957,f1471]) ).
fof(f3048,plain,
! [X0,X1] : complement(join(X0,X1)) = join(complement(top),complement(join(X1,X0))),
inference(forward_demodulation,[],[f3007,f1698]) ).
fof(f3073,plain,
! [X0,X1] : complement(join(X0,X1)) = join(zero,complement(join(X1,X0))),
inference(forward_demodulation,[],[f3048,f25]) ).
fof(f3083,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f3073,f1383]) ).
fof(f3211,plain,
! [X2,X0,X1] : join(X2,join(X1,X0)) = join(X2,complement(join(X2,complement(join(X0,X1))))),
inference(superposition,[],[f1520,f3083]) ).
fof(f3212,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X2,join(X1,X0)),
inference(forward_demodulation,[],[f3211,f1520]) ).
fof(f3818,plain,
! [X2,X0,X1] : join(X0,complement(join(X0,join(X1,X2)))) = join(X0,complement(join(X2,X1))),
inference(superposition,[],[f1743,f3212]) ).
fof(f3852,plain,
! [X2,X0,X1] : join(X0,complement(join(X1,X2))) = join(X0,complement(join(X2,X1))),
inference(forward_demodulation,[],[f3818,f1743]) ).
fof(f4363,plain,
! [X0,X1] : join(complement(join(X1,X0)),complement(complement(X0))) = join(complement(join(X1,X0)),join(complement(X1),X0)),
inference(superposition,[],[f1520,f2686]) ).
fof(f4388,plain,
! [X0,X1] : join(complement(join(X1,X0)),complement(complement(X0))) = join(complement(X1),join(X0,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f4363,f65]) ).
fof(f4477,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(join(X1,X0)),complement(complement(X0))),
inference(forward_demodulation,[],[f4388,f1264]) ).
fof(f4550,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(complement(X0)),complement(join(X1,X0))),
inference(forward_demodulation,[],[f4477,f1]) ).
fof(f4610,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(join(X1,X0))),
inference(forward_demodulation,[],[f4550,f1367]) ).
fof(f8969,plain,
! [X0] : composition(X0,one) = join(X0,composition(X0,sk1)),
inference(superposition,[],[f201,f18]) ).
fof(f9055,plain,
! [X0] : join(X0,composition(X0,sk1)) = X0,
inference(forward_demodulation,[],[f8969,f8]) ).
fof(f9151,plain,
! [X0] : composition(one,X0) = join(X0,composition(composition(one,sk1),X0)),
inference(superposition,[],[f957,f9055]) ).
fof(f9158,plain,
! [X0] : composition(one,X0) = join(X0,composition(one,composition(sk1,X0))),
inference(forward_demodulation,[],[f9151,f7]) ).
fof(f9194,plain,
! [X0] : composition(one,X0) = join(X0,composition(sk1,X0)),
inference(forward_demodulation,[],[f9158,f973]) ).
fof(f9213,plain,
! [X0] : join(X0,composition(sk1,X0)) = X0,
inference(forward_demodulation,[],[f9194,f973]) ).
fof(f9432,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(composition(sk1,X0),X1)),
inference(superposition,[],[f2,f9213]) ).
fof(f9460,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(complement(join(X0,composition(sk1,complement(X0)))),complement(complement(X0))),
inference(superposition,[],[f2686,f9213]) ).
fof(f9476,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(complement(complement(X0)),complement(join(X0,composition(sk1,complement(X0))))),
inference(forward_demodulation,[],[f9460,f1]) ).
fof(f9505,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(X0,complement(join(X0,composition(sk1,complement(X0))))),
inference(forward_demodulation,[],[f9476,f1367]) ).
fof(f9522,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(X0,complement(composition(sk1,complement(X0)))),
inference(forward_demodulation,[],[f9505,f1743]) ).
fof(f10686,plain,
! [X0,X1] : join(X0,composition(sk1,X1)) = join(X0,composition(sk1,join(X0,X1))),
inference(superposition,[],[f9432,f177]) ).
fof(f10913,plain,
! [X0] : join(X0,composition(sk1,complement(X0))) = join(X0,composition(sk1,top)),
inference(superposition,[],[f10686,f15]) ).
fof(f10922,plain,
! [X2,X0,X1] : join(X0,composition(sk1,complement(join(X2,X1)))) = join(X0,composition(sk1,join(X0,complement(join(X1,X2))))),
inference(superposition,[],[f10686,f3852]) ).
fof(f11085,plain,
! [X2,X0,X1] : join(X0,composition(sk1,complement(join(X2,X1)))) = join(X0,composition(sk1,complement(join(X1,X2)))),
inference(forward_demodulation,[],[f10922,f10686]) ).
fof(f11195,plain,
! [X0] : join(X0,complement(composition(sk1,complement(X0)))) = join(X0,complement(join(X0,composition(sk1,top)))),
inference(superposition,[],[f1743,f10913]) ).
fof(f11258,plain,
! [X0] : join(X0,complement(composition(sk1,complement(X0)))) = join(X0,complement(composition(sk1,top))),
inference(forward_demodulation,[],[f11195,f1743]) ).
fof(f11296,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(X0,complement(composition(sk1,top))),
inference(forward_demodulation,[],[f11258,f9522]) ).
fof(f11418,plain,
! [X0,X1] : complement(composition(sk1,complement(join(X0,X1)))) = join(X0,join(X1,complement(composition(sk1,top)))),
inference(superposition,[],[f2,f11296]) ).
fof(f11482,plain,
! [X0,X1] : complement(composition(sk1,complement(join(X0,X1)))) = join(X0,complement(composition(sk1,complement(X1)))),
inference(forward_demodulation,[],[f11418,f11296]) ).
fof(f11639,plain,
! [X0,X1] : join(X1,complement(composition(sk1,X0))) = complement(composition(sk1,complement(join(X1,complement(X0))))),
inference(superposition,[],[f11482,f1471]) ).
fof(f12018,plain,
! [X0,X1] : join(X1,complement(composition(sk1,X0))) = complement(composition(sk1,complement(join(complement(X0),X1)))),
inference(superposition,[],[f11639,f3083]) ).
fof(f12056,plain,
! [X0,X1] : composition(sk1,complement(join(X0,complement(X1)))) = complement(join(X0,complement(composition(sk1,X1)))),
inference(superposition,[],[f1471,f11639]) ).
fof(f12312,plain,
! [X0,X1] : complement(composition(sk1,complement(join(complement(X0),X1)))) = join(complement(join(complement(X0),complement(X1))),complement(composition(sk1,X0))),
inference(superposition,[],[f12018,f1520]) ).
fof(f12333,plain,
! [X0,X1] : join(complement(X1),complement(composition(sk1,X0))) = join(complement(X0),complement(composition(sk1,X1))),
inference(superposition,[],[f11639,f12018]) ).
fof(f12370,plain,
! [X0,X1] : composition(sk1,complement(join(complement(X1),X0))) = complement(join(X0,complement(composition(sk1,X1)))),
inference(superposition,[],[f1471,f12018]) ).
fof(f12444,plain,
! [X0,X1] : complement(composition(sk1,complement(join(complement(X0),X1)))) = join(complement(composition(sk1,X0)),complement(join(complement(X0),complement(X1)))),
inference(forward_demodulation,[],[f12312,f1]) ).
fof(f12539,plain,
! [X0,X1] : join(X1,complement(composition(sk1,X0))) = join(complement(composition(sk1,X0)),complement(join(complement(X0),complement(X1)))),
inference(forward_demodulation,[],[f12444,f12018]) ).
fof(f12734,plain,
( complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) != join(complement(join(complement(sk2),complement(composition(sk1,complement(sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))))
| spl0_1 ),
inference(superposition,[],[f32,f12333]) ).
fof(f12836,plain,
! [X0,X1] : complement(join(complement(composition(sk1,X0)),complement(X1))) = complement(join(complement(X0),complement(composition(sk1,X1)))),
inference(superposition,[],[f3083,f12333]) ).
fof(f12842,plain,
! [X2,X0,X1] : join(X2,complement(join(complement(composition(sk1,X0)),complement(X1)))) = join(X2,complement(join(complement(X0),complement(composition(sk1,X1))))),
inference(superposition,[],[f3852,f12333]) ).
fof(f12845,plain,
! [X0,X1] : join(complement(complement(X1)),complement(composition(sk1,X0))) = join(complement(composition(sk1,X0)),complement(join(complement(X0),complement(composition(sk1,X1))))),
inference(superposition,[],[f4610,f12333]) ).
fof(f12849,plain,
! [X0,X1] : join(composition(sk1,X1),complement(composition(sk1,X0))) = join(complement(complement(X1)),complement(composition(sk1,X0))),
inference(forward_demodulation,[],[f12845,f12539]) ).
fof(f12921,plain,
( complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) != join(complement(join(complement(sk2),complement(composition(sk1,complement(sk3))))),complement(join(complement(sk2),complement(composition(sk1,complement(composition(sk1,sk3)))))))
| spl0_1 ),
inference(forward_demodulation,[],[f12734,f12842]) ).
fof(f12952,plain,
! [X0,X1] : join(X1,complement(composition(sk1,X0))) = join(composition(sk1,X1),complement(composition(sk1,X0))),
inference(forward_demodulation,[],[f12849,f1367]) ).
fof(f12994,plain,
( complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) != join(complement(join(complement(sk2),complement(composition(sk1,complement(sk3))))),complement(complement(composition(sk1,complement(join(complement(sk2),composition(sk1,sk3)))))))
| spl0_1 ),
inference(forward_demodulation,[],[f12921,f11482]) ).
fof(f13035,plain,
( complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) != join(complement(join(complement(sk2),complement(composition(sk1,complement(sk3))))),composition(sk1,complement(join(complement(sk2),composition(sk1,sk3)))))
| spl0_1 ),
inference(forward_demodulation,[],[f12994,f1471]) ).
fof(f13055,plain,
( complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) != join(complement(join(complement(sk2),complement(composition(sk1,complement(sk3))))),complement(join(composition(sk1,sk3),complement(composition(sk1,sk2)))))
| spl0_1 ),
inference(forward_demodulation,[],[f13035,f12370]) ).
fof(f13069,plain,
( complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) != join(complement(join(complement(sk2),complement(composition(sk1,complement(sk3))))),complement(join(sk3,complement(composition(sk1,sk2)))))
| spl0_1 ),
inference(forward_demodulation,[],[f13055,f12952]) ).
fof(f13079,plain,
( complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) != join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(sk2),complement(composition(sk1,complement(sk3))))))
| spl0_1 ),
inference(forward_demodulation,[],[f13069,f1]) ).
fof(f13087,plain,
( complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) != join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(complement(composition(sk1,complement(join(complement(sk2),sk3))))))
| spl0_1 ),
inference(forward_demodulation,[],[f13079,f11482]) ).
fof(f13089,plain,
( complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) != join(complement(join(sk3,complement(composition(sk1,sk2)))),composition(sk1,complement(join(complement(sk2),sk3))))
| spl0_1 ),
inference(forward_demodulation,[],[f13087,f1471]) ).
fof(f13091,plain,
( complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) != join(complement(join(sk3,complement(composition(sk1,sk2)))),composition(sk1,complement(join(sk3,complement(sk2)))))
| spl0_1 ),
inference(forward_demodulation,[],[f13089,f11085]) ).
fof(f13093,plain,
( complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) != join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(sk3,complement(composition(sk1,sk2)))))
| spl0_1 ),
inference(forward_demodulation,[],[f13091,f12056]) ).
fof(f13095,plain,
( complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) != composition(complement(join(sk3,complement(composition(sk1,sk2)))),join(one,one))
| spl0_1 ),
inference(forward_demodulation,[],[f13093,f342]) ).
fof(f13097,plain,
( complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) != composition(complement(join(sk3,complement(composition(sk1,sk2)))),one)
| spl0_1 ),
inference(forward_demodulation,[],[f13095,f1497]) ).
fof(f13099,plain,
( complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) != complement(join(sk3,complement(composition(sk1,sk2))))
| spl0_1 ),
inference(forward_demodulation,[],[f13097,f8]) ).
fof(f13101,plain,
( complement(join(sk3,complement(composition(sk1,sk2)))) != complement(join(complement(sk2),complement(composition(sk1,complement(composition(sk1,sk3))))))
| spl0_1 ),
inference(forward_demodulation,[],[f13099,f12836]) ).
fof(f13103,plain,
( complement(join(sk3,complement(composition(sk1,sk2)))) != complement(complement(composition(sk1,complement(join(complement(sk2),composition(sk1,sk3))))))
| spl0_1 ),
inference(forward_demodulation,[],[f13101,f11482]) ).
fof(f13105,plain,
( complement(join(sk3,complement(composition(sk1,sk2)))) != composition(sk1,complement(join(complement(sk2),composition(sk1,sk3))))
| spl0_1 ),
inference(forward_demodulation,[],[f13103,f1471]) ).
fof(f13107,plain,
( complement(join(sk3,complement(composition(sk1,sk2)))) != complement(join(composition(sk1,sk3),complement(composition(sk1,sk2))))
| spl0_1 ),
inference(forward_demodulation,[],[f13105,f12370]) ).
fof(f13111,plain,
( complement(join(sk3,complement(composition(sk1,sk2)))) != complement(join(sk3,complement(composition(sk1,sk2))))
| spl0_1 ),
inference(forward_demodulation,[],[f13107,f12952]) ).
fof(f13112,plain,
( $false
| spl0_1 ),
inference(trivial_inequality_removal,[],[f13111]) ).
fof(f13113,plain,
spl0_1,
inference(avatar_contradiction_clause,[],[f13112]) ).
fof(f13115,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)))))))
| spl0_2 ),
inference(forward_demodulation,[],[f36,f12842]) ).
fof(f13117,plain,
( complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(complement(composition(sk1,complement(join(complement(sk2),composition(sk1,sk3)))))))
| spl0_2 ),
inference(forward_demodulation,[],[f13115,f11482]) ).
fof(f13119,plain,
( complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),composition(sk1,complement(join(complement(sk2),composition(sk1,sk3)))))
| spl0_2 ),
inference(forward_demodulation,[],[f13117,f1471]) ).
fof(f13121,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)))))
| spl0_2 ),
inference(forward_demodulation,[],[f13119,f12370]) ).
fof(f13123,plain,
( complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(sk3,complement(composition(sk1,sk2)))))
| spl0_2 ),
inference(forward_demodulation,[],[f13121,f12952]) ).
fof(f13125,plain,
( complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))))
| spl0_2 ),
inference(forward_demodulation,[],[f13123,f1]) ).
fof(f13127,plain,
( complement(join(sk3,complement(composition(sk1,sk2)))) != join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(sk3,complement(composition(sk1,sk2)))))
| spl0_2 ),
inference(forward_demodulation,[],[f13125,f1367]) ).
fof(f13129,plain,
( $false
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f13127,f1004]) ).
fof(f13130,plain,
spl0_2,
inference(avatar_contradiction_clause,[],[f13129]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(sat_conversion,[],[f37]) ).
cnf(s3,plain,
spl0_1,
inference(sat_conversion,[],[f13113]) ).
cnf(s4,plain,
spl0_2,
inference(sat_conversion,[],[f13130]) ).
cnf(s5,plain,
$false,
inference(rat,[],[s1,s4,s3]) ).
fof(f13137,plain,
$false,
inference(avatar_sat_refutation,[],[s5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL030-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.36 % Computer : n005.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 22:53:46 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/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
% 10.38/2.33 % (268370)Input is clausal, will run a generic CNF schedule.
% 10.38/2.33 % (268379)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1058629164:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.38/2.33 % (268381)dis-21_1_sil=8000:lcm=predicate:random_seed=1294562907: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)
% 10.38/2.33 % (268375)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=3674110346:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.38/2.33 % (268378)lrs+10_1_sil=8000:sp=occurrence:random_seed=1143393217:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.38/2.33 % (268377)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2556796630:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.38/2.33 % (268376)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=588152791:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.38/2.33 % (268381)Refutation not found, incomplete strategy
% 10.38/2.33 % (268381)------------------------------
% 10.38/2.33 % (268381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.38/2.33 % (268381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.38/2.33 % (268381)CaDiCaL version: 2.1.3
% 10.38/2.33 % (268381)Termination reason: Refutation not found, incomplete strategy
% 10.38/2.33 % (268381)Time elapsed: 0.002 s
% 10.38/2.33 % (268381)Peak memory usage: 88 MB
% 10.38/2.33 % (268381)Instructions burned: 1 (million)
% 10.38/2.33 % (268379)Instruction limit reached!
% 10.38/2.33 % (268379)------------------------------
% 10.38/2.33 % (268379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.38/2.33 % (268379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.38/2.33 % (268379)CaDiCaL version: 2.1.3
% 10.38/2.33 % (268379)Termination reason: Instruction limit
% 10.38/2.33 % (268379)Termination phase: Saturation
% 10.38/2.33 % (268379)Time elapsed: 0.039 s
% 10.38/2.33 % (268379)Peak memory usage: 89 MB
% 10.38/2.33 % (268379)Instructions burned: 116 (million)
% 10.38/2.33 % (268380)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2320663125:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.38/2.33 % (268378)Instruction limit reached!
% 10.38/2.33 % (268378)------------------------------
% 10.38/2.33 % (268378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.38/2.33 % (268378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.38/2.33 % (268378)CaDiCaL version: 2.1.3
% 10.38/2.33 % (268378)Termination reason: Instruction limit
% 10.38/2.33 % (268378)Termination phase: Saturation
% 10.38/2.33 % (268378)Time elapsed: 0.067 s
% 10.38/2.33 % (268378)Peak memory usage: 89 MB
% 10.38/2.33 % (268378)Instructions burned: 107 (million)
% 10.38/2.33 % (268380)Instruction limit reached!
% 10.38/2.33 % (268380)------------------------------
% 10.38/2.33 % (268380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.38/2.33 % (268380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.38/2.33 % (268380)CaDiCaL version: 2.1.3
% 10.38/2.33 % (268380)Termination reason: Instruction limit
% 10.38/2.33 % (268380)Termination phase: Saturation
% 10.38/2.33 % (268380)Time elapsed: 0.110 s
% 10.38/2.33 % (268380)Peak memory usage: 89 MB
% 10.38/2.33 % (268380)Instructions burned: 183 (million)
% 10.38/2.33 % (268389)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=2491909555:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 10.38/2.33 % (268389)Instruction limit reached!
% 10.38/2.33 % (268389)------------------------------
% 10.38/2.33 % (268389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.38/2.33 % (268389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.38/2.33 % (268389)CaDiCaL version: 2.1.3
% 10.38/2.33 % (268389)Termination reason: Instruction limit
% 10.38/2.33 % (268389)Termination phase: Saturation
% 10.38/2.33 % (268389)Time elapsed: 0.042 s
% 10.38/2.33 % (268389)Peak memory usage: 89 MB
% 10.38/2.33 % (268389)Instructions burned: 144 (million)
% 10.38/2.33 % (268390)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2431012345: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.38/2.33 % (268381)------------------------------
% 10.38/2.33 % (268381)------------------------------
% 10.38/2.33 % (268391)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=500129422:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 10.38/2.33 % (268393)lrs+10_64_to=lpo:sil=8000:random_seed=1205388827:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 10.38/2.33 % (268390)Instruction limit reached!
% 10.38/2.33 % (268390)------------------------------
% 10.38/2.33 % (268390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.38/2.33 % (268390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.38/2.33 % (268390)CaDiCaL version: 2.1.3
% 10.38/2.33 % (268390)Termination reason: Instruction limit
% 10.38/2.33 % (268390)Termination phase: Saturation
% 10.38/2.33 % (268390)Time elapsed: 0.114 s
% 10.38/2.33 % (268390)Peak memory usage: 91 MB
% 10.38/2.33 % (268390)Instructions burned: 190 (million)
% 10.38/2.33 % (268393)Instruction limit reached!
% 10.38/2.33 % (268393)------------------------------
% 10.38/2.33 % (268393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.38/2.33 % (268393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.38/2.33 % (268393)CaDiCaL version: 2.1.3
% 10.38/2.33 % (268393)Termination reason: Instruction limit
% 10.38/2.33 % (268393)Termination phase: Saturation
% 10.38/2.33 % (268393)Time elapsed: 0.042 s
% 10.38/2.33 % (268393)Peak memory usage: 89 MB
% 10.38/2.33 % (268393)Instructions burned: 129 (million)
% 10.38/2.33 % (268391)Instruction limit reached!
% 10.38/2.33 % (268391)------------------------------
% 10.38/2.33 % (268391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.38/2.33 % (268391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.38/2.33 % (268391)CaDiCaL version: 2.1.3
% 10.38/2.33 % (268391)Termination reason: Instruction limit
% 10.38/2.33 % (268391)Termination phase: Saturation
% 10.38/2.33 % (268391)Time elapsed: 0.122 s
% 10.38/2.33 % (268391)Peak memory usage: 91 MB
% 10.38/2.33 % (268391)Instructions burned: 219 (million)
% 10.38/2.33 % (268395)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3195319885:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 10.38/2.33 % (268399)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3803783121:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 10.38/2.33 % (268398)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=670976423:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 10.38/2.33 % (268395)Instruction limit reached!
% 10.38/2.33 % (268395)------------------------------
% 10.38/2.33 % (268395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.38/2.33 % (268395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.38/2.33 % (268395)CaDiCaL version: 2.1.3
% 10.38/2.33 % (268395)Termination reason: Instruction limit
% 10.38/2.33 % (268395)Termination phase: Saturation
% 10.38/2.33 % (268395)Time elapsed: 0.125 s
% 10.38/2.33 % (268395)Peak memory usage: 90 MB
% 10.38/2.33 % (268395)Instructions burned: 194 (million)
% 10.38/2.33 % (268400)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=2520357299:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 10.38/2.33 % (268398)Instruction limit reached!
% 10.38/2.33 % (268398)------------------------------
% 10.38/2.33 % (268398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.38/2.33 % (268398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.38/2.33 % (268398)CaDiCaL version: 2.1.3
% 10.38/2.33 % (268398)Termination reason: Instruction limit
% 10.38/2.33 % (268398)Termination phase: Saturation
% 10.38/2.33 % (268398)Time elapsed: 0.103 s
% 10.38/2.33 % (268398)Peak memory usage: 91 MB
% 10.38/2.33 % (268398)Instructions burned: 157 (million)
% 10.38/2.33 % (268400)Instruction limit reached!
% 10.38/2.33 % (268400)------------------------------
% 10.38/2.33 % (268400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.38/2.33 % (268400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.38/2.33 % (268400)CaDiCaL version: 2.1.3
% 10.38/2.33 % (268400)Termination reason: Instruction limit
% 10.38/2.34 % (268400)Termination phase: Saturation
% 10.38/2.34 % (268400)Time elapsed: 0.065 s
% 10.38/2.34 % (268400)Peak memory usage: 89 MB
% 10.38/2.34 % (268400)Instructions burned: 106 (million)
% 10.38/2.34 % (268404)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=30272746:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 10.38/2.34 % (268404)Instruction limit reached!
% 10.38/2.34 % (268404)------------------------------
% 10.38/2.34 % (268404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.38/2.34 % (268404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.38/2.34 % (268404)CaDiCaL version: 2.1.3
% 10.38/2.34 % (268404)Termination reason: Instruction limit
% 10.38/2.34 % (268404)Termination phase: Saturation
% 10.38/2.34 % (268404)Time elapsed: 0.060 s
% 10.38/2.34 % (268404)Peak memory usage: 88 MB
% 10.38/2.34 % (268404)Instructions burned: 108 (million)
% 10.38/2.34 % (268406)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=963405732:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 10.38/2.34 % (268407)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2989982494:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 10.38/2.34 % (268406)Instruction limit reached!
% 10.38/2.34 % (268406)------------------------------
% 10.38/2.34 % (268406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.38/2.34 % (268406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.38/2.34 % (268406)CaDiCaL version: 2.1.3
% 10.38/2.34 % (268406)Termination reason: Instruction limit
% 10.38/2.34 % (268406)Termination phase: Saturation
% 10.38/2.34 % (268406)Time elapsed: 0.124 s
% 10.38/2.34 % (268406)Peak memory usage: 89 MB
% 10.38/2.34 % (268406)Instructions burned: 244 (million)
% 10.38/2.34 % (268409)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1777951176:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 10.38/2.34 % (268409)Instruction limit reached!
% 10.38/2.34 % (268409)------------------------------
% 10.38/2.34 % (268409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.38/2.34 % (268409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.38/2.34 % (268409)CaDiCaL version: 2.1.3
% 10.38/2.34 % (268409)Termination reason: Instruction limit
% 10.38/2.34 % (268409)Termination phase: Saturation
% 10.38/2.34 % (268409)Time elapsed: 0.078 s
% 10.38/2.34 % (268409)Peak memory usage: 89 MB
% 10.38/2.34 % (268409)Instructions burned: 135 (million)
% 10.38/2.34 % (268412)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=434376503:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 10.38/2.34 % (268399)First to succeed.
% 10.38/2.34 % (268399)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-268370"
% 10.38/2.34 % (268414)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1587689828:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 10.38/2.34 % (268414)Instruction limit reached!
% 10.38/2.34 % (268414)------------------------------
% 10.38/2.34 % (268414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.38/2.34 % (268414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.38/2.34 % (268414)CaDiCaL version: 2.1.3
% 10.38/2.34 % (268414)Termination reason: Instruction limit
% 10.38/2.34 % (268414)Termination phase: Saturation
% 10.38/2.34 % (268414)Time elapsed: 0.129 s
% 10.38/2.34 % (268414)Peak memory usage: 90 MB
% 10.38/2.34 % (268414)Instructions burned: 192 (million)
% 10.38/2.34 % (268399)Refutation found. Thanks to Tanya!
% 10.38/2.34 % SZS status Unsatisfiable for theBenchmark
% 10.38/2.34 % SZS output start Proof for theBenchmark
% See solution above
% 11.10/2.53 % (268399)------------------------------
% 11.10/2.53 % (268399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.10/2.53 % (268399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.10/2.53 % (268399)CaDiCaL version: 2.1.3
% 11.10/2.53 % (268399)Termination reason: Refutation
% 11.10/2.53 % (268399)Time elapsed: 0.652 s
% 11.10/2.53 % (268399)Peak memory usage: 138 MB
% 11.10/2.53 % (268399)Instructions burned: 1875 (million)
% 11.10/2.53 % (268399)------------------------------
% 11.10/2.53 % (268399)------------------------------
% 11.10/2.53 % (268370)Success in time 1.487 s
% 11.10/2.53 % Vampire exiting
%------------------------------------------------------------------------------