%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : FLD050-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.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 09:49:13 AM UTC 2026
% Result : Unsatisfiable 14.02s 2.69s
% Output : Refutation 14.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 24
% Syntax : Number of formulae : 131 ( 40 unt; 7 def)
% Number of atoms : 402 ( 12 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 514 ( 243 ~; 270 |; 0 &)
% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 2 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 164 ( 0 sgn 164 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X2,X0,X1] :
( equalish(multiply(X0,multiply(X1,X2)),multiply(multiply(X0,X1),X2))
| ~ defined(X0)
| ~ defined(X1)
| ~ defined(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_multiplication) ).
fof(f6,axiom,
! [X0] :
( equalish(multiply(multiplicative_identity,X0),X0)
| ~ defined(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_identity_multiplication) ).
fof(f7,axiom,
! [X0] :
( equalish(multiply(X0,multiplicative_inverse(X0)),multiplicative_identity)
| ~ defined(X0)
| equalish(X0,additive_identity) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_inverse_multiplication) ).
fof(f8,axiom,
! [X0,X1] :
( equalish(multiply(X0,X1),multiply(X1,X0))
| ~ defined(X0)
| ~ defined(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_multiplication) ).
fof(f13,axiom,
! [X0,X1] :
( defined(multiply(X0,X1))
| ~ defined(X0)
| ~ defined(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',well_definedness_of_multiplication) ).
fof(f15,axiom,
! [X0] :
( equalish(X0,additive_identity)
| ~ defined(X0)
| defined(multiplicative_inverse(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',well_definedness_of_multiplicative_inverse) ).
fof(f22,axiom,
! [X0,X1] :
( ~ equalish(X1,X0)
| equalish(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry_of_equality) ).
fof(f23,axiom,
! [X2,X0,X1] :
( ~ equalish(X2,X1)
| ~ equalish(X0,X2)
| equalish(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_of_equality) ).
fof(f25,axiom,
! [X2,X0,X1] :
( equalish(multiply(X0,X1),multiply(X2,X1))
| ~ defined(X1)
| ~ equalish(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compatibility_of_equality_and_multiplication) ).
fof(f28,axiom,
defined(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_is_defined) ).
fof(f29,axiom,
defined(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_is_defined) ).
fof(f30,axiom,
defined(c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_is_defined) ).
fof(f31,axiom,
defined(d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d_is_defined) ).
fof(f32,negated_conjecture,
~ equalish(b,additive_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_not_equal_to_additive_identity_5) ).
fof(f33,negated_conjecture,
~ equalish(d,additive_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d_not_equal_to_additive_identity_6) ).
fof(f34,negated_conjecture,
equalish(multiply(a,d),multiply(b,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiply_equals_multiply_7) ).
fof(f35,negated_conjecture,
~ equalish(multiply(a,multiplicative_inverse(b)),multiply(c,multiplicative_inverse(d))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiply_not_equal_to_multiply_8) ).
fof(f36,definition,
sF0 = multiply(a,d),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f37,plain,
multiply(a,d) = sF0,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF1 = multiply(b,c),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f39,plain,
multiply(b,c) = sF1,
inference(reorient_equations,[],[f38]) ).
fof(f40,plain,
equalish(sF0,sF1),
inference(definition_folding,[],[f34,f39,f37]) ).
fof(f41,definition,
sF2 = multiplicative_inverse(b),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f42,plain,
multiplicative_inverse(b) = sF2,
inference(reorient_equations,[],[f41]) ).
fof(f43,definition,
sF3 = multiply(a,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f44,plain,
multiply(a,sF2) = sF3,
inference(reorient_equations,[],[f43]) ).
fof(f45,definition,
sF4 = multiplicative_inverse(d),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f46,plain,
multiplicative_inverse(d) = sF4,
inference(reorient_equations,[],[f45]) ).
fof(f47,definition,
sF5 = multiply(c,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f48,plain,
multiply(c,sF4) = sF5,
inference(reorient_equations,[],[f47]) ).
fof(f49,plain,
~ equalish(sF3,sF5),
inference(definition_folding,[],[f35,f48,f46,f44,f42]) ).
fof(f58,plain,
( ~ defined(b)
| defined(multiplicative_inverse(b)) ),
inference(resolution,[],[f15,f32]) ).
fof(f59,plain,
( ~ defined(d)
| defined(multiplicative_inverse(d)) ),
inference(resolution,[],[f15,f33]) ).
fof(f60,plain,
defined(multiplicative_inverse(d)),
inference(forward_subsumption_resolution,[],[f59,f31]) ).
fof(f61,plain,
defined(multiplicative_inverse(b)),
inference(forward_subsumption_resolution,[],[f58,f29]) ).
fof(f62,plain,
defined(sF4),
inference(forward_demodulation,[],[f60,f46]) ).
fof(f63,plain,
defined(sF2),
inference(forward_demodulation,[],[f61,f42]) ).
fof(f68,plain,
! [X0] :
( equalish(multiply(X0,sF2),sF3)
| ~ defined(sF2)
| ~ equalish(X0,a) ),
inference(superposition,[],[f25,f44]) ).
fof(f71,plain,
! [X0] :
( equalish(multiply(X0,sF2),sF3)
| ~ equalish(X0,a) ),
inference(forward_subsumption_resolution,[],[f68,f63]) ).
fof(f132,plain,
equalish(sF1,sF0),
inference(resolution,[],[f22,f40]) ).
fof(f136,plain,
! [X2,X3,X0,X1] :
( ~ equalish(X0,multiply(X1,X2))
| equalish(X0,multiply(X3,X2))
| ~ defined(X2)
| ~ equalish(X1,X3) ),
inference(resolution,[],[f23,f25]) ).
fof(f138,plain,
! [X0,X1] :
( ~ equalish(X0,multiply(X1,multiplicative_inverse(X1)))
| equalish(X0,multiplicative_identity)
| ~ defined(X1)
| equalish(X1,additive_identity) ),
inference(resolution,[],[f23,f7]) ).
fof(f139,plain,
! [X0,X1] :
( ~ equalish(X0,multiply(X1,sF2))
| equalish(X0,sF3)
| ~ equalish(X1,a) ),
inference(resolution,[],[f23,f71]) ).
fof(f160,plain,
! [X0,X1] :
( equalish(multiply(X0,sF2),sF3)
| ~ equalish(X1,a)
| ~ defined(sF2)
| ~ equalish(X0,X1) ),
inference(resolution,[],[f139,f25]) ).
fof(f165,plain,
! [X0,X1] :
( ~ equalish(X1,a)
| equalish(multiply(X0,sF2),sF3)
| ~ equalish(X0,X1) ),
inference(forward_subsumption_resolution,[],[f160,f63]) ).
fof(f207,definition,
( spl6_8
<=> equalish(sF5,sF3) ),
introduced(definition,[new_symbols(definition,[spl6_8])],[avatar_definition]) ).
fof(f209,plain,
( equalish(sF5,sF3)
| ~ spl6_8 ),
inference(avatar_component_clause,[],[f207]) ).
fof(f267,plain,
! [X0] :
( equalish(multiply(multiplicative_inverse(X0),X0),multiplicative_identity)
| ~ defined(X0)
| equalish(X0,additive_identity)
| ~ defined(multiplicative_inverse(X0))
| ~ defined(X0) ),
inference(resolution,[],[f138,f8]) ).
fof(f270,plain,
! [X0] :
( equalish(multiply(multiplicative_inverse(X0),X0),multiplicative_identity)
| ~ defined(X0)
| equalish(X0,additive_identity)
| ~ defined(multiplicative_inverse(X0)) ),
inference(duplicate_literal_removal,[],[f267]) ).
fof(f273,plain,
! [X0] :
( equalish(multiply(multiplicative_inverse(X0),X0),multiplicative_identity)
| ~ defined(X0)
| equalish(X0,additive_identity) ),
inference(forward_subsumption_resolution,[],[f270,f15]) ).
fof(f313,plain,
! [X0,X1] :
( ~ equalish(X1,multiply(multiplicative_identity,X0))
| ~ defined(X0)
| equalish(X1,X0) ),
inference(resolution,[],[f6,f23]) ).
fof(f359,plain,
! [X0,X1] :
( ~ defined(X0)
| equalish(multiply(X1,X0),X0)
| ~ defined(X0)
| ~ equalish(X1,multiplicative_identity) ),
inference(resolution,[],[f313,f25]) ).
fof(f365,plain,
! [X0,X1] :
( equalish(multiply(X1,X0),X0)
| ~ defined(X0)
| ~ equalish(X1,multiplicative_identity) ),
inference(duplicate_literal_removal,[],[f359]) ).
fof(f388,plain,
( defined(sF0)
| ~ defined(a)
| ~ defined(d) ),
inference(superposition,[],[f13,f37]) ).
fof(f393,plain,
( defined(sF0)
| ~ defined(d) ),
inference(forward_subsumption_resolution,[],[f388,f28]) ).
fof(f397,plain,
defined(sF0),
inference(forward_subsumption_resolution,[],[f393,f31]) ).
fof(f438,plain,
! [X2,X3,X0,X1] :
( ~ equalish(X3,multiply(X0,multiply(X1,X2)))
| ~ defined(X1)
| ~ defined(X2)
| ~ defined(X0)
| equalish(X3,multiply(multiply(X0,X1),X2)) ),
inference(resolution,[],[f5,f23]) ).
fof(f655,plain,
! [X2,X0,X1] :
( ~ defined(X0)
| ~ defined(X1)
| ~ defined(X2)
| equalish(multiply(multiply(X0,X1),X2),multiply(multiply(X2,X0),X1))
| ~ defined(multiply(X0,X1))
| ~ defined(X2) ),
inference(resolution,[],[f438,f8]) ).
fof(f664,plain,
! [X2,X0,X1] :
( ~ defined(X0)
| ~ defined(X1)
| ~ defined(X2)
| equalish(multiply(multiply(X0,X1),X2),multiply(multiply(X2,X0),X1))
| ~ defined(multiply(X0,X1)) ),
inference(duplicate_literal_removal,[],[f655]) ).
fof(f669,plain,
! [X2,X0,X1] :
( equalish(multiply(multiply(X0,X1),X2),multiply(multiply(X2,X0),X1))
| ~ defined(X1)
| ~ defined(X2)
| ~ defined(X0) ),
inference(forward_subsumption_resolution,[],[f664,f13]) ).
fof(f1159,plain,
! [X2,X0,X1] :
( ~ equalish(X2,multiply(X1,X0))
| ~ equalish(X1,multiplicative_identity)
| ~ defined(X0)
| equalish(X2,X0) ),
inference(resolution,[],[f365,f23]) ).
fof(f1206,plain,
! [X2,X0,X1] :
( ~ equalish(multiply(X0,X1),multiplicative_identity)
| ~ defined(X2)
| equalish(multiply(multiply(X1,X2),X0),X2)
| ~ defined(X2)
| ~ defined(X0)
| ~ defined(X1) ),
inference(resolution,[],[f1159,f669]) ).
fof(f1216,plain,
! [X2,X0,X1] :
( equalish(multiply(multiply(X1,X2),X0),X2)
| ~ defined(X2)
| ~ equalish(multiply(X0,X1),multiplicative_identity)
| ~ defined(X0)
| ~ defined(X1) ),
inference(duplicate_literal_removal,[],[f1206]) ).
fof(f1251,plain,
! [X2,X3,X0,X1] :
( ~ equalish(X3,multiply(multiply(X2,X0),X1))
| ~ equalish(multiply(X1,X2),multiplicative_identity)
| ~ defined(X1)
| ~ defined(X2)
| ~ defined(X0)
| equalish(X3,X0) ),
inference(resolution,[],[f1216,f23]) ).
fof(f1290,plain,
! [X2,X3,X0,X1] :
( ~ equalish(multiply(X0,X1),multiplicative_identity)
| ~ defined(X0)
| ~ defined(X1)
| ~ defined(X2)
| equalish(multiply(X3,X0),X2)
| ~ defined(X0)
| ~ equalish(X3,multiply(X1,X2)) ),
inference(resolution,[],[f1251,f25]) ).
fof(f1296,plain,
! [X2,X0,X1] :
( ~ equalish(multiply(X0,X1),multiplicative_identity)
| ~ defined(X0)
| ~ defined(X1)
| ~ defined(X2)
| equalish(multiply(multiply(X2,X0),X1),X2)
| ~ defined(X0)
| ~ defined(X1)
| ~ defined(X2) ),
inference(resolution,[],[f1251,f669]) ).
fof(f1306,plain,
! [X2,X0,X1] :
( equalish(multiply(multiply(X2,X0),X1),X2)
| ~ defined(X0)
| ~ defined(X1)
| ~ defined(X2)
| ~ equalish(multiply(X0,X1),multiplicative_identity) ),
inference(duplicate_literal_removal,[],[f1296]) ).
fof(f1311,plain,
! [X2,X3,X0,X1] :
( ~ equalish(multiply(X0,X1),multiplicative_identity)
| ~ defined(X0)
| ~ defined(X1)
| ~ defined(X2)
| equalish(multiply(X3,X0),X2)
| ~ equalish(X3,multiply(X1,X2)) ),
inference(duplicate_literal_removal,[],[f1290]) ).
fof(f1334,plain,
! [X2,X3,X0,X1] :
( ~ equalish(X3,multiply(multiply(X2,X0),X1))
| ~ defined(X1)
| ~ defined(X2)
| ~ equalish(multiply(X0,X1),multiplicative_identity)
| ~ defined(X0)
| equalish(X3,X2) ),
inference(resolution,[],[f1306,f23]) ).
fof(f1374,plain,
! [X2,X3,X0,X1] :
( ~ defined(X0)
| ~ defined(X1)
| ~ equalish(multiply(X2,X0),multiplicative_identity)
| ~ defined(X2)
| equalish(multiply(X3,X0),X1)
| ~ defined(X0)
| ~ equalish(X3,multiply(X1,X2)) ),
inference(resolution,[],[f1334,f25]) ).
fof(f1396,plain,
! [X2,X3,X0,X1] :
( ~ equalish(multiply(X2,X0),multiplicative_identity)
| ~ defined(X1)
| ~ defined(X0)
| ~ defined(X2)
| equalish(multiply(X3,X0),X1)
| ~ equalish(X3,multiply(X1,X2)) ),
inference(duplicate_literal_removal,[],[f1374]) ).
fof(f1432,plain,
! [X2,X0,X1] :
( ~ defined(X0)
| ~ defined(multiplicative_inverse(X0))
| ~ defined(X1)
| equalish(multiply(X2,X0),X1)
| ~ equalish(X2,multiply(multiplicative_inverse(X0),X1))
| ~ defined(X0)
| equalish(X0,additive_identity) ),
inference(resolution,[],[f1311,f7]) ).
fof(f1451,plain,
! [X2,X0,X1] :
( ~ defined(X0)
| ~ defined(multiplicative_inverse(X0))
| ~ defined(X1)
| equalish(multiply(X2,X0),X1)
| ~ equalish(X2,multiply(multiplicative_inverse(X0),X1))
| equalish(X0,additive_identity) ),
inference(duplicate_literal_removal,[],[f1432]) ).
fof(f1463,plain,
! [X2,X0,X1] :
( ~ equalish(X2,multiply(multiplicative_inverse(X0),X1))
| ~ defined(X1)
| equalish(multiply(X2,X0),X1)
| ~ defined(X0)
| equalish(X0,additive_identity) ),
inference(forward_subsumption_resolution,[],[f1451,f15]) ).
fof(f1486,plain,
! [X0,X1] :
( ~ defined(X0)
| equalish(multiply(multiply(X0,multiplicative_inverse(X1)),X1),X0)
| ~ defined(X1)
| equalish(X1,additive_identity)
| ~ defined(X0)
| ~ defined(multiplicative_inverse(X1)) ),
inference(resolution,[],[f1463,f8]) ).
fof(f1496,plain,
! [X0,X1] :
( ~ defined(X0)
| equalish(multiply(multiply(X0,multiplicative_inverse(X1)),X1),X0)
| ~ defined(X1)
| equalish(X1,additive_identity)
| ~ defined(multiplicative_inverse(X1)) ),
inference(duplicate_literal_removal,[],[f1486]) ).
fof(f1502,plain,
! [X0,X1] :
( equalish(multiply(multiply(X0,multiplicative_inverse(X1)),X1),X0)
| ~ defined(X0)
| ~ defined(X1)
| equalish(X1,additive_identity) ),
inference(forward_subsumption_resolution,[],[f1496,f15]) ).
fof(f1551,plain,
! [X2,X0,X1] :
( ~ defined(X0)
| ~ defined(X1)
| ~ defined(multiplicative_inverse(X1))
| equalish(multiply(X2,X1),X0)
| ~ equalish(X2,multiply(X0,multiplicative_inverse(X1)))
| ~ defined(X1)
| equalish(X1,additive_identity) ),
inference(resolution,[],[f1396,f273]) ).
fof(f1558,plain,
! [X2,X0,X1] :
( ~ defined(X0)
| ~ defined(X1)
| ~ defined(multiplicative_inverse(X1))
| equalish(multiply(X2,X1),X0)
| ~ equalish(X2,multiply(X0,multiplicative_inverse(X1)))
| equalish(X1,additive_identity) ),
inference(duplicate_literal_removal,[],[f1551]) ).
fof(f1566,plain,
! [X2,X0,X1] :
( ~ equalish(X2,multiply(X0,multiplicative_inverse(X1)))
| ~ defined(X1)
| equalish(multiply(X2,X1),X0)
| ~ defined(X0)
| equalish(X1,additive_identity) ),
inference(forward_subsumption_resolution,[],[f1558,f15]) ).
fof(f1618,plain,
! [X0,X1] :
( ~ defined(X0)
| equalish(multiply(multiply(multiplicative_inverse(X0),X1),X0),X1)
| ~ defined(X1)
| equalish(X0,additive_identity)
| ~ defined(multiplicative_inverse(X0))
| ~ defined(X1) ),
inference(resolution,[],[f1566,f8]) ).
fof(f1629,plain,
! [X0,X1] :
( ~ defined(X0)
| equalish(multiply(multiply(multiplicative_inverse(X0),X1),X0),X1)
| ~ defined(X1)
| equalish(X0,additive_identity)
| ~ defined(multiplicative_inverse(X0)) ),
inference(duplicate_literal_removal,[],[f1618]) ).
fof(f1634,plain,
! [X0,X1] :
( equalish(multiply(multiply(multiplicative_inverse(X0),X1),X0),X1)
| ~ defined(X0)
| ~ defined(X1)
| equalish(X0,additive_identity) ),
inference(forward_subsumption_resolution,[],[f1629,f15]) ).
fof(f2529,plain,
! [X2,X0,X1] :
( ~ equalish(X2,multiply(multiply(X0,multiplicative_inverse(X1)),X1))
| ~ defined(X1)
| equalish(X1,additive_identity)
| ~ defined(X0)
| equalish(X2,X0) ),
inference(resolution,[],[f1502,f23]) ).
fof(f2598,plain,
! [X0,X1] :
( ~ defined(X0)
| equalish(X0,additive_identity)
| ~ defined(X1)
| equalish(multiply(multiply(multiplicative_inverse(X0),X0),X1),X1)
| ~ defined(X0)
| ~ defined(X1)
| ~ defined(multiplicative_inverse(X0)) ),
inference(resolution,[],[f2529,f669]) ).
fof(f2609,plain,
! [X0,X1] :
( ~ defined(X0)
| equalish(X0,additive_identity)
| ~ defined(X1)
| equalish(multiply(multiply(multiplicative_inverse(X0),X0),X1),X1)
| ~ defined(multiplicative_inverse(X0)) ),
inference(duplicate_literal_removal,[],[f2598]) ).
fof(f2618,plain,
! [X0,X1] :
( equalish(multiply(multiply(multiplicative_inverse(X0),X0),X1),X1)
| equalish(X0,additive_identity)
| ~ defined(X1)
| ~ defined(X0) ),
inference(forward_subsumption_resolution,[],[f2609,f15]) ).
fof(f2628,plain,
! [X2,X0,X1] :
( ~ equalish(X2,multiply(multiply(multiplicative_inverse(X0),X0),X1))
| ~ defined(X1)
| ~ defined(X0)
| equalish(X0,additive_identity)
| equalish(X2,X1) ),
inference(resolution,[],[f2618,f23]) ).
fof(f3346,plain,
! [X0,X1] :
( ~ defined(X0)
| ~ defined(X1)
| equalish(X1,additive_identity)
| equalish(multiply(multiply(X1,X0),multiplicative_inverse(X1)),X0)
| ~ defined(X0)
| ~ defined(multiplicative_inverse(X1))
| ~ defined(X1) ),
inference(resolution,[],[f2628,f669]) ).
fof(f3363,plain,
! [X0,X1] :
( ~ defined(X0)
| ~ defined(X1)
| equalish(X1,additive_identity)
| equalish(multiply(multiply(X1,X0),multiplicative_inverse(X1)),X0)
| ~ defined(multiplicative_inverse(X1)) ),
inference(duplicate_literal_removal,[],[f3346]) ).
fof(f3373,plain,
! [X0,X1] :
( equalish(multiply(multiply(X1,X0),multiplicative_inverse(X1)),X0)
| ~ defined(X1)
| equalish(X1,additive_identity)
| ~ defined(X0) ),
inference(forward_subsumption_resolution,[],[f3363,f15]) ).
fof(f3383,plain,
! [X0,X1] :
( equalish(X1,multiply(multiply(X0,X1),multiplicative_inverse(X0)))
| equalish(X0,additive_identity)
| ~ defined(X1)
| ~ defined(X0) ),
inference(resolution,[],[f3373,f22]) ).
fof(f3481,plain,
( equalish(c,multiply(sF1,multiplicative_inverse(b)))
| equalish(b,additive_identity)
| ~ defined(c)
| ~ defined(b) ),
inference(superposition,[],[f3383,f39]) ).
fof(f3495,plain,
( equalish(c,multiply(sF1,multiplicative_inverse(b)))
| ~ defined(c)
| ~ defined(b) ),
inference(forward_subsumption_resolution,[],[f3481,f32]) ).
fof(f3507,plain,
( equalish(c,multiply(sF1,multiplicative_inverse(b)))
| ~ defined(b) ),
inference(forward_subsumption_resolution,[],[f3495,f30]) ).
fof(f3514,plain,
equalish(c,multiply(sF1,multiplicative_inverse(b))),
inference(forward_subsumption_resolution,[],[f3507,f29]) ).
fof(f3515,plain,
equalish(c,multiply(sF1,sF2)),
inference(forward_demodulation,[],[f3514,f42]) ).
fof(f3564,plain,
! [X0] :
( equalish(c,multiply(X0,sF2))
| ~ defined(sF2)
| ~ equalish(sF1,X0) ),
inference(resolution,[],[f3515,f136]) ).
fof(f3599,plain,
! [X0] :
( equalish(c,multiply(X0,sF2))
| ~ equalish(sF1,X0) ),
inference(forward_subsumption_resolution,[],[f3564,f63]) ).
fof(f6510,plain,
! [X2,X0,X1] :
( ~ equalish(X2,multiply(multiply(multiplicative_inverse(X0),X1),X0))
| ~ defined(X1)
| equalish(X0,additive_identity)
| ~ defined(X0)
| equalish(X2,X1) ),
inference(resolution,[],[f1634,f23]) ).
fof(f6752,plain,
! [X0,X1] :
( ~ defined(X0)
| equalish(X1,additive_identity)
| ~ defined(X1)
| equalish(multiply(multiply(X0,X1),multiplicative_inverse(X1)),X0)
| ~ defined(X1)
| ~ defined(multiplicative_inverse(X1))
| ~ defined(X0) ),
inference(resolution,[],[f6510,f669]) ).
fof(f6776,plain,
! [X0,X1] :
( ~ defined(X0)
| equalish(X1,additive_identity)
| ~ defined(X1)
| equalish(multiply(multiply(X0,X1),multiplicative_inverse(X1)),X0)
| ~ defined(multiplicative_inverse(X1)) ),
inference(duplicate_literal_removal,[],[f6752]) ).
fof(f6789,plain,
! [X0,X1] :
( equalish(multiply(multiply(X0,X1),multiplicative_inverse(X1)),X0)
| equalish(X1,additive_identity)
| ~ defined(X1)
| ~ defined(X0) ),
inference(forward_subsumption_resolution,[],[f6776,f15]) ).
fof(f6887,plain,
! [X0] :
( equalish(multiply(multiply(X0,d),sF4),X0)
| equalish(d,additive_identity)
| ~ defined(d)
| ~ defined(X0) ),
inference(superposition,[],[f6789,f46]) ).
fof(f6889,plain,
! [X0] :
( equalish(multiply(multiply(X0,d),sF4),X0)
| ~ defined(d)
| ~ defined(X0) ),
inference(forward_subsumption_resolution,[],[f6887,f33]) ).
fof(f6908,plain,
! [X0] :
( equalish(multiply(multiply(X0,d),sF4),X0)
| ~ defined(X0) ),
inference(forward_subsumption_resolution,[],[f6889,f31]) ).
fof(f7410,plain,
! [X0] :
( ~ defined(a)
| equalish(multiply(X0,sF2),sF3)
| ~ equalish(X0,multiply(multiply(a,d),sF4)) ),
inference(resolution,[],[f6908,f165]) ).
fof(f7419,plain,
! [X0] :
( equalish(multiply(X0,sF2),sF3)
| ~ equalish(X0,multiply(multiply(a,d),sF4)) ),
inference(forward_subsumption_resolution,[],[f7410,f28]) ).
fof(f7450,plain,
! [X0] :
( ~ equalish(X0,multiply(sF0,sF4))
| equalish(multiply(X0,sF2),sF3) ),
inference(forward_demodulation,[],[f7419,f37]) ).
fof(f7543,plain,
( equalish(multiply(multiply(sF4,sF0),sF2),sF3)
| ~ defined(sF4)
| ~ defined(sF0) ),
inference(resolution,[],[f7450,f8]) ).
fof(f7572,plain,
( equalish(multiply(multiply(sF4,sF0),sF2),sF3)
| ~ defined(sF0) ),
inference(forward_subsumption_resolution,[],[f7543,f62]) ).
fof(f7575,plain,
equalish(multiply(multiply(sF4,sF0),sF2),sF3),
inference(forward_subsumption_resolution,[],[f7572,f397]) ).
fof(f7975,plain,
! [X0] :
( ~ equalish(X0,multiply(multiply(sF4,sF0),sF2))
| equalish(X0,sF3) ),
inference(resolution,[],[f7575,f23]) ).
fof(f7989,plain,
( equalish(multiply(multiply(sF0,sF2),sF4),sF3)
| ~ defined(sF2)
| ~ defined(sF4)
| ~ defined(sF0) ),
inference(resolution,[],[f7975,f669]) ).
fof(f8097,plain,
( equalish(multiply(multiply(sF0,sF2),sF4),sF3)
| ~ defined(sF4)
| ~ defined(sF0) ),
inference(forward_subsumption_resolution,[],[f7989,f63]) ).
fof(f8131,plain,
( equalish(multiply(multiply(sF0,sF2),sF4),sF3)
| ~ defined(sF0) ),
inference(forward_subsumption_resolution,[],[f8097,f62]) ).
fof(f8143,plain,
equalish(multiply(multiply(sF0,sF2),sF4),sF3),
inference(forward_subsumption_resolution,[],[f8131,f397]) ).
fof(f9111,plain,
! [X0] :
( ~ equalish(X0,multiply(multiply(sF0,sF2),sF4))
| equalish(X0,sF3) ),
inference(resolution,[],[f8143,f23]) ).
fof(f9115,plain,
! [X0] :
( equalish(multiply(X0,sF4),sF3)
| ~ defined(sF4)
| ~ equalish(X0,multiply(sF0,sF2)) ),
inference(resolution,[],[f9111,f25]) ).
fof(f9268,plain,
! [X0] :
( ~ equalish(X0,multiply(sF0,sF2))
| equalish(multiply(X0,sF4),sF3) ),
inference(forward_subsumption_resolution,[],[f9115,f62]) ).
fof(f9311,plain,
( equalish(multiply(c,sF4),sF3)
| ~ equalish(sF1,sF0) ),
inference(resolution,[],[f9268,f3599]) ).
fof(f9322,plain,
equalish(multiply(c,sF4),sF3),
inference(forward_subsumption_resolution,[],[f9311,f132]) ).
fof(f9327,plain,
equalish(sF5,sF3),
inference(forward_demodulation,[],[f9322,f48]) ).
fof(f9338,plain,
spl6_8,
inference(avatar_split_clause,[],[f9327,f207]) ).
fof(f9705,plain,
( equalish(sF3,sF5)
| ~ spl6_8 ),
inference(resolution,[],[f209,f22]) ).
fof(f9706,plain,
( $false
| ~ spl6_8 ),
inference(forward_subsumption_resolution,[],[f9705,f49]) ).
fof(f9707,plain,
~ spl6_8,
inference(avatar_contradiction_clause,[],[f9706]) ).
cnf(s372,plain,
spl6_8,
inference(sat_conversion,[],[f9338]) ).
cnf(s402,plain,
~ spl6_8,
inference(sat_conversion,[],[f9707]) ).
cnf(s403,plain,
$false,
inference(rat,[],[s372,s402]) ).
fof(f9708,plain,
$false,
inference(avatar_sat_refutation,[],[s403]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : FLD050-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n005.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 00:39:17 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.15/1.89 % (1332278)Input is clausal, will run a generic CNF schedule.
% 7.15/1.89 % (1332285)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1638282042:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.15/1.89 % (1332288)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3537657127:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.15/1.89 % (1332284)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1928576085:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.15/1.89 % (1332289)dis-21_1_sil=8000:lcm=predicate:random_seed=1973493452:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 7.15/1.89 % (1332286)lrs+10_1_sil=8000:sp=occurrence:random_seed=2111730718:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.15/1.89 % (1332287)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2348213457:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.15/1.89 % (1332283)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1563200178:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.15/1.89 % (1332286)Instruction limit reached!
% 7.15/1.89 % (1332286)------------------------------
% 7.15/1.89 % (1332286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.15/1.89 % (1332286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.15/1.89 % (1332286)CaDiCaL version: 2.1.3
% 7.15/1.89 % (1332286)Termination reason: Instruction limit
% 7.15/1.89 % (1332286)Termination phase: Saturation
% 7.15/1.89 % (1332286)Time elapsed: 0.068 s
% 7.15/1.89 % (1332286)Peak memory usage: 89 MB
% 7.15/1.89 % (1332286)Instructions burned: 107 (million)
% 7.15/1.89 % (1332287)Instruction limit reached!
% 7.15/1.89 % (1332287)------------------------------
% 7.15/1.89 % (1332287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.15/1.89 % (1332287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.15/1.89 % (1332287)CaDiCaL version: 2.1.3
% 7.15/1.89 % (1332287)Termination reason: Instruction limit
% 7.15/1.89 % (1332287)Termination phase: Saturation
% 7.15/1.89 % (1332287)Time elapsed: 0.069 s
% 7.15/1.89 % (1332287)Peak memory usage: 88 MB
% 7.15/1.89 % (1332287)Instructions burned: 115 (million)
% 7.15/1.89 % (1332289)Instruction limit reached!
% 7.15/1.89 % (1332289)------------------------------
% 7.15/1.89 % (1332289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.15/1.89 % (1332289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.15/1.89 % (1332289)CaDiCaL version: 2.1.3
% 7.15/1.89 % (1332289)Termination reason: Instruction limit
% 7.15/1.89 % (1332289)Termination phase: Saturation
% 7.15/1.89 % (1332289)Time elapsed: 0.074 s
% 7.15/1.89 % (1332289)Peak memory usage: 89 MB
% 7.15/1.89 % (1332289)Instructions burned: 118 (million)
% 7.15/1.89 % (1332288)Instruction limit reached!
% 7.15/1.89 % (1332288)------------------------------
% 7.15/1.89 % (1332288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.15/1.89 % (1332288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.15/1.89 % (1332288)CaDiCaL version: 2.1.3
% 7.15/1.89 % (1332288)Termination reason: Instruction limit
% 7.15/1.89 % (1332288)Termination phase: Saturation
% 7.15/1.89 % (1332288)Time elapsed: 0.120 s
% 7.15/1.89 % (1332288)Peak memory usage: 89 MB
% 7.15/1.89 % (1332288)Instructions burned: 180 (million)
% 7.15/1.89 % (1332297)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3859666941:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 7.15/1.89 % (1332299)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3047843513:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 7.15/1.89 % (1332298)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3228459984:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 7.15/1.89 % (1332300)lrs+10_64_to=lpo:sil=8000:random_seed=256984874:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 7.15/1.89 % (1332297)Instruction limit reached!
% 14.02/2.69 % (1332297)------------------------------
% 14.02/2.69 % (1332297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.02/2.69 % (1332297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.02/2.69 % (1332297)CaDiCaL version: 2.1.3
% 14.02/2.69 % (1332297)Termination reason: Instruction limit
% 14.02/2.69 % (1332297)Termination phase: Saturation
% 14.02/2.69 % (1332297)Time elapsed: 0.067 s
% 14.02/2.69 % (1332297)Peak memory usage: 89 MB
% 14.02/2.69 % (1332297)Instructions burned: 146 (million)
% 14.02/2.69 % (1332298)Instruction limit reached!
% 14.02/2.69 % (1332298)------------------------------
% 14.02/2.69 % (1332298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.02/2.69 % (1332298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.02/2.69 % (1332298)CaDiCaL version: 2.1.3
% 14.02/2.69 % (1332298)Termination reason: Instruction limit
% 14.02/2.69 % (1332298)Termination phase: Saturation
% 14.02/2.69 % (1332298)Time elapsed: 0.096 s
% 14.02/2.69 % (1332298)Peak memory usage: 94 MB
% 14.02/2.69 % (1332298)Instructions burned: 190 (million)
% 14.02/2.69 % (1332300)Instruction limit reached!
% 14.02/2.69 % (1332300)------------------------------
% 14.02/2.69 % (1332300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.02/2.69 % (1332300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.02/2.69 % (1332300)CaDiCaL version: 2.1.3
% 14.02/2.69 % (1332300)Termination reason: Instruction limit
% 14.02/2.69 % (1332300)Termination phase: Saturation
% 14.02/2.69 % (1332300)Time elapsed: 0.077 s
% 14.02/2.69 % (1332300)Peak memory usage: 89 MB
% 14.02/2.69 % (1332300)Instructions burned: 127 (million)
% 14.02/2.69 % (1332299)Instruction limit reached!
% 14.02/2.69 % (1332299)------------------------------
% 14.02/2.69 % (1332299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.02/2.69 % (1332299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.02/2.69 % (1332299)CaDiCaL version: 2.1.3
% 14.02/2.69 % (1332299)Termination reason: Instruction limit
% 14.02/2.69 % (1332299)Termination phase: Saturation
% 14.02/2.69 % (1332299)Time elapsed: 0.148 s
% 14.02/2.69 % (1332299)Peak memory usage: 90 MB
% 14.02/2.69 % (1332299)Instructions burned: 220 (million)
% 14.02/2.69 % (1332305)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1772990130:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 14.02/2.69 % (1332305)Instruction limit reached!
% 14.02/2.69 % (1332305)------------------------------
% 14.02/2.69 % (1332305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.02/2.69 % (1332305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.02/2.69 % (1332305)CaDiCaL version: 2.1.3
% 14.02/2.69 % (1332305)Termination reason: Instruction limit
% 14.02/2.69 % (1332305)Termination phase: Saturation
% 14.02/2.69 % (1332305)Time elapsed: 0.061 s
% 14.02/2.69 % (1332305)Peak memory usage: 89 MB
% 14.02/2.69 % (1332305)Instructions burned: 196 (million)
% 14.02/2.69 % (1332306)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3829723901:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 14.02/2.69 % (1332307)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4256085820:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 14.02/2.69 % (1332309)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3855699558:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 14.02/2.69 % (1332310)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=735041765:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 14.02/2.69 % (1332309)Instruction limit reached!
% 14.02/2.69 % (1332309)------------------------------
% 14.02/2.69 % (1332309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.02/2.69 % (1332309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.02/2.69 % (1332309)CaDiCaL version: 2.1.3
% 14.02/2.69 % (1332309)Termination reason: Instruction limit
% 14.02/2.69 % (1332309)Termination phase: Saturation
% 14.02/2.69 % (1332309)Time elapsed: 0.056 s
% 14.02/2.69 % (1332309)Peak memory usage: 91 MB
% 14.02/2.69 % (1332309)Instructions burned: 108 (million)
% 14.02/2.69 % (1332306)Instruction limit reached!
% 14.02/2.69 % (1332306)------------------------------
% 14.02/2.69 % (1332306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.02/2.69 % (1332306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.02/2.69 % (1332306)CaDiCaL version: 2.1.3
% 14.02/2.69 % (1332306)Termination reason: Instruction limit
% 14.02/2.69 % (1332306)Termination phase: Saturation
% 14.02/2.69 % (1332306)Time elapsed: 0.113 s
% 14.02/2.69 % (1332306)Peak memory usage: 91 MB
% 14.02/2.69 % (1332306)Instructions burned: 158 (million)
% 14.02/2.69 % (1332310)Instruction limit reached!
% 14.02/2.69 % (1332310)------------------------------
% 14.02/2.69 % (1332310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.02/2.69 % (1332310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.02/2.69 % (1332310)CaDiCaL version: 2.1.3
% 14.02/2.69 % (1332310)Termination reason: Instruction limit
% 14.02/2.69 % (1332310)Termination phase: Saturation
% 14.02/2.69 % (1332310)Time elapsed: 0.034 s
% 14.02/2.69 % (1332310)Peak memory usage: 88 MB
% 14.02/2.69 % (1332310)Instructions burned: 111 (million)
% 14.02/2.69 % (1332317)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=209079469:i=134:sd=2:doe=on:ss=axioms:sgt=14_2993 on theBenchmark for (2993ds/134Mi)
% 14.02/2.69 % (1332315)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1410201756:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 14.02/2.69 % (1332317)Instruction limit reached!
% 14.02/2.69 % (1332317)------------------------------
% 14.02/2.69 % (1332317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.02/2.69 % (1332317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.02/2.69 % (1332317)CaDiCaL version: 2.1.3
% 14.02/2.69 % (1332317)Termination reason: Instruction limit
% 14.02/2.69 % (1332317)Termination phase: Saturation
% 14.02/2.69 % (1332317)Time elapsed: 0.047 s
% 14.02/2.69 % (1332317)Peak memory usage: 89 MB
% 14.02/2.69 % (1332317)Instructions burned: 135 (million)
% 14.02/2.69 % (1332316)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=524459527:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 14.02/2.69 % (1332321)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=816025725:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi)
% 14.02/2.69 % (1332315)Instruction limit reached!
% 14.02/2.69 % (1332315)------------------------------
% 14.02/2.69 % (1332315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.02/2.69 % (1332315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.02/2.69 % (1332315)CaDiCaL version: 2.1.3
% 14.02/2.69 % (1332315)Termination reason: Instruction limit
% 14.02/2.69 % (1332315)Termination phase: Saturation
% 14.02/2.69 % (1332315)Time elapsed: 0.166 s
% 14.02/2.69 % (1332315)Peak memory usage: 89 MB
% 14.02/2.69 % (1332315)Instructions burned: 242 (million)
% 14.02/2.69 % (1332321)Instruction limit reached!
% 14.02/2.69 % (1332321)------------------------------
% 14.02/2.69 % (1332321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.02/2.69 % (1332321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.02/2.69 % (1332321)CaDiCaL version: 2.1.3
% 14.02/2.69 % (1332321)Termination reason: Instruction limit
% 14.02/2.69 % (1332321)Termination phase: Saturation
% 14.02/2.69 % (1332321)Time elapsed: 0.130 s
% 14.02/2.69 % (1332321)Peak memory usage: 106 MB
% 14.02/2.69 % (1332321)Instructions burned: 500 (million)
% 14.02/2.69 % (1332323)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1273859801:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi)
% 14.02/2.69 % (1332324)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=439716254:i=264:kws=precedence:fsr=off_2989 on theBenchmark for (2989ds/264Mi)
% 14.02/2.69 % (1332324)Instruction limit reached!
% 14.02/2.69 % (1332324)------------------------------
% 14.02/2.69 % (1332324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.02/2.69 % (1332324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.02/2.69 % (1332324)CaDiCaL version: 2.1.3
% 14.02/2.69 % (1332324)Termination reason: Instruction limit
% 14.02/2.69 % (1332324)Termination phase: Saturation
% 14.02/2.69 % (1332324)Time elapsed: 0.085 s
% 14.02/2.69 % (1332324)Peak memory usage: 89 MB
% 14.02/2.69 % (1332324)Instructions burned: 266 (million)
% 14.02/2.69 % (1332323)Instruction limit reached!
% 14.02/2.69 % (1332323)------------------------------
% 14.02/2.69 % (1332323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.02/2.69 % (1332323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.02/2.69 % (1332323)CaDiCaL version: 2.1.3
% 14.02/2.69 % (1332323)Termination reason: Instruction limit
% 14.02/2.69 % (1332323)Termination phase: Saturation
% 14.02/2.69 % (1332323)Time elapsed: 0.122 s
% 14.02/2.69 % (1332323)Peak memory usage: 91 MB
% 14.02/2.69 % (1332323)Instructions burned: 191 (million)
% 14.02/2.69 % (1332327)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2338434927:cond=on:i=156:bs=on:gtg=exists_all:er=known_2987 on theBenchmark for (2987ds/156Mi)
% 14.02/2.69 % (1332327)Instruction limit reached!
% 14.02/2.69 % (1332327)------------------------------
% 14.02/2.69 % (1332327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.02/2.69 % (1332327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.02/2.69 % (1332327)CaDiCaL version: 2.1.3
% 14.02/2.69 % (1332327)Termination reason: Instruction limit
% 14.02/2.69 % (1332327)Termination phase: Saturation
% 14.02/2.69 % (1332327)Time elapsed: 0.036 s
% 14.02/2.69 % (1332327)Peak memory usage: 88 MB
% 14.02/2.69 % (1332327)Instructions burned: 161 (million)
% 14.02/2.69 % (1332328)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1513267465:i=3256:kws=precedence:bd=preordered:av=off_2987 on theBenchmark for (2987ds/3256Mi)
% 14.02/2.69 % (1332330)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2265573696:i=537:av=off:ss=included_2986 on theBenchmark for (2986ds/537Mi)
% 14.02/2.69 % (1332283)First to succeed.
% 14.02/2.69 % (1332283)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1332278"
% 14.02/2.69 % (1332330)Instruction limit reached!
% 14.02/2.69 % (1332330)------------------------------
% 14.02/2.69 % (1332330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.02/2.69 % (1332330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.02/2.69 % (1332330)CaDiCaL version: 2.1.3
% 14.02/2.69 % (1332330)Termination reason: Instruction limit
% 14.02/2.69 % (1332330)Termination phase: Saturation
% 14.02/2.69 % (1332330)Time elapsed: 0.333 s
% 14.02/2.69 % (1332330)Peak memory usage: 91 MB
% 14.02/2.69 % (1332330)Instructions burned: 538 (million)
% 14.02/2.69 % (1332333)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3386115147:i=180:bd=preordered:av=off_2981 on theBenchmark for (2981ds/180Mi)
% 14.02/2.69 % (1332283)Refutation found. Thanks to Tanya!
% 14.02/2.69 % SZS status Unsatisfiable for theBenchmark
% 14.02/2.69 % SZS output start Proof for theBenchmark
% See solution above
% 14.93/2.89 % (1332283)------------------------------
% 14.93/2.89 % (1332283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.93/2.89 % (1332283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.93/2.89 % (1332283)CaDiCaL version: 2.1.3
% 14.93/2.89 % (1332283)Termination reason: Refutation
% 14.93/2.89 % (1332283)Time elapsed: 1.625 s
% 14.93/2.89 % (1332283)Peak memory usage: 145 MB
% 14.93/2.89 % (1332283)Instructions burned: 2587 (million)
% 14.93/2.89 % (1332283)------------------------------
% 14.93/2.89 % (1332283)------------------------------
% 14.93/2.89 % (1332278)Success in time 2.034 s
% 14.93/2.89 % Vampire exiting
%------------------------------------------------------------------------------