%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP235-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 : art09.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 298.3s
% Output : Assurance 298.3s
% 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/GRP235-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(inverse(sk_c8),sk_c7) | -equal(inverse(X),sk_c8) | -equal(multiply(X,sk_c7),sk_c8) | -equal(multiply(Y,Z),sk_c7) | -equal(inverse(Y),Z) | -equal(multiply(Z,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(multiply(Y,Z),sk_c7) | -equal(inverse(Y),Z) | -equal(multiply(Z,sk_c8),sk_c7).
% -equal(inverse(X),sk_c8) | -equal(multiply(X,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(inverse(sk_c8),sk_c7) | -equal(inverse(X),sk_c8) | -equal(multiply(X,sk_c7),sk_c8) | -equal(multiply(Y,Z),sk_c7) | -equal(inverse(Y),Z) | -equal(multiply(Z,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,114194,5,1502,114195,1,1502,114195,50,1502,114195,40,1502,114235,0,1502,126339,3,1803,126997,4,1953,127662,1,2103,127662,50,2103,127662,40,2103,127702,0,2103,128342,3,2419,128354,4,2581,128375,5,2704,128375,1,2704,128375,50,2704,128375,40,2704,128415,0,2704,160444,3,4208,161203,4,4955,162017,5,5705,162018,1,5705,162018,50,5706,162018,40,5706,162058,0,5706,184300,3,6457,184833,4,6832,185486,1,7207,185486,50,7207,185486,40,7207,185526,0,7207,201464,3,7962,202434,4,8333,203370,1,8708,203370,50,8708,203370,40,8708,203410,0,8708,274186,3,12611,275095,4,14559,275297,1,16510,275297,50,16512,275297,40,16512,275337,0,16512,334343,3,19076,335163,4,20338,335669,5,21613,335670,1,21613,335670,50,21615,335670,40,21615,335710,0,21615,375772,3,23117,376588,4,23866,377308,5,24616,377309,1,24616,377309,50,24618,377309,40,24618,377349,0,24618,398299,3,25371,399002,4,25744,399564,5,26119,399565,1,26119,399565,50,26119,399565,40,26119,399605,0,26119,432609,3,27320,433312,4,27920,433901,1,28520,433901,50,28521,433901,40,28521,433941,0,28521,457413,3,29273,458072,4,29647,458639,5,30022,458640,1,30022,458640,50,30022,458640,40,30022,458640,40,30022,458675,0,30022)
%
%
% START OF PROOF
% 458642 [] equal(multiply(identity,X),X).
% 458643 [] equal(multiply(inverse(X),X),identity).
% 458644 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 458645 [] -equal(multiply(sk_c8,X),sk_c7) | -equal(multiply(Y,sk_c8),X) | -equal(inverse(Y),sk_c8).
% 458646 [] equal(multiply(sk_c3,sk_c8),sk_c7) | equal(inverse(sk_c5),sk_c8).
% 458647 [] equal(multiply(sk_c3,sk_c8),sk_c7) | equal(multiply(sk_c5,sk_c8),sk_c6).
% 458648 [] equal(multiply(sk_c3,sk_c8),sk_c7) | equal(multiply(sk_c8,sk_c6),sk_c7).
% 458651 [] equal(inverse(sk_c2),sk_c3) | equal(inverse(sk_c5),sk_c8).
% 458652 [] equal(multiply(sk_c5,sk_c8),sk_c6) | equal(inverse(sk_c2),sk_c3).
% 458653 [?] ?
% 458656 [] equal(multiply(sk_c2,sk_c3),sk_c7) | equal(inverse(sk_c5),sk_c8).
% 458657 [] equal(multiply(sk_c2,sk_c3),sk_c7) | equal(multiply(sk_c5,sk_c8),sk_c6).
% 458658 [] equal(multiply(sk_c2,sk_c3),sk_c7) | equal(multiply(sk_c8,sk_c6),sk_c7).
% 458661 [] equal(multiply(sk_c1,sk_c7),sk_c8) | equal(inverse(sk_c5),sk_c8).
% 458662 [] equal(multiply(sk_c1,sk_c7),sk_c8) | equal(multiply(sk_c5,sk_c8),sk_c6).
% 458663 [] equal(multiply(sk_c1,sk_c7),sk_c8) | equal(multiply(sk_c8,sk_c6),sk_c7).
% 458666 [] equal(inverse(sk_c1),sk_c8) | equal(inverse(sk_c5),sk_c8).
% 458667 [] equal(multiply(sk_c5,sk_c8),sk_c6) | equal(inverse(sk_c1),sk_c8).
% 458668 [?] ?
% 458671 [] equal(inverse(sk_c8),sk_c7) | equal(inverse(sk_c5),sk_c8).
% 458672 [] equal(multiply(sk_c5,sk_c8),sk_c6) | equal(inverse(sk_c8),sk_c7).
% 458673 [?] ?
% 458736 [hyper:458645,458652,458651,binarycut:458653] equal(inverse(sk_c2),sk_c3).
% 458737 [para:458736.1.1,458643.1.1.1] equal(multiply(sk_c3,sk_c2),identity).
% 458754 [hyper:458645,458648,458647,458646] equal(multiply(sk_c3,sk_c8),sk_c7).
% 458781 [hyper:458645,458667,458666,binarycut:458668] equal(inverse(sk_c1),sk_c8).
% 458788 [para:458781.1.1,458643.1.1.1] equal(multiply(sk_c8,sk_c1),identity).
% 458797 [hyper:458645,458658,458657,458656] equal(multiply(sk_c2,sk_c3),sk_c7).
% 458801 [hyper:458645,458672,458671,binarycut:458673] equal(inverse(sk_c8),sk_c7).
% 458802 [para:458801.1.1,458643.1.1.1] equal(multiply(sk_c7,sk_c8),identity).
% 458812 [hyper:458645,458663,458662,458661] equal(multiply(sk_c1,sk_c7),sk_c8).
% 458813 [para:458643.1.1,458644.1.1.1,demod:458642] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 458814 [para:458737.1.1,458644.1.1.1,demod:458642] equal(X,multiply(sk_c3,multiply(sk_c2,X))).
% 458815 [para:458754.1.1,458644.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c3,multiply(sk_c8,X))).
% 458816 [para:458788.1.1,458644.1.1.1,demod:458642] equal(X,multiply(sk_c8,multiply(sk_c1,X))).
% 458825 [para:458788.1.1,458813.1.2.2,demod:458801] equal(sk_c1,multiply(sk_c7,identity)).
% 458826 [para:458797.1.1,458813.1.2.2,demod:458736] equal(sk_c3,multiply(sk_c3,sk_c7)).
% 458829 [para:458825.1.2,458644.1.1.1,demod:458642] equal(multiply(sk_c1,X),multiply(sk_c7,X)).
% 458832 [para:458826.1.2,458813.1.2.2,demod:458643] equal(sk_c7,identity).
% 458833 [para:458832.1.1,458802.1.1.1,demod:458642] equal(sk_c8,identity).
% 458835 [para:458832.1.1,458825.1.2.1,demod:458642] equal(sk_c1,identity).
% 458836 [para:458832.1.1,458826.1.2.2] equal(sk_c3,multiply(sk_c3,identity)).
% 458837 [para:458833.1.1,458754.1.1.2,demod:458836] equal(sk_c3,sk_c7).
% 458838 [para:458833.1.1,458801.1.1.1] equal(inverse(identity),sk_c7).
% 458839 [para:458835.1.1,458781.1.1.1,demod:458838] equal(sk_c7,sk_c8).
% 458845 [para:458837.1.2,458825.1.2.1,demod:458836] equal(sk_c1,sk_c3).
% 458847 [para:458837.1.2,458832.1.1] equal(sk_c3,identity).
% 458853 [para:458845.1.2,458826.1.2.1,demod:458812] equal(sk_c3,sk_c8).
% 458855 [para:458847.1.1,458737.1.1.1,demod:458642] equal(sk_c2,identity).
% 458860 [para:458853.1.2,458801.1.1.1] equal(inverse(sk_c3),sk_c7).
% 458866 [para:458833.1.1,458815.1.2.2.1,demod:458642,458829] equal(multiply(sk_c1,X),multiply(sk_c3,X)).
% 458868 [para:458847.1.1,458815.1.2.1,demod:458642,458829] equal(multiply(sk_c1,X),multiply(sk_c8,X)).
% 458869 [para:458855.1.1,458814.1.2.2.1,demod:458866,458642] equal(X,multiply(sk_c1,X)).
% 458873 [hyper:458645,458816,458754,demod:458868,458869,demod:458860,cut:458839] 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(inverse(sk_c8),sk_c7) | -equal(inverse(X),sk_c8) | -equal(multiply(X,sk_c7),sk_c8) | -equal(multiply(Y,Z),sk_c7) | -equal(inverse(Y),Z) | -equal(multiply(Z,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,114194,5,1502,114195,1,1502,114195,50,1502,114195,40,1502,114235,0,1502,126339,3,1803,126997,4,1953,127662,1,2103,127662,50,2103,127662,40,2103,127702,0,2103,128342,3,2419,128354,4,2581,128375,5,2704,128375,1,2704,128375,50,2704,128375,40,2704,128415,0,2704,160444,3,4208,161203,4,4955,162017,5,5705,162018,1,5705,162018,50,5706,162018,40,5706,162058,0,5706,184300,3,6457,184833,4,6832,185486,1,7207,185486,50,7207,185486,40,7207,185526,0,7207,201464,3,7962,202434,4,8333,203370,1,8708,203370,50,8708,203370,40,8708,203410,0,8708,274186,3,12611,275095,4,14559,275297,1,16510,275297,50,16512,275297,40,16512,275337,0,16512,334343,3,19076,335163,4,20338,335669,5,21613,335670,1,21613,335670,50,21615,335670,40,21615,335710,0,21615,375772,3,23117,376588,4,23866,377308,5,24616,377309,1,24616,377309,50,24618,377309,40,24618,377349,0,24618,398299,3,25371,399002,4,25744,399564,5,26119,399565,1,26119,399565,50,26119,399565,40,26119,399605,0,26119,432609,3,27320,433312,4,27920,433901,1,28520,433901,50,28521,433901,40,28521,433941,0,28521,457413,3,29273,458072,4,29647,458639,5,30022,458640,1,30022,458640,50,30022,458640,40,30022,458640,40,30022,458675,0,30022,458872,50,30023,458872,30,30023,458872,40,30023,458907,0,30023)
%
%
% START OF PROOF
% 458873 [] equal(X,X).
% 458877 [] -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c8).
% 458896 [] equal(multiply(sk_c1,sk_c7),sk_c8) | equal(multiply(sk_c4,sk_c7),sk_c8).
% 458897 [?] ?
% 458901 [?] ?
% 458902 [] equal(inverse(sk_c1),sk_c8) | equal(inverse(sk_c4),sk_c8).
% 458926 [hyper:458877,458902,binarycut:458897] equal(inverse(sk_c4),sk_c8).
% 458928 [hyper:458877,458902,binarycut:458901] equal(inverse(sk_c1),sk_c8).
% 458952 [hyper:458877,458896,demod:458928,cut:458873] equal(multiply(sk_c4,sk_c7),sk_c8).
% 458954 [hyper:458877,458952,demod:458926,cut:458873] 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(inverse(sk_c8),sk_c7) | -equal(inverse(X),sk_c8) | -equal(multiply(X,sk_c7),sk_c8) | -equal(multiply(Y,Z),sk_c7) | -equal(inverse(Y),Z) | -equal(multiply(Z,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(Y,Z),sk_c7) | -equal(inverse(Y),Z) | -equal(multiply(Z,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
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,1,75,0,1,114194,5,1502,114195,1,1502,114195,50,1502,114195,40,1502,114235,0,1502,126339,3,1803,126997,4,1953,127662,1,2103,127662,50,2103,127662,40,2103,127702,0,2103,128342,3,2419,128354,4,2581,128375,5,2704,128375,1,2704,128375,50,2704,128375,40,2704,128415,0,2704,160444,3,4208,161203,4,4955,162017,5,5705,162018,1,5705,162018,50,5706,162018,40,5706,162058,0,5706,184300,3,6457,184833,4,6832,185486,1,7207,185486,50,7207,185486,40,7207,185526,0,7207,201464,3,7962,202434,4,8333,203370,1,8708,203370,50,8708,203370,40,8708,203410,0,8708,274186,3,12611,275095,4,14559,275297,1,16510,275297,50,16512,275297,40,16512,275337,0,16512,334343,3,19076,335163,4,20338,335669,5,21613,335670,1,21613,335670,50,21615,335670,40,21615,335710,0,21615,375772,3,23117,376588,4,23866,377308,5,24616,377309,1,24616,377309,50,24618,377309,40,24618,377349,0,24618,398299,3,25371,399002,4,25744,399564,5,26119,399565,1,26119,399565,50,26119,399565,40,26119,399605,0,26119,432609,3,27320,433312,4,27920,433901,1,28520,433901,50,28521,433901,40,28521,433941,0,28521,457413,3,29273,458072,4,29647,458639,5,30022,458640,1,30022,458640,50,30022,458640,40,30022,458640,40,30022,458675,0,30022,458872,50,30023,458872,30,30023,458872,40,30023,458907,0,30023,458953,50,30023,458953,30,30023,458953,40,30023,458988,0,30029)
%
%
% START OF PROOF
% 458954 [] equal(X,X).
% 458955 [] equal(multiply(identity,X),X).
% 458956 [] equal(multiply(inverse(X),X),identity).
% 458957 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 458958 [] -equal(multiply(X,sk_c8),sk_c7) | -equal(multiply(Y,X),sk_c7) | -equal(inverse(Y),X).
% 458959 [?] ?
% 458960 [] equal(multiply(sk_c3,sk_c8),sk_c7) | equal(multiply(sk_c5,sk_c8),sk_c6).
% 458961 [?] ?
% 458962 [] equal(multiply(sk_c3,sk_c8),sk_c7) | equal(multiply(sk_c4,sk_c7),sk_c8).
% 458963 [?] ?
% 458964 [] equal(inverse(sk_c2),sk_c3) | equal(inverse(sk_c5),sk_c8).
% 458965 [] equal(multiply(sk_c5,sk_c8),sk_c6) | equal(inverse(sk_c2),sk_c3).
% 458966 [] equal(multiply(sk_c8,sk_c6),sk_c7) | equal(inverse(sk_c2),sk_c3).
% 458967 [] equal(multiply(sk_c4,sk_c7),sk_c8) | equal(inverse(sk_c2),sk_c3).
% 458968 [] equal(inverse(sk_c2),sk_c3) | equal(inverse(sk_c4),sk_c8).
% 458969 [?] ?
% 458970 [?] ?
% 458971 [?] ?
% 458972 [?] ?
% 458973 [?] ?
% 458993 [hyper:458958,458964,binarycut:458969,binarycut:458959] equal(inverse(sk_c5),sk_c8).
% 458996 [para:458993.1.1,458956.1.1.1] equal(multiply(sk_c8,sk_c5),identity).
% 459000 [hyper:458958,458968,binarycut:458973,binarycut:458963] equal(inverse(sk_c4),sk_c8).
% 459004 [para:459000.1.1,458956.1.1.1] equal(multiply(sk_c8,sk_c4),identity).
% 459013 [hyper:458958,458965,binarycut:458970,binarycut:458960] equal(multiply(sk_c5,sk_c8),sk_c6).
% 459017 [hyper:458958,458966,binarycut:458971,binarycut:458961] equal(multiply(sk_c8,sk_c6),sk_c7).
% 459028 [hyper:458958,458967,binarycut:458972,binarycut:458962] equal(multiply(sk_c4,sk_c7),sk_c8).
% 459029 [para:458956.1.1,458957.1.1.1,demod:458955] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 459030 [para:458996.1.1,458957.1.1.1,demod:458955] equal(X,multiply(sk_c8,multiply(sk_c5,X))).
% 459037 [para:459013.1.1,459030.1.2.2,demod:459017] equal(sk_c8,sk_c7).
% 459040 [para:459037.1.1,459013.1.1.2] equal(multiply(sk_c5,sk_c7),sk_c6).
% 459041 [para:459037.1.1,459017.1.1.1] equal(multiply(sk_c7,sk_c6),sk_c7).
% 459048 [para:458996.1.1,459029.1.2.2] equal(sk_c5,multiply(inverse(sk_c8),identity)).
% 459049 [para:459004.1.1,459029.1.2.2,demod:459048] equal(sk_c4,sk_c5).
% 459051 [para:459028.1.1,459029.1.2.2,demod:459000] equal(sk_c7,multiply(sk_c8,sk_c8)).
% 459055 [para:459049.1.2,459040.1.1.1,demod:459028] equal(sk_c8,sk_c6).
% 459056 [para:459055.1.1,458996.1.1.1] equal(multiply(sk_c6,sk_c5),identity).
% 459067 [para:459041.1.1,459029.1.2.2,demod:458956] equal(sk_c6,identity).
% 459080 [para:459067.1.1,459056.1.1.1,demod:458955] equal(sk_c5,identity).
% 459081 [para:459080.1.1,458993.1.1.1] equal(inverse(identity),sk_c8).
% 459095 [hyper:458958,459081,demod:459051,458955,cut:459037,cut:458954] 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(inverse(sk_c8),sk_c7) | -equal(inverse(X),sk_c8) | -equal(multiply(X,sk_c7),sk_c8) | -equal(multiply(Y,Z),sk_c7) | -equal(inverse(Y),Z) | -equal(multiply(Z,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(X),sk_c8) | -equal(multiply(X,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,114194,5,1502,114195,1,1502,114195,50,1502,114195,40,1502,114235,0,1502,126339,3,1803,126997,4,1953,127662,1,2103,127662,50,2103,127662,40,2103,127702,0,2103,128342,3,2419,128354,4,2581,128375,5,2704,128375,1,2704,128375,50,2704,128375,40,2704,128415,0,2704,160444,3,4208,161203,4,4955,162017,5,5705,162018,1,5705,162018,50,5706,162018,40,5706,162058,0,5706,184300,3,6457,184833,4,6832,185486,1,7207,185486,50,7207,185486,40,7207,185526,0,7207,201464,3,7962,202434,4,8333,203370,1,8708,203370,50,8708,203370,40,8708,203410,0,8708,274186,3,12611,275095,4,14559,275297,1,16510,275297,50,16512,275297,40,16512,275337,0,16512,334343,3,19076,335163,4,20338,335669,5,21613,335670,1,21613,335670,50,21615,335670,40,21615,335710,0,21615,375772,3,23117,376588,4,23866,377308,5,24616,377309,1,24616,377309,50,24618,377309,40,24618,377349,0,24618,398299,3,25371,399002,4,25744,399564,5,26119,399565,1,26119,399565,50,26119,399565,40,26119,399605,0,26119,432609,3,27320,433312,4,27920,433901,1,28520,433901,50,28521,433901,40,28521,433941,0,28521,457413,3,29273,458072,4,29647,458639,5,30022,458640,1,30022,458640,50,30022,458640,40,30022,458640,40,30022,458675,0,30022,458872,50,30023,458872,30,30023,458872,40,30023,458907,0,30023,458953,50,30023,458953,30,30023,458953,40,30023,458988,0,30029,459094,50,30029,459094,30,30029,459094,40,30029,459129,0,30029)
%
%
% START OF PROOF
% 459095 [] equal(X,X).
% 459099 [] -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c8).
% 459118 [] equal(multiply(sk_c1,sk_c7),sk_c8) | equal(multiply(sk_c4,sk_c7),sk_c8).
% 459119 [?] ?
% 459123 [?] ?
% 459124 [] equal(inverse(sk_c1),sk_c8) | equal(inverse(sk_c4),sk_c8).
% 459148 [hyper:459099,459124,binarycut:459119] equal(inverse(sk_c4),sk_c8).
% 459150 [hyper:459099,459124,binarycut:459123] equal(inverse(sk_c1),sk_c8).
% 459174 [hyper:459099,459118,demod:459150,cut:459095] equal(multiply(sk_c4,sk_c7),sk_c8).
% 459176 [hyper:459099,459174,demod:459148,cut:459095] 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(inverse(sk_c8),sk_c7) | -equal(inverse(X),sk_c8) | -equal(multiply(X,sk_c7),sk_c8) | -equal(multiply(Y,Z),sk_c7) | -equal(inverse(Y),Z) | -equal(multiply(Z,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,114194,5,1502,114195,1,1502,114195,50,1502,114195,40,1502,114235,0,1502,126339,3,1803,126997,4,1953,127662,1,2103,127662,50,2103,127662,40,2103,127702,0,2103,128342,3,2419,128354,4,2581,128375,5,2704,128375,1,2704,128375,50,2704,128375,40,2704,128415,0,2704,160444,3,4208,161203,4,4955,162017,5,5705,162018,1,5705,162018,50,5706,162018,40,5706,162058,0,5706,184300,3,6457,184833,4,6832,185486,1,7207,185486,50,7207,185486,40,7207,185526,0,7207,201464,3,7962,202434,4,8333,203370,1,8708,203370,50,8708,203370,40,8708,203410,0,8708,274186,3,12611,275095,4,14559,275297,1,16510,275297,50,16512,275297,40,16512,275337,0,16512,334343,3,19076,335163,4,20338,335669,5,21613,335670,1,21613,335670,50,21615,335670,40,21615,335710,0,21615,375772,3,23117,376588,4,23866,377308,5,24616,377309,1,24616,377309,50,24618,377309,40,24618,377349,0,24618,398299,3,25371,399002,4,25744,399564,5,26119,399565,1,26119,399565,50,26119,399565,40,26119,399605,0,26119,432609,3,27320,433312,4,27920,433901,1,28520,433901,50,28521,433901,40,28521,433941,0,28521,457413,3,29273,458072,4,29647,458639,5,30022,458640,1,30022,458640,50,30022,458640,40,30022,458640,40,30022,458675,0,30022,458872,50,30023,458872,30,30023,458872,40,30023,458907,0,30023,458953,50,30023,458953,30,30023,458953,40,30023,458988,0,30029,459094,50,30029,459094,30,30029,459094,40,30029,459129,0,30029,459175,50,30029,459175,30,30029,459175,40,30029,459210,0,30029,459316,50,30029,459351,0,30034,459498,50,30036,459533,0,30036,459688,50,30040,459723,0,30044,459886,50,30049,459921,0,30050,460090,50,30058,460125,0,30058,460302,50,30073,460337,0,30078,460522,50,30106,460557,0,30106,460752,50,30167,460787,0,30167,460992,50,30284,461027,0,30284,461244,50,30512,461244,40,30512,461279,0,30512)
%
%
% START OF PROOF
% 461246 [] equal(multiply(identity,X),X).
% 461247 [] equal(multiply(inverse(X),X),identity).
% 461248 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 461249 [] -equal(inverse(sk_c8),sk_c7).
% 461275 [?] ?
% 461276 [?] ?
% 461277 [?] ?
% 461278 [?] ?
% 461279 [?] ?
% 461294 [input:461275,cut:461249] equal(inverse(sk_c5),sk_c8).
% 461295 [para:461294.1.1,461247.1.1.1] equal(multiply(sk_c8,sk_c5),identity).
% 461297 [input:461279,cut:461249] equal(inverse(sk_c4),sk_c8).
% 461298 [para:461297.1.1,461247.1.1.1] equal(multiply(sk_c8,sk_c4),identity).
% 461318 [input:461276,cut:461249] equal(multiply(sk_c5,sk_c8),sk_c6).
% 461319 [input:461277,cut:461249] equal(multiply(sk_c8,sk_c6),sk_c7).
% 461321 [input:461278,cut:461249] equal(multiply(sk_c4,sk_c7),sk_c8).
% 461333 [para:461247.1.1,461248.1.1.1,demod:461246] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 461335 [para:461295.1.1,461248.1.1.1,demod:461246] equal(X,multiply(sk_c8,multiply(sk_c5,X))).
% 461338 [para:461298.1.1,461248.1.1.1,demod:461246] equal(X,multiply(sk_c8,multiply(sk_c4,X))).
% 461355 [para:461319.1.1,461248.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c8,multiply(sk_c6,X))).
% 461372 [para:461318.1.1,461335.1.2.2] equal(sk_c8,multiply(sk_c8,sk_c6)).
% 461376 [para:461372.1.2,461319.1.1] equal(sk_c8,sk_c7).
% 461377 [para:461372.1.2,461248.1.1.1,demod:461355] equal(multiply(sk_c8,X),multiply(sk_c7,X)).
% 461378 [para:461376.1.1,461249.1.1.1] -equal(inverse(sk_c7),sk_c7).
% 461405 [para:461321.1.1,461338.1.2.2,demod:461377] equal(sk_c7,multiply(sk_c7,sk_c8)).
% 461458 [para:461405.1.2,461333.1.2.2,demod:461247] equal(sk_c8,identity).
% 461480 [para:461458.1.1,461295.1.1.1,demod:461246] equal(sk_c5,identity).
% 461494 [para:461458.1.1,461376.1.1] equal(identity,sk_c7).
% 461507 [para:461480.1.1,461294.1.1.1] equal(inverse(identity),sk_c8).
% 461523 [para:461494.1.2,461378.1.1.1,demod:461507,cut:461376] 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: 27712
% derived clauses: 6500986
% kept clauses: 312283
% kept size sum: 15445
% kept mid-nuclei: 94546
% kept new demods: 2103
% forw unit-subs: 2010045
% forw double-subs: 3792511
% forw overdouble-subs: 240699
% backward subs: 6632
% fast unit cutoff: 29528
% full unit cutoff: 0
% dbl unit cutoff: 25398
% real runtime : 307.17
% process. runtime: 305.12
% specific non-discr-tree subsumption statistics:
% tried: 22790671
% length fails: 2916861
% strength fails: 6572364
% predlist fails: 950137
% aux str. fails: 2594419
% by-lit fails: 3240613
% full subs tried: 2049821
% full subs fail: 1917613
%
% ; 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/GRP235-1+eq_r.in")
%
%------------------------------------------------------------------------------