%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP258-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:13:28 AM UTC 2026
% Result : Unsatisfiable 0.89s 0.82s
% Output : Refutation 2.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 84
% Syntax : Number of formulae : 566 ( 32 unt; 36 def)
% Number of atoms : 2057 ( 556 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 2875 (1384 ~;1455 |; 0 &)
% ( 36 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 38 ( 36 usr; 37 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 13 con; 0-2 aty)
% Number of variables : 81 ( 0 sgn 81 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',associativity) ).
fof(f9,negated_conjecture,
( multiply(sk_c1,sk_c12) = sk_c11
| multiply(sk_c5,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,negated_conjecture,
( multiply(sk_c1,sk_c12) = sk_c11
| inverse(sk_c5) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f11,plain,
( multiply(sk_c1,sk_c12) = sk_c11
| sk_c11 = inverse(sk_c5) ),
inference(reorient_equations,[],[f10]) ).
fof(f12,negated_conjecture,
( multiply(sk_c1,sk_c12) = sk_c11
| multiply(sk_c6,sk_c9) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f13,plain,
( multiply(sk_c1,sk_c12) = sk_c11
| sk_c12 = multiply(sk_c6,sk_c9) ),
inference(reorient_equations,[],[f12]) ).
fof(f14,negated_conjecture,
( multiply(sk_c1,sk_c12) = sk_c11
| inverse(sk_c6) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).
fof(f15,plain,
( multiply(sk_c1,sk_c12) = sk_c11
| sk_c9 = inverse(sk_c6) ),
inference(reorient_equations,[],[f14]) ).
fof(f27,negated_conjecture,
( inverse(sk_c1) = sk_c12
| multiply(sk_c5,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_13) ).
fof(f28,plain,
( sk_c12 = inverse(sk_c1)
| multiply(sk_c5,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f27]) ).
fof(f29,negated_conjecture,
( inverse(sk_c1) = sk_c12
| inverse(sk_c5) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_14) ).
fof(f30,plain,
( sk_c12 = inverse(sk_c1)
| sk_c11 = inverse(sk_c5) ),
inference(reorient_equations,[],[f29]) ).
fof(f31,negated_conjecture,
( inverse(sk_c1) = sk_c12
| multiply(sk_c6,sk_c9) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_15) ).
fof(f32,plain,
( sk_c12 = inverse(sk_c1)
| sk_c12 = multiply(sk_c6,sk_c9) ),
inference(reorient_equations,[],[f31]) ).
fof(f33,negated_conjecture,
( inverse(sk_c1) = sk_c12
| inverse(sk_c6) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_16) ).
fof(f34,plain,
( sk_c12 = inverse(sk_c1)
| sk_c9 = inverse(sk_c6) ),
inference(reorient_equations,[],[f33]) ).
fof(f47,negated_conjecture,
( multiply(sk_c2,sk_c11) = sk_c10
| multiply(sk_c5,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_23) ).
fof(f48,plain,
( sk_c10 = multiply(sk_c2,sk_c11)
| multiply(sk_c5,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f47]) ).
fof(f49,negated_conjecture,
( multiply(sk_c2,sk_c11) = sk_c10
| inverse(sk_c5) = sk_c11 ),
file('/export/starexec/sandbox/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(f51,negated_conjecture,
( multiply(sk_c2,sk_c11) = sk_c10
| multiply(sk_c6,sk_c9) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_25) ).
fof(f52,plain,
( sk_c10 = multiply(sk_c2,sk_c11)
| sk_c12 = multiply(sk_c6,sk_c9) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( multiply(sk_c2,sk_c11) = sk_c10
| inverse(sk_c6) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).
fof(f54,plain,
( sk_c10 = multiply(sk_c2,sk_c11)
| sk_c9 = inverse(sk_c6) ),
inference(reorient_equations,[],[f53]) ).
fof(f63,negated_conjecture,
( inverse(sk_c2) = sk_c11
| multiply(sk_c4,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',prove_this_32) ).
fof(f66,plain,
( sk_c11 = inverse(sk_c2)
| sk_c12 = inverse(sk_c4) ),
inference(reorient_equations,[],[f65]) ).
fof(f67,negated_conjecture,
( inverse(sk_c2) = sk_c11
| multiply(sk_c5,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_33) ).
fof(f68,plain,
( sk_c11 = inverse(sk_c2)
| multiply(sk_c5,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f67]) ).
fof(f69,negated_conjecture,
( inverse(sk_c2) = sk_c11
| inverse(sk_c5) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_34) ).
fof(f70,plain,
( sk_c11 = inverse(sk_c2)
| sk_c11 = inverse(sk_c5) ),
inference(reorient_equations,[],[f69]) ).
fof(f71,negated_conjecture,
( inverse(sk_c2) = sk_c11
| multiply(sk_c6,sk_c9) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_35) ).
fof(f72,plain,
( sk_c11 = inverse(sk_c2)
| sk_c12 = multiply(sk_c6,sk_c9) ),
inference(reorient_equations,[],[f71]) ).
fof(f73,negated_conjecture,
( inverse(sk_c2) = sk_c11
| inverse(sk_c6) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_36) ).
fof(f74,plain,
( sk_c11 = inverse(sk_c2)
| sk_c9 = inverse(sk_c6) ),
inference(reorient_equations,[],[f73]) ).
fof(f83,negated_conjecture,
( multiply(sk_c10,sk_c12) = sk_c11
| multiply(sk_c4,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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(f111,negated_conjecture,
( multiply(sk_c3,sk_c10) = sk_c12
| multiply(sk_c6,sk_c9) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_55) ).
fof(f112,plain,
( sk_c12 = multiply(sk_c3,sk_c10)
| sk_c12 = multiply(sk_c6,sk_c9) ),
inference(reorient_equations,[],[f111]) ).
fof(f113,negated_conjecture,
( multiply(sk_c3,sk_c10) = sk_c12
| inverse(sk_c6) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_56) ).
fof(f114,plain,
( sk_c12 = multiply(sk_c3,sk_c10)
| sk_c9 = inverse(sk_c6) ),
inference(reorient_equations,[],[f113]) ).
fof(f115,negated_conjecture,
( multiply(sk_c3,sk_c10) = sk_c12
| multiply(sk_c9,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox/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(f117,negated_conjecture,
( multiply(sk_c3,sk_c10) = sk_c12
| inverse(sk_c8) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_58) ).
fof(f118,plain,
( sk_c12 = multiply(sk_c3,sk_c10)
| inverse(sk_c8) = sk_c7 ),
inference(reorient_equations,[],[f117]) ).
fof(f119,negated_conjecture,
( multiply(sk_c3,sk_c10) = sk_c12
| inverse(sk_c7) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_59) ).
fof(f120,plain,
( sk_c12 = multiply(sk_c3,sk_c10)
| sk_c9 = inverse(sk_c7) ),
inference(reorient_equations,[],[f119]) ).
fof(f121,negated_conjecture,
( multiply(sk_c3,sk_c10) = sk_c12
| multiply(sk_c8,sk_c9) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_60) ).
fof(f122,plain,
( sk_c12 = multiply(sk_c3,sk_c10)
| sk_c7 = multiply(sk_c8,sk_c9) ),
inference(reorient_equations,[],[f121]) ).
fof(f123,negated_conjecture,
( inverse(sk_c3) = sk_c10
| multiply(sk_c4,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',prove_this_64) ).
fof(f130,plain,
( sk_c10 = inverse(sk_c3)
| sk_c11 = inverse(sk_c5) ),
inference(reorient_equations,[],[f129]) ).
fof(f131,negated_conjecture,
( inverse(sk_c3) = sk_c10
| multiply(sk_c6,sk_c9) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_65) ).
fof(f132,plain,
( sk_c10 = inverse(sk_c3)
| sk_c12 = multiply(sk_c6,sk_c9) ),
inference(reorient_equations,[],[f131]) ).
fof(f133,negated_conjecture,
( inverse(sk_c3) = sk_c10
| inverse(sk_c6) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_66) ).
fof(f134,plain,
( sk_c10 = inverse(sk_c3)
| sk_c9 = inverse(sk_c6) ),
inference(reorient_equations,[],[f133]) ).
fof(f135,negated_conjecture,
( inverse(sk_c3) = sk_c10
| multiply(sk_c9,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox/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(f137,negated_conjecture,
( inverse(sk_c3) = sk_c10
| inverse(sk_c8) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_68) ).
fof(f138,plain,
( sk_c10 = inverse(sk_c3)
| inverse(sk_c8) = sk_c7 ),
inference(reorient_equations,[],[f137]) ).
fof(f139,negated_conjecture,
( inverse(sk_c3) = sk_c10
| inverse(sk_c7) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_69) ).
fof(f140,plain,
( sk_c10 = inverse(sk_c3)
| sk_c9 = inverse(sk_c7) ),
inference(reorient_equations,[],[f139]) ).
fof(f141,negated_conjecture,
( inverse(sk_c3) = sk_c10
| multiply(sk_c8,sk_c9) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_70) ).
fof(f142,plain,
( sk_c10 = inverse(sk_c3)
| sk_c7 = multiply(sk_c8,sk_c9) ),
inference(reorient_equations,[],[f141]) ).
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/sandbox/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_c12 != multiply(X2,sk_c10)
| sk_c10 != inverse(X2) )
| ~ 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(f165,definition,
( spl0_6
<=> sk_c7 = multiply(sk_c8,sk_c9) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f167,plain,
( sk_c7 = multiply(sk_c8,sk_c9)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f165]) ).
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(f172,plain,
( spl0_6
| spl0_7 ),
inference(avatar_split_clause,[],[f142,f169,f165]) ).
fof(f174,definition,
( spl0_8
<=> sk_c9 = inverse(sk_c7) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f176,plain,
( sk_c9 = inverse(sk_c7)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f174]) ).
fof(f177,plain,
( spl0_8
| spl0_7 ),
inference(avatar_split_clause,[],[f140,f169,f174]) ).
fof(f179,definition,
( spl0_9
<=> inverse(sk_c8) = sk_c7 ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f181,plain,
( inverse(sk_c8) = sk_c7
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f179]) ).
fof(f182,plain,
( spl0_9
| spl0_7 ),
inference(avatar_split_clause,[],[f138,f169,f179]) ).
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(f192,plain,
( spl0_11
| spl0_7 ),
inference(avatar_split_clause,[],[f134,f169,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(f197,plain,
( spl0_12
| spl0_7 ),
inference(avatar_split_clause,[],[f132,f169,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(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(f222,plain,
( spl0_6
| spl0_17 ),
inference(avatar_split_clause,[],[f122,f219,f165]) ).
fof(f223,plain,
( spl0_8
| spl0_17 ),
inference(avatar_split_clause,[],[f120,f219,f174]) ).
fof(f224,plain,
( spl0_9
| spl0_17 ),
inference(avatar_split_clause,[],[f118,f219,f179]) ).
fof(f225,plain,
( spl0_10
| spl0_17 ),
inference(avatar_split_clause,[],[f116,f219,f184]) ).
fof(f226,plain,
( spl0_11
| spl0_17 ),
inference(avatar_split_clause,[],[f114,f219,f189]) ).
fof(f227,plain,
( spl0_12
| spl0_17 ),
inference(avatar_split_clause,[],[f112,f219,f194]) ).
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(f245,plain,
( sk_c11 = inverse(sk_c2)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f250,plain,
( spl0_11
| spl0_18 ),
inference(avatar_split_clause,[],[f74,f243,f189]) ).
fof(f251,plain,
( spl0_12
| spl0_18 ),
inference(avatar_split_clause,[],[f72,f243,f194]) ).
fof(f252,plain,
( spl0_13
| spl0_18 ),
inference(avatar_split_clause,[],[f70,f243,f199]) ).
fof(f253,plain,
( spl0_14
| spl0_18 ),
inference(avatar_split_clause,[],[f68,f243,f204]) ).
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(f264,plain,
( spl0_11
| spl0_19 ),
inference(avatar_split_clause,[],[f54,f257,f189]) ).
fof(f265,plain,
( spl0_12
| spl0_19 ),
inference(avatar_split_clause,[],[f52,f257,f194]) ).
fof(f266,plain,
( spl0_13
| spl0_19 ),
inference(avatar_split_clause,[],[f50,f257,f199]) ).
fof(f267,plain,
( spl0_14
| spl0_19 ),
inference(avatar_split_clause,[],[f48,f257,f204]) ).
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(f278,plain,
( spl0_11
| spl0_20 ),
inference(avatar_split_clause,[],[f34,f271,f189]) ).
fof(f279,plain,
( spl0_12
| spl0_20 ),
inference(avatar_split_clause,[],[f32,f271,f194]) ).
fof(f280,plain,
( spl0_13
| spl0_20 ),
inference(avatar_split_clause,[],[f30,f271,f199]) ).
fof(f281,plain,
( spl0_14
| spl0_20 ),
inference(avatar_split_clause,[],[f28,f271,f204]) ).
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(f292,plain,
( spl0_11
| spl0_21 ),
inference(avatar_split_clause,[],[f15,f285,f189]) ).
fof(f293,plain,
( spl0_12
| spl0_21 ),
inference(avatar_split_clause,[],[f13,f285,f194]) ).
fof(f294,plain,
( spl0_13
| spl0_21 ),
inference(avatar_split_clause,[],[f11,f285,f199]) ).
fof(f295,plain,
( spl0_14
| spl0_21 ),
inference(avatar_split_clause,[],[f9,f285,f204]) ).
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(f307,plain,
( ! [X0] : multiply(sk_c5,multiply(sk_c11,X0)) = multiply(sk_c10,X0)
| ~ spl0_14 ),
inference(superposition,[],[f4,f206]) ).
fof(f311,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(forward_demodulation,[],[f305,f1]) ).
fof(f314,plain,
( ! [X0] : multiply(identity,X0) = multiply(sk_c12,multiply(sk_c4,X0))
| ~ spl0_15 ),
inference(superposition,[],[f4,f298]) ).
fof(f315,plain,
( ! [X0] : multiply(sk_c12,multiply(sk_c4,X0)) = X0
| ~ spl0_15 ),
inference(forward_demodulation,[],[f314,f1]) ).
fof(f328,plain,
( sk_c12 = multiply(sk_c12,sk_c11)
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f315,f216]) ).
fof(f333,plain,
( multiply(sk_c10,sk_c5) = multiply(sk_c5,identity)
| ~ spl0_13
| ~ spl0_14 ),
inference(superposition,[],[f307,f299]) ).
fof(f375,plain,
( sk_c4 = multiply(inverse(sk_c12),identity)
| ~ spl0_15 ),
inference(superposition,[],[f311,f298]) ).
fof(f377,plain,
( sk_c11 = multiply(inverse(sk_c12),sk_c12)
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f311,f328]) ).
fof(f378,plain,
( sk_c5 = multiply(inverse(sk_c11),identity)
| ~ spl0_13 ),
inference(superposition,[],[f311,f299]) ).
fof(f382,plain,
( sk_c11 = multiply(inverse(sk_c5),sk_c10)
| ~ spl0_14 ),
inference(superposition,[],[f311,f206]) ).
fof(f385,plain,
( sk_c9 = multiply(inverse(sk_c6),sk_c12)
| ~ spl0_12 ),
inference(superposition,[],[f311,f196]) ).
fof(f389,plain,
( sk_c11 = multiply(inverse(sk_c9),sk_c12)
| ~ spl0_10 ),
inference(superposition,[],[f311,f186]) ).
fof(f390,plain,
( sk_c6 = multiply(inverse(sk_c9),identity)
| ~ spl0_11 ),
inference(superposition,[],[f311,f300]) ).
fof(f402,plain,
( sk_c9 = multiply(sk_c9,sk_c12)
| ~ spl0_11
| ~ spl0_12 ),
inference(forward_demodulation,[],[f385,f191]) ).
fof(f405,plain,
( sk_c11 = multiply(sk_c11,sk_c10)
| ~ spl0_13
| ~ spl0_14 ),
inference(forward_demodulation,[],[f382,f201]) ).
fof(f409,plain,
( identity = sk_c11
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f377,f3]) ).
fof(f423,plain,
( sk_c12 = multiply(inverse(sk_c9),sk_c9)
| ~ spl0_11
| ~ spl0_12 ),
inference(superposition,[],[f311,f402]) ).
fof(f425,plain,
( identity = sk_c12
| ~ spl0_11
| ~ spl0_12 ),
inference(forward_demodulation,[],[f423,f3]) ).
fof(f428,plain,
( sk_c12 = sk_c11
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f425,f409]) ).
fof(f433,plain,
( sk_c10 = multiply(inverse(sk_c11),sk_c11)
| ~ spl0_13
| ~ spl0_14 ),
inference(superposition,[],[f311,f405]) ).
fof(f435,plain,
( identity = sk_c10
| ~ spl0_13
| ~ spl0_14 ),
inference(forward_demodulation,[],[f433,f3]) ).
fof(f438,plain,
( sk_c11 = sk_c10
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f435,f409]) ).
fof(f441,plain,
( sk_c11 != multiply(sk_c11,sk_c12)
| spl0_5
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f162,f438]) ).
fof(f442,plain,
( sk_c4 = multiply(inverse(sk_c12),sk_c11)
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f375,f409]) ).
fof(f461,plain,
( sk_c5 = multiply(inverse(sk_c11),sk_c11)
| ~ spl0_13
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f378,f409]) ).
fof(f462,plain,
( identity = sk_c5
| ~ spl0_13
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f461,f3]) ).
fof(f463,plain,
( sk_c11 = sk_c5
| ~ spl0_13
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f462,f409]) ).
fof(f464,plain,
( sk_c12 = sk_c5
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f463,f428]) ).
fof(f477,plain,
( sk_c12 = multiply(inverse(sk_c9),sk_c12)
| ~ spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f389,f428]) ).
fof(f485,plain,
( sk_c6 = multiply(inverse(sk_c9),sk_c11)
| ~ spl0_11
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f390,f409]) ).
fof(f486,plain,
( sk_c6 = multiply(inverse(sk_c9),sk_c12)
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f485,f428]) ).
fof(f489,plain,
( sk_c4 = multiply(inverse(sk_c12),sk_c12)
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f442,f428]) ).
fof(f490,plain,
( identity = sk_c4
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f489,f3]) ).
fof(f491,plain,
( sk_c11 = sk_c4
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f490,f409]) ).
fof(f492,plain,
( sk_c12 = sk_c4
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f491,f428]) ).
fof(f497,plain,
( sk_c12 = inverse(sk_c12)
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f211,f492]) ).
fof(f508,plain,
( sk_c12 = sk_c6
| ~ spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f486,f477]) ).
fof(f511,plain,
( identity = multiply(sk_c9,sk_c12)
| ~ spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f300,f508]) ).
fof(f514,plain,
( identity = sk_c9
| ~ spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f511,f402]) ).
fof(f515,plain,
( sk_c11 = sk_c9
| ~ spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f514,f409]) ).
fof(f516,plain,
( sk_c12 = sk_c9
| ~ spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f515,f428]) ).
fof(f530,plain,
( sk_c7 = multiply(sk_c8,sk_c12)
| ~ spl0_6
| ~ spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f167,f516]) ).
fof(f533,plain,
( identity = multiply(sk_c12,sk_c6)
| ~ spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f300,f516]) ).
fof(f545,plain,
( identity = multiply(sk_c12,sk_c12)
| ~ spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f533,f508]) ).
fof(f549,plain,
( sk_c11 = multiply(sk_c12,sk_c12)
| ~ spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f545,f409]) ).
fof(f552,plain,
( sk_c12 = multiply(sk_c12,sk_c12)
| ~ spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f549,f428]) ).
fof(f570,plain,
( multiply(sk_c5,sk_c11) = multiply(sk_c10,sk_c5)
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f333,f409]) ).
fof(f571,plain,
( multiply(sk_c10,sk_c12) = multiply(sk_c12,sk_c11)
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f570,f464]) ).
fof(f572,plain,
( sk_c12 = multiply(sk_c10,sk_c12)
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f571,f328]) ).
fof(f573,plain,
( sk_c12 = multiply(sk_c11,sk_c12)
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f572,f438]) ).
fof(f574,plain,
( sk_c12 = multiply(sk_c12,sk_c12)
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f573,f428]) ).
fof(f661,plain,
( sk_c12 != multiply(sk_c12,sk_c12)
| spl0_5
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f441,f428]) ).
fof(f662,plain,
( $false
| spl0_5
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f661,f574]) ).
fof(f663,plain,
( spl0_5
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f662]) ).
fof(f664,plain,
( ! [X3] :
( sk_c12 != inverse(X3)
| sk_c12 != multiply(X3,sk_c12) )
| ~ spl0_3
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f155,f428]) ).
fof(f669,plain,
( sk_c12 != sk_c12
| sk_c12 != multiply(sk_c4,sk_c12)
| ~ spl0_3
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(superposition,[],[f664,f211]) ).
fof(f674,plain,
( sk_c12 != multiply(sk_c4,sk_c12)
| ~ spl0_3
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(trivial_inequality_removal,[],[f669]) ).
fof(f680,plain,
( sk_c12 != sk_c11
| ~ spl0_3
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f674,f216]) ).
fof(f689,plain,
( $false
| ~ spl0_3
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f680,f428]) ).
fof(f690,plain,
( ~ spl0_3
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f689]) ).
fof(f729,plain,
( identity = multiply(sk_c11,sk_c2)
| ~ spl0_18 ),
inference(superposition,[],[f3,f245]) ).
fof(f740,plain,
( sk_c12 = multiply(inverse(sk_c1),sk_c11)
| ~ spl0_21 ),
inference(superposition,[],[f311,f287]) ).
fof(f742,plain,
( sk_c12 = multiply(sk_c12,sk_c11)
| ~ spl0_20
| ~ spl0_21 ),
inference(forward_demodulation,[],[f740,f273]) ).
fof(f817,plain,
( identity = multiply(sk_c10,sk_c3)
| ~ spl0_7 ),
inference(superposition,[],[f3,f171]) ).
fof(f818,plain,
( sk_c10 = multiply(sk_c10,sk_c3)
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14 ),
inference(forward_demodulation,[],[f817,f435]) ).
fof(f821,plain,
( sk_c10 = multiply(inverse(sk_c3),sk_c12)
| ~ spl0_17 ),
inference(superposition,[],[f311,f221]) ).
fof(f823,plain,
( sk_c10 = multiply(sk_c10,sk_c12)
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f821,f171]) ).
fof(f824,plain,
( sk_c11 = sk_c10
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f823,f161]) ).
fof(f825,plain,
( sk_c11 = multiply(inverse(sk_c2),sk_c10)
| ~ spl0_19 ),
inference(superposition,[],[f311,f259]) ).
fof(f827,plain,
( sk_c11 = multiply(sk_c11,sk_c10)
| ~ spl0_18
| ~ spl0_19 ),
inference(forward_demodulation,[],[f825,f245]) ).
fof(f831,plain,
( sk_c12 != sk_c11
| sk_c12 != inverse(identity)
| ~ spl0_3 ),
inference(superposition,[],[f155,f1]) ).
fof(f834,plain,
( sk_c11 != sk_c11
| sk_c12 != inverse(sk_c1)
| ~ spl0_3
| ~ spl0_21 ),
inference(superposition,[],[f155,f287]) ).
fof(f839,plain,
( sk_c12 != inverse(sk_c1)
| ~ spl0_3
| ~ spl0_21 ),
inference(trivial_inequality_removal,[],[f834]) ).
fof(f841,plain,
( $false
| ~ spl0_3
| ~ spl0_20
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f839,f273]) ).
fof(f842,plain,
( ~ spl0_3
| ~ spl0_20
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f841]) ).
fof(f844,plain,
( sk_c12 != inverse(sk_c10)
| sk_c12 != sk_c11
| ~ spl0_3
| ~ spl0_13
| ~ spl0_14 ),
inference(forward_demodulation,[],[f831,f435]) ).
fof(f846,plain,
( sk_c12 != inverse(sk_c11)
| sk_c12 != sk_c11
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_demodulation,[],[f844,f824]) ).
fof(f848,definition,
( spl0_22
<=> sk_c12 = sk_c11 ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f849,plain,
( sk_c12 = sk_c11
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f848]) ).
fof(f852,definition,
( spl0_23
<=> sk_c12 = inverse(sk_c11) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f854,plain,
( sk_c12 != inverse(sk_c11)
| spl0_23 ),
inference(avatar_component_clause,[],[f852]) ).
fof(f855,plain,
( ~ spl0_22
| ~ spl0_23
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f846,f219,f204,f199,f169,f160,f154,f852,f848]) ).
fof(f856,plain,
( sk_c10 = multiply(sk_c11,sk_c2)
| ~ spl0_13
| ~ spl0_14
| ~ spl0_18 ),
inference(forward_demodulation,[],[f729,f435]) ).
fof(f857,plain,
( sk_c11 = multiply(sk_c11,sk_c2)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f856,f824]) ).
fof(f896,definition,
( spl0_29
<=> ! [X0] :
( inverse(X0) != multiply(X0,sk_c12)
| sk_c12 != inverse(inverse(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f897,plain,
( ! [X0] :
( sk_c12 != inverse(inverse(X0))
| inverse(X0) != multiply(X0,sk_c12) )
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f896]) ).
fof(f899,definition,
( spl0_30
<=> sk_c12 = multiply(sk_c12,sk_c11) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f900,plain,
( sk_c12 = multiply(sk_c12,sk_c11)
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f899]) ).
fof(f913,definition,
( spl0_33
<=> ! [X0] :
( inverse(X0) != multiply(X0,sk_c11)
| sk_c11 != inverse(inverse(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f914,plain,
( ! [X0] :
( sk_c11 != inverse(inverse(X0))
| inverse(X0) != multiply(X0,sk_c11) )
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f913]) ).
fof(f916,definition,
( spl0_34
<=> sk_c12 = multiply(sk_c11,sk_c11) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f917,plain,
( sk_c12 = multiply(sk_c11,sk_c11)
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f916]) ).
fof(f925,plain,
( sk_c11 = multiply(sk_c11,sk_c3)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_demodulation,[],[f818,f824]) ).
fof(f928,plain,
( sk_c2 = multiply(inverse(sk_c11),sk_c11)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18 ),
inference(superposition,[],[f311,f857]) ).
fof(f930,plain,
( identity = sk_c2
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f928,f3]) ).
fof(f933,plain,
( sk_c10 = sk_c2
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f930,f435]) ).
fof(f935,plain,
( sk_c11 = sk_c2
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f933,f824]) ).
fof(f941,plain,
( sk_c11 = inverse(sk_c11)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18 ),
inference(superposition,[],[f245,f935]) ).
fof(f945,plain,
( sk_c3 = multiply(inverse(sk_c11),sk_c11)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17 ),
inference(superposition,[],[f311,f925]) ).
fof(f947,plain,
( identity = sk_c3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_demodulation,[],[f945,f3]) ).
fof(f950,plain,
( sk_c10 = sk_c3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_demodulation,[],[f947,f435]) ).
fof(f952,plain,
( sk_c11 = sk_c3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_demodulation,[],[f950,f824]) ).
fof(f954,plain,
( sk_c12 = multiply(sk_c11,sk_c10)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17 ),
inference(superposition,[],[f221,f952]) ).
fof(f957,plain,
( sk_c12 = multiply(sk_c11,sk_c11)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_demodulation,[],[f954,f824]) ).
fof(f960,plain,
( spl0_34
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f957,f219,f204,f199,f169,f160,f916]) ).
fof(f969,plain,
( identity = multiply(sk_c11,sk_c11)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18 ),
inference(superposition,[],[f3,f941]) ).
fof(f971,plain,
( identity = sk_c12
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18
| ~ spl0_34 ),
inference(forward_demodulation,[],[f969,f917]) ).
fof(f976,plain,
( sk_c11 != inverse(sk_c11)
| sk_c11 != multiply(sk_c5,sk_c11)
| ~ spl0_13
| ~ spl0_33 ),
inference(superposition,[],[f914,f201]) ).
fof(f979,plain,
( sk_c11 != inverse(sk_c11)
| sk_c11 != multiply(sk_c2,sk_c11)
| ~ spl0_18
| ~ spl0_33 ),
inference(superposition,[],[f914,f245]) ).
fof(f982,plain,
( sk_c11 != multiply(sk_c2,sk_c11)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f979,f941]) ).
fof(f993,plain,
( sk_c11 != multiply(sk_c5,sk_c11)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f976,f941]) ).
fof(f1005,plain,
( sk_c11 != sk_c10
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19
| ~ spl0_33 ),
inference(forward_demodulation,[],[f982,f259]) ).
fof(f1015,plain,
( sk_c11 != sk_c10
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18
| ~ spl0_33 ),
inference(forward_demodulation,[],[f993,f206]) ).
fof(f1018,plain,
( $false
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f1005,f824]) ).
fof(f1019,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19
| ~ spl0_33 ),
inference(avatar_contradiction_clause,[],[f1018]) ).
fof(f1020,plain,
( $false
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f1015,f824]) ).
fof(f1021,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18
| ~ spl0_33 ),
inference(avatar_contradiction_clause,[],[f1020]) ).
fof(f1024,plain,
( ! [X4] :
( sk_c11 != inverse(X4)
| sk_c11 != multiply(X4,sk_c11) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f152,f824]) ).
fof(f1025,plain,
( sk_c12 = sk_c10
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18
| ~ spl0_34 ),
inference(superposition,[],[f971,f435]) ).
fof(f1030,plain,
( sk_c11 != sk_c11
| sk_c11 != multiply(sk_c5,sk_c11)
| ~ spl0_2
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_17 ),
inference(superposition,[],[f1024,f201]) ).
fof(f1033,plain,
( sk_c11 != sk_c11
| sk_c11 != multiply(sk_c2,sk_c11)
| ~ spl0_2
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18 ),
inference(superposition,[],[f1024,f245]) ).
fof(f1035,plain,
( sk_c11 != multiply(sk_c2,sk_c11)
| ~ spl0_2
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18 ),
inference(trivial_inequality_removal,[],[f1033]) ).
fof(f1036,plain,
( sk_c11 != multiply(sk_c5,sk_c11)
| ~ spl0_2
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_17 ),
inference(trivial_inequality_removal,[],[f1030]) ).
fof(f1039,plain,
( sk_c11 != sk_c10
| ~ spl0_2
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1035,f259]) ).
fof(f1054,plain,
( sk_c11 != sk_c10
| ~ spl0_2
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1036,f206]) ).
fof(f1057,plain,
( $false
| ~ spl0_2
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1039,f824]) ).
fof(f1058,plain,
( ~ spl0_2
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f1057]) ).
fof(f1059,plain,
( $false
| ~ spl0_2
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1054,f824]) ).
fof(f1060,plain,
( ~ spl0_2
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f1059]) ).
fof(f1062,plain,
( ! [X2] :
( sk_c12 != multiply(X2,sk_c11)
| sk_c10 != inverse(X2) )
| ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f158,f824]) ).
fof(f1063,plain,
( ! [X2] :
( sk_c11 != inverse(X2)
| sk_c12 != multiply(X2,sk_c11) )
| ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1062,f824]) ).
fof(f1065,plain,
( sk_c12 = sk_c11
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18
| ~ spl0_34 ),
inference(superposition,[],[f824,f1025]) ).
fof(f1074,plain,
( spl0_22
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f1065,f916,f243,f219,f204,f199,f169,f160,f848]) ).
fof(f1080,plain,
( sk_c11 != sk_c11
| sk_c12 != multiply(sk_c2,sk_c11)
| ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18 ),
inference(superposition,[],[f1063,f245]) ).
fof(f1081,plain,
( sk_c11 != sk_c10
| sk_c12 != multiply(sk_c3,sk_c11)
| ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(superposition,[],[f1063,f171]) ).
fof(f1082,plain,
( sk_c12 != multiply(sk_c2,sk_c11)
| ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18 ),
inference(trivial_inequality_removal,[],[f1080]) ).
fof(f1085,plain,
( sk_c12 != multiply(sk_c3,sk_c11)
| ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1081,f824]) ).
fof(f1086,plain,
( sk_c12 != sk_c10
| ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1082,f259]) ).
fof(f1097,plain,
( sk_c12 != multiply(sk_c11,sk_c11)
| ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1085,f952]) ).
fof(f1102,plain,
( $false
| ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f1097,f917]) ).
fof(f1103,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_34 ),
inference(avatar_contradiction_clause,[],[f1102]) ).
fof(f1105,plain,
( identity = multiply(sk_c11,sk_c3)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f817,f824]) ).
fof(f1106,plain,
( sk_c11 = multiply(sk_c11,sk_c11)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19 ),
inference(forward_demodulation,[],[f827,f824]) ).
fof(f1107,plain,
( sk_c12 != sk_c11
| ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1086,f824]) ).
fof(f1108,plain,
( sk_c12 = sk_c11
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19
| ~ spl0_34 ),
inference(forward_demodulation,[],[f1106,f917]) ).
fof(f1109,plain,
( ~ spl0_22
| ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f1107,f257,f243,f219,f169,f160,f157,f848]) ).
fof(f1110,plain,
( spl0_22
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f1108,f916,f257,f243,f219,f169,f160,f848]) ).
fof(f1116,definition,
( spl0_45
<=> identity = sk_c12 ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f1117,plain,
( identity = sk_c12
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f1116]) ).
fof(f1127,definition,
( spl0_46
<=> sk_c11 = multiply(sk_c5,sk_c11) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f1129,plain,
( sk_c11 != multiply(sk_c5,sk_c11)
| spl0_46 ),
inference(avatar_component_clause,[],[f1127]) ).
fof(f1131,definition,
( spl0_47
<=> sk_c11 = inverse(sk_c11) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f1132,plain,
( sk_c11 = inverse(sk_c11)
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f1131]) ).
fof(f1133,plain,
( sk_c11 != inverse(sk_c11)
| spl0_47 ),
inference(avatar_component_clause,[],[f1131]) ).
fof(f1137,plain,
( sk_c11 != sk_c10
| sk_c11 != inverse(sk_c11)
| ~ spl0_18
| ~ spl0_19
| ~ spl0_33 ),
inference(forward_demodulation,[],[f979,f259]) ).
fof(f1154,plain,
( sk_c11 != inverse(sk_c11)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f1137,f824]) ).
fof(f1165,plain,
( ~ spl0_47
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f1154,f913,f257,f243,f219,f169,f160,f1131]) ).
fof(f1180,plain,
( ! [X7,X5] :
( sk_c12 != multiply(inverse(X5),sk_c12)
| inverse(X7) != multiply(X7,inverse(X5))
| inverse(X5) != inverse(inverse(X7))
| sk_c12 != multiply(X5,inverse(X5)) )
| ~ spl0_1
| ~ spl0_22 ),
inference(forward_demodulation,[],[f149,f849]) ).
fof(f1183,plain,
( ! [X0] :
( sk_c12 != multiply(sk_c11,sk_c12)
| inverse(X0) != multiply(X0,sk_c11)
| sk_c11 != inverse(inverse(X0))
| sk_c12 != multiply(sk_c5,sk_c11) )
| ~ spl0_1
| ~ spl0_13
| ~ spl0_22 ),
inference(superposition,[],[f1180,f201]) ).
fof(f1199,plain,
( ! [X0] :
( sk_c12 != multiply(sk_c12,sk_c12)
| inverse(X0) != multiply(X0,sk_c11)
| sk_c11 != inverse(inverse(X0))
| sk_c12 != multiply(sk_c5,sk_c11) )
| ~ spl0_1
| ~ spl0_13
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1183,f849]) ).
fof(f1203,plain,
( ! [X0] :
( inverse(X0) != multiply(X0,sk_c12)
| sk_c12 != multiply(sk_c12,sk_c12)
| sk_c11 != inverse(inverse(X0))
| sk_c12 != multiply(sk_c5,sk_c11) )
| ~ spl0_1
| ~ spl0_13
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1199,f849]) ).
fof(f1207,plain,
( ! [X0] :
( sk_c12 != inverse(inverse(X0))
| inverse(X0) != multiply(X0,sk_c12)
| sk_c12 != multiply(sk_c12,sk_c12)
| sk_c12 != multiply(sk_c5,sk_c11) )
| ~ spl0_1
| ~ spl0_13
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1203,f849]) ).
fof(f1209,definition,
( spl0_52
<=> sk_c12 = multiply(sk_c12,sk_c12) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f1215,plain,
( ! [X0] :
( sk_c12 != multiply(sk_c5,sk_c12)
| sk_c12 != inverse(inverse(X0))
| inverse(X0) != multiply(X0,sk_c12)
| sk_c12 != multiply(sk_c12,sk_c12) )
| ~ spl0_1
| ~ spl0_13
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1207,f849]) ).
fof(f1224,plain,
( sk_c12 != inverse(sk_c12)
| ~ spl0_22
| spl0_47 ),
inference(forward_demodulation,[],[f1133,f849]) ).
fof(f1231,plain,
( sk_c12 != inverse(sk_c7)
| sk_c7 != multiply(sk_c8,sk_c12)
| ~ spl0_9
| ~ spl0_29 ),
inference(superposition,[],[f897,f181]) ).
fof(f1237,plain,
( sk_c12 != sk_c9
| sk_c7 != multiply(sk_c8,sk_c12)
| ~ spl0_8
| ~ spl0_9
| ~ spl0_29 ),
inference(forward_demodulation,[],[f1231,f176]) ).
fof(f1254,plain,
( identity = multiply(sk_c12,sk_c3)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1105,f849]) ).
fof(f1281,plain,
( sk_c12 = multiply(sk_c12,sk_c3)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_22
| ~ spl0_45 ),
inference(forward_demodulation,[],[f1254,f1117]) ).
fof(f1283,plain,
( sk_c3 = multiply(inverse(sk_c12),sk_c12)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_22
| ~ spl0_45 ),
inference(superposition,[],[f311,f1281]) ).
fof(f1285,plain,
( identity = sk_c3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_22
| ~ spl0_45 ),
inference(forward_demodulation,[],[f1283,f3]) ).
fof(f1287,plain,
( sk_c12 = sk_c3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_22
| ~ spl0_45 ),
inference(forward_demodulation,[],[f1285,f1117]) ).
fof(f1291,plain,
( sk_c10 = inverse(sk_c12)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_22
| ~ spl0_45 ),
inference(superposition,[],[f171,f1287]) ).
fof(f1292,plain,
( sk_c11 = inverse(sk_c12)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_22
| ~ spl0_45 ),
inference(forward_demodulation,[],[f1291,f824]) ).
fof(f1294,plain,
( sk_c12 = inverse(sk_c12)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_22
| ~ spl0_45 ),
inference(forward_demodulation,[],[f1292,f849]) ).
fof(f1296,plain,
( $false
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_22
| ~ spl0_45
| spl0_47 ),
inference(forward_subsumption_resolution,[],[f1294,f1224]) ).
fof(f1297,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_22
| ~ spl0_45
| spl0_47 ),
inference(avatar_contradiction_clause,[],[f1296]) ).
fof(f1329,definition,
( spl0_57
<=> sk_c7 = multiply(sk_c8,sk_c12) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f1333,definition,
( spl0_58
<=> sk_c12 = sk_c9 ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f1336,plain,
( ~ spl0_57
| ~ spl0_58
| ~ spl0_8
| ~ spl0_9
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f1237,f896,f179,f174,f1333,f1329]) ).
fof(f1345,definition,
( spl0_59
<=> sk_c12 = inverse(sk_c12) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f1363,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(f1366,plain,
( ! [X0] :
( sk_c12 != multiply(sk_c10,sk_c11)
| inverse(X0) != multiply(X0,sk_c10)
| sk_c10 != inverse(inverse(X0)) )
| ~ spl0_1
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1363,f221]) ).
fof(f1370,plain,
( ! [X0] :
( sk_c12 != multiply(sk_c11,sk_c11)
| inverse(X0) != multiply(X0,sk_c10)
| sk_c10 != inverse(inverse(X0)) )
| ~ spl0_1
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1366,f824]) ).
fof(f1372,plain,
( ! [X0] :
( inverse(X0) != multiply(X0,sk_c11)
| sk_c12 != multiply(sk_c11,sk_c11)
| sk_c10 != inverse(inverse(X0)) )
| ~ spl0_1
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1370,f824]) ).
fof(f1374,plain,
( ! [X0] :
( sk_c11 != inverse(inverse(X0))
| inverse(X0) != multiply(X0,sk_c11)
| sk_c12 != multiply(sk_c11,sk_c11) )
| ~ spl0_1
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1372,f824]) ).
fof(f1375,plain,
( ~ spl0_34
| spl0_33
| ~ spl0_1
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f1374,f219,f169,f160,f148,f913,f916]) ).
fof(f1377,plain,
( sk_c11 = multiply(inverse(sk_c12),sk_c12)
| ~ spl0_30 ),
inference(superposition,[],[f311,f900]) ).
fof(f1379,plain,
( identity = sk_c11
| ~ spl0_30 ),
inference(forward_demodulation,[],[f1377,f3]) ).
fof(f1381,plain,
( sk_c12 = sk_c11
| ~ spl0_30
| ~ spl0_45 ),
inference(forward_demodulation,[],[f1379,f1117]) ).
fof(f1385,plain,
( sk_c11 != inverse(sk_c11)
| sk_c11 != multiply(sk_c5,sk_c11)
| ~ spl0_13
| ~ spl0_33 ),
inference(superposition,[],[f914,f201]) ).
fof(f1393,plain,
( ~ spl0_46
| ~ spl0_47
| ~ spl0_13
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f1385,f913,f199,f1131,f1127]) ).
fof(f1423,plain,
( spl0_30
| ~ spl0_20
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f742,f285,f271,f899]) ).
fof(f1433,plain,
( sk_c11 = multiply(sk_c11,sk_c2)
| ~ spl0_18
| ~ spl0_30 ),
inference(forward_demodulation,[],[f729,f1379]) ).
fof(f1434,plain,
( sk_c11 = multiply(sk_c11,sk_c3)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_30 ),
inference(forward_demodulation,[],[f1105,f1379]) ).
fof(f1436,plain,
( sk_c2 = multiply(inverse(sk_c11),sk_c11)
| ~ spl0_18
| ~ spl0_30 ),
inference(superposition,[],[f311,f1433]) ).
fof(f1438,plain,
( identity = sk_c2
| ~ spl0_18
| ~ spl0_30 ),
inference(forward_demodulation,[],[f1436,f3]) ).
fof(f1440,plain,
( sk_c11 = sk_c2
| ~ spl0_18
| ~ spl0_30 ),
inference(forward_demodulation,[],[f1438,f1379]) ).
fof(f1442,plain,
( sk_c3 = multiply(inverse(sk_c11),sk_c11)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_30 ),
inference(superposition,[],[f311,f1434]) ).
fof(f1444,plain,
( identity = sk_c3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_30 ),
inference(forward_demodulation,[],[f1442,f3]) ).
fof(f1446,plain,
( sk_c11 = sk_c3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_30 ),
inference(forward_demodulation,[],[f1444,f1379]) ).
fof(f1449,plain,
( sk_c11 = inverse(sk_c11)
| ~ spl0_18
| ~ spl0_30 ),
inference(superposition,[],[f245,f1440]) ).
fof(f1453,plain,
( spl0_47
| ~ spl0_18
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f1449,f899,f243,f1131]) ).
fof(f1455,plain,
( sk_c12 != sk_c11
| spl0_23
| ~ spl0_47 ),
inference(superposition,[],[f854,f1132]) ).
fof(f1463,plain,
( sk_c12 = multiply(sk_c11,sk_c10)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_30 ),
inference(superposition,[],[f221,f1446]) ).
fof(f1466,plain,
( sk_c12 = multiply(sk_c11,sk_c11)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_30 ),
inference(forward_demodulation,[],[f1463,f824]) ).
fof(f1469,plain,
( spl0_59
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f497,f214,f209,f194,f189,f1345]) ).
fof(f1503,plain,
( spl0_57
| ~ spl0_6
| ~ spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f530,f214,f209,f194,f189,f184,f165,f1329]) ).
fof(f1518,plain,
( sk_c11 = multiply(sk_c5,sk_c11)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_demodulation,[],[f206,f824]) ).
fof(f1563,plain,
( spl0_34
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f1466,f899,f219,f169,f160,f916]) ).
fof(f1566,plain,
( $false
| ~ spl0_5
| ~ spl0_7
| ~ spl0_14
| ~ spl0_17
| spl0_46 ),
inference(forward_subsumption_resolution,[],[f1518,f1129]) ).
fof(f1567,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_14
| ~ spl0_17
| spl0_46 ),
inference(avatar_contradiction_clause,[],[f1566]) ).
fof(f1586,definition,
( spl0_61
<=> sk_c12 = multiply(sk_c5,sk_c12) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f1589,plain,
( ~ spl0_52
| spl0_29
| ~ spl0_61
| ~ spl0_1
| ~ spl0_13
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f1215,f848,f199,f148,f1586,f896,f1209]) ).
fof(f1593,plain,
( spl0_22
| ~ spl0_30
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f1381,f1116,f899,f848]) ).
fof(f1594,plain,
( spl0_58
| ~ spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f516,f214,f209,f194,f189,f184,f1333]) ).
fof(f1599,plain,
( spl0_52
| ~ spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f552,f214,f209,f194,f189,f184,f1209]) ).
fof(f1608,plain,
( spl0_45
| ~ spl0_11
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f425,f194,f189,f1116]) ).
fof(f1612,plain,
( ~ spl0_22
| spl0_23
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f1455,f1131,f852,f848]) ).
fof(f1613,plain,
( spl0_22
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f428,f214,f209,f194,f189,f848]) ).
fof(f1627,definition,
( spl0_64
<=> sk_c12 = sk_c10 ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f1628,plain,
( sk_c12 = sk_c10
| ~ spl0_64 ),
inference(avatar_component_clause,[],[f1627]) ).
fof(f1629,plain,
( sk_c12 != sk_c10
| spl0_64 ),
inference(avatar_component_clause,[],[f1627]) ).
fof(f1709,plain,
( sk_c12 = multiply(sk_c5,sk_c11)
| ~ spl0_14
| ~ spl0_64 ),
inference(forward_demodulation,[],[f206,f1628]) ).
fof(f1710,plain,
( sk_c12 = multiply(sk_c5,sk_c12)
| ~ spl0_14
| ~ spl0_22
| ~ spl0_64 ),
inference(forward_demodulation,[],[f1709,f849]) ).
fof(f1711,plain,
( spl0_61
| ~ spl0_14
| ~ spl0_22
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f1710,f1627,f848,f204,f1586]) ).
fof(f1798,plain,
( ! [X4] :
( sk_c10 != multiply(X4,sk_c12)
| sk_c11 != inverse(X4) )
| ~ spl0_2
| ~ spl0_22 ),
inference(forward_demodulation,[],[f152,f849]) ).
fof(f1799,plain,
( ! [X4] :
( sk_c12 != multiply(X4,sk_c12)
| sk_c11 != inverse(X4) )
| ~ spl0_2
| ~ spl0_22
| ~ spl0_64 ),
inference(forward_demodulation,[],[f1798,f1628]) ).
fof(f1800,plain,
( ! [X4] :
( sk_c12 != multiply(X4,sk_c12)
| sk_c12 != inverse(X4) )
| ~ spl0_2
| ~ spl0_22
| ~ spl0_64 ),
inference(forward_demodulation,[],[f1799,f849]) ).
fof(f1806,plain,
( sk_c12 != sk_c11
| sk_c12 != inverse(sk_c10)
| ~ spl0_2
| ~ spl0_5
| ~ spl0_22
| ~ spl0_64 ),
inference(superposition,[],[f1800,f161]) ).
fof(f1810,plain,
( sk_c12 != inverse(sk_c10)
| ~ spl0_2
| ~ spl0_5
| ~ spl0_22
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f1806,f849]) ).
fof(f1814,plain,
( sk_c12 != inverse(sk_c12)
| ~ spl0_2
| ~ spl0_5
| ~ spl0_22
| ~ spl0_64 ),
inference(forward_demodulation,[],[f1810,f1628]) ).
fof(f1818,plain,
( ~ spl0_59
| ~ spl0_2
| ~ spl0_5
| ~ spl0_22
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f1814,f1627,f848,f160,f151,f1345]) ).
fof(f1821,plain,
( ! [X2] :
( sk_c12 != multiply(X2,sk_c12)
| sk_c10 != inverse(X2) )
| ~ spl0_4
| ~ spl0_64 ),
inference(forward_demodulation,[],[f158,f1628]) ).
fof(f1822,plain,
( ! [X2] :
( sk_c12 != multiply(X2,sk_c12)
| sk_c12 != inverse(X2) )
| ~ spl0_4
| ~ spl0_64 ),
inference(forward_demodulation,[],[f1821,f1628]) ).
fof(f1827,plain,
( sk_c12 != sk_c11
| sk_c12 != inverse(sk_c4)
| ~ spl0_4
| ~ spl0_16
| ~ spl0_64 ),
inference(superposition,[],[f1822,f216]) ).
fof(f1833,plain,
( sk_c12 != inverse(sk_c4)
| ~ spl0_4
| ~ spl0_16
| ~ spl0_22
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f1827,f849]) ).
fof(f1837,plain,
( $false
| ~ spl0_4
| ~ spl0_15
| ~ spl0_16
| ~ spl0_22
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f1833,f211]) ).
fof(f1838,plain,
( ~ spl0_4
| ~ spl0_15
| ~ spl0_16
| ~ spl0_22
| ~ spl0_64 ),
inference(avatar_contradiction_clause,[],[f1837]) ).
fof(f1845,plain,
( sk_c12 = sk_c10
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16
| ~ spl0_22 ),
inference(forward_demodulation,[],[f438,f849]) ).
fof(f1846,plain,
( $false
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16
| ~ spl0_22
| spl0_64 ),
inference(forward_subsumption_resolution,[],[f1845,f1629]) ).
fof(f1847,plain,
( ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16
| ~ spl0_22
| spl0_64 ),
inference(avatar_contradiction_clause,[],[f1846]) ).
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(s3,plain,
( spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f172]) ).
cnf(s4,plain,
( spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f177]) ).
cnf(s5,plain,
( spl0_7
| spl0_9 ),
inference(sat_conversion,[],[f182]) ).
cnf(s6,plain,
( spl0_7
| spl0_10 ),
inference(sat_conversion,[],[f187]) ).
cnf(s7,plain,
( spl0_7
| spl0_11 ),
inference(sat_conversion,[],[f192]) ).
cnf(s8,plain,
( spl0_7
| spl0_12 ),
inference(sat_conversion,[],[f197]) ).
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(s13,plain,
( spl0_6
| spl0_17 ),
inference(sat_conversion,[],[f222]) ).
cnf(s14,plain,
( spl0_8
| spl0_17 ),
inference(sat_conversion,[],[f223]) ).
cnf(s15,plain,
( spl0_9
| spl0_17 ),
inference(sat_conversion,[],[f224]) ).
cnf(s16,plain,
( spl0_10
| spl0_17 ),
inference(sat_conversion,[],[f225]) ).
cnf(s17,plain,
( spl0_11
| spl0_17 ),
inference(sat_conversion,[],[f226]) ).
cnf(s18,plain,
( spl0_12
| spl0_17 ),
inference(sat_conversion,[],[f227]) ).
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(s37,plain,
( spl0_11
| spl0_18 ),
inference(sat_conversion,[],[f250]) ).
cnf(s38,plain,
( spl0_12
| spl0_18 ),
inference(sat_conversion,[],[f251]) ).
cnf(s39,plain,
( spl0_13
| spl0_18 ),
inference(sat_conversion,[],[f252]) ).
cnf(s40,plain,
( spl0_14
| spl0_18 ),
inference(sat_conversion,[],[f253]) ).
cnf(s41,plain,
( spl0_15
| spl0_18 ),
inference(sat_conversion,[],[f254]) ).
cnf(s42,plain,
( spl0_16
| spl0_18 ),
inference(sat_conversion,[],[f255]) ).
cnf(s47,plain,
( spl0_11
| spl0_19 ),
inference(sat_conversion,[],[f264]) ).
cnf(s48,plain,
( spl0_12
| spl0_19 ),
inference(sat_conversion,[],[f265]) ).
cnf(s49,plain,
( spl0_13
| spl0_19 ),
inference(sat_conversion,[],[f266]) ).
cnf(s50,plain,
( spl0_14
| spl0_19 ),
inference(sat_conversion,[],[f267]) ).
cnf(s57,plain,
( spl0_11
| spl0_20 ),
inference(sat_conversion,[],[f278]) ).
cnf(s58,plain,
( spl0_12
| spl0_20 ),
inference(sat_conversion,[],[f279]) ).
cnf(s59,plain,
( spl0_13
| spl0_20 ),
inference(sat_conversion,[],[f280]) ).
cnf(s60,plain,
( spl0_14
| spl0_20 ),
inference(sat_conversion,[],[f281]) ).
cnf(s67,plain,
( spl0_11
| spl0_21 ),
inference(sat_conversion,[],[f292]) ).
cnf(s68,plain,
( spl0_12
| spl0_21 ),
inference(sat_conversion,[],[f293]) ).
cnf(s69,plain,
( spl0_13
| spl0_21 ),
inference(sat_conversion,[],[f294]) ).
cnf(s70,plain,
( spl0_14
| spl0_21 ),
inference(sat_conversion,[],[f295]) ).
cnf(s73,plain,
( spl0_5
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(sat_conversion,[],[f663]) ).
cnf(s76,plain,
( ~ spl0_3
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16 ),
inference(sat_conversion,[],[f690]) ).
cnf(s86,plain,
( ~ spl0_3
| ~ spl0_20
| ~ spl0_21 ),
inference(sat_conversion,[],[f842]) ).
cnf(s87,plain,
( ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_22
| ~ spl0_23 ),
inference(sat_conversion,[],[f855]) ).
cnf(s96,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| spl0_34 ),
inference(sat_conversion,[],[f960]) ).
cnf(s101,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19
| ~ spl0_33 ),
inference(sat_conversion,[],[f1019]) ).
cnf(s102,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18
| ~ spl0_33 ),
inference(sat_conversion,[],[f1021]) ).
cnf(s105,plain,
( ~ spl0_2
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19 ),
inference(sat_conversion,[],[f1058]) ).
cnf(s106,plain,
( ~ spl0_2
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17 ),
inference(sat_conversion,[],[f1060]) ).
cnf(s109,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18
| spl0_22
| ~ spl0_34 ),
inference(sat_conversion,[],[f1074]) ).
cnf(s117,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_17
| ~ spl0_34 ),
inference(sat_conversion,[],[f1103]) ).
cnf(s118,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19
| ~ spl0_22 ),
inference(sat_conversion,[],[f1109]) ).
cnf(s119,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19
| spl0_22
| ~ spl0_34 ),
inference(sat_conversion,[],[f1110]) ).
cnf(s133,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19
| ~ spl0_33
| ~ spl0_47 ),
inference(sat_conversion,[],[f1165]) ).
cnf(s149,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_22
| ~ spl0_45
| spl0_47 ),
inference(sat_conversion,[],[f1297]) ).
cnf(s157,plain,
( ~ spl0_8
| ~ spl0_9
| ~ spl0_29
| ~ spl0_57
| ~ spl0_58 ),
inference(sat_conversion,[],[f1336]) ).
cnf(s167,plain,
( ~ spl0_1
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| spl0_33
| ~ spl0_34 ),
inference(sat_conversion,[],[f1375]) ).
cnf(s169,plain,
( ~ spl0_13
| ~ spl0_33
| ~ spl0_46
| ~ spl0_47 ),
inference(sat_conversion,[],[f1393]) ).
cnf(s174,plain,
( ~ spl0_20
| ~ spl0_21
| spl0_30 ),
inference(sat_conversion,[],[f1423]) ).
cnf(s176,plain,
( ~ spl0_18
| ~ spl0_30
| spl0_47 ),
inference(sat_conversion,[],[f1453]) ).
cnf(s178,plain,
( ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16
| spl0_59 ),
inference(sat_conversion,[],[f1469]) ).
cnf(s195,plain,
( ~ spl0_6
| ~ spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16
| spl0_57 ),
inference(sat_conversion,[],[f1503]) ).
cnf(s220,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_17
| ~ spl0_30
| spl0_34 ),
inference(sat_conversion,[],[f1563]) ).
cnf(s222,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_14
| ~ spl0_17
| spl0_46 ),
inference(sat_conversion,[],[f1567]) ).
cnf(s230,plain,
( ~ spl0_1
| ~ spl0_13
| ~ spl0_22
| spl0_29
| ~ spl0_52
| ~ spl0_61 ),
inference(sat_conversion,[],[f1589]) ).
cnf(s231,plain,
( spl0_22
| ~ spl0_30
| ~ spl0_45 ),
inference(sat_conversion,[],[f1593]) ).
cnf(s233,plain,
( ~ spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16
| spl0_58 ),
inference(sat_conversion,[],[f1594]) ).
cnf(s239,plain,
( ~ spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16
| spl0_52 ),
inference(sat_conversion,[],[f1599]) ).
cnf(s259,plain,
( ~ spl0_11
| ~ spl0_12
| spl0_45 ),
inference(sat_conversion,[],[f1608]) ).
cnf(s261,plain,
( ~ spl0_22
| spl0_23
| ~ spl0_47 ),
inference(sat_conversion,[],[f1612]) ).
cnf(s262,plain,
( ~ spl0_11
| ~ spl0_12
| ~ spl0_15
| ~ spl0_16
| spl0_22 ),
inference(sat_conversion,[],[f1613]) ).
cnf(s286,plain,
( ~ spl0_14
| ~ spl0_22
| spl0_61
| ~ spl0_64 ),
inference(sat_conversion,[],[f1711]) ).
cnf(s310,plain,
( ~ spl0_2
| ~ spl0_5
| ~ spl0_22
| ~ spl0_59
| ~ spl0_64 ),
inference(sat_conversion,[],[f1818]) ).
cnf(s312,plain,
( ~ spl0_4
| ~ spl0_15
| ~ spl0_16
| ~ spl0_22
| ~ spl0_64 ),
inference(sat_conversion,[],[f1838]) ).
cnf(s315,plain,
( ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16
| ~ spl0_22
| spl0_64 ),
inference(sat_conversion,[],[f1847]) ).
cnf(s316,plain,
spl0_5,
inference(rat,[],[s73,s27,s28,s29,s30,s31,s32]) ).
cnf(s317,plain,
( spl0_7
| ~ spl0_4 ),
inference(rat,[],[s315,s312,s262,s7,s8,s9,s10,s11,s12]) ).
cnf(s318,plain,
( ~ spl0_16
| ~ spl0_15
| ~ spl0_14
| ~ spl0_13
| ~ spl0_12
| ~ spl0_11
| ~ spl0_4 ),
inference(rat,[],[s315,s312,s262]) ).
cnf(s319,plain,
( ~ spl0_17
| ~ spl0_14
| ~ spl0_4
| ~ spl0_7
| ~ spl0_13 ),
inference(rat,[],[s96,s117,s316]) ).
cnf(s320,plain,
( ~ spl0_14
| ~ spl0_13
| ~ spl0_12
| ~ spl0_11
| ~ spl0_4 ),
inference(rat,[],[s318,s21,s22,s319,s317]) ).
cnf(s321,plain,
( spl0_14
| ~ spl0_45
| ~ spl0_4 ),
inference(rat,[],[s231,s118,s174,s20,s40,s50,s60,s70,s317,s316]) ).
cnf(s322,plain,
( ~ spl0_12
| ~ spl0_11
| ~ spl0_4 ),
inference(rat,[],[s231,s118,s174,s19,s39,s49,s59,s69,s320,s321,s259,s317,s316]) ).
cnf(s323,plain,
( spl0_12
| ~ spl0_4 ),
inference(rat,[],[s119,s220,s118,s174,s18,s38,s48,s58,s68,s317,s316]) ).
cnf(s324,plain,
~ spl0_4,
inference(rat,[],[s119,s220,s118,s174,s17,s37,s47,s57,s67,s322,s323,s317,s316]) ).
cnf(s325,plain,
( spl0_17
| ~ spl0_12
| ~ spl0_11
| ~ spl0_3 ),
inference(rat,[],[s76,s21,s22]) ).
cnf(s326,plain,
( ~ spl0_22
| ~ spl0_14
| ~ spl0_13
| ~ spl0_17
| ~ spl0_45
| ~ spl0_7
| ~ spl0_3 ),
inference(rat,[],[s261,s87,s149,s316]) ).
cnf(s327,plain,
( spl0_18
| ~ spl0_12
| ~ spl0_11
| ~ spl0_3 ),
inference(rat,[],[s76,s41,s42]) ).
cnf(s328,plain,
( ~ spl0_14
| ~ spl0_13
| ~ spl0_18
| ~ spl0_17
| ~ spl0_45
| ~ spl0_7
| ~ spl0_3 ),
inference(rat,[],[s109,s96,s326,s316]) ).
cnf(s329,plain,
( spl0_14
| ~ spl0_3 ),
inference(rat,[],[s86,s60,s70]) ).
cnf(s330,plain,
( spl0_13
| ~ spl0_3 ),
inference(rat,[],[s86,s59,s69]) ).
cnf(s331,plain,
( ~ spl0_12
| ~ spl0_11
| ~ spl0_7
| ~ spl0_3 ),
inference(rat,[],[s328,s327,s325,s259,s329,s330]) ).
cnf(s332,plain,
( spl0_12
| ~ spl0_3 ),
inference(rat,[],[s86,s58,s68]) ).
cnf(s333,plain,
( spl0_11
| ~ spl0_3 ),
inference(rat,[],[s86,s57,s67]) ).
cnf(s334,plain,
( ~ spl0_11
| ~ spl0_3
| ~ spl0_12 ),
inference(rat,[],[s76,s11,s12,s331]) ).
cnf(s335,plain,
~ spl0_3,
inference(rat,[],[s334,s333,s332]) ).
cnf(s336,plain,
( spl0_14
| ~ spl0_17
| ~ spl0_7
| ~ spl0_2 ),
inference(rat,[],[s105,s40,s50,s316]) ).
cnf(s337,plain,
( ~ spl0_14
| ~ spl0_17
| ~ spl0_2
| ~ spl0_7 ),
inference(rat,[],[s105,s39,s49,s106,s316]) ).
cnf(s338,plain,
( ~ spl0_17
| ~ spl0_7
| ~ spl0_2 ),
inference(rat,[],[s337,s336]) ).
cnf(s339,plain,
( spl0_17
| ~ spl0_12
| ~ spl0_11
| ~ spl0_2 ),
inference(rat,[],[s310,s315,s262,s178,s19,s20,s21,s22,s316]) ).
cnf(s340,plain,
( ~ spl0_12
| ~ spl0_11
| ~ spl0_2 ),
inference(rat,[],[s310,s315,s262,s178,s9,s10,s11,s12,s338,s339,s316]) ).
cnf(s341,plain,
( spl0_12
| ~ spl0_2 ),
inference(rat,[],[s105,s8,s18,s38,s48,s316]) ).
cnf(s342,plain,
( ~ spl0_12
| ~ spl0_2 ),
inference(rat,[],[s105,s7,s17,s37,s47,s340,s316]) ).
cnf(s343,plain,
~ spl0_2,
inference(rat,[],[s342,s341]) ).
cnf(s344,plain,
spl0_1,
inference(rat,[],[s2,s324,s316,s335,s343]) ).
cnf(s345,plain,
( ~ spl0_13
| ~ spl0_14
| ~ spl0_12
| ~ spl0_11
| ~ spl0_17
| ~ spl0_7 ),
inference(rat,[],[s262,s41,s42,s149,s102,s169,s167,s96,s259,s222,s316,s344]) ).
cnf(s346,plain,
( spl0_13
| ~ spl0_17
| ~ spl0_7 ),
inference(rat,[],[s167,s133,s220,s176,s174,s39,s49,s59,s69,s344,s316]) ).
cnf(s347,plain,
( spl0_14
| ~ spl0_17
| ~ spl0_7 ),
inference(rat,[],[s167,s133,s220,s176,s174,s40,s50,s60,s70,s344,s316]) ).
cnf(s348,plain,
( spl0_12
| ~ spl0_17
| ~ spl0_7 ),
inference(rat,[],[s101,s38,s48,s167,s96,s347,s346,s316,s344]) ).
cnf(s349,plain,
( ~ spl0_14
| ~ spl0_13
| ~ spl0_7
| ~ spl0_17 ),
inference(rat,[],[s37,s345,s102,s348,s167,s96,s344,s316]) ).
cnf(s350,plain,
( ~ spl0_17
| ~ spl0_7 ),
inference(rat,[],[s349,s347,s346]) ).
cnf(s351,plain,
spl0_17,
inference(rat,[],[s230,s286,s157,s195,s233,s315,s262,s239,s13,s14,s15,s16,s17,s18,s19,s20,s21,s22,s344]) ).
cnf(s352,plain,
~ spl0_7,
inference(rat,[],[s350,s351]) ).
cnf(s353,plain,
spl0_16,
inference(rat,[],[s12,s352]) ).
cnf(s354,plain,
spl0_15,
inference(rat,[],[s11,s352]) ).
cnf(s355,plain,
spl0_14,
inference(rat,[],[s10,s352]) ).
cnf(s356,plain,
spl0_13,
inference(rat,[],[s9,s352]) ).
cnf(s357,plain,
spl0_12,
inference(rat,[],[s8,s352]) ).
cnf(s358,plain,
spl0_11,
inference(rat,[],[s7,s352]) ).
cnf(s359,plain,
spl0_10,
inference(rat,[],[s6,s352]) ).
cnf(s360,plain,
spl0_9,
inference(rat,[],[s5,s352]) ).
cnf(s361,plain,
spl0_8,
inference(rat,[],[s4,s352]) ).
cnf(s362,plain,
spl0_6,
inference(rat,[],[s3,s352]) ).
cnf(s364,plain,
spl0_52,
inference(rat,[],[s239,s353,s357,s358,s359,s354]) ).
cnf(s366,plain,
spl0_22,
inference(rat,[],[s262,s353,s357,s358,s354]) ).
cnf(s367,plain,
spl0_64,
inference(rat,[],[s315,s366,s353,s355,s356,s354]) ).
cnf(s368,plain,
spl0_58,
inference(rat,[],[s233,s354,s357,s358,s353,s359]) ).
cnf(s369,plain,
spl0_57,
inference(rat,[],[s195,s354,s357,s358,s353,s362,s359]) ).
cnf(s370,plain,
~ spl0_29,
inference(rat,[],[s157,s368,s369,s361,s360]) ).
cnf(s374,plain,
spl0_61,
inference(rat,[],[s286,s366,s355,s367]) ).
cnf(s380,plain,
$false,
inference(rat,[],[s230,s366,s364,s356,s344,s374,s370]) ).
fof(f1848,plain,
$false,
inference(avatar_sat_refutation,[],[s380]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP258-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.02 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.03/0.31 % Computer : n012.cluster.edu
% 0.03/0.31 % Model : x86_64 x86_64
% 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.31 % Memory : 8046.5625MB
% 0.03/0.31 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Sun Sep 27 09:43:20 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.03/0.31 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.33 Running first-order theorem proving
% 0.07/0.33 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.89/0.82 % (2121591)Input is clausal, will run a generic CNF schedule.
% 0.89/0.82 % (2121598)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=141447641:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 0.89/0.82 % (2121597)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=960066674:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 0.89/0.82 % (2121599)lrs+10_1_sil=8000:sp=occurrence:random_seed=469912835:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 0.89/0.82 % (2121596)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=3930034441:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 0.89/0.82 % (2121599)Refutation not found, incomplete strategy
% 0.89/0.82 % (2121599)------------------------------
% 0.89/0.82 % (2121599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.89/0.82 % (2121599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.82 % (2121599)CaDiCaL version: 2.1.3
% 0.89/0.82 % (2121599)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.82 % (2121599)Time elapsed: 0.002 s
% 0.89/0.82 % (2121599)Peak memory usage: 88 MB
% 0.89/0.82 % (2121599)Instructions burned: 6 (million)
% 0.89/0.82 % (2121600)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=32076469:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 0.89/0.82 % (2121601)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1055971492:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 0.89/0.82 % (2121602)dis-21_1_sil=8000:lcm=predicate:random_seed=4132942237: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)
% 0.89/0.82 % (2121602)Refutation not found, incomplete strategy
% 0.89/0.82 % (2121602)------------------------------
% 0.89/0.82 % (2121602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.89/0.82 % (2121602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.82 % (2121602)CaDiCaL version: 2.1.3
% 0.89/0.82 % (2121602)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.82 % (2121602)Time elapsed: 0.001 s
% 0.89/0.82 % (2121602)Peak memory usage: 88 MB
% 0.89/0.82 % (2121602)Instructions burned: 3 (million)
% 0.89/0.82 % (2121601)First to succeed.
% 0.89/0.82 % (2121601)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2121591"
% 0.89/0.82 % (2121600)Instruction limit reached!
% 0.89/0.82 % (2121600)------------------------------
% 0.89/0.82 % (2121600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.89/0.82 % (2121600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.82 % (2121600)CaDiCaL version: 2.1.3
% 0.89/0.82 % (2121600)Termination reason: Instruction limit
% 0.89/0.82 % (2121600)Termination phase: Saturation
% 0.89/0.82 % (2121600)Time elapsed: 0.036 s
% 0.89/0.82 % (2121600)Peak memory usage: 89 MB
% 0.89/0.82 % (2121600)Instructions burned: 116 (million)
% 0.89/0.82 % (2121610)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=2018563615:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 0.89/0.82 % (2121610)Refutation not found, incomplete strategy
% 0.89/0.82 % (2121610)------------------------------
% 0.89/0.82 % (2121610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.89/0.82 % (2121610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.82 % (2121610)CaDiCaL version: 2.1.3
% 0.89/0.82 % (2121610)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.82 % (2121610)Time elapsed: 0.002 s
% 0.89/0.82 % (2121610)Peak memory usage: 88 MB
% 0.89/0.82 % (2121610)Instructions burned: 6 (million)
% 0.89/0.82 % (2121599)------------------------------
% 0.89/0.82 % (2121599)------------------------------
% 0.89/0.82 % (2121602)------------------------------
% 0.89/0.82 % (2121602)------------------------------
% 0.89/0.82 % (2121601)Refutation found. Thanks to Tanya!
% 0.89/0.82 % SZS status Unsatisfiable for theBenchmark
% 0.89/0.82 % SZS output start Proof for theBenchmark
% See solution above
% 2.28/0.91 % (2121601)------------------------------
% 2.28/0.91 % (2121601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.28/0.91 % (2121601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/0.91 % (2121601)CaDiCaL version: 2.1.3
% 2.28/0.91 % (2121601)Termination reason: Refutation
% 2.28/0.91 % (2121601)Time elapsed: 0.021 s
% 2.28/0.91 % (2121601)Peak memory usage: 90 MB
% 2.28/0.91 % (2121601)Instructions burned: 62 (million)
% 2.28/0.91 % (2121601)------------------------------
% 2.28/0.91 % (2121601)------------------------------
% 2.28/0.91 % (2121591)Success in time 0.293 s
% 2.28/0.91 % Vampire exiting
%------------------------------------------------------------------------------