%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP212-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 299.7s
% Output : Assurance 299.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/GRP212-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,Y),sk_c8) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c7),sk_c8) | -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c7),sk_c8) | -equal(inverse(sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8) | -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(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8).
% -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c7),sk_c8).
% -equal(multiply(X,Y),sk_c8) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c7),sk_c8).
% -equal(inverse(sk_c8),sk_c7).
%
% Starting a split proof attempt with 5 components.
%
% Split component 1 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(X,Y),sk_c8) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c7),sk_c8) | -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c7),sk_c8) | -equal(inverse(sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8) | -equal(multiply(sk_c8,V),sk_c7) | -equal(multiply(W,sk_c8),V) | -equal(inverse(W),sk_c8).
% Split part used next: -equal(multiply(sk_c8,V),sk_c7) | -equal(multiply(W,sk_c8),V) | -equal(inverse(W),sk_c8).
% END OF PROOFPART
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,1,75,0,1,278748,5,1502,278749,1,1502,278749,50,1502,278749,40,1502,278789,0,1502,290386,3,1803,291066,4,1953,291739,5,2103,291740,1,2103,291740,50,2103,291740,40,2103,291780,0,2103,292545,3,2411,292556,4,2565,292617,5,2704,292617,1,2704,292617,50,2704,292617,40,2704,292657,0,2704,322196,3,4205,322938,4,4955,323722,1,5705,323722,50,5706,323722,40,5706,323762,0,5706,342638,3,6457,343249,4,6832,343872,1,7207,343872,50,7207,343872,40,7207,343912,0,7207,356884,3,7986,357576,4,8333,358383,5,8708,358383,1,8708,358383,50,8708,358383,40,8708,358423,0,8708,404870,3,12609,406034,4,14559,406886,5,16509,406887,1,16509,406887,50,16511,406887,40,16511,406927,0,16511,450343,3,19062,451118,4,20337,451670,1,21612,451670,50,21613,451670,40,21613,451710,0,21613,496847,3,23117,497583,4,23864,497638,1,24614,497638,50,24616,497638,40,24616,497678,0,24616,504592,3,25367,506166,4,25743,506573,5,26117,506573,1,26117,506573,50,26117,506573,40,26117,506613,0,26117,543344,3,27319,543902,4,27918,544037,1,28518,544037,50,28520,544037,40,28520,544077,0,28520,572943,3,29271,573410,4,29646,573624,5,30021,573625,1,30021,573625,50,30022,573625,40,30022,573625,40,30022,573660,0,30022)
%
%
% START OF PROOF
% 573626 [] equal(X,X).
% 573627 [] equal(multiply(identity,X),X).
% 573628 [] equal(multiply(inverse(X),X),identity).
% 573629 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 573630 [] -equal(multiply(sk_c8,X),sk_c7) | -equal(multiply(Y,sk_c8),X) | -equal(inverse(Y),sk_c8).
% 573631 [] equal(multiply(sk_c3,sk_c7),sk_c8) | equal(inverse(sk_c5),sk_c8).
% 573632 [] equal(multiply(sk_c3,sk_c7),sk_c8) | equal(multiply(sk_c5,sk_c8),sk_c6).
% 573633 [] equal(multiply(sk_c3,sk_c7),sk_c8) | equal(multiply(sk_c8,sk_c6),sk_c7).
% 573637 [] equal(inverse(sk_c3),sk_c8) | equal(inverse(sk_c5),sk_c8).
% 573638 [] equal(multiply(sk_c5,sk_c8),sk_c6) | equal(inverse(sk_c3),sk_c8).
% 573639 [?] ?
% 573643 [] equal(multiply(sk_c2,sk_c7),sk_c8) | equal(inverse(sk_c5),sk_c8).
% 573644 [] equal(multiply(sk_c2,sk_c7),sk_c8) | equal(multiply(sk_c5,sk_c8),sk_c6).
% 573645 [] equal(multiply(sk_c2,sk_c7),sk_c8) | equal(multiply(sk_c8,sk_c6),sk_c7).
% 573649 [] equal(inverse(sk_c1),sk_c2) | equal(inverse(sk_c5),sk_c8).
% 573650 [] equal(multiply(sk_c5,sk_c8),sk_c6) | equal(inverse(sk_c1),sk_c2).
% 573651 [?] ?
% 573655 [] equal(multiply(sk_c1,sk_c2),sk_c8) | equal(inverse(sk_c5),sk_c8).
% 573656 [] equal(multiply(sk_c1,sk_c2),sk_c8) | equal(multiply(sk_c5,sk_c8),sk_c6).
% 573657 [] equal(multiply(sk_c1,sk_c2),sk_c8) | equal(multiply(sk_c8,sk_c6),sk_c7).
% 573708 [hyper:573630,573638,573637,binarycut:573639] equal(inverse(sk_c3),sk_c8).
% 573715 [para:573708.1.1,573628.1.1.1] equal(multiply(sk_c8,sk_c3),identity).
% 573724 [hyper:573630,573633,573632,573631] equal(multiply(sk_c3,sk_c7),sk_c8).
% 573742 [hyper:573630,573650,573649,binarycut:573651] equal(inverse(sk_c1),sk_c2).
% 573743 [para:573742.1.1,573628.1.1.1] equal(multiply(sk_c2,sk_c1),identity).
% 573748 [hyper:573630,573645,573644,573643] equal(multiply(sk_c2,sk_c7),sk_c8).
% 573767 [hyper:573630,573657,573656,573655] equal(multiply(sk_c1,sk_c2),sk_c8).
% 573768 [para:573628.1.1,573629.1.1.1,demod:573627] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 573769 [para:573715.1.1,573629.1.1.1,demod:573627] equal(X,multiply(sk_c8,multiply(sk_c3,X))).
% 573771 [para:573743.1.1,573629.1.1.1,demod:573627] equal(X,multiply(sk_c2,multiply(sk_c1,X))).
% 573773 [para:573767.1.1,573629.1.1.1] equal(multiply(sk_c8,X),multiply(sk_c1,multiply(sk_c2,X))).
% 573776 [para:573724.1.1,573769.1.2.2] equal(sk_c7,multiply(sk_c8,sk_c8)).
% 573777 [para:573776.1.2,573629.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c8,multiply(sk_c8,X))).
% 573780 [para:573767.1.1,573771.1.2.2] equal(sk_c2,multiply(sk_c2,sk_c8)).
% 573786 [para:573743.1.1,573768.1.2.2] equal(sk_c1,multiply(inverse(sk_c2),identity)).
% 573787 [para:573748.1.1,573768.1.2.2] equal(sk_c7,multiply(inverse(sk_c2),sk_c8)).
% 573789 [para:573771.1.2,573768.1.2.2] equal(multiply(sk_c1,X),multiply(inverse(sk_c2),X)).
% 573806 [para:573789.1.2,573628.1.1,demod:573767] equal(sk_c8,identity).
% 573808 [para:573789.1.2,573768.1.2,demod:573773] equal(X,multiply(sk_c8,X)).
% 573816 [para:573806.1.1,573776.1.2.1,demod:573627] equal(sk_c7,sk_c8).
% 573818 [para:573806.1.1,573787.1.2.2,demod:573786] equal(sk_c7,sk_c1).
% 573822 [para:573816.1.1,573748.1.1.2,demod:573780] equal(sk_c2,sk_c8).
% 573824 [para:573818.1.2,573742.1.1.1] equal(inverse(sk_c7),sk_c2).
% 573840 [hyper:573630,573777,demod:573824,573808,573776,cut:573626,cut:573822] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 6
%
%
% Split component 2 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(X,Y),sk_c8) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c7),sk_c8) | -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c7),sk_c8) | -equal(inverse(sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8) | -equal(multiply(sk_c8,V),sk_c7) | -equal(multiply(W,sk_c8),V) | -equal(inverse(W),sk_c8).
% Split part used next: -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 6
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,1,75,0,1,278748,5,1502,278749,1,1502,278749,50,1502,278749,40,1502,278789,0,1502,290386,3,1803,291066,4,1953,291739,5,2103,291740,1,2103,291740,50,2103,291740,40,2103,291780,0,2103,292545,3,2411,292556,4,2565,292617,5,2704,292617,1,2704,292617,50,2704,292617,40,2704,292657,0,2704,322196,3,4205,322938,4,4955,323722,1,5705,323722,50,5706,323722,40,5706,323762,0,5706,342638,3,6457,343249,4,6832,343872,1,7207,343872,50,7207,343872,40,7207,343912,0,7207,356884,3,7986,357576,4,8333,358383,5,8708,358383,1,8708,358383,50,8708,358383,40,8708,358423,0,8708,404870,3,12609,406034,4,14559,406886,5,16509,406887,1,16509,406887,50,16511,406887,40,16511,406927,0,16511,450343,3,19062,451118,4,20337,451670,1,21612,451670,50,21613,451670,40,21613,451710,0,21613,496847,3,23117,497583,4,23864,497638,1,24614,497638,50,24616,497638,40,24616,497678,0,24616,504592,3,25367,506166,4,25743,506573,5,26117,506573,1,26117,506573,50,26117,506573,40,26117,506613,0,26117,543344,3,27319,543902,4,27918,544037,1,28518,544037,50,28520,544037,40,28520,544077,0,28520,572943,3,29271,573410,4,29646,573624,5,30021,573625,1,30021,573625,50,30022,573625,40,30022,573625,40,30022,573660,0,30022,573839,50,30022,573839,30,30022,573839,40,30022,573874,0,30022)
%
%
% START OF PROOF
% 573840 [] equal(X,X).
% 573844 [] -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c8).
% 573848 [] equal(multiply(sk_c3,sk_c7),sk_c8) | equal(multiply(sk_c4,sk_c7),sk_c8).
% 573849 [?] ?
% 573854 [?] ?
% 573855 [] equal(inverse(sk_c3),sk_c8) | equal(inverse(sk_c4),sk_c8).
% 573884 [hyper:573844,573855,binarycut:573849] equal(inverse(sk_c4),sk_c8).
% 573886 [hyper:573844,573855,binarycut:573854] equal(inverse(sk_c3),sk_c8).
% 573905 [hyper:573844,573848,demod:573886,cut:573840] equal(multiply(sk_c4,sk_c7),sk_c8).
% 573907 [hyper:573844,573905,demod:573884,cut:573840] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 6
%
%
% Split component 3 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(X,Y),sk_c8) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c7),sk_c8) | -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c7),sk_c8) | -equal(inverse(sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8) | -equal(multiply(sk_c8,V),sk_c7) | -equal(multiply(W,sk_c8),V) | -equal(inverse(W),sk_c8).
% Split part used next: -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c7),sk_c8).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 6
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,1,75,0,1,278748,5,1502,278749,1,1502,278749,50,1502,278749,40,1502,278789,0,1502,290386,3,1803,291066,4,1953,291739,5,2103,291740,1,2103,291740,50,2103,291740,40,2103,291780,0,2103,292545,3,2411,292556,4,2565,292617,5,2704,292617,1,2704,292617,50,2704,292617,40,2704,292657,0,2704,322196,3,4205,322938,4,4955,323722,1,5705,323722,50,5706,323722,40,5706,323762,0,5706,342638,3,6457,343249,4,6832,343872,1,7207,343872,50,7207,343872,40,7207,343912,0,7207,356884,3,7986,357576,4,8333,358383,5,8708,358383,1,8708,358383,50,8708,358383,40,8708,358423,0,8708,404870,3,12609,406034,4,14559,406886,5,16509,406887,1,16509,406887,50,16511,406887,40,16511,406927,0,16511,450343,3,19062,451118,4,20337,451670,1,21612,451670,50,21613,451670,40,21613,451710,0,21613,496847,3,23117,497583,4,23864,497638,1,24614,497638,50,24616,497638,40,24616,497678,0,24616,504592,3,25367,506166,4,25743,506573,5,26117,506573,1,26117,506573,50,26117,506573,40,26117,506613,0,26117,543344,3,27319,543902,4,27918,544037,1,28518,544037,50,28520,544037,40,28520,544077,0,28520,572943,3,29271,573410,4,29646,573624,5,30021,573625,1,30021,573625,50,30022,573625,40,30022,573625,40,30022,573660,0,30022,573839,50,30022,573839,30,30022,573839,40,30022,573874,0,30022,573906,50,30022,573906,30,30022,573906,40,30022,573941,0,30028)
%
%
% START OF PROOF
% 573907 [] equal(X,X).
% 573911 [] -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c8).
% 573915 [] equal(multiply(sk_c3,sk_c7),sk_c8) | equal(multiply(sk_c4,sk_c7),sk_c8).
% 573916 [?] ?
% 573921 [?] ?
% 573922 [] equal(inverse(sk_c3),sk_c8) | equal(inverse(sk_c4),sk_c8).
% 573951 [hyper:573911,573922,binarycut:573916] equal(inverse(sk_c4),sk_c8).
% 573953 [hyper:573911,573922,binarycut:573921] equal(inverse(sk_c3),sk_c8).
% 573972 [hyper:573911,573915,demod:573953,cut:573907] equal(multiply(sk_c4,sk_c7),sk_c8).
% 573974 [hyper:573911,573972,demod:573951,cut:573907] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 6
%
%
% Split component 4 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(X,Y),sk_c8) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c7),sk_c8) | -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c7),sk_c8) | -equal(inverse(sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8) | -equal(multiply(sk_c8,V),sk_c7) | -equal(multiply(W,sk_c8),V) | -equal(inverse(W),sk_c8).
% Split part used next: -equal(multiply(X,Y),sk_c8) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c7),sk_c8).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 6
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,1,75,0,1,278748,5,1502,278749,1,1502,278749,50,1502,278749,40,1502,278789,0,1502,290386,3,1803,291066,4,1953,291739,5,2103,291740,1,2103,291740,50,2103,291740,40,2103,291780,0,2103,292545,3,2411,292556,4,2565,292617,5,2704,292617,1,2704,292617,50,2704,292617,40,2704,292657,0,2704,322196,3,4205,322938,4,4955,323722,1,5705,323722,50,5706,323722,40,5706,323762,0,5706,342638,3,6457,343249,4,6832,343872,1,7207,343872,50,7207,343872,40,7207,343912,0,7207,356884,3,7986,357576,4,8333,358383,5,8708,358383,1,8708,358383,50,8708,358383,40,8708,358423,0,8708,404870,3,12609,406034,4,14559,406886,5,16509,406887,1,16509,406887,50,16511,406887,40,16511,406927,0,16511,450343,3,19062,451118,4,20337,451670,1,21612,451670,50,21613,451670,40,21613,451710,0,21613,496847,3,23117,497583,4,23864,497638,1,24614,497638,50,24616,497638,40,24616,497678,0,24616,504592,3,25367,506166,4,25743,506573,5,26117,506573,1,26117,506573,50,26117,506573,40,26117,506613,0,26117,543344,3,27319,543902,4,27918,544037,1,28518,544037,50,28520,544037,40,28520,544077,0,28520,572943,3,29271,573410,4,29646,573624,5,30021,573625,1,30021,573625,50,30022,573625,40,30022,573625,40,30022,573660,0,30022,573839,50,30022,573839,30,30022,573839,40,30022,573874,0,30022,573906,50,30022,573906,30,30022,573906,40,30022,573941,0,30028,573973,50,30028,573973,30,30028,573973,40,30028,574008,0,30028)
%
%
% START OF PROOF
% 573975 [] equal(multiply(identity,X),X).
% 573976 [] equal(multiply(inverse(X),X),identity).
% 573977 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 573978 [] -equal(multiply(X,sk_c7),sk_c8) | -equal(multiply(Y,X),sk_c8) | -equal(inverse(Y),X).
% 573991 [?] ?
% 573992 [?] ?
% 573993 [] equal(multiply(sk_c2,sk_c7),sk_c8) | equal(multiply(sk_c8,sk_c6),sk_c7).
% 573994 [?] ?
% 573995 [?] ?
% 573996 [?] ?
% 573997 [] equal(inverse(sk_c1),sk_c2) | equal(inverse(sk_c5),sk_c8).
% 573998 [] equal(multiply(sk_c5,sk_c8),sk_c6) | equal(inverse(sk_c1),sk_c2).
% 573999 [] equal(multiply(sk_c8,sk_c6),sk_c7) | equal(inverse(sk_c1),sk_c2).
% 574000 [] equal(multiply(sk_c4,sk_c7),sk_c8) | equal(inverse(sk_c1),sk_c2).
% 574001 [] equal(inverse(sk_c1),sk_c2) | equal(inverse(sk_c4),sk_c8).
% 574002 [] equal(inverse(sk_c1),sk_c2) | equal(inverse(sk_c8),sk_c7).
% 574003 [?] ?
% 574004 [?] ?
% 574005 [?] ?
% 574006 [?] ?
% 574007 [?] ?
% 574008 [?] ?
% 574025 [hyper:573978,573997,binarycut:574003,binarycut:573991] equal(inverse(sk_c5),sk_c8).
% 574029 [para:574025.1.1,573976.1.1.1] equal(multiply(sk_c8,sk_c5),identity).
% 574038 [hyper:573978,574001,binarycut:574007,binarycut:573995] equal(inverse(sk_c4),sk_c8).
% 574046 [hyper:573978,574002,binarycut:574008,binarycut:573996] equal(inverse(sk_c8),sk_c7).
% 574050 [para:574046.1.1,573976.1.1.1] equal(multiply(sk_c7,sk_c8),identity).
% 574072 [hyper:573978,573998,binarycut:574004,binarycut:573992] equal(multiply(sk_c5,sk_c8),sk_c6).
% 574089 [hyper:573978,573999,binarycut:574005,binarycut:573993] equal(multiply(sk_c8,sk_c6),sk_c7).
% 574094 [hyper:573978,574000,binarycut:574006,binarycut:573994] equal(multiply(sk_c4,sk_c7),sk_c8).
% 574101 [para:573976.1.1,573977.1.1.1,demod:573975] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 574102 [para:574029.1.1,573977.1.1.1,demod:573975] equal(X,multiply(sk_c8,multiply(sk_c5,X))).
% 574105 [para:574072.1.1,573977.1.1.1] equal(multiply(sk_c6,X),multiply(sk_c5,multiply(sk_c8,X))).
% 574110 [para:574072.1.1,574102.1.2.2,demod:574089] equal(sk_c8,sk_c7).
% 574111 [para:574110.1.2,574050.1.1.1] equal(multiply(sk_c8,sk_c8),identity).
% 574117 [para:574029.1.1,574101.1.2.2,demod:574046] equal(sk_c5,multiply(sk_c7,identity)).
% 574120 [para:574089.1.1,574101.1.2.2,demod:574046] equal(sk_c6,multiply(sk_c7,sk_c7)).
% 574121 [para:574094.1.1,574101.1.2.2,demod:574111,574038] equal(sk_c7,identity).
% 574122 [para:574102.1.2,574101.1.2.2,demod:574046] equal(multiply(sk_c5,X),multiply(sk_c7,X)).
% 574123 [para:574111.1.1,574101.1.2.2,demod:574117,574046] equal(sk_c8,sk_c5).
% 574125 [para:574121.1.1,574050.1.1.1,demod:573975] equal(sk_c8,identity).
% 574127 [para:574123.1.2,574025.1.1.1,demod:574046] equal(sk_c7,sk_c8).
% 574134 [para:574125.1.1,574046.1.1.1] equal(inverse(identity),sk_c7).
% 574135 [para:574125.1.1,574072.1.1.2,demod:574117,574122] equal(sk_c5,sk_c6).
% 574149 [para:574135.1.1,574072.1.1.1] equal(multiply(sk_c6,sk_c8),sk_c6).
% 574157 [para:574111.1.1,574105.1.2.2,demod:574117,574122,574149] equal(sk_c6,sk_c5).
% 574161 [para:574123.1.2,574157.1.2] equal(sk_c6,sk_c8).
% 574164 [hyper:573978,574134,demod:574120,573975,cut:574127,cut:574161] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 6
%
%
% Split component 5 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(X,Y),sk_c8) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c7),sk_c8) | -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c7),sk_c8) | -equal(inverse(sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8) | -equal(multiply(sk_c8,V),sk_c7) | -equal(multiply(W,sk_c8),V) | -equal(inverse(W),sk_c8).
% Split part used next: -equal(inverse(sk_c8),sk_c7).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 6
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 4
% seconds given: 6
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 5
% seconds given: 6
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 6
% seconds given: 6
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 7
% seconds given: 6
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 8
% seconds given: 6
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 9
% seconds given: 6
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 10
% seconds given: 6
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 11
% seconds given: 6
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 12
% seconds given: 6
%
%
% proof attempt stopped: sos exhausted
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,1,75,0,1,278748,5,1502,278749,1,1502,278749,50,1502,278749,40,1502,278789,0,1502,290386,3,1803,291066,4,1953,291739,5,2103,291740,1,2103,291740,50,2103,291740,40,2103,291780,0,2103,292545,3,2411,292556,4,2565,292617,5,2704,292617,1,2704,292617,50,2704,292617,40,2704,292657,0,2704,322196,3,4205,322938,4,4955,323722,1,5705,323722,50,5706,323722,40,5706,323762,0,5706,342638,3,6457,343249,4,6832,343872,1,7207,343872,50,7207,343872,40,7207,343912,0,7207,356884,3,7986,357576,4,8333,358383,5,8708,358383,1,8708,358383,50,8708,358383,40,8708,358423,0,8708,404870,3,12609,406034,4,14559,406886,5,16509,406887,1,16509,406887,50,16511,406887,40,16511,406927,0,16511,450343,3,19062,451118,4,20337,451670,1,21612,451670,50,21613,451670,40,21613,451710,0,21613,496847,3,23117,497583,4,23864,497638,1,24614,497638,50,24616,497638,40,24616,497678,0,24616,504592,3,25367,506166,4,25743,506573,5,26117,506573,1,26117,506573,50,26117,506573,40,26117,506613,0,26117,543344,3,27319,543902,4,27918,544037,1,28518,544037,50,28520,544037,40,28520,544077,0,28520,572943,3,29271,573410,4,29646,573624,5,30021,573625,1,30021,573625,50,30022,573625,40,30022,573625,40,30022,573660,0,30022,573839,50,30022,573839,30,30022,573839,40,30022,573874,0,30022,573906,50,30022,573906,30,30022,573906,40,30022,573941,0,30028,573973,50,30028,573973,30,30028,573973,40,30028,574008,0,30028,574163,50,30029,574163,30,30029,574163,40,30029,574198,0,30029,574301,50,30030,574336,0,30034,574480,50,30037,574515,0,30037,574667,50,30040,574702,0,30045,574862,50,30050,574897,0,30050,575063,50,30058,575098,0,30058,575272,50,30073,575307,0,30078,575489,50,30106,575524,0,30106,575716,50,30167,575751,0,30167,575953,50,30280,575988,0,30280,576202,50,30510,576202,40,30510,576237,0,30510)
%
%
% START OF PROOF
% 576104 [?] ?
% 576204 [] equal(multiply(identity,X),X).
% 576205 [] equal(multiply(inverse(X),X),identity).
% 576206 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 576207 [] -equal(inverse(sk_c8),sk_c7).
% 576213 [?] ?
% 576219 [?] ?
% 576231 [?] ?
% 576237 [?] ?
% 576246 [input:576219,cut:576207] equal(inverse(sk_c3),sk_c8).
% 576247 [para:576246.1.1,576205.1.1.1] equal(multiply(sk_c8,sk_c3),identity).
% 576255 [input:576231,cut:576207] equal(inverse(sk_c1),sk_c2).
% 576256 [para:576255.1.1,576205.1.1.1] equal(multiply(sk_c2,sk_c1),identity).
% 576259 [input:576213,cut:576207] equal(multiply(sk_c3,sk_c7),sk_c8).
% 576278 [input:576237,cut:576207] equal(multiply(sk_c1,sk_c2),sk_c8).
% 576291 [para:576205.1.1,576206.1.1.1,demod:576204] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 576293 [para:576247.1.1,576206.1.1.1,demod:576204] equal(X,multiply(sk_c8,multiply(sk_c3,X))).
% 576296 [para:576256.1.1,576206.1.1.1,demod:576204] equal(X,multiply(sk_c2,multiply(sk_c1,X))).
% 576329 [para:576259.1.1,576293.1.2.2] equal(sk_c7,multiply(sk_c8,sk_c8)).
% 576333 [para:576278.1.1,576296.1.2.2] equal(sk_c2,multiply(sk_c2,sk_c8)).
% 576377 [para:576296.1.2,576291.1.2.2] equal(multiply(sk_c1,X),multiply(inverse(sk_c2),X)).
% 576378 [para:576333.1.2,576291.1.2.2,demod:576377] equal(sk_c8,multiply(sk_c1,sk_c2)).
% 576427 [para:576377.1.2,576205.1.1,demod:576378] equal(sk_c8,identity).
% 576442 [para:576427.1.1,576329.1.2.1,demod:576204] equal(sk_c7,sk_c8).
% 576450 [para:576442.1.1,576207.1.2,cut:576104] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% Split attempt finished with SUCCESS.
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 27018
% derived clauses: 6115407
% kept clauses: 266819
% kept size sum: 464831
% kept mid-nuclei: 270869
% kept new demods: 2134
% forw unit-subs: 1830646
% forw double-subs: 3340429
% forw overdouble-subs: 330333
% backward subs: 10967
% fast unit cutoff: 29133
% full unit cutoff: 0
% dbl unit cutoff: 10359
% real runtime : 305.74
% process. runtime: 305.10
% specific non-discr-tree subsumption statistics:
% tried: 18908034
% length fails: 2369223
% strength fails: 4566146
% predlist fails: 602795
% aux str. fails: 2802412
% by-lit fails: 2990668
% full subs tried: 2368555
% full subs fail: 2202891
%
% ; 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/GRP212-1+eq_r.in")
%
%------------------------------------------------------------------------------