%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP339-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 : art04.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 198.7s
% Output : Assurance 198.7s
% 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/GRP339-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 27)
% (binary-unit 12 #f)
% (binary-unit-uniteq 12 #f)
% (binary-posweight-kb-big-order 60 #f 3 27)
% (binary-posweight-lex-big-order 30 #f 3 27)
% (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(sk_c8,sk_c9),sk_c7) | -equal(inverse(X),sk_c9) | -equal(multiply(X,sk_c8),sk_c9) | -equal(multiply(Y,sk_c8),sk_c9) | -equal(inverse(Y),sk_c8) | -equal(multiply(Z,sk_c9),sk_c8) | -equal(inverse(Z),sk_c9) | -equal(inverse(sk_c8),sk_c7) | -equal(multiply(sk_c9,sk_c7),sk_c8) | -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8) | -equal(inverse(V),W) | -equal(inverse(W),sk_c9) | -equal(multiply(V,sk_c9),W).
% was split for some strategies as:
% -equal(inverse(V),W) | -equal(inverse(W),sk_c9) | -equal(multiply(V,sk_c9),W).
% -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8).
% -equal(multiply(Z,sk_c9),sk_c8) | -equal(inverse(Z),sk_c9).
% -equal(multiply(Y,sk_c8),sk_c9) | -equal(inverse(Y),sk_c8).
% -equal(inverse(X),sk_c9) | -equal(multiply(X,sk_c8),sk_c9).
% -equal(multiply(sk_c8,sk_c9),sk_c7).
% -equal(inverse(sk_c8),sk_c7).
% -equal(multiply(sk_c9,sk_c7),sk_c8).
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(42,40,0,90,0,0,52230,5,1501,52230,1,1501,52230,50,1501,52230,40,1501,52278,0,1501,59752,3,1802,60952,4,1952,61803,5,2102,61803,1,2102,61803,50,2102,61803,40,2102,61851,0,2102,63346,3,2414,63410,4,2558,63420,5,2703,63420,1,2703,63420,50,2703,63420,40,2703,63468,0,2703,95476,3,4208,96092,4,4954,96493,1,5704,96493,50,5705,96493,40,5705,96541,0,5705,119674,3,6456,120172,4,6831,120740,5,7206,120741,1,7206,120741,50,7206,120741,40,7206,120789,0,7206,135142,3,7973,136107,4,8332,137204,5,8707,137205,1,8707,137205,50,8707,137205,40,8707,137253,0,8707,220848,3,12610,221743,4,14559,222587,1,16508,222587,50,16511,222587,40,16511,222635,0,16511,280157,3,19062,280900,4,20337)
%
%
% START OF PROOF
% 222588 [] equal(X,X).
% 222589 [] equal(multiply(identity,X),X).
% 222590 [] equal(multiply(inverse(X),X),identity).
% 222591 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 222596 [] equal(multiply(sk_c4,sk_c7),sk_c8) | equal(inverse(sk_c2),sk_c8).
% 222597 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c4),sk_c8).
% 222599 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c8),sk_c7).
% 222600 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c3),sk_c9).
% 222601 [] equal(multiply(sk_c3,sk_c9),sk_c8) | equal(inverse(sk_c2),sk_c8).
% 222605 [] equal(multiply(sk_c2,sk_c8),sk_c9) | equal(multiply(sk_c4,sk_c7),sk_c8).
% 222606 [] equal(multiply(sk_c2,sk_c8),sk_c9) | equal(inverse(sk_c4),sk_c8).
% 222608 [] equal(multiply(sk_c2,sk_c8),sk_c9) | equal(inverse(sk_c8),sk_c7).
% 222609 [] equal(multiply(sk_c2,sk_c8),sk_c9) | equal(inverse(sk_c3),sk_c9).
% 222610 [] equal(multiply(sk_c2,sk_c8),sk_c9) | equal(multiply(sk_c3,sk_c9),sk_c8).
% 222614 [] equal(multiply(sk_c1,sk_c8),sk_c9) | equal(multiply(sk_c4,sk_c7),sk_c8).
% 222615 [] equal(multiply(sk_c1,sk_c8),sk_c9) | equal(inverse(sk_c4),sk_c8).
% 222616 [] equal(multiply(sk_c1,sk_c8),sk_c9) | equal(multiply(sk_c9,sk_c7),sk_c8).
% 222617 [] equal(multiply(sk_c1,sk_c8),sk_c9) | equal(inverse(sk_c8),sk_c7).
% 222618 [] equal(multiply(sk_c1,sk_c8),sk_c9) | equal(inverse(sk_c3),sk_c9).
% 222619 [] equal(multiply(sk_c1,sk_c8),sk_c9) | equal(multiply(sk_c3,sk_c9),sk_c8).
% 222623 [] equal(multiply(sk_c4,sk_c7),sk_c8) | equal(inverse(sk_c1),sk_c9).
% 222624 [] equal(inverse(sk_c1),sk_c9) | equal(inverse(sk_c4),sk_c8).
% 222625 [] equal(multiply(sk_c9,sk_c7),sk_c8) | equal(inverse(sk_c1),sk_c9).
% 222626 [] equal(inverse(sk_c1),sk_c9) | equal(inverse(sk_c8),sk_c7).
% 222627 [] equal(inverse(sk_c1),sk_c9) | equal(inverse(sk_c3),sk_c9).
% 222628 [] equal(multiply(sk_c3,sk_c9),sk_c8) | equal(inverse(sk_c1),sk_c9).
% 222629 [] equal(multiply(sk_c8,sk_c9),sk_c7).
% 222630 [?] ?
% 222631 [] $spltprd0($spltcnst37) | -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c8).
% 222632 [] $spltprd0($spltcnst38) | -equal(multiply(X,sk_c9),sk_c8) | -equal(inverse(X),sk_c9).
% 222633 [] $spltprd0($spltcnst39) | -equal(multiply(X,sk_c8),sk_c9) | -equal(inverse(X),sk_c8).
% 222634 [] $spltprd0($spltcnst40) | -equal(multiply(X,sk_c8),sk_c9) | -equal(inverse(X),sk_c9).
% 222635 [] -$spltprd0($spltcnst37) | -$spltprd0($spltcnst36) | -$spltprd0($spltcnst38) | -$spltprd0($spltcnst40) | -$spltprd0($spltcnst39).
% 222645 [para:222597.1.1,222590.1.1.1] equal(multiply(sk_c8,sk_c2),identity) | equal(inverse(sk_c4),sk_c8).
% 222646 [para:222597.2.1,222590.1.1.1] equal(multiply(sk_c8,sk_c4),identity) | equal(inverse(sk_c2),sk_c8).
% 222648 [para:222599.1.1,222590.1.1.1] equal(multiply(sk_c8,sk_c2),identity) | equal(inverse(sk_c8),sk_c7).
% 222649 [para:222599.2.1,222590.1.1.1] equal(multiply(sk_c7,sk_c8),identity) | equal(inverse(sk_c2),sk_c8).
% 222651 [para:222600.1.1,222590.1.1.1] equal(multiply(sk_c8,sk_c2),identity) | equal(inverse(sk_c3),sk_c9).
% 222662 [para:222624.1.1,222590.1.1.1] equal(multiply(sk_c9,sk_c1),identity) | equal(inverse(sk_c4),sk_c8).
% 222665 [para:222626.1.1,222590.1.1.1] equal(multiply(sk_c9,sk_c1),identity) | equal(inverse(sk_c8),sk_c7).
% 222671 [para:222596.2.1,222590.1.1.1] equal(multiply(sk_c8,sk_c2),identity) | equal(multiply(sk_c4,sk_c7),sk_c8).
% 222676 [para:222601.2.1,222590.1.1.1] equal(multiply(sk_c8,sk_c2),identity) | equal(multiply(sk_c3,sk_c9),sk_c8).
% 222751 [input:222630,cut:222588] -equal(multiply(sk_c9,sk_c7),sk_c8) | -equal(inverse(sk_c8),sk_c7) | $spltprd0($spltcnst36) | -equal(multiply(X,sk_c9),Y) | -equal(inverse(Y),sk_c9) | -equal(inverse(X),Y).
% 222763 [para:222589.1.1,222631.2.1] -equal(inverse(identity),sk_c8) | -equal(sk_c7,sk_c8) | $spltprd0($spltcnst37).
% 222765 [para:222596.1.1,222631.2.1,cut:222588] -equal(inverse(sk_c4),sk_c8) | equal(inverse(sk_c2),sk_c8) | $spltprd0($spltcnst37).
% 222767 [para:222605.2.1,222631.2.1,cut:222588] equal(multiply(sk_c2,sk_c8),sk_c9) | -equal(inverse(sk_c4),sk_c8) | $spltprd0($spltcnst37).
% 222768 [para:222623.1.1,222631.2.1,cut:222588] -equal(inverse(sk_c4),sk_c8) | equal(inverse(sk_c1),sk_c9) | $spltprd0($spltcnst37).
% 222771 [para:222614.2.1,222631.2.1,cut:222588] equal(multiply(sk_c1,sk_c8),sk_c9) | -equal(inverse(sk_c4),sk_c8) | $spltprd0($spltcnst37).
% 222778 [para:222597.2.1,222765.1.1,cut:222588] equal(inverse(sk_c2),sk_c8) | $spltprd0($spltcnst37).
% 222780 [para:222778.1.1,222590.1.1.1] equal(multiply(sk_c8,sk_c2),identity) | $spltprd0($spltcnst37).
% 222787 [para:222590.1.1,222632.2.1] -equal(inverse(inverse(sk_c9)),sk_c9) | -equal(identity,sk_c8) | $spltprd0($spltcnst38).
% 222789 [para:222601.1.1,222632.2.1,cut:222588] -equal(inverse(sk_c3),sk_c9) | equal(inverse(sk_c2),sk_c8) | $spltprd0($spltcnst38).
% 222792 [para:222628.1.1,222632.2.1,cut:222588] -equal(inverse(sk_c3),sk_c9) | equal(inverse(sk_c1),sk_c9) | $spltprd0($spltcnst38).
% 222793 [para:222610.2.1,222632.2.1,cut:222588] equal(multiply(sk_c2,sk_c8),sk_c9) | -equal(inverse(sk_c3),sk_c9) | $spltprd0($spltcnst38).
% 222795 [para:222619.2.1,222632.2.1,cut:222588] equal(multiply(sk_c1,sk_c8),sk_c9) | -equal(inverse(sk_c3),sk_c9) | $spltprd0($spltcnst38).
% 222800 [para:222589.1.1,222633.2.1] -equal(inverse(identity),sk_c8) | -equal(sk_c8,sk_c9) | $spltprd0($spltcnst39).
% 222807 [para:222606.1.1,222633.2.1,cut:222588,binarycut:222597] equal(inverse(sk_c4),sk_c8) | $spltprd0($spltcnst39).
% 222809 [para:222608.1.1,222633.2.1,cut:222588,binarycut:222599] equal(inverse(sk_c8),sk_c7) | $spltprd0($spltcnst39).
% 222812 [para:222609.1.1,222633.2.1,cut:222588,binarycut:222600] equal(inverse(sk_c3),sk_c9) | $spltprd0($spltcnst39).
% 222813 [para:222605.1.1,222633.2.1,cut:222588] equal(multiply(sk_c4,sk_c7),sk_c8) | -equal(inverse(sk_c2),sk_c8) | $spltprd0($spltcnst39).
% 222815 [para:222610.1.1,222633.2.1,cut:222588] equal(multiply(sk_c3,sk_c9),sk_c8) | -equal(inverse(sk_c2),sk_c8) | $spltprd0($spltcnst39).
% 222832 [para:222807.1.1,222590.1.1.1] equal(multiply(sk_c8,sk_c4),identity) | $spltprd0($spltcnst39).
% 222835 [para:222590.1.1,222634.2.1] -equal(inverse(inverse(sk_c8)),sk_c9) | -equal(identity,sk_c9) | $spltprd0($spltcnst40).
% 222847 [para:222615.1.1,222634.2.1,cut:222588,binarycut:222624] equal(inverse(sk_c4),sk_c8) | $spltprd0($spltcnst40).
% 222849 [para:222617.1.1,222634.2.1,cut:222588,binarycut:222626] equal(inverse(sk_c8),sk_c7) | $spltprd0($spltcnst40).
% 222857 [para:222614.1.1,222634.2.1,cut:222588] equal(multiply(sk_c4,sk_c7),sk_c8) | -equal(inverse(sk_c1),sk_c9) | $spltprd0($spltcnst40).
% 222858 [para:222616.1.1,222634.2.1,cut:222588] equal(multiply(sk_c9,sk_c7),sk_c8) | -equal(inverse(sk_c1),sk_c9) | $spltprd0($spltcnst40).
% 222867 [para:222809.1.1,222590.1.1.1] equal(multiply(sk_c7,sk_c8),identity) | $spltprd0($spltcnst39).
% 222875 [para:222847.1.1,222590.1.1.1] equal(multiply(sk_c8,sk_c4),identity) | $spltprd0($spltcnst40).
% 222876 [para:222629.1.1,222591.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c8,multiply(sk_c9,X))).
% 222877 [para:222590.1.1,222591.1.1.1,demod:222589] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 222910 [para:222645.1.1,222591.1.1.1,demod:222589] equal(inverse(sk_c4),sk_c8) | equal(X,multiply(sk_c8,multiply(sk_c2,X))).
% 222912 [para:222648.1.1,222591.1.1.1,demod:222589] equal(inverse(sk_c8),sk_c7) | equal(X,multiply(sk_c8,multiply(sk_c2,X))).
% 222913 [para:222649.1.1,222591.1.1.1,demod:222589] equal(inverse(sk_c2),sk_c8) | equal(X,multiply(sk_c7,multiply(sk_c8,X))).
% 222914 [para:222651.1.1,222591.1.1.1,demod:222589] equal(inverse(sk_c3),sk_c9) | equal(X,multiply(sk_c8,multiply(sk_c2,X))).
% 222934 [para:222671.1.1,222591.1.1.1,demod:222589] equal(multiply(sk_c4,sk_c7),sk_c8) | equal(X,multiply(sk_c8,multiply(sk_c2,X))).
% 222938 [para:222676.1.1,222591.1.1.1,demod:222589] equal(multiply(sk_c3,sk_c9),sk_c8) | equal(X,multiply(sk_c8,multiply(sk_c2,X))).
% 222989 [para:222629.1.1,222877.1.2.2] equal(sk_c9,multiply(inverse(sk_c8),sk_c7)).
% 222990 [para:222590.1.1,222877.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 223091 [para:222780.1.1,222877.1.2.2] equal(sk_c2,multiply(inverse(sk_c8),identity)) | $spltprd0($spltcnst37).
% 223095 [para:222832.1.1,222877.1.2.2] equal(sk_c4,multiply(inverse(sk_c8),identity)) | $spltprd0($spltcnst39).
% 223096 [para:222867.1.1,222877.1.2.2] equal(sk_c8,multiply(inverse(sk_c7),identity)) | $spltprd0($spltcnst39).
% 223100 [para:222875.1.1,222877.1.2.2] equal(sk_c4,multiply(inverse(sk_c8),identity)) | $spltprd0($spltcnst40).
% 223103 [para:222877.1.2,222877.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 223202 [para:222809.1.1,223095.1.2.1] equal(sk_c4,multiply(sk_c7,identity)) | $spltprd0($spltcnst39).
% 223209 [para:223202.1.2,222877.1.2.2] equal(identity,multiply(inverse(sk_c7),sk_c4)) | $spltprd0($spltcnst39).
% 223273 [para:222849.1.1,223100.1.2.1] equal(sk_c4,multiply(sk_c7,identity)) | $spltprd0($spltcnst40).
% 223279 [para:223273.1.2,222877.1.2.2] equal(identity,multiply(inverse(sk_c7),sk_c4)) | $spltprd0($spltcnst40).
% 223394 [para:223209.1.2,222877.1.2.2,demod:222990] equal(sk_c4,sk_c7) | $spltprd0($spltcnst39).
% 223410 [para:223394.1.1,222807.1.1.1] equal(inverse(sk_c7),sk_c8) | $spltprd0($spltcnst39).
% 223418 [para:223410.1.1,223096.1.2.1] equal(sk_c8,multiply(sk_c8,identity)) | $spltprd0($spltcnst39).
% 223483 [para:223279.1.2,222877.1.2.2,demod:222990] equal(sk_c4,sk_c7) | $spltprd0($spltcnst40).
% 223500 [para:223483.1.1,222875.1.1.2] equal(multiply(sk_c8,sk_c7),identity) | $spltprd0($spltcnst40).
% 223661 [para:223103.1.2,222590.1.1] equal(multiply(X,inverse(X)),identity).
% 223725 [para:223103.1.2,222990.1.2] equal(X,multiply(X,identity)).
% 223726 [para:223725.1.2,222590.1.1] equal(inverse(identity),identity).
% 223727 [para:223725.1.2,222990.1.2] equal(X,inverse(inverse(X))).
% 223728 [para:223725.1.2,223091.1.2] equal(sk_c2,inverse(sk_c8)) | $spltprd0($spltcnst37).
% 223734 [para:223725.1.2,223095.1.2] equal(sk_c4,inverse(sk_c8)) | $spltprd0($spltcnst39).
% 223743 [para:223725.1.2,223100.1.2] equal(sk_c4,inverse(sk_c8)) | $spltprd0($spltcnst40).
% 223823 [para:223728.1.2,222590.1.1.1] equal(multiply(sk_c2,sk_c8),identity) | $spltprd0($spltcnst37).
% 223893 [para:222812.1.1,223661.1.1.2] equal(multiply(sk_c3,sk_c9),identity) | $spltprd0($spltcnst39).
% 223916 [para:223734.1.2,222989.1.2.1] equal(sk_c9,multiply(sk_c4,sk_c7)) | $spltprd0($spltcnst39).
% 223939 [para:223743.1.2,222989.1.2.1] equal(sk_c9,multiply(sk_c4,sk_c7)) | $spltprd0($spltcnst40).
% 223953 [para:222606.2.1,222767.2.1,cut:222588] equal(multiply(sk_c2,sk_c8),sk_c9) | $spltprd0($spltcnst37).
% 223956 [para:222624.2.1,222768.1.1,cut:222588] equal(inverse(sk_c1),sk_c9) | $spltprd0($spltcnst37).
% 223972 [para:222615.2.1,222771.2.1,cut:222588] equal(multiply(sk_c1,sk_c8),sk_c9) | $spltprd0($spltcnst37).
% 223980 [para:223956.1.1,222990.1.2.1.1,demod:223725] equal(sk_c1,inverse(sk_c9)) | $spltprd0($spltcnst37).
% 224193 [para:223953.1.1,223823.1.1] equal(sk_c9,identity) | $spltprd0($spltcnst37).
% 224194 [para:223823.1.1,223953.1.1] equal(identity,sk_c9) | $spltprd0($spltcnst37).
% 224197 [para:224193.1.1,222629.1.1.2,demod:223725] equal(sk_c8,sk_c7) | $spltprd0($spltcnst37).
% 224224 [para:224193.1.1,223980.1.2.1,demod:223726] equal(sk_c1,identity) | $spltprd0($spltcnst37).
% 224272 [para:224197.1.1,223091.1.2.1.1,demod:223725] equal(sk_c2,inverse(sk_c7)) | $spltprd0($spltcnst37).
% 224329 [para:224272.1.2,222990.1.2.1.1,demod:223725] equal(sk_c7,inverse(sk_c2)) | $spltprd0($spltcnst37).
% 224337 [para:223727.1.2,222787.1.1,cut:222588] -equal(identity,sk_c8) | $spltprd0($spltcnst38).
% 224357 [para:224329.1.2,222778.1.1] equal(sk_c7,sk_c8) | $spltprd0($spltcnst37).
% 224370 [para:224224.1.1,223972.1.1.1,demod:222589] equal(sk_c8,sk_c9) | $spltprd0($spltcnst37).
% 224415 [para:224370.1.1,222763.1.2,demod:223726,binarycut:224357,binarycut:224194] $spltprd0($spltcnst37).
% 224418 [para:222600.2.1,222789.1.1,cut:222588] equal(inverse(sk_c2),sk_c8) | $spltprd0($spltcnst38).
% 224424 [para:224418.1.1,223661.1.1.2] equal(multiply(sk_c2,sk_c8),identity) | $spltprd0($spltcnst38).
% 224458 [para:222627.2.1,222792.1.1,cut:222588] equal(inverse(sk_c1),sk_c9) | $spltprd0($spltcnst38).
% 224462 [para:224458.1.1,222990.1.2.1.1,demod:223725] equal(sk_c1,inverse(sk_c9)) | $spltprd0($spltcnst38).
% 224483 [para:222609.2.1,222793.2.1,cut:222588] equal(multiply(sk_c2,sk_c8),sk_c9) | $spltprd0($spltcnst38).
% 224491 [para:222618.2.1,222795.2.1,cut:222588] equal(multiply(sk_c1,sk_c8),sk_c9) | $spltprd0($spltcnst38).
% 224585 [para:222596.2.1,222813.2.1,cut:222588] equal(multiply(sk_c4,sk_c7),sk_c8) | $spltprd0($spltcnst39).
% 224592 [para:224483.1.1,224424.1.1] equal(sk_c9,identity) | $spltprd0($spltcnst38).
% 224593 [para:224424.1.1,224483.1.1] equal(identity,sk_c9) | $spltprd0($spltcnst38).
% 224625 [para:224592.1.1,224462.1.2.1,demod:223726] equal(sk_c1,identity) | $spltprd0($spltcnst38).
% 224722 [para:222601.2.1,222815.2.1,cut:222588] equal(multiply(sk_c3,sk_c9),sk_c8) | $spltprd0($spltcnst39).
% 224749 [para:224625.1.1,224491.1.1.1,demod:222589] equal(sk_c8,sk_c9) | $spltprd0($spltcnst38).
% 224801 [para:224749.1.1,224337.1.2,binarycut:224593] $spltprd0($spltcnst38).
% 224810 [para:224585.1.1,223916.1.2] equal(sk_c9,sk_c8) | $spltprd0($spltcnst39).
% 224839 [para:224810.1.2,223418.1.2.1,demod:223725] equal(sk_c8,sk_c9) | $spltprd0($spltcnst39).
% 225001 [para:224722.1.1,223893.1.1] equal(sk_c8,identity) | $spltprd0($spltcnst39).
% 225027 [para:225001.1.1,222800.1.2,demod:223726,cut:222588,binarycut:224839] $spltprd0($spltcnst39).
% 225156 [para:222623.2.1,222857.2.1,cut:222588] equal(multiply(sk_c4,sk_c7),sk_c8) | $spltprd0($spltcnst40).
% 225194 [para:225156.1.1,223939.1.2] equal(sk_c9,sk_c8) | $spltprd0($spltcnst40).
% 225196 [para:222625.2.1,222858.2.1,cut:222588] equal(multiply(sk_c9,sk_c7),sk_c8) | $spltprd0($spltcnst40).
% 225225 [para:225194.1.2,223500.1.1.1] equal(multiply(sk_c9,sk_c7),identity) | $spltprd0($spltcnst40).
% 225232 [para:225194.1.2,222835.1.1.1.1,demod:223727,cut:222588] -equal(identity,sk_c9) | $spltprd0($spltcnst40).
% 225377 [binary:222635,224415,cut:225027,cut:224801] -$spltprd0($spltcnst40) | -$spltprd0($spltcnst36).
% 225514 [para:223661.1.1,222876.1.2.2,demod:223725] equal(multiply(sk_c7,inverse(sk_c9)),sk_c8).
% 225765 [para:225514.1.1,222877.1.2.2] equal(inverse(sk_c9),multiply(inverse(sk_c7),sk_c8)).
% 225929 [para:225225.1.1,225196.1.1] equal(identity,sk_c8) | $spltprd0($spltcnst40).
% 225964 [para:225194.1.2,225929.1.2,binarycut:225232] $spltprd0($spltcnst40).
% 225966 [binary:225377,225964] -$spltprd0($spltcnst36).
% 226197 [para:222606.1.1,222910.2.2.2,demod:222629] equal(inverse(sk_c4),sk_c8) | equal(sk_c8,sk_c7).
% 226255 [para:226197.2.1,222989.1.2.1.1,demod:222590] equal(inverse(sk_c4),sk_c8) | equal(sk_c9,identity).
% 226256 [para:226197.1.1,222990.1.2.1.1,demod:223725] equal(sk_c4,inverse(sk_c8)) | equal(sk_c8,sk_c7).
% 226303 [para:222608.1.1,222912.2.2.2,demod:222629] equal(inverse(sk_c8),sk_c7) | equal(sk_c8,sk_c7).
% 226631 [para:222646.1.1,222913.2.2.2,demod:223725] equal(inverse(sk_c2),sk_c8) | equal(sk_c4,sk_c7).
% 226646 [para:226255.2.1,222662.1.1.1,demod:222589] equal(inverse(sk_c4),sk_c8) | equal(sk_c1,identity).
% 226750 [para:222609.1.1,222914.2.2.2,demod:222629] equal(inverse(sk_c3),sk_c9) | equal(sk_c8,sk_c7).
% 226789 [para:226303.2.1,222989.1.2.1.1,demod:222590] equal(inverse(sk_c8),sk_c7) | equal(sk_c9,identity).
% 226798 [para:226303.1.1,226256.1.2] equal(sk_c4,sk_c7) | equal(sk_c8,sk_c7).
% 226842 [para:226798.2.1,222989.1.2.1.1,demod:222590] equal(sk_c9,identity) | equal(sk_c4,sk_c7).
% 227120 [para:222597.2.1,226631.2.1.1] equal(inverse(sk_c7),sk_c8) | equal(inverse(sk_c2),sk_c8).
% 227123 [para:226631.1.1,222990.1.2.1.1,demod:223725] equal(sk_c2,inverse(sk_c8)) | equal(sk_c4,sk_c7).
% 227130 [para:226646.2.1,222615.1.1.1,demod:222589] equal(inverse(sk_c4),sk_c8) | equal(sk_c8,sk_c9).
% 227430 [para:226750.1.1,223661.1.1.2] equal(multiply(sk_c3,sk_c9),identity) | equal(sk_c8,sk_c7).
% 227495 [para:226789.2.1,222665.1.1.1,demod:222589] equal(inverse(sk_c8),sk_c7) | equal(sk_c1,identity).
% 227812 [para:227130.1.1,222990.1.2.1.1,demod:223725] equal(sk_c4,inverse(sk_c8)) | equal(sk_c8,sk_c9).
% 227822 [para:226197.2.1,227130.2.1] equal(inverse(sk_c4),sk_c8) | equal(sk_c9,sk_c7).
% 228951 [para:227495.2.1,222617.1.1.1,demod:222589] equal(inverse(sk_c8),sk_c7) | equal(sk_c8,sk_c9).
% 229632 [para:227822.2.1,225514.1.1.2.1,demod:223661] equal(inverse(sk_c4),sk_c8) | equal(identity,sk_c8).
% 230710 [para:222605.1.1,222934.2.2.2,demod:222629] equal(multiply(sk_c4,sk_c7),sk_c8) | equal(sk_c8,sk_c7).
% 230844 [para:228951.1.1,227812.1.2] equal(sk_c4,sk_c7) | equal(sk_c8,sk_c9).
% 230953 [para:226798.2.1,230844.2.1] equal(sk_c9,sk_c7) | equal(sk_c4,sk_c7).
% 231027 [para:230953.1.1,226842.1.1] equal(sk_c7,identity) | equal(sk_c4,sk_c7).
% 231181 [para:231027.1.1,222989.1.2.2,demod:223725] equal(sk_c9,inverse(sk_c8)) | equal(sk_c4,sk_c7).
% 231526 [para:222610.1.1,222938.2.2.2,demod:222629] equal(multiply(sk_c3,sk_c9),sk_c8) | equal(sk_c8,sk_c7).
% 231643 [para:229632.2.2,222606.1.1.2,demod:223725] equal(inverse(sk_c4),sk_c8) | equal(sk_c2,sk_c9).
% 233389 [para:231181.1.2,227123.1.2] equal(sk_c2,sk_c9) | equal(sk_c4,sk_c7).
% 233520 [para:233389.1.2,230953.1.1] equal(sk_c2,sk_c7) | equal(sk_c4,sk_c7).
% 234024 [para:227822.2.2,231643.2.1] equal(inverse(sk_c4),sk_c8) | equal(sk_c2,sk_c7).
% 236797 [para:233520.2.1,234024.1.1.1] equal(inverse(sk_c7),sk_c8) | equal(sk_c2,sk_c7).
% 249452 [para:236797.2.1,227120.2.1.1] equal(inverse(sk_c7),sk_c8).
% 249453 [para:249452.1.1,222590.1.1.1] equal(multiply(sk_c8,sk_c7),identity).
% 249454 [para:249452.1.1,222877.1.2.1] equal(X,multiply(sk_c8,multiply(sk_c7,X))).
% 249455 [para:249452.1.1,222990.1.2.1.1,demod:223725] equal(sk_c7,inverse(sk_c8)).
% 249456 [para:249452.1.1,223661.1.1.2] equal(multiply(sk_c7,sk_c8),identity).
% 249463 [para:249455.1.2,222989.1.2.1] equal(sk_c9,multiply(sk_c7,sk_c7)).
% 249658 [para:249463.1.2,222591.1.1.1] equal(multiply(sk_c9,X),multiply(sk_c7,multiply(sk_c7,X))).
% 274846 [para:226798.1.1,230710.1.1.1,demod:249463] equal(sk_c9,sk_c8) | equal(sk_c8,sk_c7).
% 274919 [para:274846.2.1,222989.1.2.1.1,demod:249453,249452] equal(sk_c9,identity) | equal(sk_c9,sk_c8).
% 276487 [para:231526.1.1,227430.1.1] equal(sk_c8,identity) | equal(sk_c8,sk_c7).
% 276523 [para:276487.2.1,222989.1.2.1.1,demod:249453,249452] equal(sk_c9,identity) | equal(sk_c8,identity).
% 277193 [para:274919.2.1,276523.2.2] equal(sk_c9,identity).
% 277196 [para:277193.1.1,222629.1.1.2,demod:223725] equal(sk_c8,sk_c7).
% 277213 [para:277193.1.1,222876.1.2.2.1,demod:222589] equal(multiply(sk_c7,X),multiply(sk_c8,X)).
% 277361 [para:277196.1.1,222629.1.1.1] equal(multiply(sk_c7,sk_c9),sk_c7).
% 277363 [para:277196.1.1,222751.1.2,demod:249455,277361,249463,249658,cut:222588,cut:225966] -equal(multiply(X,sk_c9),Y) | -equal(inverse(Y),sk_c9) | -equal(inverse(X),Y).
% 277441 [para:277196.1.1,249454.1.2.1] equal(X,multiply(sk_c7,multiply(sk_c7,X))).
% 280255 [para:223725.1.2,277441.1.2.2,demod:249463] equal(identity,sk_c9).
% 280909 [binary:249658,277363,demod:249456,277213,249452,225765,249463,277361,cut:280255] 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 lex ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 51
%
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 15997
% derived clauses: 3410342
% kept clauses: 202280
% kept size sum: 775080
% kept mid-nuclei: 51886
% kept new demods: 411
% forw unit-subs: 892868
% forw double-subs: 1871593
% forw overdouble-subs: 172581
% backward subs: 7188
% fast unit cutoff: 14287
% full unit cutoff: 0
% dbl unit cutoff: 2332
% real runtime : 206.34
% process. runtime: 204.85
% specific non-discr-tree subsumption statistics:
% tried: 19616138
% length fails: 2637801
% strength fails: 6414045
% predlist fails: 1056512
% aux str. fails: 2722066
% by-lit fails: 2525984
% full subs tried: 1285360
% full subs fail: 1186740
%
% ; 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/GRP339-1+eq_r.in")
%
%------------------------------------------------------------------------------