%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT015-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.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 29.91s 5.07s
% Output : Refutation 30.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 61
% Number of leaves : 24
% Syntax : Number of formulae : 230 ( 207 unt; 22 def)
% Number of atoms : 283 ( 227 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 99 ( 46 ~; 45 |; 0 &)
% ( 8 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 20 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 9 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 17 con; 0-2 aty)
% Number of variables : 364 ( 0 sgn 364 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1,X6,X4,X5] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X3,X1),meet(X1,X4)),X1)),meet(join(meet(X1,meet(meet(join(X3,join(X1,X4)),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X3,join(X1,X4)),join(X5,X1)),X1)))),join(X0,join(join(meet(X3,X1),meet(X1,X4)),X1)))),join(join(meet(X0,X1),meet(X1,join(X0,X1))),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
( meet(a,a) != a
| meet(a,b) != meet(b,a)
| meet(meet(a,b),c) != meet(a,meet(b,c))
| join(a,a) != a
| join(a,b) != join(b,a)
| join(join(a,b),c) != join(a,join(b,c))
| meet(a,join(a,b)) != a
| join(a,meet(a,b)) != a ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_normal_axioms) ).
fof(f3,plain,
( a != meet(a,a)
| meet(a,b) != meet(b,a)
| meet(meet(a,b),c) != meet(a,meet(b,c))
| a != join(a,a)
| join(a,b) != join(b,a)
| join(join(a,b),c) != join(a,join(b,c))
| a != meet(a,join(a,b))
| a != join(a,meet(a,b)) ),
inference(reorient_equations,[],[f2]) ).
fof(f4,definition,
sF0 = meet(a,a),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f5,plain,
meet(a,a) = sF0,
inference(reorient_equations,[],[f4]) ).
fof(f6,definition,
sF1 = meet(a,b),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f7,plain,
meet(a,b) = sF1,
inference(reorient_equations,[],[f6]) ).
fof(f8,definition,
sF2 = meet(b,a),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f9,plain,
meet(b,a) = sF2,
inference(reorient_equations,[],[f8]) ).
fof(f10,definition,
sF3 = meet(sF1,c),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f11,plain,
meet(sF1,c) = sF3,
inference(reorient_equations,[],[f10]) ).
fof(f12,definition,
sF4 = meet(b,c),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f13,plain,
meet(b,c) = sF4,
inference(reorient_equations,[],[f12]) ).
fof(f14,definition,
sF5 = meet(a,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f15,plain,
meet(a,sF4) = sF5,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF6 = join(a,a),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f17,plain,
join(a,a) = sF6,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF7 = join(a,b),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f19,plain,
join(a,b) = sF7,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF8 = join(b,a),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f21,plain,
join(b,a) = sF8,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF9 = join(sF7,c),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f23,plain,
join(sF7,c) = sF9,
inference(reorient_equations,[],[f22]) ).
fof(f24,definition,
sF10 = join(b,c),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f25,plain,
join(b,c) = sF10,
inference(reorient_equations,[],[f24]) ).
fof(f26,definition,
sF11 = join(a,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f27,plain,
join(a,sF10) = sF11,
inference(reorient_equations,[],[f26]) ).
fof(f28,definition,
sF12 = meet(a,sF7),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f29,plain,
meet(a,sF7) = sF12,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF13 = join(a,sF1),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f31,plain,
join(a,sF1) = sF13,
inference(reorient_equations,[],[f30]) ).
fof(f32,plain,
( a != sF0
| sF1 != sF2
| sF3 != sF5
| a != sF6
| sF7 != sF8
| sF9 != sF11
| a != sF12
| a != sF13 ),
inference(definition_folding,[],[f3,f31,f7,f29,f19,f27,f25,f23,f19,f21,f19,f17,f15,f13,f11,f7,f9,f7,f5]) ).
fof(f34,definition,
( spl14_1
<=> a = sF13 ),
introduced(definition,[new_symbols(definition,[spl14_1])],[avatar_definition]) ).
fof(f38,definition,
( spl14_2
<=> a = sF12 ),
introduced(definition,[new_symbols(definition,[spl14_2])],[avatar_definition]) ).
fof(f40,plain,
( a != sF12
| spl14_2 ),
inference(avatar_component_clause,[],[f38]) ).
fof(f42,definition,
( spl14_3
<=> sF9 = sF11 ),
introduced(definition,[new_symbols(definition,[spl14_3])],[avatar_definition]) ).
fof(f44,plain,
( sF9 != sF11
| spl14_3 ),
inference(avatar_component_clause,[],[f42]) ).
fof(f46,definition,
( spl14_4
<=> sF7 = sF8 ),
introduced(definition,[new_symbols(definition,[spl14_4])],[avatar_definition]) ).
fof(f48,plain,
( sF7 != sF8
| spl14_4 ),
inference(avatar_component_clause,[],[f46]) ).
fof(f50,definition,
( spl14_5
<=> a = sF6 ),
introduced(definition,[new_symbols(definition,[spl14_5])],[avatar_definition]) ).
fof(f54,definition,
( spl14_6
<=> sF3 = sF5 ),
introduced(definition,[new_symbols(definition,[spl14_6])],[avatar_definition]) ).
fof(f56,plain,
( sF3 != sF5
| spl14_6 ),
inference(avatar_component_clause,[],[f54]) ).
fof(f58,definition,
( spl14_7
<=> sF1 = sF2 ),
introduced(definition,[new_symbols(definition,[spl14_7])],[avatar_definition]) ).
fof(f62,definition,
( spl14_8
<=> a = sF0 ),
introduced(definition,[new_symbols(definition,[spl14_8])],[avatar_definition]) ).
fof(f65,plain,
( ~ spl14_1
| ~ spl14_2
| ~ spl14_3
| ~ spl14_4
| ~ spl14_5
| ~ spl14_6
| ~ spl14_7
| ~ spl14_8 ),
inference(avatar_split_clause,[],[f32,f62,f58,f54,f50,f46,f42,f38,f34]) ).
fof(f66,plain,
meet(meet(a,b),c) = sF3,
inference(forward_demodulation,[],[f11,f7]) ).
fof(f67,plain,
meet(a,meet(b,c)) = sF5,
inference(forward_demodulation,[],[f15,f13]) ).
fof(f68,plain,
join(join(a,b),c) = sF9,
inference(forward_demodulation,[],[f23,f19]) ).
fof(f69,plain,
join(a,join(b,c)) = sF11,
inference(forward_demodulation,[],[f27,f25]) ).
fof(f70,plain,
meet(a,join(a,b)) = sF12,
inference(forward_demodulation,[],[f29,f19]) ).
fof(f71,plain,
join(a,meet(a,b)) = sF13,
inference(forward_demodulation,[],[f31,f7]) ).
fof(f80,plain,
! [X2,X3,X0,X1,X4,X5] : join(meet(X2,X0),meet(X0,join(X2,X0))) = join(meet(join(meet(X1,join(meet(X2,X0),meet(X0,join(X2,X0)))),meet(join(meet(X2,X0),meet(X0,join(X2,X0))),join(X1,join(meet(X2,X0),meet(X0,join(X2,X0)))))),X3),meet(join(meet(X1,join(join(meet(X4,join(meet(X2,X0),meet(X0,join(X2,X0)))),meet(join(meet(X2,X0),meet(X0,join(X2,X0))),X5)),join(meet(X2,X0),meet(X0,join(X2,X0))))),meet(X0,join(X1,join(join(meet(X4,join(meet(X2,X0),meet(X0,join(X2,X0)))),meet(join(meet(X2,X0),meet(X0,join(X2,X0))),X5)),join(meet(X2,X0),meet(X0,join(X2,X0))))))),join(join(meet(X1,join(meet(X2,X0),meet(X0,join(X2,X0)))),meet(join(meet(X2,X0),meet(X0,join(X2,X0))),join(X1,join(meet(X2,X0),meet(X0,join(X2,X0)))))),X3))),
inference(superposition,[],[f1,f1]) ).
fof(f112,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] : join(meet(join(meet(X6,X0),meet(X0,join(X6,X0))),X7),meet(join(meet(X6,join(join(meet(X8,X0),meet(X0,X9)),X0)),meet(join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(join(meet(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)),meet(X5,join(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)))),join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))),join(X6,join(join(meet(X8,X0),meet(X0,X9)),X0)))),join(join(meet(X6,X0),meet(X0,join(X6,X0))),X7))) = X0,
inference(superposition,[],[f80,f1]) ).
fof(f160,plain,
! [X2,X0,X1] : join(meet(join(meet(join(meet(X1,X0),meet(X0,join(X1,X0))),X0),meet(X0,join(join(meet(X1,X0),meet(X0,join(X1,X0))),X0))),X2),meet(X0,join(join(meet(join(meet(X1,X0),meet(X0,join(X1,X0))),X0),meet(X0,join(join(meet(X1,X0),meet(X0,join(X1,X0))),X0))),X2))) = X0,
inference(superposition,[],[f112,f1]) ).
fof(f198,plain,
! [X2,X0] : join(meet(X0,X2),meet(X0,join(X0,X2))) = X0,
inference(superposition,[],[f160,f160]) ).
fof(f202,plain,
! [X2,X3,X0,X4,X5] : join(meet(join(meet(X2,X0),meet(X0,join(X2,X0))),X3),meet(join(meet(X2,join(join(meet(X4,X0),meet(X0,X5)),X0)),meet(X0,join(X2,join(join(meet(X4,X0),meet(X0,X5)),X0)))),join(join(meet(X2,X0),meet(X0,join(X2,X0))),X3))) = X0,
inference(superposition,[],[f80,f160]) ).
fof(f208,plain,
! [X2,X3,X0,X1,X6,X4,X5] : join(meet(join(meet(join(meet(join(meet(X5,join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))),join(X5,join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))))),join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))),join(join(meet(X5,join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))),join(X5,join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))))),join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))))),X0),meet(X0,join(join(meet(join(meet(X5,join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))),join(X5,join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))))),join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))),join(join(meet(X5,join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))),join(X5,join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))))),join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))))),X0))),X6),meet(join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))),join(join(meet(join(meet(join(meet(X5,join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))),join(X5,join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))))),join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))),join(join(meet(X5,join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))),join(X5,join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))))),join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))))),X0),meet(X0,join(join(meet(join(meet(X5,join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))),join(X5,join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))))),join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))),join(join(meet(X5,join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))),join(X5,join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))))),join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))))))),X0))),X6))) = X0,
inference(superposition,[],[f1,f160]) ).
fof(f211,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X1,join(X0,X1))) = join(meet(join(meet(X2,join(meet(X0,X1),meet(X1,join(X0,X1)))),meet(join(meet(X0,X1),meet(X1,join(X0,X1))),join(X2,join(meet(X0,X1),meet(X1,join(X0,X1)))))),X3),meet(join(meet(X2,join(join(meet(X0,X1),meet(X1,join(X0,X1))),join(meet(X0,X1),meet(X1,join(X0,X1))))),meet(X1,join(X2,join(join(meet(X0,X1),meet(X1,join(X0,X1))),join(meet(X0,X1),meet(X1,join(X0,X1))))))),join(join(meet(X2,join(meet(X0,X1),meet(X1,join(X0,X1)))),meet(join(meet(X0,X1),meet(X1,join(X0,X1))),join(X2,join(meet(X0,X1),meet(X1,join(X0,X1)))))),X3))),
inference(superposition,[],[f80,f160]) ).
fof(f221,plain,
a = join(sF0,meet(a,join(a,a))),
inference(superposition,[],[f198,f5]) ).
fof(f223,plain,
a = join(sF12,meet(a,join(a,join(a,b)))),
inference(superposition,[],[f198,f70]) ).
fof(f288,plain,
! [X2,X3,X0,X1,X6,X4,X5] : join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))) = join(meet(X0,X4),meet(join(meet(join(meet(X1,X0),meet(X0,join(X1,X0))),join(join(meet(X5,join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0))))),meet(join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))),X6)),join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))))),meet(join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))),join(join(meet(X1,X0),meet(X0,join(X1,X0))),join(join(meet(X5,join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0))))),meet(join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))),X6)),join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))))))),join(X0,X4))),
inference(superposition,[],[f202,f202]) ).
fof(f308,plain,
! [X2,X3,X0,X1,X4] : join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))) = join(meet(X0,X4),meet(X0,join(X0,X4))),
inference(forward_demodulation,[],[f288,f202]) ).
fof(f316,plain,
! [X2,X3,X0,X1] : join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))) = X0,
inference(forward_demodulation,[],[f308,f198]) ).
fof(f344,plain,
! [X2,X3,X0] : join(meet(join(meet(X2,X0),meet(X0,join(X2,X0))),X3),meet(X0,join(join(meet(X2,X0),meet(X0,join(X2,X0))),X3))) = X0,
inference(backward_demodulation,[],[f202,f316]) ).
fof(f426,plain,
! [X2,X3,X0,X1,X6,X4] : join(meet(join(meet(join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))),X0),meet(X0,join(join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))),X0))),X6),meet(join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))),join(join(meet(join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))),X0),meet(X0,join(join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))),X0))),X6))) = X0,
inference(backward_demodulation,[],[f208,f344]) ).
fof(f459,plain,
! [X0,X1] : join(meet(X1,join(X0,X0)),meet(X0,join(X1,join(X0,X0)))) = X0,
inference(superposition,[],[f316,f344]) ).
fof(f525,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,join(X0,X1))) = join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),join(join(meet(X0,X1),meet(X1,join(X0,X1))),join(meet(X0,X1),meet(X1,join(X0,X1))))),meet(X1,join(join(meet(X0,X1),meet(X1,join(X0,X1))),join(join(meet(X0,X1),meet(X1,join(X0,X1))),join(meet(X0,X1),meet(X1,join(X0,X1))))))),join(join(meet(X0,X1),meet(X1,join(X0,X1))),X2))),
inference(superposition,[],[f211,f198]) ).
fof(f548,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,join(X0,X1))) = join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(X1,join(join(meet(X0,X1),meet(X1,join(X0,X1))),X2))),
inference(forward_demodulation,[],[f525,f344]) ).
fof(f555,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,join(X0,X1))) = X1,
inference(forward_demodulation,[],[f548,f344]) ).
fof(f655,plain,
! [X2,X3,X0,X1,X6,X4] : join(meet(X0,X6),meet(join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))),join(X0,X6))) = X0,
inference(backward_demodulation,[],[f426,f555]) ).
fof(f800,plain,
! [X2,X3,X0,X1,X4] : join(meet(X1,X4),meet(meet(meet(join(X0,join(X1,X2)),join(X3,X1)),X1),join(X1,X4))) = X1,
inference(superposition,[],[f655,f555]) ).
fof(f814,plain,
! [X2,X3,X0,X1,X4] : join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))) = X0,
inference(superposition,[],[f459,f655]) ).
fof(f932,plain,
! [X2,X3,X0,X1] : meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0) = X0,
inference(superposition,[],[f459,f800]) ).
fof(f940,plain,
! [X0,X4] : join(meet(X0,X0),meet(X4,join(X0,X0))) = X0,
inference(backward_demodulation,[],[f814,f932]) ).
fof(f958,plain,
! [X2,X0,X1] : join(join(meet(X0,X1),meet(X1,X2)),X1) = X1,
inference(superposition,[],[f316,f940]) ).
fof(f959,plain,
! [X0] : join(X0,X0) = X0,
inference(superposition,[],[f459,f940]) ).
fof(f970,plain,
! [X0,X4] : join(meet(X0,X0),meet(X4,X0)) = X0,
inference(backward_demodulation,[],[f940,f959]) ).
fof(f973,plain,
a = sF6,
inference(backward_demodulation,[],[f17,f959]) ).
fof(f974,plain,
a = join(sF0,meet(a,a)),
inference(backward_demodulation,[],[f221,f959]) ).
fof(f997,plain,
a = join(sF0,sF0),
inference(forward_demodulation,[],[f974,f5]) ).
fof(f998,plain,
spl14_5,
inference(avatar_split_clause,[],[f973,f50]) ).
fof(f1006,plain,
a = sF0,
inference(forward_demodulation,[],[f997,f959]) ).
fof(f1007,plain,
spl14_8,
inference(avatar_split_clause,[],[f1006,f62]) ).
fof(f1022,plain,
! [X0] : meet(X0,X0) = X0,
inference(superposition,[],[f959,f970]) ).
fof(f1025,plain,
! [X0,X4] : join(X0,meet(X4,X0)) = X0,
inference(backward_demodulation,[],[f970,f1022]) ).
fof(f1065,plain,
! [X0,X1] : join(join(X0,meet(X0,X1)),X0) = X0,
inference(superposition,[],[f958,f1022]) ).
fof(f1077,plain,
! [X0,X1] : join(meet(X0,X1),X1) = X1,
inference(superposition,[],[f958,f1025]) ).
fof(f1079,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = join(meet(join(meet(X1,X0),meet(X0,X2)),X0),meet(join(meet(X1,X0),meet(X0,X2)),X0)),
inference(superposition,[],[f198,f958]) ).
fof(f1082,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = meet(join(meet(X1,X0),meet(X0,X2)),X0),
inference(forward_demodulation,[],[f1079,f959]) ).
fof(f1101,plain,
! [X0,X1] : meet(X1,X0) = join(meet(meet(X1,X0),X0),meet(meet(X1,X0),X0)),
inference(superposition,[],[f198,f1077]) ).
fof(f1104,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(forward_demodulation,[],[f1101,f959]) ).
fof(f1122,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = join(meet(join(X0,meet(X0,X1)),X0),meet(join(X0,meet(X0,X1)),X0)),
inference(superposition,[],[f198,f1065]) ).
fof(f1125,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = meet(join(X0,meet(X0,X1)),X0),
inference(forward_demodulation,[],[f1122,f959]) ).
fof(f1148,plain,
join(meet(a,b),sF3) = meet(join(meet(a,b),sF3),meet(a,b)),
inference(superposition,[],[f1125,f66]) ).
fof(f1175,plain,
! [X2,X3,X0,X1] : meet(X0,X2) = meet(meet(join(X1,X0),join(X3,meet(X0,X2))),meet(X0,X2)),
inference(superposition,[],[f932,f198]) ).
fof(f1187,plain,
! [X3,X0,X1] : meet(meet(join(X0,X1),join(X3,X0)),X0) = X0,
inference(superposition,[],[f932,f1065]) ).
fof(f1197,plain,
! [X2,X0,X1] : meet(meet(join(X1,join(X0,X2)),X0),X0) = X0,
inference(superposition,[],[f932,f1065]) ).
fof(f1213,plain,
! [X2,X0,X1] : meet(join(X1,join(X0,X2)),X0) = X0,
inference(forward_demodulation,[],[f1197,f1104]) ).
fof(f1314,plain,
! [X0,X1] : meet(join(X1,X0),X0) = X0,
inference(superposition,[],[f1213,f1025]) ).
fof(f1315,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(join(X1,X0),meet(X0,X2)),
inference(superposition,[],[f1213,f198]) ).
fof(f1317,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(join(X1,X0),meet(X2,X0)),
inference(superposition,[],[f1213,f1077]) ).
fof(f1327,plain,
! [X0,X1] : meet(join(X0,X1),X0) = X0,
inference(superposition,[],[f1213,f1065]) ).
fof(f1338,plain,
! [X2,X0,X1] : join(join(X1,join(X0,X2)),X0) = meet(join(join(X1,join(X0,X2)),X0),join(X1,join(X0,X2))),
inference(superposition,[],[f1125,f1213]) ).
fof(f1339,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
inference(backward_demodulation,[],[f1125,f1327]) ).
fof(f1341,plain,
meet(a,b) = join(meet(a,b),sF3),
inference(backward_demodulation,[],[f1148,f1327]) ).
fof(f1342,plain,
! [X2,X0,X1] : join(X1,join(X0,X2)) = join(join(X1,join(X0,X2)),X0),
inference(backward_demodulation,[],[f1338,f1327]) ).
fof(f1363,plain,
a = sF13,
inference(backward_demodulation,[],[f71,f1339]) ).
fof(f1368,plain,
spl14_1,
inference(avatar_split_clause,[],[f1363,f34]) ).
fof(f1378,plain,
! [X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X0)) = X0,
inference(superposition,[],[f198,f1339]) ).
fof(f1383,plain,
! [X0,X1] : join(meet(X0,meet(X0,X1)),X0) = X0,
inference(forward_demodulation,[],[f1378,f1022]) ).
fof(f1386,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(superposition,[],[f1314,f1339]) ).
fof(f1395,plain,
! [X0,X1] : join(X1,X0) = join(X0,meet(join(X1,X0),join(join(X1,X0),X0))),
inference(superposition,[],[f198,f1314]) ).
fof(f1403,plain,
! [X0,X1] : join(X1,X0) = join(join(X1,X0),X0),
inference(superposition,[],[f1339,f1314]) ).
fof(f1405,plain,
! [X0,X1] : join(X1,X0) = join(X0,meet(join(X1,X0),join(X1,X0))),
inference(forward_demodulation,[],[f1395,f1403]) ).
fof(f1406,plain,
! [X0,X1] : join(meet(X0,X1),X0) = X0,
inference(backward_demodulation,[],[f1383,f1386]) ).
fof(f1410,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f1405,f1022]) ).
fof(f1421,plain,
! [X0,X1] : meet(X0,X1) = join(meet(meet(X0,X1),X0),meet(meet(X0,X1),X0)),
inference(superposition,[],[f198,f1406]) ).
fof(f1431,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(forward_demodulation,[],[f1421,f959]) ).
fof(f1453,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f1339,f1327]) ).
fof(f1454,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(superposition,[],[f1406,f1327]) ).
fof(f1455,plain,
a = join(sF12,meet(a,join(a,b))),
inference(backward_demodulation,[],[f223,f1454]) ).
fof(f1460,plain,
a = join(sF12,sF12),
inference(forward_demodulation,[],[f1455,f70]) ).
fof(f1462,plain,
a = sF12,
inference(forward_demodulation,[],[f1460,f959]) ).
fof(f1463,plain,
( $false
| spl14_2 ),
inference(forward_subsumption_resolution,[],[f1462,f40]) ).
fof(f1464,plain,
spl14_2,
inference(avatar_contradiction_clause,[],[f1463]) ).
fof(f1488,plain,
! [X0,X1] : join(meet(X1,join(X0,X1)),meet(X1,join(X0,X1))) = X1,
inference(superposition,[],[f198,f1410]) ).
fof(f1497,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(forward_demodulation,[],[f1488,f959]) ).
fof(f1541,plain,
! [X2,X0,X1] : meet(join(join(X0,X1),X2),X0) = X0,
inference(superposition,[],[f1213,f1453]) ).
fof(f1577,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
inference(superposition,[],[f1497,f1453]) ).
fof(f1581,plain,
! [X2,X0,X1] : join(X1,X0) = join(join(X0,meet(join(X1,X0),X2)),join(X1,X0)),
inference(superposition,[],[f958,f1497]) ).
fof(f1691,plain,
! [X2,X0,X1] : join(join(meet(X0,X1),meet(X0,X2)),X0) = X0,
inference(superposition,[],[f958,f1431]) ).
fof(f1840,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(meet(X0,X1),X2)),
inference(superposition,[],[f1315,f1339]) ).
fof(f2021,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(meet(X0,X1),join(X2,X1)),
inference(superposition,[],[f1431,f1317]) ).
fof(f3366,plain,
! [X2,X0,X1] : meet(X1,meet(X2,X0)) = meet(meet(X1,meet(X2,X0)),X0),
inference(superposition,[],[f2021,f1025]) ).
fof(f3492,plain,
! [X2,X0,X1] : join(X2,meet(X0,meet(X1,X2))) = X2,
inference(superposition,[],[f1025,f3366]) ).
fof(f4457,plain,
! [X2,X0,X1] : join(X0,X1) = join(join(X0,X1),meet(X2,X0)),
inference(superposition,[],[f3492,f1577]) ).
fof(f6449,plain,
! [X0,X1] : join(X0,X1) = join(join(X1,X0),join(X0,X1)),
inference(superposition,[],[f1581,f1327]) ).
fof(f6466,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(join(X2,X0),join(join(X0,X1),X2)),
inference(superposition,[],[f1581,f1541]) ).
fof(f6809,plain,
! [X0,X1] : join(X1,X0) = meet(join(X0,X1),join(X1,X0)),
inference(superposition,[],[f1327,f6449]) ).
fof(f6810,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(join(X2,join(X0,X1)),join(X1,X0)),
inference(superposition,[],[f1342,f6449]) ).
fof(f6818,plain,
! [X2,X0,X1] : join(X1,X0) = meet(join(join(X0,X1),X2),join(X1,X0)),
inference(superposition,[],[f1541,f6449]) ).
fof(f7045,plain,
! [X0,X1] : join(X1,X0) = join(join(X0,join(X0,X1)),join(X1,X0)),
inference(superposition,[],[f1581,f6809]) ).
fof(f7063,plain,
! [X2,X0,X1] : join(X1,X0) = join(join(meet(join(X1,X0),X2),join(X0,X1)),join(X1,X0)),
inference(superposition,[],[f1691,f6809]) ).
fof(f7074,plain,
! [X2,X0,X1] : join(X1,X0) = join(meet(join(X1,X0),X2),join(X0,X1)),
inference(forward_demodulation,[],[f7063,f6810]) ).
fof(f7081,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f7045,f6810]) ).
fof(f7232,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(superposition,[],[f1454,f7081]) ).
fof(f7238,plain,
! [X2,X0,X1] : join(X1,X0) = meet(meet(join(join(X1,X0),X2),join(X0,X1)),join(X1,X0)),
inference(superposition,[],[f1187,f7081]) ).
fof(f7257,plain,
! [X2,X0,X1] : meet(X2,join(X1,X0)) = meet(meet(X2,join(X1,X0)),join(X0,X1)),
inference(superposition,[],[f2021,f7081]) ).
fof(f7273,plain,
! [X2,X0,X1] : join(X1,X0) = meet(join(join(X1,X0),X2),join(X0,X1)),
inference(forward_demodulation,[],[f7238,f7257]) ).
fof(f7603,plain,
sF11 = join(a,join(c,b)),
inference(superposition,[],[f69,f7232]) ).
fof(f8185,plain,
! [X3,X0,X1] : join(join(X0,X1),meet(join(X1,X0),X3)) = meet(join(join(X0,X1),meet(join(X1,X0),X3)),join(X1,X0)),
inference(superposition,[],[f1082,f7273]) ).
fof(f8212,plain,
! [X3,X0,X1] : join(X1,X0) = join(join(X0,X1),meet(join(X1,X0),X3)),
inference(forward_demodulation,[],[f8185,f6818]) ).
fof(f8553,plain,
! [X2,X0,X1] : join(X1,join(X0,X2)) = join(join(join(X0,X2),X1),X0),
inference(superposition,[],[f8212,f1213]) ).
fof(f8646,plain,
! [X2,X0,X1] : join(X1,join(X0,X2)) = join(X0,join(join(X0,X2),X1)),
inference(forward_demodulation,[],[f8553,f7232]) ).
fof(f8830,plain,
! [X2,X0,X1] : join(X1,X0) = join(meet(X2,X0),join(X0,X1)),
inference(superposition,[],[f8646,f1077]) ).
fof(f9226,plain,
! [X2,X0,X1] : join(meet(X2,X1),join(X0,X1)) = join(join(X1,X0),meet(X2,X1)),
inference(superposition,[],[f7081,f8830]) ).
fof(f9240,plain,
! [X2,X0,X1] : join(X1,X0) = join(meet(X2,X1),join(X0,X1)),
inference(forward_demodulation,[],[f9226,f4457]) ).
fof(f9688,plain,
! [X2,X0,X1] : join(X0,X1) = join(join(X1,X0),meet(X2,X0)),
inference(superposition,[],[f7232,f9240]) ).
fof(f24209,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(join(X2,X1),join(join(X0,X1),X2)),
inference(superposition,[],[f6466,f7081]) ).
fof(f24346,plain,
! [X2,X0,X1] : join(X0,X1) = join(join(meet(X2,X0),X1),join(X0,X1)),
inference(superposition,[],[f6466,f9688]) ).
fof(f24368,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),join(X0,join(X1,X2))),
inference(superposition,[],[f6466,f7232]) ).
fof(f24531,plain,
! [X2,X0,X1] : join(X0,X1) = join(join(X0,X1),join(meet(X2,X0),X1)),
inference(forward_demodulation,[],[f24346,f7232]) ).
fof(f24913,plain,
! [X2,X0,X1] : join(X0,X1) = join(join(join(meet(X2,X0),X1),X0),join(X0,X1)),
inference(superposition,[],[f6466,f24531]) ).
fof(f25023,plain,
! [X2,X0,X1] : join(X0,X1) = join(join(X0,X1),join(join(meet(X2,X0),X1),X0)),
inference(forward_demodulation,[],[f24913,f7232]) ).
fof(f25168,plain,
! [X2,X0,X1] : join(X0,X1) = join(join(meet(X2,X0),X1),X0),
inference(forward_demodulation,[],[f25023,f24209]) ).
fof(f25197,plain,
! [X2,X0,X1] : join(X0,X1) = join(X0,join(meet(X2,X0),X1)),
inference(forward_demodulation,[],[f25168,f7232]) ).
fof(f25229,plain,
! [X2,X0,X1] : join(join(X1,X0),X2) = join(join(X1,X0),join(X0,X2)),
inference(superposition,[],[f25197,f1497]) ).
fof(f25231,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(join(X0,X1),join(X0,X2)),
inference(superposition,[],[f25197,f1577]) ).
fof(f25332,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X2,join(X1,X0)),
inference(superposition,[],[f25197,f7074]) ).
fof(f25629,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),join(X1,X2)),
inference(backward_demodulation,[],[f24368,f25231]) ).
fof(f25703,plain,
! [X2,X0,X1] : join(X1,join(X0,X2)) = join(join(X1,X0),X2),
inference(backward_demodulation,[],[f25229,f25629]) ).
fof(f26363,plain,
join(a,join(b,c)) = sF9,
inference(backward_demodulation,[],[f68,f25703]) ).
fof(f26654,plain,
sF9 = join(a,join(c,b)),
inference(forward_demodulation,[],[f26363,f25332]) ).
fof(f27044,plain,
sF9 = sF11,
inference(backward_demodulation,[],[f7603,f26654]) ).
fof(f27161,plain,
( $false
| spl14_3 ),
inference(forward_subsumption_resolution,[],[f27044,f44]) ).
fof(f27162,plain,
spl14_3,
inference(avatar_contradiction_clause,[],[f27161]) ).
fof(f27675,plain,
( join(b,a) != sF7
| spl14_4 ),
inference(forward_demodulation,[],[f48,f21]) ).
fof(f27711,plain,
( join(a,b) != join(b,a)
| spl14_4 ),
inference(forward_demodulation,[],[f27675,f19]) ).
fof(f27716,plain,
( $false
| spl14_4 ),
inference(forward_subsumption_resolution,[],[f27711,f7232]) ).
fof(f27717,plain,
spl14_4,
inference(avatar_contradiction_clause,[],[f27716]) ).
fof(f46576,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(meet(join(X2,X1),X0),meet(X1,X0)),
inference(superposition,[],[f1175,f1025]) ).
fof(f46779,plain,
! [X2,X0,X1] : meet(meet(X1,X0),X2) = meet(meet(X0,X2),meet(meet(X1,X0),X2)),
inference(superposition,[],[f46576,f1025]) ).
fof(f47375,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f46779,f1431]) ).
fof(f47388,plain,
sF3 = meet(meet(b,c),sF3),
inference(superposition,[],[f46779,f66]) ).
fof(f47609,plain,
meet(a,b) = meet(sF2,meet(a,b)),
inference(superposition,[],[f47375,f9]) ).
fof(f47717,plain,
sF2 = meet(meet(a,b),sF2),
inference(superposition,[],[f47375,f9]) ).
fof(f47776,plain,
! [X0,X1] : meet(X1,X0) = join(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f1339,f47375]) ).
fof(f47944,plain,
sF2 = meet(sF2,meet(a,b)),
inference(superposition,[],[f1431,f47717]) ).
fof(f47986,plain,
meet(a,b) = sF2,
inference(backward_demodulation,[],[f47609,f47944]) ).
fof(f47991,plain,
sF1 = sF2,
inference(backward_demodulation,[],[f7,f47986]) ).
fof(f47992,plain,
sF3 = meet(sF2,c),
inference(backward_demodulation,[],[f66,f47986]) ).
fof(f47993,plain,
sF2 = join(sF2,sF3),
inference(backward_demodulation,[],[f1341,f47986]) ).
fof(f48046,plain,
spl14_7,
inference(avatar_split_clause,[],[f47991,f58]) ).
fof(f49060,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(meet(join(X2,X1),meet(X0,X1)),meet(X1,X0)),
inference(superposition,[],[f1175,f47776]) ).
fof(f49086,plain,
! [X2,X0,X1] : meet(X2,meet(X1,X0)) = meet(meet(X2,meet(X1,X0)),meet(X0,X1)),
inference(superposition,[],[f2021,f47776]) ).
fof(f49161,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(join(X2,X1),meet(X0,X1)),
inference(forward_demodulation,[],[f49060,f49086]) ).
fof(f49367,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(join(X0,X1),meet(X2,X0)),
inference(superposition,[],[f49161,f7232]) ).
fof(f49605,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(superposition,[],[f1327,f49161]) ).
fof(f50610,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(meet(join(X2,X1),X0),meet(X0,X1)),
inference(superposition,[],[f46576,f49605]) ).
fof(f50639,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X2,X0),meet(X0,meet(X1,X2))),
inference(superposition,[],[f46779,f49605]) ).
fof(f50704,plain,
sF3 = meet(meet(c,b),sF3),
inference(superposition,[],[f47388,f49605]) ).
fof(f50707,plain,
sF5 = meet(a,meet(c,b)),
inference(superposition,[],[f67,f49605]) ).
fof(f50746,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(meet(X0,X1),meet(join(X2,X1),X0)),
inference(forward_demodulation,[],[f50610,f49605]) ).
fof(f54260,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(meet(X1,meet(join(X2,X1),X0)),meet(X0,X1)),
inference(superposition,[],[f46779,f50746]) ).
fof(f54345,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(meet(X0,X1),meet(X1,meet(join(X2,X1),X0))),
inference(forward_demodulation,[],[f54260,f49605]) ).
fof(f54470,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X1,meet(join(X2,X1),X0)),
inference(forward_demodulation,[],[f54345,f50639]) ).
fof(f54533,plain,
! [X2,X0,X1] : meet(X1,meet(X2,X0)) = meet(meet(X2,X0),meet(X0,X1)),
inference(superposition,[],[f54470,f1025]) ).
fof(f54621,plain,
! [X0] : meet(X0,sF3) = meet(sF3,meet(sF2,X0)),
inference(superposition,[],[f54470,f47993]) ).
fof(f54652,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(meet(X1,X0),X2),
inference(superposition,[],[f54470,f49367]) ).
fof(f55441,plain,
! [X0] : meet(meet(X0,b),sF2) = meet(a,meet(X0,b)),
inference(superposition,[],[f54533,f9]) ).
fof(f55457,plain,
! [X0] : meet(meet(X0,sF2),sF3) = meet(c,meet(X0,sF2)),
inference(superposition,[],[f54533,f47992]) ).
fof(f55645,plain,
! [X0] : meet(sF3,meet(sF2,X0)) = meet(c,meet(X0,sF2)),
inference(forward_demodulation,[],[f55457,f54652]) ).
fof(f55788,plain,
! [X0] : meet(X0,sF3) = meet(c,meet(X0,sF2)),
inference(forward_demodulation,[],[f55645,f54621]) ).
fof(f56703,plain,
! [X0] : meet(meet(c,X0),sF2) = meet(meet(c,X0),sF3),
inference(superposition,[],[f1840,f55788]) ).
fof(f56786,plain,
sF3 = meet(meet(c,b),sF2),
inference(backward_demodulation,[],[f50704,f56703]) ).
fof(f56825,plain,
sF3 = meet(a,meet(c,b)),
inference(forward_demodulation,[],[f56786,f55441]) ).
fof(f56833,plain,
sF3 = sF5,
inference(backward_demodulation,[],[f50707,f56825]) ).
fof(f56834,plain,
( $false
| spl14_6 ),
inference(forward_subsumption_resolution,[],[f56833,f56]) ).
fof(f56835,plain,
spl14_6,
inference(avatar_contradiction_clause,[],[f56834]) ).
cnf(s1,plain,
( ~ spl14_1
| ~ spl14_2
| ~ spl14_3
| ~ spl14_4
| ~ spl14_5
| ~ spl14_6
| ~ spl14_7
| ~ spl14_8 ),
inference(sat_conversion,[],[f65]) ).
cnf(s2,plain,
spl14_5,
inference(sat_conversion,[],[f998]) ).
cnf(s3,plain,
spl14_8,
inference(sat_conversion,[],[f1007]) ).
cnf(s5,plain,
spl14_1,
inference(sat_conversion,[],[f1368]) ).
cnf(s6,plain,
spl14_2,
inference(sat_conversion,[],[f1464]) ).
cnf(s7,plain,
spl14_3,
inference(sat_conversion,[],[f27162]) ).
cnf(s8,plain,
spl14_4,
inference(sat_conversion,[],[f27717]) ).
cnf(s9,plain,
spl14_7,
inference(sat_conversion,[],[f48046]) ).
cnf(s10,plain,
spl14_6,
inference(sat_conversion,[],[f56835]) ).
cnf(s11,plain,
$false,
inference(rat,[],[s1,s3,s9,s10,s2,s8,s7,s6,s5]) ).
fof(f56836,plain,
$false,
inference(avatar_sat_refutation,[],[s11]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT015-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n006.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 13:56:11 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.37/2.31 % (2988171)Input is clausal, will run a generic CNF schedule.
% 10.37/2.31 % (2988179)lrs+10_1_sil=8000:sp=occurrence:random_seed=1687707433:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.37/2.31 % (2988179)Instruction limit reached!
% 10.37/2.31 % (2988179)------------------------------
% 10.37/2.31 % (2988179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.37/2.31 % (2988179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.37/2.31 % (2988179)CaDiCaL version: 2.1.3
% 10.37/2.31 % (2988179)Termination reason: Instruction limit
% 10.37/2.31 % (2988179)Termination phase: Saturation
% 10.37/2.31 % (2988179)Time elapsed: 0.027 s
% 10.37/2.31 % (2988179)Peak memory usage: 91 MB
% 10.37/2.31 % (2988179)Instructions burned: 109 (million)
% 10.37/2.31 % (2988181)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3803790908:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.37/2.31 % (2988182)dis-21_1_sil=8000:lcm=predicate:random_seed=1394650710: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.37/2.31 % (2988180)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1873888965:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.37/2.31 % (2988177)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3228891017:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.37/2.31 % (2988176)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=636246382:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.37/2.31 % (2988178)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=36524156:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.37/2.31 % (2988182)Refutation not found, incomplete strategy
% 10.37/2.31 % (2988182)------------------------------
% 10.37/2.31 % (2988182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.37/2.31 % (2988182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.37/2.31 % (2988182)CaDiCaL version: 2.1.3
% 10.37/2.31 % (2988182)Termination reason: Refutation not found, incomplete strategy
% 10.37/2.31 % (2988182)Time elapsed: 0.001 s
% 10.37/2.31 % (2988182)Peak memory usage: 88 MB
% 10.37/2.31 % (2988181)Instruction limit reached!
% 10.37/2.31 % (2988181)------------------------------
% 10.37/2.31 % (2988181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.37/2.31 % (2988181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.37/2.31 % (2988181)CaDiCaL version: 2.1.3
% 10.37/2.31 % (2988181)Termination reason: Instruction limit
% 10.37/2.31 % (2988181)Termination phase: Saturation
% 10.37/2.31 % (2988181)Time elapsed: 0.044 s
% 10.37/2.31 % (2988181)Peak memory usage: 91 MB
% 10.37/2.31 % (2988181)Instructions burned: 185 (million)
% 10.37/2.31 % (2988180)Instruction limit reached!
% 10.37/2.31 % (2988180)------------------------------
% 10.37/2.31 % (2988180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.37/2.31 % (2988180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.37/2.31 % (2988180)CaDiCaL version: 2.1.3
% 10.37/2.31 % (2988180)Termination reason: Instruction limit
% 10.37/2.31 % (2988180)Termination phase: Saturation
% 10.37/2.31 % (2988180)Time elapsed: 0.056 s
% 10.37/2.31 % (2988180)Peak memory usage: 91 MB
% 10.37/2.31 % (2988180)Instructions burned: 115 (million)
% 10.37/2.31 % (2988184)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=3897698994:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 10.37/2.31 % (2988184)Refutation not found, incomplete strategy
% 10.37/2.31 % (2988184)------------------------------
% 10.37/2.31 % (2988184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.37/2.31 % (2988184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.37/2.31 % (2988184)CaDiCaL version: 2.1.3
% 10.37/2.31 % (2988184)Termination reason: Refutation not found, incomplete strategy
% 10.37/2.31 % (2988184)Time elapsed: 0.002 s
% 10.37/2.31 % (2988184)Peak memory usage: 88 MB
% 10.37/2.31 % (2988191)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3018286357: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)
% 19.22/3.68 % (2988191)Refutation not found, incomplete strategy
% 19.22/3.68 % (2988191)------------------------------
% 19.22/3.68 % (2988191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.68 % (2988191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.68 % (2988191)CaDiCaL version: 2.1.3
% 19.22/3.68 % (2988191)Termination reason: Refutation not found, incomplete strategy
% 19.22/3.68 % (2988191)Time elapsed: 0.001 s
% 19.22/3.68 % (2988191)Peak memory usage: 88 MB
% 19.22/3.68 % (2988191)Instructions burned: 1 (million)
% 19.22/3.68 % (2988192)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3983811493:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 19.22/3.68 % (2988192)Refutation not found, incomplete strategy
% 19.22/3.68 % (2988192)------------------------------
% 19.22/3.68 % (2988192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.68 % (2988192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.68 % (2988192)CaDiCaL version: 2.1.3
% 19.22/3.68 % (2988192)Termination reason: Refutation not found, incomplete strategy
% 19.22/3.68 % (2988192)Time elapsed: 0.001 s
% 19.22/3.68 % (2988192)Peak memory usage: 88 MB
% 19.22/3.68 % (2988182)------------------------------
% 19.22/3.68 % (2988182)------------------------------
% 19.22/3.68 % (2988191)------------------------------
% 19.22/3.68 % (2988191)------------------------------
% 19.22/3.68 % (2988184)------------------------------
% 19.22/3.68 % (2988184)------------------------------
% 19.22/3.68 % (2988196)lrs+10_64_to=lpo:sil=8000:random_seed=4157563247:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 19.22/3.68 % (2988192)------------------------------
% 19.22/3.68 % (2988192)------------------------------
% 19.22/3.68 % (2988197)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3144782242:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 19.22/3.68 % (2988196)Instruction limit reached!
% 19.22/3.68 % (2988196)------------------------------
% 19.22/3.68 % (2988196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.68 % (2988196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.68 % (2988196)CaDiCaL version: 2.1.3
% 19.22/3.68 % (2988196)Termination reason: Instruction limit
% 19.22/3.68 % (2988196)Termination phase: Saturation
% 19.22/3.68 % (2988196)Time elapsed: 0.059 s
% 19.22/3.68 % (2988196)Peak memory usage: 90 MB
% 19.22/3.68 % (2988196)Instructions burned: 126 (million)
% 19.22/3.68 % (2988197)Instruction limit reached!
% 19.22/3.68 % (2988197)------------------------------
% 19.22/3.68 % (2988197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.68 % (2988197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.68 % (2988197)CaDiCaL version: 2.1.3
% 19.22/3.68 % (2988197)Termination reason: Instruction limit
% 19.22/3.68 % (2988197)Termination phase: Saturation
% 19.22/3.68 % (2988197)Time elapsed: 0.047 s
% 19.22/3.68 % (2988197)Peak memory usage: 92 MB
% 19.22/3.68 % (2988197)Instructions burned: 197 (million)
% 19.22/3.68 % (2988199)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3892232792:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 19.22/3.68 % (2988202)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=458378150:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 19.22/3.68 % (2988201)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=487534862:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 19.22/3.68 % (2988203)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2052405473:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 19.22/3.68 % (2988203)Refutation not found, incomplete strategy
% 19.22/3.68 % (2988203)------------------------------
% 19.22/3.68 % (2988203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.68 % (2988203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.68 % (2988203)CaDiCaL version: 2.1.3
% 19.22/3.68 % (2988203)Termination reason: Refutation not found, incomplete strategy
% 19.22/3.68 % (2988203)Time elapsed: 0.001 s
% 19.22/3.68 % (2988203)Peak memory usage: 87 MB
% 19.22/3.68 % (2988199)Instruction limit reached!
% 28.78/4.93 % (2988199)------------------------------
% 28.78/4.93 % (2988199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.78/4.93 % (2988199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.78/4.93 % (2988199)CaDiCaL version: 2.1.3
% 28.78/4.93 % (2988199)Termination reason: Instruction limit
% 28.78/4.93 % (2988199)Termination phase: Saturation
% 28.78/4.93 % (2988199)Time elapsed: 0.083 s
% 28.78/4.93 % (2988199)Peak memory usage: 92 MB
% 28.78/4.93 % (2988199)Instructions burned: 158 (million)
% 28.78/4.93 % (2988202)Instruction limit reached!
% 28.78/4.93 % (2988202)------------------------------
% 28.78/4.93 % (2988202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.78/4.93 % (2988202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.78/4.93 % (2988202)CaDiCaL version: 2.1.3
% 28.78/4.93 % (2988202)Termination reason: Instruction limit
% 28.78/4.93 % (2988202)Termination phase: Saturation
% 28.78/4.93 % (2988202)Time elapsed: 0.048 s
% 28.78/4.93 % (2988202)Peak memory usage: 92 MB
% 28.78/4.93 % (2988202)Instructions burned: 106 (million)
% 28.78/4.94 % (2988203)------------------------------
% 28.78/4.94 % (2988203)------------------------------
% 28.78/4.94 % (2988208)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=978700484:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 28.78/4.94 % (2988209)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1860070032:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 28.78/4.94 % (2988210)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3919655047:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 28.78/4.94 % (2988210)Instruction limit reached!
% 28.78/4.94 % (2988210)------------------------------
% 28.78/4.94 % (2988210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.78/4.94 % (2988210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.78/4.94 % (2988210)CaDiCaL version: 2.1.3
% 28.78/4.94 % (2988210)Termination reason: Instruction limit
% 28.78/4.94 % (2988210)Termination phase: Saturation
% 28.78/4.94 % (2988210)Time elapsed: 0.036 s
% 28.78/4.94 % (2988210)Peak memory usage: 91 MB
% 28.78/4.94 % (2988210)Instructions burned: 138 (million)
% 28.78/4.94 % (2988208)Instruction limit reached!
% 28.78/4.94 % (2988208)------------------------------
% 28.78/4.94 % (2988208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.78/4.94 % (2988208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.78/4.94 % (2988208)CaDiCaL version: 2.1.3
% 28.78/4.94 % (2988208)Termination reason: Instruction limit
% 28.78/4.94 % (2988208)Termination phase: Saturation
% 28.78/4.94 % (2988208)Time elapsed: 0.125 s
% 28.78/4.94 % (2988208)Peak memory usage: 95 MB
% 28.78/4.94 % (2988208)Instructions burned: 243 (million)
% 28.78/4.94 % (2988214)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3450396839:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 28.78/4.94 % (2988215)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=556511025:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 28.78/4.94 % (2988214)Instruction limit reached!
% 28.78/4.94 % (2988214)------------------------------
% 28.78/4.94 % (2988214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.78/4.94 % (2988214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.78/4.94 % (2988214)CaDiCaL version: 2.1.3
% 28.78/4.94 % (2988214)Termination reason: Instruction limit
% 28.78/4.94 % (2988214)Termination phase: Saturation
% 28.78/4.94 % (2988214)Time elapsed: 0.109 s
% 28.78/4.94 % (2988214)Peak memory usage: 96 MB
% 28.78/4.94 % (2988214)Instructions burned: 502 (million)
% 28.78/4.94 % (2988215)Instruction limit reached!
% 28.78/4.94 % (2988215)------------------------------
% 28.78/4.94 % (2988215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.78/4.94 % (2988215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.78/4.94 % (2988215)CaDiCaL version: 2.1.3
% 28.78/4.94 % (2988215)Termination reason: Instruction limit
% 28.78/4.94 % (2988215)Termination phase: Saturation
% 28.78/4.94 % (2988215)Time elapsed: 0.085 s
% 28.78/4.94 % (2988215)Peak memory usage: 92 MB
% 28.78/4.94 % (2988215)Instructions burned: 191 (million)
% 28.78/4.94 % (2988218)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2564068757:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 29.91/5.07 % (2988218)Instruction limit reached!
% 29.91/5.07 % (2988218)------------------------------
% 29.91/5.07 % (2988218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.91/5.07 % (2988218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.91/5.07 % (2988218)CaDiCaL version: 2.1.3
% 29.91/5.07 % (2988218)Termination reason: Instruction limit
% 29.91/5.07 % (2988218)Termination phase: Saturation
% 29.91/5.07 % (2988218)Time elapsed: 0.074 s
% 29.91/5.07 % (2988218)Peak memory usage: 94 MB
% 29.91/5.07 % (2988218)Instructions burned: 266 (million)
% 29.91/5.07 % (2988219)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1551473950:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 29.91/5.07 % (2988219)Instruction limit reached!
% 29.91/5.07 % (2988219)------------------------------
% 29.91/5.07 % (2988219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.91/5.07 % (2988219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.91/5.07 % (2988219)CaDiCaL version: 2.1.3
% 29.91/5.07 % (2988219)Termination reason: Instruction limit
% 29.91/5.07 % (2988219)Termination phase: Saturation
% 29.91/5.07 % (2988219)Time elapsed: 0.079 s
% 29.91/5.07 % (2988219)Peak memory usage: 92 MB
% 29.91/5.07 % (2988219)Instructions burned: 158 (million)
% 29.91/5.07 % (2988221)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1897099826:i=3256:kws=precedence:bd=preordered:av=off_2984 on theBenchmark for (2984ds/3256Mi)
% 29.91/5.07 % (2988223)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3052442314:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi)
% 29.91/5.07 % (2988223)Instruction limit reached!
% 29.91/5.07 % (2988223)------------------------------
% 29.91/5.07 % (2988223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.91/5.07 % (2988223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.91/5.07 % (2988223)CaDiCaL version: 2.1.3
% 29.91/5.07 % (2988223)Termination reason: Instruction limit
% 29.91/5.07 % (2988223)Termination phase: Saturation
% 29.91/5.07 % (2988223)Time elapsed: 0.275 s
% 29.91/5.07 % (2988223)Peak memory usage: 91 MB
% 29.91/5.07 % (2988223)Instructions burned: 538 (million)
% 29.91/5.07 % (2988226)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3224008927:i=180:bd=preordered:av=off_2979 on theBenchmark for (2979ds/180Mi)
% 29.91/5.07 % (2988226)Instruction limit reached!
% 29.91/5.07 % (2988226)------------------------------
% 29.91/5.07 % (2988226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.91/5.07 % (2988226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.91/5.07 % (2988226)CaDiCaL version: 2.1.3
% 29.91/5.07 % (2988226)Termination reason: Instruction limit
% 29.91/5.07 % (2988226)Termination phase: Saturation
% 29.91/5.07 % (2988226)Time elapsed: 0.079 s
% 29.91/5.07 % (2988226)Peak memory usage: 91 MB
% 29.91/5.07 % (2988226)Instructions burned: 182 (million)
% 29.91/5.07 % (2988228)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=4091753390:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2977 on theBenchmark for (2977ds/10307Mi)
% 29.91/5.07 % (2988221)Instruction limit reached!
% 29.91/5.07 % (2988221)------------------------------
% 29.91/5.07 % (2988221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.91/5.07 % (2988221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.91/5.07 % (2988221)CaDiCaL version: 2.1.3
% 29.91/5.07 % (2988221)Termination reason: Instruction limit
% 29.91/5.07 % (2988221)Termination phase: Saturation
% 29.91/5.07 % (2988221)Time elapsed: 0.997 s
% 29.91/5.07 % (2988221)Peak memory usage: 142 MB
% 29.91/5.07 % (2988221)Instructions burned: 3258 (million)
% 29.91/5.07 % (2988230)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=3313738329:i=412:gtgl=4:gtg=exists_all_2973 on theBenchmark for (2973ds/412Mi)
% 29.91/5.07 % (2988201)Instruction limit reached!
% 29.91/5.07 % (2988201)------------------------------
% 29.91/5.07 % (2988201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.91/5.07 % (2988201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.91/5.07 % (2988201)CaDiCaL version: 2.1.3
% 29.91/5.07 % (2988201)Termination reason: Instruction limit
% 29.91/5.07 % (2988201)Termination phase: Saturation
% 29.91/5.07 % (2988201)Time elapsed: 2.039 s
% 29.91/5.07 % (2988201)Peak memory usage: 151 MB
% 29.91/5.07 % (2988201)Instructions burned: 3396 (million)
% 29.91/5.07 % (2988230)Instruction limit reached!
% 29.91/5.07 % (2988230)------------------------------
% 29.91/5.07 % (2988230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.91/5.07 % (2988230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.91/5.07 % (2988230)CaDiCaL version: 2.1.3
% 29.91/5.07 % (2988230)Termination reason: Instruction limit
% 29.91/5.07 % (2988230)Termination phase: Saturation
% 29.91/5.07 % (2988230)Time elapsed: 0.119 s
% 29.91/5.07 % (2988230)Peak memory usage: 102 MB
% 29.91/5.07 % (2988230)Instructions burned: 414 (million)
% 29.91/5.07 % (2988232)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=3265688804:s2pl=no:i=8478:s2at=4:nm=6_2971 on theBenchmark for (2971ds/8478Mi)
% 29.91/5.07 % (2988233)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=3284888237:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2971 on theBenchmark for (2971ds/303Mi)
% 29.91/5.07 % (2988233)Refutation not found, incomplete strategy
% 29.91/5.07 % (2988233)------------------------------
% 29.91/5.07 % (2988233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.91/5.07 % (2988233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.91/5.07 % (2988233)CaDiCaL version: 2.1.3
% 29.91/5.07 % (2988233)Termination reason: Refutation not found, incomplete strategy
% 29.91/5.07 % (2988233)Time elapsed: 0.001 s
% 29.91/5.07 % (2988233)Peak memory usage: 88 MB
% 29.91/5.07 % (2988233)------------------------------
% 29.91/5.07 % (2988233)------------------------------
% 29.91/5.07 % (2988236)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=752994303:st=4:i=720:sd=3:fsr=off:ss=axioms_2968 on theBenchmark for (2968ds/720Mi)
% 29.91/5.07 % (2988236)Refutation not found, incomplete strategy
% 29.91/5.07 % (2988236)------------------------------
% 29.91/5.07 % (2988236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.91/5.07 % (2988236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.91/5.07 % (2988236)CaDiCaL version: 2.1.3
% 29.91/5.07 % (2988236)Termination reason: Refutation not found, incomplete strategy
% 29.91/5.07 % (2988236)Time elapsed: 0.001 s
% 29.91/5.07 % (2988236)Peak memory usage: 88 MB
% 29.91/5.07 % (2988236)Instructions burned: 1 (million)
% 29.91/5.07 % (2988236)------------------------------
% 29.91/5.07 % (2988236)------------------------------
% 29.91/5.07 % (2988238)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1771770520:i=598:bs=on:bd=preordered:av=off:ss=axioms_2965 on theBenchmark for (2965ds/598Mi)
% 29.91/5.07 % (2988178)First to succeed.
% 29.91/5.07 % (2988178)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2988171"
% 29.91/5.07 % (2988238)Instruction limit reached!
% 29.91/5.07 % (2988238)------------------------------
% 29.91/5.07 % (2988238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.91/5.07 % (2988238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.91/5.07 % (2988238)CaDiCaL version: 2.1.3
% 29.91/5.07 % (2988238)Termination reason: Instruction limit
% 29.91/5.07 % (2988238)Termination phase: Saturation
% 29.91/5.07 % (2988238)Time elapsed: 0.301 s
% 29.91/5.07 % (2988238)Peak memory usage: 104 MB
% 29.91/5.07 % (2988238)Instructions burned: 598 (million)
% 29.91/5.07 % (2988209)Instruction limit reached!
% 29.91/5.07 % (2988209)------------------------------
% 29.91/5.07 % (2988209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.91/5.07 % (2988209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.91/5.07 % (2988209)CaDiCaL version: 2.1.3
% 29.91/5.07 % (2988209)Termination reason: Instruction limit
% 29.91/5.07 % (2988209)Termination phase: Saturation
% 29.91/5.07 % (2988209)Time elapsed: 2.966 s
% 29.91/5.07 % (2988209)Peak memory usage: 173 MB
% 29.91/5.07 % (2988209)Instructions burned: 5209 (million)
% 29.91/5.07 % (2988240)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1788679534:i=2989:sd=3:ss=axioms:sgt=60_2960 on theBenchmark for (2960ds/2989Mi)
% 29.91/5.07 % (2988241)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=2243865634:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2960 on theBenchmark for (2960ds/1997Mi)
% 29.91/5.07 % (2988178)Refutation found. Thanks to Tanya!
% 29.91/5.07 % SZS status Unsatisfiable for theBenchmark
% 29.91/5.07 % SZS output start Proof for theBenchmark
% See solution above
% 30.33/5.27 % (2988178)------------------------------
% 30.33/5.27 % (2988178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.33/5.27 % (2988178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.33/5.27 % (2988178)CaDiCaL version: 2.1.3
% 30.33/5.27 % (2988178)Termination reason: Refutation
% 30.33/5.27 % (2988178)Time elapsed: 3.733 s
% 30.33/5.27 % (2988178)Peak memory usage: 167 MB
% 30.33/5.27 % (2988178)Instructions burned: 6423 (million)
% 30.33/5.27 % (2988178)------------------------------
% 30.33/5.27 % (2988178)------------------------------
% 30.33/5.27 % (2988171)Success in time 4.206 s
% 30.33/5.27 % Vampire exiting
%------------------------------------------------------------------------------