%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP366-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 : art07.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.2s
% Output : Assurance 298.2s
% 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/GRP366-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 31)
% (binary-unit 12 #f)
% (binary-unit-uniteq 12 #f)
% (binary-posweight-kb-big-order 60 #f 3 31)
% (binary-posweight-lex-big-order 30 #f 3 31)
% (binary 30 #t)
% (binary-posweight-kb-big-order 156 #f)
% (binary-posweight-lex-big-order 102 #f)
% (binary-posweight-firstpref-order 60 #f)
% (binary-order 30 #f)
% (binary-posweight-kb-small-order 48 #f)
% (binary-posweight-lex-small-order 30 #f)
%
%
% SOS clause
% -equal(multiply(sk_c8,sk_c10),sk_c9) | -equal(multiply(sk_c10,X),sk_c9) | -equal(multiply(Y,sk_c10),X) | -equal(inverse(Y),sk_c10) | -equal(multiply(Z,sk_c8),sk_c10) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c9,sk_c10),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(inverse(sk_c9),sk_c8) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c9) | -equal(multiply(V,sk_c8),sk_c9) | -equal(inverse(W),X1) | -equal(inverse(X1),sk_c10) | -equal(multiply(W,sk_c10),X1).
% was split for some strategies as:
% -equal(inverse(W),X1) | -equal(inverse(X1),sk_c10) | -equal(multiply(W,sk_c10),X1).
% -equal(inverse(V),sk_c9) | -equal(multiply(V,sk_c8),sk_c9).
% -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10).
% -equal(multiply(Z,sk_c8),sk_c10) | -equal(inverse(Z),sk_c8).
% -equal(multiply(sk_c10,X),sk_c9) | -equal(multiply(Y,sk_c10),X) | -equal(inverse(Y),sk_c10).
% -equal(multiply(sk_c8,sk_c10),sk_c9).
% -equal(multiply(sk_c9,sk_c10),sk_c8).
% -equal(inverse(sk_c9),sk_c8).
% -equal(multiply(sk_c10,sk_c8),sk_c9).
%
% Starting a split proof attempt with 9 components.
%
% Split component 1 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c8,sk_c10),sk_c9) | -equal(multiply(sk_c10,X),sk_c9) | -equal(multiply(Y,sk_c10),X) | -equal(inverse(Y),sk_c10) | -equal(multiply(Z,sk_c8),sk_c10) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c9,sk_c10),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(inverse(sk_c9),sk_c8) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c9) | -equal(multiply(V,sk_c8),sk_c9) | -equal(inverse(W),X1) | -equal(inverse(X1),sk_c10) | -equal(multiply(W,sk_c10),X1).
% Split part used next: -equal(inverse(W),X1) | -equal(inverse(X1),sk_c10) | -equal(multiply(W,sk_c10),X1).
% END OF PROOFPART
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(65,40,0,136,0,0,5462,50,76,5533,0,77,20977,50,372,21048,0,372,38077,50,746,38148,0,746,58311,50,1246,58311,40,1246,58382,0,1247,62398,3,1550,63642,4,1699,63750,5,1848,63750,1,1848,63750,50,1848,63750,40,1848,63821,0,1848,66290,3,2150,66380,4,2301,66415,5,2449,66415,1,2449,66415,50,2449,66415,40,2449,66486,0,2449,96313,3,3950,97200,4,4700,97896,1,5450,97896,50,5451,97896,40,5451,97967,0,5451,116817,3,6203,117608,4,6577,118166,1,6952,118166,50,6952,118166,40,6952,118237,0,6952,125682,3,7762,127657,4,8078,130003,1,8453,130003,50,8453,130003,40,8453,130074,0,8453,299459,3,12357,300052,4,14305,300621,1,16254,300621,50,16257,300621,40,16257,300692,0,16257,412145,3,18809,412592,4,20084,412948,5,21358,412949,1,21358,412949,50,21361,412949,40,21361,413020,0,21361,478208,3,22868,478541,4,23612,479038,5,24362,479039,1,24362,479039,50,24364,479039,40,24364,479110,0,24364,487774,3,25133,488929,4,25491,489722,5,25865,489723,1,25865,489723,50,25865,489723,40,25865,489794,0,25865,542811,3,27070,543048,4,27666,543361,5,28267,543362,1,28267,543362,50,28268,543362,40,28268,543433,0,28269,576672,3,29020,576906,4,29395,577187,1,29770,577187,50,29771,577187,40,29771,577187,40,29771,577252,0,29771)
%
%
% START OF PROOF
% 577189 [] equal(multiply(identity,X),X).
% 577190 [] equal(multiply(inverse(X),X),identity).
% 577191 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 577192 [] -equal(multiply(X,sk_c10),Y) | -equal(inverse(Y),sk_c10) | -equal(inverse(X),Y).
% 577193 [?] ?
% 577194 [] equal(inverse(sk_c3),sk_c8) | equal(inverse(sk_c6),sk_c10).
% 577195 [] equal(inverse(sk_c3),sk_c8) | equal(inverse(sk_c7),sk_c6).
% 577203 [] equal(multiply(sk_c3,sk_c8),sk_c10) | equal(multiply(sk_c7,sk_c10),sk_c6).
% 577204 [] equal(multiply(sk_c3,sk_c8),sk_c10) | equal(inverse(sk_c6),sk_c10).
% 577205 [] equal(multiply(sk_c3,sk_c8),sk_c10) | equal(inverse(sk_c7),sk_c6).
% 577213 [?] ?
% 577214 [] equal(inverse(sk_c1),sk_c10) | equal(inverse(sk_c6),sk_c10).
% 577215 [] equal(inverse(sk_c1),sk_c10) | equal(inverse(sk_c7),sk_c6).
% 577223 [] equal(multiply(sk_c1,sk_c10),sk_c2) | equal(multiply(sk_c7,sk_c10),sk_c6).
% 577224 [] equal(multiply(sk_c1,sk_c10),sk_c2) | equal(inverse(sk_c6),sk_c10).
% 577225 [] equal(multiply(sk_c1,sk_c10),sk_c2) | equal(inverse(sk_c7),sk_c6).
% 577233 [] equal(multiply(sk_c10,sk_c2),sk_c9) | equal(multiply(sk_c7,sk_c10),sk_c6).
% 577234 [] equal(multiply(sk_c10,sk_c2),sk_c9) | equal(inverse(sk_c6),sk_c10).
% 577235 [] equal(multiply(sk_c10,sk_c2),sk_c9) | equal(inverse(sk_c7),sk_c6).
% 577243 [] equal(multiply(sk_c8,sk_c10),sk_c9) | equal(multiply(sk_c7,sk_c10),sk_c6).
% 577244 [] equal(multiply(sk_c8,sk_c10),sk_c9) | equal(inverse(sk_c6),sk_c10).
% 577245 [] equal(multiply(sk_c8,sk_c10),sk_c9) | equal(inverse(sk_c7),sk_c6).
% 577265 [hyper:577192,577195,577194,binarycut:577193] equal(inverse(sk_c3),sk_c8).
% 577271 [para:577265.1.1,577190.1.1.1] equal(multiply(sk_c8,sk_c3),identity).
% 577292 [hyper:577192,577215,577214,binarycut:577213] equal(inverse(sk_c1),sk_c10).
% 577297 [para:577292.1.1,577190.1.1.1] equal(multiply(sk_c10,sk_c1),identity).
% 577311 [hyper:577192,577205,577203,577204] equal(multiply(sk_c3,sk_c8),sk_c10).
% 577331 [hyper:577192,577225,577223,577224] equal(multiply(sk_c1,sk_c10),sk_c2).
% 577350 [hyper:577192,577233,577234,577235] equal(multiply(sk_c10,sk_c2),sk_c9).
% 577378 [hyper:577192,577243,577244,577245] equal(multiply(sk_c8,sk_c10),sk_c9).
% 577380 [para:577190.1.1,577191.1.1.1,demod:577189] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 577381 [para:577271.1.1,577191.1.1.1,demod:577189] equal(X,multiply(sk_c8,multiply(sk_c3,X))).
% 577382 [para:577297.1.1,577191.1.1.1,demod:577189] equal(X,multiply(sk_c10,multiply(sk_c1,X))).
% 577383 [para:577311.1.1,577191.1.1.1] equal(multiply(sk_c10,X),multiply(sk_c3,multiply(sk_c8,X))).
% 577388 [para:577378.1.1,577191.1.1.1] equal(multiply(sk_c9,X),multiply(sk_c8,multiply(sk_c10,X))).
% 577393 [para:577311.1.1,577381.1.2.2,demod:577378] equal(sk_c8,sk_c9).
% 577394 [para:577393.1.1,577271.1.1.1] equal(multiply(sk_c9,sk_c3),identity).
% 577395 [para:577393.1.1,577311.1.1.2] equal(multiply(sk_c3,sk_c9),sk_c10).
% 577396 [para:577393.1.1,577378.1.1.1] equal(multiply(sk_c9,sk_c10),sk_c9).
% 577406 [para:577331.1.1,577380.1.2.2,demod:577350,577292] equal(sk_c10,sk_c9).
% 577424 [para:577396.1.1,577380.1.2.2,demod:577190] equal(sk_c10,identity).
% 577426 [para:577424.1.1,577297.1.1.1,demod:577189] equal(sk_c1,identity).
% 577430 [para:577424.1.1,577406.1.1] equal(identity,sk_c9).
% 577437 [para:577426.1.1,577382.1.2.2.1,demod:577189] equal(X,multiply(sk_c10,X)).
% 577440 [para:577271.1.1,577383.1.2.2,demod:577437] equal(sk_c3,multiply(sk_c3,identity)).
% 577441 [para:577430.1.2,577394.1.1.1,demod:577189] equal(sk_c3,identity).
% 577442 [para:577430.1.2,577395.1.1.2,demod:577440] equal(sk_c3,sk_c10).
% 577451 [para:577441.1.1,577311.1.1.1,demod:577189] equal(sk_c8,sk_c10).
% 577460 [para:577442.1.2,577406.1.1] equal(sk_c3,sk_c9).
% 577466 [para:577460.1.1,577265.1.1.1] equal(inverse(sk_c9),sk_c8).
% 577467 [hyper:577192,577388,demod:577466,577378,577437,cut:577451,cut:577393] 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 31
% clause depth limited to 3
% seconds given: 2
%
%
% Split component 2 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c8,sk_c10),sk_c9) | -equal(multiply(sk_c10,X),sk_c9) | -equal(multiply(Y,sk_c10),X) | -equal(inverse(Y),sk_c10) | -equal(multiply(Z,sk_c8),sk_c10) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c9,sk_c10),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(inverse(sk_c9),sk_c8) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c9) | -equal(multiply(V,sk_c8),sk_c9) | -equal(inverse(W),X1) | -equal(inverse(X1),sk_c10) | -equal(multiply(W,sk_c10),X1).
% Split part used next: -equal(inverse(V),sk_c9) | -equal(multiply(V,sk_c8),sk_c9).
% 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 31
% clause depth limited to 3
% seconds given: 2
%
%
% 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 31
% clause depth limited to 4
% seconds given: 2
%
%
% 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 31
% clause depth limited to 5
% seconds given: 2
%
%
% 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 31
% clause depth limited to 6
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(65,40,0,136,0,0,5462,50,76,5533,0,77,20977,50,372,21048,0,372,38077,50,746,38148,0,746,58311,50,1246,58311,40,1246,58382,0,1247,62398,3,1550,63642,4,1699,63750,5,1848,63750,1,1848,63750,50,1848,63750,40,1848,63821,0,1848,66290,3,2150,66380,4,2301,66415,5,2449,66415,1,2449,66415,50,2449,66415,40,2449,66486,0,2449,96313,3,3950,97200,4,4700,97896,1,5450,97896,50,5451,97896,40,5451,97967,0,5451,116817,3,6203,117608,4,6577,118166,1,6952,118166,50,6952,118166,40,6952,118237,0,6952,125682,3,7762,127657,4,8078,130003,1,8453,130003,50,8453,130003,40,8453,130074,0,8453,299459,3,12357,300052,4,14305,300621,1,16254,300621,50,16257,300621,40,16257,300692,0,16257,412145,3,18809,412592,4,20084,412948,5,21358,412949,1,21358,412949,50,21361,412949,40,21361,413020,0,21361,478208,3,22868,478541,4,23612,479038,5,24362,479039,1,24362,479039,50,24364,479039,40,24364,479110,0,24364,487774,3,25133,488929,4,25491,489722,5,25865,489723,1,25865,489723,50,25865,489723,40,25865,489794,0,25865,542811,3,27070,543048,4,27666,543361,5,28267,543362,1,28267,543362,50,28268,543362,40,28268,543433,0,28269,576672,3,29020,576906,4,29395,577187,1,29770,577187,50,29771,577187,40,29771,577187,40,29771,577252,0,29771,577466,50,29771,577466,30,29771,577466,40,29771,577531,0,29771,577664,50,29772,577729,0,29779,577916,50,29781,577981,0,29782,578177,50,29786,578242,0,29790)
%
%
% START OF PROOF
% 578179 [] equal(multiply(identity,X),X).
% 578180 [] equal(multiply(inverse(X),X),identity).
% 578181 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 578182 [] -equal(multiply(X,sk_c8),sk_c9) | -equal(inverse(X),sk_c9).
% 578186 [?] ?
% 578187 [] equal(inverse(sk_c3),sk_c8) | equal(inverse(sk_c5),sk_c9).
% 578196 [] equal(multiply(sk_c3,sk_c8),sk_c10) | equal(multiply(sk_c5,sk_c8),sk_c9).
% 578197 [] equal(multiply(sk_c3,sk_c8),sk_c10) | equal(inverse(sk_c5),sk_c9).
% 578206 [?] ?
% 578207 [] equal(inverse(sk_c1),sk_c10) | equal(inverse(sk_c5),sk_c9).
% 578216 [] equal(multiply(sk_c1,sk_c10),sk_c2) | equal(multiply(sk_c5,sk_c8),sk_c9).
% 578217 [] equal(multiply(sk_c1,sk_c10),sk_c2) | equal(inverse(sk_c5),sk_c9).
% 578226 [] equal(multiply(sk_c10,sk_c2),sk_c9) | equal(multiply(sk_c5,sk_c8),sk_c9).
% 578227 [] equal(multiply(sk_c10,sk_c2),sk_c9) | equal(inverse(sk_c5),sk_c9).
% 578236 [] equal(multiply(sk_c8,sk_c10),sk_c9) | equal(multiply(sk_c5,sk_c8),sk_c9).
% 578237 [] equal(multiply(sk_c8,sk_c10),sk_c9) | equal(inverse(sk_c5),sk_c9).
% 578248 [hyper:578182,578187,binarycut:578186] equal(inverse(sk_c3),sk_c8).
% 578249 [para:578248.1.1,578180.1.1.1] equal(multiply(sk_c8,sk_c3),identity).
% 578255 [hyper:578182,578207,binarycut:578206] equal(inverse(sk_c1),sk_c10).
% 578268 [hyper:578182,578196,578197] equal(multiply(sk_c3,sk_c8),sk_c10).
% 578279 [hyper:578182,578216,578217] equal(multiply(sk_c1,sk_c10),sk_c2).
% 578293 [hyper:578182,578226,578227] equal(multiply(sk_c10,sk_c2),sk_c9).
% 578299 [hyper:578182,578236,578237] equal(multiply(sk_c8,sk_c10),sk_c9).
% 578300 [para:578180.1.1,578181.1.1.1,demod:578179] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 578301 [para:578249.1.1,578181.1.1.1,demod:578179] equal(X,multiply(sk_c8,multiply(sk_c3,X))).
% 578307 [para:578268.1.1,578301.1.2.2,demod:578299] equal(sk_c8,sk_c9).
% 578308 [para:578307.1.1,578249.1.1.1] equal(multiply(sk_c9,sk_c3),identity).
% 578310 [para:578307.1.1,578299.1.1.1] equal(multiply(sk_c9,sk_c10),sk_c9).
% 578314 [para:578180.1.1,578300.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 578317 [para:578279.1.1,578300.1.2.2,demod:578293,578255] equal(sk_c10,sk_c9).
% 578319 [para:578181.1.1,578300.1.2.2] equal(X,multiply(inverse(multiply(Y,Z)),multiply(Y,multiply(Z,X)))).
% 578323 [para:578300.1.2,578300.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 578331 [para:578310.1.1,578300.1.2.2,demod:578180] equal(sk_c10,identity).
% 578336 [para:578331.1.1,578299.1.1.2] equal(multiply(sk_c8,identity),sk_c9).
% 578337 [para:578331.1.1,578317.1.1] equal(identity,sk_c9).
% 578346 [para:578337.1.2,578308.1.1.1,demod:578179] equal(sk_c3,identity).
% 578357 [para:578346.1.1,578301.1.2.2.1,demod:578179] equal(X,multiply(sk_c8,X)).
% 578379 [para:578180.1.1,578319.1.2.2] equal(X,multiply(inverse(multiply(inverse(multiply(Y,X)),Y)),identity)).
% 578380 [para:578180.1.1,578319.1.2.2.2] equal(X,multiply(inverse(multiply(Y,inverse(X))),multiply(Y,identity))).
% 578402 [para:578323.1.2,578314.1.2] equal(X,multiply(X,identity)).
% 578405 [para:578402.1.2,578314.1.2] equal(X,inverse(inverse(X))).
% 578418 [para:578379.1.2,578402.1.2] equal(inverse(multiply(inverse(multiply(X,Y)),X)),Y).
% 578426 [para:578357.1.2,578380.1.2.1.1,demod:578336,578405] equal(X,multiply(X,sk_c9)).
% 578441 [hyper:578182,578418,demod:578179,578180,578426,cut:578307] 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 31
% clause depth limited to 6
% seconds given: 2
%
%
% Split component 3 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c8,sk_c10),sk_c9) | -equal(multiply(sk_c10,X),sk_c9) | -equal(multiply(Y,sk_c10),X) | -equal(inverse(Y),sk_c10) | -equal(multiply(Z,sk_c8),sk_c10) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c9,sk_c10),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(inverse(sk_c9),sk_c8) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c9) | -equal(multiply(V,sk_c8),sk_c9) | -equal(inverse(W),X1) | -equal(inverse(X1),sk_c10) | -equal(multiply(W,sk_c10),X1).
% 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 31
% clause depth limited to 3
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(65,40,0,136,0,0,5462,50,76,5533,0,77,20977,50,372,21048,0,372,38077,50,746,38148,0,746,58311,50,1246,58311,40,1246,58382,0,1247,62398,3,1550,63642,4,1699,63750,5,1848,63750,1,1848,63750,50,1848,63750,40,1848,63821,0,1848,66290,3,2150,66380,4,2301,66415,5,2449,66415,1,2449,66415,50,2449,66415,40,2449,66486,0,2449,96313,3,3950,97200,4,4700,97896,1,5450,97896,50,5451,97896,40,5451,97967,0,5451,116817,3,6203,117608,4,6577,118166,1,6952,118166,50,6952,118166,40,6952,118237,0,6952,125682,3,7762,127657,4,8078,130003,1,8453,130003,50,8453,130003,40,8453,130074,0,8453,299459,3,12357,300052,4,14305,300621,1,16254,300621,50,16257,300621,40,16257,300692,0,16257,412145,3,18809,412592,4,20084,412948,5,21358,412949,1,21358,412949,50,21361,412949,40,21361,413020,0,21361,478208,3,22868,478541,4,23612,479038,5,24362,479039,1,24362,479039,50,24364,479039,40,24364,479110,0,24364,487774,3,25133,488929,4,25491,489722,5,25865,489723,1,25865,489723,50,25865,489723,40,25865,489794,0,25865,542811,3,27070,543048,4,27666,543361,5,28267,543362,1,28267,543362,50,28268,543362,40,28268,543433,0,28269,576672,3,29020,576906,4,29395,577187,1,29770,577187,50,29771,577187,40,29771,577187,40,29771,577252,0,29771,577466,50,29771,577466,30,29771,577466,40,29771,577531,0,29771,577664,50,29772,577729,0,29779,577916,50,29781,577981,0,29782,578177,50,29786,578242,0,29790,578440,50,29792,578440,30,29792,578440,40,29792,578505,0,29793)
%
%
% START OF PROOF
% 578442 [] equal(multiply(identity,X),X).
% 578443 [] equal(multiply(inverse(X),X),identity).
% 578444 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 578445 [] -equal(multiply(X,sk_c10),sk_c9) | -equal(inverse(X),sk_c10).
% 578453 [] equal(inverse(sk_c3),sk_c8) | equal(inverse(sk_c4),sk_c10).
% 578454 [?] ?
% 578463 [] equal(multiply(sk_c3,sk_c8),sk_c10) | equal(inverse(sk_c4),sk_c10).
% 578464 [] equal(multiply(sk_c3,sk_c8),sk_c10) | equal(multiply(sk_c4,sk_c10),sk_c9).
% 578473 [] equal(inverse(sk_c1),sk_c10) | equal(inverse(sk_c4),sk_c10).
% 578474 [?] ?
% 578483 [] equal(multiply(sk_c1,sk_c10),sk_c2) | equal(inverse(sk_c4),sk_c10).
% 578484 [] equal(multiply(sk_c1,sk_c10),sk_c2) | equal(multiply(sk_c4,sk_c10),sk_c9).
% 578493 [] equal(multiply(sk_c10,sk_c2),sk_c9) | equal(inverse(sk_c4),sk_c10).
% 578494 [] equal(multiply(sk_c10,sk_c2),sk_c9) | equal(multiply(sk_c4,sk_c10),sk_c9).
% 578503 [] equal(multiply(sk_c8,sk_c10),sk_c9) | equal(inverse(sk_c4),sk_c10).
% 578504 [] equal(multiply(sk_c8,sk_c10),sk_c9) | equal(multiply(sk_c4,sk_c10),sk_c9).
% 578514 [hyper:578445,578453,binarycut:578454] equal(inverse(sk_c3),sk_c8).
% 578515 [para:578514.1.1,578443.1.1.1] equal(multiply(sk_c8,sk_c3),identity).
% 578534 [hyper:578445,578473,binarycut:578474] equal(inverse(sk_c1),sk_c10).
% 578537 [para:578534.1.1,578443.1.1.1] equal(multiply(sk_c10,sk_c1),identity).
% 578566 [hyper:578445,578464,578463] equal(multiply(sk_c3,sk_c8),sk_c10).
% 578595 [hyper:578445,578484,578483] equal(multiply(sk_c1,sk_c10),sk_c2).
% 578601 [hyper:578445,578494,578493] equal(multiply(sk_c10,sk_c2),sk_c9).
% 578614 [hyper:578445,578504,578503] equal(multiply(sk_c8,sk_c10),sk_c9).
% 578616 [para:578443.1.1,578444.1.1.1,demod:578442] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 578617 [para:578515.1.1,578444.1.1.1,demod:578442] equal(X,multiply(sk_c8,multiply(sk_c3,X))).
% 578625 [para:578566.1.1,578617.1.2.2,demod:578614] equal(sk_c8,sk_c9).
% 578628 [para:578625.1.1,578614.1.1.1] equal(multiply(sk_c9,sk_c10),sk_c9).
% 578634 [para:578595.1.1,578616.1.2.2,demod:578601,578534] equal(sk_c10,sk_c9).
% 578648 [para:578628.1.1,578616.1.2.2,demod:578443] equal(sk_c10,identity).
% 578650 [para:578648.1.1,578537.1.1.1,demod:578442] equal(sk_c1,identity).
% 578658 [para:578650.1.1,578534.1.1.1] equal(inverse(identity),sk_c10).
% 578685 [hyper:578445,578658,demod:578442,cut:578634] 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 31
% clause depth limited to 3
% seconds given: 2
%
%
% Split component 4 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c8,sk_c10),sk_c9) | -equal(multiply(sk_c10,X),sk_c9) | -equal(multiply(Y,sk_c10),X) | -equal(inverse(Y),sk_c10) | -equal(multiply(Z,sk_c8),sk_c10) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c9,sk_c10),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(inverse(sk_c9),sk_c8) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c9) | -equal(multiply(V,sk_c8),sk_c9) | -equal(inverse(W),X1) | -equal(inverse(X1),sk_c10) | -equal(multiply(W,sk_c10),X1).
% Split part used next: -equal(multiply(Z,sk_c8),sk_c10) | -equal(inverse(Z),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 31
% clause depth limited to 3
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(65,40,0,136,0,0,5462,50,76,5533,0,77,20977,50,372,21048,0,372,38077,50,746,38148,0,746,58311,50,1246,58311,40,1246,58382,0,1247,62398,3,1550,63642,4,1699,63750,5,1848,63750,1,1848,63750,50,1848,63750,40,1848,63821,0,1848,66290,3,2150,66380,4,2301,66415,5,2449,66415,1,2449,66415,50,2449,66415,40,2449,66486,0,2449,96313,3,3950,97200,4,4700,97896,1,5450,97896,50,5451,97896,40,5451,97967,0,5451,116817,3,6203,117608,4,6577,118166,1,6952,118166,50,6952,118166,40,6952,118237,0,6952,125682,3,7762,127657,4,8078,130003,1,8453,130003,50,8453,130003,40,8453,130074,0,8453,299459,3,12357,300052,4,14305,300621,1,16254,300621,50,16257,300621,40,16257,300692,0,16257,412145,3,18809,412592,4,20084,412948,5,21358,412949,1,21358,412949,50,21361,412949,40,21361,413020,0,21361,478208,3,22868,478541,4,23612,479038,5,24362,479039,1,24362,479039,50,24364,479039,40,24364,479110,0,24364,487774,3,25133,488929,4,25491,489722,5,25865,489723,1,25865,489723,50,25865,489723,40,25865,489794,0,25865,542811,3,27070,543048,4,27666,543361,5,28267,543362,1,28267,543362,50,28268,543362,40,28268,543433,0,28269,576672,3,29020,576906,4,29395,577187,1,29770,577187,50,29771,577187,40,29771,577187,40,29771,577252,0,29771,577466,50,29771,577466,30,29771,577466,40,29771,577531,0,29771,577664,50,29772,577729,0,29779,577916,50,29781,577981,0,29782,578177,50,29786,578242,0,29790,578440,50,29792,578440,30,29792,578440,40,29792,578505,0,29793,578684,50,29793,578684,30,29793,578684,40,29793,578749,0,29798)
%
%
% START OF PROOF
% 578686 [] equal(multiply(identity,X),X).
% 578687 [] equal(multiply(inverse(X),X),identity).
% 578688 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 578689 [] -equal(multiply(X,sk_c8),sk_c10) | -equal(inverse(X),sk_c8).
% 578690 [] equal(multiply(sk_c7,sk_c10),sk_c6) | equal(inverse(sk_c3),sk_c8).
% 578691 [] equal(inverse(sk_c3),sk_c8) | equal(inverse(sk_c6),sk_c10).
% 578692 [] equal(inverse(sk_c3),sk_c8) | equal(inverse(sk_c7),sk_c6).
% 578693 [] equal(multiply(sk_c5,sk_c8),sk_c9) | equal(inverse(sk_c3),sk_c8).
% 578694 [] equal(inverse(sk_c3),sk_c8) | equal(inverse(sk_c5),sk_c9).
% 578695 [] equal(multiply(sk_c10,sk_c8),sk_c9) | equal(inverse(sk_c3),sk_c8).
% 578696 [] equal(inverse(sk_c3),sk_c8) | equal(inverse(sk_c9),sk_c8).
% 578697 [] equal(inverse(sk_c3),sk_c8) | equal(inverse(sk_c4),sk_c10).
% 578698 [] equal(multiply(sk_c4,sk_c10),sk_c9) | equal(inverse(sk_c3),sk_c8).
% 578699 [] equal(multiply(sk_c9,sk_c10),sk_c8) | equal(inverse(sk_c3),sk_c8).
% 578700 [?] ?
% 578701 [?] ?
% 578702 [?] ?
% 578703 [?] ?
% 578704 [?] ?
% 578705 [?] ?
% 578706 [?] ?
% 578707 [?] ?
% 578708 [?] ?
% 578709 [?] ?
% 578752 [hyper:578689,578691,binarycut:578701] equal(inverse(sk_c6),sk_c10).
% 578753 [para:578752.1.1,578687.1.1.1] equal(multiply(sk_c10,sk_c6),identity).
% 578757 [hyper:578689,578692,binarycut:578702] equal(inverse(sk_c7),sk_c6).
% 578758 [para:578757.1.1,578687.1.1.1] equal(multiply(sk_c6,sk_c7),identity).
% 578761 [hyper:578689,578694,binarycut:578704] equal(inverse(sk_c5),sk_c9).
% 578764 [hyper:578689,578690,binarycut:578700] equal(multiply(sk_c7,sk_c10),sk_c6).
% 578768 [hyper:578689,578696,binarycut:578706] equal(inverse(sk_c9),sk_c8).
% 578776 [hyper:578689,578693,binarycut:578703] equal(multiply(sk_c5,sk_c8),sk_c9).
% 578779 [hyper:578689,578697,binarycut:578707] equal(inverse(sk_c4),sk_c10).
% 578783 [hyper:578689,578695,binarycut:578705] equal(multiply(sk_c10,sk_c8),sk_c9).
% 578786 [hyper:578689,578698,binarycut:578708] equal(multiply(sk_c4,sk_c10),sk_c9).
% 578789 [hyper:578689,578699,binarycut:578709] equal(multiply(sk_c9,sk_c10),sk_c8).
% 578790 [para:578687.1.1,578688.1.1.1,demod:578686] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 578791 [para:578753.1.1,578688.1.1.1,demod:578686] equal(X,multiply(sk_c10,multiply(sk_c6,X))).
% 578792 [para:578758.1.1,578688.1.1.1,demod:578686] equal(X,multiply(sk_c6,multiply(sk_c7,X))).
% 578793 [para:578764.1.1,578688.1.1.1] equal(multiply(sk_c6,X),multiply(sk_c7,multiply(sk_c10,X))).
% 578801 [para:578758.1.1,578791.1.2.2] equal(sk_c7,multiply(sk_c10,identity)).
% 578802 [para:578801.1.2,578688.1.1.1,demod:578686] equal(multiply(sk_c7,X),multiply(sk_c10,X)).
% 578803 [para:578764.1.1,578792.1.2.2] equal(sk_c10,multiply(sk_c6,sk_c6)).
% 578808 [para:578776.1.1,578790.1.2.2,demod:578761] equal(sk_c8,multiply(sk_c9,sk_c9)).
% 578811 [para:578786.1.1,578790.1.2.2,demod:578802,578779] equal(sk_c10,multiply(sk_c7,sk_c9)).
% 578812 [para:578789.1.1,578790.1.2.2,demod:578768] equal(sk_c10,multiply(sk_c8,sk_c8)).
% 578822 [para:578808.1.2,578790.1.2.2,demod:578812,578768] equal(sk_c9,sk_c10).
% 578824 [para:578822.1.2,578764.1.1.2,demod:578811] equal(sk_c10,sk_c6).
% 578831 [para:578783.1.1,578793.1.2.2,demod:578811] equal(multiply(sk_c6,sk_c8),sk_c10).
% 578834 [para:578824.1.1,578753.1.1.1,demod:578803] equal(sk_c10,identity).
% 578840 [para:578834.1.1,578753.1.1.1,demod:578686] equal(sk_c6,identity).
% 578847 [para:578834.1.1,578822.1.2] equal(sk_c9,identity).
% 578858 [para:578840.1.1,578752.1.1.1] equal(inverse(identity),sk_c10).
% 578868 [para:578847.1.1,578768.1.1.1,demod:578858] equal(sk_c10,sk_c8).
% 578895 [hyper:578689,578831,demod:578752,cut:578868] 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 31
% clause depth limited to 3
% seconds given: 2
%
%
% Split component 5 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c8,sk_c10),sk_c9) | -equal(multiply(sk_c10,X),sk_c9) | -equal(multiply(Y,sk_c10),X) | -equal(inverse(Y),sk_c10) | -equal(multiply(Z,sk_c8),sk_c10) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c9,sk_c10),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(inverse(sk_c9),sk_c8) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c9) | -equal(multiply(V,sk_c8),sk_c9) | -equal(inverse(W),X1) | -equal(inverse(X1),sk_c10) | -equal(multiply(W,sk_c10),X1).
% Split part used next: -equal(multiply(sk_c10,X),sk_c9) | -equal(multiply(Y,sk_c10),X) | -equal(inverse(Y),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 31
% clause depth limited to 3
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(65,40,0,136,0,0,5462,50,76,5533,0,77,20977,50,372,21048,0,372,38077,50,746,38148,0,746,58311,50,1246,58311,40,1246,58382,0,1247,62398,3,1550,63642,4,1699,63750,5,1848,63750,1,1848,63750,50,1848,63750,40,1848,63821,0,1848,66290,3,2150,66380,4,2301,66415,5,2449,66415,1,2449,66415,50,2449,66415,40,2449,66486,0,2449,96313,3,3950,97200,4,4700,97896,1,5450,97896,50,5451,97896,40,5451,97967,0,5451,116817,3,6203,117608,4,6577,118166,1,6952,118166,50,6952,118166,40,6952,118237,0,6952,125682,3,7762,127657,4,8078,130003,1,8453,130003,50,8453,130003,40,8453,130074,0,8453,299459,3,12357,300052,4,14305,300621,1,16254,300621,50,16257,300621,40,16257,300692,0,16257,412145,3,18809,412592,4,20084,412948,5,21358,412949,1,21358,412949,50,21361,412949,40,21361,413020,0,21361,478208,3,22868,478541,4,23612,479038,5,24362,479039,1,24362,479039,50,24364,479039,40,24364,479110,0,24364,487774,3,25133,488929,4,25491,489722,5,25865,489723,1,25865,489723,50,25865,489723,40,25865,489794,0,25865,542811,3,27070,543048,4,27666,543361,5,28267,543362,1,28267,543362,50,28268,543362,40,28268,543433,0,28269,576672,3,29020,576906,4,29395,577187,1,29770,577187,50,29771,577187,40,29771,577187,40,29771,577252,0,29771,577466,50,29771,577466,30,29771,577466,40,29771,577531,0,29771,577664,50,29772,577729,0,29779,577916,50,29781,577981,0,29782,578177,50,29786,578242,0,29790,578440,50,29792,578440,30,29792,578440,40,29792,578505,0,29793,578684,50,29793,578684,30,29793,578684,40,29793,578749,0,29798,578894,50,29799,578894,30,29799,578894,40,29799,578959,0,29799)
%
%
% START OF PROOF
% 578895 [] equal(X,X).
% 578896 [] equal(multiply(identity,X),X).
% 578897 [] equal(multiply(inverse(X),X),identity).
% 578898 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 578899 [] -equal(multiply(sk_c10,X),sk_c9) | -equal(multiply(Y,sk_c10),X) | -equal(inverse(Y),sk_c10).
% 578920 [] equal(multiply(sk_c7,sk_c10),sk_c6) | equal(inverse(sk_c1),sk_c10).
% 578921 [] equal(inverse(sk_c1),sk_c10) | equal(inverse(sk_c6),sk_c10).
% 578922 [] equal(inverse(sk_c1),sk_c10) | equal(inverse(sk_c7),sk_c6).
% 578923 [] equal(multiply(sk_c5,sk_c8),sk_c9) | equal(inverse(sk_c1),sk_c10).
% 578924 [] equal(inverse(sk_c1),sk_c10) | equal(inverse(sk_c5),sk_c9).
% 578926 [] equal(inverse(sk_c1),sk_c10) | equal(inverse(sk_c9),sk_c8).
% 578927 [] equal(inverse(sk_c1),sk_c10) | equal(inverse(sk_c4),sk_c10).
% 578928 [] equal(multiply(sk_c4,sk_c10),sk_c9) | equal(inverse(sk_c1),sk_c10).
% 578929 [] equal(multiply(sk_c9,sk_c10),sk_c8) | equal(inverse(sk_c1),sk_c10).
% 578930 [] equal(multiply(sk_c1,sk_c10),sk_c2) | equal(multiply(sk_c7,sk_c10),sk_c6).
% 578931 [] equal(multiply(sk_c1,sk_c10),sk_c2) | equal(inverse(sk_c6),sk_c10).
% 578932 [] equal(multiply(sk_c1,sk_c10),sk_c2) | equal(inverse(sk_c7),sk_c6).
% 578933 [] equal(multiply(sk_c1,sk_c10),sk_c2) | equal(multiply(sk_c5,sk_c8),sk_c9).
% 578934 [] equal(multiply(sk_c1,sk_c10),sk_c2) | equal(inverse(sk_c5),sk_c9).
% 578936 [] equal(multiply(sk_c1,sk_c10),sk_c2) | equal(inverse(sk_c9),sk_c8).
% 578937 [] equal(multiply(sk_c1,sk_c10),sk_c2) | equal(inverse(sk_c4),sk_c10).
% 578938 [] equal(multiply(sk_c1,sk_c10),sk_c2) | equal(multiply(sk_c4,sk_c10),sk_c9).
% 578939 [] equal(multiply(sk_c1,sk_c10),sk_c2) | equal(multiply(sk_c9,sk_c10),sk_c8).
% 578940 [?] ?
% 578941 [?] ?
% 578942 [?] ?
% 578943 [?] ?
% 578944 [?] ?
% 578946 [?] ?
% 578947 [?] ?
% 578948 [?] ?
% 578949 [?] ?
% 579087 [hyper:578899,578931,binarycut:578941,binarycut:578921] equal(inverse(sk_c6),sk_c10).
% 579097 [para:579087.1.1,578897.1.1.1] equal(multiply(sk_c10,sk_c6),identity).
% 579103 [hyper:578899,578932,binarycut:578942,binarycut:578922] equal(inverse(sk_c7),sk_c6).
% 579115 [para:579103.1.1,578897.1.1.1] equal(multiply(sk_c6,sk_c7),identity).
% 579118 [hyper:578899,578934,binarycut:578944,binarycut:578924] equal(inverse(sk_c5),sk_c9).
% 579134 [hyper:578899,578936,binarycut:578946,binarycut:578926] equal(inverse(sk_c9),sk_c8).
% 579138 [hyper:578899,578937,binarycut:578947,binarycut:578927] equal(inverse(sk_c4),sk_c10).
% 579158 [hyper:578899,578930,578920,binarycut:578940] equal(multiply(sk_c7,sk_c10),sk_c6).
% 579169 [para:579138.1.1,578897.1.1.1] equal(multiply(sk_c10,sk_c4),identity).
% 579183 [hyper:578899,578933,578923,binarycut:578943] equal(multiply(sk_c5,sk_c8),sk_c9).
% 579203 [hyper:578899,578938,578928,binarycut:578948] equal(multiply(sk_c4,sk_c10),sk_c9).
% 579225 [hyper:578899,578939,578929,binarycut:578949] equal(multiply(sk_c9,sk_c10),sk_c8).
% 579230 [para:578897.1.1,578898.1.1.1,demod:578896] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 579231 [para:579097.1.1,578898.1.1.1,demod:578896] equal(X,multiply(sk_c10,multiply(sk_c6,X))).
% 579232 [para:579115.1.1,578898.1.1.1,demod:578896] equal(X,multiply(sk_c6,multiply(sk_c7,X))).
% 579235 [para:579158.1.1,578898.1.1.1] equal(multiply(sk_c6,X),multiply(sk_c7,multiply(sk_c10,X))).
% 579243 [para:579115.1.1,579231.1.2.2] equal(sk_c7,multiply(sk_c10,identity)).
% 579244 [para:579243.1.2,578898.1.1.1,demod:578896] equal(multiply(sk_c7,X),multiply(sk_c10,X)).
% 579247 [para:579158.1.1,579232.1.2.2] equal(sk_c10,multiply(sk_c6,sk_c6)).
% 579251 [para:579097.1.1,579230.1.2.2] equal(sk_c6,multiply(inverse(sk_c10),identity)).
% 579254 [para:579169.1.1,579230.1.2.2,demod:579251] equal(sk_c4,sk_c6).
% 579255 [para:579183.1.1,579230.1.2.2,demod:579118] equal(sk_c8,multiply(sk_c9,sk_c9)).
% 579257 [para:579203.1.1,579230.1.2.2,demod:579244,579138] equal(sk_c10,multiply(sk_c7,sk_c9)).
% 579258 [para:579225.1.1,579230.1.2.2,demod:579134] equal(sk_c10,multiply(sk_c8,sk_c8)).
% 579263 [para:579254.1.2,579247.1.2.1] equal(sk_c10,multiply(sk_c4,sk_c6)).
% 579268 [para:579255.1.2,579230.1.2.2,demod:579258,579134] equal(sk_c9,sk_c10).
% 579270 [para:579268.1.2,579158.1.1.2,demod:579257] equal(sk_c10,sk_c6).
% 579278 [para:579270.1.1,579097.1.1.1,demod:579247] equal(sk_c10,identity).
% 579279 [para:579270.1.1,579158.1.1.2] equal(multiply(sk_c7,sk_c6),sk_c6).
% 579281 [para:579270.1.1,579203.1.1.2,demod:579263] equal(sk_c10,sk_c9).
% 579297 [para:579278.1.1,579281.1.1] equal(identity,sk_c9).
% 579316 [hyper:578899,579235,demod:579087,579097,579279,579158,579244,cut:579297,cut:578895] 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 31
% clause depth limited to 3
% seconds given: 2
%
%
% Split component 6 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c8,sk_c10),sk_c9) | -equal(multiply(sk_c10,X),sk_c9) | -equal(multiply(Y,sk_c10),X) | -equal(inverse(Y),sk_c10) | -equal(multiply(Z,sk_c8),sk_c10) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c9,sk_c10),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(inverse(sk_c9),sk_c8) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c9) | -equal(multiply(V,sk_c8),sk_c9) | -equal(inverse(W),X1) | -equal(inverse(X1),sk_c10) | -equal(multiply(W,sk_c10),X1).
% Split part used next: -equal(multiply(sk_c8,sk_c10),sk_c9).
% 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 31
% clause depth limited to 3
% seconds given: 2
%
%
% 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 31
% clause depth limited to 4
% seconds given: 2
%
%
% 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 31
% clause depth limited to 5
% seconds given: 2
%
%
% 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 31
% clause depth limited to 6
% seconds given: 2
%
%
% 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 31
% clause depth limited to 7
% seconds given: 2
%
%
% 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 31
% clause depth limited to 8
% seconds given: 2
%
%
% 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 31
% clause depth limited to 9
% seconds given: 2
%
%
% 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(65,40,0,136,0,0,5462,50,76,5533,0,77,20977,50,372,21048,0,372,38077,50,746,38148,0,746,58311,50,1246,58311,40,1246,58382,0,1247,62398,3,1550,63642,4,1699,63750,5,1848,63750,1,1848,63750,50,1848,63750,40,1848,63821,0,1848,66290,3,2150,66380,4,2301,66415,5,2449,66415,1,2449,66415,50,2449,66415,40,2449,66486,0,2449,96313,3,3950,97200,4,4700,97896,1,5450,97896,50,5451,97896,40,5451,97967,0,5451,116817,3,6203,117608,4,6577,118166,1,6952,118166,50,6952,118166,40,6952,118237,0,6952,125682,3,7762,127657,4,8078,130003,1,8453,130003,50,8453,130003,40,8453,130074,0,8453,299459,3,12357,300052,4,14305,300621,1,16254,300621,50,16257,300621,40,16257,300692,0,16257,412145,3,18809,412592,4,20084,412948,5,21358,412949,1,21358,412949,50,21361,412949,40,21361,413020,0,21361,478208,3,22868,478541,4,23612,479038,5,24362,479039,1,24362,479039,50,24364,479039,40,24364,479110,0,24364,487774,3,25133,488929,4,25491,489722,5,25865,489723,1,25865,489723,50,25865,489723,40,25865,489794,0,25865,542811,3,27070,543048,4,27666,543361,5,28267,543362,1,28267,543362,50,28268,543362,40,28268,543433,0,28269,576672,3,29020,576906,4,29395,577187,1,29770,577187,50,29771,577187,40,29771,577187,40,29771,577252,0,29771,577466,50,29771,577466,30,29771,577466,40,29771,577531,0,29771,577664,50,29772,577729,0,29779,577916,50,29781,577981,0,29782,578177,50,29786,578242,0,29790,578440,50,29792,578440,30,29792,578440,40,29792,578505,0,29793,578684,50,29793,578684,30,29793,578684,40,29793,578749,0,29798,578894,50,29799,578894,30,29799,578894,40,29799,578959,0,29799,579315,50,29800,579315,30,29800,579315,40,29800,579380,0,29804,579568,50,29806,579633,0,29806,579875,50,29810,579940,0,29814,580190,50,29820,580255,0,29820,580513,50,29828,580578,0,29832,580842,50,29843,580907,0,29843,581179,50,29864,581244,0,29868,581524,50,29904,581524,40,29904,581589,0,29904)
%
%
% START OF PROOF
% 581391 [?] ?
% 581526 [] equal(multiply(identity,X),X).
% 581527 [] equal(multiply(inverse(X),X),identity).
% 581528 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 581529 [] -equal(multiply(sk_c8,sk_c10),sk_c9).
% 581583 [?] ?
% 581584 [?] ?
% 581586 [?] ?
% 581589 [?] ?
% 581680 [input:581584,cut:581529] equal(inverse(sk_c5),sk_c9).
% 581681 [para:581680.1.1,581527.1.1.1] equal(multiply(sk_c9,sk_c5),identity).
% 581682 [input:581586,cut:581529] equal(inverse(sk_c9),sk_c8).
% 581683 [para:581682.1.1,581527.1.1.1] equal(multiply(sk_c8,sk_c9),identity).
% 581706 [input:581583,cut:581529] equal(multiply(sk_c5,sk_c8),sk_c9).
% 581709 [input:581589,cut:581529] equal(multiply(sk_c9,sk_c10),sk_c8).
% 581750 [para:581681.1.1,581528.1.1.1,demod:581526] equal(X,multiply(sk_c9,multiply(sk_c5,X))).
% 581751 [para:581683.1.1,581528.1.1.1,demod:581526] equal(X,multiply(sk_c8,multiply(sk_c9,X))).
% 581803 [para:581706.1.1,581750.1.2.2] equal(sk_c8,multiply(sk_c9,sk_c9)).
% 581811 [para:581709.1.1,581751.1.2.2] equal(sk_c10,multiply(sk_c8,sk_c8)).
% 581813 [para:581803.1.2,581751.1.2.2,demod:581811] equal(sk_c9,sk_c10).
% 581814 [para:581813.1.2,581529.1.1.2,demod:581683,cut:581391] 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 7 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c8,sk_c10),sk_c9) | -equal(multiply(sk_c10,X),sk_c9) | -equal(multiply(Y,sk_c10),X) | -equal(inverse(Y),sk_c10) | -equal(multiply(Z,sk_c8),sk_c10) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c9,sk_c10),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(inverse(sk_c9),sk_c8) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c9) | -equal(multiply(V,sk_c8),sk_c9) | -equal(inverse(W),X1) | -equal(inverse(X1),sk_c10) | -equal(multiply(W,sk_c10),X1).
% Split part used next: -equal(multiply(sk_c9,sk_c10),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 31
% clause depth limited to 3
% seconds given: 2
%
%
% 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 31
% clause depth limited to 4
% seconds given: 2
%
%
% 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 31
% clause depth limited to 5
% seconds given: 2
%
%
% 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 31
% clause depth limited to 6
% seconds given: 2
%
%
% 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 31
% clause depth limited to 7
% seconds given: 2
%
%
% 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 31
% clause depth limited to 8
% seconds given: 2
%
%
% 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 31
% clause depth limited to 9
% seconds given: 2
%
%
% 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 31
% clause depth limited to 10
% seconds given: 2
%
%
% 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(65,40,0,136,0,0,5462,50,76,5533,0,77,20977,50,372,21048,0,372,38077,50,746,38148,0,746,58311,50,1246,58311,40,1246,58382,0,1247,62398,3,1550,63642,4,1699,63750,5,1848,63750,1,1848,63750,50,1848,63750,40,1848,63821,0,1848,66290,3,2150,66380,4,2301,66415,5,2449,66415,1,2449,66415,50,2449,66415,40,2449,66486,0,2449,96313,3,3950,97200,4,4700,97896,1,5450,97896,50,5451,97896,40,5451,97967,0,5451,116817,3,6203,117608,4,6577,118166,1,6952,118166,50,6952,118166,40,6952,118237,0,6952,125682,3,7762,127657,4,8078,130003,1,8453,130003,50,8453,130003,40,8453,130074,0,8453,299459,3,12357,300052,4,14305,300621,1,16254,300621,50,16257,300621,40,16257,300692,0,16257,412145,3,18809,412592,4,20084,412948,5,21358,412949,1,21358,412949,50,21361,412949,40,21361,413020,0,21361,478208,3,22868,478541,4,23612,479038,5,24362,479039,1,24362,479039,50,24364,479039,40,24364,479110,0,24364,487774,3,25133,488929,4,25491,489722,5,25865,489723,1,25865,489723,50,25865,489723,40,25865,489794,0,25865,542811,3,27070,543048,4,27666,543361,5,28267,543362,1,28267,543362,50,28268,543362,40,28268,543433,0,28269,576672,3,29020,576906,4,29395,577187,1,29770,577187,50,29771,577187,40,29771,577187,40,29771,577252,0,29771,577466,50,29771,577466,30,29771,577466,40,29771,577531,0,29771,577664,50,29772,577729,0,29779,577916,50,29781,577981,0,29782,578177,50,29786,578242,0,29790,578440,50,29792,578440,30,29792,578440,40,29792,578505,0,29793,578684,50,29793,578684,30,29793,578684,40,29793,578749,0,29798,578894,50,29799,578894,30,29799,578894,40,29799,578959,0,29799,579315,50,29800,579315,30,29800,579315,40,29800,579380,0,29804,579568,50,29806,579633,0,29806,579875,50,29810,579940,0,29814,580190,50,29820,580255,0,29820,580513,50,29828,580578,0,29832,580842,50,29843,580907,0,29843,581179,50,29864,581244,0,29868,581524,50,29904,581524,40,29904,581589,0,29904,581813,50,29905,581813,30,29905,581813,40,29905,581878,0,29910,582019,50,29911,582084,0,29911,582278,50,29914,582343,0,29919,582545,50,29923,582610,0,29923,582832,50,29931,582897,0,29936,583125,50,29947,583190,0,29947,583426,50,29965,583491,0,29970,583736,50,30004,583801,0,30004,584056,50,30074,584056,40,30074,584121,0,30074)
%
%
% START OF PROOF
% 583876 [?] ?
% 584058 [] equal(multiply(identity,X),X).
% 584059 [] equal(multiply(inverse(X),X),identity).
% 584060 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 584061 [] -equal(multiply(sk_c9,sk_c10),sk_c8).
% 584071 [?] ?
% 584081 [?] ?
% 584121 [?] ?
% 584160 [input:584071,cut:584061] equal(inverse(sk_c3),sk_c8).
% 584161 [para:584160.1.1,584059.1.1.1] equal(multiply(sk_c8,sk_c3),identity).
% 584198 [input:584081,cut:584061] equal(multiply(sk_c3,sk_c8),sk_c10).
% 584241 [input:584121,cut:584061] equal(multiply(sk_c8,sk_c10),sk_c9).
% 584247 [para:584161.1.1,584060.1.1.1,demod:584058] equal(X,multiply(sk_c8,multiply(sk_c3,X))).
% 584328 [para:584198.1.1,584247.1.2.2] equal(sk_c8,multiply(sk_c8,sk_c10)).
% 584338 [para:584328.1.2,584241.1.1] equal(sk_c8,sk_c9).
% 584340 [para:584338.1.1,584061.1.2,cut:583876] 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 8 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c8,sk_c10),sk_c9) | -equal(multiply(sk_c10,X),sk_c9) | -equal(multiply(Y,sk_c10),X) | -equal(inverse(Y),sk_c10) | -equal(multiply(Z,sk_c8),sk_c10) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c9,sk_c10),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(inverse(sk_c9),sk_c8) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c9) | -equal(multiply(V,sk_c8),sk_c9) | -equal(inverse(W),X1) | -equal(inverse(X1),sk_c10) | -equal(multiply(W,sk_c10),X1).
% Split part used next: -equal(inverse(sk_c9),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 31
% clause depth limited to 3
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(65,40,0,136,0,0,5462,50,76,5533,0,77,20977,50,372,21048,0,372,38077,50,746,38148,0,746,58311,50,1246,58311,40,1246,58382,0,1247,62398,3,1550,63642,4,1699,63750,5,1848,63750,1,1848,63750,50,1848,63750,40,1848,63821,0,1848,66290,3,2150,66380,4,2301,66415,5,2449,66415,1,2449,66415,50,2449,66415,40,2449,66486,0,2449,96313,3,3950,97200,4,4700,97896,1,5450,97896,50,5451,97896,40,5451,97967,0,5451,116817,3,6203,117608,4,6577,118166,1,6952,118166,50,6952,118166,40,6952,118237,0,6952,125682,3,7762,127657,4,8078,130003,1,8453,130003,50,8453,130003,40,8453,130074,0,8453,299459,3,12357,300052,4,14305,300621,1,16254,300621,50,16257,300621,40,16257,300692,0,16257,412145,3,18809,412592,4,20084,412948,5,21358,412949,1,21358,412949,50,21361,412949,40,21361,413020,0,21361,478208,3,22868,478541,4,23612,479038,5,24362,479039,1,24362,479039,50,24364,479039,40,24364,479110,0,24364,487774,3,25133,488929,4,25491,489722,5,25865,489723,1,25865,489723,50,25865,489723,40,25865,489794,0,25865,542811,3,27070,543048,4,27666,543361,5,28267,543362,1,28267,543362,50,28268,543362,40,28268,543433,0,28269,576672,3,29020,576906,4,29395,577187,1,29770,577187,50,29771,577187,40,29771,577187,40,29771,577252,0,29771,577466,50,29771,577466,30,29771,577466,40,29771,577531,0,29771,577664,50,29772,577729,0,29779,577916,50,29781,577981,0,29782,578177,50,29786,578242,0,29790,578440,50,29792,578440,30,29792,578440,40,29792,578505,0,29793,578684,50,29793,578684,30,29793,578684,40,29793,578749,0,29798,578894,50,29799,578894,30,29799,578894,40,29799,578959,0,29799,579315,50,29800,579315,30,29800,579315,40,29800,579380,0,29804,579568,50,29806,579633,0,29806,579875,50,29810,579940,0,29814,580190,50,29820,580255,0,29820,580513,50,29828,580578,0,29832,580842,50,29843,580907,0,29843,581179,50,29864,581244,0,29868,581524,50,29904,581524,40,29904,581589,0,29904,581813,50,29905,581813,30,29905,581813,40,29905,581878,0,29910,582019,50,29911,582084,0,29911,582278,50,29914,582343,0,29919,582545,50,29923,582610,0,29923,582832,50,29931,582897,0,29936,583125,50,29947,583190,0,29947,583426,50,29965,583491,0,29970,583736,50,30004,583801,0,30004,584056,50,30074,584056,40,30074,584121,0,30074,584339,50,30075,584339,30,30075,584339,40,30075,584404,0,30075)
%
%
% START OF PROOF
% 584341 [] equal(multiply(identity,X),X).
% 584342 [] equal(multiply(inverse(X),X),identity).
% 584343 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 584344 [] -equal(inverse(sk_c9),sk_c8).
% 584351 [?] ?
% 584361 [?] ?
% 584371 [?] ?
% 584381 [?] ?
% 584391 [?] ?
% 584401 [?] ?
% 584409 [input:584351,cut:584344] equal(inverse(sk_c3),sk_c8).
% 584410 [para:584409.1.1,584342.1.1.1] equal(multiply(sk_c8,sk_c3),identity).
% 584416 [input:584371,cut:584344] equal(inverse(sk_c1),sk_c10).
% 584417 [para:584416.1.1,584342.1.1.1] equal(multiply(sk_c10,sk_c1),identity).
% 584426 [input:584361,cut:584344] equal(multiply(sk_c3,sk_c8),sk_c10).
% 584438 [input:584381,cut:584344] equal(multiply(sk_c1,sk_c10),sk_c2).
% 584445 [input:584391,cut:584344] equal(multiply(sk_c10,sk_c2),sk_c9).
% 584451 [input:584401,cut:584344] equal(multiply(sk_c8,sk_c10),sk_c9).
% 584467 [para:584342.1.1,584343.1.1.1,demod:584341] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 584468 [para:584410.1.1,584343.1.1.1,demod:584341] equal(X,multiply(sk_c8,multiply(sk_c3,X))).
% 584469 [para:584417.1.1,584343.1.1.1,demod:584341] equal(X,multiply(sk_c10,multiply(sk_c1,X))).
% 584470 [para:584426.1.1,584343.1.1.1] equal(multiply(sk_c10,X),multiply(sk_c3,multiply(sk_c8,X))).
% 584474 [para:584426.1.1,584468.1.2.2] equal(sk_c8,multiply(sk_c8,sk_c10)).
% 584475 [para:584474.1.2,584451.1.1] equal(sk_c8,sk_c9).
% 584478 [para:584475.1.1,584426.1.1.2] equal(multiply(sk_c3,sk_c9),sk_c10).
% 584479 [para:584475.1.1,584451.1.1.1] equal(multiply(sk_c9,sk_c10),sk_c9).
% 584494 [para:584479.1.1,584467.1.2.2,demod:584342] equal(sk_c10,identity).
% 584495 [para:584494.1.1,584417.1.1.1,demod:584341] equal(sk_c1,identity).
% 584500 [para:584495.1.1,584417.1.1.2] equal(multiply(sk_c10,identity),identity).
% 584501 [para:584495.1.1,584438.1.1.1,demod:584341] equal(sk_c10,sk_c2).
% 584505 [para:584495.1.1,584469.1.2.2.1,demod:584341] equal(X,multiply(sk_c10,X)).
% 584506 [para:584410.1.1,584470.1.2.2,demod:584505] equal(sk_c3,multiply(sk_c3,identity)).
% 584511 [para:584501.1.1,584494.1.1] equal(sk_c2,identity).
% 584514 [para:584511.1.1,584445.1.1.2,demod:584500] equal(identity,sk_c9).
% 584518 [para:584514.1.2,584478.1.1.2,demod:584506] equal(sk_c3,sk_c10).
% 584519 [para:584514.1.2,584479.1.1.1,demod:584341] equal(sk_c10,sk_c9).
% 584530 [para:584519.1.1,584518.1.2] equal(sk_c3,sk_c9).
% 584535 [para:584530.1.1,584409.1.1.1,cut:584344] 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 31
% clause depth limited to 3
% seconds given: 2
%
%
% Split component 9 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c8,sk_c10),sk_c9) | -equal(multiply(sk_c10,X),sk_c9) | -equal(multiply(Y,sk_c10),X) | -equal(inverse(Y),sk_c10) | -equal(multiply(Z,sk_c8),sk_c10) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c9,sk_c10),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(inverse(sk_c9),sk_c8) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c9) | -equal(multiply(V,sk_c8),sk_c9) | -equal(inverse(W),X1) | -equal(inverse(X1),sk_c10) | -equal(multiply(W,sk_c10),X1).
% Split part used next: -equal(multiply(sk_c10,sk_c8),sk_c9).
% 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 31
% clause depth limited to 3
% seconds given: 2
%
%
% 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 31
% clause depth limited to 4
% seconds given: 2
%
%
% 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 31
% clause depth limited to 5
% seconds given: 2
%
%
% 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 31
% clause depth limited to 6
% seconds given: 2
%
%
% 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 31
% clause depth limited to 7
% seconds given: 2
%
%
% 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 31
% clause depth limited to 8
% seconds given: 2
%
%
% 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 31
% clause depth limited to 9
% seconds given: 2
%
%
% 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 31
% clause depth limited to 10
% seconds given: 2
%
%
% 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(65,40,0,136,0,0,5462,50,76,5533,0,77,20977,50,372,21048,0,372,38077,50,746,38148,0,746,58311,50,1246,58311,40,1246,58382,0,1247,62398,3,1550,63642,4,1699,63750,5,1848,63750,1,1848,63750,50,1848,63750,40,1848,63821,0,1848,66290,3,2150,66380,4,2301,66415,5,2449,66415,1,2449,66415,50,2449,66415,40,2449,66486,0,2449,96313,3,3950,97200,4,4700,97896,1,5450,97896,50,5451,97896,40,5451,97967,0,5451,116817,3,6203,117608,4,6577,118166,1,6952,118166,50,6952,118166,40,6952,118237,0,6952,125682,3,7762,127657,4,8078,130003,1,8453,130003,50,8453,130003,40,8453,130074,0,8453,299459,3,12357,300052,4,14305,300621,1,16254,300621,50,16257,300621,40,16257,300692,0,16257,412145,3,18809,412592,4,20084,412948,5,21358,412949,1,21358,412949,50,21361,412949,40,21361,413020,0,21361,478208,3,22868,478541,4,23612,479038,5,24362,479039,1,24362,479039,50,24364,479039,40,24364,479110,0,24364,487774,3,25133,488929,4,25491,489722,5,25865,489723,1,25865,489723,50,25865,489723,40,25865,489794,0,25865,542811,3,27070,543048,4,27666,543361,5,28267,543362,1,28267,543362,50,28268,543362,40,28268,543433,0,28269,576672,3,29020,576906,4,29395,577187,1,29770,577187,50,29771,577187,40,29771,577187,40,29771,577252,0,29771,577466,50,29771,577466,30,29771,577466,40,29771,577531,0,29771,577664,50,29772,577729,0,29779,577916,50,29781,577981,0,29782,578177,50,29786,578242,0,29790,578440,50,29792,578440,30,29792,578440,40,29792,578505,0,29793,578684,50,29793,578684,30,29793,578684,40,29793,578749,0,29798,578894,50,29799,578894,30,29799,578894,40,29799,578959,0,29799,579315,50,29800,579315,30,29800,579315,40,29800,579380,0,29804,579568,50,29806,579633,0,29806,579875,50,29810,579940,0,29814,580190,50,29820,580255,0,29820,580513,50,29828,580578,0,29832,580842,50,29843,580907,0,29843,581179,50,29864,581244,0,29868,581524,50,29904,581524,40,29904,581589,0,29904,581813,50,29905,581813,30,29905,581813,40,29905,581878,0,29910,582019,50,29911,582084,0,29911,582278,50,29914,582343,0,29919,582545,50,29923,582610,0,29923,582832,50,29931,582897,0,29936,583125,50,29947,583190,0,29947,583426,50,29965,583491,0,29970,583736,50,30004,583801,0,30004,584056,50,30074,584056,40,30074,584121,0,30074,584339,50,30075,584339,30,30075,584339,40,30075,584404,0,30075,584534,50,30075,584534,30,30075,584534,40,30075,584599,0,30080,584740,50,30081,584805,0,30081,584999,50,30084,585064,0,30088,585266,50,30092,585331,0,30092,585553,50,30100,585618,0,30104,585846,50,30115,585911,0,30115,586147,50,30133,586212,0,30138,586457,50,30172,586522,0,30172,586777,50,30242,586777,40,30242,586842,0,30242)
%
%
% START OF PROOF
% 586725 [?] ?
% 586779 [] equal(multiply(identity,X),X).
% 586780 [] equal(multiply(inverse(X),X),identity).
% 586781 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 586782 [] -equal(multiply(sk_c10,sk_c8),sk_c9).
% 586808 [?] ?
% 586818 [?] ?
% 586828 [?] ?
% 586896 [input:586808,cut:586782] equal(inverse(sk_c1),sk_c10).
% 586897 [para:586896.1.1,586780.1.1.1] equal(multiply(sk_c10,sk_c1),identity).
% 586939 [input:586818,cut:586782] equal(multiply(sk_c1,sk_c10),sk_c2).
% 586951 [input:586828,cut:586782] equal(multiply(sk_c10,sk_c2),sk_c9).
% 586977 [para:586897.1.1,586781.1.1.1,demod:586779] equal(X,multiply(sk_c10,multiply(sk_c1,X))).
% 587086 [para:586939.1.1,586977.1.2.2] equal(sk_c10,multiply(sk_c10,sk_c2)).
% 587094 [para:587086.1.2,586951.1.1] equal(sk_c10,sk_c9).
% 587098 [para:587094.1.1,586782.1.1.1,cut:586725] 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: 29914
% derived clauses: 3528297
% kept clauses: 365065
% kept size sum: 647181
% kept mid-nuclei: 44559
% kept new demods: 5515
% forw unit-subs: 1099606
% forw double-subs: 1662739
% forw overdouble-subs: 169620
% backward subs: 13733
% fast unit cutoff: 16282
% full unit cutoff: 0
% dbl unit cutoff: 22210
% real runtime : 304.64
% process. runtime: 302.43
% specific non-discr-tree subsumption statistics:
% tried: 89737241
% length fails: 7332660
% strength fails: 28568747
% predlist fails: 5885414
% aux str. fails: 8324280
% by-lit fails: 25168014
% full subs tried: 2436256
% full subs fail: 2328503
%
% ; 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/GRP366-1+eq_r.in")
%
%------------------------------------------------------------------------------