%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : FLD053-3 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n013.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:14 AM UTC 2026
% Result : Unsatisfiable 20.88s 4.05s
% Output : Refutation 24.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 54
% Syntax : Number of formulae : 317 ( 79 unt; 30 def)
% Number of atoms : 773 ( 24 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 868 ( 412 ~; 438 |; 0 &)
% ( 18 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 19 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 18 con; 0-2 aty)
% Number of variables : 155 ( 0 sgn 155 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X4,X5,X2)
| ~ sum(X0,X3,X4)
| ~ sum(X3,X5,X1)
| sum(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_addition_1) ).
fof(f2,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X4,X1,X5)
| ~ sum(X3,X4,X0)
| sum(X0,X1,X2)
| ~ sum(X3,X5,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_addition_2) ).
fof(f3,axiom,
! [X0] :
( sum(additive_identity,X0,X0)
| ~ defined(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_of_identity_addition) ).
fof(f4,axiom,
! [X0] :
( sum(additive_inverse(X0),X0,additive_identity)
| ~ defined(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_of_inverse_addition) ).
fof(f5,axiom,
! [X2,X0,X1] :
( ~ sum(X1,X0,X2)
| sum(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_addition) ).
fof(f6,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ product(X4,X5,X2)
| ~ product(X0,X3,X4)
| ~ product(X3,X5,X1)
| product(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_multiplication_1) ).
fof(f8,axiom,
! [X0] :
( product(multiplicative_identity,X0,X0)
| ~ defined(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_of_identity_multiplication) ).
fof(f9,axiom,
! [X0] :
( product(multiplicative_inverse(X0),X0,multiplicative_identity)
| sum(additive_identity,X0,additive_identity)
| ~ defined(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_of_inverse_multiplication) ).
fof(f10,axiom,
! [X2,X0,X1] :
( ~ product(X1,X0,X2)
| product(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_multiplication) ).
fof(f11,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ product(X5,X6,X2)
| ~ sum(X3,X4,X5)
| sum(X0,X1,X2)
| ~ product(X3,X6,X0)
| ~ product(X4,X6,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',distributivity_1) ).
fof(f13,axiom,
! [X0,X1] :
( defined(add(X0,X1))
| ~ defined(X0)
| ~ defined(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_definedness_of_addition) ).
fof(f15,axiom,
! [X0] :
( defined(additive_inverse(X0))
| ~ defined(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_definedness_of_additive_inverse) ).
fof(f16,axiom,
! [X0,X1] :
( defined(multiply(X0,X1))
| ~ defined(X0)
| ~ defined(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_definedness_of_multiplication) ).
fof(f17,axiom,
defined(multiplicative_identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_definedness_of_multiplicative_identity) ).
fof(f18,axiom,
! [X0] :
( sum(additive_identity,X0,additive_identity)
| ~ defined(X0)
| defined(multiplicative_inverse(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_definedness_of_multiplicative_inverse) ).
fof(f19,axiom,
! [X0,X1] :
( sum(X0,X1,add(X0,X1))
| ~ defined(X0)
| ~ defined(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',totality_of_addition) ).
fof(f20,axiom,
! [X0,X1] :
( product(X0,X1,multiply(X0,X1))
| ~ defined(X0)
| ~ defined(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',totality_of_multiplication) ).
fof(f27,axiom,
defined(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_is_defined) ).
fof(f28,axiom,
defined(b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b_is_defined) ).
fof(f29,axiom,
defined(c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_is_defined) ).
fof(f30,axiom,
defined(d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_is_defined) ).
fof(f31,negated_conjecture,
~ sum(additive_identity,b,additive_identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_sum_5) ).
fof(f32,negated_conjecture,
~ sum(additive_identity,d,additive_identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_sum_6) ).
fof(f33,negated_conjecture,
~ sum(multiply(a,multiplicative_inverse(b)),additive_inverse(multiply(c,multiplicative_inverse(d))),multiply(add(multiply(a,d),additive_inverse(multiply(b,c))),multiplicative_inverse(multiply(b,d)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_sum_7) ).
fof(f34,definition,
sF0 = multiplicative_inverse(b),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f35,plain,
multiplicative_inverse(b) = sF0,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF1 = multiply(a,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f37,plain,
multiply(a,sF0) = sF1,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF2 = multiplicative_inverse(d),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f39,plain,
multiplicative_inverse(d) = sF2,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF3 = multiply(c,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f41,plain,
multiply(c,sF2) = sF3,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF4 = additive_inverse(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f43,plain,
additive_inverse(sF3) = sF4,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF5 = multiply(a,d),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f45,plain,
multiply(a,d) = sF5,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF6 = multiply(b,c),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f47,plain,
multiply(b,c) = sF6,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF7 = additive_inverse(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f49,plain,
additive_inverse(sF6) = sF7,
inference(reorient_equations,[],[f48]) ).
fof(f50,definition,
sF8 = add(sF5,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f51,plain,
add(sF5,sF7) = sF8,
inference(reorient_equations,[],[f50]) ).
fof(f52,definition,
sF9 = multiply(b,d),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f53,plain,
multiply(b,d) = sF9,
inference(reorient_equations,[],[f52]) ).
fof(f54,definition,
sF10 = multiplicative_inverse(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f55,plain,
multiplicative_inverse(sF9) = sF10,
inference(reorient_equations,[],[f54]) ).
fof(f56,definition,
sF11 = multiply(sF8,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f57,plain,
multiply(sF8,sF10) = sF11,
inference(reorient_equations,[],[f56]) ).
fof(f58,plain,
~ sum(sF1,sF4,sF11),
inference(definition_folding,[],[f33,f57,f55,f53,f51,f49,f47,f45,f43,f41,f39,f37,f35]) ).
fof(f61,definition,
( spl12_1
<=> defined(sF3) ),
introduced(definition,[new_symbols(definition,[spl12_1])],[avatar_definition]) ).
fof(f62,plain,
( defined(sF3)
| ~ spl12_1 ),
inference(avatar_component_clause,[],[f61]) ).
fof(f63,plain,
( ~ defined(sF3)
| spl12_1 ),
inference(avatar_component_clause,[],[f61]) ).
fof(f71,definition,
( spl12_3
<=> defined(sF6) ),
introduced(definition,[new_symbols(definition,[spl12_3])],[avatar_definition]) ).
fof(f72,plain,
( defined(sF6)
| ~ spl12_3 ),
inference(avatar_component_clause,[],[f71]) ).
fof(f73,plain,
( ~ defined(sF6)
| spl12_3 ),
inference(avatar_component_clause,[],[f71]) ).
fof(f79,plain,
( sum(sF5,sF7,sF8)
| ~ defined(sF5)
| ~ defined(sF7) ),
inference(superposition,[],[f19,f51]) ).
fof(f81,definition,
( spl12_5
<=> defined(sF7) ),
introduced(definition,[new_symbols(definition,[spl12_5])],[avatar_definition]) ).
fof(f82,plain,
( defined(sF7)
| ~ spl12_5 ),
inference(avatar_component_clause,[],[f81]) ).
fof(f83,plain,
( ~ defined(sF7)
| spl12_5 ),
inference(avatar_component_clause,[],[f81]) ).
fof(f85,definition,
( spl12_6
<=> defined(sF5) ),
introduced(definition,[new_symbols(definition,[spl12_6])],[avatar_definition]) ).
fof(f86,plain,
( defined(sF5)
| ~ spl12_6 ),
inference(avatar_component_clause,[],[f85]) ).
fof(f89,definition,
( spl12_7
<=> sum(sF5,sF7,sF8) ),
introduced(definition,[new_symbols(definition,[spl12_7])],[avatar_definition]) ).
fof(f91,plain,
( sum(sF5,sF7,sF8)
| ~ spl12_7 ),
inference(avatar_component_clause,[],[f89]) ).
fof(f92,plain,
( ~ spl12_5
| ~ spl12_6
| spl12_7 ),
inference(avatar_split_clause,[],[f79,f89,f85,f81]) ).
fof(f93,plain,
( ~ defined(b)
| defined(multiplicative_inverse(b)) ),
inference(resolution,[],[f18,f31]) ).
fof(f94,plain,
( ~ defined(d)
| defined(multiplicative_inverse(d)) ),
inference(resolution,[],[f18,f32]) ).
fof(f95,plain,
defined(multiplicative_inverse(d)),
inference(forward_subsumption_resolution,[],[f94,f30]) ).
fof(f96,plain,
defined(multiplicative_inverse(b)),
inference(forward_subsumption_resolution,[],[f93,f28]) ).
fof(f97,plain,
defined(sF2),
inference(forward_demodulation,[],[f95,f39]) ).
fof(f98,plain,
defined(sF0),
inference(forward_demodulation,[],[f96,f35]) ).
fof(f99,plain,
( product(sF2,d,multiplicative_identity)
| sum(additive_identity,d,additive_identity)
| ~ defined(d) ),
inference(superposition,[],[f9,f39]) ).
fof(f100,plain,
( product(sF0,b,multiplicative_identity)
| sum(additive_identity,b,additive_identity)
| ~ defined(b) ),
inference(superposition,[],[f9,f35]) ).
fof(f103,definition,
( spl12_8
<=> defined(sF9) ),
introduced(definition,[new_symbols(definition,[spl12_8])],[avatar_definition]) ).
fof(f104,plain,
( defined(sF9)
| ~ spl12_8 ),
inference(avatar_component_clause,[],[f103]) ).
fof(f105,plain,
( ~ defined(sF9)
| spl12_8 ),
inference(avatar_component_clause,[],[f103]) ).
fof(f107,definition,
( spl12_9
<=> sum(additive_identity,sF9,additive_identity) ),
introduced(definition,[new_symbols(definition,[spl12_9])],[avatar_definition]) ).
fof(f108,plain,
( ~ sum(additive_identity,sF9,additive_identity)
| spl12_9 ),
inference(avatar_component_clause,[],[f107]) ).
fof(f109,plain,
( sum(additive_identity,sF9,additive_identity)
| ~ spl12_9 ),
inference(avatar_component_clause,[],[f107]) ).
fof(f115,plain,
( product(sF0,b,multiplicative_identity)
| ~ defined(b) ),
inference(forward_subsumption_resolution,[],[f100,f31]) ).
fof(f116,plain,
( product(sF2,d,multiplicative_identity)
| ~ defined(d) ),
inference(forward_subsumption_resolution,[],[f99,f32]) ).
fof(f117,plain,
product(sF0,b,multiplicative_identity),
inference(forward_subsumption_resolution,[],[f115,f28]) ).
fof(f118,plain,
product(sF2,d,multiplicative_identity),
inference(forward_subsumption_resolution,[],[f116,f30]) ).
fof(f120,plain,
( defined(sF7)
| ~ defined(sF6) ),
inference(superposition,[],[f15,f49]) ).
fof(f121,plain,
! [X0] :
( sum(X0,additive_inverse(X0),additive_identity)
| ~ defined(X0) ),
inference(resolution,[],[f5,f4]) ).
fof(f126,plain,
( sum(sF6,sF7,additive_identity)
| ~ defined(sF6) ),
inference(superposition,[],[f121,f49]) ).
fof(f127,plain,
! [X0] :
( sum(X0,additive_identity,X0)
| ~ defined(X0) ),
inference(resolution,[],[f3,f5]) ).
fof(f129,plain,
! [X2,X3,X0,X1] :
( ~ sum(X0,X1,additive_inverse(X2))
| ~ sum(X1,X2,X3)
| sum(X0,X3,additive_identity)
| ~ defined(X2) ),
inference(resolution,[],[f1,f4]) ).
fof(f131,plain,
! [X2,X3,X0,X1] :
( ~ sum(X1,additive_inverse(X2),X3)
| ~ sum(X0,X1,X2)
| sum(X0,X3,additive_identity)
| ~ defined(X2) ),
inference(resolution,[],[f1,f121]) ).
fof(f134,plain,
! [X2,X3,X0,X1] :
( ~ sum(X1,X2,X3)
| ~ sum(X0,X1,additive_identity)
| sum(X0,X3,X2)
| ~ defined(X2) ),
inference(resolution,[],[f1,f3]) ).
fof(f136,plain,
! [X0,X1] :
( ~ sum(X0,X1,X1)
| sum(X0,additive_identity,additive_identity)
| ~ defined(X1)
| ~ defined(X1) ),
inference(resolution,[],[f131,f121]) ).
fof(f142,plain,
! [X0,X1] :
( ~ sum(X0,X1,X1)
| sum(X0,additive_identity,additive_identity)
| ~ defined(X1) ),
inference(duplicate_literal_removal,[],[f136]) ).
fof(f178,plain,
! [X2,X3,X0,X1] :
( ~ sum(X0,additive_identity,X3)
| sum(X2,additive_inverse(X1),X3)
| ~ sum(X0,X1,X2)
| ~ defined(X1) ),
inference(resolution,[],[f2,f121]) ).
fof(f194,plain,
( product(a,sF0,sF1)
| ~ defined(a)
| ~ defined(sF0) ),
inference(superposition,[],[f20,f37]) ).
fof(f195,plain,
( product(a,d,sF5)
| ~ defined(a)
| ~ defined(d) ),
inference(superposition,[],[f20,f45]) ).
fof(f196,plain,
( product(b,d,sF9)
| ~ defined(b)
| ~ defined(d) ),
inference(superposition,[],[f20,f53]) ).
fof(f197,plain,
( product(b,c,sF6)
| ~ defined(b)
| ~ defined(c) ),
inference(superposition,[],[f20,f47]) ).
fof(f198,plain,
( product(c,sF2,sF3)
| ~ defined(c)
| ~ defined(sF2) ),
inference(superposition,[],[f20,f41]) ).
fof(f199,plain,
( product(sF8,sF10,sF11)
| ~ defined(sF8)
| ~ defined(sF10) ),
inference(superposition,[],[f20,f57]) ).
fof(f201,definition,
( spl12_13
<=> defined(sF10) ),
introduced(definition,[new_symbols(definition,[spl12_13])],[avatar_definition]) ).
fof(f202,plain,
( defined(sF10)
| ~ spl12_13 ),
inference(avatar_component_clause,[],[f201]) ).
fof(f203,plain,
( ~ defined(sF10)
| spl12_13 ),
inference(avatar_component_clause,[],[f201]) ).
fof(f205,definition,
( spl12_14
<=> defined(sF8) ),
introduced(definition,[new_symbols(definition,[spl12_14])],[avatar_definition]) ).
fof(f206,plain,
( defined(sF8)
| ~ spl12_14 ),
inference(avatar_component_clause,[],[f205]) ).
fof(f209,definition,
( spl12_15
<=> product(sF8,sF10,sF11) ),
introduced(definition,[new_symbols(definition,[spl12_15])],[avatar_definition]) ).
fof(f211,plain,
( product(sF8,sF10,sF11)
| ~ spl12_15 ),
inference(avatar_component_clause,[],[f209]) ).
fof(f212,plain,
( ~ spl12_13
| ~ spl12_14
| spl12_15 ),
inference(avatar_split_clause,[],[f199,f209,f205,f201]) ).
fof(f213,plain,
( product(c,sF2,sF3)
| ~ defined(sF2) ),
inference(forward_subsumption_resolution,[],[f198,f29]) ).
fof(f214,plain,
( product(b,c,sF6)
| ~ defined(c) ),
inference(forward_subsumption_resolution,[],[f197,f28]) ).
fof(f215,plain,
( product(b,d,sF9)
| ~ defined(d) ),
inference(forward_subsumption_resolution,[],[f196,f28]) ).
fof(f216,plain,
( product(a,d,sF5)
| ~ defined(d) ),
inference(forward_subsumption_resolution,[],[f195,f27]) ).
fof(f217,plain,
( product(a,sF0,sF1)
| ~ defined(sF0) ),
inference(forward_subsumption_resolution,[],[f194,f27]) ).
fof(f218,plain,
product(c,sF2,sF3),
inference(forward_subsumption_resolution,[],[f213,f97]) ).
fof(f219,plain,
product(b,c,sF6),
inference(forward_subsumption_resolution,[],[f214,f29]) ).
fof(f220,plain,
product(b,d,sF9),
inference(forward_subsumption_resolution,[],[f215,f30]) ).
fof(f221,plain,
product(a,d,sF5),
inference(forward_subsumption_resolution,[],[f216,f30]) ).
fof(f222,plain,
product(a,sF0,sF1),
inference(forward_subsumption_resolution,[],[f217,f98]) ).
fof(f223,plain,
( defined(sF1)
| ~ defined(a)
| ~ defined(sF0) ),
inference(superposition,[],[f16,f37]) ).
fof(f224,plain,
( defined(sF5)
| ~ defined(a)
| ~ defined(d) ),
inference(superposition,[],[f16,f45]) ).
fof(f225,plain,
( defined(sF9)
| ~ defined(b)
| ~ defined(d) ),
inference(superposition,[],[f16,f53]) ).
fof(f226,plain,
( defined(sF6)
| ~ defined(b)
| ~ defined(c) ),
inference(superposition,[],[f16,f47]) ).
fof(f227,plain,
( defined(sF3)
| ~ defined(c)
| ~ defined(sF2) ),
inference(superposition,[],[f16,f41]) ).
fof(f228,plain,
( defined(sF11)
| ~ defined(sF8)
| ~ defined(sF10) ),
inference(superposition,[],[f16,f57]) ).
fof(f229,plain,
( ~ defined(c)
| ~ defined(sF2)
| spl12_1 ),
inference(forward_subsumption_resolution,[],[f227,f63]) ).
fof(f230,plain,
( ~ defined(b)
| ~ defined(c)
| spl12_3 ),
inference(forward_subsumption_resolution,[],[f226,f73]) ).
fof(f231,plain,
( ~ defined(b)
| ~ defined(d)
| spl12_8 ),
inference(forward_subsumption_resolution,[],[f225,f105]) ).
fof(f232,plain,
( defined(sF5)
| ~ defined(d) ),
inference(forward_subsumption_resolution,[],[f224,f27]) ).
fof(f233,plain,
( defined(sF1)
| ~ defined(sF0) ),
inference(forward_subsumption_resolution,[],[f223,f27]) ).
fof(f234,plain,
( ~ defined(sF2)
| spl12_1 ),
inference(forward_subsumption_resolution,[],[f229,f29]) ).
fof(f235,plain,
( ~ defined(c)
| spl12_3 ),
inference(forward_subsumption_resolution,[],[f230,f28]) ).
fof(f236,plain,
( ~ defined(d)
| spl12_8 ),
inference(forward_subsumption_resolution,[],[f231,f28]) ).
fof(f237,plain,
defined(sF5),
inference(forward_subsumption_resolution,[],[f232,f30]) ).
fof(f238,plain,
defined(sF1),
inference(forward_subsumption_resolution,[],[f233,f98]) ).
fof(f239,plain,
( $false
| spl12_1 ),
inference(forward_subsumption_resolution,[],[f234,f97]) ).
fof(f240,plain,
spl12_1,
inference(avatar_contradiction_clause,[],[f239]) ).
fof(f241,plain,
( $false
| spl12_3 ),
inference(forward_subsumption_resolution,[],[f235,f29]) ).
fof(f242,plain,
spl12_3,
inference(avatar_contradiction_clause,[],[f241]) ).
fof(f243,plain,
( $false
| spl12_8 ),
inference(forward_subsumption_resolution,[],[f236,f30]) ).
fof(f244,plain,
spl12_8,
inference(avatar_contradiction_clause,[],[f243]) ).
fof(f245,plain,
spl12_6,
inference(avatar_split_clause,[],[f237,f85]) ).
fof(f246,plain,
( ~ defined(sF6)
| spl12_5 ),
inference(forward_subsumption_resolution,[],[f120,f83]) ).
fof(f247,plain,
( sum(sF6,sF7,additive_identity)
| ~ spl12_3 ),
inference(forward_subsumption_resolution,[],[f126,f72]) ).
fof(f252,plain,
( $false
| ~ spl12_3
| spl12_5 ),
inference(forward_subsumption_resolution,[],[f246,f72]) ).
fof(f253,plain,
( ~ spl12_3
| spl12_5 ),
inference(avatar_contradiction_clause,[],[f252]) ).
fof(f273,plain,
( sum(sF7,sF5,sF8)
| ~ spl12_7 ),
inference(resolution,[],[f91,f5]) ).
fof(f281,plain,
product(b,sF0,multiplicative_identity),
inference(resolution,[],[f10,f117]) ).
fof(f282,plain,
product(d,sF2,multiplicative_identity),
inference(resolution,[],[f10,f118]) ).
fof(f284,plain,
product(sF0,a,sF1),
inference(resolution,[],[f10,f222]) ).
fof(f285,plain,
product(sF2,c,sF3),
inference(resolution,[],[f10,f218]) ).
fof(f286,plain,
product(d,a,sF5),
inference(resolution,[],[f10,f221]) ).
fof(f288,plain,
product(d,b,sF9),
inference(resolution,[],[f10,f220]) ).
fof(f294,plain,
( defined(sF8)
| ~ defined(sF5)
| ~ defined(sF7) ),
inference(superposition,[],[f13,f51]) ).
fof(f295,plain,
( defined(sF8)
| ~ defined(sF7)
| ~ spl12_6 ),
inference(forward_subsumption_resolution,[],[f294,f86]) ).
fof(f296,plain,
( defined(sF8)
| ~ spl12_5
| ~ spl12_6 ),
inference(forward_subsumption_resolution,[],[f295,f82]) ).
fof(f297,plain,
( spl12_14
| ~ spl12_5
| ~ spl12_6 ),
inference(avatar_split_clause,[],[f296,f85,f81,f205]) ).
fof(f324,plain,
! [X2,X3,X0,X1] :
( ~ product(X1,sF0,X3)
| sum(X2,X3,multiplicative_identity)
| ~ product(X0,sF0,X2)
| ~ sum(X0,X1,b) ),
inference(resolution,[],[f11,f281]) ).
fof(f325,plain,
! [X2,X3,X0,X1] :
( ~ product(X1,sF2,X3)
| sum(X2,X3,multiplicative_identity)
| ~ product(X0,sF2,X2)
| ~ sum(X0,X1,d) ),
inference(resolution,[],[f11,f282]) ).
fof(f331,plain,
! [X2,X3,X0,X1] :
( ~ product(X1,a,X3)
| sum(X2,X3,sF1)
| ~ product(X0,a,X2)
| ~ sum(X0,X1,sF0) ),
inference(resolution,[],[f11,f284]) ).
fof(f343,plain,
! [X0,X1] :
( ~ product(X1,a,X0)
| sum(X0,sF1,sF1)
| ~ sum(X1,sF0,sF0) ),
inference(resolution,[],[f331,f284]) ).
fof(f349,definition,
( spl12_16
<=> sum(additive_identity,a,additive_identity) ),
introduced(definition,[new_symbols(definition,[spl12_16])],[avatar_definition]) ).
fof(f350,plain,
( ~ sum(additive_identity,a,additive_identity)
| spl12_16 ),
inference(avatar_component_clause,[],[f349]) ).
fof(f351,plain,
( sum(additive_identity,a,additive_identity)
| ~ spl12_16 ),
inference(avatar_component_clause,[],[f349]) ).
fof(f393,plain,
! [X0,X1] :
( ~ sum(X0,additive_identity,additive_identity)
| sum(X0,X1,X1)
| ~ defined(X1)
| ~ defined(X1) ),
inference(resolution,[],[f134,f3]) ).
fof(f397,plain,
( ! [X0] :
( ~ sum(X0,sF7,additive_identity)
| sum(X0,sF8,sF5)
| ~ defined(sF5) )
| ~ spl12_7 ),
inference(resolution,[],[f134,f273]) ).
fof(f400,plain,
! [X0,X1] :
( ~ sum(X0,additive_identity,additive_identity)
| sum(X0,X1,X1)
| ~ defined(X1) ),
inference(duplicate_literal_removal,[],[f393]) ).
fof(f405,plain,
( ! [X0] :
( ~ sum(X0,sF7,additive_identity)
| sum(X0,sF8,sF5) )
| ~ spl12_6
| ~ spl12_7 ),
inference(forward_subsumption_resolution,[],[f397,f86]) ).
fof(f494,plain,
( ! [X2,X0,X1] :
( ~ sum(X1,sF9,X2)
| ~ sum(X0,X1,additive_identity)
| sum(X0,X2,additive_identity) )
| ~ spl12_9 ),
inference(resolution,[],[f109,f1]) ).
fof(f495,plain,
( sum(sF9,additive_identity,additive_identity)
| ~ spl12_9 ),
inference(resolution,[],[f109,f5]) ).
fof(f536,plain,
! [X0,X1] :
( ~ sum(additive_inverse(X0),X0,X1)
| sum(additive_identity,X1,additive_identity)
| ~ defined(X0)
| ~ defined(additive_inverse(X0)) ),
inference(resolution,[],[f129,f3]) ).
fof(f539,plain,
! [X0,X1] :
( ~ sum(additive_inverse(X0),X0,X1)
| sum(additive_identity,X1,additive_identity)
| ~ defined(X0) ),
inference(forward_subsumption_resolution,[],[f536,f15]) ).
fof(f611,plain,
! [X2,X3,X0,X1,X4] :
( ~ product(X2,X0,X4)
| ~ sum(X1,X2,multiplicative_identity)
| sum(X3,X4,X0)
| ~ product(X1,X0,X3)
| ~ defined(X0) ),
inference(resolution,[],[f8,f11]) ).
fof(f613,plain,
( ~ defined(a)
| sum(a,sF1,sF1)
| ~ sum(multiplicative_identity,sF0,sF0) ),
inference(resolution,[],[f8,f343]) ).
fof(f622,plain,
( sum(a,sF1,sF1)
| ~ sum(multiplicative_identity,sF0,sF0) ),
inference(forward_subsumption_resolution,[],[f613,f27]) ).
fof(f633,definition,
( spl12_33
<=> sum(multiplicative_identity,sF0,sF0) ),
introduced(definition,[new_symbols(definition,[spl12_33])],[avatar_definition]) ).
fof(f635,plain,
( ~ sum(multiplicative_identity,sF0,sF0)
| spl12_33 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f637,definition,
( spl12_34
<=> sum(a,sF1,sF1) ),
introduced(definition,[new_symbols(definition,[spl12_34])],[avatar_definition]) ).
fof(f639,plain,
( sum(a,sF1,sF1)
| ~ spl12_34 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f640,plain,
( ~ spl12_33
| spl12_34 ),
inference(avatar_split_clause,[],[f622,f637,f633]) ).
fof(f641,plain,
! [X2,X0,X1] :
( ~ sum(X0,multiplicative_identity,multiplicative_identity)
| sum(X1,X2,X2)
| ~ product(X0,X2,X1)
| ~ defined(X2)
| ~ defined(X2) ),
inference(resolution,[],[f611,f8]) ).
fof(f663,plain,
! [X2,X0,X1] :
( ~ product(X0,X2,X1)
| sum(X1,X2,X2)
| ~ sum(X0,multiplicative_identity,multiplicative_identity)
| ~ defined(X2) ),
inference(duplicate_literal_removal,[],[f641]) ).
fof(f682,plain,
( sum(multiplicative_identity,sF0,sF0)
| ~ sum(b,multiplicative_identity,multiplicative_identity)
| ~ defined(sF0) ),
inference(resolution,[],[f663,f281]) ).
fof(f715,plain,
( ~ sum(b,multiplicative_identity,multiplicative_identity)
| ~ defined(sF0)
| spl12_33 ),
inference(forward_subsumption_resolution,[],[f682,f635]) ).
fof(f726,definition,
( spl12_37
<=> sum(d,multiplicative_identity,multiplicative_identity) ),
introduced(definition,[new_symbols(definition,[spl12_37])],[avatar_definition]) ).
fof(f727,plain,
( sum(d,multiplicative_identity,multiplicative_identity)
| ~ spl12_37 ),
inference(avatar_component_clause,[],[f726]) ).
fof(f728,plain,
( ~ sum(d,multiplicative_identity,multiplicative_identity)
| spl12_37 ),
inference(avatar_component_clause,[],[f726]) ).
fof(f730,definition,
( spl12_38
<=> sum(sF9,b,b) ),
introduced(definition,[new_symbols(definition,[spl12_38])],[avatar_definition]) ).
fof(f735,definition,
( spl12_39
<=> sum(b,multiplicative_identity,multiplicative_identity) ),
introduced(definition,[new_symbols(definition,[spl12_39])],[avatar_definition]) ).
fof(f737,plain,
( ~ sum(b,multiplicative_identity,multiplicative_identity)
| spl12_39 ),
inference(avatar_component_clause,[],[f735]) ).
fof(f739,definition,
( spl12_40
<=> sum(sF9,d,d) ),
introduced(definition,[new_symbols(definition,[spl12_40])],[avatar_definition]) ).
fof(f740,plain,
( ~ sum(sF9,d,d)
| spl12_40 ),
inference(avatar_component_clause,[],[f739]) ).
fof(f814,plain,
( ~ sum(b,multiplicative_identity,multiplicative_identity)
| spl12_33 ),
inference(forward_subsumption_resolution,[],[f715,f98]) ).
fof(f815,plain,
( ~ spl12_39
| spl12_33 ),
inference(avatar_split_clause,[],[f814,f633,f735]) ).
fof(f1380,plain,
! [X2,X3,X0,X1] :
( ~ product(X1,X2,X3)
| ~ product(X0,X1,multiplicative_identity)
| product(X0,X3,X2)
| ~ defined(X2) ),
inference(resolution,[],[f6,f8]) ).
fof(f1391,plain,
! [X2,X0,X1] :
( ~ product(X1,a,X2)
| ~ product(X0,X1,sF0)
| product(X0,X2,sF1) ),
inference(resolution,[],[f6,f284]) ).
fof(f1393,plain,
! [X2,X0,X1] :
( ~ product(X1,c,X2)
| ~ product(X0,X1,sF2)
| product(X0,X2,sF3) ),
inference(resolution,[],[f6,f285]) ).
fof(f1418,plain,
! [X0] :
( ~ product(X0,b,multiplicative_identity)
| product(X0,sF9,d)
| ~ defined(d) ),
inference(resolution,[],[f1380,f220]) ).
fof(f1419,plain,
! [X0] :
( ~ product(X0,d,multiplicative_identity)
| product(X0,sF9,b)
| ~ defined(b) ),
inference(resolution,[],[f1380,f288]) ).
fof(f1424,plain,
! [X0] :
( ~ product(X0,d,multiplicative_identity)
| product(X0,sF9,b) ),
inference(forward_subsumption_resolution,[],[f1419,f28]) ).
fof(f1425,plain,
! [X0] :
( ~ product(X0,b,multiplicative_identity)
| product(X0,sF9,d) ),
inference(forward_subsumption_resolution,[],[f1418,f30]) ).
fof(f1441,plain,
product(sF0,sF9,d),
inference(resolution,[],[f1425,f117]) ).
fof(f1446,plain,
product(sF9,sF0,d),
inference(resolution,[],[f1441,f10]) ).
fof(f1469,plain,
! [X0] :
( ~ product(X0,sF9,multiplicative_identity)
| product(X0,d,sF0)
| ~ defined(sF0) ),
inference(resolution,[],[f1446,f1380]) ).
fof(f1470,plain,
! [X0] :
( ~ product(X0,sF9,multiplicative_identity)
| product(X0,d,sF0) ),
inference(forward_subsumption_resolution,[],[f1469,f98]) ).
fof(f1792,plain,
product(sF2,sF9,b),
inference(resolution,[],[f1424,f118]) ).
fof(f1797,plain,
product(sF9,sF2,b),
inference(resolution,[],[f1792,f10]) ).
fof(f1816,plain,
! [X0] :
( ~ product(X0,sF9,multiplicative_identity)
| product(X0,b,sF2)
| ~ defined(sF2) ),
inference(resolution,[],[f1797,f1380]) ).
fof(f1817,plain,
! [X0] :
( ~ product(X0,sF9,multiplicative_identity)
| product(X0,b,sF2) ),
inference(forward_subsumption_resolution,[],[f1816,f97]) ).
fof(f2039,definition,
( spl12_153
<=> sum(a,b,b) ),
introduced(definition,[new_symbols(definition,[spl12_153])],[avatar_definition]) ).
fof(f2040,plain,
( ~ sum(a,b,b)
| spl12_153 ),
inference(avatar_component_clause,[],[f2039]) ).
fof(f2041,plain,
( sum(a,b,b)
| ~ spl12_153 ),
inference(avatar_component_clause,[],[f2039]) ).
fof(f2043,plain,
( product(multiplicative_inverse(sF9),b,sF2)
| sum(additive_identity,sF9,additive_identity)
| ~ defined(sF9) ),
inference(resolution,[],[f1817,f9]) ).
fof(f2245,plain,
( sum(a,additive_identity,additive_identity)
| ~ spl12_16 ),
inference(resolution,[],[f351,f5]) ).
fof(f2249,plain,
( ! [X0] :
( sum(a,X0,X0)
| ~ defined(X0) )
| ~ spl12_16 ),
inference(resolution,[],[f2245,f400]) ).
fof(f2454,plain,
( product(multiplicative_inverse(sF9),d,sF0)
| sum(additive_identity,sF9,additive_identity)
| ~ defined(sF9) ),
inference(resolution,[],[f1470,f9]) ).
fof(f2509,plain,
! [X2,X0,X1] :
( sum(X0,additive_inverse(X1),X2)
| ~ sum(X2,X1,X0)
| ~ defined(X1)
| ~ defined(X2) ),
inference(resolution,[],[f178,f127]) ).
fof(f2546,plain,
! [X2,X0,X1] :
( sum(additive_inverse(X1),X2,X0)
| ~ defined(X1)
| ~ defined(X0)
| ~ sum(X0,X1,X2) ),
inference(resolution,[],[f2509,f5]) ).
fof(f2552,plain,
! [X0,X1] :
( sum(X0,sF4,X1)
| ~ sum(X1,sF3,X0)
| ~ defined(sF3)
| ~ defined(X1) ),
inference(superposition,[],[f2509,f43]) ).
fof(f2560,plain,
( ! [X0,X1] :
( ~ sum(X1,sF3,X0)
| sum(X0,sF4,X1)
| ~ defined(X1) )
| ~ spl12_1 ),
inference(forward_subsumption_resolution,[],[f2552,f62]) ).
fof(f2741,plain,
( ! [X0] :
( ~ sum(X0,additive_identity,additive_identity)
| sum(X0,sF9,additive_identity)
| ~ defined(sF9) )
| ~ spl12_9 ),
inference(resolution,[],[f494,f3]) ).
fof(f2750,plain,
( ! [X0] :
( ~ sum(X0,additive_identity,additive_identity)
| sum(X0,sF9,additive_identity) )
| ~ spl12_8
| ~ spl12_9 ),
inference(forward_subsumption_resolution,[],[f2741,f104]) ).
fof(f2797,plain,
! [X0] :
( ~ product(X0,d,sF0)
| product(X0,sF5,sF1) ),
inference(resolution,[],[f1391,f286]) ).
fof(f4408,plain,
( ~ defined(b)
| ~ spl12_16
| spl12_153 ),
inference(resolution,[],[f2040,f2249]) ).
fof(f4409,plain,
( $false
| ~ spl12_16
| spl12_153 ),
inference(forward_subsumption_resolution,[],[f4408,f28]) ).
fof(f4410,plain,
( ~ spl12_16
| spl12_153 ),
inference(avatar_contradiction_clause,[],[f4409]) ).
fof(f5587,plain,
! [X0,X1] :
( ~ product(X1,sF0,X0)
| sum(X0,multiplicative_identity,multiplicative_identity)
| ~ sum(X1,b,b) ),
inference(resolution,[],[f324,f281]) ).
fof(f5883,plain,
( sum(a,additive_identity,additive_identity)
| ~ defined(b)
| ~ spl12_153 ),
inference(resolution,[],[f2041,f142]) ).
fof(f5895,plain,
( sum(a,additive_identity,additive_identity)
| ~ spl12_153 ),
inference(forward_subsumption_resolution,[],[f5883,f28]) ).
fof(f6133,plain,
! [X0,X1] :
( ~ product(X1,sF2,X0)
| sum(X0,multiplicative_identity,multiplicative_identity)
| ~ sum(X1,d,d) ),
inference(resolution,[],[f325,f282]) ).
fof(f6528,plain,
( ! [X0] :
( ~ sum(X0,a,additive_identity)
| sum(X0,b,b)
| ~ defined(b) )
| ~ spl12_153 ),
inference(resolution,[],[f2041,f134]) ).
fof(f6534,plain,
( ! [X0] :
( ~ sum(X0,a,additive_identity)
| sum(X0,b,b) )
| ~ spl12_153 ),
inference(forward_subsumption_resolution,[],[f6528,f28]) ).
fof(f6570,plain,
( sum(a,sF9,additive_identity)
| ~ spl12_8
| ~ spl12_9
| ~ spl12_153 ),
inference(resolution,[],[f5895,f2750]) ).
fof(f6782,plain,
( sum(sF9,a,additive_identity)
| ~ spl12_8
| ~ spl12_9
| ~ spl12_153 ),
inference(resolution,[],[f6570,f5]) ).
fof(f6879,plain,
( sum(sF9,b,b)
| ~ spl12_8
| ~ spl12_9
| ~ spl12_153 ),
inference(resolution,[],[f6782,f6534]) ).
fof(f6889,plain,
( spl12_38
| ~ spl12_8
| ~ spl12_9
| ~ spl12_153 ),
inference(avatar_split_clause,[],[f6879,f2039,f107,f103,f730]) ).
fof(f7455,plain,
( product(multiplicative_inverse(sF9),b,sF2)
| ~ defined(sF9)
| spl12_9 ),
inference(forward_subsumption_resolution,[],[f2043,f108]) ).
fof(f7459,plain,
( product(multiplicative_inverse(sF9),d,sF0)
| ~ defined(sF9)
| spl12_9 ),
inference(forward_subsumption_resolution,[],[f2454,f108]) ).
fof(f7468,plain,
( product(multiplicative_inverse(sF9),b,sF2)
| ~ spl12_8
| spl12_9 ),
inference(forward_subsumption_resolution,[],[f7455,f104]) ).
fof(f7472,plain,
( product(multiplicative_inverse(sF9),d,sF0)
| ~ spl12_8
| spl12_9 ),
inference(forward_subsumption_resolution,[],[f7459,f104]) ).
fof(f7474,plain,
( product(sF10,b,sF2)
| ~ spl12_8
| spl12_9 ),
inference(forward_demodulation,[],[f7468,f55]) ).
fof(f7478,plain,
( product(sF10,d,sF0)
| ~ spl12_8
| spl12_9 ),
inference(forward_demodulation,[],[f7472,f55]) ).
fof(f7561,plain,
( product(sF10,sF5,sF1)
| ~ spl12_8
| spl12_9 ),
inference(resolution,[],[f7478,f2797]) ).
fof(f7712,plain,
( product(sF5,sF10,sF1)
| ~ spl12_8
| spl12_9 ),
inference(resolution,[],[f7561,f10]) ).
fof(f7730,plain,
( ! [X2,X3,X0,X1] :
( ~ product(X1,sF10,X3)
| sum(X2,X3,sF1)
| ~ product(X0,sF10,X2)
| ~ sum(X0,X1,sF5) )
| ~ spl12_8
| spl12_9 ),
inference(resolution,[],[f7712,f11]) ).
fof(f7991,plain,
( ~ defined(sF9)
| defined(multiplicative_inverse(sF9))
| spl12_9 ),
inference(resolution,[],[f108,f18]) ).
fof(f7992,plain,
( defined(multiplicative_inverse(sF9))
| ~ spl12_8
| spl12_9 ),
inference(forward_subsumption_resolution,[],[f7991,f104]) ).
fof(f7993,plain,
( defined(sF10)
| ~ spl12_8
| spl12_9 ),
inference(forward_demodulation,[],[f7992,f55]) ).
fof(f7994,plain,
( $false
| ~ spl12_8
| spl12_9
| spl12_13 ),
inference(forward_subsumption_resolution,[],[f7993,f203]) ).
fof(f7995,plain,
( ~ spl12_8
| spl12_9
| spl12_13 ),
inference(avatar_contradiction_clause,[],[f7994]) ).
fof(f7996,plain,
( defined(sF11)
| ~ defined(sF10)
| ~ spl12_14 ),
inference(forward_subsumption_resolution,[],[f228,f206]) ).
fof(f8029,plain,
( defined(sF11)
| ~ spl12_13
| ~ spl12_14 ),
inference(forward_subsumption_resolution,[],[f7996,f202]) ).
fof(f9843,plain,
! [X0,X1] :
( ~ defined(X0)
| ~ defined(X1)
| ~ sum(X1,X0,X0)
| sum(additive_identity,X1,additive_identity)
| ~ defined(X0) ),
inference(resolution,[],[f2546,f539]) ).
fof(f9914,plain,
! [X0,X1] :
( ~ sum(X1,X0,X0)
| ~ defined(X1)
| ~ defined(X0)
| sum(additive_identity,X1,additive_identity) ),
inference(duplicate_literal_removal,[],[f9843]) ).
fof(f11702,plain,
( ! [X0,X1] :
( ~ product(X1,sF10,X0)
| sum(X0,sF11,sF1)
| ~ sum(X1,sF8,sF5) )
| ~ spl12_8
| spl12_9
| ~ spl12_15 ),
inference(resolution,[],[f7730,f211]) ).
fof(f14251,plain,
( sum(b,multiplicative_identity,multiplicative_identity)
| ~ sum(sF9,d,d) ),
inference(resolution,[],[f6133,f1797]) ).
fof(f14255,plain,
( ~ sum(sF9,d,d)
| spl12_39 ),
inference(forward_subsumption_resolution,[],[f14251,f737]) ).
fof(f14258,plain,
( ~ spl12_40
| spl12_39 ),
inference(avatar_split_clause,[],[f14255,f735,f739]) ).
fof(f14435,plain,
( sum(d,multiplicative_identity,multiplicative_identity)
| ~ sum(sF9,b,b) ),
inference(resolution,[],[f5587,f1446]) ).
fof(f19320,plain,
( ~ defined(a)
| ~ defined(sF1)
| sum(additive_identity,a,additive_identity)
| ~ spl12_34 ),
inference(resolution,[],[f9914,f639]) ).
fof(f20137,plain,
( sum(sF6,sF8,sF5)
| ~ spl12_3
| ~ spl12_6
| ~ spl12_7 ),
inference(resolution,[],[f405,f247]) ).
fof(f20212,plain,
! [X0] :
( ~ product(X0,b,sF2)
| product(X0,sF6,sF3) ),
inference(resolution,[],[f1393,f219]) ).
fof(f20215,plain,
( product(sF10,sF6,sF3)
| ~ spl12_8
| spl12_9 ),
inference(resolution,[],[f20212,f7474]) ).
fof(f20220,plain,
( product(sF6,sF10,sF3)
| ~ spl12_8
| spl12_9 ),
inference(resolution,[],[f20215,f10]) ).
fof(f20251,plain,
( sum(sF3,sF11,sF1)
| ~ sum(sF6,sF8,sF5)
| ~ spl12_8
| spl12_9
| ~ spl12_15 ),
inference(resolution,[],[f20220,f11702]) ).
fof(f20274,plain,
( sum(sF3,sF11,sF1)
| ~ spl12_3
| ~ spl12_6
| ~ spl12_7
| ~ spl12_8
| spl12_9
| ~ spl12_15 ),
inference(forward_subsumption_resolution,[],[f20251,f20137]) ).
fof(f20304,plain,
( sum(sF11,sF3,sF1)
| ~ spl12_3
| ~ spl12_6
| ~ spl12_7
| ~ spl12_8
| spl12_9
| ~ spl12_15 ),
inference(resolution,[],[f20274,f5]) ).
fof(f20325,plain,
( sum(sF1,sF4,sF11)
| ~ defined(sF11)
| ~ spl12_1
| ~ spl12_3
| ~ spl12_6
| ~ spl12_7
| ~ spl12_8
| spl12_9
| ~ spl12_15 ),
inference(resolution,[],[f20304,f2560]) ).
fof(f20339,plain,
( ~ defined(sF11)
| ~ spl12_1
| ~ spl12_3
| ~ spl12_6
| ~ spl12_7
| ~ spl12_8
| spl12_9
| ~ spl12_15 ),
inference(forward_subsumption_resolution,[],[f20325,f58]) ).
fof(f20340,plain,
( $false
| ~ spl12_1
| ~ spl12_3
| ~ spl12_6
| ~ spl12_7
| ~ spl12_8
| spl12_9
| ~ spl12_13
| ~ spl12_14
| ~ spl12_15 ),
inference(forward_subsumption_resolution,[],[f20339,f8029]) ).
fof(f20341,plain,
( ~ spl12_1
| ~ spl12_3
| ~ spl12_6
| ~ spl12_7
| ~ spl12_8
| spl12_9
| ~ spl12_13
| ~ spl12_14
| ~ spl12_15 ),
inference(avatar_contradiction_clause,[],[f20340]) ).
fof(f20343,plain,
( ~ sum(sF9,b,b)
| spl12_37 ),
inference(forward_subsumption_resolution,[],[f14435,f728]) ).
fof(f20425,plain,
( ! [X0] :
( sum(sF9,X0,X0)
| ~ defined(X0) )
| ~ spl12_9 ),
inference(resolution,[],[f495,f400]) ).
fof(f20531,plain,
( ~ defined(d)
| ~ defined(multiplicative_identity)
| sum(additive_identity,d,additive_identity)
| ~ spl12_37 ),
inference(resolution,[],[f727,f9914]) ).
fof(f20549,plain,
( ~ defined(multiplicative_identity)
| sum(additive_identity,d,additive_identity)
| ~ spl12_37 ),
inference(forward_subsumption_resolution,[],[f20531,f30]) ).
fof(f20550,plain,
( sum(additive_identity,d,additive_identity)
| ~ spl12_37 ),
inference(forward_subsumption_resolution,[],[f20549,f17]) ).
fof(f20551,plain,
( $false
| ~ spl12_37 ),
inference(forward_subsumption_resolution,[],[f20550,f32]) ).
fof(f20552,plain,
~ spl12_37,
inference(avatar_contradiction_clause,[],[f20551]) ).
fof(f20554,plain,
( ~ spl12_38
| spl12_37 ),
inference(avatar_split_clause,[],[f20343,f726,f730]) ).
fof(f20682,plain,
( ~ defined(sF1)
| sum(additive_identity,a,additive_identity)
| ~ spl12_34 ),
inference(forward_subsumption_resolution,[],[f19320,f27]) ).
fof(f20728,plain,
( sum(additive_identity,a,additive_identity)
| ~ spl12_34 ),
inference(forward_subsumption_resolution,[],[f20682,f238]) ).
fof(f20753,plain,
( $false
| spl12_16
| ~ spl12_34 ),
inference(forward_subsumption_resolution,[],[f20728,f350]) ).
fof(f20754,plain,
( spl12_16
| ~ spl12_34 ),
inference(avatar_contradiction_clause,[],[f20753]) ).
fof(f21259,plain,
( ~ defined(d)
| ~ spl12_9
| spl12_40 ),
inference(resolution,[],[f20425,f740]) ).
fof(f21327,plain,
( $false
| ~ spl12_9
| spl12_40 ),
inference(forward_subsumption_resolution,[],[f21259,f30]) ).
fof(f21328,plain,
( ~ spl12_9
| spl12_40 ),
inference(avatar_contradiction_clause,[],[f21327]) ).
cnf(s3,plain,
( ~ spl12_5
| ~ spl12_6
| spl12_7 ),
inference(sat_conversion,[],[f92]) ).
cnf(s12,plain,
( ~ spl12_13
| ~ spl12_14
| spl12_15 ),
inference(sat_conversion,[],[f212]) ).
cnf(s13,plain,
spl12_1,
inference(sat_conversion,[],[f240]) ).
cnf(s14,plain,
spl12_3,
inference(sat_conversion,[],[f242]) ).
cnf(s15,plain,
spl12_8,
inference(sat_conversion,[],[f244]) ).
cnf(s16,plain,
spl12_6,
inference(sat_conversion,[],[f245]) ).
cnf(s17,plain,
( ~ spl12_3
| spl12_5 ),
inference(sat_conversion,[],[f253]) ).
cnf(s18,plain,
( ~ spl12_5
| ~ spl12_6
| spl12_14 ),
inference(sat_conversion,[],[f297]) ).
cnf(s28,plain,
( ~ spl12_33
| spl12_34 ),
inference(sat_conversion,[],[f640]) ).
cnf(s43,plain,
( spl12_33
| ~ spl12_39 ),
inference(sat_conversion,[],[f815]) ).
cnf(s151,plain,
( ~ spl12_16
| spl12_153 ),
inference(sat_conversion,[],[f4410]) ).
cnf(s249,plain,
( ~ spl12_8
| ~ spl12_9
| spl12_38
| ~ spl12_153 ),
inference(sat_conversion,[],[f6889]) ).
cnf(s284,plain,
( ~ spl12_8
| spl12_9
| spl12_13 ),
inference(sat_conversion,[],[f7995]) ).
cnf(s477,plain,
( spl12_39
| ~ spl12_40 ),
inference(sat_conversion,[],[f14258]) ).
cnf(s609,plain,
( ~ spl12_1
| ~ spl12_3
| ~ spl12_6
| ~ spl12_7
| ~ spl12_8
| spl12_9
| ~ spl12_13
| ~ spl12_14
| ~ spl12_15 ),
inference(sat_conversion,[],[f20341]) ).
cnf(s622,plain,
~ spl12_37,
inference(sat_conversion,[],[f20552]) ).
cnf(s624,plain,
( spl12_37
| ~ spl12_38 ),
inference(sat_conversion,[],[f20554]) ).
cnf(s648,plain,
( spl12_16
| ~ spl12_34 ),
inference(sat_conversion,[],[f20754]) ).
cnf(s662,plain,
( ~ spl12_9
| spl12_40 ),
inference(sat_conversion,[],[f21328]) ).
cnf(s664,plain,
~ spl12_38,
inference(rat,[],[s624,s622]) ).
cnf(s675,plain,
( ~ spl12_8
| ~ spl12_9
| ~ spl12_153 ),
inference(rat,[],[s249,s664]) ).
cnf(s684,plain,
spl12_5,
inference(rat,[],[s17,s14]) ).
cnf(s685,plain,
spl12_14,
inference(rat,[],[s18,s16,s684]) ).
cnf(s686,plain,
( ~ spl12_13
| spl12_15 ),
inference(rat,[],[s12,s685]) ).
cnf(s689,plain,
spl12_7,
inference(rat,[],[s3,s16,s684]) ).
cnf(s692,plain,
spl12_9,
inference(rat,[],[s609,s686,s284,s16,s14,s15,s13,s689,s685]) ).
cnf(s694,plain,
spl12_40,
inference(rat,[],[s662,s692]) ).
cnf(s695,plain,
~ spl12_153,
inference(rat,[],[s675,s15,s692]) ).
cnf(s698,plain,
spl12_39,
inference(rat,[],[s477,s694]) ).
cnf(s701,plain,
~ spl12_16,
inference(rat,[],[s151,s695]) ).
cnf(s704,plain,
spl12_33,
inference(rat,[],[s43,s698]) ).
cnf(s708,plain,
~ spl12_34,
inference(rat,[],[s648,s701]) ).
cnf(s716,plain,
$false,
inference(rat,[],[s28,s708,s704]) ).
fof(f21332,plain,
$false,
inference(avatar_sat_refutation,[],[s716]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : FLD053-3 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n013.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 00:41:21 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running first-order theorem proving
% 0.09/0.24 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
% 11.13/2.26 % (1751051)Input is clausal, will run a generic CNF schedule.
% 11.13/2.26 % (1751060)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3532081821:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.13/2.26 % (1751060)Instruction limit reached!
% 11.13/2.26 % (1751060)------------------------------
% 11.13/2.26 % (1751060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.13/2.26 % (1751060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.13/2.26 % (1751060)CaDiCaL version: 2.1.3
% 11.13/2.26 % (1751060)Termination reason: Instruction limit
% 11.13/2.26 % (1751060)Termination phase: Saturation
% 11.13/2.26 % (1751060)Time elapsed: 0.037 s
% 11.13/2.26 % (1751060)Peak memory usage: 88 MB
% 11.13/2.26 % (1751060)Instructions burned: 117 (million)
% 11.13/2.26 % (1751057)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3664153982:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.13/2.26 % (1751056)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=3521147299:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.13/2.26 % (1751058)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2223488041:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.13/2.26 % (1751059)lrs+10_1_sil=8000:sp=occurrence:random_seed=326330202:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.13/2.26 % (1751061)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3072368562:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.13/2.26 % (1751062)dis-21_1_sil=8000:lcm=predicate:random_seed=384283619: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)
% 11.13/2.26 % (1751059)Instruction limit reached!
% 11.13/2.26 % (1751059)------------------------------
% 11.13/2.26 % (1751059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.13/2.26 % (1751059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.13/2.26 % (1751059)CaDiCaL version: 2.1.3
% 11.13/2.26 % (1751059)Termination reason: Instruction limit
% 11.13/2.26 % (1751059)Termination phase: Saturation
% 11.13/2.26 % (1751059)Time elapsed: 0.067 s
% 11.13/2.26 % (1751059)Peak memory usage: 89 MB
% 11.13/2.26 % (1751059)Instructions burned: 108 (million)
% 11.13/2.26 % (1751062)Instruction limit reached!
% 11.13/2.26 % (1751062)------------------------------
% 11.13/2.26 % (1751062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.13/2.26 % (1751062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.13/2.26 % (1751062)CaDiCaL version: 2.1.3
% 11.13/2.26 % (1751062)Termination reason: Instruction limit
% 11.13/2.26 % (1751062)Termination phase: Saturation
% 11.13/2.26 % (1751062)Time elapsed: 0.073 s
% 11.13/2.26 % (1751062)Peak memory usage: 89 MB
% 11.13/2.26 % (1751062)Instructions burned: 118 (million)
% 11.13/2.26 % (1751064)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=4214968257:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 11.13/2.26 % (1751061)Instruction limit reached!
% 11.13/2.26 % (1751061)------------------------------
% 11.13/2.26 % (1751061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.13/2.26 % (1751061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.13/2.26 % (1751061)CaDiCaL version: 2.1.3
% 11.13/2.26 % (1751061)Termination reason: Instruction limit
% 11.13/2.26 % (1751061)Termination phase: Saturation
% 11.13/2.26 % (1751061)Time elapsed: 0.108 s
% 11.13/2.26 % (1751061)Peak memory usage: 89 MB
% 11.13/2.26 % (1751061)Instructions burned: 181 (million)
% 11.13/2.26 % (1751064)Instruction limit reached!
% 11.13/2.26 % (1751064)------------------------------
% 11.13/2.26 % (1751064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.13/2.26 % (1751064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.13/2.26 % (1751064)CaDiCaL version: 2.1.3
% 11.13/2.26 % (1751064)Termination reason: Instruction limit
% 11.13/2.26 % (1751064)Termination phase: Saturation
% 11.13/2.26 % (1751064)Time elapsed: 0.031 s
% 11.13/2.26 % (1751064)Peak memory usage: 87 MB
% 11.13/2.26 % (1751064)Instructions burned: 145 (million)
% 11.13/2.26 % (1751071)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2668234035: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)
% 17.84/3.14 % (1751072)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=455778521:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 17.84/3.14 % (1751075)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3479535116:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 17.84/3.14 % (1751074)lrs+10_64_to=lpo:sil=8000:random_seed=3309484513:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 17.84/3.14 % (1751071)Instruction limit reached!
% 17.84/3.14 % (1751071)------------------------------
% 17.84/3.14 % (1751071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.14 % (1751071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.14 % (1751071)CaDiCaL version: 2.1.3
% 17.84/3.14 % (1751071)Termination reason: Instruction limit
% 17.84/3.14 % (1751071)Termination phase: Saturation
% 17.84/3.14 % (1751071)Time elapsed: 0.097 s
% 17.84/3.14 % (1751071)Peak memory usage: 93 MB
% 17.84/3.14 % (1751071)Instructions burned: 191 (million)
% 17.84/3.14 % (1751075)Instruction limit reached!
% 17.84/3.14 % (1751075)------------------------------
% 17.84/3.14 % (1751075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.14 % (1751075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.14 % (1751075)CaDiCaL version: 2.1.3
% 17.84/3.14 % (1751075)Termination reason: Instruction limit
% 17.84/3.14 % (1751075)Termination phase: Saturation
% 17.84/3.14 % (1751075)Time elapsed: 0.067 s
% 17.84/3.14 % (1751075)Peak memory usage: 89 MB
% 17.84/3.14 % (1751075)Instructions burned: 196 (million)
% 17.84/3.14 % (1751074)Instruction limit reached!
% 17.84/3.14 % (1751074)------------------------------
% 17.84/3.14 % (1751074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.14 % (1751074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.14 % (1751074)CaDiCaL version: 2.1.3
% 17.84/3.14 % (1751074)Termination reason: Instruction limit
% 17.84/3.14 % (1751074)Termination phase: Saturation
% 17.84/3.14 % (1751074)Time elapsed: 0.071 s
% 17.84/3.14 % (1751074)Peak memory usage: 89 MB
% 17.84/3.14 % (1751074)Instructions burned: 127 (million)
% 17.84/3.14 % (1751072)Instruction limit reached!
% 17.84/3.14 % (1751072)------------------------------
% 17.84/3.14 % (1751072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.14 % (1751072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.14 % (1751072)CaDiCaL version: 2.1.3
% 17.84/3.14 % (1751072)Termination reason: Instruction limit
% 17.84/3.14 % (1751072)Termination phase: Saturation
% 17.84/3.14 % (1751072)Time elapsed: 0.131 s
% 17.84/3.14 % (1751072)Peak memory usage: 89 MB
% 17.84/3.14 % (1751072)Instructions burned: 219 (million)
% 17.84/3.14 % (1751081)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=747409966:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 17.84/3.14 % (1751080)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3495269954:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 17.84/3.14 % (1751082)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=1969206933:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 17.84/3.14 % (1751083)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2241328221:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 17.84/3.14 % (1751082)Instruction limit reached!
% 17.84/3.14 % (1751082)------------------------------
% 17.84/3.14 % (1751082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.14 % (1751082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.14 % (1751082)CaDiCaL version: 2.1.3
% 17.84/3.14 % (1751082)Termination reason: Instruction limit
% 17.84/3.14 % (1751082)Termination phase: Saturation
% 17.84/3.14 % (1751082)Time elapsed: 0.054 s
% 17.84/3.14 % (1751082)Peak memory usage: 90 MB
% 17.84/3.14 % (1751082)Instructions burned: 106 (million)
% 17.84/3.14 % (1751080)Instruction limit reached!
% 17.84/3.14 % (1751080)------------------------------
% 17.84/3.14 % (1751080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/4.05 % (1751080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/4.05 % (1751080)CaDiCaL version: 2.1.3
% 20.88/4.05 % (1751080)Termination reason: Instruction limit
% 20.88/4.05 % (1751080)Termination phase: Saturation
% 20.88/4.05 % (1751080)Time elapsed: 0.109 s
% 20.88/4.05 % (1751080)Peak memory usage: 90 MB
% 20.88/4.05 % (1751080)Instructions burned: 157 (million)
% 20.88/4.05 % (1751083)Instruction limit reached!
% 20.88/4.05 % (1751083)------------------------------
% 20.88/4.05 % (1751083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/4.05 % (1751083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/4.05 % (1751083)CaDiCaL version: 2.1.3
% 20.88/4.05 % (1751083)Termination reason: Instruction limit
% 20.88/4.05 % (1751083)Termination phase: Saturation
% 20.88/4.05 % (1751083)Time elapsed: 0.072 s
% 20.88/4.05 % (1751083)Peak memory usage: 89 MB
% 20.88/4.05 % (1751083)Instructions burned: 107 (million)
% 20.88/4.05 % (1751088)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=446234757:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 20.88/4.05 % (1751089)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1869316110:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 20.88/4.05 % (1751090)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2165431014:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi)
% 20.88/4.05 % (1751088)Instruction limit reached!
% 20.88/4.05 % (1751088)------------------------------
% 20.88/4.05 % (1751088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/4.05 % (1751088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/4.05 % (1751088)CaDiCaL version: 2.1.3
% 20.88/4.05 % (1751088)Termination reason: Instruction limit
% 20.88/4.05 % (1751088)Termination phase: Saturation
% 20.88/4.05 % (1751088)Time elapsed: 0.150 s
% 20.88/4.05 % (1751088)Peak memory usage: 89 MB
% 20.88/4.05 % (1751088)Instructions burned: 243 (million)
% 20.88/4.05 % (1751090)Instruction limit reached!
% 20.88/4.05 % (1751090)------------------------------
% 20.88/4.05 % (1751090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/4.05 % (1751090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/4.05 % (1751090)CaDiCaL version: 2.1.3
% 20.88/4.05 % (1751090)Termination reason: Instruction limit
% 20.88/4.05 % (1751090)Termination phase: Saturation
% 20.88/4.05 % (1751090)Time elapsed: 0.082 s
% 20.88/4.05 % (1751090)Peak memory usage: 89 MB
% 20.88/4.05 % (1751090)Instructions burned: 134 (million)
% 20.88/4.05 % (1751095)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2145478372:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 20.88/4.05 % (1751094)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1523851339:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 20.88/4.05 % (1751095)Instruction limit reached!
% 20.88/4.05 % (1751095)------------------------------
% 20.88/4.05 % (1751095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/4.05 % (1751095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/4.05 % (1751095)CaDiCaL version: 2.1.3
% 20.88/4.05 % (1751095)Termination reason: Instruction limit
% 20.88/4.05 % (1751095)Termination phase: Saturation
% 20.88/4.05 % (1751095)Time elapsed: 0.110 s
% 20.88/4.05 % (1751095)Peak memory usage: 91 MB
% 20.88/4.05 % (1751095)Instructions burned: 192 (million)
% 20.88/4.05 % (1751094)Instruction limit reached!
% 20.88/4.05 % (1751094)------------------------------
% 20.88/4.05 % (1751094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/4.05 % (1751094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/4.05 % (1751094)CaDiCaL version: 2.1.3
% 20.88/4.05 % (1751094)Termination reason: Instruction limit
% 20.88/4.05 % (1751094)Termination phase: Saturation
% 20.88/4.05 % (1751094)Time elapsed: 0.263 s
% 20.88/4.05 % (1751094)Peak memory usage: 105 MB
% 20.88/4.05 % (1751094)Instructions burned: 500 (million)
% 20.88/4.05 % (1751098)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4066051433:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi)
% 20.88/4.05 % (1751100)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3092595750:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 20.88/4.05 % (1751098)Instruction limit reached!
% 20.88/4.05 % (1751098)------------------------------
% 20.88/4.05 % (1751098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/4.05 % (1751098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/4.05 % (1751098)CaDiCaL version: 2.1.3
% 20.88/4.05 % (1751098)Termination reason: Instruction limit
% 20.88/4.05 % (1751098)Termination phase: Saturation
% 20.88/4.05 % (1751098)Time elapsed: 0.164 s
% 20.88/4.05 % (1751098)Peak memory usage: 90 MB
% 20.88/4.05 % (1751098)Instructions burned: 265 (million)
% 20.88/4.05 % (1751100)Instruction limit reached!
% 20.88/4.05 % (1751100)------------------------------
% 20.88/4.05 % (1751100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/4.05 % (1751100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/4.05 % (1751100)CaDiCaL version: 2.1.3
% 20.88/4.05 % (1751100)Termination reason: Instruction limit
% 20.88/4.05 % (1751100)Termination phase: Saturation
% 20.88/4.05 % (1751100)Time elapsed: 0.066 s
% 20.88/4.05 % (1751100)Peak memory usage: 88 MB
% 20.88/4.05 % (1751100)Instructions burned: 158 (million)
% 20.88/4.05 % (1751081)Instruction limit reached!
% 20.88/4.05 % (1751081)------------------------------
% 20.88/4.05 % (1751081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/4.05 % (1751081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/4.05 % (1751081)CaDiCaL version: 2.1.3
% 20.88/4.05 % (1751081)Termination reason: Instruction limit
% 20.88/4.05 % (1751081)Termination phase: Saturation
% 20.88/4.05 % (1751081)Time elapsed: 1.156 s
% 20.88/4.05 % (1751081)Peak memory usage: 149 MB
% 20.88/4.05 % (1751081)Instructions burned: 3395 (million)
% 20.88/4.05 % (1751102)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=443365988:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 20.88/4.05 % (1751103)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2684676477:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi)
% 20.88/4.05 % (1751105)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=874396092:i=180:bd=preordered:av=off_2982 on theBenchmark for (2982ds/180Mi)
% 20.88/4.05 % (1751105)Instruction limit reached!
% 20.88/4.05 % (1751105)------------------------------
% 20.88/4.05 % (1751105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/4.05 % (1751105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/4.05 % (1751105)CaDiCaL version: 2.1.3
% 20.88/4.05 % (1751105)Termination reason: Instruction limit
% 20.88/4.05 % (1751105)Termination phase: Saturation
% 20.88/4.05 % (1751105)Time elapsed: 0.049 s
% 20.88/4.05 % (1751105)Peak memory usage: 93 MB
% 20.88/4.05 % (1751105)Instructions burned: 183 (million)
% 20.88/4.05 % (1751108)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=3405893278:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2980 on theBenchmark for (2980ds/10307Mi)
% 20.88/4.05 % (1751103)Instruction limit reached!
% 20.88/4.05 % (1751103)------------------------------
% 20.88/4.05 % (1751103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/4.05 % (1751103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/4.05 % (1751103)CaDiCaL version: 2.1.3
% 20.88/4.05 % (1751103)Termination reason: Instruction limit
% 20.88/4.05 % (1751103)Termination phase: Saturation
% 20.88/4.05 % (1751103)Time elapsed: 0.304 s
% 20.88/4.05 % (1751103)Peak memory usage: 92 MB
% 20.88/4.05 % (1751103)Instructions burned: 537 (million)
% 20.88/4.05 % (1751110)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=2347424749:i=412:gtgl=4:gtg=exists_all_2978 on theBenchmark for (2978ds/412Mi)
% 20.88/4.05 % (1751110)Instruction limit reached!
% 20.88/4.05 % (1751110)------------------------------
% 20.88/4.05 % (1751110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/4.05 % (1751110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/4.05 % (1751110)CaDiCaL version: 2.1.3
% 20.88/4.05 % (1751110)Termination reason: Instruction limit
% 20.88/4.05 % (1751110)Termination phase: Saturation
% 20.88/4.05 % (1751110)Time elapsed: 0.186 s
% 20.88/4.05 % (1751110)Peak memory usage: 91 MB
% 20.88/4.05 % (1751110)Instructions burned: 412 (million)
% 20.88/4.05 % (1751112)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=3266033368:s2pl=no:i=8478:s2at=4:nm=6_2975 on theBenchmark for (2975ds/8478Mi)
% 20.88/4.05 % (1751056)First to succeed.
% 20.88/4.05 % (1751056)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1751051"
% 20.88/4.05 % (1751056)Refutation found. Thanks to Tanya!
% 20.88/4.05 % SZS status Unsatisfiable for theBenchmark
% 20.88/4.05 % SZS output start Proof for theBenchmark
% See solution above
% 24.56/4.25 % (1751056)------------------------------
% 24.56/4.25 % (1751056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.56/4.25 % (1751056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.56/4.25 % (1751056)CaDiCaL version: 2.1.3
% 24.56/4.25 % (1751056)Termination reason: Refutation
% 24.56/4.25 % (1751056)Time elapsed: 2.935 s
% 24.56/4.25 % (1751056)Peak memory usage: 155 MB
% 24.56/4.25 % (1751056)Instructions burned: 4337 (million)
% 24.56/4.25 % (1751056)------------------------------
% 24.56/4.25 % (1751056)------------------------------
% 24.56/4.25 % (1751051)Success in time 3.382 s
% 24.56/4.25 % Vampire exiting
%------------------------------------------------------------------------------