%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP113-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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 10:12:37 AM UTC 2026
% Result : Unsatisfiable 9.44s 2.32s
% Output : Refutation 10.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 55
% Syntax : Number of formulae : 767 ( 66 unt; 39 def)
% Number of atoms : 2391 ( 722 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 2777 (1153 ~;1585 |; 0 &)
% ( 39 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 41 ( 39 usr; 40 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 76 ( 0 sgn 76 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_inverse) ).
fof(f3,plain,
! [X0] : identity = multiply(inverse(X0),X0),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity) ).
fof(f5,axiom,
! [X0] : multiply(X0,identity) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_identity) ).
fof(f6,axiom,
! [X0] : multiply(X0,inverse(X0)) = identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_inverse) ).
fof(f7,plain,
! [X0] : identity = multiply(X0,inverse(X0)),
inference(reorient_equations,[],[f6]) ).
fof(f8,axiom,
! [X0] :
( X0 = a
| X0 = b
| X0 = c
| X0 = identity ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',all_of_group1) ).
fof(f9,plain,
! [X0] :
( identity = X0
| b = X0
| c = X0
| a = X0 ),
inference(reorient_equations,[],[f8]) ).
fof(f10,axiom,
a != b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_not_b) ).
fof(f11,axiom,
a != c,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_not_c) ).
fof(f12,axiom,
a != identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_not_identity) ).
fof(f13,plain,
identity != a,
inference(reorient_equations,[],[f12]) ).
fof(f14,axiom,
b != c,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b_not_c) ).
fof(f15,axiom,
b != identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b_not_identity) ).
fof(f16,plain,
identity != b,
inference(reorient_equations,[],[f15]) ).
fof(f17,axiom,
c != identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_not_identity) ).
fof(f18,plain,
identity != c,
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
( multiply(a,a) != identity
| multiply(b,b) != identity
| multiply(c,c) != identity ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',square_identity) ).
fof(f20,plain,
( identity != multiply(a,a)
| identity != multiply(b,b)
| identity != multiply(c,c) ),
inference(reorient_equations,[],[f19]) ).
fof(f21,negated_conjecture,
( multiply(a,a) != b
| multiply(a,multiply(a,a)) != c
| multiply(a,multiply(a,multiply(a,a))) != identity ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condition_a) ).
fof(f22,plain,
( b != multiply(a,a)
| c != multiply(a,multiply(a,a))
| identity != multiply(a,multiply(a,multiply(a,a))) ),
inference(reorient_equations,[],[f21]) ).
fof(f23,negated_conjecture,
( multiply(b,b) != c
| multiply(b,multiply(b,b)) != a
| multiply(b,multiply(b,multiply(b,b))) != identity ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condition_b) ).
fof(f24,plain,
( c != multiply(b,b)
| a != multiply(b,multiply(b,b))
| identity != multiply(b,multiply(b,multiply(b,b))) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( multiply(c,c) != a
| multiply(c,multiply(c,c)) != b
| multiply(c,multiply(c,multiply(c,c))) != identity ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condition_c) ).
fof(f26,plain,
( a != multiply(c,c)
| b != multiply(c,multiply(c,c))
| identity != multiply(c,multiply(c,multiply(c,c))) ),
inference(reorient_equations,[],[f25]) ).
fof(f28,definition,
( spl0_1
<=> identity = multiply(c,multiply(c,multiply(c,c))) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f29,plain,
( identity = multiply(c,multiply(c,multiply(c,c)))
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f28]) ).
fof(f30,plain,
( identity != multiply(c,multiply(c,multiply(c,c)))
| spl0_1 ),
inference(avatar_component_clause,[],[f28]) ).
fof(f32,definition,
( spl0_2
<=> b = multiply(c,multiply(c,c)) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f33,plain,
( b = multiply(c,multiply(c,c))
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f32]) ).
fof(f34,plain,
( b != multiply(c,multiply(c,c))
| spl0_2 ),
inference(avatar_component_clause,[],[f32]) ).
fof(f36,definition,
( spl0_3
<=> a = multiply(c,c) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f37,plain,
( a = multiply(c,c)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f36]) ).
fof(f38,plain,
( a != multiply(c,c)
| spl0_3 ),
inference(avatar_component_clause,[],[f36]) ).
fof(f39,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f26,f36,f32,f28]) ).
fof(f41,definition,
( spl0_4
<=> identity = multiply(b,multiply(b,multiply(b,b))) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f42,plain,
( identity = multiply(b,multiply(b,multiply(b,b)))
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f41]) ).
fof(f43,plain,
( identity != multiply(b,multiply(b,multiply(b,b)))
| spl0_4 ),
inference(avatar_component_clause,[],[f41]) ).
fof(f45,definition,
( spl0_5
<=> a = multiply(b,multiply(b,b)) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f46,plain,
( a = multiply(b,multiply(b,b))
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f45]) ).
fof(f49,definition,
( spl0_6
<=> c = multiply(b,b) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f50,plain,
( c = multiply(b,b)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f49]) ).
fof(f51,plain,
( c != multiply(b,b)
| spl0_6 ),
inference(avatar_component_clause,[],[f49]) ).
fof(f52,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f24,f49,f45,f41]) ).
fof(f54,definition,
( spl0_7
<=> identity = multiply(a,multiply(a,multiply(a,a))) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f55,plain,
( identity = multiply(a,multiply(a,multiply(a,a)))
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f54]) ).
fof(f56,plain,
( identity != multiply(a,multiply(a,multiply(a,a)))
| spl0_7 ),
inference(avatar_component_clause,[],[f54]) ).
fof(f58,definition,
( spl0_8
<=> c = multiply(a,multiply(a,a)) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f59,plain,
( c = multiply(a,multiply(a,a))
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f58]) ).
fof(f60,plain,
( c != multiply(a,multiply(a,a))
| spl0_8 ),
inference(avatar_component_clause,[],[f58]) ).
fof(f62,definition,
( spl0_9
<=> b = multiply(a,a) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f63,plain,
( b = multiply(a,a)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f62]) ).
fof(f64,plain,
( b != multiply(a,a)
| spl0_9 ),
inference(avatar_component_clause,[],[f62]) ).
fof(f65,plain,
( ~ spl0_7
| ~ spl0_8
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f22,f62,f58,f54]) ).
fof(f67,definition,
( spl0_10
<=> identity = multiply(c,c) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f68,plain,
( identity = multiply(c,c)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f67]) ).
fof(f69,plain,
( identity != multiply(c,c)
| spl0_10 ),
inference(avatar_component_clause,[],[f67]) ).
fof(f71,definition,
( spl0_11
<=> identity = multiply(b,b) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f72,plain,
( identity = multiply(b,b)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f71]) ).
fof(f73,plain,
( identity != multiply(b,b)
| spl0_11 ),
inference(avatar_component_clause,[],[f71]) ).
fof(f75,definition,
( spl0_12
<=> identity = multiply(a,a) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f76,plain,
( identity = multiply(a,a)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f75]) ).
fof(f77,plain,
( identity != multiply(a,a)
| spl0_12 ),
inference(avatar_component_clause,[],[f75]) ).
fof(f78,plain,
( ~ spl0_10
| ~ spl0_11
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f20,f75,f71,f67]) ).
fof(f82,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[],[f4,f3]) ).
fof(f83,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(forward_demodulation,[],[f82,f1]) ).
fof(f85,plain,
! [X0,X1] : multiply(identity,X1) = multiply(X0,multiply(inverse(X0),X1)),
inference(superposition,[],[f4,f7]) ).
fof(f86,plain,
! [X0,X1] : identity = multiply(X0,multiply(X1,inverse(multiply(X0,X1)))),
inference(superposition,[],[f4,f7]) ).
fof(f87,plain,
! [X0,X1] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(forward_demodulation,[],[f85,f1]) ).
fof(f92,plain,
identity = inverse(identity),
inference(superposition,[],[f3,f5]) ).
fof(f95,plain,
! [X0,X1] : multiply(X1,X0) = multiply(inverse(inverse(X1)),X0),
inference(superposition,[],[f83,f83]) ).
fof(f103,plain,
! [X0,X1] :
( multiply(inverse(X0),identity) = X1
| multiply(X0,X1) = b
| multiply(X0,X1) = c
| multiply(X0,X1) = a ),
inference(superposition,[],[f83,f9]) ).
fof(f104,plain,
! [X2,X0,X1] :
( multiply(X0,multiply(X1,X2)) = multiply(identity,X2)
| multiply(X0,X1) = b
| multiply(X0,X1) = c
| multiply(X0,X1) = a ),
inference(superposition,[],[f4,f9]) ).
fof(f108,plain,
( identity != identity
| b = multiply(a,a)
| c = multiply(a,a)
| a = multiply(a,a)
| spl0_12 ),
inference(superposition,[],[f77,f9]) ).
fof(f111,plain,
( identity != multiply(b,multiply(b,identity))
| b = multiply(b,b)
| c = multiply(b,b)
| a = multiply(b,b)
| spl0_4 ),
inference(superposition,[],[f43,f9]) ).
fof(f113,plain,
( identity != identity
| b = multiply(b,multiply(b,multiply(b,b)))
| c = multiply(b,multiply(b,multiply(b,b)))
| a = multiply(b,multiply(b,multiply(b,b)))
| spl0_4 ),
inference(superposition,[],[f43,f9]) ).
fof(f114,plain,
( identity != multiply(c,multiply(c,identity))
| b = multiply(c,c)
| c = multiply(c,c)
| a = multiply(c,c)
| spl0_1 ),
inference(superposition,[],[f30,f9]) ).
fof(f119,plain,
! [X0] :
( identity = multiply(identity,X0)
| inverse(X0) = b
| inverse(X0) = c
| inverse(X0) = a ),
inference(superposition,[],[f3,f9]) ).
fof(f124,plain,
( b = multiply(b,multiply(b,multiply(b,b)))
| c = multiply(b,multiply(b,multiply(b,b)))
| a = multiply(b,multiply(b,multiply(b,b)))
| spl0_4 ),
inference(trivial_inequality_removal,[],[f113]) ).
fof(f125,plain,
( b = multiply(a,a)
| c = multiply(a,a)
| a = multiply(a,a)
| spl0_12 ),
inference(trivial_inequality_removal,[],[f108]) ).
fof(f126,plain,
! [X0] :
( inverse(X0) = c
| inverse(X0) = b
| identity = X0
| inverse(X0) = a ),
inference(forward_demodulation,[],[f119,f1]) ).
fof(f143,plain,
( identity != multiply(c,c)
| b = multiply(c,c)
| c = multiply(c,c)
| a = multiply(c,c)
| spl0_1 ),
inference(forward_demodulation,[],[f114,f5]) ).
fof(f145,definition,
( spl0_16
<=> a = multiply(b,multiply(b,multiply(b,b))) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f147,plain,
( a = multiply(b,multiply(b,multiply(b,b)))
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f145]) ).
fof(f149,definition,
( spl0_17
<=> c = multiply(b,multiply(b,multiply(b,b))) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f151,plain,
( c = multiply(b,multiply(b,multiply(b,b)))
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f149]) ).
fof(f153,definition,
( spl0_18
<=> b = multiply(b,multiply(b,multiply(b,b))) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f155,plain,
( b = multiply(b,multiply(b,multiply(b,b)))
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f153]) ).
fof(f156,plain,
( spl0_16
| spl0_17
| spl0_18
| spl0_4 ),
inference(avatar_split_clause,[],[f124,f41,f153,f149,f145]) ).
fof(f158,plain,
( identity != multiply(b,b)
| b = multiply(b,b)
| c = multiply(b,b)
| a = multiply(b,b)
| spl0_4 ),
inference(forward_demodulation,[],[f111,f5]) ).
fof(f161,definition,
( spl0_19
<=> a = multiply(a,a) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f163,plain,
( a = multiply(a,a)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f161]) ).
fof(f165,definition,
( spl0_20
<=> c = multiply(a,a) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f167,plain,
( c = multiply(a,a)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f165]) ).
fof(f168,plain,
( spl0_19
| spl0_20
| spl0_9
| spl0_12 ),
inference(avatar_split_clause,[],[f125,f75,f62,f165,f161]) ).
fof(f172,plain,
! [X2,X0,X1] :
( multiply(X0,multiply(X1,X2)) = X2
| multiply(X0,X1) = b
| multiply(X0,X1) = c
| multiply(X0,X1) = a ),
inference(forward_demodulation,[],[f104,f1]) ).
fof(f173,plain,
! [X0,X1] :
( multiply(X0,X1) = c
| multiply(X0,X1) = b
| inverse(X0) = X1
| multiply(X0,X1) = a ),
inference(forward_demodulation,[],[f103,f5]) ).
fof(f174,plain,
( b = multiply(c,c)
| c = multiply(c,c)
| a = multiply(c,c)
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f143,f9]) ).
fof(f175,plain,
( b = multiply(b,b)
| c = multiply(b,b)
| a = multiply(b,b)
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f158,f9]) ).
fof(f180,definition,
( spl0_21
<=> c = multiply(c,c) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f181,plain,
( c != multiply(c,c)
| spl0_21 ),
inference(avatar_component_clause,[],[f180]) ).
fof(f182,plain,
( c = multiply(c,c)
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f180]) ).
fof(f184,definition,
( spl0_22
<=> b = multiply(c,c) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f185,plain,
( b != multiply(c,c)
| spl0_22 ),
inference(avatar_component_clause,[],[f184]) ).
fof(f186,plain,
( b = multiply(c,c)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f184]) ).
fof(f187,plain,
( spl0_3
| spl0_21
| spl0_22
| spl0_1 ),
inference(avatar_split_clause,[],[f174,f28,f184,f180,f36]) ).
fof(f189,definition,
( spl0_23
<=> a = multiply(b,b) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f190,plain,
( a != multiply(b,b)
| spl0_23 ),
inference(avatar_component_clause,[],[f189]) ).
fof(f191,plain,
( a = multiply(b,b)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f189]) ).
fof(f193,definition,
( spl0_24
<=> b = multiply(b,b) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f194,plain,
( b != multiply(b,b)
| spl0_24 ),
inference(avatar_component_clause,[],[f193]) ).
fof(f195,plain,
( b = multiply(b,b)
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f193]) ).
fof(f196,plain,
( spl0_23
| spl0_6
| spl0_24
| spl0_4 ),
inference(avatar_split_clause,[],[f175,f41,f193,f49,f189]) ).
fof(f205,plain,
( identity = multiply(b,identity)
| b = multiply(b,multiply(b,b))
| c = multiply(b,multiply(b,b))
| a = multiply(b,multiply(b,b))
| ~ spl0_4 ),
inference(superposition,[],[f42,f9]) ).
fof(f206,plain,
( multiply(b,multiply(b,b)) = multiply(inverse(b),identity)
| ~ spl0_4 ),
inference(superposition,[],[f83,f42]) ).
fof(f209,plain,
( multiply(b,multiply(b,b)) = inverse(b)
| ~ spl0_4 ),
inference(forward_demodulation,[],[f206,f5]) ).
fof(f210,plain,
( identity = b
| b = multiply(b,multiply(b,b))
| c = multiply(b,multiply(b,b))
| a = multiply(b,multiply(b,b))
| ~ spl0_4 ),
inference(forward_demodulation,[],[f205,f5]) ).
fof(f212,plain,
( b = multiply(b,multiply(b,b))
| c = multiply(b,multiply(b,b))
| a = multiply(b,multiply(b,b))
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f210,f16]) ).
fof(f214,plain,
( b = inverse(b)
| c = multiply(b,multiply(b,b))
| a = multiply(b,multiply(b,b))
| ~ spl0_4 ),
inference(forward_demodulation,[],[f212,f209]) ).
fof(f215,plain,
( c = inverse(b)
| b = inverse(b)
| a = multiply(b,multiply(b,b))
| ~ spl0_4 ),
inference(forward_demodulation,[],[f214,f209]) ).
fof(f216,plain,
( a = inverse(b)
| c = inverse(b)
| b = inverse(b)
| ~ spl0_4 ),
inference(forward_demodulation,[],[f215,f209]) ).
fof(f218,definition,
( spl0_25
<=> b = inverse(b) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f219,plain,
( b != inverse(b)
| spl0_25 ),
inference(avatar_component_clause,[],[f218]) ).
fof(f220,plain,
( b = inverse(b)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f218]) ).
fof(f222,definition,
( spl0_26
<=> c = inverse(b) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f223,plain,
( c != inverse(b)
| spl0_26 ),
inference(avatar_component_clause,[],[f222]) ).
fof(f224,plain,
( c = inverse(b)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f222]) ).
fof(f226,definition,
( spl0_27
<=> a = inverse(b) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f227,plain,
( a != inverse(b)
| spl0_27 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f228,plain,
( a = inverse(b)
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f229,plain,
( spl0_25
| spl0_26
| spl0_27
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f216,f41,f226,f222,f218]) ).
fof(f244,plain,
( identity = multiply(c,identity)
| b = multiply(c,multiply(c,c))
| c = multiply(c,multiply(c,c))
| a = multiply(c,multiply(c,c))
| ~ spl0_1 ),
inference(superposition,[],[f29,f9]) ).
fof(f245,plain,
( multiply(c,multiply(c,c)) = multiply(inverse(c),identity)
| ~ spl0_1 ),
inference(superposition,[],[f83,f29]) ).
fof(f248,plain,
( multiply(c,multiply(c,c)) = inverse(c)
| ~ spl0_1 ),
inference(forward_demodulation,[],[f245,f5]) ).
fof(f249,plain,
( identity = multiply(c,identity)
| c = multiply(c,multiply(c,c))
| a = multiply(c,multiply(c,c))
| ~ spl0_1
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f244,f34]) ).
fof(f251,plain,
( identity = c
| c = multiply(c,multiply(c,c))
| a = multiply(c,multiply(c,c))
| ~ spl0_1
| spl0_2 ),
inference(forward_demodulation,[],[f249,f5]) ).
fof(f253,plain,
( c = multiply(c,multiply(c,c))
| a = multiply(c,multiply(c,c))
| ~ spl0_1
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f251,f18]) ).
fof(f254,plain,
( c = inverse(c)
| a = multiply(c,multiply(c,c))
| ~ spl0_1
| spl0_2 ),
inference(forward_demodulation,[],[f253,f248]) ).
fof(f255,plain,
( a = inverse(c)
| c = inverse(c)
| ~ spl0_1
| spl0_2 ),
inference(forward_demodulation,[],[f254,f248]) ).
fof(f257,definition,
( spl0_28
<=> c = inverse(c) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f258,plain,
( c != inverse(c)
| spl0_28 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f259,plain,
( c = inverse(c)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f261,definition,
( spl0_29
<=> a = inverse(c) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f262,plain,
( a != inverse(c)
| spl0_29 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f263,plain,
( a = inverse(c)
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f267,plain,
( c = multiply(inverse(c),c)
| ~ spl0_21 ),
inference(superposition,[],[f83,f182]) ).
fof(f269,plain,
( identity = c
| ~ spl0_21 ),
inference(forward_demodulation,[],[f267,f3]) ).
fof(f271,plain,
( $false
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f269,f18]) ).
fof(f272,plain,
~ spl0_21,
inference(avatar_contradiction_clause,[],[f271]) ).
fof(f276,plain,
( identity != identity
| b = multiply(c,multiply(c,multiply(c,c)))
| c = multiply(c,multiply(c,multiply(c,c)))
| a = multiply(c,multiply(c,multiply(c,c)))
| spl0_1 ),
inference(superposition,[],[f30,f9]) ).
fof(f277,plain,
( b = multiply(c,multiply(c,multiply(c,c)))
| c = multiply(c,multiply(c,multiply(c,c)))
| a = multiply(c,multiply(c,multiply(c,c)))
| spl0_1 ),
inference(trivial_inequality_removal,[],[f276]) ).
fof(f282,plain,
( c != multiply(a,b)
| spl0_8
| ~ spl0_9 ),
inference(superposition,[],[f60,f63]) ).
fof(f284,plain,
( ! [X0] : multiply(b,X0) = multiply(a,multiply(a,X0))
| ~ spl0_9 ),
inference(superposition,[],[f4,f63]) ).
fof(f291,plain,
( c != multiply(b,a)
| spl0_8
| ~ spl0_9 ),
inference(superposition,[],[f60,f284]) ).
fof(f306,plain,
( ! [X0] : multiply(b,multiply(b,X0)) = multiply(c,X0)
| ~ spl0_6 ),
inference(superposition,[],[f4,f50]) ).
fof(f310,plain,
( multiply(b,identity) = multiply(c,inverse(b))
| ~ spl0_6 ),
inference(superposition,[],[f306,f7]) ).
fof(f315,plain,
( identity != multiply(c,multiply(b,b))
| spl0_4
| ~ spl0_6 ),
inference(superposition,[],[f43,f306]) ).
fof(f319,plain,
( identity != multiply(c,c)
| spl0_4
| ~ spl0_6 ),
inference(forward_demodulation,[],[f315,f50]) ).
fof(f323,plain,
( b = multiply(c,inverse(b))
| ~ spl0_6 ),
inference(forward_demodulation,[],[f310,f5]) ).
fof(f332,plain,
( ! [X0] : multiply(c,multiply(c,X0)) = multiply(a,X0)
| ~ spl0_3 ),
inference(superposition,[],[f4,f37]) ).
fof(f341,plain,
( b != multiply(a,c)
| spl0_2
| ~ spl0_3 ),
inference(superposition,[],[f34,f332]) ).
fof(f342,plain,
( identity != multiply(a,multiply(c,c))
| spl0_1
| ~ spl0_3 ),
inference(superposition,[],[f30,f332]) ).
fof(f346,plain,
( identity != multiply(a,a)
| spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f342,f37]) ).
fof(f409,plain,
( $false
| spl0_1
| ~ spl0_3
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f346,f76]) ).
fof(f410,plain,
( spl0_1
| ~ spl0_3
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f409]) ).
fof(f434,plain,
( ! [X0] : multiply(b,X0) = multiply(a,multiply(a,X0))
| ~ spl0_9 ),
inference(superposition,[],[f4,f63]) ).
fof(f437,plain,
( multiply(a,identity) = multiply(b,inverse(a))
| ~ spl0_9 ),
inference(superposition,[],[f434,f7]) ).
fof(f448,plain,
( a = multiply(b,inverse(a))
| ~ spl0_9 ),
inference(forward_demodulation,[],[f437,f5]) ).
fof(f476,plain,
! [X0,X1] : multiply(X1,inverse(multiply(X0,X1))) = multiply(inverse(X0),identity),
inference(superposition,[],[f83,f86]) ).
fof(f497,plain,
! [X0,X1] : inverse(X0) = multiply(X1,inverse(multiply(X0,X1))),
inference(forward_demodulation,[],[f476,f5]) ).
fof(f640,plain,
! [X0,X1] :
( multiply(X0,identity) = inverse(X1)
| multiply(X0,X1) = b
| multiply(X0,X1) = c
| multiply(X0,X1) = a ),
inference(superposition,[],[f172,f7]) ).
fof(f699,plain,
! [X0,X1] :
( multiply(X0,X1) = c
| multiply(X0,X1) = b
| inverse(X1) = X0
| multiply(X0,X1) = a ),
inference(forward_demodulation,[],[f640,f5]) ).
fof(f790,definition,
( spl0_30
<=> b = inverse(c) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f791,plain,
( b != inverse(c)
| spl0_30 ),
inference(avatar_component_clause,[],[f790]) ).
fof(f792,plain,
( b = inverse(c)
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f790]) ).
fof(f797,plain,
( b = multiply(c,multiply(c,b))
| c = multiply(c,multiply(c,multiply(c,c)))
| a = multiply(c,multiply(c,multiply(c,c)))
| spl0_1
| ~ spl0_22 ),
inference(forward_demodulation,[],[f277,f186]) ).
fof(f837,plain,
( inverse(c) = multiply(c,inverse(b))
| ~ spl0_22 ),
inference(superposition,[],[f497,f186]) ).
fof(f840,plain,
( ! [X0] : multiply(b,X0) = multiply(c,multiply(c,X0))
| ~ spl0_22 ),
inference(superposition,[],[f4,f186]) ).
fof(f842,plain,
( b = inverse(c)
| ~ spl0_6
| ~ spl0_22 ),
inference(forward_demodulation,[],[f837,f323]) ).
fof(f845,plain,
( spl0_30
| ~ spl0_6
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f842,f184,f49,f790]) ).
fof(f847,plain,
( a = multiply(b,multiply(b,a))
| ~ spl0_16
| ~ spl0_23 ),
inference(forward_demodulation,[],[f147,f191]) ).
fof(f851,plain,
( b = multiply(b,b)
| c = multiply(c,multiply(c,multiply(c,c)))
| a = multiply(c,multiply(c,multiply(c,c)))
| spl0_1
| ~ spl0_22 ),
inference(forward_demodulation,[],[f797,f840]) ).
fof(f882,plain,
( identity != multiply(b,multiply(b,a))
| spl0_4
| ~ spl0_23 ),
inference(superposition,[],[f43,f191]) ).
fof(f884,plain,
( inverse(b) = multiply(b,inverse(a))
| ~ spl0_23 ),
inference(superposition,[],[f497,f191]) ).
fof(f887,plain,
( ! [X0] : multiply(b,multiply(b,X0)) = multiply(a,X0)
| ~ spl0_23 ),
inference(superposition,[],[f4,f191]) ).
fof(f889,plain,
( a = inverse(b)
| ~ spl0_9
| ~ spl0_23 ),
inference(forward_demodulation,[],[f884,f448]) ).
fof(f890,plain,
( identity != multiply(a,a)
| spl0_4
| ~ spl0_23 ),
inference(forward_demodulation,[],[f882,f887]) ).
fof(f891,plain,
( spl0_27
| ~ spl0_9
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f889,f189,f62,f226]) ).
fof(f901,plain,
( a = multiply(inverse(a),a)
| ~ spl0_19 ),
inference(superposition,[],[f83,f163]) ).
fof(f904,plain,
( identity = a
| ~ spl0_19 ),
inference(forward_demodulation,[],[f901,f3]) ).
fof(f913,plain,
( $false
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f904,f13]) ).
fof(f914,plain,
~ spl0_19,
inference(avatar_contradiction_clause,[],[f913]) ).
fof(f918,plain,
( a = multiply(b,multiply(b,b))
| ~ spl0_4
| ~ spl0_27 ),
inference(forward_demodulation,[],[f209,f228]) ).
fof(f920,plain,
( c = multiply(b,multiply(c,c))
| b = multiply(b,b)
| a = multiply(c,multiply(c,multiply(c,c)))
| spl0_1
| ~ spl0_22 ),
inference(forward_demodulation,[],[f851,f840]) ).
fof(f924,plain,
( spl0_5
| ~ spl0_4
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f918,f226,f41,f45]) ).
fof(f925,plain,
( c = multiply(b,b)
| b = multiply(b,b)
| a = multiply(c,multiply(c,multiply(c,c)))
| spl0_1
| ~ spl0_22 ),
inference(forward_demodulation,[],[f920,f186]) ).
fof(f926,plain,
( b = multiply(b,b)
| a = multiply(c,multiply(c,multiply(c,c)))
| spl0_1
| spl0_6
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f925,f51]) ).
fof(f927,plain,
( a = multiply(b,multiply(c,c))
| b = multiply(b,b)
| spl0_1
| spl0_6
| ~ spl0_22 ),
inference(forward_demodulation,[],[f926,f840]) ).
fof(f928,plain,
( a = multiply(b,b)
| b = multiply(b,b)
| spl0_1
| spl0_6
| ~ spl0_22 ),
inference(forward_demodulation,[],[f927,f186]) ).
fof(f929,plain,
( b = multiply(b,b)
| spl0_1
| spl0_6
| ~ spl0_22
| spl0_23 ),
inference(forward_subsumption_resolution,[],[f928,f190]) ).
fof(f930,plain,
( spl0_24
| spl0_1
| spl0_6
| ~ spl0_22
| spl0_23 ),
inference(avatar_split_clause,[],[f929,f189,f184,f49,f28,f193]) ).
fof(f931,plain,
( identity = multiply(b,multiply(c,c))
| ~ spl0_1
| ~ spl0_22 ),
inference(forward_demodulation,[],[f29,f840]) ).
fof(f932,plain,
( spl0_28
| spl0_29
| ~ spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f255,f32,f28,f261,f257]) ).
fof(f935,plain,
( identity = multiply(b,b)
| ~ spl0_1
| ~ spl0_22 ),
inference(forward_demodulation,[],[f931,f186]) ).
fof(f938,plain,
( $false
| ~ spl0_1
| spl0_11
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f935,f73]) ).
fof(f939,plain,
( ~ spl0_1
| spl0_11
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f938]) ).
fof(f940,plain,
( a = multiply(b,identity)
| b = multiply(b,b)
| c = multiply(b,b)
| a = multiply(b,b)
| ~ spl0_5 ),
inference(superposition,[],[f46,f9]) ).
fof(f956,plain,
( a = multiply(b,identity)
| c = multiply(b,b)
| a = multiply(b,b)
| ~ spl0_5
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f940,f194]) ).
fof(f962,plain,
( a = multiply(b,identity)
| a = multiply(b,b)
| ~ spl0_5
| spl0_6
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f956,f51]) ).
fof(f967,plain,
( a = multiply(b,identity)
| ~ spl0_5
| spl0_6
| spl0_23
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f962,f190]) ).
fof(f974,plain,
( a = b
| ~ spl0_5
| spl0_6
| spl0_23
| spl0_24 ),
inference(forward_demodulation,[],[f967,f5]) ).
fof(f975,plain,
( $false
| ~ spl0_5
| spl0_6
| spl0_23
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f974,f10]) ).
fof(f976,plain,
( ~ spl0_5
| spl0_6
| spl0_23
| spl0_24 ),
inference(avatar_contradiction_clause,[],[f975]) ).
fof(f988,plain,
( b = multiply(inverse(b),b)
| ~ spl0_24 ),
inference(superposition,[],[f83,f195]) ).
fof(f991,plain,
( identity = b
| ~ spl0_24 ),
inference(forward_demodulation,[],[f988,f3]) ).
fof(f994,plain,
( $false
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f991,f16]) ).
fof(f995,plain,
~ spl0_24,
inference(avatar_contradiction_clause,[],[f994]) ).
fof(f1000,plain,
( ~ spl0_10
| spl0_4
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f319,f49,f41,f67]) ).
fof(f1004,plain,
( identity != identity
| b = multiply(c,c)
| c = multiply(c,c)
| a = multiply(c,c)
| spl0_10 ),
inference(superposition,[],[f69,f9]) ).
fof(f1005,plain,
( b = multiply(c,c)
| c = multiply(c,c)
| a = multiply(c,c)
| spl0_10 ),
inference(trivial_inequality_removal,[],[f1004]) ).
fof(f1006,plain,
( c = multiply(c,c)
| a = multiply(c,c)
| spl0_10
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f1005,f185]) ).
fof(f1007,plain,
( a = multiply(c,c)
| spl0_10
| spl0_21
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f1006,f181]) ).
fof(f1008,plain,
( $false
| spl0_3
| spl0_10
| spl0_21
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f1007,f38]) ).
fof(f1009,plain,
( spl0_3
| spl0_10
| spl0_21
| spl0_22 ),
inference(avatar_contradiction_clause,[],[f1008]) ).
fof(f1021,plain,
( multiply(c,multiply(c,c)) = multiply(inverse(c),identity)
| ~ spl0_1 ),
inference(superposition,[],[f83,f29]) ).
fof(f1024,plain,
( multiply(c,multiply(c,c)) = inverse(c)
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1021,f5]) ).
fof(f1040,plain,
( inverse(b) = multiply(b,inverse(c))
| ~ spl0_6 ),
inference(superposition,[],[f497,f50]) ).
fof(f1042,plain,
( b = multiply(inverse(b),c)
| ~ spl0_6 ),
inference(superposition,[],[f83,f50]) ).
fof(f1043,plain,
( ! [X0] : multiply(b,multiply(b,X0)) = multiply(c,X0)
| ~ spl0_6 ),
inference(superposition,[],[f4,f50]) ).
fof(f1044,plain,
( b = multiply(a,c)
| ~ spl0_6
| ~ spl0_27 ),
inference(forward_demodulation,[],[f1042,f228]) ).
fof(f1047,plain,
( $false
| spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f1044,f341]) ).
fof(f1048,plain,
( spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_27 ),
inference(avatar_contradiction_clause,[],[f1047]) ).
fof(f1053,plain,
( b = multiply(c,a)
| ~ spl0_2
| ~ spl0_3 ),
inference(forward_demodulation,[],[f33,f37]) ).
fof(f1070,plain,
( ! [X0] : inverse(b) = multiply(multiply(b,X0),inverse(multiply(c,X0)))
| ~ spl0_6 ),
inference(superposition,[],[f497,f1043]) ).
fof(f1077,plain,
( ! [X0] : inverse(b) = multiply(b,multiply(X0,inverse(multiply(c,X0))))
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1070,f4]) ).
fof(f1089,plain,
( inverse(b) = multiply(b,inverse(c))
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1077,f497]) ).
fof(f1113,plain,
( multiply(b,b) = inverse(b)
| ~ spl0_6
| ~ spl0_30 ),
inference(forward_demodulation,[],[f1089,f792]) ).
fof(f1116,plain,
( a = multiply(b,b)
| ~ spl0_6
| ~ spl0_27
| ~ spl0_30 ),
inference(forward_demodulation,[],[f1113,f228]) ).
fof(f1119,plain,
( $false
| ~ spl0_6
| spl0_23
| ~ spl0_27
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f1116,f190]) ).
fof(f1120,plain,
( ~ spl0_6
| spl0_23
| ~ spl0_27
| ~ spl0_30 ),
inference(avatar_contradiction_clause,[],[f1119]) ).
fof(f1132,plain,
( c = multiply(inverse(c),a)
| ~ spl0_3 ),
inference(superposition,[],[f83,f37]) ).
fof(f1133,plain,
( ! [X0] : multiply(c,multiply(c,X0)) = multiply(a,X0)
| ~ spl0_3 ),
inference(superposition,[],[f4,f37]) ).
fof(f1134,plain,
( c = multiply(a,a)
| ~ spl0_3
| ~ spl0_29 ),
inference(forward_demodulation,[],[f1132,f263]) ).
fof(f1137,plain,
( b = c
| ~ spl0_3
| ~ spl0_9
| ~ spl0_29 ),
inference(forward_demodulation,[],[f1134,f63]) ).
fof(f1138,plain,
( $false
| ~ spl0_3
| ~ spl0_9
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f1137,f14]) ).
fof(f1139,plain,
( ~ spl0_3
| ~ spl0_9
| ~ spl0_29 ),
inference(avatar_contradiction_clause,[],[f1138]) ).
fof(f1165,plain,
( ! [X0] : multiply(c,identity) = multiply(a,multiply(X0,inverse(multiply(c,X0))))
| ~ spl0_3 ),
inference(superposition,[],[f1133,f86]) ).
fof(f1188,plain,
( multiply(c,identity) = multiply(a,inverse(c))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1165,f497]) ).
fof(f1197,plain,
( multiply(a,a) = multiply(c,identity)
| ~ spl0_3
| ~ spl0_29 ),
inference(forward_demodulation,[],[f1188,f263]) ).
fof(f1201,plain,
( c = multiply(a,a)
| ~ spl0_3
| ~ spl0_29 ),
inference(forward_demodulation,[],[f1197,f5]) ).
fof(f1206,plain,
( inverse(a) = multiply(a,inverse(c))
| ~ spl0_20 ),
inference(superposition,[],[f497,f167]) ).
fof(f1209,plain,
( ! [X0] : multiply(c,X0) = multiply(a,multiply(a,X0))
| ~ spl0_20 ),
inference(superposition,[],[f4,f167]) ).
fof(f1211,plain,
( multiply(a,a) = inverse(a)
| ~ spl0_20
| ~ spl0_29 ),
inference(forward_demodulation,[],[f1206,f263]) ).
fof(f1213,plain,
( c = inverse(a)
| ~ spl0_20
| ~ spl0_29 ),
inference(forward_demodulation,[],[f1211,f167]) ).
fof(f1218,plain,
( identity = multiply(c,a)
| ~ spl0_29 ),
inference(superposition,[],[f7,f263]) ).
fof(f1221,plain,
( identity = b
| ~ spl0_2
| ~ spl0_3
| ~ spl0_29 ),
inference(forward_demodulation,[],[f1218,f1053]) ).
fof(f1224,plain,
( $false
| ~ spl0_2
| ~ spl0_3
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f1221,f16]) ).
fof(f1225,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_29 ),
inference(avatar_contradiction_clause,[],[f1224]) ).
fof(f1231,plain,
( multiply(b,b) = inverse(b)
| ~ spl0_6
| ~ spl0_30 ),
inference(forward_demodulation,[],[f1040,f792]) ).
fof(f1300,plain,
( c = inverse(b)
| ~ spl0_6
| ~ spl0_30 ),
inference(forward_demodulation,[],[f1231,f50]) ).
fof(f1308,plain,
( spl0_26
| ~ spl0_6
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f1300,f790,f49,f222]) ).
fof(f1315,plain,
( a = c
| ~ spl0_6
| ~ spl0_23 ),
inference(superposition,[],[f191,f50]) ).
fof(f1330,plain,
( $false
| ~ spl0_6
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1315,f11]) ).
fof(f1331,plain,
( ~ spl0_6
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f1330]) ).
fof(f1336,plain,
( inverse(c) = multiply(c,inverse(a))
| ~ spl0_3 ),
inference(superposition,[],[f497,f37]) ).
fof(f1339,plain,
( ! [X0] : multiply(c,multiply(c,X0)) = multiply(a,X0)
| ~ spl0_3 ),
inference(superposition,[],[f4,f37]) ).
fof(f1342,plain,
( b = multiply(c,inverse(a))
| ~ spl0_3
| ~ spl0_30 ),
inference(forward_demodulation,[],[f1336,f792]) ).
fof(f1343,plain,
( multiply(c,a) = multiply(a,c)
| ~ spl0_3 ),
inference(superposition,[],[f1339,f37]) ).
fof(f1348,plain,
( ! [X0] : multiply(c,identity) = multiply(a,multiply(X0,inverse(multiply(c,X0))))
| ~ spl0_3 ),
inference(superposition,[],[f1339,f86]) ).
fof(f1371,plain,
( multiply(c,identity) = multiply(a,inverse(c))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1348,f497]) ).
fof(f1374,plain,
( b = multiply(a,c)
| ~ spl0_2
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1343,f1053]) ).
fof(f1379,plain,
( multiply(c,identity) = multiply(a,b)
| ~ spl0_3
| ~ spl0_30 ),
inference(forward_demodulation,[],[f1371,f792]) ).
fof(f1427,plain,
( ! [X0] : multiply(a,identity) = multiply(c,multiply(X0,inverse(multiply(a,X0))))
| ~ spl0_20 ),
inference(superposition,[],[f1209,f86]) ).
fof(f1434,plain,
( c != multiply(c,a)
| spl0_8
| ~ spl0_20 ),
inference(superposition,[],[f60,f1209]) ).
fof(f1452,plain,
( multiply(a,identity) = multiply(c,inverse(a))
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1427,f497]) ).
fof(f1459,plain,
( b = multiply(a,identity)
| ~ spl0_3
| ~ spl0_20
| ~ spl0_30 ),
inference(forward_demodulation,[],[f1452,f1342]) ).
fof(f1463,plain,
( a = b
| ~ spl0_3
| ~ spl0_20
| ~ spl0_30 ),
inference(forward_demodulation,[],[f1459,f5]) ).
fof(f1466,plain,
( $false
| ~ spl0_3
| ~ spl0_20
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f1463,f10]) ).
fof(f1467,plain,
( ~ spl0_3
| ~ spl0_20
| ~ spl0_30 ),
inference(avatar_contradiction_clause,[],[f1466]) ).
fof(f1482,plain,
( c = multiply(a,b)
| ~ spl0_3
| ~ spl0_30 ),
inference(forward_demodulation,[],[f1379,f5]) ).
fof(f1489,plain,
( $false
| ~ spl0_3
| spl0_8
| ~ spl0_9
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f1482,f282]) ).
fof(f1490,plain,
( ~ spl0_3
| spl0_8
| ~ spl0_9
| ~ spl0_30 ),
inference(avatar_contradiction_clause,[],[f1489]) ).
fof(f1492,plain,
( identity != multiply(a,multiply(a,b))
| spl0_7
| ~ spl0_9 ),
inference(forward_demodulation,[],[f56,f63]) ).
fof(f1499,definition,
( spl0_31
<=> a = multiply(a,c) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f1500,plain,
( a != multiply(a,c)
| spl0_31 ),
inference(avatar_component_clause,[],[f1499]) ).
fof(f1501,plain,
( a = multiply(a,c)
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f1499]) ).
fof(f1503,definition,
( spl0_32
<=> c = multiply(a,c) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f1504,plain,
( c != multiply(a,c)
| spl0_32 ),
inference(avatar_component_clause,[],[f1503]) ).
fof(f1505,plain,
( c = multiply(a,c)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f1503]) ).
fof(f1511,plain,
( inverse(a) = multiply(c,inverse(c))
| ~ spl0_32 ),
inference(superposition,[],[f497,f1505]) ).
fof(f1516,plain,
( identity = inverse(a)
| ~ spl0_32 ),
inference(forward_demodulation,[],[f1511,f7]) ).
fof(f1520,plain,
( identity = multiply(a,identity)
| ~ spl0_32 ),
inference(superposition,[],[f7,f1516]) ).
fof(f1523,plain,
( identity = a
| ~ spl0_32 ),
inference(forward_demodulation,[],[f1520,f5]) ).
fof(f1529,plain,
( $false
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f1523,f13]) ).
fof(f1530,plain,
~ spl0_32,
inference(avatar_contradiction_clause,[],[f1529]) ).
fof(f1539,plain,
( c = multiply(inverse(a),a)
| ~ spl0_31 ),
inference(superposition,[],[f83,f1501]) ).
fof(f1542,plain,
( identity = c
| ~ spl0_31 ),
inference(forward_demodulation,[],[f1539,f3]) ).
fof(f1545,plain,
( $false
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f1542,f18]) ).
fof(f1546,plain,
~ spl0_31,
inference(avatar_contradiction_clause,[],[f1545]) ).
fof(f1613,plain,
( spl0_20
| ~ spl0_3
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f1201,f261,f36,f165]) ).
fof(f1656,plain,
( a = multiply(c,multiply(c,c))
| ~ spl0_1
| ~ spl0_29 ),
inference(forward_demodulation,[],[f1024,f263]) ).
fof(f1668,plain,
( a = multiply(a,c)
| ~ spl0_1
| ~ spl0_3
| ~ spl0_29 ),
inference(forward_demodulation,[],[f1656,f1339]) ).
fof(f1673,plain,
( $false
| ~ spl0_1
| ~ spl0_3
| ~ spl0_29
| spl0_31 ),
inference(forward_subsumption_resolution,[],[f1668,f1500]) ).
fof(f1674,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_29
| spl0_31 ),
inference(avatar_contradiction_clause,[],[f1673]) ).
fof(f1685,plain,
( multiply(c,identity) = multiply(a,c)
| ~ spl0_3
| ~ spl0_28 ),
inference(forward_demodulation,[],[f1371,f259]) ).
fof(f1689,plain,
( c = multiply(c,multiply(c,c))
| ~ spl0_1
| ~ spl0_28 ),
inference(forward_demodulation,[],[f1024,f259]) ).
fof(f1695,plain,
( c = multiply(a,c)
| ~ spl0_3
| ~ spl0_28 ),
inference(forward_demodulation,[],[f1685,f5]) ).
fof(f1698,plain,
( c = multiply(a,c)
| ~ spl0_1
| ~ spl0_3
| ~ spl0_28 ),
inference(forward_demodulation,[],[f1689,f1339]) ).
fof(f1701,plain,
( $false
| ~ spl0_3
| ~ spl0_28
| spl0_32 ),
inference(forward_subsumption_resolution,[],[f1695,f1504]) ).
fof(f1702,plain,
( ~ spl0_3
| ~ spl0_28
| spl0_32 ),
inference(avatar_contradiction_clause,[],[f1701]) ).
fof(f1707,plain,
( $false
| ~ spl0_1
| ~ spl0_3
| ~ spl0_28
| spl0_32 ),
inference(forward_subsumption_resolution,[],[f1698,f1504]) ).
fof(f1708,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_28
| spl0_32 ),
inference(avatar_contradiction_clause,[],[f1707]) ).
fof(f1717,plain,
( inverse(b) = multiply(b,a)
| ~ spl0_6
| ~ spl0_29 ),
inference(forward_demodulation,[],[f1040,f263]) ).
fof(f1730,plain,
( identity = multiply(a,multiply(a,c))
| ~ spl0_7
| ~ spl0_20 ),
inference(forward_demodulation,[],[f55,f167]) ).
fof(f1769,plain,
( identity = multiply(a,c)
| ~ spl0_29 ),
inference(superposition,[],[f3,f263]) ).
fof(f1790,plain,
( c = multiply(inverse(a),identity)
| ~ spl0_29 ),
inference(superposition,[],[f83,f1769]) ).
fof(f1793,plain,
( c = inverse(a)
| ~ spl0_29 ),
inference(forward_demodulation,[],[f1790,f5]) ).
fof(f1893,plain,
( ! [X0] : multiply(b,X0) = multiply(inverse(c),X0)
| ~ spl0_26 ),
inference(superposition,[],[f95,f224]) ).
fof(f1898,plain,
( ! [X0] : multiply(b,X0) = multiply(a,X0)
| ~ spl0_26
| ~ spl0_29 ),
inference(forward_demodulation,[],[f1893,f263]) ).
fof(f1903,plain,
( b = multiply(a,identity)
| ~ spl0_26
| ~ spl0_29 ),
inference(superposition,[],[f1898,f5]) ).
fof(f1941,plain,
( a = b
| ~ spl0_26
| ~ spl0_29 ),
inference(forward_demodulation,[],[f1903,f5]) ).
fof(f1952,plain,
( $false
| ~ spl0_26
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f1941,f10]) ).
fof(f1953,plain,
( ~ spl0_26
| ~ spl0_29 ),
inference(avatar_contradiction_clause,[],[f1952]) ).
fof(f1957,plain,
( identity = inverse(b)
| b = multiply(b,a)
| c = multiply(b,a)
| a = multiply(b,a)
| ~ spl0_6
| ~ spl0_29 ),
inference(superposition,[],[f1717,f9]) ).
fof(f1968,plain,
( b = inverse(b)
| identity = inverse(b)
| c = multiply(b,a)
| a = multiply(b,a)
| ~ spl0_6
| ~ spl0_29 ),
inference(forward_demodulation,[],[f1957,f1717]) ).
fof(f1971,plain,
( c = inverse(b)
| b = inverse(b)
| identity = inverse(b)
| a = multiply(b,a)
| ~ spl0_6
| ~ spl0_29 ),
inference(forward_demodulation,[],[f1968,f1717]) ).
fof(f1972,plain,
( b = inverse(b)
| identity = inverse(b)
| a = multiply(b,a)
| ~ spl0_6
| spl0_26
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f1971,f223]) ).
fof(f1973,plain,
( a = inverse(b)
| b = inverse(b)
| identity = inverse(b)
| ~ spl0_6
| spl0_26
| ~ spl0_29 ),
inference(forward_demodulation,[],[f1972,f1717]) ).
fof(f1974,plain,
( b = inverse(b)
| identity = inverse(b)
| ~ spl0_6
| spl0_26
| spl0_27
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f1973,f227]) ).
fof(f1976,definition,
( spl0_33
<=> identity = inverse(b) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f1978,plain,
( identity = inverse(b)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f1976]) ).
fof(f1979,plain,
( spl0_33
| spl0_25
| ~ spl0_6
| spl0_26
| spl0_27
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f1974,f261,f226,f222,f49,f218,f1976]) ).
fof(f2000,plain,
( identity = multiply(b,identity)
| ~ spl0_33 ),
inference(superposition,[],[f7,f1978]) ).
fof(f2003,plain,
( identity = b
| ~ spl0_33 ),
inference(forward_demodulation,[],[f2000,f5]) ).
fof(f2009,plain,
( $false
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f2003,f16]) ).
fof(f2010,plain,
~ spl0_33,
inference(avatar_contradiction_clause,[],[f2009]) ).
fof(f2021,plain,
( ! [X0] : multiply(b,multiply(b,X0)) = X0
| ~ spl0_25 ),
inference(superposition,[],[f83,f220]) ).
fof(f2022,plain,
( identity = multiply(b,b)
| ~ spl0_25 ),
inference(superposition,[],[f7,f220]) ).
fof(f2025,plain,
( identity = c
| ~ spl0_6
| ~ spl0_25 ),
inference(forward_demodulation,[],[f2022,f50]) ).
fof(f2028,plain,
( $false
| ~ spl0_6
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f2025,f18]) ).
fof(f2029,plain,
( ~ spl0_6
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f2028]) ).
fof(f2031,plain,
( identity = multiply(b,b)
| ~ spl0_4
| ~ spl0_25 ),
inference(forward_demodulation,[],[f42,f2021]) ).
fof(f2045,plain,
( identity != multiply(a,c)
| spl0_7
| ~ spl0_8 ),
inference(forward_demodulation,[],[f56,f59]) ).
fof(f2064,plain,
( $false
| spl0_11
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f2022,f73]) ).
fof(f2065,plain,
( spl0_11
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f2064]) ).
fof(f2087,plain,
( ! [X0] : multiply(c,X0) = multiply(a,multiply(multiply(a,a),X0))
| ~ spl0_8 ),
inference(superposition,[],[f4,f59]) ).
fof(f2088,plain,
( ! [X0] : multiply(c,X0) = multiply(a,multiply(a,multiply(a,X0)))
| ~ spl0_8 ),
inference(forward_demodulation,[],[f2087,f4]) ).
fof(f2106,plain,
( multiply(c,a) = multiply(a,c)
| ~ spl0_8 ),
inference(superposition,[],[f2088,f59]) ).
fof(f2108,plain,
( multiply(a,identity) = multiply(c,inverse(multiply(a,a)))
| ~ spl0_8 ),
inference(superposition,[],[f2088,f86]) ).
fof(f2125,plain,
( multiply(a,identity) = multiply(c,inverse(b))
| ~ spl0_8
| ~ spl0_9 ),
inference(forward_demodulation,[],[f2108,f63]) ).
fof(f2152,plain,
( identity != multiply(b,multiply(b,identity))
| spl0_4
| ~ spl0_11 ),
inference(forward_demodulation,[],[f43,f72]) ).
fof(f2159,plain,
( multiply(a,identity) = multiply(c,a)
| ~ spl0_8
| ~ spl0_9
| ~ spl0_27 ),
inference(forward_demodulation,[],[f2125,f228]) ).
fof(f2160,plain,
( identity != multiply(b,b)
| spl0_4
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2152,f5]) ).
fof(f2165,plain,
( multiply(a,identity) = multiply(a,c)
| ~ spl0_3
| ~ spl0_8
| ~ spl0_9
| ~ spl0_27 ),
inference(forward_demodulation,[],[f2159,f1343]) ).
fof(f2166,plain,
( $false
| spl0_4
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f2160,f72]) ).
fof(f2167,plain,
( spl0_4
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f2166]) ).
fof(f2172,plain,
( b = multiply(a,identity)
| ~ spl0_2
| ~ spl0_3
| ~ spl0_8
| ~ spl0_9
| ~ spl0_27 ),
inference(forward_demodulation,[],[f2165,f1374]) ).
fof(f2173,plain,
( a = b
| ~ spl0_2
| ~ spl0_3
| ~ spl0_8
| ~ spl0_9
| ~ spl0_27 ),
inference(forward_demodulation,[],[f2172,f5]) ).
fof(f2174,plain,
( $false
| ~ spl0_2
| ~ spl0_3
| ~ spl0_8
| ~ spl0_9
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f2173,f10]) ).
fof(f2175,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_8
| ~ spl0_9
| ~ spl0_27 ),
inference(avatar_contradiction_clause,[],[f2174]) ).
fof(f2193,plain,
( b = multiply(b,multiply(b,a))
| ~ spl0_18
| ~ spl0_23 ),
inference(forward_demodulation,[],[f155,f191]) ).
fof(f2253,plain,
( inverse(b) = multiply(b,inverse(a))
| ~ spl0_23 ),
inference(superposition,[],[f497,f191]) ).
fof(f2255,plain,
( b = multiply(inverse(b),a)
| ~ spl0_23 ),
inference(superposition,[],[f83,f191]) ).
fof(f2256,plain,
( ! [X0] : multiply(b,multiply(b,X0)) = multiply(a,X0)
| ~ spl0_23 ),
inference(superposition,[],[f4,f191]) ).
fof(f2257,plain,
( b = multiply(a,a)
| ~ spl0_23
| ~ spl0_27 ),
inference(forward_demodulation,[],[f2255,f228]) ).
fof(f2259,plain,
( inverse(b) = multiply(b,c)
| ~ spl0_20
| ~ spl0_23
| ~ spl0_29 ),
inference(forward_demodulation,[],[f2253,f1213]) ).
fof(f2260,plain,
( $false
| spl0_9
| ~ spl0_23
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f2257,f64]) ).
fof(f2261,plain,
( spl0_9
| ~ spl0_23
| ~ spl0_27 ),
inference(avatar_contradiction_clause,[],[f2260]) ).
fof(f2277,plain,
( ! [X0] : multiply(c,X0) = multiply(a,multiply(a,X0))
| ~ spl0_20 ),
inference(superposition,[],[f4,f167]) ).
fof(f2285,plain,
( ! [X0] : multiply(c,multiply(a,X0)) = X0
| ~ spl0_29 ),
inference(superposition,[],[f87,f263]) ).
fof(f2288,plain,
( identity = multiply(a,c)
| ~ spl0_29 ),
inference(superposition,[],[f3,f263]) ).
fof(f2322,plain,
( ! [X0] : inverse(multiply(X0,a)) = multiply(c,inverse(X0))
| ~ spl0_29 ),
inference(superposition,[],[f2285,f497]) ).
fof(f2398,plain,
( ! [X0] : multiply(b,multiply(a,X0)) = multiply(a,multiply(b,X0))
| ~ spl0_23 ),
inference(superposition,[],[f2256,f2256]) ).
fof(f2479,plain,
( inverse(b) = multiply(multiply(b,a),inverse(b))
| ~ spl0_18
| ~ spl0_23 ),
inference(superposition,[],[f497,f2193]) ).
fof(f2481,plain,
( multiply(b,a) = multiply(inverse(b),b)
| ~ spl0_18
| ~ spl0_23 ),
inference(superposition,[],[f83,f2193]) ).
fof(f2482,plain,
( ! [X0] : multiply(b,X0) = multiply(b,multiply(multiply(b,a),X0))
| ~ spl0_18
| ~ spl0_23 ),
inference(superposition,[],[f4,f2193]) ).
fof(f2483,plain,
( ! [X0] : multiply(b,X0) = multiply(b,multiply(b,multiply(a,X0)))
| ~ spl0_18
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2482,f4]) ).
fof(f2484,plain,
( identity = multiply(b,a)
| ~ spl0_18
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2481,f3]) ).
fof(f2486,plain,
( inverse(b) = multiply(b,multiply(a,inverse(b)))
| ~ spl0_18
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2479,f4]) ).
fof(f2493,plain,
( ! [X0] : multiply(b,X0) = multiply(a,multiply(a,X0))
| ~ spl0_18
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2483,f2256]) ).
fof(f2495,plain,
( inverse(b) = multiply(a,multiply(b,inverse(b)))
| ~ spl0_18
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2486,f2398]) ).
fof(f2498,plain,
( multiply(a,identity) = inverse(b)
| ~ spl0_18
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2495,f7]) ).
fof(f2500,plain,
( a = inverse(b)
| ~ spl0_18
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2498,f5]) ).
fof(f2506,plain,
( c = multiply(a,multiply(b,b))
| ~ spl0_17
| ~ spl0_23 ),
inference(forward_demodulation,[],[f151,f2256]) ).
fof(f2510,plain,
( c = multiply(a,a)
| ~ spl0_17
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2506,f191]) ).
fof(f2528,plain,
( c = inverse(b)
| b = inverse(b)
| b = inverse(c)
| a = inverse(b)
| ~ spl0_20
| ~ spl0_23
| ~ spl0_29 ),
inference(superposition,[],[f699,f2259]) ).
fof(f2556,plain,
( c != c
| b = multiply(a,c)
| a = inverse(c)
| a = multiply(a,c)
| spl0_32 ),
inference(superposition,[],[f1504,f699]) ).
fof(f2573,plain,
( c != c
| b = multiply(c,c)
| c = inverse(c)
| a = multiply(c,c)
| spl0_21 ),
inference(superposition,[],[f181,f699]) ).
fof(f2578,plain,
( b = multiply(c,c)
| c = inverse(c)
| a = multiply(c,c)
| spl0_21 ),
inference(trivial_inequality_removal,[],[f2573]) ).
fof(f2581,plain,
( b = multiply(a,c)
| a = inverse(c)
| a = multiply(a,c)
| spl0_32 ),
inference(trivial_inequality_removal,[],[f2556]) ).
fof(f2604,plain,
( b = inverse(b)
| b = inverse(c)
| a = inverse(b)
| ~ spl0_20
| ~ spl0_23
| spl0_26
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f2528,f223]) ).
fof(f2624,plain,
( b = inverse(c)
| a = inverse(b)
| ~ spl0_20
| ~ spl0_23
| spl0_25
| spl0_26
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f2604,f219]) ).
fof(f2634,plain,
( b = inverse(c)
| ~ spl0_20
| ~ spl0_23
| spl0_25
| spl0_26
| spl0_27
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f2624,f227]) ).
fof(f2638,plain,
( a = b
| ~ spl0_20
| ~ spl0_23
| spl0_25
| spl0_26
| spl0_27
| ~ spl0_29 ),
inference(forward_demodulation,[],[f2634,f263]) ).
fof(f2641,plain,
( $false
| ~ spl0_20
| ~ spl0_23
| spl0_25
| spl0_26
| spl0_27
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f2638,f10]) ).
fof(f2642,plain,
( ~ spl0_20
| ~ spl0_23
| spl0_25
| spl0_26
| spl0_27
| ~ spl0_29 ),
inference(avatar_contradiction_clause,[],[f2641]) ).
fof(f2646,plain,
( identity = multiply(a,multiply(b,b))
| ~ spl0_4
| ~ spl0_23 ),
inference(forward_demodulation,[],[f42,f2256]) ).
fof(f2649,plain,
( identity = a
| ~ spl0_11
| ~ spl0_23 ),
inference(forward_demodulation,[],[f72,f191]) ).
fof(f2651,plain,
( a = multiply(a,a)
| ~ spl0_16
| ~ spl0_23 ),
inference(forward_demodulation,[],[f847,f2256]) ).
fof(f2654,plain,
( identity = multiply(a,a)
| ~ spl0_4
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2646,f191]) ).
fof(f2658,plain,
( $false
| ~ spl0_11
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f2649,f13]) ).
fof(f2659,plain,
( ~ spl0_11
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f2658]) ).
fof(f2661,plain,
( spl0_19
| ~ spl0_16
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f2651,f189,f145,f161]) ).
fof(f2664,plain,
( identity = c
| ~ spl0_4
| ~ spl0_20
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2654,f167]) ).
fof(f2665,plain,
( $false
| ~ spl0_4
| ~ spl0_20
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f2664,f18]) ).
fof(f2666,plain,
( ~ spl0_4
| ~ spl0_20
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f2665]) ).
fof(f2672,plain,
( spl0_11
| ~ spl0_4
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f2031,f218,f41,f71]) ).
fof(f2700,plain,
( ! [X0] : multiply(identity,X0) = multiply(b,multiply(b,X0))
| ~ spl0_11 ),
inference(superposition,[],[f4,f72]) ).
fof(f2701,plain,
( ! [X0] : multiply(b,multiply(b,X0)) = X0
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2700,f1]) ).
fof(f2716,plain,
( ! [X0] :
( multiply(b,identity) = X0
| b = multiply(b,X0)
| c = multiply(b,X0)
| a = multiply(b,X0) )
| ~ spl0_11 ),
inference(superposition,[],[f2701,f9]) ).
fof(f2735,plain,
( ! [X0] :
( c = multiply(b,X0)
| b = multiply(b,X0)
| b = X0
| a = multiply(b,X0) )
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2716,f5]) ).
fof(f2775,plain,
( inverse(c) = multiply(c,inverse(a))
| ~ spl0_20
| ~ spl0_29 ),
inference(superposition,[],[f2322,f167]) ).
fof(f2795,plain,
( multiply(c,c) = inverse(c)
| ~ spl0_20
| ~ spl0_29 ),
inference(forward_demodulation,[],[f2775,f1213]) ).
fof(f2806,plain,
( a = multiply(c,c)
| ~ spl0_20
| ~ spl0_29 ),
inference(forward_demodulation,[],[f2795,f263]) ).
fof(f3054,plain,
( c != c
| b = multiply(b,b)
| b = inverse(b)
| a = multiply(b,b)
| spl0_6 ),
inference(superposition,[],[f51,f173]) ).
fof(f3066,plain,
( b = multiply(b,b)
| b = inverse(b)
| a = multiply(b,b)
| spl0_6 ),
inference(trivial_inequality_removal,[],[f3054]) ).
fof(f3281,plain,
( identity = c
| b = multiply(b,inverse(b))
| b = inverse(b)
| a = multiply(b,inverse(b))
| ~ spl0_11 ),
inference(superposition,[],[f7,f2735]) ).
fof(f3285,plain,
( inverse(c) = multiply(c,inverse(b))
| b = multiply(b,a)
| a = b
| a = multiply(b,a)
| ~ spl0_11
| ~ spl0_29 ),
inference(superposition,[],[f2322,f2735]) ).
fof(f3290,plain,
( inverse(c) = multiply(c,inverse(b))
| b = multiply(b,a)
| a = multiply(b,a)
| ~ spl0_11
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f3285,f10]) ).
fof(f3304,plain,
( inverse(c) = multiply(c,b)
| b = multiply(b,a)
| a = multiply(b,a)
| ~ spl0_11
| ~ spl0_25
| ~ spl0_29 ),
inference(forward_demodulation,[],[f3290,f220]) ).
fof(f3314,plain,
( a = multiply(c,b)
| b = multiply(b,a)
| a = multiply(b,a)
| ~ spl0_11
| ~ spl0_25
| ~ spl0_29 ),
inference(forward_demodulation,[],[f3304,f263]) ).
fof(f3329,definition,
( spl0_36
<=> a = multiply(a,b) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f3331,plain,
( a = multiply(a,b)
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f3329]) ).
fof(f3334,definition,
( spl0_37
<=> a = multiply(b,a) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f3335,plain,
( a != multiply(b,a)
| spl0_37 ),
inference(avatar_component_clause,[],[f3334]) ).
fof(f3336,plain,
( a = multiply(b,a)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f3334]) ).
fof(f3338,definition,
( spl0_38
<=> b = multiply(b,a) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f3339,plain,
( b != multiply(b,a)
| spl0_38 ),
inference(avatar_component_clause,[],[f3338]) ).
fof(f3340,plain,
( b = multiply(b,a)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f3338]) ).
fof(f3342,definition,
( spl0_39
<=> a = multiply(c,b) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f3344,plain,
( a = multiply(c,b)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f3342]) ).
fof(f3345,plain,
( spl0_37
| spl0_38
| spl0_39
| ~ spl0_11
| ~ spl0_25
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f3314,f261,f218,f71,f3342,f3338,f3334]) ).
fof(f3377,plain,
( a = multiply(inverse(b),b)
| ~ spl0_38 ),
inference(superposition,[],[f83,f3340]) ).
fof(f3384,plain,
( identity = a
| ~ spl0_38 ),
inference(forward_demodulation,[],[f3377,f3]) ).
fof(f3390,plain,
( $false
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f3384,f13]) ).
fof(f3391,plain,
~ spl0_38,
inference(avatar_contradiction_clause,[],[f3390]) ).
fof(f3403,plain,
( identity = multiply(b,multiply(a,inverse(a)))
| ~ spl0_37 ),
inference(superposition,[],[f86,f3336]) ).
fof(f3407,plain,
( identity = multiply(b,identity)
| ~ spl0_37 ),
inference(forward_demodulation,[],[f3403,f7]) ).
fof(f3412,plain,
( identity = b
| ~ spl0_37 ),
inference(forward_demodulation,[],[f3407,f5]) ).
fof(f3414,plain,
( $false
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f3412,f16]) ).
fof(f3415,plain,
~ spl0_37,
inference(avatar_contradiction_clause,[],[f3414]) ).
fof(f3423,plain,
( b = multiply(inverse(c),a)
| ~ spl0_39 ),
inference(superposition,[],[f83,f3344]) ).
fof(f3429,plain,
( b = multiply(a,a)
| ~ spl0_29
| ~ spl0_39 ),
inference(forward_demodulation,[],[f3423,f263]) ).
fof(f3436,plain,
( $false
| spl0_9
| ~ spl0_29
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f3429,f64]) ).
fof(f3437,plain,
( spl0_9
| ~ spl0_29
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f3436]) ).
fof(f3462,plain,
( identity != multiply(a,multiply(a,c))
| spl0_7
| ~ spl0_20 ),
inference(forward_demodulation,[],[f56,f167]) ).
fof(f3475,plain,
( $false
| spl0_3
| ~ spl0_20
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f2806,f38]) ).
fof(f3476,plain,
( spl0_3
| ~ spl0_20
| ~ spl0_29 ),
inference(avatar_contradiction_clause,[],[f3475]) ).
fof(f3483,plain,
( identity != multiply(c,c)
| spl0_7
| ~ spl0_20 ),
inference(forward_demodulation,[],[f3462,f2277]) ).
fof(f3520,plain,
( $false
| spl0_7
| ~ spl0_8
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f2045,f2288]) ).
fof(f3521,plain,
( spl0_7
| ~ spl0_8
| ~ spl0_29 ),
inference(avatar_contradiction_clause,[],[f3520]) ).
fof(f3536,plain,
( b = multiply(a,c)
| a = inverse(c)
| spl0_31
| spl0_32 ),
inference(forward_subsumption_resolution,[],[f2581,f1500]) ).
fof(f3565,plain,
( a = c
| b = multiply(a,c)
| ~ spl0_28
| spl0_31
| spl0_32 ),
inference(forward_demodulation,[],[f3536,f259]) ).
fof(f3580,definition,
( spl0_41
<=> b = multiply(a,c) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f3581,plain,
( b != multiply(a,c)
| spl0_41 ),
inference(avatar_component_clause,[],[f3580]) ).
fof(f3582,plain,
( b = multiply(a,c)
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f3580]) ).
fof(f3592,plain,
( b = multiply(a,c)
| ~ spl0_28
| spl0_31
| spl0_32 ),
inference(forward_subsumption_resolution,[],[f3565,f11]) ).
fof(f3598,plain,
( spl0_41
| ~ spl0_28
| spl0_31
| spl0_32 ),
inference(avatar_split_clause,[],[f3592,f1503,f1499,f257,f3580]) ).
fof(f3620,plain,
( inverse(a) = multiply(c,inverse(b))
| ~ spl0_41 ),
inference(superposition,[],[f497,f3582]) ).
fof(f3642,plain,
( c != c
| b = multiply(b,a)
| a = b
| a = multiply(b,a)
| spl0_8
| ~ spl0_9
| ~ spl0_11 ),
inference(superposition,[],[f291,f2735]) ).
fof(f3643,plain,
( c != c
| b = multiply(b,a)
| a = inverse(b)
| a = multiply(b,a)
| spl0_8
| ~ spl0_9 ),
inference(superposition,[],[f291,f173]) ).
fof(f3644,plain,
( c != c
| b = multiply(b,a)
| b = inverse(a)
| a = multiply(b,a)
| spl0_8
| ~ spl0_9 ),
inference(superposition,[],[f291,f699]) ).
fof(f3646,plain,
( b = multiply(b,a)
| b = inverse(a)
| a = multiply(b,a)
| spl0_8
| ~ spl0_9 ),
inference(trivial_inequality_removal,[],[f3644]) ).
fof(f3647,plain,
( b = multiply(b,a)
| a = inverse(b)
| a = multiply(b,a)
| spl0_8
| ~ spl0_9 ),
inference(trivial_inequality_removal,[],[f3643]) ).
fof(f3648,plain,
( b = multiply(b,a)
| a = b
| a = multiply(b,a)
| spl0_8
| ~ spl0_9
| ~ spl0_11 ),
inference(trivial_inequality_removal,[],[f3642]) ).
fof(f3649,plain,
( b = inverse(a)
| a = multiply(b,a)
| spl0_8
| ~ spl0_9
| spl0_38 ),
inference(forward_subsumption_resolution,[],[f3646,f3339]) ).
fof(f3650,plain,
( a = inverse(b)
| a = multiply(b,a)
| spl0_8
| ~ spl0_9
| spl0_38 ),
inference(forward_subsumption_resolution,[],[f3647,f3339]) ).
fof(f3651,plain,
( a = b
| a = multiply(b,a)
| spl0_8
| ~ spl0_9
| ~ spl0_11
| spl0_38 ),
inference(forward_subsumption_resolution,[],[f3648,f3339]) ).
fof(f3652,plain,
( b = inverse(a)
| spl0_8
| ~ spl0_9
| spl0_37
| spl0_38 ),
inference(forward_subsumption_resolution,[],[f3649,f3335]) ).
fof(f3653,plain,
( a = multiply(b,a)
| spl0_8
| ~ spl0_9
| spl0_27
| spl0_38 ),
inference(forward_subsumption_resolution,[],[f3650,f227]) ).
fof(f3654,plain,
( a = multiply(b,a)
| spl0_8
| ~ spl0_9
| ~ spl0_11
| spl0_38 ),
inference(forward_subsumption_resolution,[],[f3651,f10]) ).
fof(f3655,plain,
( $false
| spl0_8
| ~ spl0_9
| spl0_27
| spl0_37
| spl0_38 ),
inference(forward_subsumption_resolution,[],[f3653,f3335]) ).
fof(f3656,plain,
( spl0_8
| ~ spl0_9
| spl0_27
| spl0_37
| spl0_38 ),
inference(avatar_contradiction_clause,[],[f3655]) ).
fof(f3657,plain,
( $false
| spl0_8
| ~ spl0_9
| ~ spl0_11
| spl0_37
| spl0_38 ),
inference(forward_subsumption_resolution,[],[f3654,f3335]) ).
fof(f3658,plain,
( spl0_8
| ~ spl0_9
| ~ spl0_11
| spl0_37
| spl0_38 ),
inference(avatar_contradiction_clause,[],[f3657]) ).
fof(f3696,plain,
( identity = c
| identity = b
| c = inverse(multiply(c,multiply(c,c)))
| identity = a
| ~ spl0_1 ),
inference(superposition,[],[f699,f29]) ).
fof(f3697,plain,
( identity = b
| c = inverse(multiply(c,multiply(c,c)))
| identity = a
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f3696,f18]) ).
fof(f3707,plain,
( c = inverse(multiply(c,multiply(c,c)))
| identity = a
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f3697,f16]) ).
fof(f3717,plain,
( c = inverse(multiply(c,multiply(c,c)))
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f3707,f13]) ).
fof(f3747,plain,
( identity = multiply(a,multiply(a,inverse(b)))
| ~ spl0_9 ),
inference(superposition,[],[f86,f63]) ).
fof(f3751,plain,
( identity = multiply(a,multiply(a,b))
| ~ spl0_9
| ~ spl0_25 ),
inference(forward_demodulation,[],[f3747,f220]) ).
fof(f3754,plain,
( $false
| spl0_7
| ~ spl0_9
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f3751,f1492]) ).
fof(f3755,plain,
( spl0_7
| ~ spl0_9
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f3754]) ).
fof(f3761,plain,
( c = multiply(b,multiply(b,b))
| ~ spl0_4
| ~ spl0_26 ),
inference(forward_demodulation,[],[f209,f224]) ).
fof(f3775,plain,
( b = inverse(b)
| a = multiply(b,b)
| spl0_6
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f3066,f194]) ).
fof(f3784,plain,
( b = multiply(b,inverse(b))
| b = inverse(b)
| a = multiply(b,inverse(b))
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f3281,f18]) ).
fof(f3809,plain,
( a = multiply(b,b)
| spl0_6
| spl0_24
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f3775,f219]) ).
fof(f3815,plain,
( b = multiply(b,inverse(b))
| a = multiply(b,inverse(b))
| ~ spl0_11
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f3784,f219]) ).
fof(f3847,plain,
( identity = b
| a = multiply(b,inverse(b))
| ~ spl0_11
| spl0_25 ),
inference(forward_demodulation,[],[f3815,f7]) ).
fof(f3865,plain,
( a = multiply(b,inverse(b))
| ~ spl0_11
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f3847,f16]) ).
fof(f3870,plain,
( identity = a
| ~ spl0_11
| spl0_25 ),
inference(forward_demodulation,[],[f3865,f7]) ).
fof(f3871,plain,
( $false
| ~ spl0_11
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f3870,f13]) ).
fof(f3872,plain,
( ~ spl0_11
| spl0_25 ),
inference(avatar_contradiction_clause,[],[f3871]) ).
fof(f3939,plain,
( identity = b
| ~ spl0_10
| ~ spl0_22 ),
inference(forward_demodulation,[],[f68,f186]) ).
fof(f3940,plain,
( identity = multiply(a,b)
| ~ spl0_7
| ~ spl0_20
| ~ spl0_41 ),
inference(forward_demodulation,[],[f1730,f3582]) ).
fof(f3944,plain,
( $false
| ~ spl0_10
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f3939,f16]) ).
fof(f3945,plain,
( ~ spl0_10
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f3944]) ).
fof(f3987,definition,
( spl0_42
<=> a = multiply(c,a) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f3988,plain,
( a != multiply(c,a)
| spl0_42 ),
inference(avatar_component_clause,[],[f3987]) ).
fof(f3989,plain,
( a = multiply(c,a)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f3987]) ).
fof(f3991,definition,
( spl0_43
<=> b = multiply(c,a) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f3992,plain,
( b != multiply(c,a)
| spl0_43 ),
inference(avatar_component_clause,[],[f3991]) ).
fof(f3993,plain,
( b = multiply(c,a)
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f3991]) ).
fof(f4008,plain,
( identity = multiply(c,multiply(a,inverse(a)))
| ~ spl0_42 ),
inference(superposition,[],[f86,f3989]) ).
fof(f4012,plain,
( identity = multiply(c,identity)
| ~ spl0_42 ),
inference(forward_demodulation,[],[f4008,f7]) ).
fof(f4015,plain,
( identity = c
| ~ spl0_42 ),
inference(forward_demodulation,[],[f4012,f5]) ).
fof(f4018,plain,
( $false
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f4015,f18]) ).
fof(f4019,plain,
~ spl0_42,
inference(avatar_contradiction_clause,[],[f4018]) ).
fof(f4028,plain,
( inverse(c) = multiply(a,inverse(b))
| ~ spl0_43 ),
inference(superposition,[],[f497,f3993]) ).
fof(f4029,plain,
( inverse(c) = multiply(a,b)
| ~ spl0_25
| ~ spl0_43 ),
inference(forward_demodulation,[],[f4028,f220]) ).
fof(f4032,plain,
( identity = inverse(c)
| ~ spl0_7
| ~ spl0_20
| ~ spl0_25
| ~ spl0_41
| ~ spl0_43 ),
inference(forward_demodulation,[],[f4029,f3940]) ).
fof(f4036,plain,
( identity = c
| ~ spl0_7
| ~ spl0_20
| ~ spl0_25
| ~ spl0_28
| ~ spl0_41
| ~ spl0_43 ),
inference(forward_demodulation,[],[f4032,f259]) ).
fof(f4037,plain,
( $false
| ~ spl0_7
| ~ spl0_20
| ~ spl0_25
| ~ spl0_28
| ~ spl0_41
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f4036,f18]) ).
fof(f4038,plain,
( ~ spl0_7
| ~ spl0_20
| ~ spl0_25
| ~ spl0_28
| ~ spl0_41
| ~ spl0_43 ),
inference(avatar_contradiction_clause,[],[f4037]) ).
fof(f4040,plain,
( $false
| spl0_7
| ~ spl0_10
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f3483,f68]) ).
fof(f4041,plain,
( spl0_7
| ~ spl0_10
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f4040]) ).
fof(f4047,plain,
( c = multiply(a,c)
| ~ spl0_8
| ~ spl0_20 ),
inference(forward_demodulation,[],[f59,f167]) ).
fof(f4048,plain,
( b = multiply(c,a)
| ~ spl0_8
| ~ spl0_41 ),
inference(forward_demodulation,[],[f2106,f3582]) ).
fof(f4053,plain,
( $false
| ~ spl0_8
| ~ spl0_20
| spl0_32 ),
inference(forward_subsumption_resolution,[],[f4047,f1504]) ).
fof(f4054,plain,
( ~ spl0_8
| ~ spl0_20
| spl0_32 ),
inference(avatar_contradiction_clause,[],[f4053]) ).
fof(f4055,plain,
( $false
| ~ spl0_8
| ~ spl0_41
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f4048,f3992]) ).
fof(f4056,plain,
( ~ spl0_8
| ~ spl0_41
| spl0_43 ),
inference(avatar_contradiction_clause,[],[f4055]) ).
fof(f4166,plain,
( c = inverse(b)
| ~ spl0_1
| ~ spl0_2 ),
inference(forward_demodulation,[],[f3717,f33]) ).
fof(f4191,plain,
( b = c
| ~ spl0_1
| ~ spl0_2
| ~ spl0_25 ),
inference(forward_demodulation,[],[f4166,f220]) ).
fof(f4199,plain,
( $false
| ~ spl0_1
| ~ spl0_2
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f4191,f14]) ).
fof(f4200,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f4199]) ).
fof(f4214,plain,
( c = multiply(b,c)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_26 ),
inference(forward_demodulation,[],[f3761,f50]) ).
fof(f4216,plain,
( multiply(c,c) = inverse(a)
| ~ spl0_26
| ~ spl0_41 ),
inference(forward_demodulation,[],[f3620,f224]) ).
fof(f4223,plain,
( b = multiply(c,c)
| a = multiply(c,c)
| spl0_21
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f2578,f258]) ).
fof(f4232,plain,
( identity = multiply(b,multiply(b,c))
| ~ spl0_4
| ~ spl0_6 ),
inference(forward_demodulation,[],[f42,f50]) ).
fof(f4235,plain,
( identity = inverse(a)
| ~ spl0_10
| ~ spl0_26
| ~ spl0_41 ),
inference(forward_demodulation,[],[f4216,f68]) ).
fof(f4240,plain,
( b = multiply(c,c)
| spl0_3
| spl0_21
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f4223,f38]) ).
fof(f4247,plain,
( identity = multiply(b,c)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_26 ),
inference(forward_demodulation,[],[f4232,f4214]) ).
fof(f4251,plain,
( spl0_22
| spl0_3
| spl0_21
| spl0_28 ),
inference(avatar_split_clause,[],[f4240,f257,f180,f36,f184]) ).
fof(f4257,plain,
( identity = c
| ~ spl0_4
| ~ spl0_6
| ~ spl0_26 ),
inference(forward_demodulation,[],[f4247,f4214]) ).
fof(f4263,plain,
( $false
| ~ spl0_4
| ~ spl0_6
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f4257,f18]) ).
fof(f4264,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_26 ),
inference(avatar_contradiction_clause,[],[f4263]) ).
fof(f4270,plain,
( b = inverse(a)
| ~ spl0_22
| ~ spl0_26
| ~ spl0_41 ),
inference(forward_demodulation,[],[f4216,f186]) ).
fof(f4287,plain,
( c = multiply(inverse(c),b)
| ~ spl0_22 ),
inference(superposition,[],[f83,f186]) ).
fof(f4293,plain,
( c = multiply(b,b)
| ~ spl0_22
| ~ spl0_30 ),
inference(forward_demodulation,[],[f4287,f792]) ).
fof(f4401,plain,
( a = multiply(inverse(a),identity)
| ~ spl0_12 ),
inference(superposition,[],[f83,f76]) ).
fof(f4405,plain,
( inverse(a) = multiply(a,inverse(identity))
| ~ spl0_12 ),
inference(superposition,[],[f497,f76]) ).
fof(f4408,plain,
( multiply(a,identity) = inverse(a)
| ~ spl0_12 ),
inference(forward_demodulation,[],[f4405,f92]) ).
fof(f4412,plain,
( a = inverse(a)
| ~ spl0_12 ),
inference(forward_demodulation,[],[f4401,f5]) ).
fof(f4418,plain,
( b = multiply(a,identity)
| ~ spl0_12
| ~ spl0_22
| ~ spl0_26
| ~ spl0_41 ),
inference(forward_demodulation,[],[f4408,f4270]) ).
fof(f4421,plain,
( a = b
| ~ spl0_12
| ~ spl0_22
| ~ spl0_26
| ~ spl0_41 ),
inference(forward_demodulation,[],[f4418,f5]) ).
fof(f4422,plain,
( $false
| ~ spl0_12
| ~ spl0_22
| ~ spl0_26
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f4421,f10]) ).
fof(f4423,plain,
( ~ spl0_12
| ~ spl0_22
| ~ spl0_26
| ~ spl0_41 ),
inference(avatar_contradiction_clause,[],[f4422]) ).
fof(f4425,plain,
( a = inverse(c)
| spl0_31
| spl0_32
| spl0_41 ),
inference(forward_subsumption_resolution,[],[f3536,f3581]) ).
fof(f4429,plain,
( $false
| spl0_29
| spl0_31
| spl0_32
| spl0_41 ),
inference(forward_subsumption_resolution,[],[f4425,f262]) ).
fof(f4430,plain,
( spl0_29
| spl0_31
| spl0_32
| spl0_41 ),
inference(avatar_contradiction_clause,[],[f4429]) ).
fof(f4439,plain,
( c != c
| b = multiply(c,a)
| a = inverse(c)
| a = multiply(c,a)
| spl0_8
| ~ spl0_20 ),
inference(superposition,[],[f1434,f173]) ).
fof(f4440,plain,
( c != c
| b = multiply(c,a)
| c = inverse(a)
| a = multiply(c,a)
| spl0_8
| ~ spl0_20 ),
inference(superposition,[],[f1434,f699]) ).
fof(f4442,plain,
( b = multiply(c,a)
| c = inverse(a)
| a = multiply(c,a)
| spl0_8
| ~ spl0_20 ),
inference(trivial_inequality_removal,[],[f4440]) ).
fof(f4443,plain,
( b = multiply(c,a)
| a = inverse(c)
| a = multiply(c,a)
| spl0_8
| ~ spl0_20 ),
inference(trivial_inequality_removal,[],[f4439]) ).
fof(f4444,plain,
( c = inverse(a)
| a = multiply(c,a)
| spl0_8
| ~ spl0_20
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f4442,f3992]) ).
fof(f4445,plain,
( a = inverse(c)
| a = multiply(c,a)
| spl0_8
| ~ spl0_20
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f4443,f3992]) ).
fof(f4446,plain,
( c = inverse(a)
| spl0_8
| ~ spl0_20
| spl0_42
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f4444,f3988]) ).
fof(f4447,plain,
( a = multiply(c,a)
| spl0_8
| ~ spl0_20
| spl0_29
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f4445,f262]) ).
fof(f4448,plain,
( b = c
| spl0_8
| ~ spl0_20
| ~ spl0_22
| ~ spl0_26
| ~ spl0_41
| spl0_42
| spl0_43 ),
inference(forward_demodulation,[],[f4446,f4270]) ).
fof(f4449,plain,
( $false
| spl0_8
| ~ spl0_20
| spl0_29
| spl0_42
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f4447,f3988]) ).
fof(f4450,plain,
( spl0_8
| ~ spl0_20
| spl0_29
| spl0_42
| spl0_43 ),
inference(avatar_contradiction_clause,[],[f4449]) ).
fof(f4451,plain,
( $false
| spl0_8
| ~ spl0_20
| ~ spl0_22
| ~ spl0_26
| ~ spl0_41
| spl0_42
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f4448,f14]) ).
fof(f4452,plain,
( spl0_8
| ~ spl0_20
| ~ spl0_22
| ~ spl0_26
| ~ spl0_41
| spl0_42
| spl0_43 ),
inference(avatar_contradiction_clause,[],[f4451]) ).
fof(f4477,plain,
( a = multiply(inverse(c),b)
| ~ spl0_43 ),
inference(superposition,[],[f83,f3993]) ).
fof(f4483,plain,
( a = multiply(b,b)
| ~ spl0_30
| ~ spl0_43 ),
inference(forward_demodulation,[],[f4477,f792]) ).
fof(f4486,plain,
( $false
| spl0_23
| ~ spl0_30
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f4483,f190]) ).
fof(f4487,plain,
( spl0_23
| ~ spl0_30
| ~ spl0_43 ),
inference(avatar_contradiction_clause,[],[f4486]) ).
fof(f4488,plain,
( spl0_23
| spl0_6
| spl0_24
| spl0_25 ),
inference(avatar_split_clause,[],[f3809,f218,f193,f49,f189]) ).
fof(f4498,plain,
( $false
| spl0_6
| ~ spl0_22
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f4293,f51]) ).
fof(f4499,plain,
( spl0_6
| ~ spl0_22
| ~ spl0_30 ),
inference(avatar_contradiction_clause,[],[f4498]) ).
fof(f4528,plain,
( ! [X0] : multiply(b,multiply(b,X0)) = multiply(a,X0)
| ~ spl0_23 ),
inference(superposition,[],[f4,f191]) ).
fof(f4555,definition,
( spl0_44
<=> b = inverse(a) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f4557,plain,
( b = inverse(a)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f4555]) ).
fof(f4559,definition,
( spl0_45
<=> identity = multiply(b,c) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f4560,plain,
( identity = multiply(b,c)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f4559]) ).
fof(f4561,plain,
( identity != multiply(b,c)
| spl0_45 ),
inference(avatar_component_clause,[],[f4559]) ).
fof(f4585,plain,
( c = multiply(b,identity)
| b = multiply(b,multiply(b,b))
| c = multiply(b,multiply(b,b))
| a = multiply(b,multiply(b,b))
| ~ spl0_17 ),
inference(superposition,[],[f151,f9]) ).
fof(f4649,plain,
( a = multiply(a,b)
| ~ spl0_5
| ~ spl0_23 ),
inference(forward_demodulation,[],[f46,f4528]) ).
fof(f4651,plain,
( b = c
| b = multiply(b,multiply(b,b))
| c = multiply(b,multiply(b,b))
| a = multiply(b,multiply(b,b))
| ~ spl0_17 ),
inference(forward_demodulation,[],[f4585,f5]) ).
fof(f4652,plain,
( spl0_36
| ~ spl0_5
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f4649,f189,f45,f3329]) ).
fof(f4653,plain,
( b = multiply(b,multiply(b,b))
| c = multiply(b,multiply(b,b))
| a = multiply(b,multiply(b,b))
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f4651,f14]) ).
fof(f4654,plain,
( b = multiply(a,b)
| c = multiply(b,multiply(b,b))
| a = multiply(b,multiply(b,b))
| ~ spl0_17
| ~ spl0_23 ),
inference(forward_demodulation,[],[f4653,f4528]) ).
fof(f4655,plain,
( identity = b
| c = multiply(b,multiply(b,b))
| a = multiply(b,multiply(b,b))
| ~ spl0_7
| ~ spl0_17
| ~ spl0_20
| ~ spl0_23
| ~ spl0_41 ),
inference(forward_demodulation,[],[f4654,f3940]) ).
fof(f4656,plain,
( c = multiply(b,multiply(b,b))
| a = multiply(b,multiply(b,b))
| ~ spl0_7
| ~ spl0_17
| ~ spl0_20
| ~ spl0_23
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f4655,f16]) ).
fof(f4657,plain,
( c = multiply(a,b)
| a = multiply(b,multiply(b,b))
| ~ spl0_7
| ~ spl0_17
| ~ spl0_20
| ~ spl0_23
| ~ spl0_41 ),
inference(forward_demodulation,[],[f4656,f4528]) ).
fof(f4658,plain,
( identity = c
| a = multiply(b,multiply(b,b))
| ~ spl0_7
| ~ spl0_17
| ~ spl0_20
| ~ spl0_23
| ~ spl0_41 ),
inference(forward_demodulation,[],[f4657,f3940]) ).
fof(f4659,plain,
( a = multiply(b,multiply(b,b))
| ~ spl0_7
| ~ spl0_17
| ~ spl0_20
| ~ spl0_23
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f4658,f18]) ).
fof(f4660,plain,
( a = multiply(a,b)
| ~ spl0_7
| ~ spl0_17
| ~ spl0_20
| ~ spl0_23
| ~ spl0_41 ),
inference(forward_demodulation,[],[f4659,f4528]) ).
fof(f4661,plain,
( spl0_36
| ~ spl0_7
| ~ spl0_17
| ~ spl0_20
| ~ spl0_23
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f4660,f3580,f189,f165,f149,f54,f3329]) ).
fof(f4666,plain,
( b = multiply(inverse(a),a)
| ~ spl0_36 ),
inference(superposition,[],[f83,f3331]) ).
fof(f4672,plain,
( identity = b
| ~ spl0_36 ),
inference(forward_demodulation,[],[f4666,f3]) ).
fof(f4673,plain,
( $false
| ~ spl0_36 ),
inference(forward_subsumption_resolution,[],[f4672,f16]) ).
fof(f4674,plain,
~ spl0_36,
inference(avatar_contradiction_clause,[],[f4673]) ).
fof(f4772,plain,
( spl0_20
| ~ spl0_17
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f2510,f189,f149,f165]) ).
fof(f4807,plain,
( identity = a
| ~ spl0_10
| ~ spl0_12
| ~ spl0_26
| ~ spl0_41 ),
inference(forward_demodulation,[],[f4235,f4412]) ).
fof(f4827,plain,
( $false
| ~ spl0_10
| ~ spl0_12
| ~ spl0_26
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f4807,f13]) ).
fof(f4828,plain,
( ~ spl0_10
| ~ spl0_12
| ~ spl0_26
| ~ spl0_41 ),
inference(avatar_contradiction_clause,[],[f4827]) ).
fof(f4841,plain,
( ~ spl0_12
| spl0_4
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f890,f189,f41,f75]) ).
fof(f4847,plain,
( spl0_27
| ~ spl0_18
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f2500,f189,f153,f226]) ).
fof(f4893,plain,
( c = multiply(inverse(c),b)
| ~ spl0_22 ),
inference(superposition,[],[f83,f186]) ).
fof(f4899,plain,
( a = c
| ~ spl0_22
| ~ spl0_43 ),
inference(forward_demodulation,[],[f4893,f4477]) ).
fof(f4900,plain,
( $false
| ~ spl0_22
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f4899,f11]) ).
fof(f4901,plain,
( ~ spl0_22
| ~ spl0_43 ),
inference(avatar_contradiction_clause,[],[f4900]) ).
fof(f4904,plain,
( spl0_44
| spl0_8
| ~ spl0_9
| spl0_37
| spl0_38 ),
inference(avatar_split_clause,[],[f3652,f3338,f3334,f62,f58,f4555]) ).
fof(f4993,plain,
( multiply(b,c) = multiply(a,b)
| ~ spl0_18
| ~ spl0_23
| ~ spl0_41 ),
inference(superposition,[],[f2493,f3582]) ).
fof(f4994,plain,
( multiply(a,b) = multiply(b,a)
| ~ spl0_9
| ~ spl0_18
| ~ spl0_23 ),
inference(superposition,[],[f2493,f63]) ).
fof(f5041,plain,
( identity = multiply(a,b)
| ~ spl0_9
| ~ spl0_18
| ~ spl0_23 ),
inference(forward_demodulation,[],[f4994,f2484]) ).
fof(f5060,plain,
( identity = multiply(b,c)
| ~ spl0_9
| ~ spl0_18
| ~ spl0_23
| ~ spl0_41 ),
inference(forward_demodulation,[],[f4993,f5041]) ).
fof(f5061,plain,
( $false
| ~ spl0_9
| ~ spl0_18
| ~ spl0_23
| ~ spl0_41
| spl0_45 ),
inference(forward_subsumption_resolution,[],[f5060,f4561]) ).
fof(f5062,plain,
( ~ spl0_9
| ~ spl0_18
| ~ spl0_23
| ~ spl0_41
| spl0_45 ),
inference(avatar_contradiction_clause,[],[f5061]) ).
fof(f5080,plain,
( c != c
| b = inverse(c)
| identity = c
| a = inverse(c)
| spl0_28 ),
inference(superposition,[],[f258,f126]) ).
fof(f5082,plain,
( b = inverse(c)
| identity = c
| a = inverse(c)
| spl0_28 ),
inference(trivial_inequality_removal,[],[f5080]) ).
fof(f5083,plain,
( identity = c
| a = inverse(c)
| spl0_28
| spl0_30 ),
inference(forward_subsumption_resolution,[],[f5082,f791]) ).
fof(f5084,plain,
( a = inverse(c)
| spl0_28
| spl0_30 ),
inference(forward_subsumption_resolution,[],[f5083,f18]) ).
fof(f5088,plain,
( identity = multiply(c,c)
| ~ spl0_28 ),
inference(superposition,[],[f3,f259]) ).
fof(f5098,plain,
( $false
| spl0_10
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f5088,f69]) ).
fof(f5099,plain,
( spl0_10
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f5098]) ).
fof(f5184,plain,
( inverse(b) = multiply(c,inverse(identity))
| ~ spl0_45 ),
inference(superposition,[],[f497,f4560]) ).
fof(f5187,plain,
( multiply(c,identity) = inverse(b)
| ~ spl0_45 ),
inference(forward_demodulation,[],[f5184,f92]) ).
fof(f5196,plain,
( a = multiply(c,identity)
| ~ spl0_27
| ~ spl0_45 ),
inference(forward_demodulation,[],[f5187,f228]) ).
fof(f5204,plain,
( a = c
| ~ spl0_27
| ~ spl0_45 ),
inference(forward_demodulation,[],[f5196,f5]) ).
fof(f5210,plain,
( $false
| ~ spl0_27
| ~ spl0_45 ),
inference(forward_subsumption_resolution,[],[f5204,f11]) ).
fof(f5211,plain,
( ~ spl0_27
| ~ spl0_45 ),
inference(avatar_contradiction_clause,[],[f5210]) ).
fof(f5222,plain,
( spl0_29
| spl0_28
| spl0_30 ),
inference(avatar_split_clause,[],[f5084,f790,f257,f261]) ).
fof(f5223,plain,
( b = c
| ~ spl0_29
| ~ spl0_44 ),
inference(forward_demodulation,[],[f1793,f4557]) ).
fof(f5230,plain,
( $false
| ~ spl0_29
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f5223,f14]) ).
fof(f5231,plain,
( ~ spl0_29
| ~ spl0_44 ),
inference(avatar_contradiction_clause,[],[f5230]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f39]) ).
cnf(s2,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_6 ),
inference(sat_conversion,[],[f52]) ).
cnf(s3,plain,
( ~ spl0_7
| ~ spl0_8
| ~ spl0_9 ),
inference(sat_conversion,[],[f65]) ).
cnf(s4,plain,
( ~ spl0_10
| ~ spl0_11
| ~ spl0_12 ),
inference(sat_conversion,[],[f78]) ).
cnf(s6,plain,
( spl0_4
| spl0_16
| spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f156]) ).
cnf(s7,plain,
( spl0_9
| spl0_12
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f168]) ).
cnf(s8,plain,
( spl0_1
| spl0_3
| spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f187]) ).
cnf(s9,plain,
( spl0_4
| spl0_6
| spl0_23
| spl0_24 ),
inference(sat_conversion,[],[f196]) ).
cnf(s10,plain,
( ~ spl0_4
| spl0_25
| spl0_26
| spl0_27 ),
inference(sat_conversion,[],[f229]) ).
cnf(s12,plain,
~ spl0_21,
inference(sat_conversion,[],[f272]) ).
cnf(s19,plain,
( spl0_1
| ~ spl0_3
| ~ spl0_12 ),
inference(sat_conversion,[],[f410]) ).
cnf(s25,plain,
( ~ spl0_6
| ~ spl0_22
| spl0_30 ),
inference(sat_conversion,[],[f845]) ).
cnf(s29,plain,
( ~ spl0_9
| ~ spl0_23
| spl0_27 ),
inference(sat_conversion,[],[f891]) ).
cnf(s32,plain,
~ spl0_19,
inference(sat_conversion,[],[f914]) ).
cnf(s36,plain,
( ~ spl0_4
| spl0_5
| ~ spl0_27 ),
inference(sat_conversion,[],[f924]) ).
cnf(s37,plain,
( spl0_1
| spl0_6
| ~ spl0_22
| spl0_23
| spl0_24 ),
inference(sat_conversion,[],[f930]) ).
cnf(s38,plain,
( ~ spl0_1
| spl0_2
| spl0_28
| spl0_29 ),
inference(sat_conversion,[],[f932]) ).
cnf(s39,plain,
( ~ spl0_1
| spl0_11
| ~ spl0_22 ),
inference(sat_conversion,[],[f939]) ).
cnf(s43,plain,
( ~ spl0_5
| spl0_6
| spl0_23
| spl0_24 ),
inference(sat_conversion,[],[f976]) ).
cnf(s44,plain,
~ spl0_24,
inference(sat_conversion,[],[f995]) ).
cnf(s46,plain,
( spl0_4
| ~ spl0_6
| ~ spl0_10 ),
inference(sat_conversion,[],[f1000]) ).
cnf(s47,plain,
( spl0_3
| spl0_10
| spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f1009]) ).
cnf(s48,plain,
( spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_27 ),
inference(sat_conversion,[],[f1048]) ).
cnf(s53,plain,
( ~ spl0_6
| spl0_23
| ~ spl0_27
| ~ spl0_30 ),
inference(sat_conversion,[],[f1120]) ).
cnf(s54,plain,
( ~ spl0_3
| ~ spl0_9
| ~ spl0_29 ),
inference(sat_conversion,[],[f1139]) ).
cnf(s58,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_29 ),
inference(sat_conversion,[],[f1225]) ).
cnf(s66,plain,
( ~ spl0_6
| spl0_26
| ~ spl0_30 ),
inference(sat_conversion,[],[f1308]) ).
cnf(s69,plain,
( ~ spl0_6
| ~ spl0_23 ),
inference(sat_conversion,[],[f1331]) ).
cnf(s74,plain,
( ~ spl0_3
| ~ spl0_20
| ~ spl0_30 ),
inference(sat_conversion,[],[f1467]) ).
cnf(s77,plain,
( ~ spl0_3
| spl0_8
| ~ spl0_9
| ~ spl0_30 ),
inference(sat_conversion,[],[f1490]) ).
cnf(s80,plain,
~ spl0_32,
inference(sat_conversion,[],[f1530]) ).
cnf(s81,plain,
~ spl0_31,
inference(sat_conversion,[],[f1546]) ).
cnf(s84,plain,
( ~ spl0_3
| spl0_20
| ~ spl0_29 ),
inference(sat_conversion,[],[f1613]) ).
cnf(s97,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_29
| spl0_31 ),
inference(sat_conversion,[],[f1674]) ).
cnf(s100,plain,
( ~ spl0_3
| ~ spl0_28
| spl0_32 ),
inference(sat_conversion,[],[f1702]) ).
cnf(s103,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_28
| spl0_32 ),
inference(sat_conversion,[],[f1708]) ).
cnf(s106,plain,
( ~ spl0_26
| ~ spl0_29 ),
inference(sat_conversion,[],[f1953]) ).
cnf(s107,plain,
( ~ spl0_6
| spl0_25
| spl0_26
| spl0_27
| ~ spl0_29
| spl0_33 ),
inference(sat_conversion,[],[f1979]) ).
cnf(s109,plain,
~ spl0_33,
inference(sat_conversion,[],[f2010]) ).
cnf(s111,plain,
( ~ spl0_6
| ~ spl0_25 ),
inference(sat_conversion,[],[f2029]) ).
cnf(s113,plain,
( spl0_11
| ~ spl0_25 ),
inference(sat_conversion,[],[f2065]) ).
cnf(s118,plain,
( spl0_4
| ~ spl0_11 ),
inference(sat_conversion,[],[f2167]) ).
cnf(s121,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_8
| ~ spl0_9
| ~ spl0_27 ),
inference(sat_conversion,[],[f2175]) ).
cnf(s129,plain,
( spl0_9
| ~ spl0_23
| ~ spl0_27 ),
inference(sat_conversion,[],[f2261]) ).
cnf(s135,plain,
( ~ spl0_20
| ~ spl0_23
| spl0_25
| spl0_26
| spl0_27
| ~ spl0_29 ),
inference(sat_conversion,[],[f2642]) ).
cnf(s137,plain,
( ~ spl0_11
| ~ spl0_23 ),
inference(sat_conversion,[],[f2659]) ).
cnf(s138,plain,
( ~ spl0_16
| spl0_19
| ~ spl0_23 ),
inference(sat_conversion,[],[f2661]) ).
cnf(s140,plain,
( ~ spl0_4
| ~ spl0_20
| ~ spl0_23 ),
inference(sat_conversion,[],[f2666]) ).
cnf(s143,plain,
( ~ spl0_4
| spl0_11
| ~ spl0_25 ),
inference(sat_conversion,[],[f2672]) ).
cnf(s146,plain,
( ~ spl0_11
| ~ spl0_25
| ~ spl0_29
| spl0_37
| spl0_38
| spl0_39 ),
inference(sat_conversion,[],[f3345]) ).
cnf(s150,plain,
~ spl0_38,
inference(sat_conversion,[],[f3391]) ).
cnf(s153,plain,
~ spl0_37,
inference(sat_conversion,[],[f3415]) ).
cnf(s155,plain,
( spl0_9
| ~ spl0_29
| ~ spl0_39 ),
inference(sat_conversion,[],[f3437]) ).
cnf(s163,plain,
( spl0_3
| ~ spl0_20
| ~ spl0_29 ),
inference(sat_conversion,[],[f3476]) ).
cnf(s166,plain,
( spl0_7
| ~ spl0_8
| ~ spl0_29 ),
inference(sat_conversion,[],[f3521]) ).
cnf(s176,plain,
( ~ spl0_28
| spl0_31
| spl0_32
| spl0_41 ),
inference(sat_conversion,[],[f3598]) ).
cnf(s182,plain,
( spl0_8
| ~ spl0_9
| spl0_27
| spl0_37
| spl0_38 ),
inference(sat_conversion,[],[f3656]) ).
cnf(s183,plain,
( spl0_8
| ~ spl0_9
| ~ spl0_11
| spl0_37
| spl0_38 ),
inference(sat_conversion,[],[f3658]) ).
cnf(s186,plain,
( spl0_7
| ~ spl0_9
| ~ spl0_25 ),
inference(sat_conversion,[],[f3755]) ).
cnf(s206,plain,
( ~ spl0_11
| spl0_25 ),
inference(sat_conversion,[],[f3872]) ).
cnf(s210,plain,
( ~ spl0_10
| ~ spl0_22 ),
inference(sat_conversion,[],[f3945]) ).
cnf(s215,plain,
~ spl0_42,
inference(sat_conversion,[],[f4019]) ).
cnf(s217,plain,
( ~ spl0_7
| ~ spl0_20
| ~ spl0_25
| ~ spl0_28
| ~ spl0_41
| ~ spl0_43 ),
inference(sat_conversion,[],[f4038]) ).
cnf(s218,plain,
( spl0_7
| ~ spl0_10
| ~ spl0_20 ),
inference(sat_conversion,[],[f4041]) ).
cnf(s221,plain,
( ~ spl0_8
| ~ spl0_20
| spl0_32 ),
inference(sat_conversion,[],[f4054]) ).
cnf(s222,plain,
( ~ spl0_8
| ~ spl0_41
| spl0_43 ),
inference(sat_conversion,[],[f4056]) ).
cnf(s235,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_25 ),
inference(sat_conversion,[],[f4200]) ).
cnf(s243,plain,
( spl0_3
| spl0_21
| spl0_22
| spl0_28 ),
inference(sat_conversion,[],[f4251]) ).
cnf(s247,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_26 ),
inference(sat_conversion,[],[f4264]) ).
cnf(s253,plain,
( ~ spl0_12
| ~ spl0_22
| ~ spl0_26
| ~ spl0_41 ),
inference(sat_conversion,[],[f4423]) ).
cnf(s255,plain,
( spl0_29
| spl0_31
| spl0_32
| spl0_41 ),
inference(sat_conversion,[],[f4430]) ).
cnf(s257,plain,
( spl0_8
| ~ spl0_20
| spl0_29
| spl0_42
| spl0_43 ),
inference(sat_conversion,[],[f4450]) ).
cnf(s258,plain,
( spl0_8
| ~ spl0_20
| ~ spl0_22
| ~ spl0_26
| ~ spl0_41
| spl0_42
| spl0_43 ),
inference(sat_conversion,[],[f4452]) ).
cnf(s259,plain,
( spl0_23
| ~ spl0_30
| ~ spl0_43 ),
inference(sat_conversion,[],[f4487]) ).
cnf(s260,plain,
( spl0_6
| spl0_23
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f4488]) ).
cnf(s263,plain,
( spl0_6
| ~ spl0_22
| ~ spl0_30 ),
inference(sat_conversion,[],[f4499]) ).
cnf(s270,plain,
( ~ spl0_5
| ~ spl0_23
| spl0_36 ),
inference(sat_conversion,[],[f4652]) ).
cnf(s271,plain,
( ~ spl0_7
| ~ spl0_17
| ~ spl0_20
| ~ spl0_23
| spl0_36
| ~ spl0_41 ),
inference(sat_conversion,[],[f4661]) ).
cnf(s272,plain,
~ spl0_36,
inference(sat_conversion,[],[f4674]) ).
cnf(s276,plain,
( ~ spl0_17
| spl0_20
| ~ spl0_23 ),
inference(sat_conversion,[],[f4772]) ).
cnf(s288,plain,
( ~ spl0_10
| ~ spl0_12
| ~ spl0_26
| ~ spl0_41 ),
inference(sat_conversion,[],[f4828]) ).
cnf(s290,plain,
( spl0_4
| ~ spl0_12
| ~ spl0_23 ),
inference(sat_conversion,[],[f4841]) ).
cnf(s293,plain,
( ~ spl0_18
| ~ spl0_23
| spl0_27 ),
inference(sat_conversion,[],[f4847]) ).
cnf(s299,plain,
( ~ spl0_22
| ~ spl0_43 ),
inference(sat_conversion,[],[f4901]) ).
cnf(s300,plain,
( spl0_8
| ~ spl0_9
| spl0_37
| spl0_38
| spl0_44 ),
inference(sat_conversion,[],[f4904]) ).
cnf(s302,plain,
( ~ spl0_9
| ~ spl0_18
| ~ spl0_23
| ~ spl0_41
| spl0_45 ),
inference(sat_conversion,[],[f5062]) ).
cnf(s305,plain,
( spl0_10
| ~ spl0_28 ),
inference(sat_conversion,[],[f5099]) ).
cnf(s308,plain,
( ~ spl0_27
| ~ spl0_45 ),
inference(sat_conversion,[],[f5211]) ).
cnf(s312,plain,
( spl0_28
| spl0_29
| spl0_30 ),
inference(sat_conversion,[],[f5222]) ).
cnf(s313,plain,
( ~ spl0_29
| ~ spl0_44 ),
inference(sat_conversion,[],[f5231]) ).
cnf(s315,plain,
( ~ spl0_7
| ~ spl0_17
| ~ spl0_20
| ~ spl0_23
| ~ spl0_41 ),
inference(rat,[],[s271,s272]) ).
cnf(s316,plain,
( ~ spl0_5
| ~ spl0_23 ),
inference(rat,[],[s270,s272]) ).
cnf(s320,plain,
( ~ spl0_11
| ~ spl0_25
| ~ spl0_29
| spl0_39 ),
inference(rat,[],[s146,s150,s153]) ).
cnf(s322,plain,
( ~ spl0_6
| spl0_25
| spl0_26
| spl0_27
| ~ spl0_29 ),
inference(rat,[],[s107,s109]) ).
cnf(s324,plain,
( ~ spl0_5
| spl0_6
| spl0_23 ),
inference(rat,[],[s43,s44]) ).
cnf(s327,plain,
( spl0_1
| spl0_6
| ~ spl0_22
| spl0_23 ),
inference(rat,[],[s37,s44]) ).
cnf(s332,plain,
( spl0_4
| spl0_6
| spl0_23 ),
inference(rat,[],[s9,s44]) ).
cnf(s333,plain,
( spl0_1
| spl0_3
| spl0_22 ),
inference(rat,[],[s8,s12]) ).
cnf(s334,plain,
( spl0_9
| spl0_12
| spl0_20 ),
inference(rat,[],[s7,s32]) ).
cnf(s335,plain,
( spl0_6
| spl0_4
| ~ spl0_22
| spl0_3 ),
inference(rat,[],[s3,s166,s300,s334,s163,s313,s290,s312,s260,s263,s305,s210,s113,s118,s153,s150,s44]) ).
cnf(s336,plain,
( ~ spl0_6
| ~ spl0_22 ),
inference(rat,[],[s334,s182,s258,s253,s222,s255,s106,s66,s53,s25,s69,s299,s153,s150,s215,s81,s80]) ).
cnf(s337,plain,
( spl0_3
| spl0_1 ),
inference(rat,[],[s10,s36,s106,s143,s137,s316,s312,s335,s327,s263,s336,s305,s210,s333]) ).
cnf(s338,plain,
( ~ spl0_29
| ~ spl0_23
| spl0_25
| ~ spl0_3 ),
inference(rat,[],[s129,s135,s54,s84,s106]) ).
cnf(s339,plain,
( ~ spl0_23
| spl0_4
| spl0_1 ),
inference(rat,[],[s308,s302,s29,s6,s334,s276,s74,s312,s255,s338,s138,s100,s19,s337,s113,s118,s81,s80,s32]) ).
cnf(s340,plain,
( ~ spl0_29
| spl0_27
| ~ spl0_6
| spl0_25 ),
inference(rat,[],[s322,s106]) ).
cnf(s341,plain,
( spl0_4
| spl0_2
| spl0_1 ),
inference(rat,[],[s77,s222,s334,s259,s74,s312,s255,s340,s48,s260,s339,s113,s118,s100,s19,s337,s81,s80,s44]) ).
cnf(s342,plain,
( ~ spl0_6
| ~ spl0_4
| spl0_2
| ~ spl0_3 ),
inference(rat,[],[s10,s48,s111,s247]) ).
cnf(s343,plain,
( ~ spl0_23
| spl0_27
| ~ spl0_4
| spl0_12 ),
inference(rat,[],[s334,s29,s140]) ).
cnf(s344,plain,
( ~ spl0_29
| ~ spl0_25
| ~ spl0_3 ),
inference(rat,[],[s155,s320,s54,s113]) ).
cnf(s345,plain,
( spl0_23
| spl0_6
| spl0_1 ),
inference(rat,[],[s183,s222,s334,s259,s74,s312,s255,s344,s113,s260,s100,s19,s337,s153,s150,s81,s80,s44]) ).
cnf(s346,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s36,s343,s316,s345,s342,s341,s19,s337]) ).
cnf(s347,plain,
spl0_1,
inference(rat,[],[s29,s259,s121,s222,s77,s334,s74,s312,s255,s58,s346,s19,s100,s337,s81,s80]) ).
cnf(s349,plain,
~ spl0_3,
inference(rat,[],[s38,s1,s97,s103,s347,s81,s80]) ).
cnf(s350,plain,
( ~ spl0_9
| ~ spl0_25
| spl0_27 ),
inference(rat,[],[s3,s186,s182,s153,s150]) ).
cnf(s351,plain,
( ~ spl0_29
| spl0_9
| ~ spl0_25 ),
inference(rat,[],[s155,s320,s113]) ).
cnf(s352,plain,
( ~ spl0_25
| spl0_27 ),
inference(rat,[],[s217,s257,s218,s221,s334,s4,s305,s38,s255,s351,s350,s235,s113,s215,s80,s347,s81]) ).
cnf(s353,plain,
( spl0_27
| spl0_6
| ~ spl0_4 ),
inference(rat,[],[s288,s255,s47,s343,s106,s39,s260,s10,s206,s352,s81,s80,s12,s349,s347,s44]) ).
cnf(s354,plain,
( spl0_6
| ~ spl0_4 ),
inference(rat,[],[s324,s316,s36,s353]) ).
cnf(s355,plain,
( ~ spl0_6
| ~ spl0_4 ),
inference(rat,[],[s36,s10,s2,s111,s247]) ).
cnf(s356,plain,
~ spl0_4,
inference(rat,[],[s355,s354]) ).
cnf(s357,plain,
~ spl0_11,
inference(rat,[],[s118,s356]) ).
cnf(s359,plain,
~ spl0_22,
inference(rat,[],[s39,s347,s357]) ).
cnf(s361,plain,
spl0_28,
inference(rat,[],[s243,s349,s12,s359]) ).
cnf(s362,plain,
spl0_10,
inference(rat,[],[s47,s349,s12,s359]) ).
cnf(s363,plain,
spl0_41,
inference(rat,[],[s176,s80,s81,s361]) ).
cnf(s364,plain,
~ spl0_6,
inference(rat,[],[s46,s356,s362]) ).
cnf(s365,plain,
spl0_23,
inference(rat,[],[s332,s356,s364]) ).
cnf(s367,plain,
~ spl0_16,
inference(rat,[],[s138,s32,s365]) ).
cnf(s368,plain,
~ spl0_12,
inference(rat,[],[s290,s356,s365]) ).
cnf(s369,plain,
spl0_27,
inference(rat,[],[s315,s218,s6,s334,s293,s29,s365,s363,s362,s356,s367,s368]) ).
cnf(s370,plain,
~ spl0_45,
inference(rat,[],[s308,s369]) ).
cnf(s371,plain,
spl0_9,
inference(rat,[],[s129,s365,s369]) ).
cnf(s373,plain,
~ spl0_18,
inference(rat,[],[s302,s370,s363,s365,s371]) ).
cnf(s374,plain,
spl0_17,
inference(rat,[],[s6,s367,s356,s373]) ).
cnf(s375,plain,
spl0_20,
inference(rat,[],[s276,s365,s374]) ).
cnf(s376,plain,
~ spl0_7,
inference(rat,[],[s315,s363,s365,s375,s374]) ).
cnf(s379,plain,
$false,
inference(rat,[],[s218,s362,s375,s376]) ).
fof(f5238,plain,
$false,
inference(avatar_sat_refutation,[],[s379]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP113-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n026.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 09:22:27 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 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
% 8.69/2.11 % (2568119)Input is clausal, will run a generic CNF schedule.
% 8.69/2.11 % (2568127)lrs+10_1_sil=8000:sp=occurrence:random_seed=668725917:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.69/2.11 % (2568127)Instruction limit reached!
% 8.69/2.11 % (2568127)------------------------------
% 8.69/2.11 % (2568127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.11 % (2568127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.11 % (2568127)CaDiCaL version: 2.1.3
% 8.69/2.11 % (2568127)Termination reason: Instruction limit
% 8.69/2.11 % (2568127)Termination phase: Saturation
% 8.69/2.11 % (2568127)Time elapsed: 0.030 s
% 8.69/2.11 % (2568127)Peak memory usage: 88 MB
% 8.69/2.11 % (2568127)Instructions burned: 108 (million)
% 8.69/2.11 % (2568128)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2376436685:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.69/2.11 % (2568126)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3133203685:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.69/2.11 % (2568124)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=1214961975:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.69/2.11 % (2568130)dis-21_1_sil=8000:lcm=predicate:random_seed=1341617759: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)
% 8.69/2.11 % (2568125)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2129748593:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.69/2.11 % (2568129)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4290560911:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.69/2.11 % (2568130)Refutation not found, incomplete strategy
% 8.69/2.11 % (2568130)------------------------------
% 8.69/2.11 % (2568130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.11 % (2568130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.11 % (2568130)CaDiCaL version: 2.1.3
% 8.69/2.11 % (2568130)Termination reason: Refutation not found, incomplete strategy
% 8.69/2.11 % (2568130)Time elapsed: 0.002 s
% 8.69/2.11 % (2568130)Peak memory usage: 88 MB
% 8.69/2.11 % (2568130)Instructions burned: 1 (million)
% 8.69/2.11 % (2568128)Instruction limit reached!
% 8.69/2.11 % (2568128)------------------------------
% 8.69/2.11 % (2568128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.11 % (2568128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.11 % (2568128)CaDiCaL version: 2.1.3
% 8.69/2.11 % (2568128)Termination reason: Instruction limit
% 8.69/2.11 % (2568128)Termination phase: Saturation
% 8.69/2.11 % (2568128)Time elapsed: 0.065 s
% 8.69/2.11 % (2568128)Peak memory usage: 88 MB
% 8.69/2.11 % (2568128)Instructions burned: 114 (million)
% 8.69/2.11 % (2568132)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=1188507810:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 8.69/2.11 % (2568129)Instruction limit reached!
% 8.69/2.11 % (2568129)------------------------------
% 8.69/2.11 % (2568129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.11 % (2568129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.11 % (2568129)CaDiCaL version: 2.1.3
% 8.69/2.11 % (2568129)Termination reason: Instruction limit
% 8.69/2.11 % (2568129)Termination phase: Saturation
% 8.69/2.11 % (2568129)Time elapsed: 0.103 s
% 8.69/2.11 % (2568129)Peak memory usage: 89 MB
% 8.69/2.11 % (2568129)Instructions burned: 182 (million)
% 8.69/2.11 % (2568132)Instruction limit reached!
% 8.69/2.11 % (2568132)------------------------------
% 8.69/2.11 % (2568132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.11 % (2568132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.11 % (2568132)CaDiCaL version: 2.1.3
% 8.69/2.11 % (2568132)Termination reason: Instruction limit
% 8.69/2.11 % (2568132)Termination phase: Saturation
% 8.69/2.11 % (2568132)Time elapsed: 0.044 s
% 8.69/2.11 % (2568132)Peak memory usage: 89 MB
% 8.69/2.11 % (2568132)Instructions burned: 146 (million)
% 8.69/2.11 % (2568142)lrs+10_64_to=lpo:sil=8000:random_seed=2045692573:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 9.44/2.31 % (2568139)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1520632639: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)
% 9.44/2.31 % (2568141)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1507830470:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 9.44/2.31 % (2568142)Instruction limit reached!
% 9.44/2.31 % (2568142)------------------------------
% 9.44/2.31 % (2568142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.44/2.31 % (2568142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.44/2.31 % (2568142)CaDiCaL version: 2.1.3
% 9.44/2.31 % (2568142)Termination reason: Instruction limit
% 9.44/2.31 % (2568142)Termination phase: Saturation
% 9.44/2.31 % (2568142)Time elapsed: 0.037 s
% 9.44/2.31 % (2568142)Peak memory usage: 88 MB
% 9.44/2.31 % (2568142)Instructions burned: 127 (million)
% 9.44/2.31 % (2568130)------------------------------
% 9.44/2.31 % (2568130)------------------------------
% 9.44/2.31 % (2568139)Instruction limit reached!
% 9.44/2.31 % (2568139)------------------------------
% 9.44/2.31 % (2568139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.44/2.31 % (2568139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.44/2.31 % (2568139)CaDiCaL version: 2.1.3
% 9.44/2.31 % (2568139)Termination reason: Instruction limit
% 9.44/2.31 % (2568139)Termination phase: Saturation
% 9.44/2.31 % (2568139)Time elapsed: 0.097 s
% 9.44/2.31 % (2568139)Peak memory usage: 88 MB
% 9.44/2.31 % (2568139)Instructions burned: 190 (million)
% 9.44/2.31 % (2568146)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=850610618:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 9.44/2.31 % (2568141)Instruction limit reached!
% 9.44/2.31 % (2568141)------------------------------
% 9.44/2.31 % (2568141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.44/2.31 % (2568141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.44/2.31 % (2568141)CaDiCaL version: 2.1.3
% 9.44/2.31 % (2568141)Termination reason: Instruction limit
% 9.44/2.31 % (2568141)Termination phase: Saturation
% 9.44/2.31 % (2568141)Time elapsed: 0.111 s
% 9.44/2.31 % (2568141)Peak memory usage: 88 MB
% 9.44/2.31 % (2568141)Instructions burned: 220 (million)
% 9.44/2.31 % (2568147)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2397567404:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 9.44/2.31 % (2568146)Instruction limit reached!
% 9.44/2.31 % (2568146)------------------------------
% 9.44/2.31 % (2568146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.44/2.31 % (2568146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.44/2.31 % (2568146)CaDiCaL version: 2.1.3
% 9.44/2.31 % (2568146)Termination reason: Instruction limit
% 9.44/2.31 % (2568146)Termination phase: Saturation
% 9.44/2.31 % (2568146)Time elapsed: 0.064 s
% 9.44/2.31 % (2568146)Peak memory usage: 90 MB
% 9.44/2.31 % (2568146)Instructions burned: 197 (million)
% 9.44/2.31 % (2568148)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=866884726:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 9.44/2.31 % (2568152)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1078217703:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 9.44/2.31 % (2568150)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=999621858:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 9.44/2.31 % (2568147)Instruction limit reached!
% 9.44/2.31 % (2568147)------------------------------
% 9.44/2.31 % (2568147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.44/2.31 % (2568147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.44/2.31 % (2568147)CaDiCaL version: 2.1.3
% 9.44/2.31 % (2568147)Termination reason: Instruction limit
% 9.44/2.31 % (2568147)Termination phase: Saturation
% 9.44/2.31 % (2568147)Time elapsed: 0.092 s
% 9.44/2.31 % (2568147)Peak memory usage: 89 MB
% 9.44/2.31 % (2568147)Instructions burned: 159 (million)
% 9.44/2.31 % (2568152)Instruction limit reached!
% 9.44/2.31 % (2568152)------------------------------
% 9.44/2.31 % (2568152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.44/2.31 % (2568152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.44/2.31 % (2568152)CaDiCaL version: 2.1.3
% 9.44/2.31 % (2568152)Termination reason: Instruction limit
% 9.44/2.31 % (2568152)Termination phase: Saturation
% 9.44/2.31 % (2568152)Time elapsed: 0.036 s
% 9.44/2.31 % (2568152)Peak memory usage: 88 MB
% 9.44/2.31 % (2568152)Instructions burned: 110 (million)
% 9.44/2.31 % (2568150)Instruction limit reached!
% 9.44/2.31 % (2568150)------------------------------
% 9.44/2.31 % (2568150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.44/2.31 % (2568150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.44/2.31 % (2568150)CaDiCaL version: 2.1.3
% 9.44/2.31 % (2568150)Termination reason: Instruction limit
% 9.44/2.31 % (2568150)Termination phase: Saturation
% 9.44/2.31 % (2568150)Time elapsed: 0.051 s
% 9.44/2.31 % (2568150)Peak memory usage: 88 MB
% 9.44/2.31 % (2568150)Instructions burned: 106 (million)
% 9.44/2.31 % (2568157)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4283155067:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 9.44/2.31 % (2568156)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=241547091:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 9.44/2.31 % (2568158)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1853790654:i=134:sd=2:doe=on:ss=axioms:sgt=14_2993 on theBenchmark for (2993ds/134Mi)
% 9.44/2.31 % (2568156)Instruction limit reached!
% 9.44/2.31 % (2568156)------------------------------
% 9.44/2.31 % (2568156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.44/2.31 % (2568156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.44/2.31 % (2568156)CaDiCaL version: 2.1.3
% 9.44/2.31 % (2568156)Termination reason: Instruction limit
% 9.44/2.31 % (2568156)Termination phase: Saturation
% 9.44/2.31 % (2568156)Time elapsed: 0.120 s
% 9.44/2.31 % (2568156)Peak memory usage: 89 MB
% 9.44/2.31 % (2568156)Instructions burned: 243 (million)
% 9.44/2.31 % (2568158)Instruction limit reached!
% 9.44/2.31 % (2568158)------------------------------
% 9.44/2.31 % (2568158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.44/2.31 % (2568158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.44/2.31 % (2568158)CaDiCaL version: 2.1.3
% 9.44/2.31 % (2568158)Termination reason: Instruction limit
% 9.44/2.31 % (2568158)Termination phase: Saturation
% 9.44/2.31 % (2568158)Time elapsed: 0.075 s
% 9.44/2.31 % (2568158)Peak memory usage: 89 MB
% 9.44/2.31 % (2568158)Instructions burned: 134 (million)
% 9.44/2.31 % (2568162)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=525546463:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi)
% 9.44/2.31 % (2568163)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=4285246761:i=191:fgj=on:bd=all_2991 on theBenchmark for (2991ds/191Mi)
% 9.44/2.31 % (2568163)Instruction limit reached!
% 9.44/2.31 % (2568163)------------------------------
% 9.44/2.31 % (2568163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.44/2.32 % (2568163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.44/2.32 % (2568163)CaDiCaL version: 2.1.3
% 9.44/2.32 % (2568163)Termination reason: Instruction limit
% 9.44/2.32 % (2568163)Termination phase: Saturation
% 9.44/2.32 % (2568163)Time elapsed: 0.114 s
% 9.44/2.32 % (2568163)Peak memory usage: 89 MB
% 9.44/2.32 % (2568163)Instructions burned: 192 (million)
% 9.44/2.32 % (2568166)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3924145623:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi)
% 9.44/2.32 % (2568162)Instruction limit reached!
% 9.44/2.32 % (2568162)------------------------------
% 9.44/2.32 % (2568162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.44/2.32 % (2568162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.44/2.32 % (2568162)CaDiCaL version: 2.1.3
% 9.44/2.32 % (2568162)Termination reason: Instruction limit
% 9.44/2.32 % (2568162)Termination phase: Saturation
% 9.44/2.32 % (2568162)Time elapsed: 0.262 s
% 9.44/2.32 % (2568162)Peak memory usage: 89 MB
% 9.44/2.32 % (2568162)Instructions burned: 501 (million)
% 9.44/2.32 % (2568148)First to succeed.
% 9.44/2.32 % (2568148)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2568119"
% 9.44/2.32 % (2568168)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=685423131:cond=on:i=156:bs=on:gtg=exists_all:er=known_2987 on theBenchmark for (2987ds/156Mi)
% 9.44/2.32 % (2568166)Instruction limit reached!
% 9.44/2.32 % (2568166)------------------------------
% 9.44/2.32 % (2568166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.44/2.32 % (2568166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.44/2.32 % (2568166)CaDiCaL version: 2.1.3
% 9.44/2.32 % (2568166)Termination reason: Instruction limit
% 9.44/2.32 % (2568166)Termination phase: Saturation
% 9.44/2.32 % (2568166)Time elapsed: 0.154 s
% 9.44/2.32 % (2568166)Peak memory usage: 91 MB
% 9.44/2.32 % (2568166)Instructions burned: 264 (million)
% 9.44/2.32 % (2568148)Refutation found. Thanks to Tanya!
% 9.44/2.32 % SZS status Unsatisfiable for theBenchmark
% 9.44/2.32 % SZS output start Proof for theBenchmark
% See solution above
% 10.83/2.41 % (2568148)------------------------------
% 10.83/2.41 % (2568148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.83/2.41 % (2568148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.83/2.41 % (2568148)CaDiCaL version: 2.1.3
% 10.83/2.41 % (2568148)Termination reason: Refutation
% 10.83/2.41 % (2568148)Time elapsed: 0.706 s
% 10.83/2.41 % (2568148)Peak memory usage: 131 MB
% 10.83/2.41 % (2568148)Instructions burned: 1304 (million)
% 10.83/2.41 % (2568148)------------------------------
% 10.83/2.41 % (2568148)------------------------------
% 10.83/2.41 % (2568119)Success in time 1.46 s
% 10.83/2.41 % Vampire exiting
%------------------------------------------------------------------------------