%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP258-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n009.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:17:18 AM UTC 2026
% Result : Unsatisfiable 0.42s 0.50s
% Output : Refutation 0.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 77
% Syntax : Number of formulae : 441 ( 35 unt; 44 def)
% Number of atoms : 1188 ( 399 equ)
% Maximal formula atoms : 17 ( 2 avg)
% Number of connectives : 1371 ( 624 ~; 703 |; 0 &)
% ( 44 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 46 ( 44 usr; 45 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 60 ( 0 sgn 60 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',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/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
( multiply(sk_c1,sk_c12) = sk_c11
| multiply(sk_c4,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( multiply(sk_c1,sk_c12) = sk_c11
| sk_c11 = multiply(sk_c4,sk_c12) ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( multiply(sk_c1,sk_c12) = sk_c11
| inverse(sk_c4) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( multiply(sk_c1,sk_c12) = sk_c11
| sk_c12 = inverse(sk_c4) ),
inference(reorient_equations,[],[f7]) ).
fof(f16,negated_conjecture,
( multiply(sk_c1,sk_c12) = sk_c11
| multiply(sk_c9,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_7) ).
fof(f17,plain,
( multiply(sk_c1,sk_c12) = sk_c11
| sk_c12 = multiply(sk_c9,sk_c11) ),
inference(reorient_equations,[],[f16]) ).
fof(f23,negated_conjecture,
( inverse(sk_c1) = sk_c12
| multiply(sk_c4,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_11) ).
fof(f24,plain,
( sk_c12 = inverse(sk_c1)
| sk_c11 = multiply(sk_c4,sk_c12) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( inverse(sk_c1) = sk_c12
| inverse(sk_c4) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_12) ).
fof(f26,plain,
( sk_c12 = inverse(sk_c1)
| sk_c12 = inverse(sk_c4) ),
inference(reorient_equations,[],[f25]) ).
fof(f29,negated_conjecture,
( inverse(sk_c1) = sk_c12
| inverse(sk_c5) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_14) ).
fof(f30,plain,
( sk_c12 = inverse(sk_c1)
| sk_c11 = inverse(sk_c5) ),
inference(reorient_equations,[],[f29]) ).
fof(f35,negated_conjecture,
( inverse(sk_c1) = sk_c12
| multiply(sk_c9,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_17) ).
fof(f36,plain,
( sk_c12 = inverse(sk_c1)
| sk_c12 = multiply(sk_c9,sk_c11) ),
inference(reorient_equations,[],[f35]) ).
fof(f43,negated_conjecture,
( multiply(sk_c2,sk_c11) = sk_c10
| multiply(sk_c4,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_21) ).
fof(f44,plain,
( sk_c10 = multiply(sk_c2,sk_c11)
| sk_c11 = multiply(sk_c4,sk_c12) ),
inference(reorient_equations,[],[f43]) ).
fof(f45,negated_conjecture,
( multiply(sk_c2,sk_c11) = sk_c10
| inverse(sk_c4) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_22) ).
fof(f46,plain,
( sk_c10 = multiply(sk_c2,sk_c11)
| sk_c12 = inverse(sk_c4) ),
inference(reorient_equations,[],[f45]) ).
fof(f49,negated_conjecture,
( multiply(sk_c2,sk_c11) = sk_c10
| inverse(sk_c5) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_24) ).
fof(f50,plain,
( sk_c10 = multiply(sk_c2,sk_c11)
| sk_c11 = inverse(sk_c5) ),
inference(reorient_equations,[],[f49]) ).
fof(f63,negated_conjecture,
( inverse(sk_c2) = sk_c11
| multiply(sk_c4,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_31) ).
fof(f64,plain,
( sk_c11 = inverse(sk_c2)
| sk_c11 = multiply(sk_c4,sk_c12) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( inverse(sk_c2) = sk_c11
| inverse(sk_c4) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_32) ).
fof(f66,plain,
( sk_c11 = inverse(sk_c2)
| sk_c12 = inverse(sk_c4) ),
inference(reorient_equations,[],[f65]) ).
fof(f69,negated_conjecture,
( inverse(sk_c2) = sk_c11
| inverse(sk_c5) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_34) ).
fof(f70,plain,
( sk_c11 = inverse(sk_c2)
| sk_c11 = inverse(sk_c5) ),
inference(reorient_equations,[],[f69]) ).
fof(f83,negated_conjecture,
( multiply(sk_c10,sk_c12) = sk_c11
| multiply(sk_c4,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_41) ).
fof(f84,plain,
( sk_c11 = multiply(sk_c10,sk_c12)
| sk_c11 = multiply(sk_c4,sk_c12) ),
inference(reorient_equations,[],[f83]) ).
fof(f85,negated_conjecture,
( multiply(sk_c10,sk_c12) = sk_c11
| inverse(sk_c4) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_42) ).
fof(f86,plain,
( sk_c11 = multiply(sk_c10,sk_c12)
| sk_c12 = inverse(sk_c4) ),
inference(reorient_equations,[],[f85]) ).
fof(f87,negated_conjecture,
( multiply(sk_c10,sk_c12) = sk_c11
| multiply(sk_c5,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_43) ).
fof(f88,plain,
( sk_c11 = multiply(sk_c10,sk_c12)
| multiply(sk_c5,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f87]) ).
fof(f89,negated_conjecture,
( multiply(sk_c10,sk_c12) = sk_c11
| inverse(sk_c5) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_44) ).
fof(f90,plain,
( sk_c11 = multiply(sk_c10,sk_c12)
| sk_c11 = inverse(sk_c5) ),
inference(reorient_equations,[],[f89]) ).
fof(f91,negated_conjecture,
( multiply(sk_c10,sk_c12) = sk_c11
| multiply(sk_c6,sk_c9) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_45) ).
fof(f92,plain,
( sk_c11 = multiply(sk_c10,sk_c12)
| sk_c12 = multiply(sk_c6,sk_c9) ),
inference(reorient_equations,[],[f91]) ).
fof(f93,negated_conjecture,
( multiply(sk_c10,sk_c12) = sk_c11
| inverse(sk_c6) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_46) ).
fof(f94,plain,
( sk_c11 = multiply(sk_c10,sk_c12)
| sk_c9 = inverse(sk_c6) ),
inference(reorient_equations,[],[f93]) ).
fof(f103,negated_conjecture,
( multiply(sk_c3,sk_c10) = sk_c12
| multiply(sk_c4,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_51) ).
fof(f104,plain,
( sk_c12 = multiply(sk_c3,sk_c10)
| sk_c11 = multiply(sk_c4,sk_c12) ),
inference(reorient_equations,[],[f103]) ).
fof(f105,negated_conjecture,
( multiply(sk_c3,sk_c10) = sk_c12
| inverse(sk_c4) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_52) ).
fof(f106,plain,
( sk_c12 = multiply(sk_c3,sk_c10)
| sk_c12 = inverse(sk_c4) ),
inference(reorient_equations,[],[f105]) ).
fof(f107,negated_conjecture,
( multiply(sk_c3,sk_c10) = sk_c12
| multiply(sk_c5,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_53) ).
fof(f108,plain,
( sk_c12 = multiply(sk_c3,sk_c10)
| multiply(sk_c5,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f107]) ).
fof(f109,negated_conjecture,
( multiply(sk_c3,sk_c10) = sk_c12
| inverse(sk_c5) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_54) ).
fof(f110,plain,
( sk_c12 = multiply(sk_c3,sk_c10)
| sk_c11 = inverse(sk_c5) ),
inference(reorient_equations,[],[f109]) ).
fof(f115,negated_conjecture,
( multiply(sk_c3,sk_c10) = sk_c12
| multiply(sk_c9,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_57) ).
fof(f116,plain,
( sk_c12 = multiply(sk_c3,sk_c10)
| sk_c12 = multiply(sk_c9,sk_c11) ),
inference(reorient_equations,[],[f115]) ).
fof(f123,negated_conjecture,
( inverse(sk_c3) = sk_c10
| multiply(sk_c4,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_61) ).
fof(f124,plain,
( sk_c10 = inverse(sk_c3)
| sk_c11 = multiply(sk_c4,sk_c12) ),
inference(reorient_equations,[],[f123]) ).
fof(f125,negated_conjecture,
( inverse(sk_c3) = sk_c10
| inverse(sk_c4) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_62) ).
fof(f126,plain,
( sk_c10 = inverse(sk_c3)
| sk_c12 = inverse(sk_c4) ),
inference(reorient_equations,[],[f125]) ).
fof(f127,negated_conjecture,
( inverse(sk_c3) = sk_c10
| multiply(sk_c5,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_63) ).
fof(f128,plain,
( sk_c10 = inverse(sk_c3)
| multiply(sk_c5,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f127]) ).
fof(f129,negated_conjecture,
( inverse(sk_c3) = sk_c10
| inverse(sk_c5) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_64) ).
fof(f130,plain,
( sk_c10 = inverse(sk_c3)
| sk_c11 = inverse(sk_c5) ),
inference(reorient_equations,[],[f129]) ).
fof(f135,negated_conjecture,
( inverse(sk_c3) = sk_c10
| multiply(sk_c9,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_67) ).
fof(f136,plain,
( sk_c10 = inverse(sk_c3)
| sk_c12 = multiply(sk_c9,sk_c11) ),
inference(reorient_equations,[],[f135]) ).
fof(f143,negated_conjecture,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( multiply(X0,sk_c12) != sk_c11
| inverse(X0) != sk_c12
| multiply(X1,sk_c11) != sk_c10
| inverse(X1) != sk_c11
| multiply(sk_c10,sk_c12) != sk_c11
| multiply(X2,sk_c10) != sk_c12
| inverse(X2) != sk_c10
| multiply(X3,sk_c12) != sk_c11
| inverse(X3) != sk_c12
| multiply(X4,sk_c11) != sk_c10
| inverse(X4) != sk_c11
| multiply(X5,X6) != sk_c12
| inverse(X5) != X6
| multiply(X6,sk_c11) != sk_c12
| inverse(X7) != X8
| inverse(X8) != X6
| multiply(X7,X6) != X8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_71) ).
fof(f144,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( sk_c11 != multiply(X0,sk_c12)
| inverse(X0) != sk_c12
| sk_c10 != multiply(X1,sk_c11)
| sk_c11 != inverse(X1)
| sk_c11 != multiply(sk_c10,sk_c12)
| sk_c12 != multiply(X2,sk_c10)
| sk_c10 != inverse(X2)
| sk_c11 != multiply(X3,sk_c12)
| sk_c12 != inverse(X3)
| sk_c10 != multiply(X4,sk_c11)
| sk_c11 != inverse(X4)
| sk_c12 != multiply(X5,X6)
| inverse(X5) != X6
| sk_c12 != multiply(X6,sk_c11)
| inverse(X7) != X8
| inverse(X8) != X6
| multiply(X7,X6) != X8 ),
inference(reorient_equations,[],[f143]) ).
fof(f145,plain,
! [X2,X3,X0,X1,X8,X7,X4,X5] :
( sk_c11 != multiply(X0,sk_c12)
| inverse(X0) != sk_c12
| sk_c10 != multiply(X1,sk_c11)
| sk_c11 != inverse(X1)
| sk_c11 != multiply(sk_c10,sk_c12)
| sk_c12 != multiply(X2,sk_c10)
| sk_c10 != inverse(X2)
| sk_c11 != multiply(X3,sk_c12)
| sk_c12 != inverse(X3)
| sk_c10 != multiply(X4,sk_c11)
| sk_c11 != inverse(X4)
| sk_c12 != multiply(X5,inverse(X5))
| sk_c12 != multiply(inverse(X5),sk_c11)
| inverse(X7) != X8
| inverse(X5) != inverse(X8)
| multiply(X7,inverse(X5)) != X8 ),
inference(equality_resolution,[],[f144]) ).
fof(f146,plain,
! [X2,X3,X0,X1,X7,X4,X5] :
( sk_c11 != multiply(X0,sk_c12)
| inverse(X0) != sk_c12
| sk_c10 != multiply(X1,sk_c11)
| sk_c11 != inverse(X1)
| sk_c11 != multiply(sk_c10,sk_c12)
| sk_c12 != multiply(X2,sk_c10)
| sk_c10 != inverse(X2)
| sk_c11 != multiply(X3,sk_c12)
| sk_c12 != inverse(X3)
| sk_c10 != multiply(X4,sk_c11)
| sk_c11 != inverse(X4)
| sk_c12 != multiply(X5,inverse(X5))
| sk_c12 != multiply(inverse(X5),sk_c11)
| inverse(X5) != inverse(inverse(X7))
| inverse(X7) != multiply(X7,inverse(X5)) ),
inference(equality_resolution,[],[f145]) ).
fof(f148,definition,
( spl0_1
<=> ! [X5,X7] :
( sk_c12 != multiply(X5,inverse(X5))
| inverse(X7) != multiply(X7,inverse(X5))
| inverse(X5) != inverse(inverse(X7))
| sk_c12 != multiply(inverse(X5),sk_c11) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f149,plain,
( ! [X7,X5] :
( sk_c12 != multiply(inverse(X5),sk_c11)
| inverse(X7) != multiply(X7,inverse(X5))
| inverse(X5) != inverse(inverse(X7))
| sk_c12 != multiply(X5,inverse(X5)) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f148]) ).
fof(f151,definition,
( spl0_2
<=> ! [X4] :
( sk_c10 != multiply(X4,sk_c11)
| sk_c11 != inverse(X4) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f152,plain,
( ! [X4] :
( sk_c10 != multiply(X4,sk_c11)
| sk_c11 != inverse(X4) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f151]) ).
fof(f154,definition,
( spl0_3
<=> ! [X3] :
( sk_c11 != multiply(X3,sk_c12)
| sk_c12 != inverse(X3) ) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f155,plain,
( ! [X3] :
( sk_c11 != multiply(X3,sk_c12)
| sk_c12 != inverse(X3) )
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f154]) ).
fof(f157,definition,
( spl0_4
<=> ! [X2] :
( sk_c12 != multiply(X2,sk_c10)
| sk_c10 != inverse(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f158,plain,
( ! [X2] :
( sk_c10 != inverse(X2)
| sk_c12 != multiply(X2,sk_c10) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f157]) ).
fof(f160,definition,
( spl0_5
<=> sk_c11 = multiply(sk_c10,sk_c12) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f161,plain,
( sk_c11 = multiply(sk_c10,sk_c12)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f160]) ).
fof(f162,plain,
( sk_c11 != multiply(sk_c10,sk_c12)
| spl0_5 ),
inference(avatar_component_clause,[],[f160]) ).
fof(f163,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4
| ~ spl0_5
| spl0_2
| spl0_3 ),
inference(avatar_split_clause,[],[f146,f154,f151,f160,f157,f154,f151,f148]) ).
fof(f169,definition,
( spl0_7
<=> sk_c10 = inverse(sk_c3) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f171,plain,
( sk_c10 = inverse(sk_c3)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f169]) ).
fof(f184,definition,
( spl0_10
<=> sk_c12 = multiply(sk_c9,sk_c11) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f186,plain,
( sk_c12 = multiply(sk_c9,sk_c11)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f184]) ).
fof(f187,plain,
( spl0_10
| spl0_7 ),
inference(avatar_split_clause,[],[f136,f169,f184]) ).
fof(f189,definition,
( spl0_11
<=> sk_c9 = inverse(sk_c6) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f191,plain,
( sk_c9 = inverse(sk_c6)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f189]) ).
fof(f194,definition,
( spl0_12
<=> sk_c12 = multiply(sk_c6,sk_c9) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f196,plain,
( sk_c12 = multiply(sk_c6,sk_c9)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f194]) ).
fof(f199,definition,
( spl0_13
<=> sk_c11 = inverse(sk_c5) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f201,plain,
( sk_c11 = inverse(sk_c5)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f199]) ).
fof(f202,plain,
( spl0_13
| spl0_7 ),
inference(avatar_split_clause,[],[f130,f169,f199]) ).
fof(f204,definition,
( spl0_14
<=> multiply(sk_c5,sk_c11) = sk_c10 ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f205,plain,
( multiply(sk_c5,sk_c11) != sk_c10
| spl0_14 ),
inference(avatar_component_clause,[],[f204]) ).
fof(f206,plain,
( multiply(sk_c5,sk_c11) = sk_c10
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f204]) ).
fof(f207,plain,
( spl0_14
| spl0_7 ),
inference(avatar_split_clause,[],[f128,f169,f204]) ).
fof(f209,definition,
( spl0_15
<=> sk_c12 = inverse(sk_c4) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f211,plain,
( sk_c12 = inverse(sk_c4)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f209]) ).
fof(f212,plain,
( spl0_15
| spl0_7 ),
inference(avatar_split_clause,[],[f126,f169,f209]) ).
fof(f214,definition,
( spl0_16
<=> sk_c11 = multiply(sk_c4,sk_c12) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f216,plain,
( sk_c11 = multiply(sk_c4,sk_c12)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f214]) ).
fof(f217,plain,
( spl0_16
| spl0_7 ),
inference(avatar_split_clause,[],[f124,f169,f214]) ).
fof(f219,definition,
( spl0_17
<=> sk_c12 = multiply(sk_c3,sk_c10) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f221,plain,
( sk_c12 = multiply(sk_c3,sk_c10)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f219]) ).
fof(f225,plain,
( spl0_10
| spl0_17 ),
inference(avatar_split_clause,[],[f116,f219,f184]) ).
fof(f228,plain,
( spl0_13
| spl0_17 ),
inference(avatar_split_clause,[],[f110,f219,f199]) ).
fof(f229,plain,
( spl0_14
| spl0_17 ),
inference(avatar_split_clause,[],[f108,f219,f204]) ).
fof(f230,plain,
( spl0_15
| spl0_17 ),
inference(avatar_split_clause,[],[f106,f219,f209]) ).
fof(f231,plain,
( spl0_16
| spl0_17 ),
inference(avatar_split_clause,[],[f104,f219,f214]) ).
fof(f236,plain,
( spl0_11
| spl0_5 ),
inference(avatar_split_clause,[],[f94,f160,f189]) ).
fof(f237,plain,
( spl0_12
| spl0_5 ),
inference(avatar_split_clause,[],[f92,f160,f194]) ).
fof(f238,plain,
( spl0_13
| spl0_5 ),
inference(avatar_split_clause,[],[f90,f160,f199]) ).
fof(f239,plain,
( spl0_14
| spl0_5 ),
inference(avatar_split_clause,[],[f88,f160,f204]) ).
fof(f240,plain,
( spl0_15
| spl0_5 ),
inference(avatar_split_clause,[],[f86,f160,f209]) ).
fof(f241,plain,
( spl0_16
| spl0_5 ),
inference(avatar_split_clause,[],[f84,f160,f214]) ).
fof(f243,definition,
( spl0_18
<=> sk_c11 = inverse(sk_c2) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f252,plain,
( spl0_13
| spl0_18 ),
inference(avatar_split_clause,[],[f70,f243,f199]) ).
fof(f254,plain,
( spl0_15
| spl0_18 ),
inference(avatar_split_clause,[],[f66,f243,f209]) ).
fof(f255,plain,
( spl0_16
| spl0_18 ),
inference(avatar_split_clause,[],[f64,f243,f214]) ).
fof(f257,definition,
( spl0_19
<=> sk_c10 = multiply(sk_c2,sk_c11) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f259,plain,
( sk_c10 = multiply(sk_c2,sk_c11)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f266,plain,
( spl0_13
| spl0_19 ),
inference(avatar_split_clause,[],[f50,f257,f199]) ).
fof(f268,plain,
( spl0_15
| spl0_19 ),
inference(avatar_split_clause,[],[f46,f257,f209]) ).
fof(f269,plain,
( spl0_16
| spl0_19 ),
inference(avatar_split_clause,[],[f44,f257,f214]) ).
fof(f271,definition,
( spl0_20
<=> sk_c12 = inverse(sk_c1) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f273,plain,
( sk_c12 = inverse(sk_c1)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f277,plain,
( spl0_10
| spl0_20 ),
inference(avatar_split_clause,[],[f36,f271,f184]) ).
fof(f280,plain,
( spl0_13
| spl0_20 ),
inference(avatar_split_clause,[],[f30,f271,f199]) ).
fof(f282,plain,
( spl0_15
| spl0_20 ),
inference(avatar_split_clause,[],[f26,f271,f209]) ).
fof(f283,plain,
( spl0_16
| spl0_20 ),
inference(avatar_split_clause,[],[f24,f271,f214]) ).
fof(f285,definition,
( spl0_21
<=> multiply(sk_c1,sk_c12) = sk_c11 ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f287,plain,
( multiply(sk_c1,sk_c12) = sk_c11
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f285]) ).
fof(f291,plain,
( spl0_10
| spl0_21 ),
inference(avatar_split_clause,[],[f17,f285,f184]) ).
fof(f296,plain,
( spl0_15
| spl0_21 ),
inference(avatar_split_clause,[],[f8,f285,f209]) ).
fof(f297,plain,
( spl0_16
| spl0_21 ),
inference(avatar_split_clause,[],[f6,f285,f214]) ).
fof(f298,plain,
( identity = multiply(sk_c12,sk_c4)
| ~ spl0_15 ),
inference(superposition,[],[f3,f211]) ).
fof(f299,plain,
( identity = multiply(sk_c11,sk_c5)
| ~ spl0_13 ),
inference(superposition,[],[f3,f201]) ).
fof(f300,plain,
( identity = multiply(sk_c9,sk_c6)
| ~ spl0_11 ),
inference(superposition,[],[f3,f191]) ).
fof(f305,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[],[f4,f3]) ).
fof(f306,plain,
( ! [X0] : multiply(identity,X0) = multiply(sk_c12,multiply(sk_c4,X0))
| ~ spl0_15 ),
inference(superposition,[],[f4,f298]) ).
fof(f308,plain,
( ! [X0] : multiply(sk_c4,multiply(sk_c12,X0)) = multiply(sk_c11,X0)
| ~ spl0_16 ),
inference(superposition,[],[f4,f216]) ).
fof(f310,plain,
( ! [X0] : multiply(sk_c12,X0) = multiply(sk_c6,multiply(sk_c9,X0))
| ~ spl0_12 ),
inference(superposition,[],[f4,f196]) ).
fof(f311,plain,
( ! [X0] : multiply(sk_c12,X0) = multiply(sk_c9,multiply(sk_c11,X0))
| ~ spl0_10 ),
inference(superposition,[],[f4,f186]) ).
fof(f312,plain,
( ! [X0] : multiply(identity,X0) = multiply(sk_c9,multiply(sk_c6,X0))
| ~ spl0_11 ),
inference(superposition,[],[f4,f300]) ).
fof(f339,plain,
( multiply(sk_c12,sk_c11) = multiply(identity,sk_c12)
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f306,f216]) ).
fof(f344,plain,
( multiply(sk_c11,sk_c11) = multiply(sk_c4,multiply(identity,sk_c12))
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f308,f339]) ).
fof(f355,plain,
( multiply(identity,sk_c9) = multiply(sk_c9,sk_c12)
| ~ spl0_11
| ~ spl0_12 ),
inference(superposition,[],[f312,f196]) ).
fof(f358,plain,
( multiply(sk_c12,sk_c12) = multiply(sk_c6,multiply(identity,sk_c9))
| ~ spl0_11
| ~ spl0_12 ),
inference(superposition,[],[f310,f355]) ).
fof(f388,plain,
( multiply(sk_c4,sk_c12) = multiply(sk_c11,sk_c11)
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f344,f1]) ).
fof(f486,plain,
( sk_c11 = multiply(sk_c11,sk_c11)
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f216,f388]) ).
fof(f490,plain,
( multiply(sk_c9,sk_c11) = multiply(sk_c12,sk_c11)
| ~ spl0_10
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f311,f486]) ).
fof(f491,plain,
( multiply(identity,sk_c11) = multiply(inverse(sk_c11),sk_c11)
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f305,f486]) ).
fof(f573,plain,
( sk_c12 = multiply(sk_c12,sk_c11)
| ~ spl0_10
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f186,f490]) ).
fof(f585,plain,
( identity = multiply(identity,sk_c11)
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f3,f491]) ).
fof(f590,plain,
( identity = sk_c11
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f1,f585]) ).
fof(f597,plain,
( identity = multiply(identity,sk_c5)
| ~ spl0_13
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f299,f590]) ).
fof(f624,plain,
( identity = sk_c5
| ~ spl0_13
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f1,f597]) ).
fof(f629,plain,
( sk_c10 = multiply(identity,sk_c11)
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f206,f624]) ).
fof(f662,plain,
( sk_c11 = sk_c10
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f1,f629]) ).
fof(f686,plain,
( sk_c11 != multiply(sk_c11,sk_c12)
| spl0_5
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f162,f662]) ).
fof(f813,plain,
( multiply(sk_c6,sk_c9) = multiply(sk_c12,sk_c12)
| ~ spl0_11
| ~ spl0_12 ),
inference(superposition,[],[f358,f1]) ).
fof(f820,plain,
( sk_c12 = multiply(sk_c12,sk_c12)
| ~ spl0_11
| ~ spl0_12 ),
inference(superposition,[],[f196,f813]) ).
fof(f826,plain,
( multiply(sk_c4,sk_c12) = multiply(sk_c11,sk_c12)
| ~ spl0_11
| ~ spl0_12
| ~ spl0_16 ),
inference(superposition,[],[f308,f820]) ).
fof(f835,plain,
( sk_c11 = multiply(sk_c11,sk_c12)
| ~ spl0_11
| ~ spl0_12
| ~ spl0_16 ),
inference(superposition,[],[f216,f826]) ).
fof(f841,plain,
( sk_c11 != sk_c11
| spl0_5
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f686,f835]) ).
fof(f848,plain,
( $false
| spl0_5
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(trivial_inequality_removal,[],[f841]) ).
fof(f849,plain,
( spl0_5
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f848]) ).
fof(f882,plain,
( sk_c11 != sk_c11
| sk_c12 != inverse(sk_c4)
| ~ spl0_3
| ~ spl0_16 ),
inference(superposition,[],[f155,f216]) ).
fof(f890,plain,
( sk_c12 != inverse(sk_c4)
| ~ spl0_3
| ~ spl0_16 ),
inference(trivial_inequality_removal,[],[f882]) ).
fof(f902,definition,
( spl0_24
<=> identity = sk_c11 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f903,plain,
( identity = sk_c11
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f902]) ).
fof(f925,definition,
( spl0_29
<=> sk_c12 = inverse(sk_c10) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f926,plain,
( sk_c12 = inverse(sk_c10)
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f925]) ).
fof(f927,plain,
( sk_c12 != inverse(sk_c10)
| spl0_29 ),
inference(avatar_component_clause,[],[f925]) ).
fof(f934,plain,
( ~ spl0_15
| ~ spl0_3
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f890,f214,f154,f209]) ).
fof(f946,definition,
( spl0_33
<=> sk_c11 = multiply(sk_c11,sk_c12) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f947,plain,
( sk_c11 = multiply(sk_c11,sk_c12)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f946]) ).
fof(f951,definition,
( spl0_34
<=> sk_c12 = inverse(sk_c12) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f955,definition,
( spl0_35
<=> sk_c12 = sk_c11 ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f956,plain,
( sk_c12 = sk_c11
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f955]) ).
fof(f957,plain,
( sk_c12 != sk_c11
| spl0_35 ),
inference(avatar_component_clause,[],[f955]) ).
fof(f979,definition,
( spl0_40
<=> sk_c12 = inverse(identity) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f980,plain,
( sk_c12 = inverse(identity)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f979]) ).
fof(f981,plain,
( sk_c12 != inverse(identity)
| spl0_40 ),
inference(avatar_component_clause,[],[f979]) ).
fof(f988,plain,
( identity = multiply(sk_c12,sk_c1)
| ~ spl0_20 ),
inference(superposition,[],[f3,f273]) ).
fof(f993,plain,
( multiply(identity,sk_c10) = multiply(inverse(sk_c3),sk_c12)
| ~ spl0_17 ),
inference(superposition,[],[f305,f221]) ).
fof(f998,plain,
( sk_c11 != sk_c11
| sk_c12 != inverse(sk_c1)
| ~ spl0_3
| ~ spl0_21 ),
inference(superposition,[],[f155,f287]) ).
fof(f1000,plain,
( multiply(identity,sk_c12) = multiply(inverse(sk_c1),sk_c11)
| ~ spl0_21 ),
inference(superposition,[],[f305,f287]) ).
fof(f1002,plain,
( sk_c12 != inverse(sk_c1)
| ~ spl0_3
| ~ spl0_21 ),
inference(trivial_inequality_removal,[],[f998]) ).
fof(f1003,plain,
( ~ spl0_20
| ~ spl0_3
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f1002,f285,f154,f271]) ).
fof(f1005,plain,
( sk_c11 != sk_c10
| sk_c12 != multiply(sk_c5,sk_c10)
| ~ spl0_4
| ~ spl0_13 ),
inference(superposition,[],[f158,f201]) ).
fof(f1010,plain,
( sk_c10 != sk_c10
| sk_c12 != multiply(sk_c3,sk_c10)
| ~ spl0_4
| ~ spl0_7 ),
inference(superposition,[],[f158,f171]) ).
fof(f1011,plain,
( sk_c12 != multiply(sk_c3,sk_c10)
| ~ spl0_4
| ~ spl0_7 ),
inference(trivial_inequality_removal,[],[f1010]) ).
fof(f1012,plain,
( ~ spl0_17
| ~ spl0_4
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f1011,f169,f157,f219]) ).
fof(f1018,definition,
( spl0_42
<=> sk_c11 = sk_c10 ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f1019,plain,
( sk_c11 = sk_c10
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f1018]) ).
fof(f1046,definition,
( spl0_48
<=> sk_c12 = multiply(sk_c5,sk_c10) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f1047,plain,
( sk_c12 = multiply(sk_c5,sk_c10)
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f1046]) ).
fof(f1048,plain,
( sk_c12 != multiply(sk_c5,sk_c10)
| spl0_48 ),
inference(avatar_component_clause,[],[f1046]) ).
fof(f1049,plain,
( ~ spl0_48
| ~ spl0_42
| ~ spl0_4
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1005,f199,f157,f1018,f1046]) ).
fof(f1055,definition,
( spl0_50
<=> sk_c12 = sk_c10 ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f1056,plain,
( sk_c12 = sk_c10
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f1055]) ).
fof(f1057,plain,
( sk_c12 != sk_c10
| spl0_50 ),
inference(avatar_component_clause,[],[f1055]) ).
fof(f1083,plain,
( ! [X0] :
( sk_c12 != multiply(sk_c10,sk_c11)
| inverse(X0) != multiply(X0,sk_c10)
| sk_c10 != inverse(inverse(X0))
| sk_c12 != multiply(sk_c3,sk_c10) )
| ~ spl0_1
| ~ spl0_7 ),
inference(superposition,[],[f149,f171]) ).
fof(f1088,definition,
( spl0_51
<=> sk_c12 = multiply(sk_c10,inverse(sk_c10)) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f1089,plain,
( sk_c12 = multiply(sk_c10,inverse(sk_c10))
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f1088]) ).
fof(f1090,plain,
( sk_c12 != multiply(sk_c10,inverse(sk_c10))
| spl0_51 ),
inference(avatar_component_clause,[],[f1088]) ).
fof(f1095,definition,
( spl0_53
<=> sk_c12 = multiply(identity,sk_c12) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f1097,plain,
( sk_c12 != multiply(identity,sk_c12)
| spl0_53 ),
inference(avatar_component_clause,[],[f1095]) ).
fof(f1108,definition,
( spl0_56
<=> sk_c12 = multiply(sk_c11,inverse(sk_c11)) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f1110,plain,
( sk_c12 != multiply(sk_c11,inverse(sk_c11))
| spl0_56 ),
inference(avatar_component_clause,[],[f1108]) ).
fof(f1115,definition,
( spl0_58
<=> identity = sk_c12 ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f1116,plain,
( identity = sk_c12
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f1115]) ).
fof(f1120,definition,
( spl0_59
<=> ! [X0] :
( inverse(X0) != multiply(X0,sk_c10)
| sk_c10 != inverse(inverse(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f1121,plain,
( ! [X0] :
( sk_c10 != inverse(inverse(X0))
| inverse(X0) != multiply(X0,sk_c10) )
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f1120]) ).
fof(f1123,definition,
( spl0_60
<=> sk_c12 = multiply(sk_c10,sk_c11) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f1124,plain,
( sk_c12 = multiply(sk_c10,sk_c11)
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f1123]) ).
fof(f1125,plain,
( sk_c12 != multiply(sk_c10,sk_c11)
| spl0_60 ),
inference(avatar_component_clause,[],[f1123]) ).
fof(f1135,definition,
( spl0_63
<=> sk_c12 = multiply(sk_c11,sk_c11) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f1137,plain,
( sk_c12 != multiply(sk_c11,sk_c11)
| spl0_63 ),
inference(avatar_component_clause,[],[f1135]) ).
fof(f1161,definition,
( spl0_69
<=> sk_c12 = multiply(sk_c5,sk_c11) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f1162,plain,
( sk_c12 = multiply(sk_c5,sk_c11)
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f1161]) ).
fof(f1173,definition,
( spl0_72
<=> sk_c12 = multiply(sk_c12,sk_c11) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f1174,plain,
( sk_c12 = multiply(sk_c12,sk_c11)
| ~ spl0_72 ),
inference(avatar_component_clause,[],[f1173]) ).
fof(f1175,plain,
( sk_c12 != multiply(sk_c12,sk_c11)
| spl0_72 ),
inference(avatar_component_clause,[],[f1173]) ).
fof(f1190,plain,
( sk_c12 != sk_c12
| spl0_53 ),
inference(superposition,[],[f1097,f1]) ).
fof(f1191,plain,
( $false
| spl0_53 ),
inference(trivial_inequality_removal,[],[f1190]) ).
fof(f1192,plain,
spl0_53,
inference(avatar_contradiction_clause,[],[f1191]) ).
fof(f1198,plain,
( multiply(sk_c10,sk_c12) = multiply(identity,sk_c10)
| ~ spl0_7
| ~ spl0_17 ),
inference(superposition,[],[f993,f171]) ).
fof(f1206,plain,
( multiply(sk_c12,sk_c11) = multiply(identity,sk_c12)
| ~ spl0_20
| ~ spl0_21 ),
inference(superposition,[],[f1000,f273]) ).
fof(f1251,plain,
( sk_c11 = multiply(identity,sk_c10)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(superposition,[],[f161,f1198]) ).
fof(f1256,plain,
( sk_c11 = sk_c10
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(superposition,[],[f1,f1251]) ).
fof(f1260,plain,
( spl0_42
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f1256,f219,f169,f160,f1018]) ).
fof(f1261,plain,
( sk_c11 = multiply(sk_c11,sk_c12)
| ~ spl0_5
| ~ spl0_42 ),
inference(superposition,[],[f161,f1019]) ).
fof(f1265,plain,
( sk_c12 != inverse(sk_c11)
| spl0_29
| ~ spl0_42 ),
inference(superposition,[],[f927,f1019]) ).
fof(f1274,plain,
( sk_c12 != sk_c11
| ~ spl0_42
| spl0_50 ),
inference(superposition,[],[f1057,f1019]) ).
fof(f1277,plain,
( sk_c12 != multiply(sk_c11,inverse(sk_c11))
| ~ spl0_42
| spl0_51 ),
inference(superposition,[],[f1090,f1019]) ).
fof(f1278,plain,
( sk_c12 != multiply(sk_c11,sk_c11)
| ~ spl0_42
| spl0_60 ),
inference(superposition,[],[f1125,f1019]) ).
fof(f1282,plain,
( spl0_33
| ~ spl0_5
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f1261,f1018,f160,f946]) ).
fof(f1326,plain,
( sk_c12 != multiply(identity,sk_c12)
| ~ spl0_20
| ~ spl0_21
| spl0_72 ),
inference(superposition,[],[f1175,f1206]) ).
fof(f1333,plain,
( ~ spl0_53
| ~ spl0_20
| ~ spl0_21
| spl0_72 ),
inference(avatar_split_clause,[],[f1326,f1173,f285,f271,f1095]) ).
fof(f1340,plain,
( multiply(identity,sk_c11) = multiply(inverse(sk_c12),sk_c12)
| ~ spl0_72 ),
inference(superposition,[],[f305,f1174]) ).
fof(f1365,plain,
( identity = multiply(identity,sk_c11)
| ~ spl0_72 ),
inference(superposition,[],[f3,f1340]) ).
fof(f1370,plain,
( identity = sk_c11
| ~ spl0_72 ),
inference(superposition,[],[f1,f1365]) ).
fof(f1374,plain,
( spl0_24
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f1370,f1173,f902]) ).
fof(f1379,plain,
( identity = multiply(identity,sk_c5)
| ~ spl0_13
| ~ spl0_24 ),
inference(superposition,[],[f299,f903]) ).
fof(f1390,plain,
( identity = multiply(identity,sk_c12)
| ~ spl0_24
| ~ spl0_33 ),
inference(superposition,[],[f947,f903]) ).
fof(f1391,plain,
( identity != sk_c12
| ~ spl0_24
| spl0_35 ),
inference(superposition,[],[f957,f903]) ).
fof(f1398,plain,
( sk_c12 != multiply(identity,identity)
| ~ spl0_24
| spl0_63 ),
inference(superposition,[],[f1137,f903]) ).
fof(f1407,plain,
( sk_c12 != inverse(identity)
| ~ spl0_24
| spl0_29
| ~ spl0_42 ),
inference(superposition,[],[f1265,f903]) ).
fof(f1439,plain,
( identity = sk_c5
| ~ spl0_13
| ~ spl0_24 ),
inference(superposition,[],[f1,f1379]) ).
fof(f1443,plain,
( sk_c11 = inverse(identity)
| ~ spl0_13
| ~ spl0_24 ),
inference(superposition,[],[f201,f1439]) ).
fof(f1454,plain,
( sk_c12 != sk_c11
| ~ spl0_13
| ~ spl0_24
| spl0_40 ),
inference(superposition,[],[f981,f1443]) ).
fof(f1470,plain,
( identity = sk_c12
| ~ spl0_24
| ~ spl0_33 ),
inference(superposition,[],[f1,f1390]) ).
fof(f1474,plain,
( spl0_58
| ~ spl0_24
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f1470,f946,f902,f1115]) ).
fof(f1476,plain,
( ~ spl0_58
| ~ spl0_24
| spl0_35 ),
inference(avatar_split_clause,[],[f1391,f955,f902,f1115]) ).
fof(f1478,plain,
( ~ spl0_35
| ~ spl0_42
| spl0_50 ),
inference(avatar_split_clause,[],[f1274,f1055,f1018,f955]) ).
fof(f1480,plain,
( ~ spl0_35
| ~ spl0_13
| ~ spl0_24
| spl0_40 ),
inference(avatar_split_clause,[],[f1454,f979,f902,f199,f955]) ).
fof(f1482,plain,
( ~ spl0_63
| ~ spl0_42
| spl0_60 ),
inference(avatar_split_clause,[],[f1278,f1123,f1018,f1135]) ).
fof(f1484,plain,
( ~ spl0_40
| ~ spl0_24
| spl0_29
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f1407,f1018,f925,f902,f979]) ).
fof(f1498,plain,
( sk_c12 != multiply(sk_c5,sk_c12)
| spl0_48
| ~ spl0_50 ),
inference(superposition,[],[f1048,f1056]) ).
fof(f1519,plain,
( identity = multiply(identity,sk_c1)
| ~ spl0_20
| ~ spl0_58 ),
inference(superposition,[],[f988,f1116]) ).
fof(f1568,plain,
( sk_c12 = inverse(sk_c11)
| ~ spl0_29
| ~ spl0_42 ),
inference(superposition,[],[f926,f1019]) ).
fof(f1585,plain,
( sk_c11 != sk_c10
| sk_c11 != inverse(identity)
| ~ spl0_2 ),
inference(superposition,[],[f152,f1]) ).
fof(f1597,plain,
( sk_c10 != sk_c10
| sk_c11 != inverse(sk_c2)
| ~ spl0_2
| ~ spl0_19 ),
inference(superposition,[],[f152,f259]) ).
fof(f1600,plain,
( sk_c11 != inverse(sk_c2)
| ~ spl0_2
| ~ spl0_19 ),
inference(trivial_inequality_removal,[],[f1597]) ).
fof(f1611,plain,
( ~ spl0_18
| ~ spl0_2
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f1600,f257,f151,f243]) ).
fof(f1627,definition,
( spl0_80
<=> sk_c11 = inverse(sk_c11) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f1628,plain,
( sk_c11 = inverse(sk_c11)
| ~ spl0_80 ),
inference(avatar_component_clause,[],[f1627]) ).
fof(f1629,plain,
( sk_c11 != inverse(sk_c11)
| spl0_80 ),
inference(avatar_component_clause,[],[f1627]) ).
fof(f1632,definition,
( spl0_81
<=> sk_c11 = inverse(sk_c12) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f1633,plain,
( sk_c11 = inverse(sk_c12)
| ~ spl0_81 ),
inference(avatar_component_clause,[],[f1632]) ).
fof(f1634,plain,
( sk_c11 != inverse(sk_c12)
| spl0_81 ),
inference(avatar_component_clause,[],[f1632]) ).
fof(f1666,definition,
( spl0_88
<=> sk_c11 = inverse(identity) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f1668,plain,
( sk_c11 != inverse(identity)
| spl0_88 ),
inference(avatar_component_clause,[],[f1666]) ).
fof(f1669,plain,
( ~ spl0_88
| ~ spl0_42
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f1585,f151,f1018,f1666]) ).
fof(f1673,plain,
( ~ spl0_17
| spl0_59
| ~ spl0_60
| ~ spl0_1
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f1083,f169,f148,f1123,f1120,f219]) ).
fof(f1703,plain,
( sk_c12 != sk_c11
| ~ spl0_40
| spl0_88 ),
inference(superposition,[],[f1668,f980]) ).
fof(f1704,plain,
( sk_c11 != sk_c11
| ~ spl0_13
| ~ spl0_24
| spl0_88 ),
inference(superposition,[],[f1668,f1443]) ).
fof(f1705,plain,
( $false
| ~ spl0_13
| ~ spl0_24
| spl0_88 ),
inference(trivial_inequality_removal,[],[f1704]) ).
fof(f1706,plain,
( ~ spl0_13
| ~ spl0_24
| spl0_88 ),
inference(avatar_contradiction_clause,[],[f1705]) ).
fof(f1707,plain,
( ~ spl0_35
| ~ spl0_40
| spl0_88 ),
inference(avatar_split_clause,[],[f1703,f1666,f979,f955]) ).
fof(f1717,plain,
( sk_c11 != inverse(identity)
| ~ spl0_58
| spl0_81 ),
inference(superposition,[],[f1634,f1116]) ).
fof(f1720,plain,
( ~ spl0_88
| ~ spl0_58
| spl0_81 ),
inference(avatar_split_clause,[],[f1717,f1632,f1115,f1666]) ).
fof(f1728,plain,
( sk_c12 != inverse(sk_c12)
| ~ spl0_35
| spl0_80 ),
inference(superposition,[],[f1629,f956]) ).
fof(f1730,plain,
( ~ spl0_34
| ~ spl0_35
| spl0_80 ),
inference(avatar_split_clause,[],[f1728,f1627,f955,f951]) ).
fof(f1734,plain,
( sk_c12 != multiply(sk_c11,sk_c11)
| spl0_56
| ~ spl0_80 ),
inference(superposition,[],[f1110,f1628]) ).
fof(f1738,plain,
( ~ spl0_63
| spl0_56
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f1734,f1627,f1108,f1135]) ).
fof(f1739,plain,
( ~ spl0_56
| ~ spl0_42
| spl0_51 ),
inference(avatar_split_clause,[],[f1277,f1088,f1018,f1108]) ).
fof(f1760,plain,
( sk_c12 = multiply(sk_c10,sk_c12)
| ~ spl0_35
| ~ spl0_60 ),
inference(superposition,[],[f1124,f956]) ).
fof(f1840,plain,
( sk_c12 = inverse(sk_c12)
| ~ spl0_29
| ~ spl0_35
| ~ spl0_42 ),
inference(superposition,[],[f1568,f956]) ).
fof(f1978,plain,
( sk_c12 != multiply(identity,sk_c12)
| ~ spl0_13
| ~ spl0_24
| spl0_48
| ~ spl0_50 ),
inference(superposition,[],[f1498,f1439]) ).
fof(f1980,plain,
( ~ spl0_53
| ~ spl0_13
| ~ spl0_24
| spl0_48
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f1978,f1055,f1046,f902,f199,f1095]) ).
fof(f1981,plain,
( sk_c12 = multiply(identity,sk_c10)
| ~ spl0_13
| ~ spl0_24
| ~ spl0_48 ),
inference(superposition,[],[f1047,f1439]) ).
fof(f1984,plain,
( sk_c12 = multiply(sk_c5,sk_c11)
| ~ spl0_42
| ~ spl0_48 ),
inference(superposition,[],[f1047,f1019]) ).
fof(f1989,plain,
( spl0_69
| ~ spl0_42
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f1984,f1046,f1018,f1161]) ).
fof(f1991,definition,
( spl0_89
<=> sk_c12 = multiply(identity,identity) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f1993,plain,
( sk_c12 != multiply(identity,identity)
| spl0_89 ),
inference(avatar_component_clause,[],[f1991]) ).
fof(f2005,plain,
( sk_c12 != sk_c10
| spl0_14
| ~ spl0_69 ),
inference(superposition,[],[f205,f1162]) ).
fof(f2010,plain,
( ~ spl0_50
| spl0_14
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f2005,f1161,f204,f1055]) ).
fof(f2020,plain,
( identity != sk_c12
| spl0_89 ),
inference(superposition,[],[f1993,f1]) ).
fof(f2021,plain,
( ~ spl0_58
| spl0_89 ),
inference(avatar_split_clause,[],[f2020,f1991,f1115]) ).
fof(f2081,plain,
( identity = sk_c1
| ~ spl0_20
| ~ spl0_58 ),
inference(superposition,[],[f1,f1519]) ).
fof(f2085,plain,
( sk_c12 = inverse(identity)
| ~ spl0_20
| ~ spl0_58 ),
inference(superposition,[],[f273,f2081]) ).
fof(f2328,plain,
( sk_c12 = multiply(identity,sk_c10)
| ~ spl0_7
| ~ spl0_17
| ~ spl0_35
| ~ spl0_60 ),
inference(superposition,[],[f1198,f1760]) ).
fof(f2336,plain,
( sk_c10 != inverse(sk_c12)
| sk_c12 != multiply(identity,sk_c10)
| ~ spl0_40
| ~ spl0_59 ),
inference(superposition,[],[f1121,f980]) ).
fof(f2398,definition,
( spl0_98
<=> sk_c10 = inverse(sk_c10) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f2399,plain,
( sk_c10 = inverse(sk_c10)
| ~ spl0_98 ),
inference(avatar_component_clause,[],[f2398]) ).
fof(f2400,plain,
( sk_c10 != inverse(sk_c10)
| spl0_98 ),
inference(avatar_component_clause,[],[f2398]) ).
fof(f2440,definition,
( spl0_107
<=> sk_c12 = multiply(sk_c10,sk_c10) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f2444,definition,
( spl0_108
<=> sk_c10 = inverse(sk_c12) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f2446,plain,
( sk_c10 != inverse(sk_c12)
| spl0_108 ),
inference(avatar_component_clause,[],[f2444]) ).
fof(f2524,definition,
( spl0_124
<=> sk_c12 = multiply(identity,sk_c10) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f2527,plain,
( ~ spl0_124
| ~ spl0_108
| ~ spl0_40
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f2336,f1120,f979,f2444,f2524]) ).
fof(f2536,plain,
( sk_c12 != sk_c10
| ~ spl0_29
| spl0_98 ),
inference(superposition,[],[f2400,f926]) ).
fof(f2537,plain,
( ~ spl0_50
| ~ spl0_29
| spl0_98 ),
inference(avatar_split_clause,[],[f2536,f2398,f925,f1055]) ).
fof(f2541,plain,
( spl0_40
| ~ spl0_20
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f2085,f1115,f271,f979]) ).
fof(f2543,plain,
( spl0_124
| ~ spl0_7
| ~ spl0_17
| ~ spl0_35
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f2328,f1123,f955,f219,f169,f2524]) ).
fof(f2546,plain,
( spl0_34
| ~ spl0_29
| ~ spl0_35
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f1840,f1018,f955,f925,f951]) ).
fof(f2582,plain,
( sk_c12 = multiply(sk_c10,sk_c10)
| ~ spl0_51
| ~ spl0_98 ),
inference(superposition,[],[f1089,f2399]) ).
fof(f2586,plain,
( ! [X0] :
( sk_c12 != multiply(sk_c10,sk_c11)
| inverse(X0) != multiply(X0,sk_c10)
| sk_c10 != inverse(inverse(X0))
| sk_c12 != multiply(sk_c10,sk_c10) )
| ~ spl0_1
| ~ spl0_98 ),
inference(superposition,[],[f149,f2399]) ).
fof(f2594,plain,
( spl0_107
| ~ spl0_51
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f2582,f2398,f1088,f2440]) ).
fof(f2598,plain,
( sk_c11 != sk_c10
| ~ spl0_81
| spl0_108 ),
inference(superposition,[],[f2446,f1633]) ).
fof(f2599,plain,
( ~ spl0_42
| ~ spl0_81
| spl0_108 ),
inference(avatar_split_clause,[],[f2598,f2444,f1632,f1018]) ).
fof(f2600,plain,
( spl0_124
| ~ spl0_13
| ~ spl0_24
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f1981,f1046,f902,f199,f2524]) ).
fof(f2601,plain,
( spl0_42
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f662,f214,f209,f204,f199,f1018]) ).
fof(f2606,plain,
( ~ spl0_89
| ~ spl0_24
| spl0_63 ),
inference(avatar_split_clause,[],[f1398,f1135,f902,f1991]) ).
fof(f2607,plain,
( spl0_72
| ~ spl0_10
| ~ spl0_15
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f573,f214,f209,f184,f1173]) ).
fof(f2614,plain,
( ~ spl0_107
| spl0_59
| ~ spl0_60
| ~ spl0_1
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f2586,f2398,f148,f1123,f1120,f2440]) ).
cnf(s1,plain,
( spl0_2
| spl0_3
| spl0_2
| spl0_1
| spl0_3
| spl0_4
| ~ spl0_5 ),
inference(sat_conversion,[],[f163]) ).
cnf(s2,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4
| ~ spl0_5 ),
inference(rat,[],[s1]) ).
cnf(s6,plain,
( spl0_7
| spl0_10 ),
inference(sat_conversion,[],[f187]) ).
cnf(s9,plain,
( spl0_7
| spl0_13 ),
inference(sat_conversion,[],[f202]) ).
cnf(s10,plain,
( spl0_7
| spl0_14 ),
inference(sat_conversion,[],[f207]) ).
cnf(s11,plain,
( spl0_7
| spl0_15 ),
inference(sat_conversion,[],[f212]) ).
cnf(s12,plain,
( spl0_7
| spl0_16 ),
inference(sat_conversion,[],[f217]) ).
cnf(s16,plain,
( spl0_10
| spl0_17 ),
inference(sat_conversion,[],[f225]) ).
cnf(s19,plain,
( spl0_13
| spl0_17 ),
inference(sat_conversion,[],[f228]) ).
cnf(s20,plain,
( spl0_14
| spl0_17 ),
inference(sat_conversion,[],[f229]) ).
cnf(s21,plain,
( spl0_15
| spl0_17 ),
inference(sat_conversion,[],[f230]) ).
cnf(s22,plain,
( spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f231]) ).
cnf(s27,plain,
( spl0_5
| spl0_11 ),
inference(sat_conversion,[],[f236]) ).
cnf(s28,plain,
( spl0_5
| spl0_12 ),
inference(sat_conversion,[],[f237]) ).
cnf(s29,plain,
( spl0_5
| spl0_13 ),
inference(sat_conversion,[],[f238]) ).
cnf(s30,plain,
( spl0_5
| spl0_14 ),
inference(sat_conversion,[],[f239]) ).
cnf(s31,plain,
( spl0_5
| spl0_15 ),
inference(sat_conversion,[],[f240]) ).
cnf(s32,plain,
( spl0_5
| spl0_16 ),
inference(sat_conversion,[],[f241]) ).
cnf(s39,plain,
( spl0_13
| spl0_18 ),
inference(sat_conversion,[],[f252]) ).
cnf(s41,plain,
( spl0_15
| spl0_18 ),
inference(sat_conversion,[],[f254]) ).
cnf(s42,plain,
( spl0_16
| spl0_18 ),
inference(sat_conversion,[],[f255]) ).
cnf(s49,plain,
( spl0_13
| spl0_19 ),
inference(sat_conversion,[],[f266]) ).
cnf(s51,plain,
( spl0_15
| spl0_19 ),
inference(sat_conversion,[],[f268]) ).
cnf(s52,plain,
( spl0_16
| spl0_19 ),
inference(sat_conversion,[],[f269]) ).
cnf(s56,plain,
( spl0_10
| spl0_20 ),
inference(sat_conversion,[],[f277]) ).
cnf(s59,plain,
( spl0_13
| spl0_20 ),
inference(sat_conversion,[],[f280]) ).
cnf(s61,plain,
( spl0_15
| spl0_20 ),
inference(sat_conversion,[],[f282]) ).
cnf(s62,plain,
( spl0_16
| spl0_20 ),
inference(sat_conversion,[],[f283]) ).
cnf(s66,plain,
( spl0_10
| spl0_21 ),
inference(sat_conversion,[],[f291]) ).
cnf(s71,plain,
( spl0_15
| spl0_21 ),
inference(sat_conversion,[],[f296]) ).
cnf(s72,plain,
( spl0_16
| spl0_21 ),
inference(sat_conversion,[],[f297]) ).
cnf(s73,plain,
( spl0_5
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(sat_conversion,[],[f849]) ).
cnf(s80,plain,
( ~ spl0_3
| ~ spl0_15
| ~ spl0_16 ),
inference(sat_conversion,[],[f934]) ).
cnf(s91,plain,
( ~ spl0_3
| ~ spl0_20
| ~ spl0_21 ),
inference(sat_conversion,[],[f1003]) ).
cnf(s92,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_17 ),
inference(sat_conversion,[],[f1012]) ).
cnf(s97,plain,
( ~ spl0_4
| ~ spl0_13
| ~ spl0_42
| ~ spl0_48 ),
inference(sat_conversion,[],[f1049]) ).
cnf(s110,plain,
spl0_53,
inference(sat_conversion,[],[f1192]) ).
cnf(s113,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| spl0_42 ),
inference(sat_conversion,[],[f1260]) ).
cnf(s115,plain,
( ~ spl0_5
| spl0_33
| ~ spl0_42 ),
inference(sat_conversion,[],[f1282]) ).
cnf(s116,plain,
( ~ spl0_20
| ~ spl0_21
| ~ spl0_53
| spl0_72 ),
inference(sat_conversion,[],[f1333]) ).
cnf(s119,plain,
( spl0_24
| ~ spl0_72 ),
inference(sat_conversion,[],[f1374]) ).
cnf(s123,plain,
( ~ spl0_24
| ~ spl0_33
| spl0_58 ),
inference(sat_conversion,[],[f1474]) ).
cnf(s127,plain,
( ~ spl0_24
| spl0_35
| ~ spl0_58 ),
inference(sat_conversion,[],[f1476]) ).
cnf(s129,plain,
( ~ spl0_35
| ~ spl0_42
| spl0_50 ),
inference(sat_conversion,[],[f1478]) ).
cnf(s131,plain,
( ~ spl0_13
| ~ spl0_24
| ~ spl0_35
| spl0_40 ),
inference(sat_conversion,[],[f1480]) ).
cnf(s133,plain,
( ~ spl0_42
| spl0_60
| ~ spl0_63 ),
inference(sat_conversion,[],[f1482]) ).
cnf(s135,plain,
( ~ spl0_24
| spl0_29
| ~ spl0_40
| ~ spl0_42 ),
inference(sat_conversion,[],[f1484]) ).
cnf(s143,plain,
( ~ spl0_2
| ~ spl0_18
| ~ spl0_19 ),
inference(sat_conversion,[],[f1611]) ).
cnf(s153,plain,
( ~ spl0_2
| ~ spl0_42
| ~ spl0_88 ),
inference(sat_conversion,[],[f1669]) ).
cnf(s157,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_17
| spl0_59
| ~ spl0_60 ),
inference(sat_conversion,[],[f1673]) ).
cnf(s161,plain,
( ~ spl0_13
| ~ spl0_24
| spl0_88 ),
inference(sat_conversion,[],[f1706]) ).
cnf(s162,plain,
( ~ spl0_35
| ~ spl0_40
| spl0_88 ),
inference(sat_conversion,[],[f1707]) ).
cnf(s165,plain,
( ~ spl0_58
| spl0_81
| ~ spl0_88 ),
inference(sat_conversion,[],[f1720]) ).
cnf(s166,plain,
( ~ spl0_34
| ~ spl0_35
| spl0_80 ),
inference(sat_conversion,[],[f1730]) ).
cnf(s167,plain,
( spl0_56
| ~ spl0_63
| ~ spl0_80 ),
inference(sat_conversion,[],[f1738]) ).
cnf(s168,plain,
( ~ spl0_42
| spl0_51
| ~ spl0_56 ),
inference(sat_conversion,[],[f1739]) ).
cnf(s178,plain,
( ~ spl0_13
| ~ spl0_24
| spl0_48
| ~ spl0_50
| ~ spl0_53 ),
inference(sat_conversion,[],[f1980]) ).
cnf(s179,plain,
( ~ spl0_42
| ~ spl0_48
| spl0_69 ),
inference(sat_conversion,[],[f1989]) ).
cnf(s181,plain,
( spl0_14
| ~ spl0_50
| ~ spl0_69 ),
inference(sat_conversion,[],[f2010]) ).
cnf(s182,plain,
( ~ spl0_58
| spl0_89 ),
inference(sat_conversion,[],[f2021]) ).
cnf(s216,plain,
( ~ spl0_40
| ~ spl0_59
| ~ spl0_108
| ~ spl0_124 ),
inference(sat_conversion,[],[f2527]) ).
cnf(s218,plain,
( ~ spl0_29
| ~ spl0_50
| spl0_98 ),
inference(sat_conversion,[],[f2537]) ).
cnf(s223,plain,
( ~ spl0_20
| spl0_40
| ~ spl0_58 ),
inference(sat_conversion,[],[f2541]) ).
cnf(s225,plain,
( ~ spl0_7
| ~ spl0_17
| ~ spl0_35
| ~ spl0_60
| spl0_124 ),
inference(sat_conversion,[],[f2543]) ).
cnf(s229,plain,
( ~ spl0_29
| spl0_34
| ~ spl0_35
| ~ spl0_42 ),
inference(sat_conversion,[],[f2546]) ).
cnf(s234,plain,
( ~ spl0_51
| ~ spl0_98
| spl0_107 ),
inference(sat_conversion,[],[f2594]) ).
cnf(s235,plain,
( ~ spl0_42
| ~ spl0_81
| spl0_108 ),
inference(sat_conversion,[],[f2599]) ).
cnf(s236,plain,
( ~ spl0_13
| ~ spl0_24
| ~ spl0_48
| spl0_124 ),
inference(sat_conversion,[],[f2600]) ).
cnf(s237,plain,
( ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16
| spl0_42 ),
inference(sat_conversion,[],[f2601]) ).
cnf(s249,plain,
( ~ spl0_24
| spl0_63
| ~ spl0_89 ),
inference(sat_conversion,[],[f2606]) ).
cnf(s250,plain,
( ~ spl0_10
| ~ spl0_15
| ~ spl0_16
| spl0_72 ),
inference(sat_conversion,[],[f2607]) ).
cnf(s259,plain,
( ~ spl0_1
| spl0_59
| ~ spl0_60
| ~ spl0_98
| ~ spl0_107 ),
inference(sat_conversion,[],[f2614]) ).
cnf(s263,plain,
spl0_5,
inference(rat,[],[s73,s27,s28,s29,s30,s31,s32]) ).
cnf(s264,plain,
( spl0_7
| ~ spl0_4 ),
inference(rat,[],[s129,s127,s178,s123,s119,s97,s115,s250,s237,s6,s9,s10,s11,s12,s110,s263]) ).
cnf(s265,plain,
( ~ spl0_7
| ~ spl0_4 ),
inference(rat,[],[s129,s127,s178,s123,s119,s97,s115,s250,s237,s16,s19,s20,s21,s22,s92,s263,s110]) ).
cnf(s266,plain,
~ spl0_4,
inference(rat,[],[s265,s264]) ).
cnf(s268,plain,
( spl0_16
| ~ spl0_3 ),
inference(rat,[],[s91,s62,s72]) ).
cnf(s269,plain,
( ~ spl0_16
| ~ spl0_3 ),
inference(rat,[],[s91,s61,s71,s80]) ).
cnf(s270,plain,
~ spl0_3,
inference(rat,[],[s269,s268]) ).
cnf(s271,plain,
( spl0_16
| ~ spl0_2 ),
inference(rat,[],[s143,s42,s52]) ).
cnf(s272,plain,
( ~ spl0_13
| ~ spl0_24
| ~ spl0_7
| ~ spl0_15
| ~ spl0_2 ),
inference(rat,[],[s20,s113,s237,s153,s161,s271,s263]) ).
cnf(s273,plain,
( spl0_13
| ~ spl0_2 ),
inference(rat,[],[s143,s39,s49]) ).
cnf(s274,plain,
( spl0_72
| ~ spl0_15
| ~ spl0_16 ),
inference(rat,[],[s116,s56,s66,s250,s110]) ).
cnf(s275,plain,
( ~ spl0_15
| ~ spl0_2 ),
inference(rat,[],[s237,s153,s10,s161,s272,s119,s274,s271,s273]) ).
cnf(s276,plain,
~ spl0_2,
inference(rat,[],[s143,s41,s51,s275]) ).
cnf(s277,plain,
spl0_1,
inference(rat,[],[s2,s266,s263,s270,s276]) ).
cnf(s278,plain,
( spl0_14
| ~ spl0_13
| ~ spl0_7
| ~ spl0_24 ),
inference(rat,[],[s179,s178,s181,s129,s127,s123,s115,s113,s20,s110,s263]) ).
cnf(s279,plain,
( ~ spl0_40
| ~ spl0_124
| ~ spl0_108
| ~ spl0_42
| ~ spl0_24 ),
inference(rat,[],[s259,s216,s234,s168,s167,s166,s218,s229,s135,s129,s127,s133,s249,s182,s123,s115,s277,s263]) ).
cnf(s280,plain,
( ~ spl0_13
| ~ spl0_7
| ~ spl0_16
| ~ spl0_15 ),
inference(rat,[],[s131,s279,s236,s178,s129,s235,s127,s165,s123,s115,s237,s278,s161,s119,s274,s110,s263]) ).
cnf(s281,plain,
( ~ spl0_7
| ~ spl0_16
| ~ spl0_15 ),
inference(rat,[],[s216,s235,s157,s225,s165,s133,s162,s249,s223,s127,s182,s123,s115,s113,s19,s59,s280,s119,s274,s277,s263]) ).
cnf(s282,plain,
( ~ spl0_16
| ~ spl0_15 ),
inference(rat,[],[s236,s279,s178,s235,s131,s129,s165,s127,s123,s115,s161,s237,s9,s10,s281,s119,s274,s263,s110]) ).
cnf(s283,plain,
spl0_16,
inference(rat,[],[s216,s235,s157,s225,s165,s133,s162,s249,s223,s127,s182,s123,s115,s119,s113,s116,s12,s22,s62,s72,s277,s263,s110]) ).
cnf(s284,plain,
~ spl0_15,
inference(rat,[],[s282,s283]) ).
cnf(s285,plain,
spl0_21,
inference(rat,[],[s71,s284]) ).
cnf(s286,plain,
spl0_20,
inference(rat,[],[s61,s284]) ).
cnf(s289,plain,
spl0_17,
inference(rat,[],[s21,s284]) ).
cnf(s290,plain,
spl0_7,
inference(rat,[],[s11,s284]) ).
cnf(s291,plain,
spl0_72,
inference(rat,[],[s116,s285,s110,s286]) ).
cnf(s292,plain,
spl0_42,
inference(rat,[],[s113,s290,s263,s289]) ).
cnf(s294,plain,
spl0_24,
inference(rat,[],[s119,s291]) ).
cnf(s296,plain,
spl0_33,
inference(rat,[],[s115,s263,s292]) ).
cnf(s300,plain,
spl0_58,
inference(rat,[],[s123,s294,s296]) ).
cnf(s304,plain,
spl0_89,
inference(rat,[],[s182,s300]) ).
cnf(s305,plain,
spl0_35,
inference(rat,[],[s127,s294,s300]) ).
cnf(s306,plain,
spl0_40,
inference(rat,[],[s223,s286,s300]) ).
cnf(s307,plain,
spl0_63,
inference(rat,[],[s249,s294,s304]) ).
cnf(s310,plain,
spl0_88,
inference(rat,[],[s162,s305,s306]) ).
cnf(s312,plain,
spl0_60,
inference(rat,[],[s133,s292,s307]) ).
cnf(s318,plain,
spl0_81,
inference(rat,[],[s165,s300,s310]) ).
cnf(s323,plain,
spl0_124,
inference(rat,[],[s225,s305,s289,s290,s312]) ).
cnf(s324,plain,
spl0_59,
inference(rat,[],[s157,s289,s290,s277,s312]) ).
cnf(s328,plain,
spl0_108,
inference(rat,[],[s235,s292,s318]) ).
cnf(s333,plain,
$false,
inference(rat,[],[s216,s328,s306,s323,s324]) ).
fof(f2615,plain,
$false,
inference(avatar_sat_refutation,[],[s333]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP258-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.39 % Computer : n009.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 09:43:30 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.42 Running first-order model finding
% 0.13/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/0.50 % (1783138)Will run a generic schedule for satisfiability detection.
% 0.42/0.50 % (1783149)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3889985152:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.42/0.50 % (1783144)% WARNING: option uhcvi not known.
% 0.42/0.50 % (1783143)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3827854411_2999 on theBenchmark for (2999ds/0Mi)
% 0.42/0.50 % (1783144)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=577061099:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.42/0.50 % (1783146)dis+10_1_sil=32000:sp=arity:random_seed=3694226693:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.42/0.50 % (1783147)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1514524917:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.42/0.50 % (1783145)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3796769594:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.42/0.50 % TRYING [1]
% 0.42/0.50 % TRYING [2]
% 0.42/0.50 % (1783148)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1988855354:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.42/0.50 % TRYING [3]
% 0.42/0.50 % TRYING [4]
% 0.42/0.50 % (1783149) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1783138-1783149"...
% 0.42/0.50 % TRYING [5]
% 0.42/0.50 % (1783149)...printing done.
% 0.42/0.50 % (1783149)Refutation found. Thanks to Tanya!
% 0.42/0.50 % SZS status Unsatisfiable for theBenchmark
% 0.42/0.50 % SZS output start Proof for theBenchmark
% See solution above
% 0.42/0.50 % (1783149)------------------------------
% 0.42/0.50 % (1783149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.42/0.50 % (1783149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.42/0.50 % (1783149)CaDiCaL version: 2.1.3
% 0.42/0.50 % (1783149)Termination reason: Refutation
% 0.42/0.50 % (1783149)Time elapsed: 0.037 s
% 0.42/0.50 % (1783149)Peak memory usage: 13 MB
% 0.42/0.50 % (1783149)Instructions burned: 113 (million)
% 0.42/0.50 % (1783138)Success in time 0.067 s
% 0.42/0.50 % Vampire exiting
%------------------------------------------------------------------------------