%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP379-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 : art05.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 297.9s
% Output : Assurance 297.9s
% 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/GRP379-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 29)
% (binary-unit 12 #f)
% (binary-unit-uniteq 12 #f)
% (binary-posweight-kb-big-order 60 #f 3 29)
% (binary-posweight-lex-big-order 30 #f 3 29)
% (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_c11),sk_c10) | -equal(multiply(sk_c10,sk_c9),sk_c11) | -equal(multiply(X,Y),sk_c11) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c9),sk_c11) | -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X1),X2) | -equal(inverse(X2),W) | -equal(multiply(X1,W),X2).
% was split for some strategies as:
% -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X2),W) | -equal(inverse(X1),X2) | -equal(multiply(X1,W),X2).
% -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10).
% -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11).
% -equal(multiply(X,Y),sk_c11) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c9),sk_c11).
% -equal(inverse(sk_c11),sk_c10).
% -equal(multiply(sk_c10,sk_c9),sk_c11).
%
% Starting a split proof attempt with 6 components.
%
% Split component 1 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(inverse(sk_c11),sk_c10) | -equal(multiply(sk_c10,sk_c9),sk_c11) | -equal(multiply(X,Y),sk_c11) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c9),sk_c11) | -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X1),X2) | -equal(inverse(X2),W) | -equal(multiply(X1,W),X2).
% Split part used next: -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X2),W) | -equal(inverse(X1),X2) | -equal(multiply(X1,W),X2).
% END OF PROOFPART
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(55,40,0,118,0,0,61904,50,1038,61904,40,1038,61967,0,1038,62548,5,1639,62548,1,1639,62548,50,1639,62548,40,1639,62611,0,1639,63218,5,2241,63221,1,2242,63221,50,2242,63221,40,2242,63284,0,2242,86648,3,3743,87788,4,4493,88950,5,5243,88951,1,5243,88951,50,5243,88951,40,5243,89014,0,5244,104471,3,5995,105430,4,6370,106039,5,6745,106040,1,6745,106040,50,6745,106040,40,6745,106103,0,6745,106922,5,8247,106923,1,8247,106923,50,8247,106923,40,8247,106986,0,8247,157438,3,12149,158690,4,14098,160052,5,16048,160053,1,16048,160053,50,16050,160053,40,16050,160116,0,16050,203318,3,18601,204230,4,19876,205314,5,21151,205315,1,21151,205315,50,21153,205315,40,21153,205378,0,21153,245013,3,22655,245768,4,23404,246654,1,24154,246654,50,24155,246654,40,24155,246717,0,24155,247541,5,25659,247544,1,25660,247544,50,25660,247544,40,25660,247607,0,25660,273068,3,26862,273844,4,27461,274443,1,28061,274443,50,28061,274443,40,28061,274506,0,28062,294643,3,28813,295125,4,29188,295500,1,29563,295500,50,29563,295500,40,29563,295500,40,29563,295609,0,29563,297148,50,29568,297257,0,29569)
%
%
% START OF PROOF
% 297150 [] equal(multiply(identity,X),X).
% 297151 [] equal(multiply(inverse(X),X),identity).
% 297152 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 297203 [] -equal(multiply(X,sk_c10),sk_c11) | -equal(multiply(Y,X),sk_c11) | -equal(multiply(Z,X),U) | -equal(inverse(Z),U) | -equal(inverse(U),X) | -equal(inverse(Y),X).
% 297204 [] -equal(multiply(X,Y),Z) | -equal(inverse(X),Z) | -equal(inverse(Z),Y) | $spltprd1($spltcnst85,Y).
% 297205 [] -equal(multiply(X,Y),sk_c11) | -equal(inverse(X),Y) | $spltprd1($spltcnst86,Y).
% 297206 [] -equal(multiply(X,sk_c10),sk_c11) | $spltprd1($spltcnst87,X).
% 297207 [] -$spltprd1($spltcnst86,X) | -$spltprd1($spltcnst85,X) | -$spltprd1($spltcnst87,X).
% 297208 [] equal(multiply(sk_c2,sk_c9),sk_c11) | equal(multiply(sk_c7,sk_c8),sk_c6).
% 297209 [] equal(multiply(sk_c2,sk_c9),sk_c11) | equal(inverse(sk_c6),sk_c8).
% 297210 [] equal(multiply(sk_c2,sk_c9),sk_c11) | equal(inverse(sk_c7),sk_c6).
% 297211 [] equal(multiply(sk_c2,sk_c9),sk_c11) | equal(multiply(sk_c8,sk_c10),sk_c11).
% 297212 [] equal(multiply(sk_c2,sk_c9),sk_c11) | equal(inverse(sk_c5),sk_c8).
% 297213 [] equal(multiply(sk_c2,sk_c9),sk_c11) | equal(multiply(sk_c5,sk_c8),sk_c11).
% 297218 [] equal(multiply(sk_c7,sk_c8),sk_c6) | equal(inverse(sk_c1),sk_c2).
% 297219 [] equal(inverse(sk_c1),sk_c2) | equal(inverse(sk_c6),sk_c8).
% 297220 [] equal(inverse(sk_c1),sk_c2) | equal(inverse(sk_c7),sk_c6).
% 297221 [] equal(multiply(sk_c8,sk_c10),sk_c11) | equal(inverse(sk_c1),sk_c2).
% 297222 [] equal(inverse(sk_c1),sk_c2) | equal(inverse(sk_c5),sk_c8).
% 297223 [?] ?
% 297228 [] equal(multiply(sk_c1,sk_c2),sk_c11) | equal(multiply(sk_c7,sk_c8),sk_c6).
% 297229 [] equal(multiply(sk_c1,sk_c2),sk_c11) | equal(inverse(sk_c6),sk_c8).
% 297230 [] equal(multiply(sk_c1,sk_c2),sk_c11) | equal(inverse(sk_c7),sk_c6).
% 297231 [] equal(multiply(sk_c1,sk_c2),sk_c11) | equal(multiply(sk_c8,sk_c10),sk_c11).
% 297232 [] equal(multiply(sk_c1,sk_c2),sk_c11) | equal(inverse(sk_c5),sk_c8).
% 297233 [] equal(multiply(sk_c1,sk_c2),sk_c11) | equal(multiply(sk_c5,sk_c8),sk_c11).
% 297238 [] equal(multiply(sk_c10,sk_c9),sk_c11) | equal(multiply(sk_c7,sk_c8),sk_c6).
% 297239 [] equal(multiply(sk_c10,sk_c9),sk_c11) | equal(inverse(sk_c6),sk_c8).
% 297240 [] equal(multiply(sk_c10,sk_c9),sk_c11) | equal(inverse(sk_c7),sk_c6).
% 297241 [] equal(multiply(sk_c10,sk_c9),sk_c11) | equal(multiply(sk_c8,sk_c10),sk_c11).
% 297242 [] equal(multiply(sk_c10,sk_c9),sk_c11) | equal(inverse(sk_c5),sk_c8).
% 297243 [] equal(multiply(sk_c10,sk_c9),sk_c11) | equal(multiply(sk_c5,sk_c8),sk_c11).
% 297248 [] equal(multiply(sk_c7,sk_c8),sk_c6) | equal(inverse(sk_c11),sk_c10).
% 297249 [] equal(inverse(sk_c11),sk_c10) | equal(inverse(sk_c6),sk_c8).
% 297250 [] equal(inverse(sk_c11),sk_c10) | equal(inverse(sk_c7),sk_c6).
% 297251 [] equal(multiply(sk_c8,sk_c10),sk_c11) | equal(inverse(sk_c11),sk_c10).
% 297252 [] equal(inverse(sk_c11),sk_c10) | equal(inverse(sk_c5),sk_c8).
% 297253 [?] ?
% 297350 [hyper:297205,297222,binarycut:297223] equal(inverse(sk_c1),sk_c2) | $spltprd1($spltcnst86,sk_c8).
% 297465 [hyper:297205,297252,binarycut:297253] equal(inverse(sk_c11),sk_c10) | $spltprd1($spltcnst86,sk_c8).
% 297615 [hyper:297204,297218,297219,297220] equal(inverse(sk_c1),sk_c2) | $spltprd1($spltcnst85,sk_c8).
% 297663 [hyper:297206,297221] equal(inverse(sk_c1),sk_c2) | $spltprd1($spltcnst87,sk_c8).
% 297677 [hyper:297207,297663,297615,297350] equal(inverse(sk_c1),sk_c2).
% 297684 [para:297677.1.1,297151.1.1.1] equal(multiply(sk_c2,sk_c1),identity).
% 297906 [hyper:297204,297248,297249,297250] equal(inverse(sk_c11),sk_c10) | $spltprd1($spltcnst85,sk_c8).
% 297931 [hyper:297206,297251] equal(inverse(sk_c11),sk_c10) | $spltprd1($spltcnst87,sk_c8).
% 297942 [hyper:297207,297931,297906,297465] equal(inverse(sk_c11),sk_c10).
% 297952 [para:297942.1.1,297151.1.1.1] equal(multiply(sk_c10,sk_c11),identity).
% 298106 [hyper:297203,297213,297211,297212,297209,297208,297210] equal(multiply(sk_c2,sk_c9),sk_c11).
% 298622 [hyper:297203,297233,297231,297232,297229,297228,297230] equal(multiply(sk_c1,sk_c2),sk_c11).
% 298707 [hyper:297203,297243,297241,297242,297239,297238,297240] equal(multiply(sk_c10,sk_c9),sk_c11).
% 298724 [para:297151.1.1,297152.1.1.1,demod:297150] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 298725 [para:297684.1.1,297152.1.1.1,demod:297150] equal(X,multiply(sk_c2,multiply(sk_c1,X))).
% 298726 [para:297952.1.1,297152.1.1.1,demod:297150] equal(X,multiply(sk_c10,multiply(sk_c11,X))).
% 298730 [para:298622.1.1,297152.1.1.1] equal(multiply(sk_c11,X),multiply(sk_c1,multiply(sk_c2,X))).
% 298764 [para:298622.1.1,298725.1.2.2] equal(sk_c2,multiply(sk_c2,sk_c11)).
% 298823 [para:297151.1.1,298724.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 298824 [para:297684.1.1,298724.1.2.2] equal(sk_c1,multiply(inverse(sk_c2),identity)).
% 298825 [para:297952.1.1,298724.1.2.2] equal(sk_c11,multiply(inverse(sk_c10),identity)).
% 298835 [para:298106.1.1,298724.1.2.2] equal(sk_c9,multiply(inverse(sk_c2),sk_c11)).
% 298847 [para:298707.1.1,298724.1.2.2] equal(sk_c9,multiply(inverse(sk_c10),sk_c11)).
% 298848 [para:297152.1.1,298724.1.2.2] equal(X,multiply(inverse(multiply(Y,Z)),multiply(Y,multiply(Z,X)))).
% 298849 [para:298725.1.2,298724.1.2.2] equal(multiply(sk_c1,X),multiply(inverse(sk_c2),X)).
% 298850 [para:298726.1.2,298724.1.2.2] equal(multiply(sk_c11,X),multiply(inverse(sk_c10),X)).
% 298851 [para:298724.1.2,298724.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 298948 [para:298849.1.2,297151.1.1,demod:298622] equal(sk_c11,identity).
% 298951 [para:298849.1.2,298724.1.2,demod:298730] equal(X,multiply(sk_c11,X)).
% 298954 [para:298948.1.1,297942.1.1.1] equal(inverse(identity),sk_c10).
% 298955 [para:298948.1.1,297952.1.1.2] equal(multiply(sk_c10,identity),identity).
% 298958 [para:298948.1.1,298835.1.2.2,demod:298824] equal(sk_c9,sk_c1).
% 298959 [para:298948.1.1,298847.1.2.2,demod:298825] equal(sk_c9,sk_c11).
% 298960 [para:298958.1.2,297677.1.1.1] equal(inverse(sk_c9),sk_c2).
% 298961 [para:298958.1.2,298622.1.1.1] equal(multiply(sk_c9,sk_c2),sk_c11).
% 298962 [para:298959.1.2,297942.1.1.1,demod:298960] equal(sk_c2,sk_c10).
% 298963 [para:298959.1.2,298764.1.2.2,demod:298106] equal(sk_c2,sk_c11).
% 298965 [para:298959.1.2,298948.1.1] equal(sk_c9,identity).
% 298966 [para:298962.1.2,297952.1.1.1,demod:298764] equal(sk_c2,identity).
% 298969 [para:298963.1.2,297942.1.1.1] equal(inverse(sk_c2),sk_c10).
% 298972 [para:298965.1.1,298707.1.1.2,demod:298955] equal(identity,sk_c11).
% 298977 [para:298966.1.1,298725.1.2.1,demod:297150] equal(X,multiply(sk_c1,X)).
% 299369 [para:298850.1.2,297151.1.1,demod:298951] equal(sk_c10,identity).
% 299378 [para:298851.1.2,297151.1.1] equal(multiply(X,inverse(X)),identity).
% 299382 [para:298851.1.2,298823.1.2] equal(X,multiply(X,identity)).
% 299451 [para:299382.1.2,298825.1.2] equal(sk_c11,inverse(sk_c10)).
% 299452 [para:299382.1.2,298823.1.2] equal(X,inverse(inverse(X))).
% 299561 [para:299378.1.1,298848.1.2.2.2,demod:299382] equal(inverse(X),multiply(inverse(multiply(Y,X)),Y)).
% 299596 [para:298725.1.2,299561.1.2.1.1,demod:298977] equal(inverse(X),multiply(inverse(X),sk_c2)).
% 299597 [para:298726.1.2,299561.1.2.1.1,demod:298951] equal(inverse(X),multiply(inverse(X),sk_c10)).
% 299602 [para:298961.1.1,299561.1.2.1.1,demod:298707,297942,298969] equal(sk_c10,sk_c11).
% 299645 [hyper:297203,299596,299452,297151,demod:299597,299378,299596,cut:298972,demod:299452,demod:297942,299451,298954,cut:299602,cut:299369] 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 29
% clause depth limited to 4
% seconds given: 4
%
%
% Split component 2 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(inverse(sk_c11),sk_c10) | -equal(multiply(sk_c10,sk_c9),sk_c11) | -equal(multiply(X,Y),sk_c11) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c9),sk_c11) | -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X1),X2) | -equal(inverse(X2),W) | -equal(multiply(X1,W),X2).
% Split part used next: -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10).
% 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 29
% clause depth limited to 3
% seconds given: 4
%
%
% 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 29
% clause depth limited to 4
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(55,40,0,118,0,0,61904,50,1038,61904,40,1038,61967,0,1038,62548,5,1639,62548,1,1639,62548,50,1639,62548,40,1639,62611,0,1639,63218,5,2241,63221,1,2242,63221,50,2242,63221,40,2242,63284,0,2242,86648,3,3743,87788,4,4493,88950,5,5243,88951,1,5243,88951,50,5243,88951,40,5243,89014,0,5244,104471,3,5995,105430,4,6370,106039,5,6745,106040,1,6745,106040,50,6745,106040,40,6745,106103,0,6745,106922,5,8247,106923,1,8247,106923,50,8247,106923,40,8247,106986,0,8247,157438,3,12149,158690,4,14098,160052,5,16048,160053,1,16048,160053,50,16050,160053,40,16050,160116,0,16050,203318,3,18601,204230,4,19876,205314,5,21151,205315,1,21151,205315,50,21153,205315,40,21153,205378,0,21153,245013,3,22655,245768,4,23404,246654,1,24154,246654,50,24155,246654,40,24155,246717,0,24155,247541,5,25659,247544,1,25660,247544,50,25660,247544,40,25660,247607,0,25660,273068,3,26862,273844,4,27461,274443,1,28061,274443,50,28061,274443,40,28061,274506,0,28062,294643,3,28813,295125,4,29188,295500,1,29563,295500,50,29563,295500,40,29563,295500,40,29563,295609,0,29563,297148,50,29568,297257,0,29569,299644,50,29577,299644,30,29577,299644,40,29577,299699,0,29582,299822,50,29582,299877,0,29582)
%
%
% START OF PROOF
% 299824 [] equal(multiply(identity,X),X).
% 299825 [] equal(multiply(inverse(X),X),identity).
% 299826 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 299827 [] -equal(multiply(X,sk_c10),sk_c9) | -equal(inverse(X),sk_c10).
% 299834 [] equal(multiply(sk_c2,sk_c9),sk_c11) | equal(inverse(sk_c4),sk_c10).
% 299835 [] equal(multiply(sk_c2,sk_c9),sk_c11) | equal(multiply(sk_c4,sk_c10),sk_c9).
% 299844 [] equal(inverse(sk_c1),sk_c2) | equal(inverse(sk_c4),sk_c10).
% 299845 [?] ?
% 299854 [] equal(multiply(sk_c1,sk_c2),sk_c11) | equal(inverse(sk_c4),sk_c10).
% 299855 [] equal(multiply(sk_c1,sk_c2),sk_c11) | equal(multiply(sk_c4,sk_c10),sk_c9).
% 299864 [] equal(multiply(sk_c10,sk_c9),sk_c11) | equal(inverse(sk_c4),sk_c10).
% 299865 [] equal(multiply(sk_c10,sk_c9),sk_c11) | equal(multiply(sk_c4,sk_c10),sk_c9).
% 299874 [] equal(inverse(sk_c11),sk_c10) | equal(inverse(sk_c4),sk_c10).
% 299875 [?] ?
% 299884 [hyper:299827,299844,binarycut:299845] equal(inverse(sk_c1),sk_c2).
% 299885 [para:299884.1.1,299825.1.1.1] equal(multiply(sk_c2,sk_c1),identity).
% 299899 [hyper:299827,299874,binarycut:299875] equal(inverse(sk_c11),sk_c10).
% 299902 [para:299899.1.1,299825.1.1.1] equal(multiply(sk_c10,sk_c11),identity).
% 299929 [hyper:299827,299835,299834] equal(multiply(sk_c2,sk_c9),sk_c11).
% 299935 [hyper:299827,299855,299854] equal(multiply(sk_c1,sk_c2),sk_c11).
% 299941 [hyper:299827,299865,299864] equal(multiply(sk_c10,sk_c9),sk_c11).
% 299942 [para:299825.1.1,299826.1.1.1,demod:299824] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 299943 [para:299885.1.1,299826.1.1.1,demod:299824] equal(X,multiply(sk_c2,multiply(sk_c1,X))).
% 299946 [para:299935.1.1,299826.1.1.1] equal(multiply(sk_c11,X),multiply(sk_c1,multiply(sk_c2,X))).
% 299948 [para:299935.1.1,299943.1.2.2] equal(sk_c2,multiply(sk_c2,sk_c11)).
% 299951 [para:299825.1.1,299942.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 299952 [para:299885.1.1,299942.1.2.2] equal(sk_c1,multiply(inverse(sk_c2),identity)).
% 299953 [para:299902.1.1,299942.1.2.2] equal(sk_c11,multiply(inverse(sk_c10),identity)).
% 299954 [para:299929.1.1,299942.1.2.2] equal(sk_c9,multiply(inverse(sk_c2),sk_c11)).
% 299955 [para:299941.1.1,299942.1.2.2] equal(sk_c9,multiply(inverse(sk_c10),sk_c11)).
% 299956 [para:299826.1.1,299942.1.2.2] equal(X,multiply(inverse(multiply(Y,Z)),multiply(Y,multiply(Z,X)))).
% 299957 [para:299943.1.2,299942.1.2.2] equal(multiply(sk_c1,X),multiply(inverse(sk_c2),X)).
% 299959 [para:299942.1.2,299942.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 299962 [para:299957.1.2,299825.1.1,demod:299935] equal(sk_c11,identity).
% 299963 [para:299957.1.2,299942.1.2,demod:299946] equal(X,multiply(sk_c11,X)).
% 299970 [para:299962.1.1,299954.1.2.2,demod:299952] equal(sk_c9,sk_c1).
% 299971 [para:299962.1.1,299955.1.2.2,demod:299953] equal(sk_c9,sk_c11).
% 299972 [para:299970.1.2,299884.1.1.1] equal(inverse(sk_c9),sk_c2).
% 299974 [para:299971.1.2,299899.1.1.1,demod:299972] equal(sk_c2,sk_c10).
% 299975 [para:299971.1.2,299948.1.2.2,demod:299929] equal(sk_c2,sk_c11).
% 299984 [para:299975.1.2,299899.1.1.1] equal(inverse(sk_c2),sk_c10).
% 300015 [para:299959.1.2,299825.1.1] equal(multiply(X,inverse(X)),identity).
% 300017 [para:299959.1.2,299951.1.2] equal(X,multiply(X,identity)).
% 300022 [para:299963.1.2,299956.1.2.2.2] equal(X,multiply(inverse(multiply(Y,sk_c11)),multiply(Y,X))).
% 300031 [para:300017.1.2,299953.1.2] equal(sk_c11,inverse(sk_c10)).
% 300032 [para:300017.1.2,299951.1.2] equal(X,inverse(inverse(X))).
% 300033 [para:299974.1.2,300031.1.2.1,demod:299984] equal(sk_c11,sk_c10).
% 300040 [para:300015.1.1,300022.1.2.2,demod:300017] equal(inverse(X),inverse(multiply(X,sk_c11))).
% 300047 [para:300040.1.2,299951.1.2.1.1,demod:300017,300032] equal(multiply(X,sk_c11),X).
% 300055 [para:300033.1.1,300047.1.1.2] equal(multiply(X,sk_c10),X).
% 300057 [hyper:299827,300055,demod:299972,cut:299974] 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 29
% clause depth limited to 4
% seconds given: 4
%
%
% Split component 3 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(inverse(sk_c11),sk_c10) | -equal(multiply(sk_c10,sk_c9),sk_c11) | -equal(multiply(X,Y),sk_c11) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c9),sk_c11) | -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X1),X2) | -equal(inverse(X2),W) | -equal(multiply(X1,W),X2).
% Split part used next: -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11).
% 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 29
% clause depth limited to 3
% seconds given: 4
%
%
% 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 29
% clause depth limited to 4
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(55,40,0,118,0,0,61904,50,1038,61904,40,1038,61967,0,1038,62548,5,1639,62548,1,1639,62548,50,1639,62548,40,1639,62611,0,1639,63218,5,2241,63221,1,2242,63221,50,2242,63221,40,2242,63284,0,2242,86648,3,3743,87788,4,4493,88950,5,5243,88951,1,5243,88951,50,5243,88951,40,5243,89014,0,5244,104471,3,5995,105430,4,6370,106039,5,6745,106040,1,6745,106040,50,6745,106040,40,6745,106103,0,6745,106922,5,8247,106923,1,8247,106923,50,8247,106923,40,8247,106986,0,8247,157438,3,12149,158690,4,14098,160052,5,16048,160053,1,16048,160053,50,16050,160053,40,16050,160116,0,16050,203318,3,18601,204230,4,19876,205314,5,21151,205315,1,21151,205315,50,21153,205315,40,21153,205378,0,21153,245013,3,22655,245768,4,23404,246654,1,24154,246654,50,24155,246654,40,24155,246717,0,24155,247541,5,25659,247544,1,25660,247544,50,25660,247544,40,25660,247607,0,25660,273068,3,26862,273844,4,27461,274443,1,28061,274443,50,28061,274443,40,28061,274506,0,28062,294643,3,28813,295125,4,29188,295500,1,29563,295500,50,29563,295500,40,29563,295500,40,29563,295609,0,29563,297148,50,29568,297257,0,29569,299644,50,29577,299644,30,29577,299644,40,29577,299699,0,29582,299822,50,29582,299877,0,29582,300056,50,29583,300056,30,29583,300056,40,29583,300111,0,29588,300225,50,29589,300280,0,29589)
%
%
% START OF PROOF
% 300226 [] equal(X,X).
% 300227 [] equal(multiply(identity,X),X).
% 300228 [] equal(multiply(inverse(X),X),identity).
% 300229 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 300230 [] -equal(multiply(X,sk_c11),sk_c10) | -equal(inverse(X),sk_c11).
% 300249 [] equal(inverse(sk_c1),sk_c2) | equal(inverse(sk_c3),sk_c11).
% 300250 [?] ?
% 300259 [] equal(multiply(sk_c1,sk_c2),sk_c11) | equal(inverse(sk_c3),sk_c11).
% 300260 [] equal(multiply(sk_c1,sk_c2),sk_c11) | equal(multiply(sk_c3,sk_c11),sk_c10).
% 300279 [] equal(inverse(sk_c11),sk_c10) | equal(inverse(sk_c3),sk_c11).
% 300280 [?] ?
% 300288 [hyper:300230,300249,binarycut:300250] equal(inverse(sk_c1),sk_c2).
% 300289 [para:300288.1.1,300228.1.1.1] equal(multiply(sk_c2,sk_c1),identity).
% 300297 [hyper:300230,300279,binarycut:300280] equal(inverse(sk_c11),sk_c10).
% 300299 [para:300297.1.1,300228.1.1.1] equal(multiply(sk_c10,sk_c11),identity).
% 300332 [hyper:300230,300260,300259] equal(multiply(sk_c1,sk_c2),sk_c11).
% 300340 [para:300228.1.1,300229.1.1.1,demod:300227] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 300341 [para:300289.1.1,300229.1.1.1,demod:300227] equal(X,multiply(sk_c2,multiply(sk_c1,X))).
% 300344 [para:300332.1.1,300229.1.1.1] equal(multiply(sk_c11,X),multiply(sk_c1,multiply(sk_c2,X))).
% 300349 [para:300228.1.1,300340.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 300351 [para:300299.1.1,300340.1.2.2] equal(sk_c11,multiply(inverse(sk_c10),identity)).
% 300354 [para:300229.1.1,300340.1.2.2] equal(X,multiply(inverse(multiply(Y,Z)),multiply(Y,multiply(Z,X)))).
% 300355 [para:300341.1.2,300340.1.2.2] equal(multiply(sk_c1,X),multiply(inverse(sk_c2),X)).
% 300357 [para:300340.1.2,300340.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 300361 [para:300355.1.2,300340.1.2,demod:300344] equal(X,multiply(sk_c11,X)).
% 300413 [para:300357.1.2,300228.1.1] equal(multiply(X,inverse(X)),identity).
% 300415 [para:300357.1.2,300349.1.2] equal(X,multiply(X,identity)).
% 300416 [para:300361.1.2,300354.1.2.2.2] equal(X,multiply(inverse(multiply(Y,sk_c11)),multiply(Y,X))).
% 300425 [para:300415.1.2,300351.1.2] equal(sk_c11,inverse(sk_c10)).
% 300426 [para:300415.1.2,300349.1.2] equal(X,inverse(inverse(X))).
% 300434 [para:300413.1.1,300416.1.2.2,demod:300415] equal(inverse(X),inverse(multiply(X,sk_c11))).
% 300441 [para:300434.1.2,300349.1.2.1.1,demod:300415,300426] equal(multiply(X,sk_c11),X).
% 300446 [hyper:300230,300441,demod:300425,cut:300226] 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 29
% clause depth limited to 4
% seconds given: 4
%
%
% Split component 4 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(inverse(sk_c11),sk_c10) | -equal(multiply(sk_c10,sk_c9),sk_c11) | -equal(multiply(X,Y),sk_c11) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c9),sk_c11) | -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X1),X2) | -equal(inverse(X2),W) | -equal(multiply(X1,W),X2).
% Split part used next: -equal(multiply(X,Y),sk_c11) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c9),sk_c11).
% 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 29
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(55,40,0,118,0,0,61904,50,1038,61904,40,1038,61967,0,1038,62548,5,1639,62548,1,1639,62548,50,1639,62548,40,1639,62611,0,1639,63218,5,2241,63221,1,2242,63221,50,2242,63221,40,2242,63284,0,2242,86648,3,3743,87788,4,4493,88950,5,5243,88951,1,5243,88951,50,5243,88951,40,5243,89014,0,5244,104471,3,5995,105430,4,6370,106039,5,6745,106040,1,6745,106040,50,6745,106040,40,6745,106103,0,6745,106922,5,8247,106923,1,8247,106923,50,8247,106923,40,8247,106986,0,8247,157438,3,12149,158690,4,14098,160052,5,16048,160053,1,16048,160053,50,16050,160053,40,16050,160116,0,16050,203318,3,18601,204230,4,19876,205314,5,21151,205315,1,21151,205315,50,21153,205315,40,21153,205378,0,21153,245013,3,22655,245768,4,23404,246654,1,24154,246654,50,24155,246654,40,24155,246717,0,24155,247541,5,25659,247544,1,25660,247544,50,25660,247544,40,25660,247607,0,25660,273068,3,26862,273844,4,27461,274443,1,28061,274443,50,28061,274443,40,28061,274506,0,28062,294643,3,28813,295125,4,29188,295500,1,29563,295500,50,29563,295500,40,29563,295500,40,29563,295609,0,29563,297148,50,29568,297257,0,29569,299644,50,29577,299644,30,29577,299644,40,29577,299699,0,29582,299822,50,29582,299877,0,29582,300056,50,29583,300056,30,29583,300056,40,29583,300111,0,29588,300225,50,29589,300280,0,29589,300445,50,29590,300445,30,29590,300445,40,29590,300500,0,29595)
%
%
% START OF PROOF
% 300446 [] equal(X,X).
% 300447 [] equal(multiply(identity,X),X).
% 300448 [] equal(multiply(inverse(X),X),identity).
% 300449 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 300450 [] -equal(multiply(X,sk_c9),sk_c11) | -equal(multiply(Y,X),sk_c11) | -equal(inverse(Y),X).
% 300452 [?] ?
% 300453 [?] ?
% 300454 [] equal(multiply(sk_c2,sk_c9),sk_c11) | equal(multiply(sk_c8,sk_c10),sk_c11).
% 300455 [?] ?
% 300456 [] equal(multiply(sk_c2,sk_c9),sk_c11) | equal(multiply(sk_c5,sk_c8),sk_c11).
% 300457 [?] ?
% 300458 [] equal(multiply(sk_c2,sk_c9),sk_c11) | equal(multiply(sk_c4,sk_c10),sk_c9).
% 300459 [?] ?
% 300460 [] equal(multiply(sk_c2,sk_c9),sk_c11) | equal(multiply(sk_c3,sk_c11),sk_c10).
% 300462 [] equal(inverse(sk_c1),sk_c2) | equal(inverse(sk_c6),sk_c8).
% 300463 [] equal(inverse(sk_c1),sk_c2) | equal(inverse(sk_c7),sk_c6).
% 300464 [] equal(multiply(sk_c8,sk_c10),sk_c11) | equal(inverse(sk_c1),sk_c2).
% 300465 [] equal(inverse(sk_c1),sk_c2) | equal(inverse(sk_c5),sk_c8).
% 300466 [] equal(multiply(sk_c5,sk_c8),sk_c11) | equal(inverse(sk_c1),sk_c2).
% 300467 [] equal(inverse(sk_c1),sk_c2) | equal(inverse(sk_c4),sk_c10).
% 300468 [] equal(multiply(sk_c4,sk_c10),sk_c9) | equal(inverse(sk_c1),sk_c2).
% 300469 [] equal(inverse(sk_c1),sk_c2) | equal(inverse(sk_c3),sk_c11).
% 300470 [] equal(multiply(sk_c3,sk_c11),sk_c10) | equal(inverse(sk_c1),sk_c2).
% 300472 [?] ?
% 300473 [?] ?
% 300474 [?] ?
% 300475 [?] ?
% 300476 [?] ?
% 300477 [?] ?
% 300478 [?] ?
% 300479 [?] ?
% 300480 [?] ?
% 300505 [hyper:300450,300462,binarycut:300472,binarycut:300452] equal(inverse(sk_c6),sk_c8).
% 300508 [para:300505.1.1,300448.1.1.1] equal(multiply(sk_c8,sk_c6),identity).
% 300512 [hyper:300450,300463,binarycut:300473,binarycut:300453] equal(inverse(sk_c7),sk_c6).
% 300516 [para:300512.1.1,300448.1.1.1] equal(multiply(sk_c6,sk_c7),identity).
% 300520 [hyper:300450,300465,binarycut:300475,binarycut:300455] equal(inverse(sk_c5),sk_c8).
% 300531 [para:300520.1.1,300448.1.1.1] equal(multiply(sk_c8,sk_c5),identity).
% 300535 [hyper:300450,300467,binarycut:300477,binarycut:300457] equal(inverse(sk_c4),sk_c10).
% 300550 [hyper:300450,300469,binarycut:300479,binarycut:300459] equal(inverse(sk_c3),sk_c11).
% 300554 [para:300550.1.1,300448.1.1.1] equal(multiply(sk_c11,sk_c3),identity).
% 300569 [hyper:300450,300464,binarycut:300474,binarycut:300454] equal(multiply(sk_c8,sk_c10),sk_c11).
% 300581 [hyper:300450,300466,binarycut:300476,binarycut:300456] equal(multiply(sk_c5,sk_c8),sk_c11).
% 300587 [hyper:300450,300468,binarycut:300478,binarycut:300458] equal(multiply(sk_c4,sk_c10),sk_c9).
% 300595 [hyper:300450,300470,binarycut:300480,binarycut:300460] equal(multiply(sk_c3,sk_c11),sk_c10).
% 300596 [para:300448.1.1,300449.1.1.1,demod:300447] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 300597 [para:300508.1.1,300449.1.1.1,demod:300447] equal(X,multiply(sk_c8,multiply(sk_c6,X))).
% 300598 [para:300516.1.1,300449.1.1.1,demod:300447] equal(X,multiply(sk_c6,multiply(sk_c7,X))).
% 300604 [para:300581.1.1,300449.1.1.1] equal(multiply(sk_c11,X),multiply(sk_c5,multiply(sk_c8,X))).
% 300609 [para:300516.1.1,300597.1.2.2] equal(sk_c7,multiply(sk_c8,identity)).
% 300613 [para:300508.1.1,300596.1.2.2] equal(sk_c6,multiply(inverse(sk_c8),identity)).
% 300614 [para:300531.1.1,300596.1.2.2,demod:300613] equal(sk_c5,sk_c6).
% 300619 [para:300581.1.1,300596.1.2.2,demod:300520] equal(sk_c8,multiply(sk_c8,sk_c11)).
% 300620 [para:300587.1.1,300596.1.2.2,demod:300535] equal(sk_c10,multiply(sk_c10,sk_c9)).
% 300624 [para:300609.1.2,300449.1.1.1,demod:300447] equal(multiply(sk_c7,X),multiply(sk_c8,X)).
% 300633 [para:300614.1.2,300598.1.2.1,demod:300604,300624] equal(X,multiply(sk_c11,X)).
% 300640 [para:300633.1.2,300554.1.1] equal(sk_c3,identity).
% 300642 [para:300640.1.1,300550.1.1.1] equal(inverse(identity),sk_c11).
% 300643 [para:300640.1.1,300595.1.1.1,demod:300447] equal(sk_c11,sk_c10).
% 300646 [para:300643.1.1,300619.1.2.2,demod:300569] equal(sk_c8,sk_c11).
% 300654 [para:300646.1.2,300633.1.2.1] equal(X,multiply(sk_c8,X)).
% 300655 [para:300646.1.2,300643.1.1] equal(sk_c8,sk_c10).
% 300665 [para:300655.1.2,300620.1.2.1,demod:300654] equal(sk_c10,sk_c9).
% 300687 [para:300665.1.1,300569.1.1.2,demod:300654] equal(sk_c9,sk_c11).
% 300753 [hyper:300450,300642,demod:300633,300447,cut:300446,cut:300687] 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 29
% clause depth limited to 3
% seconds given: 4
%
%
% Split component 5 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(inverse(sk_c11),sk_c10) | -equal(multiply(sk_c10,sk_c9),sk_c11) | -equal(multiply(X,Y),sk_c11) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c9),sk_c11) | -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X1),X2) | -equal(inverse(X2),W) | -equal(multiply(X1,W),X2).
% Split part used next: -equal(inverse(sk_c11),sk_c10).
% 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 29
% clause depth limited to 3
% seconds given: 4
%
%
% 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 29
% clause depth limited to 4
% seconds given: 4
%
%
% 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 29
% clause depth limited to 5
% seconds given: 4
%
%
% 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 29
% clause depth limited to 6
% seconds given: 4
%
%
% 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 29
% clause depth limited to 7
% seconds given: 4
%
%
% 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 29
% clause depth limited to 8
% seconds given: 4
%
%
% 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 29
% clause depth limited to 9
% seconds given: 4
%
%
% 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 29
% clause depth limited to 10
% seconds given: 4
%
%
% 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 29
% clause depth limited to 11
% seconds given: 4
%
%
% 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(55,40,0,118,0,0,61904,50,1038,61904,40,1038,61967,0,1038,62548,5,1639,62548,1,1639,62548,50,1639,62548,40,1639,62611,0,1639,63218,5,2241,63221,1,2242,63221,50,2242,63221,40,2242,63284,0,2242,86648,3,3743,87788,4,4493,88950,5,5243,88951,1,5243,88951,50,5243,88951,40,5243,89014,0,5244,104471,3,5995,105430,4,6370,106039,5,6745,106040,1,6745,106040,50,6745,106040,40,6745,106103,0,6745,106922,5,8247,106923,1,8247,106923,50,8247,106923,40,8247,106986,0,8247,157438,3,12149,158690,4,14098,160052,5,16048,160053,1,16048,160053,50,16050,160053,40,16050,160116,0,16050,203318,3,18601,204230,4,19876,205314,5,21151,205315,1,21151,205315,50,21153,205315,40,21153,205378,0,21153,245013,3,22655,245768,4,23404,246654,1,24154,246654,50,24155,246654,40,24155,246717,0,24155,247541,5,25659,247544,1,25660,247544,50,25660,247544,40,25660,247607,0,25660,273068,3,26862,273844,4,27461,274443,1,28061,274443,50,28061,274443,40,28061,274506,0,28062,294643,3,28813,295125,4,29188,295500,1,29563,295500,50,29563,295500,40,29563,295500,40,29563,295609,0,29563,297148,50,29568,297257,0,29569,299644,50,29577,299644,30,29577,299644,40,29577,299699,0,29582,299822,50,29582,299877,0,29582,300056,50,29583,300056,30,29583,300056,40,29583,300111,0,29588,300225,50,29589,300280,0,29589,300445,50,29590,300445,30,29590,300445,40,29590,300500,0,29595,300752,50,29596,300752,30,29596,300752,40,29596,300807,0,29596,301011,50,29599,301066,0,29604,301334,50,29609,301389,0,29609,301665,50,29616,301720,0,29620,302004,50,29630,302059,0,29630,302349,50,29642,302404,0,29647,302702,50,29668,302757,0,29668,303063,50,29704,303118,0,29709,303434,50,29777,303489,0,29777,303815,50,29914,303815,40,29914,303870,0,29914)
%
%
% START OF PROOF
% 303817 [] equal(multiply(identity,X),X).
% 303818 [] equal(multiply(inverse(X),X),identity).
% 303819 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 303820 [] -equal(inverse(sk_c11),sk_c10).
% 303861 [?] ?
% 303862 [?] ?
% 303863 [?] ?
% 303864 [?] ?
% 303865 [?] ?
% 303866 [?] ?
% 303867 [?] ?
% 303868 [?] ?
% 303869 [?] ?
% 303870 [?] ?
% 303887 [input:303862,cut:303820] equal(inverse(sk_c6),sk_c8).
% 303888 [para:303887.1.1,303818.1.1.1] equal(multiply(sk_c8,sk_c6),identity).
% 303890 [input:303863,cut:303820] equal(inverse(sk_c7),sk_c6).
% 303891 [para:303890.1.1,303818.1.1.1] equal(multiply(sk_c6,sk_c7),identity).
% 303892 [input:303865,cut:303820] equal(inverse(sk_c5),sk_c8).
% 303893 [para:303892.1.1,303818.1.1.1] equal(multiply(sk_c8,sk_c5),identity).
% 303895 [input:303867,cut:303820] equal(inverse(sk_c4),sk_c10).
% 303896 [para:303895.1.1,303818.1.1.1] equal(multiply(sk_c10,sk_c4),identity).
% 303897 [input:303869,cut:303820] equal(inverse(sk_c3),sk_c11).
% 303898 [para:303897.1.1,303818.1.1.1] equal(multiply(sk_c11,sk_c3),identity).
% 303927 [input:303861,cut:303820] equal(multiply(sk_c7,sk_c8),sk_c6).
% 303928 [input:303864,cut:303820] equal(multiply(sk_c8,sk_c10),sk_c11).
% 303930 [input:303866,cut:303820] equal(multiply(sk_c5,sk_c8),sk_c11).
% 303931 [input:303868,cut:303820] equal(multiply(sk_c4,sk_c10),sk_c9).
% 303932 [input:303870,cut:303820] equal(multiply(sk_c3,sk_c11),sk_c10).
% 303952 [para:303888.1.1,303819.1.1.1,demod:303817] equal(X,multiply(sk_c8,multiply(sk_c6,X))).
% 303953 [para:303891.1.1,303819.1.1.1,demod:303817] equal(X,multiply(sk_c6,multiply(sk_c7,X))).
% 303954 [para:303893.1.1,303819.1.1.1,demod:303817] equal(X,multiply(sk_c8,multiply(sk_c5,X))).
% 303956 [para:303896.1.1,303819.1.1.1,demod:303817] equal(X,multiply(sk_c10,multiply(sk_c4,X))).
% 303957 [para:303898.1.1,303819.1.1.1,demod:303817] equal(X,multiply(sk_c11,multiply(sk_c3,X))).
% 303989 [para:303930.1.1,303819.1.1.1] equal(multiply(sk_c11,X),multiply(sk_c5,multiply(sk_c8,X))).
% 304007 [para:303891.1.1,303952.1.2.2] equal(sk_c7,multiply(sk_c8,identity)).
% 304008 [para:304007.1.2,303819.1.1.1,demod:303817] equal(multiply(sk_c7,X),multiply(sk_c8,X)).
% 304012 [para:303927.1.1,303953.1.2.2] equal(sk_c8,multiply(sk_c6,sk_c6)).
% 304015 [para:304012.1.2,303952.1.2.2] equal(sk_c6,multiply(sk_c8,sk_c8)).
% 304021 [para:303930.1.1,303954.1.2.2] equal(sk_c8,multiply(sk_c8,sk_c11)).
% 304027 [para:303931.1.1,303956.1.2.2] equal(sk_c10,multiply(sk_c10,sk_c9)).
% 304042 [para:303932.1.1,303957.1.2.2] equal(sk_c11,multiply(sk_c11,sk_c10)).
% 304044 [para:304008.1.1,303953.1.2.2] equal(X,multiply(sk_c6,multiply(sk_c8,X))).
% 304045 [para:303888.1.1,304044.1.2.2] equal(sk_c6,multiply(sk_c6,identity)).
% 304046 [para:303893.1.1,304044.1.2.2,demod:304045] equal(sk_c5,sk_c6).
% 304054 [para:304046.1.2,303953.1.2.1,demod:303989,304008] equal(X,multiply(sk_c11,X)).
% 304114 [para:304054.1.2,303957.1.2] equal(X,multiply(sk_c3,X)).
% 304115 [para:304054.1.2,304042.1.2] equal(sk_c11,sk_c10).
% 304121 [para:304115.1.1,304021.1.2.2] equal(sk_c8,multiply(sk_c8,sk_c10)).
% 304122 [para:304115.1.1,303957.1.2.1,demod:304114] equal(X,multiply(sk_c10,X)).
% 304132 [para:304122.1.2,304027.1.2] equal(sk_c10,sk_c9).
% 304142 [para:304132.1.1,303928.1.1.2] equal(multiply(sk_c8,sk_c9),sk_c11).
% 304145 [para:304132.1.1,304042.1.2.2,demod:304054] equal(sk_c11,sk_c9).
% 304148 [para:304145.1.1,304021.1.2.2,demod:304142] equal(sk_c8,sk_c11).
% 304153 [para:304148.1.2,303932.1.1.2,demod:304114] equal(sk_c8,sk_c10).
% 304154 [para:304148.1.2,304021.1.2.2,demod:304015] equal(sk_c8,sk_c6).
% 304156 [para:304148.1.2,304042.1.2.1,demod:304121] equal(sk_c11,sk_c8).
% 304169 [para:304154.1.2,303887.1.1.1] equal(inverse(sk_c8),sk_c8).
% 304175 [para:304156.1.1,303820.1.1.1,demod:304169,cut:304153] 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 component 6 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(inverse(sk_c11),sk_c10) | -equal(multiply(sk_c10,sk_c9),sk_c11) | -equal(multiply(X,Y),sk_c11) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c9),sk_c11) | -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X1),X2) | -equal(inverse(X2),W) | -equal(multiply(X1,W),X2).
% Split part used next: -equal(multiply(sk_c10,sk_c9),sk_c11).
% 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 29
% clause depth limited to 3
% seconds given: 4
%
%
% 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 29
% clause depth limited to 4
% seconds given: 4
%
%
% 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 29
% clause depth limited to 5
% seconds given: 4
%
%
% 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 29
% clause depth limited to 6
% seconds given: 4
%
%
% 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 29
% clause depth limited to 7
% seconds given: 4
%
%
% 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 29
% clause depth limited to 8
% seconds given: 4
%
%
% 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 29
% clause depth limited to 9
% seconds given: 4
%
%
% 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 29
% clause depth limited to 10
% seconds given: 4
%
%
% 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 29
% clause depth limited to 11
% seconds given: 4
%
%
% 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(55,40,0,118,0,0,61904,50,1038,61904,40,1038,61967,0,1038,62548,5,1639,62548,1,1639,62548,50,1639,62548,40,1639,62611,0,1639,63218,5,2241,63221,1,2242,63221,50,2242,63221,40,2242,63284,0,2242,86648,3,3743,87788,4,4493,88950,5,5243,88951,1,5243,88951,50,5243,88951,40,5243,89014,0,5244,104471,3,5995,105430,4,6370,106039,5,6745,106040,1,6745,106040,50,6745,106040,40,6745,106103,0,6745,106922,5,8247,106923,1,8247,106923,50,8247,106923,40,8247,106986,0,8247,157438,3,12149,158690,4,14098,160052,5,16048,160053,1,16048,160053,50,16050,160053,40,16050,160116,0,16050,203318,3,18601,204230,4,19876,205314,5,21151,205315,1,21151,205315,50,21153,205315,40,21153,205378,0,21153,245013,3,22655,245768,4,23404,246654,1,24154,246654,50,24155,246654,40,24155,246717,0,24155,247541,5,25659,247544,1,25660,247544,50,25660,247544,40,25660,247607,0,25660,273068,3,26862,273844,4,27461,274443,1,28061,274443,50,28061,274443,40,28061,274506,0,28062,294643,3,28813,295125,4,29188,295500,1,29563,295500,50,29563,295500,40,29563,295500,40,29563,295609,0,29563,297148,50,29568,297257,0,29569,299644,50,29577,299644,30,29577,299644,40,29577,299699,0,29582,299822,50,29582,299877,0,29582,300056,50,29583,300056,30,29583,300056,40,29583,300111,0,29588,300225,50,29589,300280,0,29589,300445,50,29590,300445,30,29590,300445,40,29590,300500,0,29595,300752,50,29596,300752,30,29596,300752,40,29596,300807,0,29596,301011,50,29599,301066,0,29604,301334,50,29609,301389,0,29609,301665,50,29616,301720,0,29620,302004,50,29630,302059,0,29630,302349,50,29642,302404,0,29647,302702,50,29668,302757,0,29668,303063,50,29704,303118,0,29709,303434,50,29777,303489,0,29777,303815,50,29914,303815,40,29914,303870,0,29914,304174,50,29915,304174,30,29915,304174,40,29915,304229,0,29915,304433,50,29918,304488,0,29922,304756,50,29927,304811,0,29927,305087,50,29933,305142,0,29938,305426,50,29947,305481,0,29947,305771,50,29960,305826,0,29964,306124,50,29985,306179,0,29985,306485,50,30021,306540,0,30026,306856,50,30094,306911,0,30094,307237,50,30229,307237,40,30229,307292,0,30229)
%
%
% START OF PROOF
% 307028 [?] ?
% 307239 [] equal(multiply(identity,X),X).
% 307240 [] equal(multiply(inverse(X),X),identity).
% 307241 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 307242 [] -equal(multiply(sk_c10,sk_c9),sk_c11).
% 307279 [?] ?
% 307280 [?] ?
% 307366 [input:307279,cut:307242] equal(inverse(sk_c4),sk_c10).
% 307367 [para:307366.1.1,307240.1.1.1] equal(multiply(sk_c10,sk_c4),identity).
% 307396 [input:307280,cut:307242] equal(multiply(sk_c4,sk_c10),sk_c9).
% 307431 [para:307367.1.1,307241.1.1.1,demod:307239] equal(X,multiply(sk_c10,multiply(sk_c4,X))).
% 307480 [para:307396.1.1,307431.1.2.2] equal(sk_c10,multiply(sk_c10,sk_c9)).
% 307481 [para:307480.1.2,307242.1.1,cut:307028] 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: 33222
% derived clauses: 4148433
% kept clauses: 201100
% kept size sum: 781781
% kept mid-nuclei: 59209
% kept new demods: 5276
% forw unit-subs: 1422149
% forw double-subs: 2241510
% forw overdouble-subs: 161792
% backward subs: 13213
% fast unit cutoff: 31955
% full unit cutoff: 0
% dbl unit cutoff: 13602
% real runtime : 304.69
% process. runtime: 302.29
% specific non-discr-tree subsumption statistics:
% tried: 82328381
% length fails: 11025904
% strength fails: 28143913
% predlist fails: 346415
% aux str. fails: 13295907
% by-lit fails: 14997744
% full subs tried: 7623611
% full subs fail: 7524114
%
% ; 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/GRP379-1+eq_r.in")
%
%------------------------------------------------------------------------------