%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP264-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 : art01.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 30.0s
% Output : Assurance 30.0s
% 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/GRP264-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 21)
% (binary-unit 12 #f)
% (binary-unit-uniteq 12 #f)
% (binary-posweight-kb-big-order 60 #f 3 21)
% (binary-posweight-lex-big-order 30 #f 3 21)
% (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_c9),sk_c8) | -equal(inverse(X),sk_c9) | -equal(multiply(Y,sk_c8),sk_c7) | -equal(inverse(Y),sk_c8) | -equal(multiply(Z,sk_c9),sk_c8) | -equal(inverse(Z),sk_c9) | -equal(multiply(U,sk_c7),sk_c8) | -equal(inverse(U),sk_c7) | -equal(multiply(sk_c8,V),sk_c7) | -equal(multiply(W,sk_c8),V) | -equal(inverse(W),sk_c8).
% was split for some strategies as:
% -equal(multiply(sk_c8,V),sk_c7) | -equal(multiply(W,sk_c8),V) | -equal(inverse(W),sk_c8).
% -equal(multiply(U,sk_c7),sk_c8) | -equal(inverse(U),sk_c7).
% -equal(multiply(Z,sk_c9),sk_c8) | -equal(inverse(Z),sk_c9).
% -equal(multiply(Y,sk_c8),sk_c7) | -equal(inverse(Y),sk_c8).
% -equal(multiply(X,sk_c9),sk_c8) | -equal(inverse(X),sk_c9).
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(33,40,1,72,0,1,120237,5,1502,120238,1,1502,120238,50,1502,120238,40,1502,120277,0,1502,131984,3,1803,132653,4,1953,134328,5,2103,134329,1,2103,134329,50,2103,134329,40,2103,134368,0,2103,134571,3,2411,134580,4,2564,134587,5,2704,134587,1,2704,134587,50,2704,134587,40,2704,134626,0,2704)
%
%
% START OF PROOF
% 134424 [?] ?
% 134588 [] equal(X,X).
% 134589 [] equal(multiply(identity,X),X).
% 134590 [] equal(multiply(inverse(X),X),identity).
% 134591 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 134593 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c5),sk_c8).
% 134594 [] equal(multiply(sk_c5,sk_c8),sk_c6) | equal(inverse(sk_c2),sk_c8).
% 134595 [] equal(multiply(sk_c8,sk_c6),sk_c7) | equal(inverse(sk_c2),sk_c8).
% 134596 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c4),sk_c7).
% 134597 [] equal(multiply(sk_c4,sk_c7),sk_c8) | equal(inverse(sk_c2),sk_c8).
% 134598 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c3),sk_c9).
% 134600 [] equal(multiply(sk_c2,sk_c8),sk_c7) | equal(inverse(sk_c5),sk_c8).
% 134601 [] equal(multiply(sk_c2,sk_c8),sk_c7) | equal(multiply(sk_c5,sk_c8),sk_c6).
% 134602 [] equal(multiply(sk_c2,sk_c8),sk_c7) | equal(multiply(sk_c8,sk_c6),sk_c7).
% 134603 [] equal(multiply(sk_c2,sk_c8),sk_c7) | equal(inverse(sk_c4),sk_c7).
% 134604 [] equal(multiply(sk_c2,sk_c8),sk_c7) | equal(multiply(sk_c4,sk_c7),sk_c8).
% 134605 [] equal(multiply(sk_c2,sk_c8),sk_c7) | equal(inverse(sk_c3),sk_c9).
% 134607 [] equal(inverse(sk_c1),sk_c9) | equal(inverse(sk_c5),sk_c8).
% 134608 [] equal(multiply(sk_c5,sk_c8),sk_c6) | equal(inverse(sk_c1),sk_c9).
% 134609 [] equal(multiply(sk_c8,sk_c6),sk_c7) | equal(inverse(sk_c1),sk_c9).
% 134610 [] equal(inverse(sk_c1),sk_c9) | equal(inverse(sk_c4),sk_c7).
% 134611 [] equal(multiply(sk_c4,sk_c7),sk_c8) | equal(inverse(sk_c1),sk_c9).
% 134612 [] equal(inverse(sk_c1),sk_c9) | equal(inverse(sk_c3),sk_c9).
% 134613 [] equal(multiply(sk_c3,sk_c9),sk_c8) | equal(inverse(sk_c1),sk_c9).
% 134614 [] equal(multiply(sk_c1,sk_c9),sk_c8) | equal(inverse(sk_c5),sk_c8).
% 134617 [] equal(multiply(sk_c1,sk_c9),sk_c8) | equal(inverse(sk_c4),sk_c7).
% 134618 [] equal(multiply(sk_c1,sk_c9),sk_c8) | equal(multiply(sk_c4,sk_c7),sk_c8).
% 134619 [] equal(multiply(sk_c1,sk_c9),sk_c8) | equal(inverse(sk_c3),sk_c9).
% 134620 [] equal(multiply(sk_c1,sk_c9),sk_c8) | equal(multiply(sk_c3,sk_c9),sk_c8).
% 134621 [] $spltprd0($spltcnst16) | -equal(multiply(sk_c8,X),sk_c7) | -equal(multiply(Y,sk_c8),X) | -equal(inverse(Y),sk_c8).
% 134622 [] $spltprd0($spltcnst17) | -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7).
% 134623 [] $spltprd0($spltcnst18) | -equal(multiply(X,sk_c9),sk_c8) | -equal(inverse(X),sk_c9).
% 134624 [] $spltprd0($spltcnst19) | -equal(multiply(X,sk_c8),sk_c7) | -equal(inverse(X),sk_c8).
% 134625 [] $spltprd0($spltcnst20) | -equal(multiply(X,sk_c9),sk_c8) | -equal(inverse(X),sk_c9).
% 134626 [] -$spltprd0($spltcnst17) | -$spltprd0($spltcnst16) | -$spltprd0($spltcnst18) | -$spltprd0($spltcnst20) | -$spltprd0($spltcnst19).
% 134630 [para:134593.2.1,134590.1.1.1] equal(multiply(sk_c8,sk_c5),identity) | equal(inverse(sk_c2),sk_c8).
% 134639 [para:134607.1.1,134590.1.1.1] equal(multiply(sk_c9,sk_c1),identity) | equal(inverse(sk_c5),sk_c8).
% 134645 [para:134612.1.1,134590.1.1.1] equal(multiply(sk_c9,sk_c1),identity) | equal(inverse(sk_c3),sk_c9).
% 134741 [para:134589.1.1,134622.2.1] -equal(inverse(identity),sk_c7) | -equal(sk_c7,sk_c8) | $spltprd0($spltcnst17).
% 134743 [para:134597.1.1,134622.2.1,cut:134588] -equal(inverse(sk_c4),sk_c7) | equal(inverse(sk_c2),sk_c8) | $spltprd0($spltcnst17).
% 134744 [para:134611.1.1,134622.2.1,cut:134588] -equal(inverse(sk_c4),sk_c7) | equal(inverse(sk_c1),sk_c9) | $spltprd0($spltcnst17).
% 134745 [para:134604.2.1,134622.2.1,cut:134588] equal(multiply(sk_c2,sk_c8),sk_c7) | -equal(inverse(sk_c4),sk_c7) | $spltprd0($spltcnst17).
% 134746 [para:134618.2.1,134622.2.1,cut:134588] equal(multiply(sk_c1,sk_c9),sk_c8) | -equal(inverse(sk_c4),sk_c7) | $spltprd0($spltcnst17).
% 134751 [para:134596.2.1,134743.1.1,cut:134588] equal(inverse(sk_c2),sk_c8) | $spltprd0($spltcnst17).
% 134753 [para:134751.1.1,134590.1.1.1] equal(multiply(sk_c8,sk_c2),identity) | $spltprd0($spltcnst17).
% 134768 [para:134619.1.1,134623.2.1,cut:134588,binarycut:134612] equal(inverse(sk_c3),sk_c9) | $spltprd0($spltcnst18).
% 134776 [para:134620.2.1,134623.2.1,cut:134588,binarycut:134768] equal(multiply(sk_c1,sk_c9),sk_c8) | $spltprd0($spltcnst18).
% 134787 [para:134776.1.1,134623.2.1,cut:134588] -equal(inverse(sk_c1),sk_c9) | $spltprd0($spltcnst18).
% 134789 [para:134589.1.1,134624.2.1] -equal(inverse(identity),sk_c8) | -equal(sk_c8,sk_c7) | $spltprd0($spltcnst19).
% 134793 [para:134600.1.1,134624.2.1,cut:134588,binarycut:134593] equal(inverse(sk_c5),sk_c8) | $spltprd0($spltcnst19).
% 134795 [para:134603.1.1,134624.2.1,cut:134588,binarycut:134596] equal(inverse(sk_c4),sk_c7) | $spltprd0($spltcnst19).
% 134797 [para:134605.1.1,134624.2.1,cut:134588,binarycut:134598] equal(inverse(sk_c3),sk_c9) | $spltprd0($spltcnst19).
% 134802 [para:134608.1.1,134624.2.1,binarycut:134793] equal(inverse(sk_c1),sk_c9) | -equal(sk_c6,sk_c7) | $spltprd0($spltcnst19).
% 134818 [para:134613.2.1,134787.1.1,cut:134588] equal(multiply(sk_c3,sk_c9),sk_c8) | $spltprd0($spltcnst18).
% 134820 [para:134793.1.1,134590.1.1.1] equal(multiply(sk_c8,sk_c5),identity) | $spltprd0($spltcnst19).
% 134822 [para:134795.1.1,134590.1.1.1] equal(multiply(sk_c7,sk_c4),identity) | $spltprd0($spltcnst19).
% 134824 [para:134797.1.1,134590.1.1.1] equal(multiply(sk_c9,sk_c3),identity) | $spltprd0($spltcnst19).
% 134837 [para:134619.1.1,134625.2.1,cut:134588,binarycut:134612] equal(inverse(sk_c3),sk_c9) | $spltprd0($spltcnst20).
% 134845 [para:134620.2.1,134625.2.1,cut:134588,binarycut:134837] equal(multiply(sk_c1,sk_c9),sk_c8) | $spltprd0($spltcnst20).
% 134857 [para:134590.1.1,134591.1.1.1,demod:134589] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 134884 [para:134639.1.1,134591.1.1.1,demod:134589] equal(inverse(sk_c5),sk_c8) | equal(X,multiply(sk_c9,multiply(sk_c1,X))).
% 134890 [para:134645.1.1,134591.1.1.1,demod:134589] equal(inverse(sk_c3),sk_c9) | equal(X,multiply(sk_c9,multiply(sk_c1,X))).
% 134946 [para:134818.1.1,134623.2.1,cut:134588,binarycut:134768] $spltprd0($spltcnst18).
% 134958 [para:134824.1.1,134591.1.1.1,demod:134589] $spltprd0($spltcnst19) | equal(X,multiply(sk_c9,multiply(sk_c3,X))).
% 134963 [para:134845.1.1,134625.2.1,cut:134588] -equal(inverse(sk_c1),sk_c9) | $spltprd0($spltcnst20).
% 134969 [para:134613.2.1,134963.1.1,cut:134588] equal(multiply(sk_c3,sk_c9),sk_c8) | $spltprd0($spltcnst20).
% 135005 [para:134969.1.1,134625.2.1,cut:134588,binarycut:134837] $spltprd0($spltcnst20).
% 135011 [para:134594.1.1,134857.1.2.2] equal(sk_c8,multiply(inverse(sk_c5),sk_c6)) | equal(inverse(sk_c2),sk_c8).
% 135013 [para:134597.1.1,134857.1.2.2] equal(sk_c7,multiply(inverse(sk_c4),sk_c8)) | equal(inverse(sk_c2),sk_c8).
% 135015 [para:134600.1.1,134857.1.2.2] equal(sk_c8,multiply(inverse(sk_c2),sk_c7)) | equal(inverse(sk_c5),sk_c8).
% 135022 [para:134611.1.1,134857.1.2.2] equal(sk_c7,multiply(inverse(sk_c4),sk_c8)) | equal(inverse(sk_c1),sk_c9).
% 135083 [para:134753.1.1,134857.1.2.2] equal(sk_c2,multiply(inverse(sk_c8),identity)) | $spltprd0($spltcnst17).
% 135084 [para:134820.1.1,134857.1.2.2] equal(sk_c5,multiply(inverse(sk_c8),identity)) | $spltprd0($spltcnst19).
% 135085 [para:134822.1.1,134857.1.2.2] equal(sk_c4,multiply(inverse(sk_c7),identity)) | $spltprd0($spltcnst19).
% 135088 [para:134824.1.1,134857.1.2.2] equal(sk_c3,multiply(inverse(sk_c9),identity)) | $spltprd0($spltcnst19).
% 135103 [para:135083.1.2,134591.1.1.1,demod:134589] $spltprd0($spltcnst17) | equal(multiply(sk_c2,X),multiply(inverse(sk_c8),X)).
% 135105 [para:135084.1.2,134591.1.1.1,demod:134589] $spltprd0($spltcnst19) | equal(multiply(sk_c5,X),multiply(inverse(sk_c8),X)).
% 135121 [para:135085.1.2,134591.1.1.1,demod:134589] $spltprd0($spltcnst19) | equal(multiply(sk_c4,X),multiply(inverse(sk_c7),X)).
% 135176 [para:135103.2.2,134590.1.1] equal(multiply(sk_c2,sk_c8),identity) | $spltprd0($spltcnst17).
% 135356 [para:135105.2.2,134590.1.1] equal(multiply(sk_c5,sk_c8),identity) | $spltprd0($spltcnst19).
% 135364 [para:135356.1.1,134594.1.1] equal(inverse(sk_c2),sk_c8) | equal(identity,sk_c6) | $spltprd0($spltcnst19).
% 135375 [para:135356.1.1,134624.2.1,binarycut:134793] -equal(identity,sk_c7) | $spltprd0($spltcnst19).
% 135437 [para:135121.2.2,134590.1.1] equal(multiply(sk_c4,sk_c7),identity) | $spltprd0($spltcnst19).
% 135445 [para:135437.1.1,134597.1.1] equal(inverse(sk_c2),sk_c8) | equal(identity,sk_c8) | $spltprd0($spltcnst19).
% 135447 [para:135437.1.1,134611.1.1] equal(inverse(sk_c1),sk_c9) | equal(identity,sk_c8) | $spltprd0($spltcnst19).
% 135482 [para:135445.2.2,134595.1.1.1,demod:134589] equal(inverse(sk_c2),sk_c8) | equal(sk_c6,sk_c7) | $spltprd0($spltcnst19).
% 135508 [para:135447.2.2,134609.1.1.1,demod:134589] equal(inverse(sk_c1),sk_c9) | equal(sk_c6,sk_c7) | $spltprd0($spltcnst19).
% 135537 [para:135364.2.1,135482.2.2,binarycut:135375] equal(inverse(sk_c2),sk_c8) | $spltprd0($spltcnst19).
% 135539 [para:135537.1.1,134590.1.1.1] equal(multiply(sk_c8,sk_c2),identity) | $spltprd0($spltcnst19).
% 135626 [para:135508.2.1,134802.2.1,cut:134588] equal(inverse(sk_c1),sk_c9) | $spltprd0($spltcnst19).
% 135628 [para:135626.1.1,134590.1.1.1] equal(multiply(sk_c9,sk_c1),identity) | $spltprd0($spltcnst19).
% 135631 [para:135628.1.1,134857.1.2.2] equal(sk_c1,multiply(inverse(sk_c9),identity)) | $spltprd0($spltcnst19).
% 135634 [para:135631.1.2,135088.1.2] equal(sk_c3,sk_c1) | $spltprd0($spltcnst19).
% 135642 [para:135634.1.2,134620.1.1.1] equal(multiply(sk_c3,sk_c9),sk_c8) | $spltprd0($spltcnst19).
% 135647 [para:135642.1.1,134958.2.2.2] equal(sk_c9,multiply(sk_c9,sk_c8)) | $spltprd0($spltcnst19).
% 135651 [para:135647.1.2,134857.1.2.2,demod:134590] equal(sk_c8,identity) | $spltprd0($spltcnst19).
% 135673 [para:135651.1.1,134789.1.2,cut:134424] -equal(sk_c8,sk_c7) | $spltprd0($spltcnst19).
% 135681 [para:135651.1.1,135539.1.1.1,demod:134589] equal(sk_c2,identity) | $spltprd0($spltcnst19).
% 135705 [para:135681.1.1,134601.1.1.1,demod:134589,binarycut:135673] equal(multiply(sk_c5,sk_c8),sk_c6) | $spltprd0($spltcnst19).
% 135707 [para:135681.1.1,134602.1.1.1,demod:134589,binarycut:135673] equal(multiply(sk_c8,sk_c6),sk_c7) | $spltprd0($spltcnst19).
% 135761 [para:135705.1.1,134624.2.1,binarycut:134793] -equal(sk_c6,sk_c7) | $spltprd0($spltcnst19).
% 135789 [para:135651.1.1,135707.1.1.1,demod:134589,binarycut:135761] $spltprd0($spltcnst19).
% 135796 [para:134610.2.1,134744.1.1,cut:134588] equal(inverse(sk_c1),sk_c9) | $spltprd0($spltcnst17).
% 135810 [para:134603.2.1,134745.2.1,cut:134588] equal(multiply(sk_c2,sk_c8),sk_c7) | $spltprd0($spltcnst17).
% 135816 [para:135810.1.1,135176.1.1] equal(sk_c7,identity) | $spltprd0($spltcnst17).
% 135825 [para:135816.1.1,134741.1.2,cut:134424] -equal(sk_c7,sk_c8) | $spltprd0($spltcnst17).
% 135839 [para:134617.2.1,134746.2.1,cut:134588] equal(multiply(sk_c1,sk_c9),sk_c8) | $spltprd0($spltcnst17).
% 135855 [para:135839.1.1,134857.1.2.2] equal(sk_c9,multiply(inverse(sk_c1),sk_c8)) | $spltprd0($spltcnst17).
% 135884 [para:135796.1.1,135855.1.2.1] equal(sk_c9,multiply(sk_c9,sk_c8)) | $spltprd0($spltcnst17).
% 135888 [para:135884.1.2,134857.1.2.2,demod:134590] equal(sk_c8,identity) | $spltprd0($spltcnst17).
% 135916 [para:135888.1.1,135825.1.2,binarycut:135816] $spltprd0($spltcnst17).
% 135917 [binary:134626,135916,cut:134946,cut:135005,cut:135789] -$spltprd0($spltcnst16).
% 135919 [para:134593.2.1,135011.1.2.1] equal(sk_c8,multiply(sk_c8,sk_c6)) | equal(inverse(sk_c2),sk_c8).
% 135924 [para:135919.1.2,134595.1.1] equal(inverse(sk_c2),sk_c8) | equal(sk_c8,sk_c7).
% 135930 [para:135924.1.1,134590.1.1.1] equal(multiply(sk_c8,sk_c2),identity) | equal(sk_c8,sk_c7).
% 135965 [para:135930.1.1,134857.1.2.2] equal(sk_c2,multiply(inverse(sk_c8),identity)) | equal(sk_c8,sk_c7).
% 136089 [para:134596.2.1,135013.1.2.1] equal(sk_c7,multiply(sk_c7,sk_c8)) | equal(inverse(sk_c2),sk_c8).
% 136098 [para:136089.1.2,134857.1.2.2,demod:134590] equal(inverse(sk_c2),sk_c8) | equal(sk_c8,identity).
% 136109 [para:136098.2.1,134630.1.1.1,demod:134589] equal(inverse(sk_c2),sk_c8) | equal(sk_c5,identity).
% 136134 [para:134593.2.1,136109.2.1.1] equal(inverse(identity),sk_c8) | equal(inverse(sk_c2),sk_c8).
% 136167 [para:136134.2.1,134590.1.1.1] equal(multiply(sk_c8,sk_c2),identity) | equal(inverse(identity),sk_c8).
% 136829 [para:134593.1.1,135015.1.2.1] equal(sk_c8,multiply(sk_c8,sk_c7)) | equal(inverse(sk_c5),sk_c8).
% 137848 [para:134610.2.1,135022.1.2.1] equal(sk_c7,multiply(sk_c7,sk_c8)) | equal(inverse(sk_c1),sk_c9).
% 137859 [para:137848.1.2,134857.1.2.2,demod:134590] equal(inverse(sk_c1),sk_c9) | equal(sk_c8,identity).
% 137869 [para:137859.1.1,134590.1.1.1] equal(multiply(sk_c9,sk_c1),identity) | equal(sk_c8,identity).
% 138004 [para:137869.1.1,134857.1.2.2] equal(sk_c1,multiply(inverse(sk_c9),identity)) | equal(sk_c8,identity).
% 138252 [para:134614.1.1,134884.2.2.2] equal(sk_c9,multiply(sk_c9,sk_c8)) | equal(inverse(sk_c5),sk_c8).
% 138748 [para:134619.1.1,134890.2.2.2] equal(sk_c9,multiply(sk_c9,sk_c8)) | equal(inverse(sk_c3),sk_c9).
% 139176 [para:138252.1.2,134857.1.2.2,demod:134590] equal(inverse(sk_c5),sk_c8) | equal(sk_c8,identity).
% 139204 [para:139176.2.1,136829.1.2.1,demod:134589] equal(inverse(sk_c5),sk_c8) | equal(sk_c8,sk_c7).
% 139228 [para:139204.1.1,134590.1.1.1] equal(multiply(sk_c8,sk_c5),identity) | equal(sk_c8,sk_c7).
% 141440 [para:138748.1.2,134857.1.2.2,demod:134590] equal(inverse(sk_c3),sk_c9) | equal(sk_c8,identity).
% 141453 [para:141440.1.1,134590.1.1.1] equal(multiply(sk_c9,sk_c3),identity) | equal(sk_c8,identity).
% 141547 [para:141453.1.1,134857.1.2.2] equal(sk_c3,multiply(inverse(sk_c9),identity)) | equal(sk_c8,identity).
% 142434 [para:141547.1.2,138004.1.2] equal(sk_c1,sk_c3) | equal(sk_c8,identity).
% 142458 [para:142434.1.1,134620.1.1.1] equal(multiply(sk_c3,sk_c9),sk_c8) | equal(sk_c8,identity).
% 142629 [para:142458.1.1,134857.1.2.2] equal(sk_c9,multiply(inverse(sk_c3),sk_c8)) | equal(sk_c8,identity).
% 143009 [para:138748.2.1,142629.1.2.1] equal(sk_c9,multiply(sk_c9,sk_c8)) | equal(sk_c8,identity).
% 143024 [para:143009.1.2,134857.1.2.2,demod:134590] equal(sk_c8,identity).
% 143099 [para:143024.1.1,135930.1.1.1,demod:134589] equal(sk_c2,identity) | equal(sk_c8,sk_c7).
% 143111 [para:143024.1.1,136167.1.1.1,demod:134589] equal(inverse(identity),sk_c8) | equal(sk_c2,identity).
% 143141 [para:143024.1.1,139228.1.1.1,demod:134589] equal(sk_c5,identity) | equal(sk_c8,sk_c7).
% 143162 [para:143099.1.1,134601.1.1.1,demod:134589] equal(multiply(sk_c5,sk_c8),sk_c6) | equal(sk_c8,sk_c7).
% 143564 [para:136134.2.1,143111.2.1.1] equal(inverse(identity),sk_c8).
% 143566 [para:143564.1.1,134857.1.2.1,demod:134589] equal(X,multiply(sk_c8,X)).
% 143592 [para:143566.1.2,134857.1.2.2] equal(X,multiply(inverse(sk_c8),X)).
% 143630 [para:135965.1.2,143592.1.2] equal(identity,sk_c2) | equal(sk_c8,sk_c7).
% 143650 [para:143630.1.2,134602.1.1.1,demod:143566,134589] equal(sk_c8,sk_c7) | equal(sk_c6,sk_c7).
% 144592 [para:143141.1.1,143162.1.1.1,demod:134589] equal(sk_c8,sk_c6) | equal(sk_c8,sk_c7).
% 144616 [para:143650.1.2,144592.2.1] equal(sk_c8,sk_c7).
% 144640 [para:144616.1.2,134621.2.2,demod:143566,cut:135917,factor] -equal(multiply(X,sk_c8),inverse(X)) | -equal(inverse(X),sk_c8).
% 146192 [para:134589.1.1,144640.1.1,demod:143564,cut:134588] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% using first neg lit preferred strategy
% not using sos 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 21
% clause depth limited to 3
% seconds given: 30
%
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 4345
% derived clauses: 1317562
% kept clauses: 20291
% kept size sum: 347562
% kept mid-nuclei: 120669
% kept new demods: 189
% forw unit-subs: 184680
% forw double-subs: 180892
% forw overdouble-subs: 58717
% backward subs: 1142
% fast unit cutoff: 5162
% full unit cutoff: 0
% dbl unit cutoff: 649
% real runtime : 32.84
% process. runtime: 32.75
% specific non-discr-tree subsumption statistics:
% tried: 420817
% length fails: 33311
% strength fails: 53422
% predlist fails: 2492
% aux str. fails: 45164
% by-lit fails: 93813
% full subs tried: 174350
% full subs fail: 117800
%
% ; 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/GRP264-1+eq_r.in")
%
%------------------------------------------------------------------------------