%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT141-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.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:46:03 AM UTC 2026
% Result : Unsatisfiable 17.25s 3.11s
% Output : Refutation 17.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 77
% Number of leaves : 16
% Syntax : Number of formulae : 277 ( 277 unt; 7 def)
% Number of atoms : 277 ( 276 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 327 ( 327 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : meet(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_meet) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_meet) ).
fof(f8,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f9,axiom,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X1,join(X0,meet(X1,X2))),meet(X2,join(X0,X1)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H21) ).
fof(f10,negated_conjecture,
meet(a,join(b,meet(a,c))) != meet(a,join(meet(a,join(b,meet(a,c))),meet(c,join(a,b)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_H6) ).
fof(f11,definition,
sF0 = meet(a,c),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f12,plain,
meet(a,c) = sF0,
inference(reorient_equations,[],[f11]) ).
fof(f13,definition,
sF1 = join(b,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f14,plain,
join(b,sF0) = sF1,
inference(reorient_equations,[],[f13]) ).
fof(f15,definition,
sF2 = meet(a,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f16,plain,
meet(a,sF1) = sF2,
inference(reorient_equations,[],[f15]) ).
fof(f17,definition,
sF3 = join(a,b),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f18,plain,
join(a,b) = sF3,
inference(reorient_equations,[],[f17]) ).
fof(f19,definition,
sF4 = meet(c,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f20,plain,
meet(c,sF3) = sF4,
inference(reorient_equations,[],[f19]) ).
fof(f21,definition,
sF5 = join(sF2,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f22,plain,
join(sF2,sF4) = sF5,
inference(reorient_equations,[],[f21]) ).
fof(f23,definition,
sF6 = meet(a,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f24,plain,
meet(a,sF5) = sF6,
inference(reorient_equations,[],[f23]) ).
fof(f25,plain,
sF2 != sF6,
inference(definition_folding,[],[f10,f24,f22,f20,f18,f16,f14,f12,f16,f14,f12]) ).
fof(f26,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X2,join(X0,X1)),meet(X1,join(X0,meet(X1,X2))))),
inference(backward_demodulation,[],[f9,f6]) ).
fof(f27,plain,
sF1 = join(sF0,b),
inference(forward_demodulation,[],[f14,f6]) ).
fof(f28,plain,
sF2 = meet(sF1,a),
inference(forward_demodulation,[],[f16,f5]) ).
fof(f29,plain,
sF4 = meet(sF3,c),
inference(forward_demodulation,[],[f20,f5]) ).
fof(f30,plain,
sF5 = join(sF4,sF2),
inference(forward_demodulation,[],[f22,f6]) ).
fof(f31,plain,
sF6 = meet(sF5,a),
inference(forward_demodulation,[],[f24,f5]) ).
fof(f66,plain,
sF4 = meet(sF4,sF5),
inference(superposition,[],[f3,f30]) ).
fof(f69,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,join(X0,X2))) = meet(X1,join(meet(join(X0,X2),join(X1,X0)),meet(X0,join(X1,X0)))),
inference(superposition,[],[f26,f3]) ).
fof(f70,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,join(X0,X2))) = meet(X1,join(meet(X0,join(X1,X0)),meet(join(X0,X2),join(X1,X0)))),
inference(forward_demodulation,[],[f69,f6]) ).
fof(f77,plain,
! [X0] : join(meet(X0,a),meet(X0,c)) = meet(X0,join(meet(c,join(X0,a)),meet(a,join(X0,sF0)))),
inference(superposition,[],[f26,f12]) ).
fof(f78,plain,
! [X0] : join(meet(X0,a),meet(X0,c)) = meet(X0,join(meet(a,join(X0,sF0)),meet(c,join(X0,a)))),
inference(forward_demodulation,[],[f77,f6]) ).
fof(f79,plain,
sF0 = meet(sF0,sF1),
inference(superposition,[],[f3,f27]) ).
fof(f81,plain,
a = meet(a,sF3),
inference(superposition,[],[f3,f18]) ).
fof(f83,plain,
a = meet(sF3,a),
inference(forward_demodulation,[],[f81,f5]) ).
fof(f91,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(meet(X0,X1),join(X0,meet(meet(X0,X1),X2))))),
inference(superposition,[],[f26,f4]) ).
fof(f92,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X0,meet(X1,join(X0,meet(meet(X0,X1),X2)))))),
inference(forward_demodulation,[],[f91,f7]) ).
fof(f95,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X0,meet(X1,join(X0,meet(X0,meet(X1,X2))))))),
inference(forward_demodulation,[],[f92,f7]) ).
fof(f97,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X0,meet(X1,X0)))),
inference(forward_demodulation,[],[f95,f4]) ).
fof(f107,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f112,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f113,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,X2)) = meet(X1,join(meet(X2,join(X0,X1)),meet(X0,join(X1,meet(X0,X2))))),
inference(superposition,[],[f26,f6]) ).
fof(f114,plain,
! [X2,X0,X1] : join(meet(X2,X0),meet(X2,X1)) = meet(X2,join(meet(X1,join(X2,X0)),meet(X0,join(meet(X0,X1),X2)))),
inference(superposition,[],[f26,f6]) ).
fof(f115,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,join(X0,X2))) = meet(X1,join(X0,meet(join(X0,X2),join(X1,X0)))),
inference(backward_demodulation,[],[f70,f112]) ).
fof(f116,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f112,f4]) ).
fof(f121,plain,
sF2 = meet(sF2,sF5),
inference(superposition,[],[f112,f30]) ).
fof(f127,plain,
sF2 = meet(sF5,sF2),
inference(forward_demodulation,[],[f121,f5]) ).
fof(f130,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f116,f7]) ).
fof(f132,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X0,X1))),
inference(backward_demodulation,[],[f97,f130]) ).
fof(f134,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f135,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f112]) ).
fof(f137,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)),
inference(superposition,[],[f7,f5]) ).
fof(f139,plain,
! [X0] : meet(sF0,X0) = meet(a,meet(c,X0)),
inference(superposition,[],[f7,f12]) ).
fof(f140,plain,
! [X0] : meet(sF2,X0) = meet(sF1,meet(a,X0)),
inference(superposition,[],[f7,f28]) ).
fof(f141,plain,
! [X0] : meet(sF4,X0) = meet(sF3,meet(c,X0)),
inference(superposition,[],[f7,f29]) ).
fof(f142,plain,
! [X0] : meet(sF5,meet(a,X0)) = meet(sF6,X0),
inference(superposition,[],[f7,f31]) ).
fof(f154,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f156,plain,
! [X2,X3,X0,X1] : join(meet(X3,meet(X0,X1)),meet(X3,X2)) = meet(X3,join(meet(X2,join(X3,meet(X0,X1))),meet(meet(X0,X1),join(X3,meet(X0,meet(X1,X2)))))),
inference(superposition,[],[f26,f7]) ).
fof(f157,plain,
! [X2,X3,X0,X1] : join(meet(X3,meet(X0,X1)),meet(X3,X2)) = meet(X3,join(meet(X2,join(X3,meet(X0,X1))),meet(X0,meet(X1,join(X3,meet(X0,meet(X1,X2))))))),
inference(forward_demodulation,[],[f156,f7]) ).
fof(f168,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f8,f4]) ).
fof(f172,plain,
! [X0] : join(a,join(b,X0)) = join(sF3,X0),
inference(superposition,[],[f8,f18]) ).
fof(f174,plain,
! [X0] : join(sF4,join(sF2,X0)) = join(sF5,X0),
inference(superposition,[],[f8,f30]) ).
fof(f180,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f202,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f107]) ).
fof(f229,plain,
! [X0] : join(sF3,X0) = join(a,join(X0,b)),
inference(superposition,[],[f172,f6]) ).
fof(f253,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(superposition,[],[f134,f107]) ).
fof(f257,plain,
! [X0] : meet(a,X0) = meet(a,meet(sF3,X0)),
inference(superposition,[],[f134,f18]) ).
fof(f283,plain,
! [X0] : meet(a,X0) = meet(sF3,meet(X0,a)),
inference(forward_demodulation,[],[f257,f154]) ).
fof(f284,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X0,X1))),
inference(backward_demodulation,[],[f132,f253]) ).
fof(f294,plain,
! [X0] : meet(sF0,X0) = meet(a,meet(X0,c)),
inference(superposition,[],[f139,f5]) ).
fof(f310,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(superposition,[],[f168,f112]) ).
fof(f349,plain,
meet(sF6,c) = meet(sF5,sF0),
inference(superposition,[],[f142,f12]) ).
fof(f355,plain,
! [X0] : meet(sF6,X0) = meet(sF5,meet(X0,a)),
inference(superposition,[],[f142,f5]) ).
fof(f368,plain,
meet(sF6,c) = meet(sF0,sF5),
inference(forward_demodulation,[],[f349,f5]) ).
fof(f372,plain,
meet(sF0,sF5) = meet(c,sF6),
inference(forward_demodulation,[],[f368,f5]) ).
fof(f373,plain,
meet(sF2,c) = meet(sF1,sF0),
inference(superposition,[],[f140,f12]) ).
fof(f379,plain,
! [X0] : meet(sF2,X0) = meet(sF1,meet(X0,a)),
inference(superposition,[],[f140,f5]) ).
fof(f392,plain,
meet(sF0,sF1) = meet(sF2,c),
inference(forward_demodulation,[],[f373,f5]) ).
fof(f395,plain,
sF0 = meet(sF2,c),
inference(forward_demodulation,[],[f392,f79]) ).
fof(f396,plain,
sF2 = join(sF2,sF0),
inference(superposition,[],[f4,f395]) ).
fof(f405,plain,
sF2 = join(sF0,sF2),
inference(forward_demodulation,[],[f396,f6]) ).
fof(f406,plain,
sF0 = meet(sF0,sF2),
inference(superposition,[],[f3,f405]) ).
fof(f564,plain,
! [X2,X0,X1] : meet(X2,X0) = join(meet(X2,X0),meet(X0,meet(X1,X2))),
inference(superposition,[],[f107,f154]) ).
fof(f584,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,meet(X2,X3))) = meet(X2,meet(X3,meet(X0,X1))),
inference(superposition,[],[f7,f154]) ).
fof(f830,plain,
! [X2,X0,X1] : join(meet(meet(meet(X0,X1),X2),X0),meet(meet(meet(X0,X1),X2),X1)) = meet(meet(meet(X0,X1),X2),join(meet(X1,join(meet(meet(X0,X1),X2),X0)),meet(X0,meet(X0,X1)))),
inference(superposition,[],[f114,f4]) ).
fof(f877,plain,
! [X2,X0,X1] : join(meet(meet(meet(X0,X1),X2),X0),meet(meet(meet(X0,X1),X2),X1)) = meet(meet(X0,X1),meet(X2,join(meet(X1,join(meet(meet(X0,X1),X2),X0)),meet(X0,meet(X0,X1))))),
inference(forward_demodulation,[],[f830,f7]) ).
fof(f924,plain,
! [X2,X0,X1] : join(meet(meet(meet(X0,X1),X2),X0),meet(meet(meet(X0,X1),X2),X1)) = meet(X0,meet(X1,meet(X2,join(meet(X1,join(meet(meet(X0,X1),X2),X0)),meet(X0,meet(X0,X1)))))),
inference(forward_demodulation,[],[f877,f7]) ).
fof(f950,plain,
! [X2,X0,X1] : join(meet(meet(meet(X0,X1),X2),X0),meet(meet(meet(X0,X1),X2),X1)) = meet(X0,meet(X1,meet(X2,join(meet(X0,meet(X0,X1)),meet(X1,join(meet(meet(X0,X1),X2),X0)))))),
inference(forward_demodulation,[],[f924,f6]) ).
fof(f967,plain,
! [X2,X0,X1] : join(meet(meet(meet(X0,X1),X2),X0),meet(meet(meet(X0,X1),X2),X1)) = meet(X0,meet(X1,meet(X2,join(meet(X0,meet(X0,X1)),meet(X1,join(X0,meet(meet(X0,X1),X2))))))),
inference(forward_demodulation,[],[f950,f6]) ).
fof(f980,plain,
! [X2,X0,X1] : join(meet(meet(X0,meet(X1,X2)),X0),meet(meet(X0,meet(X1,X2)),X1)) = meet(X0,meet(X1,meet(X2,join(meet(X0,meet(X0,X1)),meet(X1,join(X0,meet(X0,meet(X1,X2)))))))),
inference(forward_demodulation,[],[f967,f7]) ).
fof(f991,plain,
! [X2,X0,X1] : join(meet(meet(X0,meet(X1,X2)),X0),meet(meet(X0,meet(X1,X2)),X1)) = meet(X0,meet(X1,meet(X2,join(meet(X0,meet(X0,X1)),meet(X1,X0))))),
inference(forward_demodulation,[],[f980,f4]) ).
fof(f1002,plain,
! [X2,X0,X1] : join(meet(meet(X0,meet(X1,X2)),X0),meet(meet(X0,meet(X1,X2)),X1)) = meet(X0,meet(X1,meet(X2,join(meet(X1,X0),meet(X0,meet(X0,X1)))))),
inference(forward_demodulation,[],[f991,f6]) ).
fof(f1012,plain,
! [X2,X0,X1] : join(meet(meet(X0,meet(X1,X2)),X0),meet(meet(X0,meet(X1,X2)),X1)) = meet(X0,meet(X1,meet(X2,meet(X1,X0)))),
inference(forward_demodulation,[],[f1002,f564]) ).
fof(f1021,plain,
! [X2,X0,X1] : meet(X0,meet(X1,meet(X2,meet(X1,X0)))) = join(meet(meet(X0,meet(X1,X2)),X0),meet(X0,meet(meet(X1,X2),X1))),
inference(forward_demodulation,[],[f1012,f7]) ).
fof(f1030,plain,
! [X2,X0,X1] : meet(X0,meet(X1,meet(X2,meet(X1,X0)))) = join(meet(meet(X0,meet(X1,X2)),X0),meet(X0,meet(X1,meet(X2,X1)))),
inference(forward_demodulation,[],[f1021,f7]) ).
fof(f1039,plain,
! [X2,X0,X1] : meet(X0,meet(X1,meet(X2,meet(X1,X0)))) = join(meet(meet(X0,meet(X1,X2)),X0),meet(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f1030,f130]) ).
fof(f1048,plain,
! [X2,X0,X1] : meet(X0,meet(X1,meet(X2,meet(X1,X0)))) = join(meet(X0,meet(X1,X2)),meet(meet(X0,meet(X1,X2)),X0)),
inference(forward_demodulation,[],[f1039,f6]) ).
fof(f1056,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X1,meet(X2,meet(X1,X0)))),
inference(forward_demodulation,[],[f1048,f4]) ).
fof(f1072,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),meet(X2,X3)) = meet(meet(X0,X1),meet(X2,meet(X3,meet(X0,meet(X1,X2))))),
inference(superposition,[],[f1056,f154]) ).
fof(f1090,plain,
! [X2,X0,X1] : meet(X1,meet(X0,X2)) = meet(X1,meet(X0,meet(X0,meet(X1,X2)))),
inference(superposition,[],[f1056,f154]) ).
fof(f1125,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),meet(X2,X3)) = meet(X0,meet(X1,meet(X2,meet(X3,meet(X2,meet(X0,X1)))))),
inference(superposition,[],[f7,f1056]) ).
fof(f1144,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,meet(X2,X3))) = meet(X0,meet(X1,meet(X2,meet(X3,meet(X2,meet(X0,X1)))))),
inference(forward_demodulation,[],[f1125,f7]) ).
fof(f1175,plain,
! [X2,X0,X1] : meet(X1,meet(X0,X2)) = meet(X1,meet(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f1090,f253]) ).
fof(f1193,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),meet(X2,X3)) = meet(X0,meet(X1,meet(X2,meet(X3,meet(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f1072,f7]) ).
fof(f1228,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X1,meet(X2,X0))),
inference(backward_demodulation,[],[f1056,f1175]) ).
fof(f1230,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,meet(X2,X3))) = meet(X0,meet(X1,meet(X2,meet(X3,meet(X0,X1))))),
inference(backward_demodulation,[],[f1144,f1175]) ).
fof(f1253,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,meet(X2,X3))) = meet(X0,meet(X1,meet(X2,meet(X3,meet(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f1193,f7]) ).
fof(f1297,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,meet(X2,X3))) = meet(X0,meet(X1,meet(X2,meet(X3,X0)))),
inference(forward_demodulation,[],[f1253,f1230]) ).
fof(f2206,plain,
meet(sF4,sF6) = meet(sF3,meet(sF0,sF5)),
inference(superposition,[],[f141,f372]) ).
fof(f2222,plain,
meet(sF4,sF6) = meet(sF0,meet(sF5,sF3)),
inference(forward_demodulation,[],[f2206,f154]) ).
fof(f2223,plain,
meet(sF4,sF6) = meet(sF0,meet(sF3,sF5)),
inference(forward_demodulation,[],[f2222,f5]) ).
fof(f2314,plain,
meet(sF0,sF2) = meet(a,sF0),
inference(superposition,[],[f294,f395]) ).
fof(f2315,plain,
meet(a,sF4) = meet(sF0,sF3),
inference(superposition,[],[f294,f29]) ).
fof(f2345,plain,
meet(sF0,sF3) = meet(sF4,a),
inference(forward_demodulation,[],[f2315,f5]) ).
fof(f2346,plain,
meet(sF0,sF2) = meet(sF0,a),
inference(forward_demodulation,[],[f2314,f5]) ).
fof(f2358,plain,
sF0 = meet(sF0,a),
inference(forward_demodulation,[],[f2346,f406]) ).
fof(f2383,plain,
! [X0] : meet(sF4,meet(a,X0)) = meet(meet(sF0,sF3),X0),
inference(superposition,[],[f7,f2345]) ).
fof(f2394,plain,
! [X0] : meet(sF4,meet(a,X0)) = meet(sF0,meet(sF3,X0)),
inference(forward_demodulation,[],[f2383,f7]) ).
fof(f2413,plain,
! [X0] : meet(sF0,X0) = meet(a,meet(sF0,X0)),
inference(superposition,[],[f137,f2358]) ).
fof(f2468,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X0,meet(X1,join(meet(X1,X0),X2))),
inference(superposition,[],[f3,f137]) ).
fof(f2511,plain,
! [X0] : meet(sF0,X0) = meet(sF0,meet(X0,a)),
inference(forward_demodulation,[],[f2413,f154]) ).
fof(f2592,plain,
join(sF3,sF0) = join(a,sF1),
inference(superposition,[],[f229,f27]) ).
fof(f2616,plain,
join(sF3,sF0) = join(sF1,a),
inference(forward_demodulation,[],[f2592,f6]) ).
fof(f2623,plain,
join(sF1,a) = join(sF0,sF3),
inference(forward_demodulation,[],[f2616,f6]) ).
fof(f2631,plain,
! [X0] : join(meet(a,sF1),meet(a,X0)) = meet(a,join(meet(X0,join(sF0,sF3)),meet(sF1,join(a,meet(sF1,X0))))),
inference(superposition,[],[f113,f2623]) ).
fof(f2633,plain,
! [X0] : meet(sF1,X0) = meet(sF1,meet(join(sF0,sF3),X0)),
inference(superposition,[],[f134,f2623]) ).
fof(f2638,plain,
! [X0] : meet(a,join(meet(X0,join(sF0,sF3)),meet(sF1,join(a,meet(sF1,X0))))) = join(meet(sF1,a),meet(a,X0)),
inference(forward_demodulation,[],[f2631,f5]) ).
fof(f2643,plain,
! [X0] : meet(a,join(meet(X0,join(sF0,sF3)),meet(sF1,join(a,meet(sF1,X0))))) = join(sF2,meet(a,X0)),
inference(forward_demodulation,[],[f2638,f28]) ).
fof(f2697,plain,
! [X0] : join(meet(X0,sF3),meet(X0,a)) = meet(X0,join(meet(a,join(X0,sF3)),meet(sF3,join(a,X0)))),
inference(superposition,[],[f114,f83]) ).
fof(f2699,plain,
! [X0] : meet(X0,a) = meet(sF3,meet(a,X0)),
inference(superposition,[],[f154,f83]) ).
fof(f2704,plain,
! [X0] : join(meet(X0,sF3),meet(X0,a)) = meet(X0,join(meet(sF3,join(a,X0)),meet(a,join(X0,sF3)))),
inference(forward_demodulation,[],[f2697,f6]) ).
fof(f2845,plain,
meet(sF2,sF5) = meet(sF1,sF6),
inference(superposition,[],[f379,f31]) ).
fof(f2873,plain,
meet(sF5,sF2) = meet(sF1,sF6),
inference(forward_demodulation,[],[f2845,f5]) ).
fof(f2888,plain,
sF2 = meet(sF1,sF6),
inference(forward_demodulation,[],[f2873,f127]) ).
fof(f2924,plain,
sF6 = join(sF6,sF2),
inference(superposition,[],[f107,f2888]) ).
fof(f2937,plain,
sF6 = join(sF2,sF6),
inference(forward_demodulation,[],[f2924,f6]) ).
fof(f3004,plain,
sF1 = join(sF1,sF0),
inference(superposition,[],[f107,f79]) ).
fof(f3017,plain,
sF1 = join(sF0,sF1),
inference(forward_demodulation,[],[f3004,f6]) ).
fof(f3041,plain,
! [X0] : meet(a,meet(X0,sF1)) = meet(a,meet(X0,sF2)),
inference(superposition,[],[f1228,f28]) ).
fof(f3047,plain,
! [X0] : meet(c,meet(X0,sF3)) = meet(c,meet(X0,sF4)),
inference(superposition,[],[f1228,f29]) ).
fof(f3050,plain,
! [X0] : meet(a,meet(X0,sF4)) = meet(a,meet(X0,meet(sF0,sF3))),
inference(superposition,[],[f1228,f2345]) ).
fof(f3146,plain,
! [X0] : meet(a,meet(X0,sF4)) = meet(sF0,meet(sF3,meet(a,X0))),
inference(forward_demodulation,[],[f3050,f584]) ).
fof(f3149,plain,
! [X0] : meet(c,meet(X0,sF3)) = meet(sF4,meet(c,X0)),
inference(forward_demodulation,[],[f3047,f154]) ).
fof(f3155,plain,
! [X0] : meet(sF1,meet(a,X0)) = meet(a,meet(X0,sF2)),
inference(forward_demodulation,[],[f3041,f154]) ).
fof(f3201,plain,
! [X0] : meet(a,meet(X0,sF4)) = meet(sF0,meet(X0,a)),
inference(forward_demodulation,[],[f3146,f2699]) ).
fof(f3204,plain,
! [X0] : meet(sF3,meet(c,X0)) = meet(sF4,meet(c,X0)),
inference(forward_demodulation,[],[f3149,f154]) ).
fof(f3210,plain,
! [X0] : meet(sF2,X0) = meet(a,meet(X0,sF2)),
inference(forward_demodulation,[],[f3155,f140]) ).
fof(f3237,plain,
! [X0] : meet(sF0,X0) = meet(a,meet(X0,sF4)),
inference(forward_demodulation,[],[f3201,f2511]) ).
fof(f3238,plain,
! [X0] : meet(sF4,X0) = meet(sF4,meet(c,X0)),
inference(forward_demodulation,[],[f3204,f141]) ).
fof(f3262,plain,
! [X0] : meet(sF0,X0) = meet(sF4,meet(a,X0)),
inference(forward_demodulation,[],[f3237,f154]) ).
fof(f3275,plain,
! [X0] : meet(sF0,X0) = meet(sF0,meet(sF3,X0)),
inference(backward_demodulation,[],[f2394,f3262]) ).
fof(f3284,plain,
meet(sF0,sF5) = meet(sF4,sF6),
inference(backward_demodulation,[],[f2223,f3275]) ).
fof(f3319,plain,
! [X0] : meet(sF4,X0) = meet(sF5,meet(sF4,X0)),
inference(superposition,[],[f137,f66]) ).
fof(f3324,plain,
! [X0] : meet(sF4,X0) = meet(sF4,meet(X0,sF5)),
inference(forward_demodulation,[],[f3319,f154]) ).
fof(f3444,plain,
meet(sF4,sF6) = meet(sF4,meet(sF0,sF5)),
inference(superposition,[],[f3238,f372]) ).
fof(f3497,plain,
meet(sF4,sF0) = meet(sF4,sF6),
inference(forward_demodulation,[],[f3444,f3324]) ).
fof(f3508,plain,
meet(sF0,sF5) = meet(sF4,sF0),
inference(forward_demodulation,[],[f3497,f3284]) ).
fof(f3512,plain,
meet(sF0,sF5) = meet(sF0,sF4),
inference(forward_demodulation,[],[f3508,f5]) ).
fof(f3514,plain,
meet(c,sF6) = meet(sF0,sF4),
inference(backward_demodulation,[],[f372,f3512]) ).
fof(f3523,plain,
meet(sF0,sF4) = meet(sF4,sF6),
inference(backward_demodulation,[],[f3284,f3512]) ).
fof(f3535,plain,
meet(sF0,sF6) = meet(a,meet(sF0,sF4)),
inference(superposition,[],[f139,f3514]) ).
fof(f3553,plain,
meet(sF0,sF6) = meet(sF4,meet(a,sF0)),
inference(forward_demodulation,[],[f3535,f154]) ).
fof(f3559,plain,
meet(sF0,sF0) = meet(sF0,sF6),
inference(forward_demodulation,[],[f3553,f3262]) ).
fof(f3566,plain,
sF0 = meet(sF0,sF6),
inference(forward_demodulation,[],[f3559,f1]) ).
fof(f3671,plain,
meet(sF5,sF0) = meet(sF6,sF0),
inference(superposition,[],[f355,f2358]) ).
fof(f3710,plain,
meet(sF5,sF0) = meet(sF0,sF6),
inference(forward_demodulation,[],[f3671,f5]) ).
fof(f3727,plain,
sF0 = meet(sF5,sF0),
inference(forward_demodulation,[],[f3710,f3566]) ).
fof(f3735,plain,
sF0 = meet(sF0,sF5),
inference(forward_demodulation,[],[f3727,f5]) ).
fof(f3738,plain,
sF0 = meet(sF0,sF4),
inference(backward_demodulation,[],[f3512,f3735]) ).
fof(f3741,plain,
sF0 = meet(c,sF6),
inference(backward_demodulation,[],[f3514,f3738]) ).
fof(f3749,plain,
sF0 = meet(sF4,sF6),
inference(backward_demodulation,[],[f3523,f3738]) ).
fof(f3865,plain,
meet(sF4,sF6) = meet(sF3,sF0),
inference(superposition,[],[f141,f3741]) ).
fof(f3890,plain,
meet(sF4,sF6) = meet(sF0,sF3),
inference(forward_demodulation,[],[f3865,f5]) ).
fof(f3894,plain,
sF0 = meet(sF0,sF3),
inference(forward_demodulation,[],[f3890,f3749]) ).
fof(f4002,plain,
sF3 = join(sF3,sF0),
inference(superposition,[],[f107,f3894]) ).
fof(f4015,plain,
sF3 = join(sF0,sF3),
inference(forward_demodulation,[],[f4002,f6]) ).
fof(f4019,plain,
sF3 = join(sF1,a),
inference(backward_demodulation,[],[f2623,f4015]) ).
fof(f4022,plain,
! [X0] : meet(sF1,X0) = meet(sF1,meet(sF3,X0)),
inference(backward_demodulation,[],[f2633,f4015]) ).
fof(f4026,plain,
! [X0] : join(sF2,meet(a,X0)) = meet(a,join(meet(X0,sF3),meet(sF1,join(a,meet(sF1,X0))))),
inference(backward_demodulation,[],[f2643,f4015]) ).
fof(f4052,plain,
meet(sF1,c) = meet(sF1,sF4),
inference(superposition,[],[f4022,f29]) ).
fof(f4270,plain,
! [X2,X3,X0,X1] : join(meet(X0,meet(X1,X2)),meet(X1,X3)) = meet(X1,join(meet(X3,X1),meet(X0,meet(X1,X2)))),
inference(superposition,[],[f284,f154]) ).
fof(f4324,plain,
! [X2,X0,X1] : join(meet(meet(X2,X0),X0),meet(meet(X2,X0),X1)) = meet(meet(X2,X0),join(meet(X1,join(meet(X2,X0),X0)),join(meet(X0,X1),meet(X0,X2)))),
inference(superposition,[],[f26,f284]) ).
fof(f4373,plain,
! [X2,X0,X1] : join(meet(meet(X2,X0),X0),meet(meet(X2,X0),X1)) = meet(X2,meet(X0,join(meet(X1,join(meet(X2,X0),X0)),join(meet(X0,X1),meet(X0,X2))))),
inference(forward_demodulation,[],[f4324,f7]) ).
fof(f4475,plain,
! [X2,X0,X1] : join(meet(meet(X2,X0),X0),meet(meet(X2,X0),X1)) = meet(X2,meet(X0,join(meet(X0,X2),join(meet(X1,join(meet(X2,X0),X0)),meet(X0,X1))))),
inference(forward_demodulation,[],[f4373,f180]) ).
fof(f4539,plain,
! [X2,X0,X1] : meet(X0,X2) = join(meet(meet(X2,X0),X0),meet(meet(X2,X0),X1)),
inference(forward_demodulation,[],[f4475,f2468]) ).
fof(f4594,plain,
! [X2,X0,X1] : meet(X0,X2) = join(meet(meet(X2,X0),X0),meet(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f4539,f7]) ).
fof(f4633,plain,
! [X2,X0,X1] : meet(X0,X2) = join(meet(X2,meet(X0,X0)),meet(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f4594,f7]) ).
fof(f4659,plain,
! [X2,X0,X1] : meet(X0,X2) = join(meet(X2,X0),meet(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f4633,f1]) ).
fof(f5146,plain,
! [X0] : meet(sF3,X0) = join(meet(X0,sF3),meet(X0,a)),
inference(superposition,[],[f4659,f83]) ).
fof(f5245,plain,
! [X0] : meet(sF3,X0) = meet(X0,join(meet(sF3,join(a,X0)),meet(a,join(X0,sF3)))),
inference(backward_demodulation,[],[f2704,f5146]) ).
fof(f8473,plain,
! [X2,X0,X1] : join(meet(join(X0,X1),X0),meet(join(X0,X1),X2)) = meet(join(X0,X1),join(meet(X2,join(X0,X1)),meet(X0,join(join(X0,X1),meet(X0,X2))))),
inference(superposition,[],[f113,f310]) ).
fof(f8499,plain,
! [X2,X0,X1] : join(meet(join(X0,X1),X0),meet(join(X0,X1),X2)) = meet(join(X0,X1),join(meet(X2,join(X0,X1)),meet(X0,join(X0,join(X1,meet(X0,X2)))))),
inference(forward_demodulation,[],[f8473,f8]) ).
fof(f8521,plain,
! [X2,X0,X1] : join(meet(join(X0,X1),X0),meet(join(X0,X1),X2)) = meet(join(X0,X1),join(meet(X2,join(X0,X1)),X0)),
inference(forward_demodulation,[],[f8499,f3]) ).
fof(f8530,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,meet(X2,join(X0,X1)))) = join(meet(join(X0,X1),X0),meet(join(X0,X1),X2)),
inference(forward_demodulation,[],[f8521,f6]) ).
fof(f8532,plain,
! [X2,X0,X1] : join(meet(X0,join(X0,X1)),meet(join(X0,X1),X2)) = meet(join(X0,X1),join(X0,meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f8530,f5]) ).
fof(f8534,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(X0,meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f8532,f3]) ).
fof(f8606,plain,
! [X0] : join(meet(sF1,a),meet(sF1,join(a,X0))) = meet(sF1,join(a,meet(join(a,X0),sF3))),
inference(superposition,[],[f115,f4019]) ).
fof(f8710,plain,
! [X0] : join(meet(sF1,a),meet(sF1,join(a,X0))) = meet(sF1,join(a,meet(sF3,join(a,X0)))),
inference(forward_demodulation,[],[f8606,f5]) ).
fof(f8787,plain,
! [X0] : meet(sF1,join(a,meet(sF3,join(a,X0)))) = join(sF2,meet(sF1,join(a,X0))),
inference(forward_demodulation,[],[f8710,f28]) ).
fof(f9304,plain,
! [X0] : meet(sF3,a) = meet(a,join(X0,sF3)),
inference(superposition,[],[f135,f283]) ).
fof(f9323,plain,
! [X0,X1] : join(meet(a,X0),meet(sF3,X1)) = meet(sF3,join(meet(X1,sF3),meet(a,X0))),
inference(superposition,[],[f284,f283]) ).
fof(f9327,plain,
! [X0,X1] : meet(meet(X0,a),meet(X1,sF3)) = meet(meet(X0,a),meet(X1,meet(a,X0))),
inference(superposition,[],[f1228,f283]) ).
fof(f9331,plain,
! [X0,X1] : meet(meet(X0,a),meet(X1,sF3)) = meet(X0,meet(a,meet(X1,meet(a,X0)))),
inference(forward_demodulation,[],[f9327,f7]) ).
fof(f9348,plain,
! [X0] : a = meet(a,join(X0,sF3)),
inference(forward_demodulation,[],[f9304,f83]) ).
fof(f9361,plain,
! [X0,X1] : meet(meet(X0,a),meet(X1,sF3)) = meet(X0,meet(a,meet(X1,a))),
inference(forward_demodulation,[],[f9331,f1297]) ).
fof(f9377,plain,
! [X0] : meet(sF3,X0) = meet(X0,join(meet(sF3,join(a,X0)),a)),
inference(backward_demodulation,[],[f5245,f9348]) ).
fof(f9384,plain,
! [X0,X1] : meet(X0,meet(a,X1)) = meet(meet(X0,a),meet(X1,sF3)),
inference(forward_demodulation,[],[f9361,f130]) ).
fof(f9395,plain,
! [X0] : meet(sF3,X0) = meet(X0,join(a,meet(sF3,join(a,X0)))),
inference(forward_demodulation,[],[f9377,f6]) ).
fof(f9400,plain,
! [X0,X1] : meet(X0,meet(a,X1)) = meet(X0,meet(a,meet(X1,sF3))),
inference(forward_demodulation,[],[f9384,f7]) ).
fof(f9409,plain,
! [X0,X1] : meet(X0,meet(a,X1)) = meet(X0,meet(sF3,meet(a,X1))),
inference(forward_demodulation,[],[f9400,f154]) ).
fof(f9413,plain,
! [X0,X1] : meet(X0,meet(a,X1)) = meet(X0,meet(X1,a)),
inference(forward_demodulation,[],[f9409,f2699]) ).
fof(f12176,plain,
! [X0] : a = join(a,meet(sF2,X0)),
inference(superposition,[],[f4,f3210]) ).
fof(f14313,plain,
! [X0] : meet(sF3,join(a,X0)) = meet(join(a,X0),join(a,meet(sF3,join(a,X0)))),
inference(superposition,[],[f9395,f310]) ).
fof(f14407,plain,
! [X0] : meet(sF3,join(a,X0)) = join(a,meet(join(a,X0),sF3)),
inference(forward_demodulation,[],[f14313,f8534]) ).
fof(f14443,plain,
! [X0] : meet(sF3,join(a,X0)) = join(a,meet(sF3,join(a,X0))),
inference(forward_demodulation,[],[f14407,f5]) ).
fof(f14471,plain,
! [X0] : join(sF2,meet(sF1,join(a,X0))) = meet(sF1,meet(sF3,join(a,X0))),
inference(backward_demodulation,[],[f8787,f14443]) ).
fof(f14520,plain,
! [X0] : meet(sF1,join(a,X0)) = join(sF2,meet(sF1,join(a,X0))),
inference(forward_demodulation,[],[f14471,f4022]) ).
fof(f14593,plain,
! [X0] : join(sF5,meet(sF1,join(a,X0))) = join(sF4,meet(sF1,join(a,X0))),
inference(superposition,[],[f174,f14520]) ).
fof(f16033,plain,
! [X2,X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X1,meet(X0,join(X0,meet(X1,meet(X0,X2))))))),
inference(superposition,[],[f157,f107]) ).
fof(f16480,plain,
! [X2,X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,X2)) = join(meet(X1,meet(X0,join(X0,meet(X1,meet(X0,X2))))),meet(X0,X2)),
inference(forward_demodulation,[],[f16033,f4270]) ).
fof(f16688,plain,
! [X2,X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,X2)) = join(meet(X0,X2),meet(X1,meet(X0,join(X0,meet(X1,meet(X0,X2)))))),
inference(forward_demodulation,[],[f16480,f6]) ).
fof(f16859,plain,
! [X2,X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,X2)) = join(meet(X0,X2),meet(X1,X0)),
inference(forward_demodulation,[],[f16688,f3]) ).
fof(f16982,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,X2),meet(X1,X0)),
inference(forward_demodulation,[],[f16859,f130]) ).
fof(f17437,plain,
! [X0] : join(sF2,meet(a,meet(X0,a))) = meet(a,join(meet(meet(X0,a),sF3),meet(sF1,join(a,meet(sF2,X0))))),
inference(superposition,[],[f4026,f379]) ).
fof(f17444,plain,
join(sF2,meet(a,c)) = meet(a,join(meet(c,sF3),meet(sF1,join(a,meet(sF1,sF4))))),
inference(superposition,[],[f4026,f4052]) ).
fof(f17468,plain,
join(sF2,meet(a,join(meet(a,join(sF1,sF0)),meet(c,join(sF1,a))))) = meet(a,join(meet(join(meet(a,join(sF1,sF0)),meet(c,join(sF1,a))),sF3),meet(sF1,join(a,join(meet(sF1,a),meet(sF1,c)))))),
inference(superposition,[],[f4026,f78]) ).
fof(f17541,plain,
join(sF2,meet(a,join(meet(a,join(sF1,sF0)),meet(c,join(sF1,a))))) = meet(a,join(meet(sF1,join(a,join(meet(sF1,a),meet(sF1,c)))),meet(join(meet(a,join(sF1,sF0)),meet(c,join(sF1,a))),sF3))),
inference(forward_demodulation,[],[f17468,f6]) ).
fof(f17563,plain,
join(sF2,meet(a,c)) = meet(a,join(meet(sF3,c),meet(sF1,join(a,meet(sF1,sF4))))),
inference(forward_demodulation,[],[f17444,f5]) ).
fof(f17570,plain,
! [X0] : join(sF2,meet(a,meet(X0,a))) = meet(a,join(meet(meet(X0,a),sF3),meet(sF1,a))),
inference(forward_demodulation,[],[f17437,f12176]) ).
fof(f17599,plain,
join(sF2,meet(a,join(meet(a,join(sF1,sF0)),meet(c,join(sF1,a))))) = meet(a,join(meet(sF1,join(a,join(meet(sF1,a),meet(sF1,c)))),meet(sF3,join(meet(a,join(sF1,sF0)),meet(c,join(sF1,a)))))),
inference(forward_demodulation,[],[f17541,f5]) ).
fof(f17617,plain,
join(sF2,meet(a,c)) = meet(a,join(sF4,meet(sF1,join(a,meet(sF1,sF4))))),
inference(forward_demodulation,[],[f17563,f29]) ).
fof(f17624,plain,
! [X0] : join(sF2,meet(a,meet(X0,a))) = meet(a,join(meet(sF1,a),meet(meet(X0,a),sF3))),
inference(forward_demodulation,[],[f17570,f6]) ).
fof(f17648,plain,
join(sF2,meet(a,join(meet(a,join(sF1,sF0)),meet(c,sF3)))) = meet(a,join(meet(sF1,join(a,join(meet(sF1,a),meet(sF1,c)))),meet(sF3,join(meet(a,join(sF1,sF0)),meet(c,sF3))))),
inference(forward_demodulation,[],[f17599,f4019]) ).
fof(f17661,plain,
join(sF2,sF0) = meet(a,join(sF4,meet(sF1,join(a,meet(sF1,sF4))))),
inference(forward_demodulation,[],[f17617,f12]) ).
fof(f17668,plain,
! [X0] : join(sF2,meet(a,meet(X0,a))) = meet(a,join(meet(sF1,a),meet(X0,meet(a,sF3)))),
inference(forward_demodulation,[],[f17624,f7]) ).
fof(f17686,plain,
join(sF2,meet(a,join(meet(c,sF3),meet(a,join(sF1,sF0))))) = meet(a,join(meet(sF1,join(a,join(meet(sF1,a),meet(sF1,c)))),meet(sF3,join(meet(c,sF3),meet(a,join(sF1,sF0)))))),
inference(forward_demodulation,[],[f17648,f6]) ).
fof(f17694,plain,
join(sF0,sF2) = meet(a,join(sF4,meet(sF1,join(a,meet(sF1,sF4))))),
inference(forward_demodulation,[],[f17661,f6]) ).
fof(f17701,plain,
! [X0] : join(sF2,meet(a,meet(X0,a))) = join(meet(X0,meet(a,sF3)),meet(a,sF1)),
inference(forward_demodulation,[],[f17668,f4270]) ).
fof(f17716,plain,
join(sF2,meet(a,join(meet(c,sF3),meet(a,join(sF1,sF0))))) = meet(a,join(meet(sF1,join(a,join(meet(sF1,a),meet(sF1,c)))),join(meet(a,join(sF1,sF0)),meet(sF3,c)))),
inference(forward_demodulation,[],[f17686,f9323]) ).
fof(f17724,plain,
sF2 = meet(a,join(sF4,meet(sF1,join(a,meet(sF1,sF4))))),
inference(forward_demodulation,[],[f17694,f405]) ).
fof(f17729,plain,
! [X0] : join(sF2,meet(a,meet(X0,a))) = join(meet(a,sF1),meet(X0,meet(a,sF3))),
inference(forward_demodulation,[],[f17701,f6]) ).
fof(f17742,plain,
join(sF2,meet(a,join(meet(c,sF3),meet(a,join(sF1,sF0))))) = meet(a,join(join(meet(a,join(sF1,sF0)),meet(sF3,c)),meet(sF1,join(a,join(meet(sF1,a),meet(sF1,c)))))),
inference(forward_demodulation,[],[f17716,f6]) ).
fof(f17752,plain,
! [X0] : join(sF2,meet(a,meet(X0,a))) = join(meet(a,sF1),meet(X0,meet(sF3,a))),
inference(forward_demodulation,[],[f17729,f9413]) ).
fof(f17764,plain,
join(sF2,meet(a,join(meet(c,sF3),meet(a,join(sF1,sF0))))) = meet(a,join(meet(a,join(sF1,sF0)),join(meet(sF3,c),meet(sF1,join(a,join(meet(sF1,a),meet(sF1,c))))))),
inference(forward_demodulation,[],[f17742,f8]) ).
fof(f17774,plain,
! [X0] : join(sF2,meet(a,meet(X0,a))) = join(meet(a,sF1),meet(X0,a)),
inference(forward_demodulation,[],[f17752,f83]) ).
fof(f17785,plain,
join(sF2,meet(a,join(meet(c,sF3),meet(a,join(sF1,sF0))))) = meet(a,join(meet(sF3,c),join(meet(sF1,join(a,join(meet(sF1,a),meet(sF1,c)))),meet(a,join(sF1,sF0))))),
inference(forward_demodulation,[],[f17764,f180]) ).
fof(f17789,plain,
! [X0] : join(sF2,meet(a,meet(X0,a))) = join(meet(sF1,a),meet(X0,a)),
inference(forward_demodulation,[],[f17774,f5]) ).
fof(f17799,plain,
join(sF2,meet(a,join(meet(c,sF3),meet(a,join(sF1,sF0))))) = meet(a,join(meet(sF3,c),join(meet(a,join(sF1,sF0)),meet(sF1,join(a,join(meet(sF1,a),meet(sF1,c))))))),
inference(forward_demodulation,[],[f17785,f6]) ).
fof(f17802,plain,
! [X0] : join(sF2,meet(X0,a)) = join(sF2,meet(a,meet(X0,a))),
inference(forward_demodulation,[],[f17789,f28]) ).
fof(f17812,plain,
join(sF2,meet(a,join(meet(c,sF3),meet(a,join(sF1,sF0))))) = meet(a,join(meet(sF3,c),join(meet(a,join(sF1,sF0)),meet(sF1,join(a,meet(sF1,c)))))),
inference(forward_demodulation,[],[f17799,f202]) ).
fof(f17815,plain,
! [X0] : join(sF2,meet(a,X0)) = join(sF2,meet(X0,a)),
inference(forward_demodulation,[],[f17802,f130]) ).
fof(f17825,plain,
join(sF2,meet(a,join(meet(c,sF3),meet(a,join(sF1,sF0))))) = meet(a,join(meet(sF3,c),join(meet(a,join(sF1,sF0)),meet(sF1,join(a,meet(sF1,sF4)))))),
inference(forward_demodulation,[],[f17812,f4052]) ).
fof(f17835,plain,
join(sF2,meet(a,join(meet(c,sF3),meet(a,join(sF0,sF1))))) = meet(a,join(meet(sF3,c),join(meet(a,join(sF0,sF1)),meet(sF1,join(a,meet(sF1,sF4)))))),
inference(forward_demodulation,[],[f17825,f6]) ).
fof(f17845,plain,
join(sF2,meet(a,join(meet(c,sF3),meet(a,sF1)))) = meet(a,join(meet(sF3,c),join(meet(a,sF1),meet(sF1,join(a,meet(sF1,sF4)))))),
inference(forward_demodulation,[],[f17835,f3017]) ).
fof(f17852,plain,
join(sF2,meet(a,join(meet(c,sF3),meet(sF1,a)))) = meet(a,join(meet(sF3,c),join(meet(sF1,a),meet(sF1,join(a,meet(sF1,sF4)))))),
inference(forward_demodulation,[],[f17845,f5]) ).
fof(f17858,plain,
join(sF2,meet(a,join(meet(c,sF3),meet(sF1,a)))) = meet(a,join(meet(sF1,a),join(meet(sF1,join(a,meet(sF1,sF4))),meet(sF3,c)))),
inference(forward_demodulation,[],[f17852,f180]) ).
fof(f17862,plain,
join(sF2,meet(a,join(meet(c,sF3),meet(sF1,a)))) = meet(a,join(meet(sF1,a),join(meet(sF3,c),meet(sF1,join(a,meet(sF1,sF4)))))),
inference(forward_demodulation,[],[f17858,f6]) ).
fof(f17865,plain,
join(sF2,meet(a,join(meet(c,sF3),meet(sF1,a)))) = meet(a,join(meet(sF1,a),join(sF4,meet(sF1,join(a,meet(sF1,sF4)))))),
inference(forward_demodulation,[],[f17862,f29]) ).
fof(f17867,plain,
join(sF2,meet(a,join(meet(c,sF3),meet(sF1,a)))) = meet(a,join(sF4,join(meet(sF1,join(a,meet(sF1,sF4))),meet(sF1,a)))),
inference(forward_demodulation,[],[f17865,f180]) ).
fof(f17869,plain,
join(sF2,meet(a,join(meet(c,sF3),meet(sF1,a)))) = meet(a,join(sF4,join(meet(sF1,a),meet(join(a,meet(sF1,sF4)),sF1)))),
inference(forward_demodulation,[],[f17867,f16982]) ).
fof(f17871,plain,
join(sF2,meet(a,join(meet(c,sF3),meet(sF1,a)))) = meet(a,join(sF4,join(meet(sF1,a),meet(sF1,join(a,meet(sF1,sF4)))))),
inference(forward_demodulation,[],[f17869,f5]) ).
fof(f17872,plain,
join(sF2,meet(a,join(meet(c,sF3),sF2))) = meet(a,join(sF4,join(sF2,meet(sF1,join(a,meet(sF1,sF4)))))),
inference(forward_demodulation,[],[f17871,f28]) ).
fof(f17873,plain,
join(sF2,meet(a,join(meet(c,sF3),sF2))) = meet(a,join(sF5,meet(sF1,join(a,meet(sF1,sF4))))),
inference(forward_demodulation,[],[f17872,f174]) ).
fof(f17874,plain,
meet(a,join(sF4,meet(sF1,join(a,meet(sF1,sF4))))) = join(sF2,meet(a,join(meet(c,sF3),sF2))),
inference(forward_demodulation,[],[f17873,f14593]) ).
fof(f17875,plain,
meet(a,join(sF4,meet(sF1,join(a,meet(sF1,sF4))))) = join(sF2,meet(a,join(sF2,meet(c,sF3)))),
inference(forward_demodulation,[],[f17874,f6]) ).
fof(f17876,plain,
meet(a,join(sF4,meet(sF1,join(a,meet(sF1,sF4))))) = join(sF2,meet(a,join(sF2,meet(sF3,c)))),
inference(forward_demodulation,[],[f17875,f5]) ).
fof(f17877,plain,
meet(a,join(sF4,meet(sF1,join(a,meet(sF1,sF4))))) = join(sF2,meet(a,join(sF2,sF4))),
inference(forward_demodulation,[],[f17876,f29]) ).
fof(f17878,plain,
meet(a,join(sF4,meet(sF1,join(a,meet(sF1,sF4))))) = join(sF2,meet(a,join(sF4,sF2))),
inference(forward_demodulation,[],[f17877,f6]) ).
fof(f17879,plain,
meet(a,join(sF4,meet(sF1,join(a,meet(sF1,sF4))))) = join(sF2,meet(a,sF5)),
inference(forward_demodulation,[],[f17878,f30]) ).
fof(f17880,plain,
meet(a,join(sF4,meet(sF1,join(a,meet(sF1,sF4))))) = join(sF2,meet(sF5,a)),
inference(forward_demodulation,[],[f17879,f17815]) ).
fof(f17881,plain,
join(sF2,sF6) = meet(a,join(sF4,meet(sF1,join(a,meet(sF1,sF4))))),
inference(forward_demodulation,[],[f17880,f31]) ).
fof(f17882,plain,
sF2 = join(sF2,sF6),
inference(forward_demodulation,[],[f17881,f17724]) ).
fof(f17883,plain,
sF2 = sF6,
inference(backward_demodulation,[],[f2937,f17882]) ).
fof(f17884,plain,
$false,
inference(forward_subsumption_resolution,[],[f17883,f25]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT141-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n020.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 14:03:49 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/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
% 17.25/3.11 % (3406481)Detected a unit-equality problem, will run specialized UEQ schedule.
% 17.25/3.11 % (3406508)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=1396982860:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 17.25/3.11 % (3406506)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=1404764053:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 17.25/3.11 % (3406512)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3324555441:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 17.25/3.11 % (3406510)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3876639877:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 17.25/3.11 % (3406507)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=1811896844:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 17.25/3.11 % (3406511)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=2497000733:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 17.25/3.11 % (3406509)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2909153713:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 17.25/3.11 % (3406510)Refutation not found, incomplete strategy
% 17.25/3.11 % (3406510)------------------------------
% 17.25/3.11 % (3406510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.25/3.11 % (3406510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.25/3.11 % (3406510)CaDiCaL version: 2.1.3
% 17.25/3.11 % (3406510)Termination reason: Refutation not found, incomplete strategy
% 17.25/3.11 % (3406510)Time elapsed: 0.002 s
% 17.25/3.11 % (3406510)Peak memory usage: 87 MB
% 17.25/3.11 % (3406510)Instructions burned: 1 (million)
% 17.25/3.11 % (3406509)Instruction limit reached!
% 17.25/3.11 % (3406509)------------------------------
% 17.25/3.11 % (3406509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.25/3.11 % (3406509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.25/3.11 % (3406509)CaDiCaL version: 2.1.3
% 17.25/3.11 % (3406509)Termination reason: Instruction limit
% 17.25/3.11 % (3406509)Termination phase: Saturation
% 17.25/3.11 % (3406509)Time elapsed: 0.138 s
% 17.25/3.11 % (3406509)Peak memory usage: 89 MB
% 17.25/3.11 % (3406509)Instructions burned: 137 (million)
% 17.25/3.11 % (3406511)Instruction limit reached!
% 17.25/3.11 % (3406511)------------------------------
% 17.25/3.11 % (3406511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.25/3.11 % (3406511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.25/3.11 % (3406511)CaDiCaL version: 2.1.3
% 17.25/3.11 % (3406511)Termination reason: Instruction limit
% 17.25/3.11 % (3406511)Termination phase: Saturation
% 17.25/3.11 % (3406511)Time elapsed: 0.251 s
% 17.25/3.11 % (3406511)Peak memory usage: 90 MB
% 17.25/3.11 % (3406511)Instructions burned: 257 (million)
% 17.25/3.11 % (3406510)------------------------------
% 17.25/3.11 % (3406510)------------------------------
% 17.25/3.11 % (3406537)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1350615051:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2996 on theBenchmark for (2996ds/2051Mi)
% 17.25/3.11 % (3406541)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2541303476:i=4948:ss=axioms:sgt=16_2994 on theBenchmark for (2994ds/4948Mi)
% 17.25/3.11 % (3406547)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=4144380604:i=215:ep=RSTC_2993 on theBenchmark for (2993ds/215Mi)
% 17.25/3.11 % (3406547)Instruction limit reached!
% 17.25/3.11 % (3406547)------------------------------
% 17.25/3.11 % (3406547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.25/3.11 % (3406547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.25/3.11 % (3406547)CaDiCaL version: 2.1.3
% 17.25/3.11 % (3406547)Termination reason: Instruction limit
% 17.25/3.11 % (3406547)Termination phase: Saturation
% 17.25/3.11 % (3406547)Time elapsed: 0.163 s
% 17.25/3.11 % (3406547)Peak memory usage: 90 MB
% 17.25/3.11 % (3406547)Instructions burned: 216 (million)
% 17.25/3.11 % (3406512)Instruction limit reached!
% 17.25/3.11 % (3406512)------------------------------
% 17.25/3.11 % (3406512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.25/3.11 % (3406512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.25/3.11 % (3406512)CaDiCaL version: 2.1.3
% 17.25/3.11 % (3406512)Termination reason: Instruction limit
% 17.25/3.11 % (3406512)Termination phase: Saturation
% 17.25/3.11 % (3406512)Time elapsed: 1.007 s
% 17.25/3.11 % (3406512)Peak memory usage: 98 MB
% 17.25/3.11 % (3406512)Instructions burned: 1187 (million)
% 17.25/3.11 % (3406553)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=1904495267:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2988 on theBenchmark for (2988ds/317Mi)
% 17.25/3.11 % (3406558)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=1159530374:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2987 on theBenchmark for (2987ds/12125Mi)
% 17.25/3.11 % (3406553)Instruction limit reached!
% 17.25/3.11 % (3406553)------------------------------
% 17.25/3.11 % (3406553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.25/3.11 % (3406553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.25/3.11 % (3406553)CaDiCaL version: 2.1.3
% 17.25/3.11 % (3406553)Termination reason: Instruction limit
% 17.25/3.11 % (3406553)Termination phase: Saturation
% 17.25/3.11 % (3406553)Time elapsed: 0.312 s
% 17.25/3.11 % (3406553)Peak memory usage: 93 MB
% 17.25/3.11 % (3406553)Instructions burned: 317 (million)
% 17.25/3.11 % (3406563)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=1912895219:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2983 on theBenchmark for (2983ds/2836Mi)
% 17.25/3.11 % (3406508)First to succeed.
% 17.25/3.11 % (3406508)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3406481"
% 17.25/3.11 % (3406508)Refutation found. Thanks to Tanya!
% 17.25/3.11 % SZS status Unsatisfiable for theBenchmark
% 17.25/3.11 % SZS output start Proof for theBenchmark
% See solution above
% 17.93/3.34 % (3406508)------------------------------
% 17.93/3.34 % (3406508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.93/3.34 % (3406508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.93/3.34 % (3406508)CaDiCaL version: 2.1.3
% 17.93/3.34 % (3406508)Termination reason: Refutation
% 17.93/3.34 % (3406508)Time elapsed: 1.967 s
% 17.93/3.34 % (3406508)Peak memory usage: 152 MB
% 17.93/3.34 % (3406508)Instructions burned: 3362 (million)
% 17.93/3.34 % (3406508)------------------------------
% 17.93/3.34 % (3406508)------------------------------
% 17.93/3.34 % (3406481)Success in time 2.481 s
% 17.93/3.34 % Vampire exiting
%------------------------------------------------------------------------------