%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT017-1 : TPTP v9.3.1. Bugfixed v2.2.1.
% 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 11:45:50 AM UTC 2026
% Result : Unsatisfiable 8.99s 2.30s
% Output : Refutation 10.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 53
% Syntax : Number of formulae : 236 ( 106 unt; 46 def)
% Number of atoms : 492 ( 174 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 495 ( 239 ~; 233 |; 0 &)
% ( 23 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 25 ( 23 usr; 24 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 26 con; 0-2 aty)
% Number of variables : 29 ( 0 sgn 29 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : join(complement(X0),X0) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',top) ).
fof(f3,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption2) ).
fof(f5,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f8,axiom,
! [X0] : complement(complement(X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement_involution) ).
fof(f11,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_complement) ).
fof(f12,negated_conjecture,
join(a,join(meet(complement(a),meet(join(a,complement(b)),join(a,b))),meet(complement(a),join(meet(complement(a),b),meet(complement(a),complement(b)))))) != n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_e2) ).
fof(f13,plain,
n1 != join(a,join(meet(complement(a),meet(join(a,complement(b)),join(a,b))),meet(complement(a),join(meet(complement(a),b),meet(complement(a),complement(b)))))),
inference(reorient_equations,[],[f12]) ).
fof(f15,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(X1)))) = X0,
inference(definition_unfolding,[],[f3,f11]) ).
fof(f18,plain,
n1 != join(a,join(complement(join(complement(complement(a)),complement(complement(join(complement(join(a,complement(b))),complement(join(a,b))))))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))),
inference(definition_unfolding,[],[f13,f11,f11,f11,f11,f11]) ).
fof(f19,definition,
sF0 = complement(a),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f20,plain,
complement(a) = sF0,
inference(reorient_equations,[],[f19]) ).
fof(f21,definition,
sF1 = complement(sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f22,plain,
complement(sF0) = sF1,
inference(reorient_equations,[],[f21]) ).
fof(f23,definition,
sF2 = complement(b),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f24,plain,
complement(b) = sF2,
inference(reorient_equations,[],[f23]) ).
fof(f25,definition,
sF3 = join(a,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f26,plain,
join(a,sF2) = sF3,
inference(reorient_equations,[],[f25]) ).
fof(f27,definition,
sF4 = complement(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f28,plain,
complement(sF3) = sF4,
inference(reorient_equations,[],[f27]) ).
fof(f29,definition,
sF5 = join(a,b),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f30,plain,
join(a,b) = sF5,
inference(reorient_equations,[],[f29]) ).
fof(f31,definition,
sF6 = complement(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f32,plain,
complement(sF5) = sF6,
inference(reorient_equations,[],[f31]) ).
fof(f33,definition,
sF7 = join(sF4,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f34,plain,
join(sF4,sF6) = sF7,
inference(reorient_equations,[],[f33]) ).
fof(f35,definition,
sF8 = complement(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f36,plain,
complement(sF7) = sF8,
inference(reorient_equations,[],[f35]) ).
fof(f37,definition,
sF9 = complement(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f38,plain,
complement(sF8) = sF9,
inference(reorient_equations,[],[f37]) ).
fof(f39,definition,
sF10 = join(sF1,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f40,plain,
join(sF1,sF9) = sF10,
inference(reorient_equations,[],[f39]) ).
fof(f41,definition,
sF11 = complement(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f42,plain,
complement(sF10) = sF11,
inference(reorient_equations,[],[f41]) ).
fof(f43,definition,
sF12 = join(sF1,sF2),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f44,plain,
join(sF1,sF2) = sF12,
inference(reorient_equations,[],[f43]) ).
fof(f45,definition,
sF13 = complement(sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f46,plain,
complement(sF12) = sF13,
inference(reorient_equations,[],[f45]) ).
fof(f47,definition,
sF14 = complement(sF2),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f48,plain,
complement(sF2) = sF14,
inference(reorient_equations,[],[f47]) ).
fof(f49,definition,
sF15 = join(sF1,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f50,plain,
join(sF1,sF14) = sF15,
inference(reorient_equations,[],[f49]) ).
fof(f51,definition,
sF16 = complement(sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f52,plain,
complement(sF15) = sF16,
inference(reorient_equations,[],[f51]) ).
fof(f53,definition,
sF17 = join(sF13,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f54,plain,
join(sF13,sF16) = sF17,
inference(reorient_equations,[],[f53]) ).
fof(f55,definition,
sF18 = complement(sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f56,plain,
complement(sF17) = sF18,
inference(reorient_equations,[],[f55]) ).
fof(f57,definition,
sF19 = join(sF1,sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f58,plain,
join(sF1,sF18) = sF19,
inference(reorient_equations,[],[f57]) ).
fof(f59,definition,
sF20 = complement(sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f60,plain,
complement(sF19) = sF20,
inference(reorient_equations,[],[f59]) ).
fof(f61,definition,
sF21 = join(sF11,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f62,plain,
join(sF11,sF20) = sF21,
inference(reorient_equations,[],[f61]) ).
fof(f63,definition,
sF22 = join(a,sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f64,plain,
join(a,sF21) = sF22,
inference(reorient_equations,[],[f63]) ).
fof(f65,plain,
n1 != sF22,
inference(definition_folding,[],[f18,f64,f62,f60,f58,f56,f54,f52,f50,f48,f24,f22,f20,f46,f44,f24,f22,f20,f22,f20,f42,f40,f38,f36,f34,f32,f30,f28,f26,f24,f22,f20]) ).
fof(f68,plain,
! [X0] : n1 = join(X0,complement(X0)),
inference(forward_demodulation,[],[f1,f5]) ).
fof(f69,plain,
sF3 = join(sF2,a),
inference(forward_demodulation,[],[f26,f5]) ).
fof(f70,plain,
sF5 = join(b,a),
inference(forward_demodulation,[],[f30,f5]) ).
fof(f71,plain,
sF10 = join(sF9,sF1),
inference(forward_demodulation,[],[f40,f5]) ).
fof(f72,plain,
sF12 = join(sF2,sF1),
inference(forward_demodulation,[],[f44,f5]) ).
fof(f73,plain,
sF15 = join(sF14,sF1),
inference(forward_demodulation,[],[f50,f5]) ).
fof(f74,plain,
sF19 = join(sF18,sF1),
inference(forward_demodulation,[],[f58,f5]) ).
fof(f75,plain,
sF22 = join(sF21,a),
inference(forward_demodulation,[],[f64,f5]) ).
fof(f89,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,complement(X1)))),
inference(superposition,[],[f15,f8]) ).
fof(f92,definition,
( spl23_1
<=> complement(a) = sF0 ),
introduced(definition,[new_symbols(definition,[spl23_1])],[avatar_definition]) ).
fof(f94,plain,
( complement(a) = sF0
| ~ spl23_1 ),
inference(avatar_component_clause,[],[f92]) ).
fof(f95,plain,
spl23_1,
inference(avatar_split_clause,[],[f20,f92]) ).
fof(f97,definition,
( spl23_2
<=> complement(b) = sF2 ),
introduced(definition,[new_symbols(definition,[spl23_2])],[avatar_definition]) ).
fof(f99,plain,
( complement(b) = sF2
| ~ spl23_2 ),
inference(avatar_component_clause,[],[f97]) ).
fof(f100,plain,
spl23_2,
inference(avatar_split_clause,[],[f24,f97]) ).
fof(f101,plain,
( b = complement(sF2)
| ~ spl23_2 ),
inference(superposition,[],[f8,f99]) ).
fof(f104,plain,
( b = sF14
| ~ spl23_2 ),
inference(forward_demodulation,[],[f101,f48]) ).
fof(f107,plain,
( sF5 = join(sF14,a)
| ~ spl23_2 ),
inference(backward_demodulation,[],[f70,f104]) ).
fof(f114,plain,
( a = complement(sF0)
| ~ spl23_1 ),
inference(superposition,[],[f8,f94]) ).
fof(f117,plain,
( a = sF1
| ~ spl23_1 ),
inference(forward_demodulation,[],[f114,f22]) ).
fof(f119,plain,
( sF5 = join(sF14,sF1)
| ~ spl23_1
| ~ spl23_2 ),
inference(backward_demodulation,[],[f107,f117]) ).
fof(f120,plain,
( sF0 = complement(sF1)
| ~ spl23_1 ),
inference(backward_demodulation,[],[f94,f117]) ).
fof(f121,plain,
( sF22 = join(sF21,sF1)
| ~ spl23_1 ),
inference(backward_demodulation,[],[f75,f117]) ).
fof(f122,plain,
( sF3 = join(sF2,sF1)
| ~ spl23_1 ),
inference(backward_demodulation,[],[f69,f117]) ).
fof(f123,plain,
( sF3 = sF12
| ~ spl23_1 ),
inference(forward_demodulation,[],[f122,f72]) ).
fof(f124,plain,
( sF5 = sF15
| ~ spl23_1
| ~ spl23_2 ),
inference(forward_demodulation,[],[f119,f73]) ).
fof(f125,plain,
( sF3 = join(sF2,sF1)
| ~ spl23_1 ),
inference(backward_demodulation,[],[f72,f123]) ).
fof(f126,plain,
( complement(sF3) = sF13
| ~ spl23_1 ),
inference(backward_demodulation,[],[f46,f123]) ).
fof(f127,plain,
( sF5 = join(sF14,sF1)
| ~ spl23_1
| ~ spl23_2 ),
inference(backward_demodulation,[],[f73,f124]) ).
fof(f128,plain,
( complement(sF5) = sF16
| ~ spl23_1
| ~ spl23_2 ),
inference(backward_demodulation,[],[f52,f124]) ).
fof(f129,plain,
( sF4 = sF13
| ~ spl23_1 ),
inference(forward_demodulation,[],[f126,f28]) ).
fof(f130,plain,
( sF6 = sF16
| ~ spl23_1
| ~ spl23_2 ),
inference(forward_demodulation,[],[f128,f32]) ).
fof(f131,plain,
( sF17 = join(sF4,sF16)
| ~ spl23_1 ),
inference(backward_demodulation,[],[f54,f129]) ).
fof(f132,plain,
( join(sF4,sF6) = sF17
| ~ spl23_1
| ~ spl23_2 ),
inference(forward_demodulation,[],[f131,f130]) ).
fof(f133,plain,
( sF7 = sF17
| ~ spl23_1
| ~ spl23_2 ),
inference(forward_demodulation,[],[f132,f34]) ).
fof(f134,plain,
( complement(sF7) = sF18
| ~ spl23_1
| ~ spl23_2 ),
inference(backward_demodulation,[],[f56,f133]) ).
fof(f135,plain,
( sF8 = sF18
| ~ spl23_1
| ~ spl23_2 ),
inference(forward_demodulation,[],[f134,f36]) ).
fof(f136,plain,
( sF19 = join(sF8,sF1)
| ~ spl23_1
| ~ spl23_2 ),
inference(backward_demodulation,[],[f74,f135]) ).
fof(f143,definition,
( spl23_5
<=> complement(sF0) = sF1 ),
introduced(definition,[new_symbols(definition,[spl23_5])],[avatar_definition]) ).
fof(f145,plain,
( complement(sF0) = sF1
| ~ spl23_5 ),
inference(avatar_component_clause,[],[f143]) ).
fof(f146,plain,
spl23_5,
inference(avatar_split_clause,[],[f22,f143]) ).
fof(f165,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f179,definition,
( spl23_8
<=> n1 = sF22 ),
introduced(definition,[new_symbols(definition,[spl23_8])],[avatar_definition]) ).
fof(f181,plain,
( n1 != sF22
| spl23_8 ),
inference(avatar_component_clause,[],[f179]) ).
fof(f182,plain,
~ spl23_8,
inference(avatar_split_clause,[],[f65,f179]) ).
fof(f187,definition,
( spl23_9
<=> complement(sF8) = sF9 ),
introduced(definition,[new_symbols(definition,[spl23_9])],[avatar_definition]) ).
fof(f189,plain,
( complement(sF8) = sF9
| ~ spl23_9 ),
inference(avatar_component_clause,[],[f187]) ).
fof(f190,plain,
spl23_9,
inference(avatar_split_clause,[],[f38,f187]) ).
fof(f192,definition,
( spl23_10
<=> complement(sF7) = sF8 ),
introduced(definition,[new_symbols(definition,[spl23_10])],[avatar_definition]) ).
fof(f194,plain,
( complement(sF7) = sF8
| ~ spl23_10 ),
inference(avatar_component_clause,[],[f192]) ).
fof(f195,plain,
spl23_10,
inference(avatar_split_clause,[],[f36,f192]) ).
fof(f197,definition,
( spl23_11
<=> complement(sF3) = sF4 ),
introduced(definition,[new_symbols(definition,[spl23_11])],[avatar_definition]) ).
fof(f199,plain,
( complement(sF3) = sF4
| ~ spl23_11 ),
inference(avatar_component_clause,[],[f197]) ).
fof(f200,plain,
spl23_11,
inference(avatar_split_clause,[],[f28,f197]) ).
fof(f202,definition,
( spl23_12
<=> complement(sF5) = sF6 ),
introduced(definition,[new_symbols(definition,[spl23_12])],[avatar_definition]) ).
fof(f204,plain,
( complement(sF5) = sF6
| ~ spl23_12 ),
inference(avatar_component_clause,[],[f202]) ).
fof(f205,plain,
spl23_12,
inference(avatar_split_clause,[],[f32,f202]) ).
fof(f207,definition,
( spl23_13
<=> complement(sF10) = sF11 ),
introduced(definition,[new_symbols(definition,[spl23_13])],[avatar_definition]) ).
fof(f209,plain,
( complement(sF10) = sF11
| ~ spl23_13 ),
inference(avatar_component_clause,[],[f207]) ).
fof(f210,plain,
spl23_13,
inference(avatar_split_clause,[],[f42,f207]) ).
fof(f212,definition,
( spl23_14
<=> sF22 = join(sF21,sF1) ),
introduced(definition,[new_symbols(definition,[spl23_14])],[avatar_definition]) ).
fof(f214,plain,
( sF22 = join(sF21,sF1)
| ~ spl23_14 ),
inference(avatar_component_clause,[],[f212]) ).
fof(f215,plain,
( spl23_14
| ~ spl23_1 ),
inference(avatar_split_clause,[],[f121,f92,f212]) ).
fof(f219,definition,
( spl23_15
<=> complement(sF19) = sF20 ),
introduced(definition,[new_symbols(definition,[spl23_15])],[avatar_definition]) ).
fof(f221,plain,
( complement(sF19) = sF20
| ~ spl23_15 ),
inference(avatar_component_clause,[],[f219]) ).
fof(f222,plain,
spl23_15,
inference(avatar_split_clause,[],[f60,f219]) ).
fof(f226,definition,
( spl23_16
<=> sF0 = complement(sF1) ),
introduced(definition,[new_symbols(definition,[spl23_16])],[avatar_definition]) ).
fof(f228,plain,
( sF0 = complement(sF1)
| ~ spl23_16 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f229,plain,
( spl23_16
| ~ spl23_1 ),
inference(avatar_split_clause,[],[f120,f92,f226]) ).
fof(f236,plain,
( n1 = join(sF10,sF11)
| ~ spl23_13 ),
inference(superposition,[],[f68,f209]) ).
fof(f239,plain,
( sF7 = complement(sF8)
| ~ spl23_10 ),
inference(superposition,[],[f8,f194]) ).
fof(f241,plain,
( sF7 = sF9
| ~ spl23_9
| ~ spl23_10 ),
inference(forward_demodulation,[],[f239,f189]) ).
fof(f244,plain,
( sF7 = complement(sF8)
| ~ spl23_9
| ~ spl23_10 ),
inference(backward_demodulation,[],[f189,f241]) ).
fof(f245,plain,
( sF10 = join(sF7,sF1)
| ~ spl23_9
| ~ spl23_10 ),
inference(backward_demodulation,[],[f71,f241]) ).
fof(f425,definition,
( spl23_18
<=> join(sF4,sF6) = sF7 ),
introduced(definition,[new_symbols(definition,[spl23_18])],[avatar_definition]) ).
fof(f427,plain,
( join(sF4,sF6) = sF7
| ~ spl23_18 ),
inference(avatar_component_clause,[],[f425]) ).
fof(f428,plain,
spl23_18,
inference(avatar_split_clause,[],[f34,f425]) ).
fof(f429,plain,
( ! [X0] : join(sF4,join(sF6,X0)) = join(sF7,X0)
| ~ spl23_18 ),
inference(superposition,[],[f7,f427]) ).
fof(f431,definition,
( spl23_19
<=> join(sF11,sF20) = sF21 ),
introduced(definition,[new_symbols(definition,[spl23_19])],[avatar_definition]) ).
fof(f433,plain,
( join(sF11,sF20) = sF21
| ~ spl23_19 ),
inference(avatar_component_clause,[],[f431]) ).
fof(f434,plain,
spl23_19,
inference(avatar_split_clause,[],[f62,f431]) ).
fof(f435,plain,
( ! [X0] : join(sF11,join(sF20,X0)) = join(sF21,X0)
| ~ spl23_19 ),
inference(superposition,[],[f7,f433]) ).
fof(f447,definition,
( spl23_22
<=> sF3 = join(sF2,sF1) ),
introduced(definition,[new_symbols(definition,[spl23_22])],[avatar_definition]) ).
fof(f449,plain,
( sF3 = join(sF2,sF1)
| ~ spl23_22 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f450,plain,
( spl23_22
| ~ spl23_1 ),
inference(avatar_split_clause,[],[f125,f92,f447]) ).
fof(f465,plain,
! [X0,X1] : complement(X1) = join(complement(X1),complement(join(X1,X0))),
inference(superposition,[],[f89,f8]) ).
fof(f500,definition,
( spl23_24
<=> sF10 = join(sF7,sF1) ),
introduced(definition,[new_symbols(definition,[spl23_24])],[avatar_definition]) ).
fof(f502,plain,
( sF10 = join(sF7,sF1)
| ~ spl23_24 ),
inference(avatar_component_clause,[],[f500]) ).
fof(f503,plain,
( spl23_24
| ~ spl23_9
| ~ spl23_10 ),
inference(avatar_split_clause,[],[f245,f192,f187,f500]) ).
fof(f504,plain,
( ! [X0] : join(sF7,join(sF1,X0)) = join(sF10,X0)
| ~ spl23_24 ),
inference(superposition,[],[f7,f502]) ).
fof(f506,definition,
( spl23_25
<=> sF5 = join(sF14,sF1) ),
introduced(definition,[new_symbols(definition,[spl23_25])],[avatar_definition]) ).
fof(f508,plain,
( sF5 = join(sF14,sF1)
| ~ spl23_25 ),
inference(avatar_component_clause,[],[f506]) ).
fof(f509,plain,
( spl23_25
| ~ spl23_1
| ~ spl23_2 ),
inference(avatar_split_clause,[],[f127,f97,f92,f506]) ).
fof(f512,definition,
( spl23_26
<=> sF7 = complement(sF8) ),
introduced(definition,[new_symbols(definition,[spl23_26])],[avatar_definition]) ).
fof(f514,plain,
( sF7 = complement(sF8)
| ~ spl23_26 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f515,plain,
( spl23_26
| ~ spl23_9
| ~ spl23_10 ),
inference(avatar_split_clause,[],[f244,f192,f187,f512]) ).
fof(f528,definition,
( spl23_27
<=> sF19 = join(sF8,sF1) ),
introduced(definition,[new_symbols(definition,[spl23_27])],[avatar_definition]) ).
fof(f530,plain,
( sF19 = join(sF8,sF1)
| ~ spl23_27 ),
inference(avatar_component_clause,[],[f528]) ).
fof(f531,plain,
( spl23_27
| ~ spl23_1
| ~ spl23_2 ),
inference(avatar_split_clause,[],[f136,f97,f92,f528]) ).
fof(f1039,plain,
! [X0,X1] : complement(X1) = join(complement(X1),complement(join(X0,X1))),
inference(superposition,[],[f465,f5]) ).
fof(f1130,plain,
( complement(sF1) = join(complement(sF1),complement(sF3))
| ~ spl23_22 ),
inference(superposition,[],[f1039,f449]) ).
fof(f1135,plain,
( complement(sF1) = join(complement(sF1),complement(sF5))
| ~ spl23_25 ),
inference(superposition,[],[f1039,f508]) ).
fof(f1149,plain,
( complement(sF1) = join(complement(sF5),complement(sF1))
| ~ spl23_25 ),
inference(forward_demodulation,[],[f1135,f5]) ).
fof(f1154,plain,
( complement(sF1) = join(complement(sF3),complement(sF1))
| ~ spl23_22 ),
inference(forward_demodulation,[],[f1130,f5]) ).
fof(f1162,plain,
( sF0 = join(complement(sF5),sF0)
| ~ spl23_16
| ~ spl23_25 ),
inference(forward_demodulation,[],[f1149,f228]) ).
fof(f1166,plain,
( sF0 = join(complement(sF3),sF0)
| ~ spl23_16
| ~ spl23_22 ),
inference(forward_demodulation,[],[f1154,f228]) ).
fof(f1170,plain,
( sF0 = join(sF0,complement(sF5))
| ~ spl23_16
| ~ spl23_25 ),
inference(forward_demodulation,[],[f1162,f5]) ).
fof(f1174,plain,
( sF0 = join(sF0,complement(sF3))
| ~ spl23_16
| ~ spl23_22 ),
inference(forward_demodulation,[],[f1166,f5]) ).
fof(f1177,plain,
( sF0 = join(sF0,sF6)
| ~ spl23_12
| ~ spl23_16
| ~ spl23_25 ),
inference(forward_demodulation,[],[f1170,f204]) ).
fof(f1181,plain,
( sF0 = join(sF0,sF4)
| ~ spl23_11
| ~ spl23_16
| ~ spl23_22 ),
inference(forward_demodulation,[],[f1174,f199]) ).
fof(f1907,definition,
( spl23_38
<=> sF0 = join(sF0,sF4) ),
introduced(definition,[new_symbols(definition,[spl23_38])],[avatar_definition]) ).
fof(f1909,plain,
( sF0 = join(sF0,sF4)
| ~ spl23_38 ),
inference(avatar_component_clause,[],[f1907]) ).
fof(f1910,plain,
( spl23_38
| ~ spl23_11
| ~ spl23_16
| ~ spl23_22 ),
inference(avatar_split_clause,[],[f1181,f447,f226,f197,f1907]) ).
fof(f1928,definition,
( spl23_39
<=> sF0 = join(sF0,sF6) ),
introduced(definition,[new_symbols(definition,[spl23_39])],[avatar_definition]) ).
fof(f1930,plain,
( sF0 = join(sF0,sF6)
| ~ spl23_39 ),
inference(avatar_component_clause,[],[f1928]) ).
fof(f1931,plain,
( spl23_39
| ~ spl23_12
| ~ spl23_16
| ~ spl23_25 ),
inference(avatar_split_clause,[],[f1177,f506,f226,f202,f1928]) ).
fof(f2037,plain,
( ! [X0] : join(sF7,X0) = join(sF4,join(X0,sF6))
| ~ spl23_18 ),
inference(superposition,[],[f429,f5]) ).
fof(f4062,definition,
( spl23_65
<=> n1 = join(sF10,sF11) ),
introduced(definition,[new_symbols(definition,[spl23_65])],[avatar_definition]) ).
fof(f4064,plain,
( n1 = join(sF10,sF11)
| ~ spl23_65 ),
inference(avatar_component_clause,[],[f4062]) ).
fof(f4065,plain,
( spl23_65
| ~ spl23_13 ),
inference(avatar_split_clause,[],[f236,f207,f4062]) ).
fof(f5217,plain,
( join(sF4,sF0) = join(sF7,sF0)
| ~ spl23_18
| ~ spl23_39 ),
inference(superposition,[],[f2037,f1930]) ).
fof(f5245,plain,
( join(sF4,sF0) = join(sF0,sF7)
| ~ spl23_18
| ~ spl23_39 ),
inference(forward_demodulation,[],[f5217,f5]) ).
fof(f5259,plain,
( join(sF0,sF4) = join(sF0,sF7)
| ~ spl23_18
| ~ spl23_39 ),
inference(forward_demodulation,[],[f5245,f5]) ).
fof(f5266,plain,
( sF0 = join(sF0,sF7)
| ~ spl23_18
| ~ spl23_38
| ~ spl23_39 ),
inference(forward_demodulation,[],[f5259,f1909]) ).
fof(f12562,definition,
( spl23_99
<=> sF0 = join(sF0,sF7) ),
introduced(definition,[new_symbols(definition,[spl23_99])],[avatar_definition]) ).
fof(f12564,plain,
( sF0 = join(sF0,sF7)
| ~ spl23_99 ),
inference(avatar_component_clause,[],[f12562]) ).
fof(f12565,plain,
( spl23_99
| ~ spl23_18
| ~ spl23_38
| ~ spl23_39 ),
inference(avatar_split_clause,[],[f5266,f1928,f1907,f425,f12562]) ).
fof(f12573,plain,
( complement(sF7) = join(complement(sF7),complement(sF0))
| ~ spl23_99 ),
inference(superposition,[],[f1039,f12564]) ).
fof(f12581,plain,
( complement(sF7) = join(complement(sF0),complement(sF7))
| ~ spl23_99 ),
inference(forward_demodulation,[],[f12573,f5]) ).
fof(f12586,plain,
( sF8 = join(complement(sF0),sF8)
| ~ spl23_10
| ~ spl23_99 ),
inference(forward_demodulation,[],[f12581,f194]) ).
fof(f12588,plain,
( sF8 = join(sF8,complement(sF0))
| ~ spl23_10
| ~ spl23_99 ),
inference(forward_demodulation,[],[f12586,f5]) ).
fof(f12590,plain,
( sF8 = join(sF8,sF1)
| ~ spl23_5
| ~ spl23_10
| ~ spl23_99 ),
inference(forward_demodulation,[],[f12588,f145]) ).
fof(f12592,plain,
( sF8 = sF19
| ~ spl23_5
| ~ spl23_10
| ~ spl23_27
| ~ spl23_99 ),
inference(forward_demodulation,[],[f12590,f530]) ).
fof(f12674,plain,
( complement(sF8) = sF20
| ~ spl23_5
| ~ spl23_10
| ~ spl23_15
| ~ spl23_27
| ~ spl23_99 ),
inference(backward_demodulation,[],[f221,f12592]) ).
fof(f12741,plain,
( sF7 = sF20
| ~ spl23_5
| ~ spl23_10
| ~ spl23_15
| ~ spl23_26
| ~ spl23_27
| ~ spl23_99 ),
inference(forward_demodulation,[],[f12674,f514]) ).
fof(f12745,plain,
( ! [X0] : join(sF21,X0) = join(sF11,join(sF7,X0))
| ~ spl23_5
| ~ spl23_10
| ~ spl23_15
| ~ spl23_19
| ~ spl23_26
| ~ spl23_27
| ~ spl23_99 ),
inference(backward_demodulation,[],[f435,f12741]) ).
fof(f12833,plain,
( ! [X0] : join(sF21,X0) = join(sF7,join(X0,sF11))
| ~ spl23_5
| ~ spl23_10
| ~ spl23_15
| ~ spl23_19
| ~ spl23_26
| ~ spl23_27
| ~ spl23_99 ),
inference(forward_demodulation,[],[f12745,f165]) ).
fof(f13087,plain,
( join(sF21,sF1) = join(sF10,sF11)
| ~ spl23_5
| ~ spl23_10
| ~ spl23_15
| ~ spl23_19
| ~ spl23_24
| ~ spl23_26
| ~ spl23_27
| ~ spl23_99 ),
inference(superposition,[],[f12833,f504]) ).
fof(f13130,plain,
( n1 = join(sF21,sF1)
| ~ spl23_5
| ~ spl23_10
| ~ spl23_15
| ~ spl23_19
| ~ spl23_24
| ~ spl23_26
| ~ spl23_27
| ~ spl23_65
| ~ spl23_99 ),
inference(forward_demodulation,[],[f13087,f4064]) ).
fof(f13153,plain,
( n1 = sF22
| ~ spl23_5
| ~ spl23_10
| ~ spl23_14
| ~ spl23_15
| ~ spl23_19
| ~ spl23_24
| ~ spl23_26
| ~ spl23_27
| ~ spl23_65
| ~ spl23_99 ),
inference(forward_demodulation,[],[f13130,f214]) ).
fof(f13165,plain,
( $false
| ~ spl23_5
| spl23_8
| ~ spl23_10
| ~ spl23_14
| ~ spl23_15
| ~ spl23_19
| ~ spl23_24
| ~ spl23_26
| ~ spl23_27
| ~ spl23_65
| ~ spl23_99 ),
inference(forward_subsumption_resolution,[],[f13153,f181]) ).
fof(f13166,plain,
( ~ spl23_5
| spl23_8
| ~ spl23_10
| ~ spl23_14
| ~ spl23_15
| ~ spl23_19
| ~ spl23_24
| ~ spl23_26
| ~ spl23_27
| ~ spl23_65
| ~ spl23_99 ),
inference(avatar_contradiction_clause,[],[f13165]) ).
cnf(s1,plain,
spl23_1,
inference(sat_conversion,[],[f95]) ).
cnf(s2,plain,
spl23_2,
inference(sat_conversion,[],[f100]) ).
cnf(s5,plain,
spl23_5,
inference(sat_conversion,[],[f146]) ).
cnf(s8,plain,
~ spl23_8,
inference(sat_conversion,[],[f182]) ).
cnf(s9,plain,
spl23_9,
inference(sat_conversion,[],[f190]) ).
cnf(s10,plain,
spl23_10,
inference(sat_conversion,[],[f195]) ).
cnf(s11,plain,
spl23_11,
inference(sat_conversion,[],[f200]) ).
cnf(s12,plain,
spl23_12,
inference(sat_conversion,[],[f205]) ).
cnf(s13,plain,
spl23_13,
inference(sat_conversion,[],[f210]) ).
cnf(s14,plain,
( ~ spl23_1
| spl23_14 ),
inference(sat_conversion,[],[f215]) ).
cnf(s15,plain,
spl23_15,
inference(sat_conversion,[],[f222]) ).
cnf(s16,plain,
( ~ spl23_1
| spl23_16 ),
inference(sat_conversion,[],[f229]) ).
cnf(s18,plain,
spl23_18,
inference(sat_conversion,[],[f428]) ).
cnf(s19,plain,
spl23_19,
inference(sat_conversion,[],[f434]) ).
cnf(s22,plain,
( ~ spl23_1
| spl23_22 ),
inference(sat_conversion,[],[f450]) ).
cnf(s24,plain,
( ~ spl23_9
| ~ spl23_10
| spl23_24 ),
inference(sat_conversion,[],[f503]) ).
cnf(s25,plain,
( ~ spl23_1
| ~ spl23_2
| spl23_25 ),
inference(sat_conversion,[],[f509]) ).
cnf(s26,plain,
( ~ spl23_9
| ~ spl23_10
| spl23_26 ),
inference(sat_conversion,[],[f515]) ).
cnf(s27,plain,
( ~ spl23_1
| ~ spl23_2
| spl23_27 ),
inference(sat_conversion,[],[f531]) ).
cnf(s38,plain,
( ~ spl23_11
| ~ spl23_16
| ~ spl23_22
| spl23_38 ),
inference(sat_conversion,[],[f1910]) ).
cnf(s39,plain,
( ~ spl23_12
| ~ spl23_16
| ~ spl23_25
| spl23_39 ),
inference(sat_conversion,[],[f1931]) ).
cnf(s65,plain,
( ~ spl23_13
| spl23_65 ),
inference(sat_conversion,[],[f4065]) ).
cnf(s99,plain,
( ~ spl23_18
| ~ spl23_38
| ~ spl23_39
| spl23_99 ),
inference(sat_conversion,[],[f12565]) ).
cnf(s106,plain,
( ~ spl23_5
| spl23_8
| ~ spl23_10
| ~ spl23_14
| ~ spl23_15
| ~ spl23_19
| ~ spl23_24
| ~ spl23_26
| ~ spl23_27
| ~ spl23_65
| ~ spl23_99 ),
inference(sat_conversion,[],[f13166]) ).
cnf(s112,plain,
spl23_65,
inference(rat,[],[s65,s13]) ).
cnf(s124,plain,
spl23_26,
inference(rat,[],[s26,s10,s9]) ).
cnf(s125,plain,
spl23_24,
inference(rat,[],[s24,s10,s9]) ).
cnf(s136,plain,
spl23_27,
inference(rat,[],[s27,s2,s1]) ).
cnf(s137,plain,
spl23_25,
inference(rat,[],[s25,s2,s1]) ).
cnf(s139,plain,
spl23_22,
inference(rat,[],[s22,s1]) ).
cnf(s143,plain,
spl23_16,
inference(rat,[],[s16,s1]) ).
cnf(s144,plain,
spl23_14,
inference(rat,[],[s14,s1]) ).
cnf(s166,plain,
spl23_39,
inference(rat,[],[s39,s137,s12,s143]) ).
cnf(s167,plain,
spl23_38,
inference(rat,[],[s38,s139,s11,s143]) ).
cnf(s176,plain,
~ spl23_99,
inference(rat,[],[s106,s136,s112,s5,s124,s125,s19,s15,s8,s10,s144]) ).
cnf(s187,plain,
$false,
inference(rat,[],[s99,s176,s18,s166,s167]) ).
fof(f13172,plain,
$false,
inference(avatar_sat_refutation,[],[s187]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT017-1 : TPTP v9.3.1. Bugfixed v2.2.1.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 % Computer : n011.cluster.edu
% 0.11/0.41 % Model : x86_64 x86_64
% 0.11/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.41 % Memory : 8046.5625MB
% 0.11/0.41 % OS : Linux 6.8.0-71-generic
% 0.11/0.41 % CPULimit : 300
% 0.11/0.41 % WCLimit : 300
% 0.11/0.41 % DateTime : Sun Sep 27 13:56:45 UTC 2026
% 0.11/0.41 % CPUTime :
% 0.11/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.44 Running first-order theorem proving
% 0.11/0.44 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
% 8.99/2.30 % (2427309)Detected a unit-equality problem, will run specialized UEQ schedule.
% 8.99/2.30 % (2427410)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=3204252972:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 8.99/2.30 % (2427412)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=72448294:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 8.99/2.30 % (2427411)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3220930084:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 8.99/2.30 % (2427415)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1129796521:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 8.99/2.30 % (2427414)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2192216053:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 8.99/2.30 % (2427416)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=854755118:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 8.99/2.30 % (2427413)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=1712667760:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 8.99/2.30 % (2427414)Instruction limit reached!
% 8.99/2.30 % (2427414)------------------------------
% 8.99/2.30 % (2427414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.99/2.30 % (2427414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/2.30 % (2427414)CaDiCaL version: 2.1.3
% 8.99/2.30 % (2427414)Termination reason: Instruction limit
% 8.99/2.30 % (2427414)Termination phase: Saturation
% 8.99/2.30 % (2427414)Time elapsed: 0.121 s
% 8.99/2.30 % (2427414)Peak memory usage: 89 MB
% 8.99/2.30 % (2427414)Instructions burned: 182 (million)
% 8.99/2.30 % (2427413)Instruction limit reached!
% 8.99/2.30 % (2427413)------------------------------
% 8.99/2.30 % (2427413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.99/2.30 % (2427413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/2.30 % (2427413)CaDiCaL version: 2.1.3
% 8.99/2.30 % (2427413)Termination reason: Instruction limit
% 8.99/2.30 % (2427413)Termination phase: Saturation
% 8.99/2.30 % (2427413)Time elapsed: 0.099 s
% 8.99/2.30 % (2427413)Peak memory usage: 88 MB
% 8.99/2.30 % (2427413)Instructions burned: 136 (million)
% 8.99/2.30 % (2427415)Instruction limit reached!
% 8.99/2.30 % (2427415)------------------------------
% 8.99/2.30 % (2427415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.99/2.30 % (2427415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/2.30 % (2427415)CaDiCaL version: 2.1.3
% 8.99/2.30 % (2427415)Termination reason: Instruction limit
% 8.99/2.30 % (2427415)Termination phase: Saturation
% 8.99/2.30 % (2427415)Time elapsed: 0.214 s
% 8.99/2.30 % (2427415)Peak memory usage: 90 MB
% 8.99/2.30 % (2427415)Instructions burned: 257 (million)
% 8.99/2.30 % (2427451)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=392795670:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 8.99/2.30 % (2427452)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=428604106:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 8.99/2.30 % (2427457)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=3060453512:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 8.99/2.30 % (2427457)Instruction limit reached!
% 8.99/2.30 % (2427457)------------------------------
% 8.99/2.30 % (2427457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.99/2.30 % (2427457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/2.30 % (2427457)CaDiCaL version: 2.1.3
% 8.99/2.30 % (2427457)Termination reason: Instruction limit
% 8.99/2.30 % (2427457)Termination phase: Saturation
% 8.99/2.30 % (2427457)Time elapsed: 0.165 s
% 8.99/2.30 % (2427457)Peak memory usage: 91 MB
% 8.99/2.30 % (2427457)Instructions burned: 216 (million)
% 8.99/2.30 % (2427471)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=517625020:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2991 on theBenchmark for (2991ds/317Mi)
% 8.99/2.30 % (2427410)First to succeed.
% 8.99/2.30 % (2427410)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2427309"
% 8.99/2.30 % (2427416)Instruction limit reached!
% 8.99/2.30 % (2427416)------------------------------
% 8.99/2.30 % (2427416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.99/2.30 % (2427416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/2.30 % (2427416)CaDiCaL version: 2.1.3
% 8.99/2.30 % (2427416)Termination reason: Instruction limit
% 8.99/2.30 % (2427416)Termination phase: Saturation
% 8.99/2.30 % (2427416)Time elapsed: 1.004 s
% 8.99/2.30 % (2427416)Peak memory usage: 98 MB
% 8.99/2.30 % (2427416)Instructions burned: 1187 (million)
% 8.99/2.30 % (2427410)Refutation found. Thanks to Tanya!
% 8.99/2.30 % SZS status Unsatisfiable for theBenchmark
% 8.99/2.30 % SZS output start Proof for theBenchmark
% See solution above
% 10.51/2.42 % (2427410)------------------------------
% 10.51/2.42 % (2427410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.51/2.42 % (2427410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.51/2.42 % (2427410)CaDiCaL version: 2.1.3
% 10.51/2.42 % (2427410)Termination reason: Refutation
% 10.51/2.42 % (2427410)Time elapsed: 1.040 s
% 10.51/2.42 % (2427410)Peak memory usage: 141 MB
% 10.51/2.42 % (2427410)Instructions burned: 2000 (million)
% 10.51/2.42 % (2427410)------------------------------
% 10.51/2.42 % (2427410)------------------------------
% 10.51/2.42 % (2427309)Success in time 1.411 s
% 10.51/2.42 % Vampire exiting
%------------------------------------------------------------------------------