%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP251-1 : TPTP v3.4.2. Released v2.5.0.
% Transfm : add_equality:r
% Format : otter:hypothesis:set(auto),clear(print_given)
% Command : gandalf-wrapper -time %d %s
% Computer : art02.cs.miami.edu
% Model : i686 unknown
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 1000MB
% OS : Linux 2.4.22-21mdk-i686-up-4GB
% CPULimit : 600s
% Result : Unsatisfiable 49.5s
% Output : Assurance 49.5s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----NO SOLUTION OUTPUT BY SYSTEM
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
%
% Gandalf c-2.6 r1 starting to prove: /home/graph/tptp/TSTP/PreparedTPTP/otter:hypothesis:set(auto),clear(print_given)---add_equality:r/GRP/GRP251-1+eq_r.in
% Using automatic strategy selection.
% Time limit in seconds: 600
%
% prove-all-passes started
%
% detected problem class: peq
%
% strategies selected:
% (hyper 30 #f 3 25)
% (binary-unit 12 #f)
% (binary-unit-uniteq 12 #f)
% (binary-posweight-kb-big-order 60 #f 3 25)
% (binary-posweight-lex-big-order 30 #f 3 25)
% (binary 30 #t)
% (binary-posweight-kb-big-order 156 #f)
% (binary-posweight-lex-big-order 102 #f)
% (binary-posweight-firstpref-order 60 #f)
% (binary-order 30 #f)
% (binary-posweight-kb-small-order 48 #f)
% (binary-posweight-lex-small-order 30 #f)
%
%
% SOS clause
% -equal(multiply(X,sk_c10),sk_c9) | -equal(inverse(X),sk_c10) | -equal(multiply(Y,sk_c9),sk_c8) | -equal(inverse(Y),sk_c9) | -equal(inverse(Z),sk_c9) | -equal(multiply(Z,sk_c8),sk_c9) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(V,sk_c8),sk_c9) | -equal(inverse(V),sk_c8) | -equal(multiply(sk_c9,W),sk_c8) | -equal(multiply(X1,sk_c9),W) | -equal(inverse(X1),sk_c9).
% was split for some strategies as:
% -equal(multiply(sk_c9,W),sk_c8) | -equal(multiply(X1,sk_c9),W) | -equal(inverse(X1),sk_c9).
% -equal(multiply(V,sk_c8),sk_c9) | -equal(inverse(V),sk_c8).
% -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10).
% -equal(inverse(Z),sk_c9) | -equal(multiply(Z,sk_c8),sk_c9).
% -equal(multiply(Y,sk_c9),sk_c8) | -equal(inverse(Y),sk_c9).
% -equal(multiply(X,sk_c10),sk_c9) | -equal(inverse(X),sk_c10).
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(47,40,1,101,0,1,195303,5,1502,195303,1,1502,195303,50,1502,195303,40,1502,195357,0,1502,207239,3,1803,207874,4,1953,208881,1,2103,208881,50,2103,208881,40,2103,208935,0,2103,209307,3,2406,209318,4,2565,209344,5,2704,209344,1,2704,209344,50,2704,209344,40,2704,209398,0,2704,231693,3,4205,232134,4,4955)
%
%
% START OF PROOF
% 209075 [?] ?
% 209345 [] equal(X,X).
% 209346 [] equal(multiply(identity,X),X).
% 209347 [] equal(multiply(inverse(X),X),identity).
% 209348 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 209350 [] equal(multiply(sk_c3,sk_c8),sk_c9) | equal(inverse(sk_c6),sk_c9).
% 209351 [] equal(multiply(sk_c3,sk_c8),sk_c9) | equal(multiply(sk_c6,sk_c9),sk_c7).
% 209352 [] equal(multiply(sk_c3,sk_c8),sk_c9) | equal(multiply(sk_c9,sk_c7),sk_c8).
% 209353 [] equal(multiply(sk_c3,sk_c8),sk_c9) | equal(inverse(sk_c5),sk_c8).
% 209354 [] equal(multiply(sk_c3,sk_c8),sk_c9) | equal(multiply(sk_c5,sk_c8),sk_c9).
% 209355 [] equal(multiply(sk_c3,sk_c8),sk_c9) | equal(inverse(sk_c4),sk_c10).
% 209357 [] equal(inverse(sk_c3),sk_c9) | equal(inverse(sk_c6),sk_c9).
% 209358 [] equal(multiply(sk_c6,sk_c9),sk_c7) | equal(inverse(sk_c3),sk_c9).
% 209359 [] equal(multiply(sk_c9,sk_c7),sk_c8) | equal(inverse(sk_c3),sk_c9).
% 209360 [] equal(inverse(sk_c3),sk_c9) | equal(inverse(sk_c5),sk_c8).
% 209361 [] equal(multiply(sk_c5,sk_c8),sk_c9) | equal(inverse(sk_c3),sk_c9).
% 209362 [] equal(inverse(sk_c3),sk_c9) | equal(inverse(sk_c4),sk_c10).
% 209364 [] equal(inverse(sk_c2),sk_c9) | equal(inverse(sk_c6),sk_c9).
% 209365 [] equal(multiply(sk_c6,sk_c9),sk_c7) | equal(inverse(sk_c2),sk_c9).
% 209366 [] equal(multiply(sk_c9,sk_c7),sk_c8) | equal(inverse(sk_c2),sk_c9).
% 209367 [] equal(inverse(sk_c2),sk_c9) | equal(inverse(sk_c5),sk_c8).
% 209368 [] equal(multiply(sk_c5,sk_c8),sk_c9) | equal(inverse(sk_c2),sk_c9).
% 209369 [] equal(inverse(sk_c2),sk_c9) | equal(inverse(sk_c4),sk_c10).
% 209371 [] equal(multiply(sk_c2,sk_c9),sk_c8) | equal(inverse(sk_c6),sk_c9).
% 209372 [] equal(multiply(sk_c2,sk_c9),sk_c8) | equal(multiply(sk_c6,sk_c9),sk_c7).
% 209373 [] equal(multiply(sk_c2,sk_c9),sk_c8) | equal(multiply(sk_c9,sk_c7),sk_c8).
% 209374 [] equal(multiply(sk_c2,sk_c9),sk_c8) | equal(inverse(sk_c5),sk_c8).
% 209375 [] equal(multiply(sk_c2,sk_c9),sk_c8) | equal(multiply(sk_c5,sk_c8),sk_c9).
% 209376 [] equal(multiply(sk_c2,sk_c9),sk_c8) | equal(inverse(sk_c4),sk_c10).
% 209378 [] equal(inverse(sk_c1),sk_c10) | equal(inverse(sk_c6),sk_c9).
% 209379 [] equal(multiply(sk_c6,sk_c9),sk_c7) | equal(inverse(sk_c1),sk_c10).
% 209380 [] equal(multiply(sk_c9,sk_c7),sk_c8) | equal(inverse(sk_c1),sk_c10).
% 209381 [] equal(inverse(sk_c1),sk_c10) | equal(inverse(sk_c5),sk_c8).
% 209382 [] equal(multiply(sk_c5,sk_c8),sk_c9) | equal(inverse(sk_c1),sk_c10).
% 209383 [] equal(inverse(sk_c1),sk_c10) | equal(inverse(sk_c4),sk_c10).
% 209384 [] equal(multiply(sk_c4,sk_c10),sk_c9) | equal(inverse(sk_c1),sk_c10).
% 209385 [] equal(multiply(sk_c1,sk_c10),sk_c9) | equal(inverse(sk_c6),sk_c9).
% 209388 [] equal(multiply(sk_c1,sk_c10),sk_c9) | equal(inverse(sk_c5),sk_c8).
% 209389 [] equal(multiply(sk_c1,sk_c10),sk_c9) | equal(multiply(sk_c5,sk_c8),sk_c9).
% 209390 [] equal(multiply(sk_c1,sk_c10),sk_c9) | equal(inverse(sk_c4),sk_c10).
% 209391 [] equal(multiply(sk_c1,sk_c10),sk_c9) | equal(multiply(sk_c4,sk_c10),sk_c9).
% 209392 [] $spltprd0($spltcnst19) | -equal(multiply(sk_c9,X),sk_c8) | -equal(multiply(Y,sk_c9),X) | -equal(inverse(Y),sk_c9).
% 209393 [] $spltprd0($spltcnst20) | -equal(multiply(X,sk_c8),sk_c9) | -equal(inverse(X),sk_c8).
% 209394 [] $spltprd0($spltcnst21) | -equal(multiply(X,sk_c10),sk_c9) | -equal(inverse(X),sk_c10).
% 209395 [] $spltprd0($spltcnst22) | -equal(multiply(X,sk_c8),sk_c9) | -equal(inverse(X),sk_c9).
% 209396 [] $spltprd0($spltcnst23) | -equal(multiply(X,sk_c9),sk_c8) | -equal(inverse(X),sk_c9).
% 209397 [] $spltprd0($spltcnst24) | -equal(multiply(X,sk_c10),sk_c9) | -equal(inverse(X),sk_c10).
% 209398 [] -$spltprd0($spltcnst20) | -$spltprd0($spltcnst19) | -$spltprd0($spltcnst21) | -$spltprd0($spltcnst23) | -$spltprd0($spltcnst22) | -$spltprd0($spltcnst24).
% 209402 [para:209357.2.1,209347.1.1.1] equal(multiply(sk_c9,sk_c6),identity) | equal(inverse(sk_c3),sk_c9).
% 209404 [para:209360.1.1,209347.1.1.1] equal(multiply(sk_c9,sk_c3),identity) | equal(inverse(sk_c5),sk_c8).
% 209405 [para:209360.2.1,209347.1.1.1] equal(multiply(sk_c8,sk_c5),identity) | equal(inverse(sk_c3),sk_c9).
% 209414 [para:209367.1.1,209347.1.1.1] equal(multiply(sk_c9,sk_c2),identity) | equal(inverse(sk_c5),sk_c8).
% 209417 [para:209369.1.1,209347.1.1.1] equal(multiply(sk_c9,sk_c2),identity) | equal(inverse(sk_c4),sk_c10).
% 209420 [para:209378.1.1,209347.1.1.1] equal(multiply(sk_c10,sk_c1),identity) | equal(inverse(sk_c6),sk_c9).
% 209421 [para:209378.2.1,209347.1.1.1] equal(multiply(sk_c9,sk_c6),identity) | equal(inverse(sk_c1),sk_c10).
% 209425 [para:209381.1.1,209347.1.1.1] equal(multiply(sk_c10,sk_c1),identity) | equal(inverse(sk_c5),sk_c8).
% 209426 [para:209381.2.1,209347.1.1.1] equal(multiply(sk_c8,sk_c5),identity) | equal(inverse(sk_c1),sk_c10).
% 209428 [para:209383.1.1,209347.1.1.1] equal(multiply(sk_c10,sk_c1),identity) | equal(inverse(sk_c4),sk_c10).
% 209563 [para:209361.1.1,209393.2.1,cut:209345] -equal(inverse(sk_c5),sk_c8) | equal(inverse(sk_c3),sk_c9) | $spltprd0($spltcnst20).
% 209565 [para:209368.1.1,209393.2.1,cut:209345] -equal(inverse(sk_c5),sk_c8) | equal(inverse(sk_c2),sk_c9) | $spltprd0($spltcnst20).
% 209567 [para:209354.2.1,209393.2.1,cut:209345] equal(multiply(sk_c3,sk_c8),sk_c9) | -equal(inverse(sk_c5),sk_c8) | $spltprd0($spltcnst20).
% 209568 [para:209382.1.1,209393.2.1,cut:209345] -equal(inverse(sk_c5),sk_c8) | equal(inverse(sk_c1),sk_c10) | $spltprd0($spltcnst20).
% 209570 [para:209375.2.1,209393.2.1,cut:209345] equal(multiply(sk_c2,sk_c9),sk_c8) | -equal(inverse(sk_c5),sk_c8) | $spltprd0($spltcnst20).
% 209571 [para:209389.2.1,209393.2.1,cut:209345] equal(multiply(sk_c1,sk_c10),sk_c9) | -equal(inverse(sk_c5),sk_c8) | $spltprd0($spltcnst20).
% 209595 [para:209390.1.1,209394.2.1,cut:209345,binarycut:209383] equal(inverse(sk_c4),sk_c10) | $spltprd0($spltcnst21).
% 209603 [para:209391.2.1,209394.2.1,cut:209345,binarycut:209595] equal(multiply(sk_c1,sk_c10),sk_c9) | $spltprd0($spltcnst21).
% 209607 [para:209346.1.1,209395.2.1] -equal(inverse(identity),sk_c9) | -equal(sk_c8,sk_c9) | $spltprd0($spltcnst22).
% 209610 [para:209350.1.1,209395.2.1,cut:209345,binarycut:209357] equal(inverse(sk_c6),sk_c9) | $spltprd0($spltcnst22).
% 209612 [para:209353.1.1,209395.2.1,cut:209345,binarycut:209360] equal(inverse(sk_c5),sk_c8) | $spltprd0($spltcnst22).
% 209614 [para:209355.1.1,209395.2.1,cut:209345,binarycut:209362] equal(inverse(sk_c4),sk_c10) | $spltprd0($spltcnst22).
% 209634 [para:209610.1.1,209347.1.1.1] equal(multiply(sk_c9,sk_c6),identity) | $spltprd0($spltcnst22).
% 209642 [para:209371.1.1,209396.2.1,cut:209345,binarycut:209364] equal(inverse(sk_c6),sk_c9) | $spltprd0($spltcnst23).
% 209644 [para:209374.1.1,209396.2.1,cut:209345,binarycut:209367] equal(inverse(sk_c5),sk_c8) | $spltprd0($spltcnst23).
% 209660 [para:209612.1.1,209347.1.1.1] equal(multiply(sk_c8,sk_c5),identity) | $spltprd0($spltcnst22).
% 209662 [para:209614.1.1,209347.1.1.1] equal(multiply(sk_c10,sk_c4),identity) | $spltprd0($spltcnst22).
% 209664 [para:209642.1.1,209347.1.1.1] equal(multiply(sk_c9,sk_c6),identity) | $spltprd0($spltcnst23).
% 209666 [para:209644.1.1,209347.1.1.1] equal(multiply(sk_c8,sk_c5),identity) | $spltprd0($spltcnst23).
% 209681 [para:209390.1.1,209397.2.1,cut:209345,binarycut:209383] equal(inverse(sk_c4),sk_c10) | $spltprd0($spltcnst24).
% 209689 [para:209391.2.1,209397.2.1,cut:209345,binarycut:209681] equal(multiply(sk_c1,sk_c10),sk_c9) | $spltprd0($spltcnst24).
% 209699 [para:209603.1.1,209394.2.1,cut:209345] -equal(inverse(sk_c1),sk_c10) | $spltprd0($spltcnst21).
% 209705 [para:209384.2.1,209699.1.1,cut:209345] equal(multiply(sk_c4,sk_c10),sk_c9) | $spltprd0($spltcnst21).
% 209712 [para:209347.1.1,209348.1.1.1,demod:209346] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 209748 [para:209404.1.1,209348.1.1.1,demod:209346] equal(inverse(sk_c5),sk_c8) | equal(X,multiply(sk_c9,multiply(sk_c3,X))).
% 209756 [para:209414.1.1,209348.1.1.1,demod:209346] equal(inverse(sk_c5),sk_c8) | equal(X,multiply(sk_c9,multiply(sk_c2,X))).
% 209758 [para:209417.1.1,209348.1.1.1,demod:209346] equal(inverse(sk_c4),sk_c10) | equal(X,multiply(sk_c9,multiply(sk_c2,X))).
% 209762 [para:209420.1.1,209348.1.1.1,demod:209346] equal(inverse(sk_c6),sk_c9) | equal(X,multiply(sk_c10,multiply(sk_c1,X))).
% 209763 [para:209421.1.1,209348.1.1.1,demod:209346] equal(inverse(sk_c1),sk_c10) | equal(X,multiply(sk_c9,multiply(sk_c6,X))).
% 209764 [para:209425.1.1,209348.1.1.1,demod:209346] equal(inverse(sk_c5),sk_c8) | equal(X,multiply(sk_c10,multiply(sk_c1,X))).
% 209765 [para:209426.1.1,209348.1.1.1,demod:209346] equal(inverse(sk_c1),sk_c10) | equal(X,multiply(sk_c8,multiply(sk_c5,X))).
% 209766 [para:209428.1.1,209348.1.1.1,demod:209346] equal(inverse(sk_c4),sk_c10) | equal(X,multiply(sk_c10,multiply(sk_c1,X))).
% 209802 [para:209662.1.1,209348.1.1.1,demod:209346] $spltprd0($spltcnst22) | equal(X,multiply(sk_c10,multiply(sk_c4,X))).
% 209815 [para:209689.1.1,209397.2.1,cut:209345] -equal(inverse(sk_c1),sk_c10) | $spltprd0($spltcnst24).
% 209821 [para:209384.2.1,209815.1.1,cut:209345] equal(multiply(sk_c4,sk_c10),sk_c9) | $spltprd0($spltcnst24).
% 209858 [para:209705.1.1,209394.2.1,cut:209345,binarycut:209595] $spltprd0($spltcnst21).
% 209881 [para:209821.1.1,209397.2.1,cut:209345,binarycut:209681] $spltprd0($spltcnst24).
% 209890 [para:209350.1.1,209712.1.2.2] equal(sk_c8,multiply(inverse(sk_c3),sk_c9)) | equal(inverse(sk_c6),sk_c9).
% 209893 [para:209358.1.1,209712.1.2.2] equal(sk_c9,multiply(inverse(sk_c6),sk_c7)) | equal(inverse(sk_c3),sk_c9).
% 209897 [para:209361.1.1,209712.1.2.2] equal(sk_c8,multiply(inverse(sk_c5),sk_c9)) | equal(inverse(sk_c3),sk_c9).
% 209995 [para:209634.1.1,209712.1.2.2] equal(sk_c6,multiply(inverse(sk_c9),identity)) | $spltprd0($spltcnst22).
% 209996 [para:209660.1.1,209712.1.2.2] equal(sk_c5,multiply(inverse(sk_c8),identity)) | $spltprd0($spltcnst22).
% 209997 [para:209662.1.1,209712.1.2.2] equal(sk_c4,multiply(inverse(sk_c10),identity)) | $spltprd0($spltcnst22).
% 209998 [para:209664.1.1,209712.1.2.2] equal(sk_c6,multiply(inverse(sk_c9),identity)) | $spltprd0($spltcnst23).
% 209999 [para:209666.1.1,209712.1.2.2] equal(sk_c5,multiply(inverse(sk_c8),identity)) | $spltprd0($spltcnst23).
% 210019 [para:209995.1.2,209348.1.1.1,demod:209346] $spltprd0($spltcnst22) | equal(multiply(sk_c6,X),multiply(inverse(sk_c9),X)).
% 210021 [para:209996.1.2,209348.1.1.1,demod:209346] $spltprd0($spltcnst22) | equal(multiply(sk_c5,X),multiply(inverse(sk_c8),X)).
% 210031 [para:209998.1.2,209348.1.1.1,demod:209346] $spltprd0($spltcnst23) | equal(multiply(sk_c6,X),multiply(inverse(sk_c9),X)).
% 210033 [para:209999.1.2,209348.1.1.1,demod:209346] $spltprd0($spltcnst23) | equal(multiply(sk_c5,X),multiply(inverse(sk_c8),X)).
% 210125 [para:210019.2.2,209347.1.1] equal(multiply(sk_c6,sk_c9),identity) | $spltprd0($spltcnst22).
% 210134 [para:210125.1.1,209358.1.1] equal(inverse(sk_c3),sk_c9) | equal(identity,sk_c7) | $spltprd0($spltcnst22).
% 210140 [para:210125.1.1,209379.1.1] equal(inverse(sk_c1),sk_c10) | equal(identity,sk_c7) | $spltprd0($spltcnst22).
% 210248 [para:210021.2.2,209347.1.1] equal(multiply(sk_c5,sk_c8),identity) | $spltprd0($spltcnst22).
% 210257 [para:210248.1.1,209361.1.1] equal(inverse(sk_c3),sk_c9) | equal(identity,sk_c9) | $spltprd0($spltcnst22).
% 210263 [para:210248.1.1,209382.1.1] equal(inverse(sk_c1),sk_c10) | equal(identity,sk_c9) | $spltprd0($spltcnst22).
% 210310 [para:210257.2.2,209359.1.1.1,demod:209346] equal(inverse(sk_c3),sk_c9) | equal(sk_c7,sk_c8) | $spltprd0($spltcnst22).
% 210318 [para:210257.2.2,209607.1.2,cut:209075] equal(inverse(sk_c3),sk_c9) | -equal(sk_c8,sk_c9) | $spltprd0($spltcnst22).
% 210357 [para:210263.2.2,209380.1.1.1,demod:209346] equal(inverse(sk_c1),sk_c10) | equal(sk_c7,sk_c8) | $spltprd0($spltcnst22).
% 210365 [para:210263.2.2,209607.1.2,cut:209075] equal(inverse(sk_c1),sk_c10) | -equal(sk_c8,sk_c9) | $spltprd0($spltcnst22).
% 210399 [para:210134.2.1,210310.2.2] equal(inverse(sk_c3),sk_c9) | equal(identity,sk_c8) | $spltprd0($spltcnst22).
% 210411 [para:210257.2.2,210318.2.2] equal(inverse(sk_c3),sk_c9) | -equal(sk_c8,identity) | $spltprd0($spltcnst22).
% 210453 [para:210140.2.1,210357.2.2] equal(inverse(sk_c1),sk_c10) | equal(identity,sk_c8) | $spltprd0($spltcnst22).
% 210474 [para:210263.2.2,210365.2.2] equal(inverse(sk_c1),sk_c10) | -equal(sk_c8,identity) | $spltprd0($spltcnst22).
% 210510 [para:210399.2.2,210411.2.1,cut:209345] equal(inverse(sk_c3),sk_c9) | $spltprd0($spltcnst22).
% 210512 [para:210510.1.1,209347.1.1.1] equal(multiply(sk_c9,sk_c3),identity) | $spltprd0($spltcnst22).
% 210696 [para:210453.2.2,210474.2.1,cut:209345] equal(inverse(sk_c1),sk_c10) | $spltprd0($spltcnst22).
% 210698 [para:210696.1.1,209347.1.1.1] equal(multiply(sk_c10,sk_c1),identity) | $spltprd0($spltcnst22).
% 210701 [para:210698.1.1,209712.1.2.2] equal(sk_c1,multiply(inverse(sk_c10),identity)) | $spltprd0($spltcnst22).
% 210704 [para:210701.1.2,209997.1.2] equal(sk_c4,sk_c1) | $spltprd0($spltcnst22).
% 210710 [para:210704.1.2,209391.1.1.1] equal(multiply(sk_c4,sk_c10),sk_c9) | $spltprd0($spltcnst22).
% 210720 [para:210710.1.1,209802.2.2.2] equal(sk_c10,multiply(sk_c10,sk_c9)) | $spltprd0($spltcnst22).
% 210724 [para:210720.1.2,209712.1.2.2,demod:209347] equal(sk_c9,identity) | $spltprd0($spltcnst22).
% 210748 [para:210724.1.1,209607.1.2,cut:209075] -equal(sk_c8,sk_c9) | $spltprd0($spltcnst22).
% 210754 [para:210724.1.1,210512.1.1.1,demod:209346] equal(sk_c3,identity) | $spltprd0($spltcnst22).
% 210778 [para:210724.1.1,210748.1.2] -equal(sk_c8,identity) | $spltprd0($spltcnst22).
% 210782 [para:210754.1.1,209351.1.1.1,demod:209346,binarycut:210748] equal(multiply(sk_c6,sk_c9),sk_c7) | $spltprd0($spltcnst22).
% 210784 [para:210754.1.1,209352.1.1.1,demod:209346,binarycut:210748] equal(multiply(sk_c9,sk_c7),sk_c8) | $spltprd0($spltcnst22).
% 210843 [para:210782.1.1,210125.1.1] equal(sk_c7,identity) | $spltprd0($spltcnst22).
% 210871 [para:210724.1.1,210784.1.1.1,demod:209346] equal(sk_c7,sk_c8) | $spltprd0($spltcnst22).
% 210877 [para:210871.1.1,210843.1.1,binarycut:210778] $spltprd0($spltcnst22).
% 210903 [para:210031.2.2,209347.1.1] equal(multiply(sk_c6,sk_c9),identity) | $spltprd0($spltcnst23).
% 210906 [para:210031.2.2,209712.1.2] $spltprd0($spltcnst23) | equal(X,multiply(sk_c6,multiply(sk_c9,X))).
% 210908 [para:210031.2.2,209998.1.2] equal(sk_c6,multiply(sk_c6,identity)) | $spltprd0($spltcnst23).
% 210919 [para:210903.1.1,209358.1.1] equal(inverse(sk_c3),sk_c9) | equal(identity,sk_c7) | $spltprd0($spltcnst23).
% 210923 [para:210903.1.1,209365.1.1] equal(inverse(sk_c2),sk_c9) | equal(identity,sk_c7) | $spltprd0($spltcnst23).
% 210934 [para:210903.1.1,209396.2.1,binarycut:209642] -equal(identity,sk_c8) | $spltprd0($spltcnst23).
% 211020 [para:210033.2.2,209347.1.1] equal(multiply(sk_c5,sk_c8),identity) | $spltprd0($spltcnst23).
% 211034 [para:211020.1.1,209361.1.1] equal(inverse(sk_c3),sk_c9) | equal(identity,sk_c9) | $spltprd0($spltcnst23).
% 211036 [para:211020.1.1,209368.1.1] equal(inverse(sk_c2),sk_c9) | equal(identity,sk_c9) | $spltprd0($spltcnst23).
% 211072 [para:211034.2.2,209359.1.1.1,demod:209346] equal(inverse(sk_c3),sk_c9) | equal(sk_c7,sk_c8) | $spltprd0($spltcnst23).
% 211093 [para:211036.2.2,209366.1.1.1,demod:209346] equal(inverse(sk_c2),sk_c9) | equal(sk_c7,sk_c8) | $spltprd0($spltcnst23).
% 211148 [para:210919.2.1,211072.2.2,binarycut:210934] equal(inverse(sk_c3),sk_c9) | $spltprd0($spltcnst23).
% 211150 [para:211148.1.1,209347.1.1.1] equal(multiply(sk_c9,sk_c3),identity) | $spltprd0($spltcnst23).
% 211154 [para:211150.1.1,210906.2.2.2] equal(sk_c3,multiply(sk_c6,identity)) | $spltprd0($spltcnst23).
% 211159 [para:211154.1.2,209348.1.1.1,demod:209346] $spltprd0($spltcnst23) | equal(multiply(sk_c3,X),multiply(sk_c6,X)).
% 211201 [para:211159.2.1,209396.2.1,binarycut:211148] -equal(multiply(sk_c6,sk_c9),sk_c8) | $spltprd0($spltcnst23).
% 211234 [para:210923.2.1,211093.2.2,binarycut:210934] equal(inverse(sk_c2),sk_c9) | $spltprd0($spltcnst23).
% 211236 [para:211234.1.1,209347.1.1.1] equal(multiply(sk_c9,sk_c2),identity) | $spltprd0($spltcnst23).
% 211240 [para:211236.1.1,210906.2.2.2] equal(sk_c2,multiply(sk_c6,identity)) | $spltprd0($spltcnst23).
% 211247 [para:211240.1.2,210908.1.2] equal(sk_c6,sk_c2) | $spltprd0($spltcnst23).
% 211256 [para:211247.1.2,209372.1.1.1,binarycut:211201] equal(multiply(sk_c6,sk_c9),sk_c7) | $spltprd0($spltcnst23).
% 211258 [para:211247.1.2,209373.1.1.1,binarycut:211201] equal(multiply(sk_c9,sk_c7),sk_c8) | $spltprd0($spltcnst23).
% 211260 [para:211247.1.2,209375.1.1.1,binarycut:211201] equal(multiply(sk_c5,sk_c8),sk_c9) | $spltprd0($spltcnst23).
% 211269 [para:209360.2.1,209563.1.1,cut:209345] equal(inverse(sk_c3),sk_c9) | $spltprd0($spltcnst20).
% 211278 [para:211256.1.1,209396.2.1,binarycut:209642] -equal(sk_c7,sk_c8) | $spltprd0($spltcnst23).
% 211309 [para:211260.1.1,211020.1.1] equal(sk_c9,identity) | $spltprd0($spltcnst23).
% 211341 [para:211309.1.1,211258.1.1.1,demod:209346,binarycut:211278] $spltprd0($spltcnst23).
% 211343 [para:209367.2.1,209565.1.1,cut:209345] equal(inverse(sk_c2),sk_c9) | $spltprd0($spltcnst20).
% 211352 [para:209353.2.1,209567.2.1,cut:209345] equal(multiply(sk_c3,sk_c8),sk_c9) | $spltprd0($spltcnst20).
% 211355 [para:209381.2.1,209568.1.1,cut:209345] equal(inverse(sk_c1),sk_c10) | $spltprd0($spltcnst20).
% 211368 [para:209374.2.1,209570.2.1,cut:209345] equal(multiply(sk_c2,sk_c9),sk_c8) | $spltprd0($spltcnst20).
% 211370 [para:209388.2.1,209571.2.1,cut:209345] equal(multiply(sk_c1,sk_c10),sk_c9) | $spltprd0($spltcnst20).
% 211378 [para:211352.1.1,209393.2.1,cut:209345] -equal(inverse(sk_c3),sk_c8) | $spltprd0($spltcnst20).
% 211385 [para:211269.1.1,211378.1.1] -equal(sk_c9,sk_c8) | $spltprd0($spltcnst20).
% 211394 [para:211368.1.1,209712.1.2.2] equal(sk_c9,multiply(inverse(sk_c2),sk_c8)) | $spltprd0($spltcnst20).
% 211398 [para:211370.1.1,209712.1.2.2] equal(sk_c10,multiply(inverse(sk_c1),sk_c9)) | $spltprd0($spltcnst20).
% 211474 [para:211343.1.1,211394.1.2.1] equal(sk_c9,multiply(sk_c9,sk_c8)) | $spltprd0($spltcnst20).
% 211491 [para:211474.1.2,209712.1.2.2,demod:209347] equal(sk_c8,identity) | $spltprd0($spltcnst20).
% 211520 [para:211491.1.1,211385.1.2] -equal(sk_c9,identity) | $spltprd0($spltcnst20).
% 211563 [para:211355.1.1,211398.1.2.1] equal(sk_c10,multiply(sk_c10,sk_c9)) | $spltprd0($spltcnst20).
% 211568 [para:211563.1.2,209712.1.2.2,demod:209347,binarycut:211520] $spltprd0($spltcnst20).
% 211569 [binary:209398,211568,cut:209858,cut:211341,cut:210877,cut:209881] -$spltprd0($spltcnst19).
% 211571 [para:209357.1.1,209890.1.2.1] equal(sk_c8,multiply(sk_c9,sk_c9)) | equal(inverse(sk_c6),sk_c9).
% 211604 [para:209357.2.1,209893.1.2.1] equal(sk_c9,multiply(sk_c9,sk_c7)) | equal(inverse(sk_c3),sk_c9).
% 211609 [para:211604.1.2,209359.1.1] equal(inverse(sk_c3),sk_c9) | equal(sk_c9,sk_c8).
% 211612 [para:211604.1.2,209712.1.2.2,demod:209347] equal(inverse(sk_c3),sk_c9) | equal(sk_c7,identity).
% 211622 [para:211609.2.2,209405.1.1.1] equal(multiply(sk_c9,sk_c5),identity) | equal(inverse(sk_c3),sk_c9).
% 211799 [para:209360.2.1,209897.1.2.1] equal(sk_c8,multiply(sk_c8,sk_c9)) | equal(inverse(sk_c3),sk_c9).
% 211808 [para:211799.1.2,209712.1.2.2,demod:209347] equal(inverse(sk_c3),sk_c9) | equal(sk_c9,identity).
% 211818 [para:211808.2.1,209359.1.1.1,demod:209346] equal(inverse(sk_c3),sk_c9) | equal(sk_c7,sk_c8).
% 211819 [para:211808.2.1,209402.1.1.1,demod:209346] equal(inverse(sk_c3),sk_c9) | equal(sk_c6,identity).
% 211828 [para:211808.2.1,211622.1.1.1,demod:209346] equal(inverse(sk_c3),sk_c9) | equal(sk_c5,identity).
% 211833 [para:211818.1.1,209347.1.1.1] equal(multiply(sk_c9,sk_c3),identity) | equal(sk_c7,sk_c8).
% 211841 [para:211612.2.1,211818.2.1] equal(inverse(sk_c3),sk_c9) | equal(sk_c8,identity).
% 211844 [para:209357.2.1,211819.2.1.1] equal(inverse(identity),sk_c9) | equal(inverse(sk_c3),sk_c9).
% 211857 [para:211828.2.1,209361.1.1.1,demod:209346] equal(inverse(sk_c3),sk_c9) | equal(sk_c8,sk_c9).
% 211859 [para:211828.1.1,209712.1.2.1] equal(sk_c5,identity) | equal(X,multiply(sk_c9,multiply(sk_c3,X))).
% 211868 [para:211841.1.1,209347.1.1.1] equal(multiply(sk_c9,sk_c3),identity) | equal(sk_c8,identity).
% 211871 [para:211857.1.1,209347.1.1.1] equal(multiply(sk_c9,sk_c3),identity) | equal(sk_c8,sk_c9).
% 211877 [para:211844.2.1,209347.1.1.1] equal(multiply(sk_c9,sk_c3),identity) | equal(inverse(identity),sk_c9).
% 211921 [para:211833.1.1,209712.1.2.2] equal(sk_c3,multiply(inverse(sk_c9),identity)) | equal(sk_c7,sk_c8).
% 211995 [para:211871.1.1,209712.1.2.2] equal(sk_c3,multiply(inverse(sk_c9),identity)) | equal(sk_c8,sk_c9).
% 215595 [para:209374.1.1,209756.2.2.2] equal(sk_c9,multiply(sk_c9,sk_c8)) | equal(inverse(sk_c5),sk_c8).
% 216012 [para:209376.1.1,209758.2.2.2] equal(sk_c9,multiply(sk_c9,sk_c8)) | equal(inverse(sk_c4),sk_c10).
% 216130 [para:216012.1.2,209712.1.2.2,demod:209347] equal(inverse(sk_c4),sk_c10) | equal(sk_c8,identity).
% 216175 [para:216130.1.1,209347.1.1.1] equal(multiply(sk_c10,sk_c4),identity) | equal(sk_c8,identity).
% 216194 [para:216175.1.1,209712.1.2.2] equal(sk_c4,multiply(inverse(sk_c10),identity)) | equal(sk_c8,identity).
% 216232 [para:209385.1.1,209762.2.2.2] equal(sk_c10,multiply(sk_c10,sk_c9)) | equal(inverse(sk_c6),sk_c9).
% 216352 [para:209379.1.1,209763.2.2.2] equal(sk_c9,multiply(sk_c9,sk_c7)) | equal(inverse(sk_c1),sk_c10).
% 216445 [para:209388.1.1,209764.2.2.2] equal(sk_c10,multiply(sk_c10,sk_c9)) | equal(inverse(sk_c5),sk_c8).
% 216483 [para:216232.1.2,209712.1.2.2,demod:209347] equal(inverse(sk_c6),sk_c9) | equal(sk_c9,identity).
% 216501 [para:216483.2.1,211571.1.2.1,demod:209346] equal(inverse(sk_c6),sk_c9) | equal(sk_c8,sk_c9).
% 216553 [para:209382.1.1,209765.2.2.2] equal(sk_c8,multiply(sk_c8,sk_c9)) | equal(inverse(sk_c1),sk_c10).
% 216583 [para:216501.1.1,209347.1.1.1] equal(multiply(sk_c9,sk_c6),identity) | equal(sk_c8,sk_c9).
% 216605 [para:209390.1.1,209766.2.2.2] equal(sk_c10,multiply(sk_c10,sk_c9)) | equal(inverse(sk_c4),sk_c10).
% 216844 [para:216583.1.1,209712.1.2.2] equal(sk_c6,multiply(inverse(sk_c9),identity)) | equal(sk_c8,sk_c9).
% 217214 [para:216352.1.2,209712.1.2.2,demod:209347] equal(inverse(sk_c1),sk_c10) | equal(sk_c7,identity).
% 217352 [para:216445.1.2,209712.1.2.2,demod:209347] equal(inverse(sk_c5),sk_c8) | equal(sk_c9,identity).
% 217393 [para:217352.2.1,209404.1.1.1,demod:209346] equal(inverse(sk_c5),sk_c8) | equal(sk_c3,identity).
% 217417 [para:217352.2.1,215595.1.2.1,demod:209346] equal(inverse(sk_c5),sk_c8) | equal(sk_c9,sk_c8).
% 217423 [para:217393.1.1,209347.1.1.1] equal(multiply(sk_c8,sk_c5),identity) | equal(sk_c3,identity).
% 217445 [para:209748.2.1,217393.2.2.2.1,demod:209346] equal(inverse(sk_c5),sk_c8) | equal(X,multiply(sk_c9,X)).
% 217467 [para:217417.1.1,209347.1.1.1] equal(multiply(sk_c8,sk_c5),identity) | equal(sk_c9,sk_c8).
% 217760 [para:209748.2.2,217445.2.2] equal(inverse(sk_c5),sk_c8) | equal(multiply(sk_c3,X),X).
% 217830 [para:216553.1.2,209712.1.2.2,demod:209347] equal(inverse(sk_c1),sk_c10) | equal(sk_c9,identity).
% 217898 [para:217830.1.1,209347.1.1.1] equal(multiply(sk_c10,sk_c1),identity) | equal(sk_c9,identity).
% 217905 [para:217830.2.1,209380.1.1.1,demod:209346] equal(inverse(sk_c1),sk_c10) | equal(sk_c7,sk_c8).
% 217977 [para:217214.2.1,217905.2.1] equal(inverse(sk_c1),sk_c10) | equal(sk_c8,identity).
% 217997 [para:217977.1.1,209347.1.1.1] equal(multiply(sk_c10,sk_c1),identity) | equal(sk_c8,identity).
% 218122 [para:217898.1.1,209712.1.2.2] equal(sk_c1,multiply(inverse(sk_c10),identity)) | equal(sk_c9,identity).
% 218241 [para:217997.1.1,209712.1.2.2] equal(sk_c1,multiply(inverse(sk_c10),identity)) | equal(sk_c8,identity).
% 218398 [para:216605.1.2,209712.1.2.2,demod:209347] equal(inverse(sk_c4),sk_c10) | equal(sk_c9,identity).
% 218405 [para:218398.1.1,209347.1.1.1] equal(multiply(sk_c10,sk_c4),identity) | equal(sk_c9,identity).
% 218516 [para:218405.1.1,209712.1.2.2] equal(sk_c4,multiply(inverse(sk_c10),identity)) | equal(sk_c9,identity).
% 219254 [para:216844.1.2,211995.1.2] equal(sk_c3,sk_c6) | equal(sk_c8,sk_c9).
% 219960 [para:218241.1.2,216194.1.2] equal(sk_c4,sk_c1) | equal(sk_c8,identity).
% 219977 [para:219960.1.2,209391.1.1.1] equal(multiply(sk_c4,sk_c10),sk_c9) | equal(sk_c8,identity).
% 220070 [para:219977.1.1,209712.1.2.2] equal(sk_c10,multiply(inverse(sk_c4),sk_c9)) | equal(sk_c8,identity).
% 220219 [para:218516.1.2,218122.1.2] equal(sk_c1,sk_c4) | equal(sk_c9,identity).
% 220260 [para:220219.1.1,209391.1.1.1] equal(multiply(sk_c4,sk_c10),sk_c9) | equal(sk_c9,identity).
% 220493 [para:220260.1.1,209712.1.2.2] equal(sk_c10,multiply(inverse(sk_c4),sk_c9)) | equal(sk_c9,identity).
% 220870 [para:216130.1.1,220070.1.2.1] equal(sk_c10,multiply(sk_c10,sk_c9)) | equal(sk_c8,identity).
% 220881 [para:220870.1.2,209712.1.2.2,demod:209347] equal(sk_c9,identity) | equal(sk_c8,identity).
% 220981 [para:220881.1.1,211868.1.1.1,demod:209346] equal(sk_c3,identity) | equal(sk_c8,identity).
% 221118 [para:220981.2.1,217423.1.1.1,demod:209346] equal(sk_c5,identity) | equal(sk_c3,identity).
% 221441 [para:211859.2.1,221118.2.2.2.1,demod:209346] equal(sk_c5,identity) | equal(X,multiply(sk_c9,X)).
% 222006 [para:211859.2.2,221441.2.2] equal(sk_c5,identity) | equal(multiply(sk_c3,X),X).
% 222475 [para:222006.1.1,217760.1.1.1,factor] equal(inverse(identity),sk_c8) | equal(multiply(sk_c3,X),X).
% 225233 [para:216605.2.1,220493.1.2.1] equal(sk_c10,multiply(sk_c10,sk_c9)) | equal(sk_c9,identity).
% 225260 [para:225233.1.2,209712.1.2.2,demod:209347] equal(sk_c9,identity).
% 225363 [para:225260.1.1,209392.2.1.1,demod:209346,cut:211569] -equal(multiply(X,sk_c9),Y) | -equal(inverse(X),sk_c9) | -equal(Y,sk_c8).
% 225386 [para:225260.1.1,211871.1.1.1,demod:209346] equal(sk_c3,identity) | equal(sk_c8,sk_c9).
% 225390 [para:225260.1.1,211877.1.1.1,demod:209346] equal(inverse(identity),sk_c9) | equal(sk_c3,identity).
% 225764 [para:225386.1.1,209351.1.1.1,demod:209346] equal(multiply(sk_c6,sk_c9),sk_c7) | equal(sk_c8,sk_c9).
% 226441 [para:211844.2.1,225390.2.1.1] equal(inverse(identity),sk_c9).
% 226443 [para:226441.1.1,209712.1.2.1,demod:209346] equal(X,multiply(sk_c9,X)).
% 226446 [para:222475.1.1,226441.1.1] equal(sk_c8,sk_c9) | equal(multiply(sk_c3,X),X).
% 226449 [para:226443.1.2,209712.1.2.2] equal(X,multiply(inverse(sk_c9),X)).
% 226516 [para:211921.1.2,226449.1.2] equal(identity,sk_c3) | equal(sk_c7,sk_c8).
% 226597 [para:226516.1.2,209352.1.1.1,demod:226443,209346] equal(sk_c8,sk_c9) | equal(sk_c7,sk_c8).
% 227472 [para:219254.1.1,226446.2.1.1] equal(sk_c8,sk_c9) | equal(multiply(sk_c6,X),X).
% 228462 [para:227472.1.1,225764.2.1] equal(sk_c7,sk_c9) | equal(sk_c8,sk_c9).
% 228528 [para:226597.2.1,228462.1.1] equal(sk_c8,sk_c9).
% 228558 [para:228528.1.1,217467.1.1.1,demod:226443] equal(sk_c5,identity) | equal(sk_c9,sk_c8).
% 228640 [para:215595.1.1,228558.2.1.1,demod:226443,226441] equal(sk_c9,sk_c8).
% 232206 [binary:209346,225363,demod:226441,cut:209345,cut:228640] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% using first neg lit preferred strategy
% not using sos strategy
% using unit paramodulation strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% clause length limited to 25
% clause depth limited to 3
% seconds given: 30
%
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 5377
% derived clauses: 1554833
% kept clauses: 30580
% kept size sum: 512216
% kept mid-nuclei: 195547
% kept new demods: 206
% forw unit-subs: 319210
% forw double-subs: 340902
% forw overdouble-subs: 87898
% backward subs: 2730
% fast unit cutoff: 9474
% full unit cutoff: 0
% dbl unit cutoff: 429
% real runtime : 50.85
% process. runtime: 50.30
% specific non-discr-tree subsumption statistics:
% tried: 703502
% length fails: 55205
% strength fails: 78716
% predlist fails: 9041
% aux str. fails: 87663
% by-lit fails: 194898
% full subs tried: 213860
% full subs fail: 133801
%
% ; program args: ("/home/graph/tptp/Systems/Gandalf---c-2.6/gandalf" "-time" "600" "/home/graph/tptp/TSTP/PreparedTPTP/otter:hypothesis:set(auto),clear(print_given)---add_equality:r/GRP/GRP251-1+eq_r.in")
%
%------------------------------------------------------------------------------