%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN615-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.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 02:01:05 PM UTC 2026
% Result : Unsatisfiable 18.33s 3.26s
% Output : Refutation 18.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 61
% Syntax : Number of formulae : 197 ( 197 unt; 47 def)
% Number of atoms : 197 ( 196 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 1 ( 1 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 77 ( 77 usr; 38 con; 0-4 aty)
% Number of variables : 229 ( 229 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : ifeq3(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom) ).
fof(f3,axiom,
! [X2,X0,X1] : ifeq(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom_002) ).
fof(f5,negated_conjecture,
! [X0] : p7(X0,X0) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p7_2) ).
fof(f6,plain,
! [X0] : true = p7(X0,X0),
inference(reorient_equations,[],[f5]) ).
fof(f11,negated_conjecture,
p2(c26,f3(c22)) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_5) ).
fof(f12,plain,
true = p2(c26,f3(c22)),
inference(reorient_equations,[],[f11]) ).
fof(f13,negated_conjecture,
p19(c23,f3(f4(f5(c22)))) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p19_7) ).
fof(f14,plain,
true = p19(c23,f3(f4(f5(c22)))),
inference(reorient_equations,[],[f13]) ).
fof(f15,negated_conjecture,
p20(c24,f6(f3(f4(f5(c22))),c21)) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p20_8) ).
fof(f16,plain,
true = p20(c24,f6(f3(f4(f5(c22))),c21)),
inference(reorient_equations,[],[f15]) ).
fof(f27,negated_conjecture,
p2(c26,f14(f16(c28,f17(c21,c27)),c25)) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_14) ).
fof(f28,plain,
true = p2(c26,f14(f16(c28,f17(c21,c27)),c25)),
inference(reorient_equations,[],[f27]) ).
fof(f31,negated_conjecture,
! [X2,X0,X1] : ifeq3(p7(X0,X1),true,ifeq3(p7(X0,X2),true,p7(X2,X1),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p7_16) ).
fof(f32,plain,
! [X2,X0,X1] : true = ifeq3(p7(X0,X1),true,ifeq3(p7(X0,X2),true,p7(X2,X1),true),true),
inference(reorient_equations,[],[f31]) ).
fof(f33,negated_conjecture,
! [X2,X0,X1] : ifeq3(p2(X0,X1),true,ifeq3(p2(X0,X2),true,p2(X2,X1),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_17) ).
fof(f34,plain,
! [X2,X0,X1] : true = ifeq3(p2(X0,X1),true,ifeq3(p2(X0,X2),true,p2(X2,X1),true),true),
inference(reorient_equations,[],[f33]) ).
fof(f45,negated_conjecture,
! [X2,X3,X0,X1] : ifeq3(p7(X0,X1),true,ifeq3(p7(X2,X3),true,p7(f8(X2,X0),f8(X3,X1)),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p7_23) ).
fof(f46,plain,
! [X2,X3,X0,X1] : true = ifeq3(p7(X0,X1),true,ifeq3(p7(X2,X3),true,p7(f8(X2,X0),f8(X3,X1)),true),true),
inference(reorient_equations,[],[f45]) ).
fof(f47,negated_conjecture,
! [X2,X3,X0,X1] : ifeq3(p2(X0,X1),true,ifeq3(p7(X2,X3),true,p7(f10(X2,X0),f10(X3,X1)),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p7_24) ).
fof(f48,plain,
! [X2,X3,X0,X1] : true = ifeq3(p2(X0,X1),true,ifeq3(p7(X2,X3),true,p7(f10(X2,X0),f10(X3,X1)),true),true),
inference(reorient_equations,[],[f47]) ).
fof(f57,negated_conjecture,
p7(c25,f8(f10(f12(f11(f3(f5(c22)))),c23),f8(f10(f11(f3(f4(f5(c22)))),c26),f9(f11(c24),f10(f11(f3(f4(f5(c22)))),c27))))) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p7_29) ).
fof(f58,plain,
true = p7(c25,f8(f10(f12(f11(f3(f5(c22)))),c23),f8(f10(f11(f3(f4(f5(c22)))),c26),f9(f11(c24),f10(f11(f3(f4(f5(c22)))),c27))))),
inference(reorient_equations,[],[f57]) ).
fof(f61,negated_conjecture,
! [X0,X1] : ifeq(tuple(p7(c25,f8(f10(f12(f11(f3(f5(c22)))),X0),f8(f10(f11(f3(f4(f5(c22)))),f14(f16(c28,f17(c21,c27)),c25)),f9(f11(X1),f10(f11(f3(f4(f5(c22)))),c27))))),p2(f14(f16(c28,f17(c21,c27)),c25),f3(c22)),p19(X0,f3(f4(f5(c22)))),p20(X1,f6(f3(f4(f5(c22))),c21))),tuple(true,true,true,true),a,b) = b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p19_30) ).
fof(f62,plain,
! [X0,X1] : b = ifeq(tuple(p7(c25,f8(f10(f12(f11(f3(f5(c22)))),X0),f8(f10(f11(f3(f4(f5(c22)))),f14(f16(c28,f17(c21,c27)),c25)),f9(f11(X1),f10(f11(f3(f4(f5(c22)))),c27))))),p2(f14(f16(c28,f17(c21,c27)),c25),f3(c22)),p19(X0,f3(f4(f5(c22)))),p20(X1,f6(f3(f4(f5(c22))),c21))),tuple(true,true,true,true),a,b),
inference(reorient_equations,[],[f61]) ).
fof(f65,negated_conjecture,
a != b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f69,definition,
! [X0] : sF1(X0) = p7(X0,X0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f70,plain,
! [X0] : p7(X0,X0) = sF1(X0),
inference(reorient_equations,[],[f69]) ).
fof(f71,plain,
! [X0] : true = sF1(X0),
inference(definition_folding,[],[f6,f70]) ).
fof(f78,definition,
sF4 = f3(c22),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f79,plain,
f3(c22) = sF4,
inference(reorient_equations,[],[f78]) ).
fof(f80,definition,
sF5 = p2(c26,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f81,plain,
p2(c26,sF4) = sF5,
inference(reorient_equations,[],[f80]) ).
fof(f82,plain,
true = sF5,
inference(definition_folding,[],[f12,f81,f79]) ).
fof(f83,definition,
sF6 = f5(c22),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f84,plain,
f5(c22) = sF6,
inference(reorient_equations,[],[f83]) ).
fof(f85,definition,
sF7 = f4(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f86,plain,
f4(sF6) = sF7,
inference(reorient_equations,[],[f85]) ).
fof(f87,definition,
sF8 = f3(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f88,plain,
f3(sF7) = sF8,
inference(reorient_equations,[],[f87]) ).
fof(f89,definition,
sF9 = p19(c23,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f90,plain,
p19(c23,sF8) = sF9,
inference(reorient_equations,[],[f89]) ).
fof(f91,plain,
true = sF9,
inference(definition_folding,[],[f14,f90,f88,f86,f84]) ).
fof(f92,definition,
sF10 = f6(sF8,c21),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f93,plain,
f6(sF8,c21) = sF10,
inference(reorient_equations,[],[f92]) ).
fof(f94,definition,
sF11 = p20(c24,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f95,plain,
p20(c24,sF10) = sF11,
inference(reorient_equations,[],[f94]) ).
fof(f96,plain,
true = sF11,
inference(definition_folding,[],[f16,f95,f93,f88,f86,f84]) ).
fof(f122,definition,
sF22 = f17(c21,c27),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f123,plain,
f17(c21,c27) = sF22,
inference(reorient_equations,[],[f122]) ).
fof(f124,definition,
sF23 = f16(c28,sF22),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f125,plain,
f16(c28,sF22) = sF23,
inference(reorient_equations,[],[f124]) ).
fof(f126,definition,
sF24 = f14(sF23,c25),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f127,plain,
f14(sF23,c25) = sF24,
inference(reorient_equations,[],[f126]) ).
fof(f128,definition,
sF25 = p2(c26,sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f129,plain,
p2(c26,sF24) = sF25,
inference(reorient_equations,[],[f128]) ).
fof(f130,plain,
true = sF25,
inference(definition_folding,[],[f28,f129,f127,f125,f123]) ).
fof(f136,definition,
! [X2,X0,X1] : sF28(X0,X2,X1) = ifeq3(p7(X0,X2),true,p7(X2,X1),true),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f137,plain,
! [X2,X0,X1] : ifeq3(p7(X0,X2),true,p7(X2,X1),true) = sF28(X0,X2,X1),
inference(reorient_equations,[],[f136]) ).
fof(f138,definition,
! [X2,X0,X1] : sF29(X0,X1,X2) = ifeq3(p7(X0,X1),true,sF28(X0,X2,X1),true),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f139,plain,
! [X2,X0,X1] : ifeq3(p7(X0,X1),true,sF28(X0,X2,X1),true) = sF29(X0,X1,X2),
inference(reorient_equations,[],[f138]) ).
fof(f140,plain,
! [X2,X0,X1] : true = sF29(X0,X1,X2),
inference(definition_folding,[],[f32,f139,f137]) ).
fof(f141,definition,
! [X2,X0,X1] : sF30(X0,X2,X1) = ifeq3(p2(X0,X2),true,p2(X2,X1),true),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f142,plain,
! [X2,X0,X1] : ifeq3(p2(X0,X2),true,p2(X2,X1),true) = sF30(X0,X2,X1),
inference(reorient_equations,[],[f141]) ).
fof(f143,definition,
! [X2,X0,X1] : sF31(X0,X1,X2) = ifeq3(p2(X0,X1),true,sF30(X0,X2,X1),true),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f144,plain,
! [X2,X0,X1] : ifeq3(p2(X0,X1),true,sF30(X0,X2,X1),true) = sF31(X0,X1,X2),
inference(reorient_equations,[],[f143]) ).
fof(f145,plain,
! [X2,X0,X1] : true = sF31(X0,X1,X2),
inference(definition_folding,[],[f34,f144,f142]) ).
fof(f179,definition,
! [X2,X3,X0,X1] : sF46(X2,X0,X3,X1) = p7(f8(X2,X0),f8(X3,X1)),
introduced(definition,[new_symbols(definition,[sF46])],[function_definition]) ).
fof(f180,plain,
! [X2,X3,X0,X1] : p7(f8(X2,X0),f8(X3,X1)) = sF46(X2,X0,X3,X1),
inference(reorient_equations,[],[f179]) ).
fof(f181,definition,
! [X2,X3,X0,X1] : sF47(X2,X3,X0,X1) = ifeq3(p7(X2,X3),true,sF46(X2,X0,X3,X1),true),
introduced(definition,[new_symbols(definition,[sF47])],[function_definition]) ).
fof(f182,plain,
! [X2,X3,X0,X1] : ifeq3(p7(X2,X3),true,sF46(X2,X0,X3,X1),true) = sF47(X2,X3,X0,X1),
inference(reorient_equations,[],[f181]) ).
fof(f183,definition,
! [X2,X3,X0,X1] : sF48(X0,X1,X2,X3) = ifeq3(p7(X0,X1),true,sF47(X2,X3,X0,X1),true),
introduced(definition,[new_symbols(definition,[sF48])],[function_definition]) ).
fof(f184,plain,
! [X2,X3,X0,X1] : ifeq3(p7(X0,X1),true,sF47(X2,X3,X0,X1),true) = sF48(X0,X1,X2,X3),
inference(reorient_equations,[],[f183]) ).
fof(f185,plain,
! [X2,X3,X0,X1] : true = sF48(X0,X1,X2,X3),
inference(definition_folding,[],[f46,f184,f182,f180]) ).
fof(f186,definition,
! [X2,X3,X0,X1] : sF49(X2,X0,X3,X1) = p7(f10(X2,X0),f10(X3,X1)),
introduced(definition,[new_symbols(definition,[sF49])],[function_definition]) ).
fof(f187,plain,
! [X2,X3,X0,X1] : p7(f10(X2,X0),f10(X3,X1)) = sF49(X2,X0,X3,X1),
inference(reorient_equations,[],[f186]) ).
fof(f188,definition,
! [X2,X3,X0,X1] : sF50(X2,X3,X0,X1) = ifeq3(p7(X2,X3),true,sF49(X2,X0,X3,X1),true),
introduced(definition,[new_symbols(definition,[sF50])],[function_definition]) ).
fof(f189,plain,
! [X2,X3,X0,X1] : ifeq3(p7(X2,X3),true,sF49(X2,X0,X3,X1),true) = sF50(X2,X3,X0,X1),
inference(reorient_equations,[],[f188]) ).
fof(f190,definition,
! [X2,X3,X0,X1] : sF51(X0,X1,X2,X3) = ifeq3(p2(X0,X1),true,sF50(X2,X3,X0,X1),true),
introduced(definition,[new_symbols(definition,[sF51])],[function_definition]) ).
fof(f191,plain,
! [X2,X3,X0,X1] : ifeq3(p2(X0,X1),true,sF50(X2,X3,X0,X1),true) = sF51(X0,X1,X2,X3),
inference(reorient_equations,[],[f190]) ).
fof(f192,plain,
! [X2,X3,X0,X1] : true = sF51(X0,X1,X2,X3),
inference(definition_folding,[],[f48,f191,f189,f187]) ).
fof(f221,definition,
sF64 = f3(sF6),
introduced(definition,[new_symbols(definition,[sF64])],[function_definition]) ).
fof(f222,plain,
f3(sF6) = sF64,
inference(reorient_equations,[],[f221]) ).
fof(f223,definition,
sF65 = f11(sF64),
introduced(definition,[new_symbols(definition,[sF65])],[function_definition]) ).
fof(f224,plain,
f11(sF64) = sF65,
inference(reorient_equations,[],[f223]) ).
fof(f225,definition,
sF66 = f12(sF65),
introduced(definition,[new_symbols(definition,[sF66])],[function_definition]) ).
fof(f226,plain,
f12(sF65) = sF66,
inference(reorient_equations,[],[f225]) ).
fof(f227,definition,
sF67 = f10(sF66,c23),
introduced(definition,[new_symbols(definition,[sF67])],[function_definition]) ).
fof(f228,plain,
f10(sF66,c23) = sF67,
inference(reorient_equations,[],[f227]) ).
fof(f229,definition,
sF68 = f11(sF8),
introduced(definition,[new_symbols(definition,[sF68])],[function_definition]) ).
fof(f230,plain,
f11(sF8) = sF68,
inference(reorient_equations,[],[f229]) ).
fof(f231,definition,
sF69 = f10(sF68,c26),
introduced(definition,[new_symbols(definition,[sF69])],[function_definition]) ).
fof(f232,plain,
f10(sF68,c26) = sF69,
inference(reorient_equations,[],[f231]) ).
fof(f233,definition,
sF70 = f11(c24),
introduced(definition,[new_symbols(definition,[sF70])],[function_definition]) ).
fof(f234,plain,
f11(c24) = sF70,
inference(reorient_equations,[],[f233]) ).
fof(f235,definition,
sF71 = f10(sF68,c27),
introduced(definition,[new_symbols(definition,[sF71])],[function_definition]) ).
fof(f236,plain,
f10(sF68,c27) = sF71,
inference(reorient_equations,[],[f235]) ).
fof(f237,definition,
sF72 = f9(sF70,sF71),
introduced(definition,[new_symbols(definition,[sF72])],[function_definition]) ).
fof(f238,plain,
f9(sF70,sF71) = sF72,
inference(reorient_equations,[],[f237]) ).
fof(f239,definition,
sF73 = f8(sF69,sF72),
introduced(definition,[new_symbols(definition,[sF73])],[function_definition]) ).
fof(f240,plain,
f8(sF69,sF72) = sF73,
inference(reorient_equations,[],[f239]) ).
fof(f241,definition,
sF74 = f8(sF67,sF73),
introduced(definition,[new_symbols(definition,[sF74])],[function_definition]) ).
fof(f242,plain,
f8(sF67,sF73) = sF74,
inference(reorient_equations,[],[f241]) ).
fof(f243,definition,
sF75 = p7(c25,sF74),
introduced(definition,[new_symbols(definition,[sF75])],[function_definition]) ).
fof(f244,plain,
p7(c25,sF74) = sF75,
inference(reorient_equations,[],[f243]) ).
fof(f245,plain,
true = sF75,
inference(definition_folding,[],[f58,f244,f242,f240,f238,f236,f230,f88,f86,f84,f234,f232,f230,f88,f86,f84,f228,f226,f224,f222,f84]) ).
fof(f251,definition,
! [X0] : sF78(X0) = f10(sF66,X0),
introduced(definition,[new_symbols(definition,[sF78])],[function_definition]) ).
fof(f252,plain,
! [X0] : f10(sF66,X0) = sF78(X0),
inference(reorient_equations,[],[f251]) ).
fof(f253,definition,
sF79 = f10(sF68,sF24),
introduced(definition,[new_symbols(definition,[sF79])],[function_definition]) ).
fof(f254,plain,
f10(sF68,sF24) = sF79,
inference(reorient_equations,[],[f253]) ).
fof(f255,definition,
! [X1] : sF80(X1) = f9(f11(X1),sF71),
introduced(definition,[new_symbols(definition,[sF80])],[function_definition]) ).
fof(f256,plain,
! [X1] : f9(f11(X1),sF71) = sF80(X1),
inference(reorient_equations,[],[f255]) ).
fof(f257,definition,
! [X1] : sF81(X1) = f8(sF79,sF80(X1)),
introduced(definition,[new_symbols(definition,[sF81])],[function_definition]) ).
fof(f258,plain,
! [X1] : f8(sF79,sF80(X1)) = sF81(X1),
inference(reorient_equations,[],[f257]) ).
fof(f259,definition,
! [X0,X1] : sF82(X0,X1) = f8(sF78(X0),sF81(X1)),
introduced(definition,[new_symbols(definition,[sF82])],[function_definition]) ).
fof(f260,plain,
! [X0,X1] : f8(sF78(X0),sF81(X1)) = sF82(X0,X1),
inference(reorient_equations,[],[f259]) ).
fof(f261,definition,
! [X0,X1] : sF83(X0,X1) = p7(c25,sF82(X0,X1)),
introduced(definition,[new_symbols(definition,[sF83])],[function_definition]) ).
fof(f262,plain,
! [X0,X1] : p7(c25,sF82(X0,X1)) = sF83(X0,X1),
inference(reorient_equations,[],[f261]) ).
fof(f263,definition,
sF84 = p2(sF24,sF4),
introduced(definition,[new_symbols(definition,[sF84])],[function_definition]) ).
fof(f264,plain,
p2(sF24,sF4) = sF84,
inference(reorient_equations,[],[f263]) ).
fof(f265,definition,
! [X0] : sF85(X0) = p19(X0,sF8),
introduced(definition,[new_symbols(definition,[sF85])],[function_definition]) ).
fof(f266,plain,
! [X0] : p19(X0,sF8) = sF85(X0),
inference(reorient_equations,[],[f265]) ).
fof(f267,definition,
! [X1] : sF86(X1) = p20(X1,sF10),
introduced(definition,[new_symbols(definition,[sF86])],[function_definition]) ).
fof(f268,plain,
! [X1] : p20(X1,sF10) = sF86(X1),
inference(reorient_equations,[],[f267]) ).
fof(f269,definition,
! [X0,X1] : sF87(X0,X1) = tuple(sF83(X0,X1),sF84,sF85(X0),sF86(X1)),
introduced(definition,[new_symbols(definition,[sF87])],[function_definition]) ).
fof(f270,plain,
! [X0,X1] : tuple(sF83(X0,X1),sF84,sF85(X0),sF86(X1)) = sF87(X0,X1),
inference(reorient_equations,[],[f269]) ).
fof(f271,definition,
sF88 = tuple(true,true,true,true),
introduced(definition,[new_symbols(definition,[sF88])],[function_definition]) ).
fof(f272,plain,
tuple(true,true,true,true) = sF88,
inference(reorient_equations,[],[f271]) ).
fof(f273,definition,
! [X0,X1] : sF89(X0,X1) = ifeq(sF87(X0,X1),sF88,a,b),
introduced(definition,[new_symbols(definition,[sF89])],[function_definition]) ).
fof(f274,plain,
! [X0,X1] : ifeq(sF87(X0,X1),sF88,a,b) = sF89(X0,X1),
inference(reorient_equations,[],[f273]) ).
fof(f275,plain,
! [X0,X1] : b = sF89(X0,X1),
inference(definition_folding,[],[f62,f274,f272,f270,f268,f93,f88,f86,f84,f266,f88,f86,f84,f264,f79,f127,f125,f123,f262,f260,f258,f256,f236,f230,f88,f86,f84,f254,f127,f125,f123,f230,f88,f86,f84,f252,f226,f224,f222,f84]) ).
fof(f288,plain,
! [X0] : true = p7(X0,X0),
inference(forward_demodulation,[],[f70,f71]) ).
fof(f291,plain,
true = p2(c26,sF4),
inference(forward_demodulation,[],[f81,f82]) ).
fof(f292,plain,
true = p19(c23,sF8),
inference(forward_demodulation,[],[f90,f91]) ).
fof(f293,plain,
true = p20(c24,sF10),
inference(forward_demodulation,[],[f95,f96]) ).
fof(f299,plain,
true = p2(c26,sF24),
inference(forward_demodulation,[],[f129,f130]) ).
fof(f301,plain,
! [X2,X0,X1] : true = ifeq3(p7(X0,X1),true,sF28(X0,X2,X1),true),
inference(forward_demodulation,[],[f139,f140]) ).
fof(f302,plain,
! [X2,X0,X1] : true = ifeq3(p2(X0,X1),true,sF30(X0,X2,X1),true),
inference(forward_demodulation,[],[f144,f145]) ).
fof(f308,plain,
! [X2,X3,X0,X1] : true = ifeq3(p7(X0,X1),true,sF47(X2,X3,X0,X1),true),
inference(forward_demodulation,[],[f184,f185]) ).
fof(f309,plain,
! [X2,X3,X0,X1] : true = ifeq3(p2(X0,X1),true,sF50(X2,X3,X0,X1),true),
inference(forward_demodulation,[],[f191,f192]) ).
fof(f314,plain,
true = p7(c25,sF74),
inference(forward_demodulation,[],[f244,f245]) ).
fof(f316,plain,
! [X0,X1] : b = ifeq(sF87(X0,X1),sF88,a,b),
inference(forward_demodulation,[],[f274,f275]) ).
fof(f318,plain,
true = sF85(c23),
inference(forward_demodulation,[],[f292,f266]) ).
fof(f319,plain,
true = sF86(c24),
inference(forward_demodulation,[],[f293,f268]) ).
fof(f323,plain,
sF67 = sF78(c23),
inference(superposition,[],[f252,f228]) ).
fof(f352,plain,
! [X0] : sF87(c23,X0) = tuple(sF83(c23,X0),sF84,true,sF86(X0)),
inference(superposition,[],[f270,f318]) ).
fof(f355,plain,
f9(sF70,sF71) = sF80(c24),
inference(superposition,[],[f256,f234]) ).
fof(f357,plain,
sF72 = sF80(c24),
inference(forward_demodulation,[],[f355,f238]) ).
fof(f358,plain,
sF81(c24) = f8(sF79,sF72),
inference(superposition,[],[f258,f357]) ).
fof(f361,plain,
! [X0,X1] : true = ifeq3(true,true,sF28(X0,X1,X0),true),
inference(superposition,[],[f301,f288]) ).
fof(f367,plain,
! [X0,X1] : true = sF28(X0,X1,X0),
inference(forward_demodulation,[],[f361,f1]) ).
fof(f371,plain,
! [X0] : true = ifeq3(true,true,sF30(c26,X0,sF4),true),
inference(superposition,[],[f302,f291]) ).
fof(f379,plain,
! [X0] : true = sF30(c26,X0,sF4),
inference(forward_demodulation,[],[f371,f1]) ).
fof(f385,plain,
! [X0,X1] : sF49(sF68,c26,X0,X1) = p7(sF69,f10(X0,X1)),
inference(superposition,[],[f187,f232]) ).
fof(f411,plain,
! [X0] : sF30(c26,sF24,X0) = ifeq3(true,true,p2(sF24,X0),true),
inference(superposition,[],[f142,f299]) ).
fof(f425,plain,
! [X0] : p2(sF24,X0) = sF30(c26,sF24,X0),
inference(forward_demodulation,[],[f411,f1]) ).
fof(f449,plain,
true = p2(sF24,sF4),
inference(superposition,[],[f425,f379]) ).
fof(f514,plain,
! [X2,X0,X1] : true = ifeq3(true,true,sF47(X1,X2,X0,X0),true),
inference(superposition,[],[f308,f288]) ).
fof(f521,plain,
! [X2,X0,X1] : true = sF47(X1,X2,X0,X0),
inference(forward_demodulation,[],[f514,f1]) ).
fof(f569,plain,
! [X0,X1] : true = ifeq3(true,true,sF50(X0,X1,c26,sF24),true),
inference(superposition,[],[f309,f299]) ).
fof(f580,plain,
! [X0,X1] : true = sF50(X0,X1,c26,sF24),
inference(forward_demodulation,[],[f569,f1]) ).
fof(f725,plain,
! [X0,X1] : sF46(sF67,sF73,X0,X1) = p7(sF74,f8(X0,X1)),
inference(superposition,[],[f180,f242]) ).
fof(f726,plain,
! [X0,X1] : sF46(sF69,sF72,X0,X1) = p7(sF73,f8(X0,X1)),
inference(superposition,[],[f180,f240]) ).
fof(f742,plain,
! [X0] : sF28(c25,sF74,X0) = ifeq3(true,true,p7(sF74,X0),true),
inference(superposition,[],[f137,f314]) ).
fof(f753,plain,
! [X0] : p7(sF74,X0) = sF28(c25,sF74,X0),
inference(forward_demodulation,[],[f742,f1]) ).
fof(f757,plain,
true = p7(sF74,c25),
inference(superposition,[],[f367,f753]) ).
fof(f763,plain,
! [X0] : sF82(c23,X0) = f8(sF67,sF81(X0)),
inference(superposition,[],[f260,f323]) ).
fof(f815,plain,
! [X0] : sF28(sF74,c25,X0) = ifeq3(true,true,p7(c25,X0),true),
inference(superposition,[],[f137,f757]) ).
fof(f824,plain,
! [X0] : p7(c25,X0) = sF28(sF74,c25,X0),
inference(forward_demodulation,[],[f815,f1]) ).
fof(f1003,plain,
true = sF84,
inference(superposition,[],[f264,f449]) ).
fof(f1093,plain,
sF87(c23,c24) = tuple(sF83(c23,c24),sF84,true,true),
inference(superposition,[],[f352,f319]) ).
fof(f1094,plain,
sF87(c23,c24) = tuple(sF83(c23,c24),true,true,true),
inference(forward_demodulation,[],[f1093,f1003]) ).
fof(f1383,plain,
! [X2,X0,X1] : sF50(X0,X0,X1,X2) = ifeq3(true,true,sF49(X0,X1,X0,X2),true),
inference(superposition,[],[f189,f288]) ).
fof(f1396,plain,
! [X2,X0,X1] : sF49(X0,X1,X0,X2) = sF50(X0,X0,X1,X2),
inference(forward_demodulation,[],[f1383,f1]) ).
fof(f1406,plain,
! [X0] : true = sF49(X0,c26,X0,sF24),
inference(superposition,[],[f580,f1396]) ).
fof(f1426,plain,
! [X2,X0,X1] : sF47(X0,X0,X1,X2) = ifeq3(true,true,sF46(X0,X1,X0,X2),true),
inference(superposition,[],[f182,f288]) ).
fof(f1439,plain,
! [X2,X0,X1] : sF46(X0,X1,X0,X2) = sF47(X0,X0,X1,X2),
inference(forward_demodulation,[],[f1426,f1]) ).
fof(f1908,plain,
true = p7(sF69,f10(sF68,sF24)),
inference(superposition,[],[f1406,f385]) ).
fof(f1912,plain,
true = p7(sF69,sF79),
inference(forward_demodulation,[],[f1908,f254]) ).
fof(f1918,plain,
! [X0,X1] : sF47(sF69,sF79,X0,X1) = ifeq3(true,true,sF46(sF69,X0,sF79,X1),true),
inference(superposition,[],[f182,f1912]) ).
fof(f1931,plain,
! [X0,X1] : sF46(sF69,X0,sF79,X1) = sF47(sF69,sF79,X0,X1),
inference(forward_demodulation,[],[f1918,f1]) ).
fof(f1964,plain,
! [X0] : true = sF46(sF69,X0,sF79,X0),
inference(superposition,[],[f521,f1931]) ).
fof(f2593,plain,
true = p7(sF73,f8(sF79,sF72)),
inference(superposition,[],[f726,f1964]) ).
fof(f2596,plain,
true = p7(sF73,sF81(c24)),
inference(forward_demodulation,[],[f2593,f358]) ).
fof(f2609,plain,
! [X0,X1] : true = ifeq3(true,true,sF47(X0,X1,sF73,sF81(c24)),true),
inference(superposition,[],[f308,f2596]) ).
fof(f2610,plain,
! [X0,X1] : true = sF47(X0,X1,sF73,sF81(c24)),
inference(forward_demodulation,[],[f2609,f1]) ).
fof(f2749,plain,
! [X0] : true = sF46(X0,sF73,X0,sF81(c24)),
inference(superposition,[],[f1439,f2610]) ).
fof(f6235,plain,
true = p7(sF74,f8(sF67,sF81(c24))),
inference(superposition,[],[f725,f2749]) ).
fof(f6236,plain,
true = p7(sF74,sF82(c23,c24)),
inference(forward_demodulation,[],[f6235,f763]) ).
fof(f6250,plain,
! [X0] : true = ifeq3(true,true,sF28(sF74,X0,sF82(c23,c24)),true),
inference(superposition,[],[f301,f6236]) ).
fof(f6258,plain,
! [X0] : true = sF28(sF74,X0,sF82(c23,c24)),
inference(forward_demodulation,[],[f6250,f1]) ).
fof(f6271,plain,
true = p7(c25,sF82(c23,c24)),
inference(superposition,[],[f824,f6258]) ).
fof(f6275,plain,
true = sF83(c23,c24),
inference(forward_demodulation,[],[f6271,f262]) ).
fof(f6278,plain,
tuple(true,true,true,true) = sF87(c23,c24),
inference(superposition,[],[f1094,f6275]) ).
fof(f6303,plain,
sF88 = sF87(c23,c24),
inference(forward_demodulation,[],[f6278,f272]) ).
fof(f6316,plain,
b = ifeq(sF88,sF88,a,b),
inference(superposition,[],[f316,f6303]) ).
fof(f6317,plain,
a = b,
inference(forward_demodulation,[],[f6316,f3]) ).
fof(f6318,plain,
$false,
inference(forward_subsumption_resolution,[],[f6317,f65]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN615-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.19 % Computer : n017.cluster.edu
% 0.11/0.19 % Model : x86_64 x86_64
% 0.11/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.19 % Memory : 8046.5625MB
% 0.11/0.19 % OS : Linux 6.8.0-71-generic
% 0.11/0.19 % CPULimit : 300
% 0.11/0.19 % WCLimit : 300
% 0.11/0.19 % DateTime : Mon Sep 28 16:31:36 UTC 2026
% 0.11/0.19 % CPUTime :
% 0.11/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.23 Running first-order theorem proving
% 0.11/0.23 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
% 18.33/3.26 % (3687429)Detected a unit-equality problem, will run specialized UEQ schedule.
% 18.33/3.26 % (3687436)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2785376790:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 18.33/3.26 % (3687437)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=185091423:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 18.33/3.26 % (3687438)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=124354058:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 18.33/3.26 % (3687434)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=2957277360:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 18.33/3.26 % (3687439)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1802009055:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 18.33/3.26 % (3687435)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=4104913279:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 18.33/3.26 % (3687440)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3087545298:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 18.33/3.26 % (3687437)Instruction limit reached!
% 18.33/3.26 % (3687437)------------------------------
% 18.33/3.26 % (3687437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.33/3.26 % (3687437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.33/3.26 % (3687437)CaDiCaL version: 2.1.3
% 18.33/3.26 % (3687437)Termination reason: Instruction limit
% 18.33/3.26 % (3687437)Termination phase: Saturation
% 18.33/3.26 % (3687437)Time elapsed: 0.073 s
% 18.33/3.26 % (3687437)Peak memory usage: 88 MB
% 18.33/3.26 % (3687437)Instructions burned: 136 (million)
% 18.33/3.26 % (3687438)Instruction limit reached!
% 18.33/3.26 % (3687438)------------------------------
% 18.33/3.26 % (3687438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.33/3.26 % (3687438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.33/3.26 % (3687438)CaDiCaL version: 2.1.3
% 18.33/3.26 % (3687438)Termination reason: Instruction limit
% 18.33/3.26 % (3687438)Termination phase: Saturation
% 18.33/3.26 % (3687438)Time elapsed: 0.093 s
% 18.33/3.26 % (3687438)Peak memory usage: 90 MB
% 18.33/3.26 % (3687438)Instructions burned: 181 (million)
% 18.33/3.26 % (3687439)Instruction limit reached!
% 18.33/3.26 % (3687439)------------------------------
% 18.33/3.26 % (3687439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.33/3.26 % (3687439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.33/3.26 % (3687439)CaDiCaL version: 2.1.3
% 18.33/3.26 % (3687439)Termination reason: Instruction limit
% 18.33/3.26 % (3687439)Termination phase: Saturation
% 18.33/3.26 % (3687439)Time elapsed: 0.144 s
% 18.33/3.26 % (3687439)Peak memory usage: 91 MB
% 18.33/3.26 % (3687439)Instructions burned: 257 (million)
% 18.33/3.26 % (3687448)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=412094692:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 18.33/3.26 % (3687449)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1069521596:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 18.33/3.26 % (3687450)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=843797112:i=215:ep=RSTC_2997 on theBenchmark for (2997ds/215Mi)
% 18.33/3.26 % (3687450)Instruction limit reached!
% 18.33/3.26 % (3687450)------------------------------
% 18.33/3.26 % (3687450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.33/3.26 % (3687450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.33/3.26 % (3687450)CaDiCaL version: 2.1.3
% 18.33/3.26 % (3687450)Termination reason: Instruction limit
% 18.33/3.26 % (3687450)Termination phase: Saturation
% 18.33/3.26 % (3687450)Time elapsed: 0.105 s
% 18.33/3.26 % (3687450)Peak memory usage: 92 MB
% 18.33/3.26 % (3687450)Instructions burned: 215 (million)
% 18.33/3.26 % (3687454)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=847825585: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)
% 18.33/3.26 % (3687440)Instruction limit reached!
% 18.33/3.26 % (3687440)------------------------------
% 18.33/3.26 % (3687440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.33/3.26 % (3687440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.33/3.26 % (3687440)CaDiCaL version: 2.1.3
% 18.33/3.26 % (3687440)Termination reason: Instruction limit
% 18.33/3.26 % (3687440)Termination phase: Saturation
% 18.33/3.26 % (3687440)Time elapsed: 0.581 s
% 18.33/3.26 % (3687440)Peak memory usage: 104 MB
% 18.33/3.26 % (3687440)Instructions burned: 1189 (million)
% 18.33/3.26 % (3687454)Instruction limit reached!
% 18.33/3.26 % (3687454)------------------------------
% 18.33/3.26 % (3687454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.33/3.26 % (3687454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.33/3.26 % (3687454)CaDiCaL version: 2.1.3
% 18.33/3.26 % (3687454)Termination reason: Instruction limit
% 18.33/3.26 % (3687454)Termination phase: Saturation
% 18.33/3.26 % (3687454)Time elapsed: 0.200 s
% 18.33/3.26 % (3687454)Peak memory usage: 94 MB
% 18.33/3.26 % (3687454)Instructions burned: 318 (million)
% 18.33/3.26 % (3687456)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=199764584:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/12125Mi)
% 18.33/3.26 % (3687457)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=346516701:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2991 on theBenchmark for (2991ds/2836Mi)
% 18.33/3.26 % (3687448)Instruction limit reached!
% 18.33/3.26 % (3687448)------------------------------
% 18.33/3.26 % (3687448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.33/3.26 % (3687448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.33/3.26 % (3687448)CaDiCaL version: 2.1.3
% 18.33/3.26 % (3687448)Termination reason: Instruction limit
% 18.33/3.26 % (3687448)Termination phase: Saturation
% 18.33/3.26 % (3687448)Time elapsed: 1.244 s
% 18.33/3.26 % (3687448)Peak memory usage: 142 MB
% 18.33/3.26 % (3687448)Instructions burned: 2052 (million)
% 18.33/3.26 % (3687460)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2731695710:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2983 on theBenchmark for (2983ds/14534Mi)
% 18.33/3.26 % (3687456)First to succeed.
% 18.33/3.26 % (3687456)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3687429"
% 18.33/3.26 % (3687456)Refutation found. Thanks to Tanya!
% 18.33/3.26 % SZS status Unsatisfiable for theBenchmark
% 18.33/3.26 % SZS output start Proof for theBenchmark
% See solution above
% 18.76/3.35 % (3687456)------------------------------
% 18.76/3.35 % (3687456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.76/3.35 % (3687456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/3.35 % (3687456)CaDiCaL version: 2.1.3
% 18.76/3.35 % (3687456)Termination reason: Refutation
% 18.76/3.35 % (3687456)Time elapsed: 1.445 s
% 18.76/3.35 % (3687456)Peak memory usage: 141 MB
% 18.76/3.35 % (3687456)Instructions burned: 2209 (million)
% 18.76/3.35 % (3687456)------------------------------
% 18.76/3.35 % (3687456)------------------------------
% 18.76/3.35 % (3687429)Success in time 2.592 s
% 18.76/3.35 % Vampire exiting
%------------------------------------------------------------------------------