%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT399-2 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.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:47:36 AM UTC 2026
% Result : Unsatisfiable 17.20s 3.09s
% Output : Refutation 17.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 16
% Syntax : Number of formulae : 312 ( 312 unt; 6 def)
% Number of atoms : 312 ( 311 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-3 aty)
% Number of variables : 400 ( 400 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity) ).
fof(f2,axiom,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity) ).
fof(f3,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_001) ).
fof(f4,axiom,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_002) ).
fof(f5,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption) ).
fof(f6,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption_003) ).
fof(f7,negated_conjecture,
! [X2,X0,X1] : upme(X0,X1,X2) = meet(X0,join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_of_upme) ).
fof(f8,negated_conjecture,
! [X2,X0,X1] : lome(X0,X1,X2) = join(meet(X0,X1),meet(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_of_lome) ).
fof(f11,negated_conjecture,
! [X2,X0,X1] : join(upme(meet(a,X0),X1,X2),meet(X1,X2)) = meet(join(meet(meet(a,X0),X1),X2),join(meet(meet(a,X0),X2),X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture) ).
fof(f12,negated_conjecture,
upme(meet(a,z1),z2,z3) != lome(meet(a,z1),z2,z3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture_1) ).
fof(f13,plain,
! [X2,X0,X1] : meet(join(meet(meet(a,X0),X1),X2),join(meet(meet(a,X0),X2),X1)) = join(meet(meet(a,X0),join(X1,X2)),meet(X1,X2)),
inference(definition_unfolding,[],[f11,f7]) ).
fof(f14,plain,
meet(meet(a,z1),join(z2,z3)) != join(meet(meet(a,z1),z2),meet(meet(a,z1),z3)),
inference(definition_unfolding,[],[f12,f7,f8]) ).
fof(f15,definition,
sF0 = meet(a,z1),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f16,plain,
meet(a,z1) = sF0,
inference(reorient_equations,[],[f15]) ).
fof(f17,definition,
sF1 = join(z2,z3),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f18,plain,
join(z2,z3) = sF1,
inference(reorient_equations,[],[f17]) ).
fof(f19,definition,
sF2 = meet(sF0,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f20,plain,
meet(sF0,sF1) = sF2,
inference(reorient_equations,[],[f19]) ).
fof(f21,definition,
sF3 = meet(sF0,z2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f22,plain,
meet(sF0,z2) = sF3,
inference(reorient_equations,[],[f21]) ).
fof(f23,definition,
sF4 = meet(sF0,z3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f24,plain,
meet(sF0,z3) = sF4,
inference(reorient_equations,[],[f23]) ).
fof(f25,definition,
sF5 = join(sF3,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f26,plain,
join(sF3,sF4) = sF5,
inference(reorient_equations,[],[f25]) ).
fof(f27,plain,
sF2 != sF5,
inference(definition_folding,[],[f14,f26,f24,f16,f22,f16,f20,f18,f16]) ).
fof(f28,plain,
! [X2,X0,X1] : meet(join(meet(meet(a,X0),X1),X2),join(meet(meet(a,X0),X2),X1)) = join(meet(X1,X2),meet(meet(a,X0),join(X1,X2))),
inference(backward_demodulation,[],[f13,f3]) ).
fof(f29,plain,
! [X2,X0,X1] : meet(join(meet(meet(a,X0),X1),X2),join(meet(meet(a,X0),X2),X1)) = join(meet(X1,X2),meet(a,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f28,f2]) ).
fof(f30,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(a,meet(X0,join(X1,X2)))) = meet(join(meet(meet(a,X0),X1),X2),join(meet(a,meet(X0,X2)),X1)),
inference(forward_demodulation,[],[f29,f2]) ).
fof(f31,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(a,meet(X0,join(X1,X2)))) = meet(join(meet(a,meet(X0,X1)),X2),join(meet(a,meet(X0,X2)),X1)),
inference(forward_demodulation,[],[f30,f2]) ).
fof(f40,plain,
! [X2,X0,X1] : join(meet(X1,join(X0,X2)),meet(a,meet(X0,join(X1,join(X0,X2))))) = meet(join(meet(a,meet(X0,X1)),join(X0,X2)),join(meet(a,X0),X1)),
inference(superposition,[],[f31,f6]) ).
fof(f41,plain,
! [X2,X0,X1] : join(meet(join(X0,X1),X2),meet(a,meet(X0,join(join(X0,X1),X2)))) = meet(join(meet(a,X0),X2),join(meet(a,meet(X0,X2)),join(X0,X1))),
inference(superposition,[],[f31,f6]) ).
fof(f42,plain,
! [X2,X0,X1] : meet(join(meet(a,X0),X2),join(meet(a,meet(X0,X2)),join(X0,X1))) = join(meet(join(X0,X1),X2),meet(a,meet(X0,join(X0,join(X1,X2))))),
inference(forward_demodulation,[],[f41,f4]) ).
fof(f43,plain,
! [X2,X0,X1] : join(meet(X1,join(X0,X2)),meet(a,meet(X0,join(X1,join(X0,X2))))) = meet(join(meet(a,X0),X1),join(meet(a,meet(X0,X1)),join(X0,X2))),
inference(forward_demodulation,[],[f40,f1]) ).
fof(f44,plain,
! [X2,X0,X1] : meet(join(meet(a,X0),X2),join(meet(a,meet(X0,X2)),join(X0,X1))) = join(meet(join(X0,X1),X2),meet(a,X0)),
inference(forward_demodulation,[],[f42,f6]) ).
fof(f45,plain,
! [X2,X0,X1] : meet(join(meet(a,X0),X2),join(meet(a,meet(X0,X2)),join(X0,X1))) = join(meet(a,X0),meet(join(X0,X1),X2)),
inference(forward_demodulation,[],[f44,f3]) ).
fof(f46,plain,
! [X2,X0,X1] : join(meet(X1,join(X0,X2)),meet(a,meet(X0,join(X1,join(X0,X2))))) = join(meet(a,X0),meet(join(X0,X2),X1)),
inference(backward_demodulation,[],[f43,f45]) ).
fof(f48,plain,
! [X0] : join(X0,X0) = X0,
inference(superposition,[],[f5,f6]) ).
fof(f51,plain,
! [X0] : meet(X0,X0) = X0,
inference(superposition,[],[f6,f5]) ).
fof(f68,plain,
z2 = meet(z2,sF1),
inference(superposition,[],[f6,f18]) ).
fof(f69,plain,
z2 = meet(sF1,z2),
inference(forward_demodulation,[],[f68,f1]) ).
fof(f70,plain,
a = join(a,sF0),
inference(superposition,[],[f5,f16]) ).
fof(f72,plain,
! [X0] : join(meet(z1,X0),meet(a,meet(a,join(z1,X0)))) = meet(join(meet(a,sF0),X0),join(meet(a,meet(a,X0)),z1)),
inference(superposition,[],[f31,f16]) ).
fof(f73,plain,
! [X0] : join(meet(z1,X0),meet(a,meet(a,join(z1,X0)))) = meet(join(meet(a,sF0),X0),join(z1,meet(a,meet(a,X0)))),
inference(forward_demodulation,[],[f72,f3]) ).
fof(f75,plain,
a = join(sF0,a),
inference(forward_demodulation,[],[f70,f3]) ).
fof(f76,plain,
! [X0] : join(meet(z1,X0),meet(a,meet(a,join(z1,X0)))) = meet(join(meet(sF0,a),X0),join(z1,meet(a,meet(a,X0)))),
inference(forward_demodulation,[],[f73,f1]) ).
fof(f79,plain,
sF0 = join(sF0,sF3),
inference(superposition,[],[f5,f22]) ).
fof(f87,plain,
sF0 = join(sF0,sF4),
inference(superposition,[],[f5,f24]) ).
fof(f108,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f5,f1]) ).
fof(f109,plain,
! [X2,X0,X1] : join(meet(X2,X0),meet(a,meet(X1,join(X2,X0)))) = meet(join(meet(a,meet(X1,X2)),X0),join(meet(a,meet(X0,X1)),X2)),
inference(superposition,[],[f31,f1]) ).
fof(f110,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(a,meet(X1,join(X0,X2)))) = meet(join(meet(a,meet(X0,X1)),X2),join(meet(a,meet(X1,X2)),X0)),
inference(superposition,[],[f31,f1]) ).
fof(f118,plain,
z3 = join(z3,sF4),
inference(superposition,[],[f108,f24]) ).
fof(f125,plain,
z3 = join(sF4,z3),
inference(forward_demodulation,[],[f118,f3]) ).
fof(f142,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f6,f3]) ).
fof(f144,plain,
! [X2,X0,X1] : join(meet(X2,X0),meet(a,meet(X1,join(X2,X0)))) = meet(join(X0,meet(a,meet(X1,X2))),join(meet(a,meet(X1,X0)),X2)),
inference(superposition,[],[f31,f3]) ).
fof(f147,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f142,f5]) ).
fof(f151,plain,
z3 = meet(z3,sF1),
inference(superposition,[],[f142,f18]) ).
fof(f155,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,X0)),meet(a,meet(X0,join(X1,join(X2,X0))))) = meet(join(meet(a,meet(X0,X1)),join(X2,X0)),join(meet(a,X0),X1)),
inference(superposition,[],[f31,f142]) ).
fof(f156,plain,
! [X2,X0,X1] : join(meet(join(X1,X0),X2),meet(a,meet(X0,join(join(X1,X0),X2)))) = meet(join(meet(a,X0),X2),join(meet(a,meet(X0,X2)),join(X1,X0))),
inference(superposition,[],[f31,f142]) ).
fof(f157,plain,
! [X2,X0,X1] : meet(join(meet(a,X0),X2),join(meet(a,meet(X0,X2)),join(X1,X0))) = join(meet(join(X1,X0),X2),meet(a,meet(X0,join(X1,join(X0,X2))))),
inference(forward_demodulation,[],[f156,f4]) ).
fof(f158,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,X0)),meet(a,meet(X0,join(X1,join(X2,X0))))) = meet(join(meet(a,X0),X1),join(meet(a,meet(X0,X1)),join(X2,X0))),
inference(forward_demodulation,[],[f155,f1]) ).
fof(f160,plain,
z3 = meet(sF1,z3),
inference(forward_demodulation,[],[f151,f1]) ).
fof(f162,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f147,f2]) ).
fof(f167,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f2,f6]) ).
fof(f168,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f2,f142]) ).
fof(f169,plain,
! [X0] : meet(sF0,X0) = meet(a,meet(z1,X0)),
inference(superposition,[],[f2,f16]) ).
fof(f171,plain,
! [X0] : meet(sF0,meet(z3,X0)) = meet(sF4,X0),
inference(superposition,[],[f2,f24]) ).
fof(f172,plain,
! [X0] : meet(sF0,meet(sF1,X0)) = meet(sF2,X0),
inference(superposition,[],[f2,f20]) ).
fof(f178,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f209,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f4,f5]) ).
fof(f210,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f4,f108]) ).
fof(f214,plain,
! [X0] : join(sF1,X0) = join(z2,join(z3,X0)),
inference(superposition,[],[f4,f18]) ).
fof(f215,plain,
! [X0] : join(sF3,join(sF4,X0)) = join(sF5,X0),
inference(superposition,[],[f4,f26]) ).
fof(f220,plain,
! [X2,X0,X1] : meet(X2,join(X0,join(X1,X2))) = X2,
inference(superposition,[],[f142,f4]) ).
fof(f222,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f3,f4]) ).
fof(f226,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,X0)),meet(a,meet(X0,join(X1,join(X2,X0))))) = meet(join(meet(a,X0),X1),join(X0,join(meet(a,meet(X0,X1)),X2))),
inference(backward_demodulation,[],[f158,f222]) ).
fof(f227,plain,
! [X2,X0,X1] : join(meet(join(X1,X0),X2),meet(a,meet(X0,join(X1,join(X0,X2))))) = meet(join(meet(a,X0),X2),join(X0,join(meet(a,meet(X0,X2)),X1))),
inference(backward_demodulation,[],[f157,f222]) ).
fof(f228,plain,
! [X2,X0,X1] : join(meet(a,X0),meet(join(X0,X1),X2)) = meet(join(meet(a,X0),X2),join(X0,join(X1,meet(a,meet(X0,X2))))),
inference(backward_demodulation,[],[f45,f222]) ).
fof(f232,plain,
! [X2,X0,X1] : meet(join(meet(a,X0),X1),join(X0,join(meet(a,meet(X0,X1)),X2))) = join(meet(X1,join(X2,X0)),meet(a,X0)),
inference(forward_demodulation,[],[f226,f220]) ).
fof(f234,plain,
! [X2,X0,X1] : meet(join(meet(a,X0),X1),join(X0,join(meet(a,meet(X0,X1)),X2))) = join(meet(a,X0),meet(X1,join(X2,X0))),
inference(forward_demodulation,[],[f232,f3]) ).
fof(f235,plain,
! [X2,X0,X1] : join(meet(join(X1,X0),X2),meet(a,meet(X0,join(X1,join(X0,X2))))) = join(meet(a,X0),meet(X2,join(X1,X0))),
inference(backward_demodulation,[],[f227,f234]) ).
fof(f244,plain,
! [X0] : join(sF0,X0) = join(sF0,join(sF4,X0)),
inference(superposition,[],[f209,f24]) ).
fof(f247,plain,
! [X2,X0,X1] : join(X0,meet(X0,X1)) = join(X0,meet(X2,meet(X0,X1))),
inference(superposition,[],[f209,f108]) ).
fof(f249,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f209,f3]) ).
fof(f265,plain,
! [X2,X0,X1] : join(X0,meet(X2,meet(X0,X1))) = X0,
inference(forward_demodulation,[],[f247,f5]) ).
fof(f283,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(superposition,[],[f167,f108]) ).
fof(f291,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f167,f1]) ).
fof(f295,plain,
! [X2,X0,X1] : meet(X0,join(X0,X1)) = meet(X0,join(X2,join(X0,X1))),
inference(superposition,[],[f167,f142]) ).
fof(f314,plain,
! [X2,X0,X1] : meet(X0,join(X2,join(X0,X1))) = X0,
inference(forward_demodulation,[],[f295,f6]) ).
fof(f320,plain,
! [X0] : join(meet(z1,X0),meet(a,meet(a,join(z1,X0)))) = meet(join(meet(sF0,a),X0),join(z1,meet(a,X0))),
inference(backward_demodulation,[],[f76,f283]) ).
fof(f324,plain,
! [X2,X0,X1] : join(meet(a,X0),meet(X2,join(X1,X0))) = join(meet(join(X1,X0),X2),meet(a,X0)),
inference(backward_demodulation,[],[f235,f314]) ).
fof(f325,plain,
! [X2,X0,X1] : join(meet(a,X0),meet(join(X0,X2),X1)) = join(meet(X1,join(X0,X2)),meet(a,X0)),
inference(backward_demodulation,[],[f46,f314]) ).
fof(f329,plain,
! [X0] : join(meet(z1,X0),meet(a,meet(a,join(z1,X0)))) = meet(join(z1,meet(a,X0)),join(meet(sF0,a),X0)),
inference(forward_demodulation,[],[f320,f1]) ).
fof(f332,plain,
! [X2,X0,X1] : join(meet(a,X0),meet(join(X0,X2),X1)) = join(meet(a,X0),meet(X1,join(X0,X2))),
inference(forward_demodulation,[],[f325,f3]) ).
fof(f333,plain,
! [X2,X0,X1] : join(meet(a,X0),meet(X2,join(X1,X0))) = join(meet(a,X0),meet(join(X1,X0),X2)),
inference(forward_demodulation,[],[f324,f3]) ).
fof(f335,plain,
! [X0] : meet(join(z1,meet(a,X0)),join(meet(sF0,a),X0)) = join(meet(z1,X0),meet(a,join(z1,X0))),
inference(forward_demodulation,[],[f329,f283]) ).
fof(f434,plain,
! [X0,X1] : meet(sF0,meet(z3,X0)) = meet(sF4,meet(join(z3,X1),X0)),
inference(superposition,[],[f171,f167]) ).
fof(f449,plain,
! [X0,X1] : meet(sF4,X0) = meet(sF4,meet(join(z3,X1),X0)),
inference(forward_demodulation,[],[f434,f171]) ).
fof(f463,plain,
! [X0,X1] : join(meet(X0,X1),meet(a,meet(X0,join(X0,X1)))) = meet(join(meet(a,X0),X1),join(meet(a,meet(X0,X1)),X0)),
inference(superposition,[],[f31,f51]) ).
fof(f464,plain,
! [X0,X1] : join(meet(X1,X0),meet(a,meet(X0,join(X1,X0)))) = meet(join(meet(a,meet(X0,X1)),X0),join(meet(a,X0),X1)),
inference(superposition,[],[f31,f51]) ).
fof(f476,plain,
! [X0,X1] : meet(join(meet(a,X0),X1),join(meet(a,meet(X0,X1)),X0)) = join(meet(X1,X0),meet(a,meet(X0,join(X1,X0)))),
inference(forward_demodulation,[],[f464,f1]) ).
fof(f477,plain,
! [X0,X1] : join(meet(X0,X1),meet(a,meet(X0,join(X0,X1)))) = meet(join(meet(a,X0),X1),join(X0,meet(a,meet(X0,X1)))),
inference(forward_demodulation,[],[f463,f3]) ).
fof(f481,plain,
! [X0,X1] : meet(join(meet(a,X0),X1),join(meet(a,meet(X0,X1)),X0)) = join(meet(X1,X0),meet(a,X0)),
inference(forward_demodulation,[],[f476,f142]) ).
fof(f482,plain,
! [X0,X1] : join(meet(X0,X1),meet(a,meet(X0,join(X0,X1)))) = meet(join(meet(a,X0),X1),X0),
inference(forward_demodulation,[],[f477,f265]) ).
fof(f484,plain,
! [X0,X1] : meet(join(meet(a,X0),X1),join(X0,meet(a,meet(X0,X1)))) = join(meet(X1,X0),meet(a,X0)),
inference(forward_demodulation,[],[f481,f3]) ).
fof(f485,plain,
! [X0,X1] : join(meet(X0,X1),meet(a,meet(X0,join(X0,X1)))) = meet(X0,join(meet(a,X0),X1)),
inference(forward_demodulation,[],[f482,f1]) ).
fof(f487,plain,
! [X0,X1] : join(meet(X1,X0),meet(a,X0)) = meet(join(meet(a,X0),X1),X0),
inference(forward_demodulation,[],[f484,f265]) ).
fof(f488,plain,
! [X0,X1] : meet(X0,join(meet(a,X0),X1)) = join(meet(X0,X1),meet(a,X0)),
inference(forward_demodulation,[],[f485,f6]) ).
fof(f490,plain,
! [X0,X1] : join(meet(X1,X0),meet(a,X0)) = meet(X0,join(meet(a,X0),X1)),
inference(forward_demodulation,[],[f487,f1]) ).
fof(f515,plain,
! [X0,X1] : join(meet(X1,meet(a,a)),meet(a,meet(X0,join(X1,meet(a,a))))) = meet(meet(a,join(meet(a,a),meet(X0,X1))),join(meet(a,meet(X0,meet(a,a))),X1)),
inference(superposition,[],[f31,f488]) ).
fof(f530,plain,
! [X0,X1] : join(meet(X1,meet(a,a)),meet(a,meet(X0,join(X1,meet(a,a))))) = meet(a,meet(join(meet(a,a),meet(X0,X1)),join(meet(a,meet(X0,meet(a,a))),X1))),
inference(forward_demodulation,[],[f515,f2]) ).
fof(f551,plain,
! [X0,X1] : join(meet(X1,a),meet(a,meet(X0,join(X1,a)))) = meet(a,meet(join(a,meet(X0,X1)),join(meet(a,meet(X0,a)),X1))),
inference(forward_demodulation,[],[f530,f51]) ).
fof(f563,plain,
! [X0,X1] : join(meet(X1,a),meet(a,meet(X0,join(X1,a)))) = meet(a,join(meet(a,meet(X0,a)),X1)),
inference(forward_demodulation,[],[f551,f167]) ).
fof(f567,plain,
! [X0,X1] : join(meet(X1,a),meet(a,meet(X0,join(X1,a)))) = meet(a,join(meet(a,X0),X1)),
inference(forward_demodulation,[],[f563,f162]) ).
fof(f613,plain,
meet(z3,join(meet(a,z3),sF0)) = join(sF4,meet(a,z3)),
inference(superposition,[],[f490,f24]) ).
fof(f646,plain,
join(sF4,meet(a,z3)) = meet(z3,join(sF0,meet(a,z3))),
inference(forward_demodulation,[],[f613,f3]) ).
fof(f837,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,X0)),meet(a,meet(X0,join(X1,join(X2,X0))))) = meet(join(meet(a,meet(X1,X0)),join(X2,X0)),join(meet(a,X0),X1)),
inference(superposition,[],[f110,f142]) ).
fof(f901,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,X0)),meet(a,meet(X0,join(X1,join(X2,X0))))) = meet(join(meet(a,X0),X1),join(meet(a,meet(X1,X0)),join(X2,X0))),
inference(forward_demodulation,[],[f837,f1]) ).
fof(f958,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,X0)),meet(a,meet(X0,join(X1,join(X2,X0))))) = meet(join(meet(a,X0),X1),join(X0,join(meet(a,meet(X1,X0)),X2))),
inference(forward_demodulation,[],[f901,f222]) ).
fof(f1008,plain,
! [X2,X0,X1] : join(meet(X1,join(X2,X0)),meet(a,X0)) = meet(join(meet(a,X0),X1),join(X0,join(meet(a,meet(X1,X0)),X2))),
inference(forward_demodulation,[],[f958,f220]) ).
fof(f1051,plain,
! [X2,X0,X1] : join(meet(a,X0),meet(X1,join(X2,X0))) = meet(join(meet(a,X0),X1),join(X0,join(meet(a,meet(X1,X0)),X2))),
inference(forward_demodulation,[],[f1008,f3]) ).
fof(f1248,plain,
! [X0] : join(meet(z3,X0),meet(a,meet(sF0,join(z3,X0)))) = meet(join(meet(a,sF4),X0),join(meet(a,meet(X0,sF0)),z3)),
inference(superposition,[],[f109,f24]) ).
fof(f1274,plain,
! [X0] : join(meet(X0,a),meet(a,meet(z1,join(X0,a)))) = meet(join(meet(a,meet(z1,X0)),a),join(meet(a,sF0),X0)),
inference(superposition,[],[f109,f16]) ).
fof(f1338,plain,
! [X0] : meet(join(meet(a,sF0),X0),join(meet(a,meet(z1,X0)),a)) = join(meet(X0,a),meet(a,meet(z1,join(X0,a)))),
inference(forward_demodulation,[],[f1274,f1]) ).
fof(f1359,plain,
! [X0] : join(meet(z3,X0),meet(a,meet(sF0,join(z3,X0)))) = meet(join(meet(a,sF4),X0),join(z3,meet(a,meet(X0,sF0)))),
inference(forward_demodulation,[],[f1248,f3]) ).
fof(f1400,plain,
! [X0] : meet(join(meet(a,sF0),X0),join(meet(a,meet(z1,X0)),a)) = meet(a,join(meet(a,z1),X0)),
inference(forward_demodulation,[],[f1338,f567]) ).
fof(f1421,plain,
! [X0] : join(meet(z3,X0),meet(a,meet(sF0,join(z3,X0)))) = meet(join(meet(a,sF4),X0),join(z3,meet(sF0,meet(a,X0)))),
inference(forward_demodulation,[],[f1359,f178]) ).
fof(f1458,plain,
! [X0] : meet(join(meet(a,sF0),X0),join(meet(a,meet(z1,X0)),a)) = meet(a,join(sF0,X0)),
inference(forward_demodulation,[],[f1400,f16]) ).
fof(f1476,plain,
! [X0] : join(meet(z3,X0),meet(a,meet(sF0,join(z3,X0)))) = meet(join(meet(sF4,a),X0),join(z3,meet(sF0,meet(a,X0)))),
inference(forward_demodulation,[],[f1421,f1]) ).
fof(f1506,plain,
! [X0] : meet(join(meet(a,sF0),X0),join(a,meet(a,meet(z1,X0)))) = meet(a,join(sF0,X0)),
inference(forward_demodulation,[],[f1458,f3]) ).
fof(f1520,plain,
! [X0] : join(meet(z3,X0),meet(sF0,meet(join(z3,X0),a))) = meet(join(meet(sF4,a),X0),join(z3,meet(sF0,meet(a,X0)))),
inference(forward_demodulation,[],[f1476,f178]) ).
fof(f1544,plain,
! [X0] : meet(join(meet(a,sF0),X0),a) = meet(a,join(sF0,X0)),
inference(forward_demodulation,[],[f1506,f5]) ).
fof(f1553,plain,
! [X0] : join(meet(z3,X0),meet(sF0,meet(a,join(z3,X0)))) = meet(join(meet(sF4,a),X0),join(z3,meet(sF0,meet(a,X0)))),
inference(forward_demodulation,[],[f1520,f1]) ).
fof(f1573,plain,
! [X0] : meet(a,join(meet(a,sF0),X0)) = meet(a,join(sF0,X0)),
inference(forward_demodulation,[],[f1544,f1]) ).
fof(f1587,plain,
! [X0] : meet(a,join(sF0,X0)) = meet(a,join(meet(sF0,a),X0)),
inference(forward_demodulation,[],[f1573,f1]) ).
fof(f1649,plain,
! [X0] : join(meet(sF0,a),X0) = join(join(meet(sF0,a),X0),meet(a,join(sF0,X0))),
inference(superposition,[],[f108,f1587]) ).
fof(f1665,plain,
! [X0] : join(meet(sF0,a),X0) = join(meet(a,join(sF0,X0)),join(meet(sF0,a),X0)),
inference(forward_demodulation,[],[f1649,f3]) ).
fof(f1684,plain,
! [X0] : join(meet(sF0,a),X0) = join(X0,join(meet(a,join(sF0,X0)),meet(sF0,a))),
inference(forward_demodulation,[],[f1665,f222]) ).
fof(f1698,plain,
! [X0] : join(meet(sF0,a),X0) = join(X0,join(meet(sF0,a),meet(a,join(sF0,X0)))),
inference(forward_demodulation,[],[f1684,f3]) ).
fof(f1875,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = meet(meet(join(X2,X0),X1),join(meet(a,X0),meet(X1,join(X2,X0)))),
inference(superposition,[],[f142,f333]) ).
fof(f1878,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = meet(join(X2,X0),meet(X1,join(meet(a,X0),meet(X1,join(X2,X0))))),
inference(forward_demodulation,[],[f1875,f2]) ).
fof(f2024,plain,
! [X2,X3,X0,X1] : join(X1,X3) = join(X1,join(meet(X0,meet(X1,X2)),X3)),
inference(superposition,[],[f209,f178]) ).
fof(f2031,plain,
! [X2,X3,X0,X1] : meet(X1,meet(X3,X0)) = meet(X1,meet(X0,meet(join(X1,X2),X3))),
inference(superposition,[],[f167,f178]) ).
fof(f2060,plain,
! [X2,X3,X0,X1] : join(X2,X3) = join(X2,join(meet(X0,meet(X1,X2)),X3)),
inference(superposition,[],[f209,f178]) ).
fof(f2089,plain,
! [X2,X0,X1] : join(meet(a,X0),meet(X1,join(X2,X0))) = meet(join(meet(a,X0),X1),join(X0,X2)),
inference(backward_demodulation,[],[f1051,f2060]) ).
fof(f2146,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = meet(join(X2,X0),meet(X1,meet(join(meet(a,X0),X1),join(X0,X2)))),
inference(backward_demodulation,[],[f1878,f2089]) ).
fof(f2181,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = meet(join(X2,X0),meet(X1,join(X0,X2))),
inference(forward_demodulation,[],[f2146,f168]) ).
fof(f2435,plain,
! [X2,X3,X0,X1] : join(X0,join(X1,join(X2,X3))) = join(X2,join(X3,join(X0,X1))),
inference(superposition,[],[f4,f222]) ).
fof(f2711,plain,
join(z2,z3) = join(sF1,z3),
inference(superposition,[],[f214,f48]) ).
fof(f2713,plain,
! [X0] : join(sF1,X0) = join(z2,join(X0,z3)),
inference(superposition,[],[f214,f3]) ).
fof(f2737,plain,
sF1 = join(sF1,z3),
inference(forward_demodulation,[],[f2711,f18]) ).
fof(f2755,plain,
! [X0,X1] : join(meet(X1,X0),meet(a,meet(z1,join(X1,X0)))) = meet(join(meet(a,meet(z1,X1)),X0),join(meet(sF0,X0),X1)),
inference(superposition,[],[f31,f169]) ).
fof(f2756,plain,
! [X0,X1] : join(meet(X0,X1),meet(a,meet(z1,join(X0,X1)))) = meet(join(meet(sF0,X0),X1),join(meet(a,meet(z1,X1)),X0)),
inference(superposition,[],[f31,f169]) ).
fof(f2798,plain,
! [X0,X1] : join(meet(X0,X1),meet(a,meet(z1,join(X0,X1)))) = meet(join(meet(sF0,X0),X1),join(meet(sF0,X1),X0)),
inference(forward_demodulation,[],[f2756,f169]) ).
fof(f2799,plain,
! [X0,X1] : join(meet(X1,X0),meet(a,meet(z1,join(X1,X0)))) = meet(join(meet(sF0,X0),X1),join(meet(a,meet(z1,X1)),X0)),
inference(forward_demodulation,[],[f2755,f1]) ).
fof(f2825,plain,
! [X0,X1] : meet(join(meet(sF0,X0),X1),join(meet(sF0,X1),X0)) = join(meet(X0,X1),meet(sF0,join(X0,X1))),
inference(forward_demodulation,[],[f2798,f169]) ).
fof(f2826,plain,
! [X0,X1] : join(meet(X1,X0),meet(a,meet(z1,join(X1,X0)))) = meet(join(meet(sF0,X0),X1),join(meet(sF0,X1),X0)),
inference(forward_demodulation,[],[f2799,f169]) ).
fof(f2841,plain,
! [X0,X1] : join(meet(X1,X0),meet(a,meet(z1,join(X1,X0)))) = join(meet(X0,X1),meet(sF0,join(X0,X1))),
inference(forward_demodulation,[],[f2826,f2825]) ).
fof(f2851,plain,
! [X0,X1] : join(meet(X0,X1),meet(sF0,join(X0,X1))) = join(meet(X1,X0),meet(sF0,join(X1,X0))),
inference(forward_demodulation,[],[f2841,f169]) ).
fof(f2865,plain,
sF0 = meet(sF0,a),
inference(superposition,[],[f6,f75]) ).
fof(f2867,plain,
! [X0] : meet(sF0,X0) = meet(sF0,meet(a,X0)),
inference(superposition,[],[f167,f75]) ).
fof(f2870,plain,
! [X0] : join(meet(a,sF0),meet(a,X0)) = join(meet(a,sF0),meet(X0,a)),
inference(superposition,[],[f332,f75]) ).
fof(f2871,plain,
! [X0] : join(meet(sF0,a),meet(a,X0)) = join(meet(sF0,a),meet(X0,a)),
inference(forward_demodulation,[],[f2870,f1]) ).
fof(f2879,plain,
! [X0] : join(meet(z3,X0),meet(sF0,meet(a,join(z3,X0)))) = meet(join(meet(sF4,a),X0),join(z3,meet(sF0,X0))),
inference(backward_demodulation,[],[f1553,f2867]) ).
fof(f2897,plain,
! [X0] : join(meet(z1,X0),meet(a,join(z1,X0))) = meet(join(z1,meet(a,X0)),join(sF0,X0)),
inference(backward_demodulation,[],[f335,f2865]) ).
fof(f2909,plain,
! [X0] : join(sF0,X0) = join(X0,join(sF0,meet(a,join(sF0,X0)))),
inference(backward_demodulation,[],[f1698,f2865]) ).
fof(f2917,plain,
! [X0] : join(sF0,meet(X0,a)) = join(sF0,meet(a,X0)),
inference(forward_demodulation,[],[f2871,f2865]) ).
fof(f2925,plain,
! [X0] : join(meet(z3,X0),meet(sF0,meet(a,join(z3,X0)))) = meet(join(z3,meet(sF0,X0)),join(meet(sF4,a),X0)),
inference(forward_demodulation,[],[f2879,f1]) ).
fof(f2943,plain,
! [X0] : join(meet(z1,X0),meet(a,join(z1,X0))) = meet(join(sF0,X0),join(z1,meet(a,X0))),
inference(forward_demodulation,[],[f2897,f1]) ).
fof(f2949,plain,
! [X0] : join(meet(z3,X0),meet(sF0,join(z3,X0))) = meet(join(z3,meet(sF0,X0)),join(meet(sF4,a),X0)),
inference(forward_demodulation,[],[f2925,f2867]) ).
fof(f3369,plain,
join(meet(z3,z2),meet(sF0,join(z3,z2))) = meet(join(z3,sF3),join(meet(sF4,a),z2)),
inference(superposition,[],[f2949,f22]) ).
fof(f3371,plain,
join(meet(z3,sF1),meet(sF0,join(z3,sF1))) = meet(join(z3,sF2),join(meet(sF4,a),sF1)),
inference(superposition,[],[f2949,f20]) ).
fof(f3373,plain,
join(meet(z3,meet(a,sF4)),meet(sF0,join(z3,meet(a,sF4)))) = meet(join(z3,meet(sF0,meet(a,sF4))),meet(sF4,join(meet(a,sF4),a))),
inference(superposition,[],[f2949,f488]) ).
fof(f3421,plain,
join(meet(z3,meet(a,sF4)),meet(sF0,join(z3,meet(a,sF4)))) = meet(meet(sF4,join(meet(a,sF4),a)),join(z3,meet(sF0,meet(a,sF4)))),
inference(forward_demodulation,[],[f3373,f1]) ).
fof(f3423,plain,
join(meet(z3,sF1),meet(sF0,join(z3,sF1))) = meet(join(z3,sF2),join(sF1,meet(sF4,a))),
inference(forward_demodulation,[],[f3371,f3]) ).
fof(f3425,plain,
join(meet(z3,z2),meet(sF0,join(z3,z2))) = meet(join(z3,sF3),join(z2,meet(sF4,a))),
inference(forward_demodulation,[],[f3369,f3]) ).
fof(f3451,plain,
join(meet(z3,meet(a,sF4)),meet(sF0,join(z3,meet(a,sF4)))) = meet(sF4,meet(join(meet(a,sF4),a),join(z3,meet(sF0,meet(a,sF4))))),
inference(forward_demodulation,[],[f3421,f2]) ).
fof(f3453,plain,
meet(join(z3,sF2),join(sF1,meet(sF4,a))) = join(meet(sF1,z3),meet(sF0,join(sF1,z3))),
inference(forward_demodulation,[],[f3423,f2851]) ).
fof(f3455,plain,
join(meet(z3,z2),meet(sF0,join(z3,z2))) = meet(join(sF3,z3),join(z2,meet(sF4,a))),
inference(forward_demodulation,[],[f3425,f3]) ).
fof(f3479,plain,
join(meet(z3,meet(a,sF4)),meet(sF0,join(z3,meet(a,sF4)))) = meet(sF4,meet(join(meet(a,sF4),a),join(z3,meet(sF0,sF4)))),
inference(forward_demodulation,[],[f3451,f2867]) ).
fof(f3481,plain,
meet(join(z3,sF2),join(sF1,meet(sF4,a))) = join(meet(sF1,z3),meet(sF0,sF1)),
inference(forward_demodulation,[],[f3453,f2737]) ).
fof(f3483,plain,
join(meet(z2,z3),meet(sF0,join(z2,z3))) = meet(join(sF3,z3),join(z2,meet(sF4,a))),
inference(forward_demodulation,[],[f3455,f2851]) ).
fof(f3500,plain,
join(meet(z3,meet(a,sF4)),meet(sF0,join(z3,meet(a,sF4)))) = meet(sF4,meet(join(z3,meet(sF0,sF4)),join(meet(a,sF4),a))),
inference(forward_demodulation,[],[f3479,f1]) ).
fof(f3502,plain,
meet(join(z3,sF2),join(sF1,meet(sF4,a))) = join(meet(sF0,sF1),meet(sF1,z3)),
inference(forward_demodulation,[],[f3481,f3]) ).
fof(f3504,plain,
join(meet(z2,z3),meet(sF0,sF1)) = meet(join(sF3,z3),join(z2,meet(sF4,a))),
inference(forward_demodulation,[],[f3483,f18]) ).
fof(f3517,plain,
meet(sF4,join(meet(a,sF4),a)) = join(meet(z3,meet(a,sF4)),meet(sF0,join(z3,meet(a,sF4)))),
inference(forward_demodulation,[],[f3500,f449]) ).
fof(f3519,plain,
meet(join(z3,sF2),join(sF1,meet(sF4,a))) = join(meet(sF0,sF1),z3),
inference(forward_demodulation,[],[f3502,f160]) ).
fof(f3521,plain,
join(meet(sF0,sF1),meet(z2,z3)) = meet(join(sF3,z3),join(z2,meet(sF4,a))),
inference(forward_demodulation,[],[f3504,f3]) ).
fof(f3527,plain,
join(meet(z3,meet(sF4,a)),meet(sF0,join(z3,meet(sF4,a)))) = meet(sF4,join(meet(sF4,a),a)),
inference(forward_demodulation,[],[f3517,f1]) ).
fof(f3528,plain,
join(z3,meet(sF0,sF1)) = meet(join(z3,sF2),join(sF1,meet(sF4,a))),
inference(forward_demodulation,[],[f3519,f3]) ).
fof(f3530,plain,
join(sF2,meet(z2,z3)) = meet(join(sF3,z3),join(z2,meet(sF4,a))),
inference(forward_demodulation,[],[f3521,f20]) ).
fof(f3534,plain,
join(meet(z3,meet(sF4,a)),meet(sF0,join(z3,meet(sF4,a)))) = meet(sF4,join(a,meet(sF4,a))),
inference(forward_demodulation,[],[f3527,f3]) ).
fof(f3535,plain,
join(z3,sF2) = meet(join(z3,sF2),join(sF1,meet(sF4,a))),
inference(forward_demodulation,[],[f3528,f20]) ).
fof(f3540,plain,
meet(sF4,a) = join(meet(z3,meet(sF4,a)),meet(sF0,join(z3,meet(sF4,a)))),
inference(forward_demodulation,[],[f3534,f108]) ).
fof(f3544,plain,
meet(sF4,a) = join(meet(a,meet(z3,sF4)),meet(sF0,join(z3,meet(sF4,a)))),
inference(forward_demodulation,[],[f3540,f178]) ).
fof(f3546,plain,
meet(sF4,a) = join(meet(sF4,meet(a,z3)),meet(sF0,join(z3,meet(sF4,a)))),
inference(forward_demodulation,[],[f3544,f178]) ).
fof(f3578,plain,
! [X0,X1] : meet(meet(z1,X0),X1) = meet(meet(z1,X0),meet(meet(join(sF0,X0),join(z1,meet(a,X0))),X1)),
inference(superposition,[],[f167,f2943]) ).
fof(f3584,plain,
! [X0,X1] : meet(meet(z1,X0),X1) = meet(z1,meet(X0,meet(meet(join(sF0,X0),join(z1,meet(a,X0))),X1))),
inference(forward_demodulation,[],[f3578,f2]) ).
fof(f3598,plain,
! [X0,X1] : meet(meet(z1,X0),X1) = meet(z1,meet(X0,meet(join(sF0,X0),meet(join(z1,meet(a,X0)),X1)))),
inference(forward_demodulation,[],[f3584,f2]) ).
fof(f3608,plain,
! [X0,X1] : meet(meet(z1,X0),X1) = meet(z1,meet(X0,meet(join(z1,meet(a,X0)),X1))),
inference(forward_demodulation,[],[f3598,f168]) ).
fof(f3617,plain,
! [X0,X1] : meet(z1,meet(X1,X0)) = meet(meet(z1,X0),X1),
inference(forward_demodulation,[],[f3608,f2031]) ).
fof(f3624,plain,
! [X0,X1] : meet(z1,meet(X1,X0)) = meet(z1,meet(X0,X1)),
inference(forward_demodulation,[],[f3617,f2]) ).
fof(f3698,plain,
! [X0,X1] : meet(a,meet(z1,meet(X0,X1))) = meet(sF0,meet(X1,X0)),
inference(superposition,[],[f169,f3624]) ).
fof(f3733,plain,
! [X0,X1] : meet(sF0,meet(X0,X1)) = meet(sF0,meet(X1,X0)),
inference(forward_demodulation,[],[f3698,f169]) ).
fof(f3825,plain,
join(sF3,z3) = join(join(sF3,z3),join(sF2,meet(z2,z3))),
inference(superposition,[],[f5,f3530]) ).
fof(f3853,plain,
join(sF3,z3) = join(meet(z2,z3),join(join(sF3,z3),sF2)),
inference(forward_demodulation,[],[f3825,f222]) ).
fof(f3867,plain,
join(sF3,z3) = join(sF2,join(meet(z2,z3),join(sF3,z3))),
inference(forward_demodulation,[],[f3853,f222]) ).
fof(f3880,plain,
join(sF3,z3) = join(sF3,join(z3,join(sF2,meet(z2,z3)))),
inference(forward_demodulation,[],[f3867,f2435]) ).
fof(f3890,plain,
! [X0] : join(sF3,sF4) = join(sF5,meet(sF4,X0)),
inference(superposition,[],[f215,f5]) ).
fof(f3895,plain,
join(sF5,join(sF0,meet(a,join(sF0,sF4)))) = join(sF3,join(sF0,sF4)),
inference(superposition,[],[f215,f2909]) ).
fof(f3911,plain,
join(sF5,join(sF0,meet(a,join(sF0,sF4)))) = join(sF0,join(sF4,sF3)),
inference(forward_demodulation,[],[f3895,f222]) ).
fof(f3914,plain,
! [X0] : sF5 = join(sF5,meet(sF4,X0)),
inference(forward_demodulation,[],[f3890,f26]) ).
fof(f3919,plain,
join(sF0,sF3) = join(sF5,join(sF0,meet(a,join(sF0,sF4)))),
inference(forward_demodulation,[],[f3911,f244]) ).
fof(f3922,plain,
join(sF0,sF3) = join(sF0,join(meet(a,join(sF0,sF4)),sF5)),
inference(forward_demodulation,[],[f3919,f222]) ).
fof(f3923,plain,
join(sF0,sF3) = join(sF0,join(sF5,meet(a,join(sF0,sF4)))),
inference(forward_demodulation,[],[f3922,f3]) ).
fof(f3924,plain,
join(sF0,sF3) = join(sF0,join(sF5,meet(a,sF0))),
inference(forward_demodulation,[],[f3923,f87]) ).
fof(f3925,plain,
join(sF0,sF3) = join(sF0,join(sF5,meet(sF0,a))),
inference(forward_demodulation,[],[f3924,f1]) ).
fof(f3926,plain,
join(sF0,sF3) = join(sF0,sF5),
inference(forward_demodulation,[],[f3925,f249]) ).
fof(f3927,plain,
sF0 = join(sF0,sF5),
inference(forward_demodulation,[],[f3926,f79]) ).
fof(f3931,plain,
sF5 = meet(sF5,sF0),
inference(superposition,[],[f142,f3927]) ).
fof(f3938,plain,
sF5 = meet(sF0,sF5),
inference(forward_demodulation,[],[f3931,f1]) ).
fof(f3941,plain,
join(meet(z3,sF5),meet(sF0,join(z3,sF5))) = meet(join(z3,sF5),join(meet(sF4,a),sF5)),
inference(superposition,[],[f2949,f3938]) ).
fof(f3951,plain,
! [X0] : join(meet(X0,sF5),meet(a,meet(sF0,join(X0,sF5)))) = meet(join(meet(a,meet(X0,sF0)),sF5),join(meet(a,sF5),X0)),
inference(superposition,[],[f110,f3938]) ).
fof(f3956,plain,
meet(sF5,join(meet(a,sF5),sF0)) = join(sF5,meet(a,sF5)),
inference(superposition,[],[f490,f3938]) ).
fof(f3961,plain,
sF5 = meet(sF5,join(meet(a,sF5),sF0)),
inference(forward_demodulation,[],[f3956,f108]) ).
fof(f3964,plain,
! [X0] : join(meet(X0,sF5),meet(a,meet(sF0,join(X0,sF5)))) = meet(join(meet(a,sF5),X0),join(meet(a,meet(X0,sF0)),sF5)),
inference(forward_demodulation,[],[f3951,f1]) ).
fof(f3971,plain,
join(meet(z3,sF5),meet(sF0,join(z3,sF5))) = meet(join(z3,sF5),join(sF5,meet(sF4,a))),
inference(forward_demodulation,[],[f3941,f3]) ).
fof(f3974,plain,
sF5 = meet(sF5,join(sF0,meet(a,sF5))),
inference(forward_demodulation,[],[f3961,f3]) ).
fof(f3976,plain,
! [X0] : join(meet(X0,sF5),meet(a,meet(sF0,join(X0,sF5)))) = meet(join(meet(a,sF5),X0),join(sF5,meet(a,meet(X0,sF0)))),
inference(forward_demodulation,[],[f3964,f3]) ).
fof(f3981,plain,
join(meet(z3,sF5),meet(sF0,join(z3,sF5))) = meet(join(z3,sF5),sF5),
inference(forward_demodulation,[],[f3971,f3914]) ).
fof(f3985,plain,
! [X0] : join(meet(X0,sF5),meet(a,meet(sF0,join(X0,sF5)))) = meet(join(meet(a,sF5),X0),join(sF5,meet(sF0,meet(a,X0)))),
inference(forward_demodulation,[],[f3976,f178]) ).
fof(f3989,plain,
join(meet(z3,sF5),meet(sF0,join(z3,sF5))) = meet(sF5,join(z3,sF5)),
inference(forward_demodulation,[],[f3981,f1]) ).
fof(f3992,plain,
! [X0] : join(meet(X0,sF5),meet(a,meet(sF0,join(X0,sF5)))) = meet(join(meet(a,sF5),X0),join(sF5,meet(sF0,X0))),
inference(forward_demodulation,[],[f3985,f2867]) ).
fof(f3996,plain,
sF5 = join(meet(z3,sF5),meet(sF0,join(z3,sF5))),
inference(forward_demodulation,[],[f3989,f142]) ).
fof(f3999,plain,
! [X0] : join(meet(X0,sF5),meet(a,meet(sF0,join(X0,sF5)))) = meet(join(sF5,meet(sF0,X0)),join(meet(a,sF5),X0)),
inference(forward_demodulation,[],[f3992,f1]) ).
fof(f4003,plain,
! [X0] : join(meet(X0,sF5),meet(sF0,meet(join(X0,sF5),a))) = meet(join(sF5,meet(sF0,X0)),join(meet(a,sF5),X0)),
inference(forward_demodulation,[],[f3999,f178]) ).
fof(f4006,plain,
! [X0] : join(meet(X0,sF5),meet(sF0,meet(a,join(X0,sF5)))) = meet(join(sF5,meet(sF0,X0)),join(meet(a,sF5),X0)),
inference(forward_demodulation,[],[f4003,f3733]) ).
fof(f4008,plain,
! [X0] : meet(join(sF5,meet(sF0,X0)),join(meet(a,sF5),X0)) = join(meet(X0,sF5),meet(sF0,join(X0,sF5))),
inference(forward_demodulation,[],[f4006,f2867]) ).
fof(f4068,plain,
meet(sF0,z2) = meet(sF2,z2),
inference(superposition,[],[f172,f69]) ).
fof(f4106,plain,
meet(sF0,z2) = meet(z2,sF2),
inference(forward_demodulation,[],[f4068,f1]) ).
fof(f4125,plain,
sF3 = meet(z2,sF2),
inference(forward_demodulation,[],[f4106,f22]) ).
fof(f4808,plain,
! [X2,X0,X1] : join(meet(join(X1,X0),X2),meet(a,meet(X0,join(join(X1,X0),X2)))) = meet(join(X2,meet(a,X0)),join(meet(a,meet(X0,X2)),join(X1,X0))),
inference(superposition,[],[f144,f142]) ).
fof(f5004,plain,
! [X2,X0,X1] : join(meet(join(X1,X0),X2),meet(a,meet(X0,join(join(X1,X0),X2)))) = meet(join(X2,meet(a,X0)),join(X0,join(meet(a,meet(X0,X2)),X1))),
inference(forward_demodulation,[],[f4808,f222]) ).
fof(f5102,plain,
! [X2,X0,X1] : join(meet(join(X1,X0),X2),meet(a,meet(X0,join(join(X1,X0),X2)))) = meet(join(X2,meet(a,X0)),join(X0,X1)),
inference(forward_demodulation,[],[f5004,f2024]) ).
fof(f5188,plain,
! [X2,X0,X1] : join(meet(join(X1,X0),X2),meet(a,meet(X0,join(X1,join(X0,X2))))) = meet(join(X2,meet(a,X0)),join(X0,X1)),
inference(forward_demodulation,[],[f5102,f4]) ).
fof(f5258,plain,
! [X2,X0,X1] : join(meet(join(X1,X0),X2),meet(a,X0)) = meet(join(X2,meet(a,X0)),join(X0,X1)),
inference(forward_demodulation,[],[f5188,f314]) ).
fof(f5319,plain,
! [X2,X0,X1] : join(meet(a,X0),meet(join(X1,X0),X2)) = meet(join(X2,meet(a,X0)),join(X0,X1)),
inference(forward_demodulation,[],[f5258,f3]) ).
fof(f5819,plain,
! [X2,X0,X1] : join(meet(a,X0),meet(join(X0,X1),X2)) = meet(join(X2,meet(a,X0)),join(X0,X1)),
inference(superposition,[],[f5319,f3]) ).
fof(f5844,plain,
! [X0] : meet(join(X0,meet(a,sF5)),join(sF5,sF0)) = join(meet(a,sF5),meet(sF0,X0)),
inference(superposition,[],[f5319,f3927]) ).
fof(f5924,plain,
! [X0] : join(meet(a,sF5),meet(sF0,X0)) = meet(join(sF5,sF0),join(X0,meet(a,sF5))),
inference(forward_demodulation,[],[f5844,f1]) ).
fof(f5953,plain,
! [X2,X0,X1] : join(meet(a,X0),meet(X1,join(X0,X2))) = meet(join(X1,meet(a,X0)),join(X0,X2)),
inference(backward_demodulation,[],[f332,f5819]) ).
fof(f5954,plain,
! [X2,X0,X1] : meet(join(meet(a,X0),X2),join(X0,join(X1,meet(a,meet(X0,X2))))) = meet(join(X2,meet(a,X0)),join(X0,X1)),
inference(backward_demodulation,[],[f228,f5819]) ).
fof(f6005,plain,
! [X0] : join(meet(a,sF5),meet(sF0,X0)) = meet(join(sF0,sF5),join(X0,meet(a,sF5))),
inference(forward_demodulation,[],[f5924,f3]) ).
fof(f6064,plain,
! [X0] : join(meet(a,sF5),meet(sF0,X0)) = meet(sF0,join(X0,meet(a,sF5))),
inference(forward_demodulation,[],[f6005,f3927]) ).
fof(f6270,plain,
! [X0] : join(meet(a,sF0),meet(X0,a)) = meet(join(X0,meet(a,sF0)),a),
inference(superposition,[],[f5953,f75]) ).
fof(f6286,plain,
! [X0,X1] : join(meet(a,X0),join(X0,X1)) = meet(join(join(X0,X1),meet(a,X0)),join(X0,X1)),
inference(superposition,[],[f5953,f51]) ).
fof(f6331,plain,
! [X0,X1] : join(meet(a,X0),join(X0,X1)) = meet(join(X0,X1),join(join(X0,X1),meet(a,X0))),
inference(forward_demodulation,[],[f6286,f1]) ).
fof(f6345,plain,
! [X0] : join(meet(a,sF0),meet(X0,a)) = meet(a,join(X0,meet(a,sF0))),
inference(forward_demodulation,[],[f6270,f1]) ).
fof(f6396,plain,
! [X0,X1] : join(X0,X1) = join(meet(a,X0),join(X0,X1)),
inference(forward_demodulation,[],[f6331,f6]) ).
fof(f6408,plain,
! [X0] : join(meet(sF0,a),meet(X0,a)) = meet(a,join(X0,meet(sF0,a))),
inference(forward_demodulation,[],[f6345,f1]) ).
fof(f6444,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,meet(a,X0))),
inference(forward_demodulation,[],[f6396,f222]) ).
fof(f6455,plain,
! [X0] : meet(a,join(X0,sF0)) = join(sF0,meet(X0,a)),
inference(forward_demodulation,[],[f6408,f2865]) ).
fof(f6493,plain,
! [X0] : meet(a,join(X0,sF0)) = join(sF0,meet(a,X0)),
inference(backward_demodulation,[],[f2917,f6455]) ).
fof(f6541,plain,
join(sF4,meet(a,z3)) = meet(z3,meet(a,join(z3,sF0))),
inference(backward_demodulation,[],[f646,f6493]) ).
fof(f6542,plain,
sF5 = meet(sF5,meet(a,join(sF5,sF0))),
inference(backward_demodulation,[],[f3974,f6493]) ).
fof(f6558,plain,
sF5 = meet(sF5,a),
inference(forward_demodulation,[],[f6542,f291]) ).
fof(f6559,plain,
join(sF4,meet(a,z3)) = meet(z3,a),
inference(forward_demodulation,[],[f6541,f291]) ).
fof(f6591,plain,
sF5 = meet(a,sF5),
inference(forward_demodulation,[],[f6558,f1]) ).
fof(f6592,plain,
meet(a,z3) = join(sF4,meet(a,z3)),
inference(forward_demodulation,[],[f6559,f1]) ).
fof(f6624,plain,
! [X0] : join(meet(X0,sF5),meet(sF0,join(X0,sF5))) = meet(join(sF5,meet(sF0,X0)),join(sF5,X0)),
inference(backward_demodulation,[],[f4008,f6591]) ).
fof(f6626,plain,
! [X0] : meet(sF0,join(X0,sF5)) = join(sF5,meet(sF0,X0)),
inference(backward_demodulation,[],[f6064,f6591]) ).
fof(f6651,plain,
! [X0] : join(meet(X0,sF5),meet(sF0,join(X0,sF5))) = meet(join(sF5,X0),join(sF5,meet(sF0,X0))),
inference(forward_demodulation,[],[f6624,f1]) ).
fof(f6672,plain,
! [X0] : join(meet(X0,sF5),meet(sF0,join(X0,sF5))) = meet(join(sF5,X0),meet(sF0,join(X0,sF5))),
inference(forward_demodulation,[],[f6651,f6626]) ).
fof(f6680,plain,
! [X0] : join(meet(X0,sF5),meet(sF0,join(X0,sF5))) = meet(join(sF5,X0),sF0),
inference(forward_demodulation,[],[f6672,f2181]) ).
fof(f6687,plain,
! [X0] : meet(sF0,join(sF5,X0)) = join(meet(X0,sF5),meet(sF0,join(X0,sF5))),
inference(forward_demodulation,[],[f6680,f1]) ).
fof(f6693,plain,
sF5 = meet(sF0,join(sF5,z3)),
inference(backward_demodulation,[],[f3996,f6687]) ).
fof(f6697,plain,
sF5 = meet(sF0,join(z3,sF5)),
inference(forward_demodulation,[],[f6693,f3]) ).
fof(f6982,plain,
! [X2,X0,X1] : join(X0,join(meet(X0,X1),X2)) = join(X0,join(X2,meet(a,meet(X0,X1)))),
inference(superposition,[],[f209,f6444]) ).
fof(f6997,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(X2,meet(a,meet(X0,X1)))),
inference(forward_demodulation,[],[f6982,f209]) ).
fof(f7040,plain,
! [X2,X0,X1] : meet(join(meet(a,X0),X2),join(X0,X1)) = meet(join(X2,meet(a,X0)),join(X0,X1)),
inference(backward_demodulation,[],[f5954,f6997]) ).
fof(f7321,plain,
! [X0,X1] : join(meet(a,X1),X0) = meet(join(X0,meet(a,X1)),join(X1,join(meet(a,X1),X0))),
inference(superposition,[],[f142,f7040]) ).
fof(f7324,plain,
! [X2,X0,X1] : meet(join(X0,meet(a,X1)),join(X1,X2)) = meet(join(X1,X2),join(meet(a,X1),X0)),
inference(superposition,[],[f1,f7040]) ).
fof(f7414,plain,
! [X0,X1] : join(meet(a,X1),X0) = meet(join(X0,meet(a,X1)),join(X1,X0)),
inference(forward_demodulation,[],[f7321,f210]) ).
fof(f7466,plain,
! [X0,X1] : join(meet(a,X1),X0) = meet(join(X1,X0),join(meet(a,X1),X0)),
inference(forward_demodulation,[],[f7414,f7324]) ).
fof(f8981,plain,
sF4 = meet(sF4,meet(a,z3)),
inference(superposition,[],[f6,f6592]) ).
fof(f8998,plain,
meet(sF4,a) = join(sF4,meet(sF0,join(z3,meet(sF4,a)))),
inference(backward_demodulation,[],[f3546,f8981]) ).
fof(f10979,plain,
join(sF3,z3) = join(sF5,z3),
inference(superposition,[],[f215,f125]) ).
fof(f10990,plain,
join(meet(a,sF4),z3) = meet(z3,join(meet(a,sF4),z3)),
inference(superposition,[],[f7466,f125]) ).
fof(f10991,plain,
z3 = join(meet(a,sF4),z3),
inference(forward_demodulation,[],[f10990,f142]) ).
fof(f10997,plain,
join(sF3,z3) = join(z3,sF5),
inference(forward_demodulation,[],[f10979,f3]) ).
fof(f10998,plain,
z3 = join(z3,meet(a,sF4)),
inference(forward_demodulation,[],[f10991,f3]) ).
fof(f11003,plain,
sF5 = meet(sF0,join(sF3,z3)),
inference(backward_demodulation,[],[f6697,f10997]) ).
fof(f11018,plain,
z3 = join(z3,meet(sF4,a)),
inference(forward_demodulation,[],[f10998,f1]) ).
fof(f11024,plain,
meet(sF4,a) = join(sF4,meet(sF0,z3)),
inference(backward_demodulation,[],[f8998,f11018]) ).
fof(f11026,plain,
meet(sF4,a) = join(sF4,sF4),
inference(forward_demodulation,[],[f11024,f24]) ).
fof(f11028,plain,
sF4 = meet(sF4,a),
inference(forward_demodulation,[],[f11026,f48]) ).
fof(f11056,plain,
join(z3,sF2) = meet(join(z3,sF2),join(sF1,sF4)),
inference(backward_demodulation,[],[f3535,f11028]) ).
fof(f11115,plain,
join(z3,sF2) = meet(join(sF1,sF4),join(z3,sF2)),
inference(forward_demodulation,[],[f11056,f1]) ).
fof(f13184,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f210,f3]) ).
fof(f13270,plain,
join(sF3,z3) = join(sF3,join(z3,sF2)),
inference(backward_demodulation,[],[f3880,f13184]) ).
fof(f14839,plain,
! [X0] : join(sF2,X0) = join(sF2,join(sF3,X0)),
inference(superposition,[],[f210,f4125]) ).
fof(f14850,plain,
! [X0] : join(sF2,X0) = join(sF3,join(X0,sF2)),
inference(forward_demodulation,[],[f14839,f222]) ).
fof(f14870,plain,
join(sF3,z3) = join(sF2,z3),
inference(backward_demodulation,[],[f13270,f14850]) ).
fof(f14884,plain,
join(z3,sF2) = join(sF3,z3),
inference(forward_demodulation,[],[f14870,f3]) ).
fof(f14899,plain,
join(sF3,z3) = meet(join(sF1,sF4),join(sF3,z3)),
inference(backward_demodulation,[],[f11115,f14884]) ).
fof(f15078,plain,
sF2 = meet(sF2,join(sF3,z3)),
inference(superposition,[],[f142,f14884]) ).
fof(f15445,plain,
join(z2,z3) = join(sF1,sF4),
inference(superposition,[],[f2713,f125]) ).
fof(f15473,plain,
sF1 = join(sF1,sF4),
inference(forward_demodulation,[],[f15445,f18]) ).
fof(f15480,plain,
join(sF3,z3) = meet(sF1,join(sF3,z3)),
inference(backward_demodulation,[],[f14899,f15473]) ).
fof(f15508,plain,
meet(sF0,join(sF3,z3)) = meet(sF2,join(sF3,z3)),
inference(superposition,[],[f172,f15480]) ).
fof(f15549,plain,
sF2 = meet(sF0,join(sF3,z3)),
inference(forward_demodulation,[],[f15508,f15078]) ).
fof(f15564,plain,
sF2 = sF5,
inference(backward_demodulation,[],[f11003,f15549]) ).
fof(f15576,plain,
$false,
inference(forward_subsumption_resolution,[],[f15564,f27]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT399-2 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 % Computer : n003.cluster.edu
% 0.11/0.40 % Model : x86_64 x86_64
% 0.11/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.40 % Memory : 8046.5625MB
% 0.11/0.40 % OS : Linux 6.8.0-71-generic
% 0.11/0.40 % CPULimit : 300
% 0.11/0.40 % WCLimit : 300
% 0.11/0.40 % DateTime : Sun Sep 27 15:16:56 UTC 2026
% 0.11/0.40 % CPUTime :
% 0.11/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 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
% 17.20/3.09 % (683304)Detected a unit-equality problem, will run specialized UEQ schedule.
% 17.20/3.09 % (683314)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=2104222849:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 17.20/3.09 % (683311)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=3410261469:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 17.20/3.09 % (683315)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=369753151:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 17.20/3.09 % (683310)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=2698414573:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 17.20/3.09 % (683312)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2520448995:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 17.20/3.09 % (683313)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2466825335:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 17.20/3.09 % (683309)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=1894150100:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 17.20/3.09 % (683312)Instruction limit reached!
% 17.20/3.09 % (683312)------------------------------
% 17.20/3.09 % (683312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.20/3.09 % (683312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.20/3.09 % (683312)CaDiCaL version: 2.1.3
% 17.20/3.09 % (683312)Termination reason: Instruction limit
% 17.20/3.09 % (683312)Termination phase: Saturation
% 17.20/3.09 % (683312)Time elapsed: 0.079 s
% 17.20/3.09 % (683312)Peak memory usage: 89 MB
% 17.20/3.09 % (683312)Instructions burned: 137 (million)
% 17.20/3.09 % (683314)Instruction limit reached!
% 17.20/3.09 % (683314)------------------------------
% 17.20/3.09 % (683314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.20/3.09 % (683314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.20/3.09 % (683314)CaDiCaL version: 2.1.3
% 17.20/3.09 % (683314)Termination reason: Instruction limit
% 17.20/3.09 % (683314)Termination phase: Saturation
% 17.20/3.09 % (683314)Time elapsed: 0.089 s
% 17.20/3.09 % (683314)Peak memory usage: 90 MB
% 17.20/3.09 % (683314)Instructions burned: 260 (million)
% 17.20/3.09 % (683313)Instruction limit reached!
% 17.20/3.09 % (683313)------------------------------
% 17.20/3.09 % (683313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.20/3.09 % (683313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.20/3.09 % (683313)CaDiCaL version: 2.1.3
% 17.20/3.09 % (683313)Termination reason: Instruction limit
% 17.20/3.09 % (683313)Termination phase: Saturation
% 17.20/3.09 % (683313)Time elapsed: 0.105 s
% 17.20/3.09 % (683313)Peak memory usage: 89 MB
% 17.20/3.09 % (683313)Instructions burned: 181 (million)
% 17.20/3.09 % (683324)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2465740520:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 17.20/3.09 % (683323)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=193085902:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 17.20/3.09 % (683325)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=3359605567:i=215:ep=RSTC_2997 on theBenchmark for (2997ds/215Mi)
% 17.20/3.09 % (683325)Instruction limit reached!
% 17.20/3.09 % (683325)------------------------------
% 17.20/3.09 % (683325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.20/3.09 % (683325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.20/3.09 % (683325)CaDiCaL version: 2.1.3
% 17.20/3.09 % (683325)Termination reason: Instruction limit
% 17.20/3.09 % (683325)Termination phase: Saturation
% 17.20/3.09 % (683325)Time elapsed: 0.115 s
% 17.20/3.09 % (683325)Peak memory usage: 91 MB
% 17.20/3.09 % (683325)Instructions burned: 217 (million)
% 17.20/3.09 % (683329)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=466040142:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2994 on theBenchmark for (2994ds/317Mi)
% 17.20/3.09 % (683315)Instruction limit reached!
% 17.20/3.09 % (683315)------------------------------
% 17.20/3.09 % (683315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.20/3.09 % (683315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.20/3.09 % (683315)CaDiCaL version: 2.1.3
% 17.20/3.09 % (683315)Termination reason: Instruction limit
% 17.20/3.09 % (683315)Termination phase: Saturation
% 17.20/3.09 % (683315)Time elapsed: 0.638 s
% 17.20/3.09 % (683315)Peak memory usage: 97 MB
% 17.20/3.09 % (683315)Instructions burned: 1187 (million)
% 17.20/3.09 % (683329)Instruction limit reached!
% 17.20/3.09 % (683329)------------------------------
% 17.20/3.09 % (683329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.20/3.09 % (683329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.20/3.09 % (683329)CaDiCaL version: 2.1.3
% 17.20/3.09 % (683329)Termination reason: Instruction limit
% 17.20/3.09 % (683329)Termination phase: Saturation
% 17.20/3.09 % (683329)Time elapsed: 0.185 s
% 17.20/3.09 % (683329)Peak memory usage: 91 MB
% 17.20/3.09 % (683329)Instructions burned: 318 (million)
% 17.20/3.09 % (683331)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=3835115617:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/12125Mi)
% 17.20/3.09 % (683332)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=2156580324:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2991 on theBenchmark for (2991ds/2836Mi)
% 17.20/3.09 % (683323)Instruction limit reached!
% 17.20/3.09 % (683323)------------------------------
% 17.20/3.09 % (683323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.20/3.09 % (683323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.20/3.09 % (683323)CaDiCaL version: 2.1.3
% 17.20/3.09 % (683323)Termination reason: Instruction limit
% 17.20/3.09 % (683323)Termination phase: Saturation
% 17.20/3.09 % (683323)Time elapsed: 1.319 s
% 17.20/3.09 % (683323)Peak memory usage: 141 MB
% 17.20/3.09 % (683323)Instructions burned: 2052 (million)
% 17.20/3.09 % (683335)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=4004897748:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2982 on theBenchmark for (2982ds/14534Mi)
% 17.20/3.09 % (683311)First to succeed.
% 17.20/3.09 % (683311)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-683304"
% 17.20/3.09 % (683311)Refutation found. Thanks to Tanya!
% 17.20/3.09 % SZS status Unsatisfiable for theBenchmark
% 17.20/3.09 % SZS output start Proof for theBenchmark
% See solution above
% 17.73/3.29 % (683311)------------------------------
% 17.73/3.29 % (683311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.29 % (683311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.29 % (683311)CaDiCaL version: 2.1.3
% 17.73/3.29 % (683311)Termination reason: Refutation
% 17.73/3.29 % (683311)Time elapsed: 2.041 s
% 17.73/3.29 % (683311)Peak memory usage: 148 MB
% 17.73/3.29 % (683311)Instructions burned: 3296 (million)
% 17.73/3.29 % (683311)------------------------------
% 17.73/3.29 % (683311)------------------------------
% 17.73/3.29 % (683304)Success in time 2.459 s
% 17.73/3.29 % Vampire exiting
%------------------------------------------------------------------------------