%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP314-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 20.0s
% Output : Assurance 20.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/GRP314-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(sk_c7,sk_c8),sk_c6) | -equal(multiply(X,sk_c8),sk_c7) | -equal(inverse(X),sk_c8) | -equal(multiply(Y,sk_c7),sk_c6) | -equal(inverse(Y),sk_c7) | -equal(multiply(Z,sk_c7),sk_c8) | -equal(inverse(Z),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8) | -equal(inverse(V),sk_c7) | -equal(multiply(V,sk_c6),sk_c7).
% was split for some strategies as:
% -equal(inverse(V),sk_c7) | -equal(multiply(V,sk_c6),sk_c7).
% -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8).
% -equal(multiply(Z,sk_c7),sk_c8) | -equal(inverse(Z),sk_c7).
% -equal(multiply(Y,sk_c7),sk_c6) | -equal(inverse(Y),sk_c7).
% -equal(multiply(X,sk_c8),sk_c7) | -equal(inverse(X),sk_c8).
% -equal(multiply(sk_c7,sk_c8),sk_c6).
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(30,40,1,66,0,1,21157,50,241,21193,0,241,42316,50,512,42352,0,512,63489,50,679,63525,0,679,84672,50,860,84672,40,860,84708,0,860,95081,3,1164,95803,4,1311,96531,5,1461,96532,1,1461,96532,50,1461,96532,40,1461,96568,0,1461,96820,3,1763,96829,4,1920,96837,5,2062,96837,1,2062,96837,50,2062,96837,40,2062,96873,0,2062)
%
%
% START OF PROOF
% 96838 [] equal(X,X).
% 96839 [] equal(multiply(identity,X),X).
% 96840 [] equal(multiply(inverse(X),X),identity).
% 96841 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 96843 [] equal(multiply(sk_c5,sk_c6),sk_c7) | equal(inverse(sk_c3),sk_c7).
% 96844 [] equal(inverse(sk_c3),sk_c7) | equal(inverse(sk_c5),sk_c7).
% 96845 [] equal(multiply(sk_c4,sk_c7),sk_c8) | equal(inverse(sk_c3),sk_c7).
% 96846 [] equal(inverse(sk_c3),sk_c7) | equal(inverse(sk_c4),sk_c8).
% 96847 [] equal(multiply(sk_c3,sk_c7),sk_c8) | equal(multiply(sk_c5,sk_c6),sk_c7).
% 96848 [] equal(multiply(sk_c3,sk_c7),sk_c8) | equal(inverse(sk_c5),sk_c7).
% 96849 [] equal(multiply(sk_c3,sk_c7),sk_c8) | equal(multiply(sk_c4,sk_c7),sk_c8).
% 96850 [] equal(multiply(sk_c3,sk_c7),sk_c8) | equal(inverse(sk_c4),sk_c8).
% 96851 [] equal(multiply(sk_c5,sk_c6),sk_c7) | equal(inverse(sk_c2),sk_c7).
% 96852 [] equal(inverse(sk_c2),sk_c7) | equal(inverse(sk_c5),sk_c7).
% 96853 [] equal(multiply(sk_c4,sk_c7),sk_c8) | equal(inverse(sk_c2),sk_c7).
% 96854 [] equal(inverse(sk_c2),sk_c7) | equal(inverse(sk_c4),sk_c8).
% 96855 [] equal(multiply(sk_c2,sk_c7),sk_c6) | equal(multiply(sk_c5,sk_c6),sk_c7).
% 96856 [] equal(multiply(sk_c2,sk_c7),sk_c6) | equal(inverse(sk_c5),sk_c7).
% 96857 [] equal(multiply(sk_c2,sk_c7),sk_c6) | equal(multiply(sk_c4,sk_c7),sk_c8).
% 96858 [] equal(multiply(sk_c2,sk_c7),sk_c6) | equal(inverse(sk_c4),sk_c8).
% 96859 [] equal(multiply(sk_c5,sk_c6),sk_c7) | equal(inverse(sk_c1),sk_c8).
% 96860 [] equal(inverse(sk_c1),sk_c8) | equal(inverse(sk_c5),sk_c7).
% 96861 [] equal(multiply(sk_c4,sk_c7),sk_c8) | equal(inverse(sk_c1),sk_c8).
% 96862 [] equal(inverse(sk_c1),sk_c8) | equal(inverse(sk_c4),sk_c8).
% 96863 [] equal(multiply(sk_c1,sk_c8),sk_c7) | equal(multiply(sk_c5,sk_c6),sk_c7).
% 96864 [] equal(multiply(sk_c1,sk_c8),sk_c7) | equal(inverse(sk_c5),sk_c7).
% 96865 [] equal(multiply(sk_c1,sk_c8),sk_c7) | equal(multiply(sk_c4,sk_c7),sk_c8).
% 96866 [] equal(multiply(sk_c1,sk_c8),sk_c7) | equal(inverse(sk_c4),sk_c8).
% 96867 [] equal(multiply(sk_c7,sk_c8),sk_c6).
% 96868 [?] ?
% 96869 [] $spltprd0($spltcnst17) | -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c8).
% 96870 [] $spltprd0($spltcnst18) | -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7).
% 96871 [] $spltprd0($spltcnst19) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7).
% 96872 [] $spltprd0($spltcnst20) | -equal(multiply(X,sk_c8),sk_c7) | -equal(inverse(X),sk_c8).
% 96873 [] -$spltprd0($spltcnst17) | -$spltprd0($spltcnst16) | -$spltprd0($spltcnst18) | -$spltprd0($spltcnst20) | -$spltprd0($spltcnst19).
% 96890 [para:96860.1.1,96840.1.1.1] equal(multiply(sk_c8,sk_c1),identity) | equal(inverse(sk_c5),sk_c7).
% 96924 [para:96859.2.1,96840.1.1.1] equal(multiply(sk_c8,sk_c1),identity) | equal(multiply(sk_c5,sk_c6),sk_c7).
% 96970 [input:96868,cut:96838] $spltprd0($spltcnst16) | -equal(multiply(X,sk_c6),sk_c7) | -equal(inverse(X),sk_c7).
% 96973 [para:96843.1.1,96970.2.1,cut:96838] -equal(inverse(sk_c5),sk_c7) | equal(inverse(sk_c3),sk_c7) | $spltprd0($spltcnst16).
% 96974 [para:96851.1.1,96970.2.1,cut:96838] -equal(inverse(sk_c5),sk_c7) | equal(inverse(sk_c2),sk_c7) | $spltprd0($spltcnst16).
% 96984 [para:96844.2.1,96973.1.1,cut:96838] equal(inverse(sk_c3),sk_c7) | $spltprd0($spltcnst16).
% 96986 [para:96984.1.1,96840.1.1.1] equal(multiply(sk_c7,sk_c3),identity) | $spltprd0($spltcnst16).
% 96991 [para:96845.1.1,96869.2.1,cut:96838] -equal(inverse(sk_c4),sk_c8) | equal(inverse(sk_c3),sk_c7) | $spltprd0($spltcnst17).
% 96994 [para:96853.1.1,96869.2.1,cut:96838] -equal(inverse(sk_c4),sk_c8) | equal(inverse(sk_c2),sk_c7) | $spltprd0($spltcnst17).
% 97000 [para:96849.2.1,96869.2.1,cut:96838] equal(multiply(sk_c3,sk_c7),sk_c8) | -equal(inverse(sk_c4),sk_c8) | $spltprd0($spltcnst17).
% 97003 [para:96857.2.1,96869.2.1,cut:96838] equal(multiply(sk_c2,sk_c7),sk_c6) | -equal(inverse(sk_c4),sk_c8) | $spltprd0($spltcnst17).
% 97010 [para:96852.2.1,96974.1.1,cut:96838] equal(inverse(sk_c2),sk_c7) | $spltprd0($spltcnst16).
% 97012 [para:97010.1.1,96840.1.1.1] equal(multiply(sk_c7,sk_c2),identity) | $spltprd0($spltcnst16).
% 97019 [para:96845.1.1,96870.2.1,cut:96838] -equal(inverse(sk_c4),sk_c7) | equal(inverse(sk_c3),sk_c7) | $spltprd0($spltcnst18).
% 97021 [para:96848.1.1,96870.2.1,cut:96838,binarycut:96844] equal(inverse(sk_c5),sk_c7) | $spltprd0($spltcnst18).
% 97023 [para:96850.1.1,96870.2.1,cut:96838,binarycut:96846] equal(inverse(sk_c4),sk_c8) | $spltprd0($spltcnst18).
% 97025 [para:96847.1.1,96870.2.1,cut:96838] equal(multiply(sk_c5,sk_c6),sk_c7) | -equal(inverse(sk_c3),sk_c7) | $spltprd0($spltcnst18).
% 97039 [para:97021.1.1,96840.1.1.1] equal(multiply(sk_c7,sk_c5),identity) | $spltprd0($spltcnst18).
% 97041 [para:97023.1.1,96840.1.1.1] equal(multiply(sk_c8,sk_c4),identity) | $spltprd0($spltcnst18).
% 97055 [para:96856.1.1,96871.2.1,cut:96838,binarycut:96852] equal(inverse(sk_c5),sk_c7) | $spltprd0($spltcnst19).
% 97057 [para:96858.1.1,96871.2.1,cut:96838,binarycut:96854] equal(inverse(sk_c4),sk_c8) | $spltprd0($spltcnst19).
% 97069 [para:97055.1.1,96840.1.1.1] equal(multiply(sk_c7,sk_c5),identity) | $spltprd0($spltcnst19).
% 97071 [para:97057.1.1,96840.1.1.1] equal(multiply(sk_c8,sk_c4),identity) | $spltprd0($spltcnst19).
% 97080 [para:96864.1.1,96872.2.1,cut:96838,binarycut:96860] equal(inverse(sk_c5),sk_c7) | $spltprd0($spltcnst20).
% 97082 [para:96866.1.1,96872.2.1,cut:96838,binarycut:96862] equal(inverse(sk_c4),sk_c8) | $spltprd0($spltcnst20).
% 97086 [para:97080.1.1,96840.1.1.1] equal(multiply(sk_c7,sk_c5),identity) | $spltprd0($spltcnst20).
% 97088 [para:97082.1.1,96840.1.1.1] equal(multiply(sk_c8,sk_c4),identity) | $spltprd0($spltcnst20).
% 97092 [para:96867.1.1,96841.1.1.1] equal(multiply(sk_c6,X),multiply(sk_c7,multiply(sk_c8,X))).
% 97093 [para:96840.1.1,96841.1.1.1,demod:96839] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 97142 [para:96986.1.1,96841.1.1.1,demod:96839] $spltprd0($spltcnst16) | equal(X,multiply(sk_c7,multiply(sk_c3,X))).
% 97147 [para:97039.1.1,96841.1.1.1,demod:96839] $spltprd0($spltcnst18) | equal(X,multiply(sk_c7,multiply(sk_c5,X))).
% 97149 [para:97041.1.1,96841.1.1.1,demod:96839] $spltprd0($spltcnst18) | equal(X,multiply(sk_c8,multiply(sk_c4,X))).
% 97150 [para:97069.1.1,96841.1.1.1,demod:96839] $spltprd0($spltcnst19) | equal(X,multiply(sk_c7,multiply(sk_c5,X))).
% 97151 [para:97071.1.1,96841.1.1.1,demod:96839] $spltprd0($spltcnst19) | equal(X,multiply(sk_c8,multiply(sk_c4,X))).
% 97153 [para:97086.1.1,96841.1.1.1,demod:96839] $spltprd0($spltcnst20) | equal(X,multiply(sk_c7,multiply(sk_c5,X))).
% 97154 [para:97088.1.1,96841.1.1.1,demod:96839] $spltprd0($spltcnst20) | equal(X,multiply(sk_c8,multiply(sk_c4,X))).
% 97156 [para:96867.1.1,97093.1.2.2] equal(sk_c8,multiply(inverse(sk_c7),sk_c6)).
% 97222 [para:96986.1.1,97093.1.2.2] equal(sk_c3,multiply(inverse(sk_c7),identity)) | $spltprd0($spltcnst16).
% 97223 [para:97012.1.1,97093.1.2.2] equal(sk_c2,multiply(inverse(sk_c7),identity)) | $spltprd0($spltcnst16).
% 97227 [para:97069.1.1,97093.1.2.2] equal(sk_c5,multiply(inverse(sk_c7),identity)) | $spltprd0($spltcnst19).
% 97239 [para:97156.1.2,96841.1.1.1] equal(multiply(sk_c8,X),multiply(inverse(sk_c7),multiply(sk_c6,X))).
% 97241 [para:97222.1.2,96841.1.1.1,demod:96839] $spltprd0($spltcnst16) | equal(multiply(sk_c3,X),multiply(inverse(sk_c7),X)).
% 97245 [para:97223.1.2,97222.1.2] equal(sk_c3,sk_c2) | $spltprd0($spltcnst16).
% 97346 [para:97071.1.1,97092.1.2.2] equal(multiply(sk_c6,sk_c4),multiply(sk_c7,identity)) | $spltprd0($spltcnst19).
% 97347 [para:97088.1.1,97092.1.2.2] equal(multiply(sk_c6,sk_c4),multiply(sk_c7,identity)) | $spltprd0($spltcnst20).
% 97352 [para:96848.1.1,97142.2.2.2,demod:96867] equal(inverse(sk_c5),sk_c7) | equal(sk_c7,sk_c6) | $spltprd0($spltcnst16).
% 97458 [para:97346.1.2,97093.1.2.2,demod:97239] equal(identity,multiply(sk_c8,sk_c4)) | $spltprd0($spltcnst19).
% 97463 [para:97347.1.2,97093.1.2.2,demod:97239] equal(identity,multiply(sk_c8,sk_c4)) | $spltprd0($spltcnst20).
% 97484 [para:97352.2.1,97156.1.2.1.1,demod:96840] equal(inverse(sk_c5),sk_c7) | equal(sk_c8,identity) | $spltprd0($spltcnst16).
% 97513 [para:97484.2.1,96890.1.1.1,demod:96839] equal(inverse(sk_c5),sk_c7) | equal(sk_c1,identity) | $spltprd0($spltcnst16).
% 97542 [para:97513.2.1,96864.1.1.1,demod:96839] equal(inverse(sk_c5),sk_c7) | equal(sk_c8,sk_c7) | $spltprd0($spltcnst16).
% 97669 [para:97241.2.2,96840.1.1] equal(multiply(sk_c3,sk_c7),identity) | $spltprd0($spltcnst16).
% 97678 [para:97241.2.2,97156.1.2] equal(sk_c8,multiply(sk_c3,sk_c6)) | $spltprd0($spltcnst16).
% 97715 [para:97245.1.1,97669.1.1.1] equal(multiply(sk_c2,sk_c7),identity) | $spltprd0($spltcnst16).
% 97726 [para:97678.1.2,96970.2.1,binarycut:96984] -equal(sk_c8,sk_c7) | $spltprd0($spltcnst16).
% 97739 [para:97542.2.2,97726.1.2,cut:96838] equal(inverse(sk_c5),sk_c7) | $spltprd0($spltcnst16).
% 97742 [para:97739.1.1,96840.1.1.1] equal(multiply(sk_c7,sk_c5),identity) | $spltprd0($spltcnst16).
% 97813 [para:97742.1.1,97093.1.2.2] equal(sk_c5,multiply(inverse(sk_c7),identity)) | $spltprd0($spltcnst16).
% 97872 [para:97813.1.2,97222.1.2] equal(sk_c3,sk_c5) | $spltprd0($spltcnst16).
% 97882 [para:97872.1.1,97678.1.2.1] equal(sk_c8,multiply(sk_c5,sk_c6)) | $spltprd0($spltcnst16).
% 97916 [para:96847.1.2,97882.2.1,binarycut:97726] equal(multiply(sk_c3,sk_c7),sk_c8) | $spltprd0($spltcnst16).
% 97918 [para:96855.1.2,97882.2.1,binarycut:97726] equal(multiply(sk_c2,sk_c7),sk_c6) | $spltprd0($spltcnst16).
% 97955 [para:97916.1.1,97142.2.2.2,demod:96867] equal(sk_c7,sk_c6) | $spltprd0($spltcnst16).
% 97956 [para:97916.1.1,97669.1.1] equal(sk_c8,identity) | $spltprd0($spltcnst16).
% 97997 [para:97955.1.1,97726.1.2] -equal(sk_c8,sk_c6) | $spltprd0($spltcnst16).
% 98032 [para:97956.1.1,97997.1.1] -equal(identity,sk_c6) | $spltprd0($spltcnst16).
% 98084 [para:97715.1.1,97918.1.1,binarycut:98032] $spltprd0($spltcnst16).
% 98089 [para:96846.2.1,96991.1.1,cut:96838] equal(inverse(sk_c3),sk_c7) | $spltprd0($spltcnst17).
% 98091 [para:98089.1.1,96840.1.1.1] equal(multiply(sk_c7,sk_c3),identity) | $spltprd0($spltcnst17).
% 98096 [para:98091.1.1,97093.1.2.2] equal(sk_c3,multiply(inverse(sk_c7),identity)) | $spltprd0($spltcnst17).
% 98102 [para:96854.2.1,96994.1.1,cut:96838] equal(inverse(sk_c2),sk_c7) | $spltprd0($spltcnst17).
% 98104 [para:98102.1.1,96840.1.1.1] equal(multiply(sk_c7,sk_c2),identity) | $spltprd0($spltcnst17).
% 98109 [para:98104.1.1,97093.1.2.2] equal(sk_c2,multiply(inverse(sk_c7),identity)) | $spltprd0($spltcnst17).
% 98157 [para:98109.1.2,98096.1.2] equal(sk_c3,sk_c2) | $spltprd0($spltcnst17).
% 98186 [para:96850.2.1,97000.2.1,cut:96838] equal(multiply(sk_c3,sk_c7),sk_c8) | $spltprd0($spltcnst17).
% 98194 [para:98186.1.1,96869.2.1,cut:96838] -equal(inverse(sk_c3),sk_c8) | $spltprd0($spltcnst17).
% 98200 [para:98186.1.1,97093.1.2.2] equal(sk_c7,multiply(inverse(sk_c3),sk_c8)) | $spltprd0($spltcnst17).
% 98203 [para:98157.1.1,98186.1.1.1] equal(multiply(sk_c2,sk_c7),sk_c8) | $spltprd0($spltcnst17).
% 98208 [para:98089.1.1,98194.1.1] -equal(sk_c7,sk_c8) | $spltprd0($spltcnst17).
% 98249 [para:96858.2.1,97003.2.1,cut:96838] equal(multiply(sk_c2,sk_c7),sk_c6) | $spltprd0($spltcnst17).
% 98257 [para:98249.1.1,98203.1.1] equal(sk_c6,sk_c8) | $spltprd0($spltcnst17).
% 98288 [para:98257.1.2,98208.1.2] -equal(sk_c7,sk_c6) | $spltprd0($spltcnst17).
% 98333 [para:98089.1.1,98200.1.2.1,demod:96867,binarycut:98288] $spltprd0($spltcnst17).
% 98334 [binary:96873,98333,cut:98084] -$spltprd0($spltcnst20) | -$spltprd0($spltcnst19) | -$spltprd0($spltcnst18).
% 98343 [binary:97153,98334,binarycut:97147,binarycut:97150] equal(X,multiply(sk_c7,multiply(sk_c5,X))).
% 98345 [binary:97154,98334,binarycut:97149,binarycut:97151] equal(X,multiply(sk_c8,multiply(sk_c4,X))).
% 98356 [para:98343.1.2,97093.1.2.2] equal(multiply(sk_c5,X),multiply(inverse(sk_c7),X)).
% 98365 [para:98345.1.2,97093.1.2.2] equal(multiply(sk_c4,X),multiply(inverse(sk_c8),X)).
% 98369 [para:98356.1.2,96840.1.1] equal(multiply(sk_c5,sk_c7),identity).
% 98372 [para:98356.1.2,97156.1.2] equal(sk_c8,multiply(sk_c5,sk_c6)).
% 98384 [para:98369.1.1,96871.2.1,binarycut:97055] -equal(identity,sk_c6) | $spltprd0($spltcnst19).
% 98389 [para:98369.1.1,98343.1.2.2] equal(sk_c7,multiply(sk_c7,identity)).
% 98393 [para:98372.1.2,96859.1.1] equal(inverse(sk_c1),sk_c8) | equal(sk_c8,sk_c7).
% 98407 [para:98389.1.2,97347.1.2] equal(multiply(sk_c6,sk_c4),sk_c7) | $spltprd0($spltcnst20).
% 98442 [para:96843.2.1,97025.2.1,demod:98372,cut:96838] equal(sk_c8,sk_c7) | $spltprd0($spltcnst18).
% 98479 [para:98442.1.2,97019.1.2,binarycut:97023] equal(inverse(sk_c3),sk_c7) | $spltprd0($spltcnst18).
% 98502 [para:96849.1.1,96870.2.1,cut:96838,binarycut:98479] equal(multiply(sk_c4,sk_c7),sk_c8) | $spltprd0($spltcnst18).
% 98503 [para:98502.1.1,96870.2.1,cut:96838] -equal(inverse(sk_c4),sk_c7) | $spltprd0($spltcnst18).
% 98516 [para:97023.1.1,98503.1.1,binarycut:98442] $spltprd0($spltcnst18).
% 98642 [binary:98334,98407.2,cut:98516] equal(multiply(sk_c6,sk_c4),sk_c7) | -$spltprd0($spltcnst19).
% 98661 [binary:97346.2,98642.2,demod:98389] equal(multiply(sk_c6,sk_c4),sk_c7).
% 98662 [para:98661.1.1,97093.1.2.2] equal(sk_c4,multiply(inverse(sk_c6),sk_c7)).
% 98663 [para:98661.1.1,97239.1.2.2,demod:98369,98356] equal(multiply(sk_c8,sk_c4),identity).
% 98664 [para:98663.1.1,97093.1.2.2,demod:98365] equal(sk_c4,multiply(sk_c4,identity)).
% 98683 [para:98365.1.2,96840.1.1] equal(multiply(sk_c4,sk_c8),identity).
% 98686 [para:98365.1.2,97093.1.2] equal(X,multiply(sk_c4,multiply(sk_c8,X))).
% 98690 [para:98683.1.1,96872.2.1,binarycut:97082] -equal(identity,sk_c7) | $spltprd0($spltcnst20).
% 98694 [para:98683.1.1,98345.1.2.2] equal(sk_c8,multiply(sk_c8,identity)).
% 98707 [para:96924.1.1,98686.1.2.2,demod:98372,98664] equal(sk_c1,sk_c4) | equal(sk_c8,sk_c7).
% 98767 [para:98707.2.2,98389.1.2.1,demod:98694] equal(sk_c7,sk_c8) | equal(sk_c1,sk_c4).
% 98786 [para:96862.2.2,98767.2.1.1] equal(inverse(sk_c1),sk_c8) | equal(sk_c7,sk_c8).
% 98853 [para:98786.2.1,96861.1.1.2,demod:98683] equal(inverse(sk_c1),sk_c8) | equal(identity,sk_c8).
% 98857 [para:98853.2.2,96867.1.1.2,demod:98389] equal(inverse(sk_c1),sk_c8) | equal(sk_c7,sk_c6).
% 98910 [para:98393.2.1,98857.2.2] equal(inverse(sk_c1),sk_c8) | equal(sk_c8,sk_c6).
% 99020 [para:98910.2.1,97463.1.2.1,demod:98661,binarycut:98690] equal(inverse(sk_c1),sk_c8) | $spltprd0($spltcnst20).
% 99026 [para:98853.2.1,98910.2.2] equal(inverse(sk_c1),sk_c8) | equal(identity,sk_c6).
% 99035 [binary:98334,99020.2,cut:98516] equal(inverse(sk_c1),sk_c8) | -$spltprd0($spltcnst19).
% 99081 [para:99026.2.2,98384.1.2,cut:96838] equal(inverse(sk_c1),sk_c8) | $spltprd0($spltcnst19).
% 99088 [binary:99035.2,99081.2] equal(inverse(sk_c1),sk_c8).
% 99089 [para:99088.1.1,96840.1.1.1] equal(multiply(sk_c8,sk_c1),identity).
% 99091 [para:99089.1.1,97093.1.2.2,demod:98664,98365] equal(sk_c1,sk_c4).
% 99100 [para:99091.1.2,98664.1.2.1] equal(sk_c4,multiply(sk_c1,identity)).
% 99101 [para:99091.1.2,98683.1.1.1] equal(multiply(sk_c1,sk_c8),identity).
% 99106 [para:99100.1.2,96841.1.1.1,demod:96839] equal(multiply(sk_c4,X),multiply(sk_c1,X)).
% 99111 [para:99101.1.1,96863.1.1,demod:98372] equal(identity,sk_c7) | equal(sk_c8,sk_c7).
% 99134 [para:96865.2.2,99111.2.1.2,demod:99101,98683] equal(identity,sk_c8) | equal(identity,sk_c7).
% 99216 [para:99111.2.2,98690.1.2,binarycut:99134,binarycut:98690] $spltprd0($spltcnst20).
% 99219 [binary:98334,99216,cut:98516] -$spltprd0($spltcnst19).
% 99222 [para:96855.1.1,96871.2.1,cut:96838,cut:99219] equal(multiply(sk_c5,sk_c6),sk_c7) | -equal(inverse(sk_c2),sk_c7).
% 99223 [para:96851.2.1,99222.2.1,demod:98372,cut:96838] equal(sk_c8,sk_c7).
% 99251 [para:99223.1.2,97227.1.2.1.1,demod:98664,98365,cut:99219] equal(sk_c5,sk_c4).
% 99263 [para:99223.1.2,98356.1.2.1.1,demod:99106,98365] equal(multiply(sk_c5,X),multiply(sk_c1,X)).
% 99271 [para:99251.1.1,98369.1.1.1,demod:99106] equal(multiply(sk_c1,sk_c7),identity).
% 99278 [para:96857.1.1,96871.2.1,cut:96838,cut:99219] equal(multiply(sk_c4,sk_c7),sk_c8) | -equal(inverse(sk_c2),sk_c7).
% 99279 [para:96853.2.1,99278.2.1,demod:99271,99106,cut:96838] equal(identity,sk_c8).
% 99280 [para:99279.1.2,96867.1.1.2,demod:98389] equal(sk_c7,sk_c6).
% 99283 [para:99279.1.2,97151.2.2.1,demod:96839,99106,cut:99219] equal(X,multiply(sk_c1,X)).
% 99304 [para:99280.1.1,97150.2.2.1,demod:99283,99263,cut:99219] equal(X,multiply(sk_c6,X)).
% 99305 [para:99280.1.1,97239.1.2.1.1,demod:99304] equal(multiply(sk_c8,X),multiply(inverse(sk_c6),X)).
% 99306 [para:99280.1.1,98356.1.2.1.1,demod:99305,99283,99263] equal(X,multiply(sk_c8,X)).
% 99307 [para:99280.1.1,98662.1.2.2,demod:99306,99305] equal(sk_c4,sk_c6).
% 99320 [para:99307.1.1,97458.1.2.2,demod:99306,cut:99219] equal(identity,sk_c6).
% 99335 [para:99320.1.2,98384.1.2,cut:96838,cut:99219] 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: 3756
% derived clauses: 377049
% kept clauses: 11289
% kept size sum: 210124
% kept mid-nuclei: 78398
% kept new demods: 476
% forw unit-subs: 70734
% forw double-subs: 130077
% forw overdouble-subs: 20862
% backward subs: 483
% fast unit cutoff: 1468
% full unit cutoff: 0
% dbl unit cutoff: 5646
% real runtime : 20.88
% process. runtime: 20.85
% specific non-discr-tree subsumption statistics:
% tried: 378692
% length fails: 56631
% strength fails: 94087
% predlist fails: 1132
% aux str. fails: 25257
% by-lit fails: 17092
% full subs tried: 178510
% full subs fail: 158317
%
% ; 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/GRP314-1+eq_r.in")
%
%------------------------------------------------------------------------------