%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP301-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 : art02.cs.miami.edu
% Model : i686 unknown
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 1000MB
% OS : Linux 2.4.22-21mdk-i686-up-4GB
% CPULimit : 600s
% Result : Unsatisfiable 299.5s
% Output : Assurance 299.5s
% 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/GRP301-1+eq_r.in
% Using automatic strategy selection.
% Time limit in seconds: 600
%
% prove-all-passes started
%
% detected problem class: peq
%
% strategies selected:
% (hyper 30 #f 3 21)
% (binary-unit 12 #f)
% (binary-unit-uniteq 12 #f)
% (binary-posweight-kb-big-order 60 #f 3 21)
% (binary-posweight-lex-big-order 30 #f 3 21)
% (binary 30 #t)
% (binary-posweight-kb-big-order 156 #f)
% (binary-posweight-lex-big-order 102 #f)
% (binary-posweight-firstpref-order 60 #f)
% (binary-order 30 #f)
% (binary-posweight-kb-small-order 48 #f)
% (binary-posweight-lex-small-order 30 #f)
%
%
% SOS clause
% -equal(multiply(sk_c7,sk_c6),sk_c5) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(inverse(sk_c7),sk_c5) | -equal(multiply(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(inverse(Z),sk_c7) | -equal(multiply(Z,sk_c6),sk_c7) | -equal(inverse(U),sk_c6) | -equal(multiply(U,sk_c5),sk_c6).
% was split for some strategies as:
% -equal(inverse(U),sk_c6) | -equal(multiply(U,sk_c5),sk_c6).
% -equal(inverse(Z),sk_c7) | -equal(multiply(Z,sk_c6),sk_c7).
% -equal(multiply(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6).
% -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7).
% -equal(multiply(sk_c7,sk_c6),sk_c5).
% -equal(inverse(sk_c7),sk_c5).
% -equal(multiply(sk_c6,sk_c7),sk_c5).
%
% Starting a split proof attempt with 7 components.
%
% Split component 1 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c6),sk_c5) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(inverse(sk_c7),sk_c5) | -equal(multiply(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(inverse(Z),sk_c7) | -equal(multiply(Z,sk_c6),sk_c7) | -equal(inverse(U),sk_c6) | -equal(multiply(U,sk_c5),sk_c6).
% Split part used next: -equal(inverse(U),sk_c6) | -equal(multiply(U,sk_c5),sk_c6).
% END OF PROOFPART
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,1,75,0,1,580,50,4,620,0,4,1140,50,8,1180,0,8,1711,50,14,1751,0,14,2289,50,20,2329,0,20,2874,50,27,2914,0,27,3467,50,41,3507,0,41,4069,50,69,4109,0,69,4681,50,130,4721,0,130,5304,50,264,5344,0,264,5939,50,477,5979,0,477,6587,50,897,6587,40,897,6627,0,897,16947,3,1198,17681,4,1348,18406,1,1498,18406,50,1498,18406,40,1498,18446,0,1498,18617,3,1805,18626,4,1959,18633,5,2099,18633,1,2099,18633,50,2099,18633,40,2099,18673,0,2099,41991,3,3601,43309,4,4350,44560,5,5100,44561,1,5100,44561,50,5101,44561,40,5101,44601,0,5101,59627,3,5852,60579,4,6227,61434,5,6602,61435,1,6602,61435,50,6602,61435,40,6602,61475,0,6602,71161,3,7355,72366,4,7728,73537,1,8103,73537,50,8103,73537,40,8103,73577,0,8103,131505,3,12006,132703,4,13954,133802,1,15904,133802,50,15906,133802,40,15906,133842,0,15906,177536,3,18457,178746,4,19732,179339,5,21007,179340,1,21007,179340,50,21009,179340,40,21009,179380,0,21009,215630,3,22511,216496,4,23260,217334,1,24010,217334,50,24011,217334,40,24011,217374,0,24012,226576,3,24765,227737,4,25140,227903,5,25513,227903,1,25513,227903,50,25513,227903,40,25513,227943,0,25513,255888,3,26714,256804,4,27314,257210,5,27914,257211,1,27914,257211,50,27915,257211,40,27915,257251,0,27915,277334,3,28666,278078,4,29041,278432,1,29416,278432,50,29416,278432,40,29416,278432,40,29416,278467,0,29416)
%
%
% START OF PROOF
% 278434 [] equal(multiply(identity,X),X).
% 278435 [] equal(multiply(inverse(X),X),identity).
% 278436 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 278437 [] -equal(multiply(X,sk_c5),sk_c6) | -equal(inverse(X),sk_c6).
% 278438 [?] ?
% 278439 [] equal(inverse(sk_c2),sk_c6) | equal(inverse(sk_c4),sk_c6).
% 278443 [] equal(multiply(sk_c2,sk_c6),sk_c5) | equal(multiply(sk_c4,sk_c5),sk_c6).
% 278444 [] equal(multiply(sk_c2,sk_c6),sk_c5) | equal(inverse(sk_c4),sk_c6).
% 278448 [?] ?
% 278449 [] equal(inverse(sk_c7),sk_c5) | equal(inverse(sk_c4),sk_c6).
% 278453 [?] ?
% 278454 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c4),sk_c6).
% 278458 [] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(multiply(sk_c4,sk_c5),sk_c6).
% 278459 [] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(inverse(sk_c4),sk_c6).
% 278463 [] equal(multiply(sk_c7,sk_c6),sk_c5) | equal(multiply(sk_c4,sk_c5),sk_c6).
% 278464 [] equal(multiply(sk_c7,sk_c6),sk_c5) | equal(inverse(sk_c4),sk_c6).
% 278471 [hyper:278437,278439,binarycut:278438] equal(inverse(sk_c2),sk_c6).
% 278473 [para:278471.1.1,278435.1.1.1] equal(multiply(sk_c6,sk_c2),identity).
% 278480 [hyper:278437,278449,binarycut:278448] equal(inverse(sk_c7),sk_c5).
% 278481 [para:278480.1.1,278435.1.1.1] equal(multiply(sk_c5,sk_c7),identity).
% 278484 [hyper:278437,278454,binarycut:278453] equal(inverse(sk_c1),sk_c7).
% 278485 [para:278484.1.1,278435.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 278488 [hyper:278437,278444,278443] equal(multiply(sk_c2,sk_c6),sk_c5).
% 278494 [hyper:278437,278459,278458] equal(multiply(sk_c1,sk_c7),sk_c6).
% 278501 [hyper:278437,278463,278464] equal(multiply(sk_c7,sk_c6),sk_c5).
% 278502 [para:278435.1.1,278436.1.1.1,demod:278434] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 278503 [para:278473.1.1,278436.1.1.1,demod:278434] equal(X,multiply(sk_c6,multiply(sk_c2,X))).
% 278504 [para:278481.1.1,278436.1.1.1,demod:278434] equal(X,multiply(sk_c5,multiply(sk_c7,X))).
% 278509 [para:278488.1.1,278503.1.2.2] equal(sk_c6,multiply(sk_c6,sk_c5)).
% 278511 [para:278485.1.1,278504.1.2.2] equal(sk_c1,multiply(sk_c5,identity)).
% 278512 [para:278501.1.1,278504.1.2.2] equal(sk_c6,multiply(sk_c5,sk_c5)).
% 278516 [para:278494.1.1,278502.1.2.2,demod:278501,278484] equal(sk_c7,sk_c5).
% 278520 [para:278516.1.1,278481.1.1.2,demod:278512] equal(sk_c6,identity).
% 278525 [para:278520.1.1,278473.1.1.1,demod:278434] equal(sk_c2,identity).
% 278529 [para:278520.1.1,278509.1.2.1,demod:278434] equal(sk_c6,sk_c5).
% 278530 [para:278525.1.1,278471.1.1.1] equal(inverse(identity),sk_c6).
% 278536 [para:278529.1.1,278520.1.1] equal(sk_c5,identity).
% 278538 [para:278536.1.1,278481.1.1.1,demod:278434] equal(sk_c7,identity).
% 278541 [para:278538.1.1,278481.1.1.2,demod:278511] equal(sk_c1,identity).
% 278544 [para:278541.1.1,278494.1.1.1,demod:278434] equal(sk_c7,sk_c6).
% 278546 [para:278516.1.1,278544.1.1] equal(sk_c5,sk_c6).
% 278547 [hyper:278437,278530,demod:278434,cut:278546] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% Split component 2 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c6),sk_c5) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(inverse(sk_c7),sk_c5) | -equal(multiply(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(inverse(Z),sk_c7) | -equal(multiply(Z,sk_c6),sk_c7) | -equal(inverse(U),sk_c6) | -equal(multiply(U,sk_c5),sk_c6).
% Split part used next: -equal(inverse(Z),sk_c7) | -equal(multiply(Z,sk_c6),sk_c7).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 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 21
% clause depth limited to 4
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,1,75,0,1,580,50,4,620,0,4,1140,50,8,1180,0,8,1711,50,14,1751,0,14,2289,50,20,2329,0,20,2874,50,27,2914,0,27,3467,50,41,3507,0,41,4069,50,69,4109,0,69,4681,50,130,4721,0,130,5304,50,264,5344,0,264,5939,50,477,5979,0,477,6587,50,897,6587,40,897,6627,0,897,16947,3,1198,17681,4,1348,18406,1,1498,18406,50,1498,18406,40,1498,18446,0,1498,18617,3,1805,18626,4,1959,18633,5,2099,18633,1,2099,18633,50,2099,18633,40,2099,18673,0,2099,41991,3,3601,43309,4,4350,44560,5,5100,44561,1,5100,44561,50,5101,44561,40,5101,44601,0,5101,59627,3,5852,60579,4,6227,61434,5,6602,61435,1,6602,61435,50,6602,61435,40,6602,61475,0,6602,71161,3,7355,72366,4,7728,73537,1,8103,73537,50,8103,73537,40,8103,73577,0,8103,131505,3,12006,132703,4,13954,133802,1,15904,133802,50,15906,133802,40,15906,133842,0,15906,177536,3,18457,178746,4,19732,179339,5,21007,179340,1,21007,179340,50,21009,179340,40,21009,179380,0,21009,215630,3,22511,216496,4,23260,217334,1,24010,217334,50,24011,217334,40,24011,217374,0,24012,226576,3,24765,227737,4,25140,227903,5,25513,227903,1,25513,227903,50,25513,227903,40,25513,227943,0,25513,255888,3,26714,256804,4,27314,257210,5,27914,257211,1,27914,257211,50,27915,257211,40,27915,257251,0,27915,277334,3,28666,278078,4,29041,278432,1,29416,278432,50,29416,278432,40,29416,278432,40,29416,278467,0,29416,278546,50,29417,278546,30,29417,278546,40,29417,278581,0,29417,278682,50,29417,278717,0,29421)
%
%
% START OF PROOF
% 278684 [] equal(multiply(identity,X),X).
% 278685 [] equal(multiply(inverse(X),X),identity).
% 278686 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 278687 [] -equal(multiply(X,sk_c6),sk_c7) | -equal(inverse(X),sk_c7).
% 278690 [?] ?
% 278691 [] equal(inverse(sk_c2),sk_c6) | equal(inverse(sk_c3),sk_c7).
% 278695 [] equal(multiply(sk_c2,sk_c6),sk_c5) | equal(multiply(sk_c3,sk_c6),sk_c7).
% 278696 [] equal(multiply(sk_c2,sk_c6),sk_c5) | equal(inverse(sk_c3),sk_c7).
% 278700 [?] ?
% 278701 [] equal(inverse(sk_c7),sk_c5) | equal(inverse(sk_c3),sk_c7).
% 278705 [?] ?
% 278706 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c3),sk_c7).
% 278710 [] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(multiply(sk_c3,sk_c6),sk_c7).
% 278711 [] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(inverse(sk_c3),sk_c7).
% 278715 [] equal(multiply(sk_c7,sk_c6),sk_c5) | equal(multiply(sk_c3,sk_c6),sk_c7).
% 278716 [] equal(multiply(sk_c7,sk_c6),sk_c5) | equal(inverse(sk_c3),sk_c7).
% 278721 [hyper:278687,278691,binarycut:278690] equal(inverse(sk_c2),sk_c6).
% 278723 [para:278721.1.1,278685.1.1.1] equal(multiply(sk_c6,sk_c2),identity).
% 278728 [hyper:278687,278701,binarycut:278700] equal(inverse(sk_c7),sk_c5).
% 278729 [para:278728.1.1,278685.1.1.1] equal(multiply(sk_c5,sk_c7),identity).
% 278737 [hyper:278687,278706,binarycut:278705] equal(inverse(sk_c1),sk_c7).
% 278740 [para:278737.1.1,278685.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 278748 [hyper:278687,278695,278696] equal(multiply(sk_c2,sk_c6),sk_c5).
% 278759 [hyper:278687,278710,278711] equal(multiply(sk_c1,sk_c7),sk_c6).
% 278763 [hyper:278687,278715,278716] equal(multiply(sk_c7,sk_c6),sk_c5).
% 278764 [para:278685.1.1,278686.1.1.1,demod:278684] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 278765 [para:278723.1.1,278686.1.1.1,demod:278684] equal(X,multiply(sk_c6,multiply(sk_c2,X))).
% 278766 [para:278729.1.1,278686.1.1.1,demod:278684] equal(X,multiply(sk_c5,multiply(sk_c7,X))).
% 278771 [para:278748.1.1,278765.1.2.2] equal(sk_c6,multiply(sk_c6,sk_c5)).
% 278773 [para:278740.1.1,278766.1.2.2] equal(sk_c1,multiply(sk_c5,identity)).
% 278774 [para:278763.1.1,278766.1.2.2] equal(sk_c6,multiply(sk_c5,sk_c5)).
% 278776 [para:278685.1.1,278764.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 278779 [para:278759.1.1,278764.1.2.2,demod:278763,278737] equal(sk_c7,sk_c5).
% 278780 [para:278686.1.1,278764.1.2.2] equal(X,multiply(inverse(multiply(Y,Z)),multiply(Y,multiply(Z,X)))).
% 278783 [para:278764.1.2,278764.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 278784 [para:278779.1.1,278728.1.1.1] equal(inverse(sk_c5),sk_c5).
% 278785 [para:278779.1.1,278729.1.1.2,demod:278774] equal(sk_c6,identity).
% 278793 [para:278785.1.1,278765.1.2.1,demod:278684] equal(X,multiply(sk_c2,X)).
% 278794 [para:278785.1.1,278771.1.2.1,demod:278684] equal(sk_c6,sk_c5).
% 278801 [para:278794.1.1,278785.1.1] equal(sk_c5,identity).
% 278813 [para:278801.1.1,278774.1.2.2,demod:278773] equal(sk_c6,sk_c1).
% 278814 [para:278813.1.1,278748.1.1.2,demod:278793] equal(sk_c1,sk_c5).
% 278816 [para:278814.1.1,278737.1.1.1,demod:278784] equal(sk_c5,sk_c7).
% 278822 [para:278783.1.2,278685.1.1] equal(multiply(X,inverse(X)),identity).
% 278824 [para:278783.1.2,278776.1.2] equal(X,multiply(X,identity)).
% 278843 [para:278822.1.1,278780.1.2.2.2,demod:278824] equal(inverse(X),multiply(inverse(multiply(Y,X)),Y)).
% 278844 [para:278824.1.2,278776.1.2] equal(X,inverse(inverse(X))).
% 278846 [para:278765.1.2,278843.1.2.1.1,demod:278793] equal(inverse(X),multiply(inverse(X),sk_c6)).
% 278857 [para:278846.1.2,278783.1.2,demod:278844] equal(multiply(X,sk_c6),X).
% 278858 [hyper:278687,278857,demod:278728,cut:278816] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 4
% seconds given: 4
%
%
% Split component 3 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c6),sk_c5) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(inverse(sk_c7),sk_c5) | -equal(multiply(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(inverse(Z),sk_c7) | -equal(multiply(Z,sk_c6),sk_c7) | -equal(inverse(U),sk_c6) | -equal(multiply(U,sk_c5),sk_c6).
% Split part used next: -equal(multiply(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,1,75,0,1,580,50,4,620,0,4,1140,50,8,1180,0,8,1711,50,14,1751,0,14,2289,50,20,2329,0,20,2874,50,27,2914,0,27,3467,50,41,3507,0,41,4069,50,69,4109,0,69,4681,50,130,4721,0,130,5304,50,264,5344,0,264,5939,50,477,5979,0,477,6587,50,897,6587,40,897,6627,0,897,16947,3,1198,17681,4,1348,18406,1,1498,18406,50,1498,18406,40,1498,18446,0,1498,18617,3,1805,18626,4,1959,18633,5,2099,18633,1,2099,18633,50,2099,18633,40,2099,18673,0,2099,41991,3,3601,43309,4,4350,44560,5,5100,44561,1,5100,44561,50,5101,44561,40,5101,44601,0,5101,59627,3,5852,60579,4,6227,61434,5,6602,61435,1,6602,61435,50,6602,61435,40,6602,61475,0,6602,71161,3,7355,72366,4,7728,73537,1,8103,73537,50,8103,73537,40,8103,73577,0,8103,131505,3,12006,132703,4,13954,133802,1,15904,133802,50,15906,133802,40,15906,133842,0,15906,177536,3,18457,178746,4,19732,179339,5,21007,179340,1,21007,179340,50,21009,179340,40,21009,179380,0,21009,215630,3,22511,216496,4,23260,217334,1,24010,217334,50,24011,217334,40,24011,217374,0,24012,226576,3,24765,227737,4,25140,227903,5,25513,227903,1,25513,227903,50,25513,227903,40,25513,227943,0,25513,255888,3,26714,256804,4,27314,257210,5,27914,257211,1,27914,257211,50,27915,257211,40,27915,257251,0,27915,277334,3,28666,278078,4,29041,278432,1,29416,278432,50,29416,278432,40,29416,278432,40,29416,278467,0,29416,278546,50,29417,278546,30,29417,278546,40,29417,278581,0,29417,278682,50,29417,278717,0,29421,278857,50,29421,278857,30,29421,278857,40,29421,278892,0,29421)
%
%
% START OF PROOF
% 278858 [] equal(X,X).
% 278859 [] equal(multiply(identity,X),X).
% 278860 [] equal(multiply(inverse(X),X),identity).
% 278861 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 278862 [] -equal(multiply(X,sk_c6),sk_c5) | -equal(inverse(X),sk_c6).
% 278863 [] equal(multiply(sk_c4,sk_c5),sk_c6) | equal(inverse(sk_c2),sk_c6).
% 278864 [] equal(inverse(sk_c2),sk_c6) | equal(inverse(sk_c4),sk_c6).
% 278865 [] equal(multiply(sk_c3,sk_c6),sk_c7) | equal(inverse(sk_c2),sk_c6).
% 278866 [] equal(inverse(sk_c2),sk_c6) | equal(inverse(sk_c3),sk_c7).
% 278867 [] equal(multiply(sk_c6,sk_c7),sk_c5) | equal(inverse(sk_c2),sk_c6).
% 278868 [?] ?
% 278869 [?] ?
% 278870 [?] ?
% 278871 [?] ?
% 278872 [?] ?
% 278895 [hyper:278862,278864,binarycut:278869] equal(inverse(sk_c4),sk_c6).
% 278898 [para:278895.1.1,278860.1.1.1] equal(multiply(sk_c6,sk_c4),identity).
% 278902 [hyper:278862,278866,binarycut:278871] equal(inverse(sk_c3),sk_c7).
% 278903 [para:278902.1.1,278860.1.1.1] equal(multiply(sk_c7,sk_c3),identity).
% 278906 [hyper:278862,278863,binarycut:278868] equal(multiply(sk_c4,sk_c5),sk_c6).
% 278909 [hyper:278862,278865,binarycut:278870] equal(multiply(sk_c3,sk_c6),sk_c7).
% 278912 [hyper:278862,278867,binarycut:278872] equal(multiply(sk_c6,sk_c7),sk_c5).
% 278913 [para:278860.1.1,278861.1.1.1,demod:278859] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 278914 [para:278898.1.1,278861.1.1.1,demod:278859] equal(X,multiply(sk_c6,multiply(sk_c4,X))).
% 278915 [para:278903.1.1,278861.1.1.1,demod:278859] equal(X,multiply(sk_c7,multiply(sk_c3,X))).
% 278916 [para:278906.1.1,278861.1.1.1] equal(multiply(sk_c6,X),multiply(sk_c4,multiply(sk_c5,X))).
% 278917 [para:278909.1.1,278861.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c3,multiply(sk_c6,X))).
% 278919 [para:278906.1.1,278914.1.2.2] equal(sk_c5,multiply(sk_c6,sk_c6)).
% 278920 [para:278919.1.2,278861.1.1.1] equal(multiply(sk_c5,X),multiply(sk_c6,multiply(sk_c6,X))).
% 278921 [para:278909.1.1,278915.1.2.2] equal(sk_c6,multiply(sk_c7,sk_c7)).
% 278924 [para:278898.1.1,278913.1.2.2] equal(sk_c4,multiply(inverse(sk_c6),identity)).
% 278926 [para:278912.1.1,278913.1.2.2] equal(sk_c7,multiply(inverse(sk_c6),sk_c5)).
% 278928 [para:278919.1.2,278913.1.2.2,demod:278926] equal(sk_c6,sk_c7).
% 278930 [para:278928.1.2,278903.1.1.1] equal(multiply(sk_c6,sk_c3),identity).
% 278932 [para:278928.1.2,278921.1.2.1,demod:278912] equal(sk_c6,sk_c5).
% 278933 [para:278928.1.2,278921.1.2.2] equal(sk_c6,multiply(sk_c7,sk_c6)).
% 278935 [para:278932.1.1,278909.1.1.2] equal(multiply(sk_c3,sk_c5),sk_c7).
% 278936 [para:278932.1.1,278912.1.1.1] equal(multiply(sk_c5,sk_c7),sk_c5).
% 278938 [para:278932.1.1,278919.1.2.1] equal(sk_c5,multiply(sk_c5,sk_c6)).
% 278940 [para:278930.1.1,278913.1.2.2,demod:278924] equal(sk_c3,sk_c4).
% 278943 [para:278940.1.2,278916.1.2.1] equal(multiply(sk_c6,X),multiply(sk_c3,multiply(sk_c5,X))).
% 278946 [para:278932.1.1,278917.1.2.2.1,demod:278943] equal(multiply(sk_c7,X),multiply(sk_c6,X)).
% 278948 [para:278933.1.2,278861.1.1.1,demod:278920,278946] equal(multiply(sk_c6,X),multiply(sk_c5,X)).
% 278953 [para:278936.1.1,278913.1.2.2,demod:278860] equal(sk_c7,identity).
% 278954 [?] ?
% 278956 [para:278953.1.1,278903.1.1.1,demod:278859] equal(sk_c3,identity).
% 278957 [para:278953.1.1,278912.1.1.2,demod:278954,278948] equal(identity,sk_c5).
% 278963 [para:278956.1.1,278935.1.1.1,demod:278859] equal(sk_c5,sk_c7).
% 278970 [para:278957.1.2,278926.1.2.2,demod:278924] equal(sk_c7,sk_c4).
% 278974 [para:278970.1.1,278963.1.2] equal(sk_c5,sk_c4).
% 278978 [para:278974.1.2,278895.1.1.1] equal(inverse(sk_c5),sk_c6).
% 278981 [hyper:278862,278978,demod:278938,cut:278858] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% Split component 4 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c6),sk_c5) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(inverse(sk_c7),sk_c5) | -equal(multiply(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(inverse(Z),sk_c7) | -equal(multiply(Z,sk_c6),sk_c7) | -equal(inverse(U),sk_c6) | -equal(multiply(U,sk_c5),sk_c6).
% Split part used next: -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,1,75,0,1,580,50,4,620,0,4,1140,50,8,1180,0,8,1711,50,14,1751,0,14,2289,50,20,2329,0,20,2874,50,27,2914,0,27,3467,50,41,3507,0,41,4069,50,69,4109,0,69,4681,50,130,4721,0,130,5304,50,264,5344,0,264,5939,50,477,5979,0,477,6587,50,897,6587,40,897,6627,0,897,16947,3,1198,17681,4,1348,18406,1,1498,18406,50,1498,18406,40,1498,18446,0,1498,18617,3,1805,18626,4,1959,18633,5,2099,18633,1,2099,18633,50,2099,18633,40,2099,18673,0,2099,41991,3,3601,43309,4,4350,44560,5,5100,44561,1,5100,44561,50,5101,44561,40,5101,44601,0,5101,59627,3,5852,60579,4,6227,61434,5,6602,61435,1,6602,61435,50,6602,61435,40,6602,61475,0,6602,71161,3,7355,72366,4,7728,73537,1,8103,73537,50,8103,73537,40,8103,73577,0,8103,131505,3,12006,132703,4,13954,133802,1,15904,133802,50,15906,133802,40,15906,133842,0,15906,177536,3,18457,178746,4,19732,179339,5,21007,179340,1,21007,179340,50,21009,179340,40,21009,179380,0,21009,215630,3,22511,216496,4,23260,217334,1,24010,217334,50,24011,217334,40,24011,217374,0,24012,226576,3,24765,227737,4,25140,227903,5,25513,227903,1,25513,227903,50,25513,227903,40,25513,227943,0,25513,255888,3,26714,256804,4,27314,257210,5,27914,257211,1,27914,257211,50,27915,257211,40,27915,257251,0,27915,277334,3,28666,278078,4,29041,278432,1,29416,278432,50,29416,278432,40,29416,278432,40,29416,278467,0,29416,278546,50,29417,278546,30,29417,278546,40,29417,278581,0,29417,278682,50,29417,278717,0,29421,278857,50,29421,278857,30,29421,278857,40,29421,278892,0,29421,278980,50,29422,278980,30,29422,278980,40,29422,279015,0,29422)
%
%
% START OF PROOF
% 278982 [] equal(multiply(identity,X),X).
% 278983 [] equal(multiply(inverse(X),X),identity).
% 278984 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 278985 [] -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7).
% 279001 [] equal(multiply(sk_c4,sk_c5),sk_c6) | equal(inverse(sk_c1),sk_c7).
% 279002 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c4),sk_c6).
% 279003 [] equal(multiply(sk_c3,sk_c6),sk_c7) | equal(inverse(sk_c1),sk_c7).
% 279004 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c3),sk_c7).
% 279005 [] equal(multiply(sk_c6,sk_c7),sk_c5) | equal(inverse(sk_c1),sk_c7).
% 279006 [?] ?
% 279007 [?] ?
% 279008 [?] ?
% 279009 [?] ?
% 279010 [?] ?
% 279026 [hyper:278985,279002,binarycut:279007] equal(inverse(sk_c4),sk_c6).
% 279027 [para:279026.1.1,278983.1.1.1] equal(multiply(sk_c6,sk_c4),identity).
% 279031 [hyper:278985,279004,binarycut:279009] equal(inverse(sk_c3),sk_c7).
% 279035 [para:279031.1.1,278983.1.1.1] equal(multiply(sk_c7,sk_c3),identity).
% 279045 [hyper:278985,279001,binarycut:279006] equal(multiply(sk_c4,sk_c5),sk_c6).
% 279049 [hyper:278985,279003,binarycut:279008] equal(multiply(sk_c3,sk_c6),sk_c7).
% 279052 [hyper:278985,279005,binarycut:279010] equal(multiply(sk_c6,sk_c7),sk_c5).
% 279053 [para:278983.1.1,278984.1.1.1,demod:278982] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 279054 [para:279027.1.1,278984.1.1.1,demod:278982] equal(X,multiply(sk_c6,multiply(sk_c4,X))).
% 279055 [para:279035.1.1,278984.1.1.1,demod:278982] equal(X,multiply(sk_c7,multiply(sk_c3,X))).
% 279059 [para:279045.1.1,279054.1.2.2] equal(sk_c5,multiply(sk_c6,sk_c6)).
% 279061 [para:279049.1.1,279055.1.2.2] equal(sk_c6,multiply(sk_c7,sk_c7)).
% 279064 [para:279027.1.1,279053.1.2.2] equal(sk_c4,multiply(inverse(sk_c6),identity)).
% 279066 [para:279052.1.1,279053.1.2.2] equal(sk_c7,multiply(inverse(sk_c6),sk_c5)).
% 279068 [para:279059.1.2,279053.1.2.2,demod:279066] equal(sk_c6,sk_c7).
% 279070 [para:279068.1.2,279035.1.1.1] equal(multiply(sk_c6,sk_c3),identity).
% 279072 [para:279068.1.2,279061.1.2.1,demod:279052] equal(sk_c6,sk_c5).
% 279076 [para:279072.1.1,279052.1.1.1] equal(multiply(sk_c5,sk_c7),sk_c5).
% 279080 [para:279070.1.1,279053.1.2.2,demod:279064] equal(sk_c3,sk_c4).
% 279082 [para:279080.1.2,279026.1.1.1,demod:279031] equal(sk_c7,sk_c6).
% 279093 [para:279076.1.1,279053.1.2.2,demod:278983] equal(sk_c7,identity).
% 279096 [para:279093.1.1,279035.1.1.1,demod:278982] equal(sk_c3,identity).
% 279101 [para:279096.1.1,279031.1.1.1] equal(inverse(identity),sk_c7).
% 279109 [hyper:278985,279101,demod:278982,cut:279082] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% Split component 5 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c6),sk_c5) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(inverse(sk_c7),sk_c5) | -equal(multiply(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(inverse(Z),sk_c7) | -equal(multiply(Z,sk_c6),sk_c7) | -equal(inverse(U),sk_c6) | -equal(multiply(U,sk_c5),sk_c6).
% Split part used next: -equal(multiply(sk_c7,sk_c6),sk_c5).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 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 21
% 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 21
% 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 21
% 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 21
% 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 21
% 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 21
% 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 21
% 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 21
% 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(35,40,1,75,0,1,580,50,4,620,0,4,1140,50,8,1180,0,8,1711,50,14,1751,0,14,2289,50,20,2329,0,20,2874,50,27,2914,0,27,3467,50,41,3507,0,41,4069,50,69,4109,0,69,4681,50,130,4721,0,130,5304,50,264,5344,0,264,5939,50,477,5979,0,477,6587,50,897,6587,40,897,6627,0,897,16947,3,1198,17681,4,1348,18406,1,1498,18406,50,1498,18406,40,1498,18446,0,1498,18617,3,1805,18626,4,1959,18633,5,2099,18633,1,2099,18633,50,2099,18633,40,2099,18673,0,2099,41991,3,3601,43309,4,4350,44560,5,5100,44561,1,5100,44561,50,5101,44561,40,5101,44601,0,5101,59627,3,5852,60579,4,6227,61434,5,6602,61435,1,6602,61435,50,6602,61435,40,6602,61475,0,6602,71161,3,7355,72366,4,7728,73537,1,8103,73537,50,8103,73537,40,8103,73577,0,8103,131505,3,12006,132703,4,13954,133802,1,15904,133802,50,15906,133802,40,15906,133842,0,15906,177536,3,18457,178746,4,19732,179339,5,21007,179340,1,21007,179340,50,21009,179340,40,21009,179380,0,21009,215630,3,22511,216496,4,23260,217334,1,24010,217334,50,24011,217334,40,24011,217374,0,24012,226576,3,24765,227737,4,25140,227903,5,25513,227903,1,25513,227903,50,25513,227903,40,25513,227943,0,25513,255888,3,26714,256804,4,27314,257210,5,27914,257211,1,27914,257211,50,27915,257211,40,27915,257251,0,27915,277334,3,28666,278078,4,29041,278432,1,29416,278432,50,29416,278432,40,29416,278432,40,29416,278467,0,29416,278546,50,29417,278546,30,29417,278546,40,29417,278581,0,29417,278682,50,29417,278717,0,29421,278857,50,29421,278857,30,29421,278857,40,29421,278892,0,29421,278980,50,29422,278980,30,29422,278980,40,29422,279015,0,29422,279108,50,29422,279108,30,29422,279108,40,29422,279143,0,29427,279246,50,29427,279281,0,29427,279427,50,29430,279462,0,29434,279616,50,29438,279651,0,29438,279813,50,29443,279848,0,29443,280016,50,29451,280051,0,29455,280227,50,29470,280262,0,29470,280446,50,29499,280481,0,29503,280675,50,29561,280710,0,29561,280914,50,29677,280914,40,29677,280949,0,29677)
%
%
% START OF PROOF
% 280915 [] equal(X,X).
% 280916 [] equal(multiply(identity,X),X).
% 280917 [] equal(multiply(inverse(X),X),identity).
% 280918 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 280919 [] -equal(multiply(sk_c7,sk_c6),sk_c5).
% 280945 [?] ?
% 280946 [?] ?
% 280949 [?] ?
% 280996 [input:280946,cut:280919] equal(inverse(sk_c4),sk_c6).
% 280997 [para:280996.1.1,280917.1.1.1] equal(multiply(sk_c6,sk_c4),identity).
% 281010 [input:280945,cut:280919] equal(multiply(sk_c4,sk_c5),sk_c6).
% 281012 [input:280949,cut:280919] equal(multiply(sk_c6,sk_c7),sk_c5).
% 281016 [para:280917.1.1,280918.1.1.1,demod:280916] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 281034 [para:280997.1.1,280918.1.1.1,demod:280916] equal(X,multiply(sk_c6,multiply(sk_c4,X))).
% 281061 [para:281010.1.1,281034.1.2.2] equal(sk_c5,multiply(sk_c6,sk_c6)).
% 281113 [para:281012.1.1,281016.1.2.2] equal(sk_c7,multiply(inverse(sk_c6),sk_c5)).
% 281119 [para:281061.1.2,281016.1.2.2,demod:281113] equal(sk_c6,sk_c7).
% 281125 [para:281119.1.2,280919.1.1.1,demod:281061,cut:280915] 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(multiply(sk_c7,sk_c6),sk_c5) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(inverse(sk_c7),sk_c5) | -equal(multiply(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(inverse(Z),sk_c7) | -equal(multiply(Z,sk_c6),sk_c7) | -equal(inverse(U),sk_c6) | -equal(multiply(U,sk_c5),sk_c6).
% Split part used next: -equal(inverse(sk_c7),sk_c5).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 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 21
% 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 21
% 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 21
% 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 21
% 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 21
% 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 21
% 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 21
% 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 21
% 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(35,40,1,75,0,1,580,50,4,620,0,4,1140,50,8,1180,0,8,1711,50,14,1751,0,14,2289,50,20,2329,0,20,2874,50,27,2914,0,27,3467,50,41,3507,0,41,4069,50,69,4109,0,69,4681,50,130,4721,0,130,5304,50,264,5344,0,264,5939,50,477,5979,0,477,6587,50,897,6587,40,897,6627,0,897,16947,3,1198,17681,4,1348,18406,1,1498,18406,50,1498,18406,40,1498,18446,0,1498,18617,3,1805,18626,4,1959,18633,5,2099,18633,1,2099,18633,50,2099,18633,40,2099,18673,0,2099,41991,3,3601,43309,4,4350,44560,5,5100,44561,1,5100,44561,50,5101,44561,40,5101,44601,0,5101,59627,3,5852,60579,4,6227,61434,5,6602,61435,1,6602,61435,50,6602,61435,40,6602,61475,0,6602,71161,3,7355,72366,4,7728,73537,1,8103,73537,50,8103,73537,40,8103,73577,0,8103,131505,3,12006,132703,4,13954,133802,1,15904,133802,50,15906,133802,40,15906,133842,0,15906,177536,3,18457,178746,4,19732,179339,5,21007,179340,1,21007,179340,50,21009,179340,40,21009,179380,0,21009,215630,3,22511,216496,4,23260,217334,1,24010,217334,50,24011,217334,40,24011,217374,0,24012,226576,3,24765,227737,4,25140,227903,5,25513,227903,1,25513,227903,50,25513,227903,40,25513,227943,0,25513,255888,3,26714,256804,4,27314,257210,5,27914,257211,1,27914,257211,50,27915,257211,40,27915,257251,0,27915,277334,3,28666,278078,4,29041,278432,1,29416,278432,50,29416,278432,40,29416,278432,40,29416,278467,0,29416,278546,50,29417,278546,30,29417,278546,40,29417,278581,0,29417,278682,50,29417,278717,0,29421,278857,50,29421,278857,30,29421,278857,40,29421,278892,0,29421,278980,50,29422,278980,30,29422,278980,40,29422,279015,0,29422,279108,50,29422,279108,30,29422,279108,40,29422,279143,0,29427,279246,50,29427,279281,0,29427,279427,50,29430,279462,0,29434,279616,50,29438,279651,0,29438,279813,50,29443,279848,0,29443,280016,50,29451,280051,0,29455,280227,50,29470,280262,0,29470,280446,50,29499,280481,0,29503,280675,50,29561,280710,0,29561,280914,50,29677,280914,40,29677,280949,0,29677,281124,50,29678,281124,30,29678,281124,40,29678,281159,0,29678,281262,50,29678,281297,0,29683,281443,50,29685,281478,0,29685,281632,50,29689,281667,0,29689,281829,50,29694,281864,0,29699,282032,50,29707,282067,0,29707,282243,50,29722,282278,0,29726,282462,50,29755,282497,0,29755,282691,50,29816,282726,0,29816,282930,50,29932,282930,40,29932,282965,0,29932)
%
%
% START OF PROOF
% 282932 [] equal(multiply(identity,X),X).
% 282933 [] equal(multiply(inverse(X),X),identity).
% 282934 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 282935 [] -equal(inverse(sk_c7),sk_c5).
% 282946 [?] ?
% 282947 [?] ?
% 282948 [?] ?
% 282949 [?] ?
% 282950 [?] ?
% 282974 [input:282947,cut:282935] equal(inverse(sk_c4),sk_c6).
% 282975 [para:282974.1.1,282933.1.1.1] equal(multiply(sk_c6,sk_c4),identity).
% 282976 [input:282949,cut:282935] equal(inverse(sk_c3),sk_c7).
% 282977 [para:282976.1.1,282933.1.1.1] equal(multiply(sk_c7,sk_c3),identity).
% 282989 [input:282946,cut:282935] equal(multiply(sk_c4,sk_c5),sk_c6).
% 282990 [input:282948,cut:282935] equal(multiply(sk_c3,sk_c6),sk_c7).
% 282991 [input:282950,cut:282935] equal(multiply(sk_c6,sk_c7),sk_c5).
% 283019 [para:282933.1.1,282934.1.1.1,demod:282932] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 283021 [para:282975.1.1,282934.1.1.1,demod:282932] equal(X,multiply(sk_c6,multiply(sk_c4,X))).
% 283022 [para:282977.1.1,282934.1.1.1,demod:282932] equal(X,multiply(sk_c7,multiply(sk_c3,X))).
% 283055 [para:282989.1.1,283021.1.2.2] equal(sk_c5,multiply(sk_c6,sk_c6)).
% 283058 [para:282990.1.1,283022.1.2.2] equal(sk_c6,multiply(sk_c7,sk_c7)).
% 283073 [para:282991.1.1,283019.1.2.2] equal(sk_c7,multiply(inverse(sk_c6),sk_c5)).
% 283098 [para:283055.1.2,283019.1.2.2,demod:283073] equal(sk_c6,sk_c7).
% 283104 [para:283098.1.2,282935.1.1.1] -equal(inverse(sk_c6),sk_c5).
% 283114 [para:283098.1.2,283058.1.2.1] equal(sk_c6,multiply(sk_c6,sk_c7)).
% 283127 [para:283114.1.2,282991.1.1] equal(sk_c6,sk_c5).
% 283134 [para:283127.1.1,282991.1.1.1] equal(multiply(sk_c5,sk_c7),sk_c5).
% 283153 [para:283134.1.1,283019.1.2.2,demod:282933] equal(sk_c7,identity).
% 283155 [para:283153.1.1,282977.1.1.1,demod:282932] equal(sk_c3,identity).
% 283161 [para:283153.1.1,283098.1.2] equal(sk_c6,identity).
% 283164 [para:283155.1.1,282976.1.1.1] equal(inverse(identity),sk_c7).
% 283172 [para:283161.1.1,282991.1.1.1,demod:282932] equal(sk_c7,sk_c5).
% 283175 [para:283161.1.1,283104.1.1.1,demod:283164,cut:283172] 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_c7,sk_c6),sk_c5) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(inverse(sk_c7),sk_c5) | -equal(multiply(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(inverse(Z),sk_c7) | -equal(multiply(Z,sk_c6),sk_c7) | -equal(inverse(U),sk_c6) | -equal(multiply(U,sk_c5),sk_c6).
% Split part used next: -equal(multiply(sk_c6,sk_c7),sk_c5).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 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 21
% 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 21
% 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 21
% 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 21
% 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 21
% 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 21
% 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 21
% 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 21
% 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(35,40,1,75,0,1,580,50,4,620,0,4,1140,50,8,1180,0,8,1711,50,14,1751,0,14,2289,50,20,2329,0,20,2874,50,27,2914,0,27,3467,50,41,3507,0,41,4069,50,69,4109,0,69,4681,50,130,4721,0,130,5304,50,264,5344,0,264,5939,50,477,5979,0,477,6587,50,897,6587,40,897,6627,0,897,16947,3,1198,17681,4,1348,18406,1,1498,18406,50,1498,18406,40,1498,18446,0,1498,18617,3,1805,18626,4,1959,18633,5,2099,18633,1,2099,18633,50,2099,18633,40,2099,18673,0,2099,41991,3,3601,43309,4,4350,44560,5,5100,44561,1,5100,44561,50,5101,44561,40,5101,44601,0,5101,59627,3,5852,60579,4,6227,61434,5,6602,61435,1,6602,61435,50,6602,61435,40,6602,61475,0,6602,71161,3,7355,72366,4,7728,73537,1,8103,73537,50,8103,73537,40,8103,73577,0,8103,131505,3,12006,132703,4,13954,133802,1,15904,133802,50,15906,133802,40,15906,133842,0,15906,177536,3,18457,178746,4,19732,179339,5,21007,179340,1,21007,179340,50,21009,179340,40,21009,179380,0,21009,215630,3,22511,216496,4,23260,217334,1,24010,217334,50,24011,217334,40,24011,217374,0,24012,226576,3,24765,227737,4,25140,227903,5,25513,227903,1,25513,227903,50,25513,227903,40,25513,227943,0,25513,255888,3,26714,256804,4,27314,257210,5,27914,257211,1,27914,257211,50,27915,257211,40,27915,257251,0,27915,277334,3,28666,278078,4,29041,278432,1,29416,278432,50,29416,278432,40,29416,278432,40,29416,278467,0,29416,278546,50,29417,278546,30,29417,278546,40,29417,278581,0,29417,278682,50,29417,278717,0,29421,278857,50,29421,278857,30,29421,278857,40,29421,278892,0,29421,278980,50,29422,278980,30,29422,278980,40,29422,279015,0,29422,279108,50,29422,279108,30,29422,279108,40,29422,279143,0,29427,279246,50,29427,279281,0,29427,279427,50,29430,279462,0,29434,279616,50,29438,279651,0,29438,279813,50,29443,279848,0,29443,280016,50,29451,280051,0,29455,280227,50,29470,280262,0,29470,280446,50,29499,280481,0,29503,280675,50,29561,280710,0,29561,280914,50,29677,280914,40,29677,280949,0,29677,281124,50,29678,281124,30,29678,281124,40,29678,281159,0,29678,281262,50,29678,281297,0,29683,281443,50,29685,281478,0,29685,281632,50,29689,281667,0,29689,281829,50,29694,281864,0,29699,282032,50,29707,282067,0,29707,282243,50,29722,282278,0,29726,282462,50,29755,282497,0,29755,282691,50,29816,282726,0,29816,282930,50,29932,282930,40,29932,282965,0,29932,283174,50,29932,283174,30,29932,283174,40,29932,283209,0,29932,283305,50,29933,283340,0,29938,283483,50,29940,283518,0,29940,283669,50,29944,283704,0,29944,283863,50,29949,283898,0,29954,284063,50,29962,284098,0,29962,284271,50,29977,284306,0,29982,284487,50,30010,284522,0,30010,284713,50,30071,284748,0,30071,284949,50,30186,284949,40,30186,284984,0,30186)
%
%
% START OF PROOF
% 284821 [?] ?
% 284951 [] equal(multiply(identity,X),X).
% 284952 [] equal(multiply(inverse(X),X),identity).
% 284953 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 284954 [] -equal(multiply(sk_c6,sk_c7),sk_c5).
% 284959 [?] ?
% 284964 [?] ?
% 284974 [?] ?
% 284979 [?] ?
% 284984 [?] ?
% 285007 [input:284959,cut:284954] equal(inverse(sk_c2),sk_c6).
% 285008 [para:285007.1.1,284952.1.1.1] equal(multiply(sk_c6,sk_c2),identity).
% 285025 [input:284974,cut:284954] equal(inverse(sk_c1),sk_c7).
% 285026 [para:285025.1.1,284952.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 285033 [input:284964,cut:284954] equal(multiply(sk_c2,sk_c6),sk_c5).
% 285042 [input:284979,cut:284954] equal(multiply(sk_c1,sk_c7),sk_c6).
% 285047 [input:284984,cut:284954] equal(multiply(sk_c7,sk_c6),sk_c5).
% 285053 [para:285008.1.1,284953.1.1.1,demod:284951] equal(X,multiply(sk_c6,multiply(sk_c2,X))).
% 285065 [para:285026.1.1,284953.1.1.1,demod:284951] equal(X,multiply(sk_c7,multiply(sk_c1,X))).
% 285093 [para:285033.1.1,285053.1.2.2] equal(sk_c6,multiply(sk_c6,sk_c5)).
% 285111 [para:285042.1.1,285065.1.2.2] equal(sk_c7,multiply(sk_c7,sk_c6)).
% 285117 [para:285111.1.2,285047.1.1] equal(sk_c7,sk_c5).
% 285120 [para:285117.1.1,284954.1.1.2,demod:285093,cut:284821] 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: 38034
% derived clauses: 6572261
% kept clauses: 240848
% kept size sum: 280093
% kept mid-nuclei: 3163
% kept new demods: 5331
% forw unit-subs: 2553397
% forw double-subs: 3469134
% forw overdouble-subs: 262467
% backward subs: 10331
% fast unit cutoff: 26098
% full unit cutoff: 0
% dbl unit cutoff: 5792
% real runtime : 302.61
% process. runtime: 301.85
% specific non-discr-tree subsumption statistics:
% tried: 37554782
% length fails: 5195508
% strength fails: 9261907
% predlist fails: 1672521
% aux str. fails: 5781150
% by-lit fails: 9046612
% full subs tried: 1384794
% full subs fail: 1300639
%
% ; 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/GRP301-1+eq_r.in")
%
%------------------------------------------------------------------------------