%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : FLD049-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 : n012.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:12 AM UTC 2026
% Result : Unsatisfiable 6.28s 2.13s
% Output : Refutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 24
% Syntax : Number of formulae : 137 ( 33 unt; 7 def)
% Number of atoms : 421 ( 12 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 552 ( 268 ~; 283 |; 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,multiplicative_inverse(b)),multiply(c,multiplicative_inverse(d))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiply_equals_multiply_7) ).
fof(f35,negated_conjecture,
~ equalish(multiply(a,d),multiply(b,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiply_not_equal_to_multiply_8) ).
fof(f36,definition,
sF0 = multiplicative_inverse(b),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f37,plain,
multiplicative_inverse(b) = sF0,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF1 = multiply(a,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f39,plain,
multiply(a,sF0) = sF1,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF2 = multiplicative_inverse(d),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f41,plain,
multiplicative_inverse(d) = sF2,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF3 = multiply(c,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f43,plain,
multiply(c,sF2) = sF3,
inference(reorient_equations,[],[f42]) ).
fof(f44,plain,
equalish(sF1,sF3),
inference(definition_folding,[],[f34,f43,f41,f39,f37]) ).
fof(f45,definition,
sF4 = multiply(a,d),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f46,plain,
multiply(a,d) = sF4,
inference(reorient_equations,[],[f45]) ).
fof(f47,definition,
sF5 = multiply(b,c),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f48,plain,
multiply(b,c) = sF5,
inference(reorient_equations,[],[f47]) ).
fof(f49,plain,
~ equalish(sF4,sF5),
inference(definition_folding,[],[f35,f48,f46]) ).
fof(f57,plain,
! [X0] :
( equalish(multiply(X0,d),sF4)
| ~ defined(d)
| ~ equalish(X0,a) ),
inference(superposition,[],[f25,f46]) ).
fof(f58,plain,
! [X0] :
( equalish(multiply(X0,d),sF4)
| ~ equalish(X0,a) ),
inference(forward_subsumption_resolution,[],[f57,f31]) ).
fof(f60,definition,
( spl6_1
<=> defined(sF0) ),
introduced(definition,[new_symbols(definition,[spl6_1])],[avatar_definition]) ).
fof(f61,plain,
( defined(sF0)
| ~ spl6_1 ),
inference(avatar_component_clause,[],[f60]) ).
fof(f62,plain,
( ~ defined(sF0)
| spl6_1 ),
inference(avatar_component_clause,[],[f60]) ).
fof(f96,plain,
( ~ defined(b)
| defined(multiplicative_inverse(b)) ),
inference(resolution,[],[f15,f32]) ).
fof(f99,plain,
defined(multiplicative_inverse(b)),
inference(forward_subsumption_resolution,[],[f96,f29]) ).
fof(f101,plain,
defined(sF0),
inference(forward_demodulation,[],[f99,f37]) ).
fof(f104,plain,
( $false
| spl6_1 ),
inference(forward_subsumption_resolution,[],[f101,f62]) ).
fof(f105,plain,
spl6_1,
inference(avatar_contradiction_clause,[],[f104]) ).
fof(f110,plain,
( equalish(multiply(c,b),sF5)
| ~ defined(c)
| ~ defined(b) ),
inference(superposition,[],[f8,f48]) ).
fof(f117,plain,
( equalish(multiply(c,b),sF5)
| ~ defined(b) ),
inference(forward_subsumption_resolution,[],[f110,f30]) ).
fof(f125,plain,
equalish(multiply(c,b),sF5),
inference(forward_subsumption_resolution,[],[f117,f29]) ).
fof(f136,plain,
equalish(sF3,sF1),
inference(resolution,[],[f22,f44]) ).
fof(f146,plain,
! [X0,X1] :
( ~ equalish(X0,multiply(X1,d))
| equalish(X0,sF4)
| ~ equalish(X1,a) ),
inference(resolution,[],[f23,f58]) ).
fof(f148,plain,
! [X0] :
( ~ equalish(X0,multiply(c,b))
| equalish(X0,sF5) ),
inference(resolution,[],[f23,f125]) ).
fof(f152,plain,
! [X0,X1] :
( equalish(multiply(X0,d),sF4)
| ~ equalish(X1,a)
| ~ defined(d)
| ~ equalish(X0,X1) ),
inference(resolution,[],[f146,f25]) ).
fof(f156,plain,
! [X0,X1] :
( ~ equalish(X1,a)
| equalish(multiply(X0,d),sF4)
| ~ equalish(X0,X1) ),
inference(forward_subsumption_resolution,[],[f152,f31]) ).
fof(f170,plain,
! [X0] :
( equalish(multiply(X0,b),sF5)
| ~ defined(b)
| ~ equalish(X0,c) ),
inference(resolution,[],[f148,f25]) ).
fof(f173,plain,
! [X0] :
( equalish(multiply(X0,b),sF5)
| ~ equalish(X0,c) ),
inference(forward_subsumption_resolution,[],[f170,f29]) ).
fof(f176,plain,
! [X0,X1] :
( ~ equalish(X1,multiply(X0,b))
| ~ equalish(X0,c)
| equalish(X1,sF5) ),
inference(resolution,[],[f173,f23]) ).
fof(f401,plain,
! [X0,X1] :
( ~ equalish(X1,multiply(multiplicative_identity,X0))
| ~ defined(X0)
| equalish(X1,X0) ),
inference(resolution,[],[f6,f23]) ).
fof(f422,plain,
( defined(sF1)
| ~ defined(a)
| ~ defined(sF0) ),
inference(superposition,[],[f13,f39]) ).
fof(f425,plain,
( defined(sF1)
| ~ defined(sF0) ),
inference(forward_subsumption_resolution,[],[f422,f28]) ).
fof(f429,plain,
( defined(sF1)
| ~ spl6_1 ),
inference(forward_subsumption_resolution,[],[f425,f61]) ).
fof(f432,plain,
! [X0,X1] :
( ~ defined(X0)
| equalish(multiply(X1,X0),X0)
| ~ defined(X0)
| ~ equalish(X1,multiplicative_identity) ),
inference(resolution,[],[f401,f25]) ).
fof(f437,plain,
! [X0,X1] :
( equalish(multiply(X1,X0),X0)
| ~ defined(X0)
| ~ equalish(X1,multiplicative_identity) ),
inference(duplicate_literal_removal,[],[f432]) ).
fof(f539,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(f1026,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,[],[f539,f8]) ).
fof(f1035,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,[],[f1026]) ).
fof(f1041,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,[],[f1035,f13]) ).
fof(f1226,plain,
! [X2,X0,X1] :
( ~ equalish(X2,multiply(X1,X0))
| ~ equalish(X1,multiplicative_identity)
| ~ defined(X0)
| equalish(X2,X0) ),
inference(resolution,[],[f437,f23]) ).
fof(f1278,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,[],[f1226,f1041]) ).
fof(f1285,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,[],[f1278]) ).
fof(f1299,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,[],[f1285,f23]) ).
fof(f1343,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,[],[f1299,f25]) ).
fof(f1347,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,[],[f1299,f1041]) ).
fof(f1356,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,[],[f1347]) ).
fof(f1359,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,[],[f1343]) ).
fof(f1375,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,[],[f1356,f23]) ).
fof(f1420,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,[],[f1375,f25]) ).
fof(f1437,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,[],[f1420]) ).
fof(f1450,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,[],[f1359,f7]) ).
fof(f1467,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,[],[f1450]) ).
fof(f1479,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,[],[f1467,f15]) ).
fof(f1520,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,[],[f1479,f8]) ).
fof(f1529,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,[],[f1520]) ).
fof(f1534,plain,
! [X0,X1] :
( equalish(multiply(multiply(X0,multiplicative_inverse(X1)),X1),X0)
| ~ defined(X0)
| ~ defined(X1)
| equalish(X1,additive_identity) ),
inference(forward_subsumption_resolution,[],[f1529,f15]) ).
fof(f1582,plain,
! [X2,X0,X1] :
( ~ defined(X0)
| ~ defined(multiplicative_inverse(X1))
| ~ defined(X1)
| equalish(multiply(X2,multiplicative_inverse(X1)),X0)
| ~ equalish(X2,multiply(X0,X1))
| ~ defined(X1)
| equalish(X1,additive_identity) ),
inference(resolution,[],[f1437,f7]) ).
fof(f1600,plain,
! [X2,X0,X1] :
( ~ defined(X0)
| ~ defined(multiplicative_inverse(X1))
| ~ defined(X1)
| equalish(multiply(X2,multiplicative_inverse(X1)),X0)
| ~ equalish(X2,multiply(X0,X1))
| equalish(X1,additive_identity) ),
inference(duplicate_literal_removal,[],[f1582]) ).
fof(f1609,plain,
! [X2,X0,X1] :
( equalish(multiply(X2,multiplicative_inverse(X1)),X0)
| ~ defined(X1)
| ~ defined(X0)
| ~ equalish(X2,multiply(X0,X1))
| equalish(X1,additive_identity) ),
inference(forward_subsumption_resolution,[],[f1600,f15]) ).
fof(f1649,plain,
! [X2,X0,X1] :
( ~ defined(X0)
| ~ defined(a)
| ~ equalish(X1,multiply(a,X0))
| equalish(X0,additive_identity)
| equalish(multiply(X2,d),sF4)
| ~ equalish(X2,multiply(X1,multiplicative_inverse(X0))) ),
inference(resolution,[],[f1609,f156]) ).
fof(f1652,plain,
! [X2,X0,X1] :
( ~ equalish(X2,multiply(X1,multiplicative_inverse(X0)))
| ~ equalish(X1,multiply(a,X0))
| equalish(X0,additive_identity)
| equalish(multiply(X2,d),sF4)
| ~ defined(X0) ),
inference(forward_subsumption_resolution,[],[f1649,f28]) ).
fof(f2301,plain,
! [X0,X1] :
( ~ equalish(X0,multiply(X1,sF0))
| ~ equalish(X1,multiply(a,b))
| equalish(b,additive_identity)
| equalish(multiply(X0,d),sF4)
| ~ defined(b) ),
inference(superposition,[],[f1652,f37]) ).
fof(f2306,plain,
! [X0,X1] :
( ~ equalish(X0,multiply(X1,sF0))
| ~ equalish(X1,multiply(a,b))
| equalish(multiply(X0,d),sF4)
| ~ defined(b) ),
inference(forward_subsumption_resolution,[],[f2301,f32]) ).
fof(f2314,plain,
! [X0,X1] :
( ~ equalish(X1,multiply(a,b))
| ~ equalish(X0,multiply(X1,sF0))
| equalish(multiply(X0,d),sF4) ),
inference(forward_subsumption_resolution,[],[f2306,f29]) ).
fof(f2345,plain,
! [X0] :
( ~ equalish(X0,multiply(multiply(b,a),sF0))
| equalish(multiply(X0,d),sF4)
| ~ defined(b)
| ~ defined(a) ),
inference(resolution,[],[f2314,f8]) ).
fof(f2380,plain,
! [X0] :
( ~ equalish(X0,multiply(multiply(b,a),sF0))
| equalish(multiply(X0,d),sF4)
| ~ defined(a) ),
inference(forward_subsumption_resolution,[],[f2345,f29]) ).
fof(f2383,plain,
! [X0] :
( ~ equalish(X0,multiply(multiply(b,a),sF0))
| equalish(multiply(X0,d),sF4) ),
inference(forward_subsumption_resolution,[],[f2380,f28]) ).
fof(f2388,plain,
( equalish(multiply(multiply(b,multiply(a,sF0)),d),sF4)
| ~ defined(b)
| ~ defined(a)
| ~ defined(sF0) ),
inference(resolution,[],[f2383,f5]) ).
fof(f2426,plain,
( equalish(multiply(multiply(b,multiply(a,sF0)),d),sF4)
| ~ defined(a)
| ~ defined(sF0) ),
inference(forward_subsumption_resolution,[],[f2388,f29]) ).
fof(f2432,plain,
( equalish(multiply(multiply(b,multiply(a,sF0)),d),sF4)
| ~ defined(sF0) ),
inference(forward_subsumption_resolution,[],[f2426,f28]) ).
fof(f2444,plain,
( equalish(multiply(multiply(b,multiply(a,sF0)),d),sF4)
| ~ spl6_1 ),
inference(forward_subsumption_resolution,[],[f2432,f61]) ).
fof(f2447,plain,
( equalish(multiply(multiply(b,sF1),d),sF4)
| ~ spl6_1 ),
inference(forward_demodulation,[],[f2444,f39]) ).
fof(f2536,plain,
( ! [X0] :
( ~ equalish(X0,multiply(multiply(b,sF1),d))
| equalish(X0,sF4) )
| ~ spl6_1 ),
inference(resolution,[],[f2447,f23]) ).
fof(f2546,plain,
( equalish(multiply(multiply(sF1,d),b),sF4)
| ~ defined(d)
| ~ defined(b)
| ~ defined(sF1)
| ~ spl6_1 ),
inference(resolution,[],[f2536,f1041]) ).
fof(f2568,plain,
( equalish(multiply(multiply(sF1,d),b),sF4)
| ~ defined(b)
| ~ defined(sF1)
| ~ spl6_1 ),
inference(forward_subsumption_resolution,[],[f2546,f31]) ).
fof(f2586,plain,
( equalish(multiply(multiply(sF1,d),b),sF4)
| ~ defined(sF1)
| ~ spl6_1 ),
inference(forward_subsumption_resolution,[],[f2568,f29]) ).
fof(f2598,plain,
( equalish(multiply(multiply(sF1,d),b),sF4)
| ~ spl6_1 ),
inference(forward_subsumption_resolution,[],[f2586,f429]) ).
fof(f2613,plain,
( ! [X0] :
( ~ equalish(X0,multiply(multiply(sF1,d),b))
| equalish(X0,sF4) )
| ~ spl6_1 ),
inference(resolution,[],[f2598,f23]) ).
fof(f2617,plain,
( ! [X0] :
( equalish(multiply(X0,b),sF4)
| ~ defined(b)
| ~ equalish(X0,multiply(sF1,d)) )
| ~ spl6_1 ),
inference(resolution,[],[f2613,f25]) ).
fof(f2658,plain,
( ! [X0] :
( ~ equalish(X0,multiply(sF1,d))
| equalish(multiply(X0,b),sF4) )
| ~ spl6_1 ),
inference(forward_subsumption_resolution,[],[f2617,f29]) ).
fof(f2673,plain,
( ! [X0] :
( equalish(multiply(multiply(X0,d),b),sF4)
| ~ defined(d)
| ~ equalish(X0,sF1) )
| ~ spl6_1 ),
inference(resolution,[],[f2658,f25]) ).
fof(f2721,plain,
( ! [X0] :
( equalish(multiply(multiply(X0,d),b),sF4)
| ~ equalish(X0,sF1) )
| ~ spl6_1 ),
inference(forward_subsumption_resolution,[],[f2673,f31]) ).
fof(f2732,plain,
( ! [X0,X1] :
( ~ equalish(X1,multiply(multiply(X0,d),b))
| ~ equalish(X0,sF1)
| equalish(X1,sF4) )
| ~ spl6_1 ),
inference(resolution,[],[f2721,f23]) ).
fof(f2737,plain,
( ! [X0,X1] :
( ~ equalish(X0,sF1)
| equalish(multiply(X1,b),sF4)
| ~ defined(b)
| ~ equalish(X1,multiply(X0,d)) )
| ~ spl6_1 ),
inference(resolution,[],[f2732,f25]) ).
fof(f2751,plain,
( ! [X0,X1] :
( ~ equalish(X1,multiply(X0,d))
| equalish(multiply(X1,b),sF4)
| ~ equalish(X0,sF1) )
| ~ spl6_1 ),
inference(forward_subsumption_resolution,[],[f2737,f29]) ).
fof(f3448,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,[],[f1534,f23]) ).
fof(f3449,plain,
! [X0,X1] :
( equalish(X0,multiply(multiply(X0,multiplicative_inverse(X1)),X1))
| ~ defined(X1)
| equalish(X1,additive_identity)
| ~ defined(X0) ),
inference(resolution,[],[f1534,f22]) ).
fof(f3546,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,[],[f3448,f1041]) ).
fof(f3555,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,[],[f3546]) ).
fof(f3565,plain,
! [X0,X1] :
( equalish(multiply(multiply(multiplicative_inverse(X0),X0),X1),X1)
| equalish(X0,additive_identity)
| ~ defined(X1)
| ~ defined(X0) ),
inference(forward_subsumption_resolution,[],[f3555,f15]) ).
fof(f3660,plain,
! [X0] :
( equalish(multiply(multiply(sF2,d),X0),X0)
| equalish(d,additive_identity)
| ~ defined(X0)
| ~ defined(d) ),
inference(superposition,[],[f3565,f41]) ).
fof(f3663,plain,
! [X0] :
( equalish(multiply(multiply(sF2,d),X0),X0)
| ~ defined(X0)
| ~ defined(d) ),
inference(forward_subsumption_resolution,[],[f3660,f33]) ).
fof(f3672,plain,
! [X0] :
( equalish(multiply(multiply(sF2,d),X0),X0)
| ~ defined(X0) ),
inference(forward_subsumption_resolution,[],[f3663,f31]) ).
fof(f7414,plain,
! [X0] :
( equalish(X0,multiply(multiply(X0,sF2),d))
| ~ defined(d)
| equalish(d,additive_identity)
| ~ defined(X0) ),
inference(superposition,[],[f3449,f41]) ).
fof(f7434,plain,
! [X0] :
( equalish(X0,multiply(multiply(X0,sF2),d))
| equalish(d,additive_identity)
| ~ defined(X0) ),
inference(forward_subsumption_resolution,[],[f7414,f31]) ).
fof(f7459,plain,
! [X0] :
( equalish(X0,multiply(multiply(X0,sF2),d))
| ~ defined(X0) ),
inference(forward_subsumption_resolution,[],[f7434,f33]) ).
fof(f8061,plain,
( equalish(c,multiply(sF3,d))
| ~ defined(c) ),
inference(superposition,[],[f7459,f43]) ).
fof(f8066,plain,
equalish(c,multiply(sF3,d)),
inference(forward_subsumption_resolution,[],[f8061,f30]) ).
fof(f8179,plain,
( equalish(multiply(c,b),sF4)
| ~ equalish(sF3,sF1)
| ~ spl6_1 ),
inference(resolution,[],[f8066,f2751]) ).
fof(f8219,plain,
( equalish(multiply(c,b),sF4)
| ~ spl6_1 ),
inference(forward_subsumption_resolution,[],[f8179,f136]) ).
fof(f8250,plain,
( ! [X0] :
( ~ equalish(X0,multiply(c,b))
| equalish(X0,sF4) )
| ~ spl6_1 ),
inference(resolution,[],[f8219,f23]) ).
fof(f8253,plain,
( ! [X0] :
( equalish(multiply(X0,b),sF4)
| ~ defined(b)
| ~ equalish(X0,c) )
| ~ spl6_1 ),
inference(resolution,[],[f8250,f25]) ).
fof(f8270,plain,
( ! [X0] :
( equalish(multiply(X0,b),sF4)
| ~ equalish(X0,c) )
| ~ spl6_1 ),
inference(forward_subsumption_resolution,[],[f8253,f29]) ).
fof(f8280,plain,
( ! [X0] :
( equalish(sF4,multiply(X0,b))
| ~ equalish(X0,c) )
| ~ spl6_1 ),
inference(resolution,[],[f8270,f22]) ).
fof(f10314,plain,
( ! [X0] :
( ~ equalish(X0,c)
| ~ equalish(X0,c)
| equalish(sF4,sF5) )
| ~ spl6_1 ),
inference(resolution,[],[f8280,f176]) ).
fof(f10390,plain,
( ! [X0] :
( ~ equalish(X0,c)
| equalish(sF4,sF5) )
| ~ spl6_1 ),
inference(duplicate_literal_removal,[],[f10314]) ).
fof(f10401,plain,
( ! [X0] : ~ equalish(X0,c)
| ~ spl6_1 ),
inference(forward_subsumption_resolution,[],[f10390,f49]) ).
fof(f10408,plain,
( ~ defined(c)
| ~ spl6_1 ),
inference(resolution,[],[f10401,f3672]) ).
fof(f10437,plain,
( $false
| ~ spl6_1 ),
inference(forward_subsumption_resolution,[],[f10408,f30]) ).
fof(f10438,plain,
~ spl6_1,
inference(avatar_contradiction_clause,[],[f10437]) ).
cnf(s7,plain,
spl6_1,
inference(sat_conversion,[],[f105]) ).
cnf(s590,plain,
~ spl6_1,
inference(sat_conversion,[],[f10438]) ).
cnf(s591,plain,
$false,
inference(rat,[],[s7,s590]) ).
fof(f10442,plain,
$false,
inference(avatar_sat_refutation,[],[s591]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : FLD049-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Tue Sep 29 00:38:49 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.13 Running first-order theorem proving
% 0.09/0.13 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
% 9.07/1.90 % (3951962)Input is clausal, will run a generic CNF schedule.
% 9.07/1.90 % (3952030)dis-21_1_sil=8000:lcm=predicate:random_seed=853230179: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)
% 9.07/1.90 % (3952028)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=768490133:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.07/1.90 % (3952025)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1870831283:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.07/1.90 % (3952024)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=2390300554:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.07/1.90 % (3952029)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1459966227:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.07/1.90 % (3952027)lrs+10_1_sil=8000:sp=occurrence:random_seed=3375167062:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.07/1.90 % (3952026)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1480849016:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.07/1.90 % (3952030)Instruction limit reached!
% 9.07/1.90 % (3952030)------------------------------
% 9.07/1.90 % (3952030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.07/1.90 % (3952030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.07/1.90 % (3952030)CaDiCaL version: 2.1.3
% 9.07/1.90 % (3952030)Termination reason: Instruction limit
% 9.07/1.90 % (3952030)Termination phase: Saturation
% 9.07/1.90 % (3952030)Time elapsed: 0.069 s
% 9.07/1.90 % (3952030)Peak memory usage: 89 MB
% 9.07/1.90 % (3952030)Instructions burned: 117 (million)
% 9.07/1.90 % (3952027)Instruction limit reached!
% 9.07/1.90 % (3952027)------------------------------
% 9.07/1.90 % (3952027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.07/1.90 % (3952027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.07/1.90 % (3952027)CaDiCaL version: 2.1.3
% 9.07/1.90 % (3952027)Termination reason: Instruction limit
% 9.07/1.90 % (3952027)Termination phase: Saturation
% 9.07/1.90 % (3952027)Time elapsed: 0.058 s
% 9.07/1.90 % (3952027)Peak memory usage: 89 MB
% 9.07/1.90 % (3952027)Instructions burned: 108 (million)
% 9.07/1.90 % (3952028)Instruction limit reached!
% 9.07/1.90 % (3952028)------------------------------
% 9.07/1.90 % (3952028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.07/1.90 % (3952028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.07/1.90 % (3952028)CaDiCaL version: 2.1.3
% 9.07/1.90 % (3952028)Termination reason: Instruction limit
% 9.07/1.90 % (3952028)Termination phase: Saturation
% 9.07/1.90 % (3952028)Time elapsed: 0.061 s
% 9.07/1.90 % (3952028)Peak memory usage: 88 MB
% 9.07/1.90 % (3952028)Instructions burned: 119 (million)
% 9.07/1.90 % (3952029)Instruction limit reached!
% 9.07/1.90 % (3952029)------------------------------
% 9.07/1.90 % (3952029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.07/1.90 % (3952029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.07/1.90 % (3952029)CaDiCaL version: 2.1.3
% 9.07/1.90 % (3952029)Termination reason: Instruction limit
% 9.07/1.90 % (3952029)Termination phase: Saturation
% 9.07/1.90 % (3952029)Time elapsed: 0.085 s
% 9.07/1.90 % (3952029)Peak memory usage: 89 MB
% 9.07/1.90 % (3952029)Instructions burned: 181 (million)
% 9.07/1.90 % (3952045)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1703998549:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi)
% 9.07/1.90 % (3952044)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=1180179813:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 9.07/1.90 % (3952046)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=443214748:st=4:i=219:sd=3:ss=axioms_2998 on theBenchmark for (2998ds/219Mi)
% 9.07/1.90 % (3952047)lrs+10_64_to=lpo:sil=8000:random_seed=3244469235:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 9.07/1.90 % (3952045)Instruction limit reached!
% 6.28/2.13 % (3952045)------------------------------
% 6.28/2.13 % (3952045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/2.13 % (3952045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/2.13 % (3952045)CaDiCaL version: 2.1.3
% 6.28/2.13 % (3952045)Termination reason: Instruction limit
% 6.28/2.13 % (3952045)Termination phase: Saturation
% 6.28/2.13 % (3952045)Time elapsed: 0.073 s
% 6.28/2.13 % (3952045)Peak memory usage: 94 MB
% 6.28/2.13 % (3952045)Instructions burned: 191 (million)
% 6.28/2.13 % (3952044)Instruction limit reached!
% 6.28/2.13 % (3952044)------------------------------
% 6.28/2.13 % (3952044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/2.13 % (3952044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/2.13 % (3952044)CaDiCaL version: 2.1.3
% 6.28/2.13 % (3952044)Termination reason: Instruction limit
% 6.28/2.13 % (3952044)Termination phase: Saturation
% 6.28/2.13 % (3952044)Time elapsed: 0.078 s
% 6.28/2.13 % (3952044)Peak memory usage: 89 MB
% 6.28/2.13 % (3952044)Instructions burned: 144 (million)
% 6.28/2.13 % (3952047)Instruction limit reached!
% 6.28/2.13 % (3952047)------------------------------
% 6.28/2.13 % (3952047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/2.13 % (3952047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/2.13 % (3952047)CaDiCaL version: 2.1.3
% 6.28/2.13 % (3952047)Termination reason: Instruction limit
% 6.28/2.13 % (3952047)Termination phase: Saturation
% 6.28/2.13 % (3952047)Time elapsed: 0.067 s
% 6.28/2.13 % (3952047)Peak memory usage: 89 MB
% 6.28/2.13 % (3952047)Instructions burned: 126 (million)
% 6.28/2.13 % (3952046)Instruction limit reached!
% 6.28/2.13 % (3952046)------------------------------
% 6.28/2.13 % (3952046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/2.13 % (3952046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/2.13 % (3952046)CaDiCaL version: 2.1.3
% 6.28/2.13 % (3952046)Termination reason: Instruction limit
% 6.28/2.13 % (3952046)Termination phase: Saturation
% 6.28/2.13 % (3952046)Time elapsed: 0.128 s
% 6.28/2.13 % (3952046)Peak memory usage: 90 MB
% 6.28/2.13 % (3952046)Instructions burned: 220 (million)
% 6.28/2.13 % (3952054)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4004733458:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 6.28/2.13 % (3952056)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3685849653:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 6.28/2.13 % (3952055)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1354801476:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 6.28/2.13 % (3952054)Instruction limit reached!
% 6.28/2.13 % (3952054)------------------------------
% 6.28/2.13 % (3952054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/2.13 % (3952054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/2.13 % (3952054)CaDiCaL version: 2.1.3
% 6.28/2.13 % (3952054)Termination reason: Instruction limit
% 6.28/2.13 % (3952054)Termination phase: Saturation
% 6.28/2.13 % (3952054)Time elapsed: 0.097 s
% 6.28/2.13 % (3952054)Peak memory usage: 89 MB
% 6.28/2.13 % (3952054)Instructions burned: 196 (million)
% 6.28/2.13 % (3952058)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=102360203:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 6.28/2.13 % (3952055)Instruction limit reached!
% 6.28/2.13 % (3952055)------------------------------
% 6.28/2.13 % (3952055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/2.13 % (3952055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/2.13 % (3952055)CaDiCaL version: 2.1.3
% 6.28/2.13 % (3952055)Termination reason: Instruction limit
% 6.28/2.13 % (3952055)Termination phase: Saturation
% 6.28/2.13 % (3952055)Time elapsed: 0.098 s
% 6.28/2.13 % (3952055)Peak memory usage: 91 MB
% 6.28/2.13 % (3952055)Instructions burned: 157 (million)
% 6.28/2.13 % (3952058)Instruction limit reached!
% 6.28/2.13 % (3952058)------------------------------
% 6.28/2.13 % (3952058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/2.13 % (3952058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/2.13 % (3952058)CaDiCaL version: 2.1.3
% 6.28/2.13 % (3952058)Termination reason: Instruction limit
% 6.28/2.13 % (3952058)Termination phase: Saturation
% 6.28/2.13 % (3952058)Time elapsed: 0.050 s
% 6.28/2.13 % (3952058)Peak memory usage: 89 MB
% 6.28/2.13 % (3952058)Instructions burned: 108 (million)
% 6.28/2.13 % (3952066)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3692773908:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 6.28/2.13 % (3952066)Instruction limit reached!
% 6.28/2.13 % (3952066)------------------------------
% 6.28/2.13 % (3952066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/2.13 % (3952066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/2.13 % (3952066)CaDiCaL version: 2.1.3
% 6.28/2.13 % (3952066)Termination reason: Instruction limit
% 6.28/2.13 % (3952066)Termination phase: Saturation
% 6.28/2.13 % (3952066)Time elapsed: 0.056 s
% 6.28/2.13 % (3952066)Peak memory usage: 89 MB
% 6.28/2.13 % (3952066)Instructions burned: 109 (million)
% 6.28/2.13 % (3952070)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1703916526:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 6.28/2.13 % (3952069)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3483197571:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 6.28/2.13 % (3952074)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=489540046:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi)
% 6.28/2.13 % (3952069)Instruction limit reached!
% 6.28/2.13 % (3952069)------------------------------
% 6.28/2.13 % (3952069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/2.13 % (3952069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/2.13 % (3952069)CaDiCaL version: 2.1.3
% 6.28/2.13 % (3952069)Termination reason: Instruction limit
% 6.28/2.13 % (3952069)Termination phase: Saturation
% 6.28/2.13 % (3952069)Time elapsed: 0.144 s
% 6.28/2.13 % (3952069)Peak memory usage: 89 MB
% 6.28/2.13 % (3952069)Instructions burned: 242 (million)
% 6.28/2.13 % (3952074)Instruction limit reached!
% 6.28/2.13 % (3952074)------------------------------
% 6.28/2.13 % (3952074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/2.13 % (3952074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/2.13 % (3952074)CaDiCaL version: 2.1.3
% 6.28/2.13 % (3952074)Termination reason: Instruction limit
% 6.28/2.13 % (3952074)Termination phase: Saturation
% 6.28/2.13 % (3952074)Time elapsed: 0.075 s
% 6.28/2.13 % (3952074)Peak memory usage: 90 MB
% 6.28/2.13 % (3952074)Instructions burned: 136 (million)
% 6.28/2.13 % (3952078)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1826521445:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 6.28/2.13 % (3952079)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=585694789:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 6.28/2.13 % (3952079)Instruction limit reached!
% 6.28/2.13 % (3952079)------------------------------
% 6.28/2.13 % (3952079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/2.13 % (3952079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/2.13 % (3952079)CaDiCaL version: 2.1.3
% 6.28/2.13 % (3952079)Termination reason: Instruction limit
% 6.28/2.13 % (3952079)Termination phase: Saturation
% 6.28/2.13 % (3952079)Time elapsed: 0.108 s
% 6.28/2.13 % (3952079)Peak memory usage: 91 MB
% 6.28/2.13 % (3952079)Instructions burned: 192 (million)
% 6.28/2.13 % (3952078)Instruction limit reached!
% 6.28/2.13 % (3952078)------------------------------
% 6.28/2.13 % (3952078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/2.13 % (3952078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/2.13 % (3952078)CaDiCaL version: 2.1.3
% 6.28/2.13 % (3952078)Termination reason: Instruction limit
% 6.28/2.13 % (3952078)Termination phase: Saturation
% 6.28/2.13 % (3952078)Time elapsed: 0.227 s
% 6.28/2.13 % (3952078)Peak memory usage: 106 MB
% 6.28/2.13 % (3952078)Instructions burned: 499 (million)
% 6.28/2.13 % (3952084)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=946469692:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi)
% 6.28/2.13 % (3952024)First to succeed.
% 6.28/2.13 % (3952024)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3951962"
% 6.28/2.13 % (3952085)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=509645811:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 6.28/2.13 % (3952085)Instruction limit reached!
% 6.28/2.13 % (3952085)------------------------------
% 6.28/2.13 % (3952085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/2.13 % (3952085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/2.13 % (3952085)CaDiCaL version: 2.1.3
% 6.28/2.13 % (3952085)Termination reason: Instruction limit
% 6.28/2.13 % (3952085)Termination phase: Saturation
% 6.28/2.13 % (3952085)Time elapsed: 0.061 s
% 6.28/2.13 % (3952085)Peak memory usage: 88 MB
% 6.28/2.13 % (3952085)Instructions burned: 157 (million)
% 6.28/2.13 % (3952084)Instruction limit reached!
% 6.28/2.13 % (3952084)------------------------------
% 6.28/2.13 % (3952084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/2.13 % (3952084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/2.13 % (3952084)CaDiCaL version: 2.1.3
% 6.28/2.13 % (3952084)Termination reason: Instruction limit
% 6.28/2.13 % (3952084)Termination phase: Saturation
% 6.28/2.13 % (3952084)Time elapsed: 0.151 s
% 6.28/2.13 % (3952084)Peak memory usage: 89 MB
% 6.28/2.13 % (3952084)Instructions burned: 264 (million)
% 6.28/2.13 % (3952024)Refutation found. Thanks to Tanya!
% 6.28/2.13 % SZS status Unsatisfiable for theBenchmark
% 6.28/2.13 % SZS output start Proof for theBenchmark
% See solution above
% 0.09/2.31 % (3952024)------------------------------
% 0.09/2.31 % (3952024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.09/2.31 % (3952024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/2.31 % (3952024)CaDiCaL version: 2.1.3
% 0.09/2.31 % (3952024)Termination reason: Refutation
% 0.09/2.31 % (3952024)Time elapsed: 1.345 s
% 0.09/2.31 % (3952024)Peak memory usage: 144 MB
% 0.09/2.31 % (3952024)Instructions burned: 2537 (million)
% 0.09/2.31 % (3952024)------------------------------
% 0.09/2.31 % (3952024)------------------------------
% 0.09/2.31 % (3951962)Success in time 1.713 s
% 0.09/2.31 % Vampire exiting
%------------------------------------------------------------------------------