%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP350-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 : art03.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.3s
% Output : Assurance 299.3s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----NO SOLUTION OUTPUT BY SYSTEM
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
%
% Gandalf c-2.6 r1 starting to prove: /home/graph/tptp/TSTP/PreparedTPTP/otter:hypothesis:set(auto),clear(print_given)---add_equality:r/GRP/GRP350-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 33)
% (binary-unit 12 #f)
% (binary-unit-uniteq 12 #f)
% (binary-posweight-kb-big-order 60 #f 3 33)
% (binary-posweight-lex-big-order 30 #f 3 33)
% (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_c10,sk_c11),sk_c9) | -equal(inverse(sk_c10),sk_c9) | -equal(multiply(sk_c9,sk_c11),sk_c10) | -equal(inverse(X),sk_c11) | -equal(multiply(X,sk_c10),sk_c11) | -equal(inverse(Y),sk_c10) | -equal(multiply(Y,sk_c9),sk_c10) | -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X1),X2) | -equal(inverse(X2),W) | -equal(multiply(X1,W),X2).
% was split for some strategies as:
% -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X2),W) | -equal(inverse(X1),X2) | -equal(multiply(X1,W),X2).
% -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10).
% -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11).
% -equal(inverse(Y),sk_c10) | -equal(multiply(Y,sk_c9),sk_c10).
% -equal(inverse(X),sk_c11) | -equal(multiply(X,sk_c10),sk_c11).
% -equal(multiply(sk_c10,sk_c11),sk_c9).
% -equal(inverse(sk_c10),sk_c9).
% -equal(multiply(sk_c9,sk_c11),sk_c10).
%
% Starting a split proof attempt with 8 components.
%
% Split component 1 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c10,sk_c11),sk_c9) | -equal(inverse(sk_c10),sk_c9) | -equal(multiply(sk_c9,sk_c11),sk_c10) | -equal(inverse(X),sk_c11) | -equal(multiply(X,sk_c10),sk_c11) | -equal(inverse(Y),sk_c10) | -equal(multiply(Y,sk_c9),sk_c10) | -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X1),X2) | -equal(inverse(X2),W) | -equal(multiply(X1,W),X2).
% Split part used next: -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X2),W) | -equal(inverse(X1),X2) | -equal(multiply(X1,W),X2).
% END OF PROOFPART
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(75,40,1,159,0,1,97795,4,1147,102557,5,1502,102559,1,1502,102559,50,1502,102559,40,1502,102643,0,1502,103033,5,2116,103036,1,2117,103036,50,2117,103036,40,2117,103120,0,2117,103510,5,2725,103513,1,2727,103513,50,2727,103513,40,2727,103597,0,2727,121455,3,4228,123040,4,4978,124915,1,5728,124915,50,5728,124915,40,5728,124999,0,5728,138246,3,6483,139337,4,6854,140443,1,7229,140443,50,7229,140443,40,7229,140527,0,7229,141087,5,8732,141093,1,8733,141093,50,8733,141093,40,8733,141177,0,8733,182210,3,12636,183789,4,14584,185091,5,16534,185092,1,16534,185092,50,16535,185092,40,16535,185176,0,16535,221225,3,19087,222335,4,20361,223283,5,21636,223284,1,21636,223284,50,21637,223284,40,21637,223368,0,21637,252878,3,23138,253665,4,23888,254252,5,24638,254253,1,24638,254253,50,24639,254253,40,24639,254337,0,24639,254908,5,26145,254911,1,26146,254911,50,26146,254911,40,26146,254995,0,26146,276896,3,27347,277776,4,27947,278592,1,28547,278592,50,28548,278592,40,28548,278676,0,28548,294655,3,29299,295155,4,29674,295595,1,30049,295595,50,30051,295595,40,30051,295595,40,30051,295744,0,30052)
%
%
% START OF PROOF
% 295597 [] equal(multiply(identity,X),X).
% 295598 [] equal(multiply(inverse(X),X),identity).
% 295599 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 295670 [] -equal(multiply(X,sk_c10),sk_c11) | -equal(multiply(Y,X),sk_c11) | -equal(multiply(Z,X),U) | -equal(inverse(Z),U) | -equal(inverse(U),X) | -equal(inverse(Y),X).
% 295671 [] -equal(multiply(X,Y),Z) | -equal(inverse(X),Z) | -equal(inverse(Z),Y) | $spltprd1($spltcnst97,Y).
% 295672 [] -equal(multiply(X,Y),sk_c11) | -equal(inverse(X),Y) | $spltprd1($spltcnst98,Y).
% 295673 [] -equal(multiply(X,sk_c10),sk_c11) | $spltprd1($spltcnst99,X).
% 295674 [] -$spltprd1($spltcnst98,X) | -$spltprd1($spltcnst97,X) | -$spltprd1($spltcnst99,X).
% 295675 [] equal(multiply(sk_c2,sk_c9),sk_c10) | equal(multiply(sk_c7,sk_c8),sk_c6).
% 295676 [] equal(multiply(sk_c2,sk_c9),sk_c10) | equal(inverse(sk_c6),sk_c8).
% 295677 [] equal(multiply(sk_c2,sk_c9),sk_c10) | equal(inverse(sk_c7),sk_c6).
% 295678 [] equal(multiply(sk_c2,sk_c9),sk_c10) | equal(multiply(sk_c8,sk_c10),sk_c11).
% 295679 [] equal(multiply(sk_c2,sk_c9),sk_c10) | equal(inverse(sk_c5),sk_c8).
% 295680 [] equal(multiply(sk_c2,sk_c9),sk_c10) | equal(multiply(sk_c5,sk_c8),sk_c11).
% 295685 [] equal(multiply(sk_c7,sk_c8),sk_c6) | equal(inverse(sk_c2),sk_c10).
% 295686 [] equal(inverse(sk_c2),sk_c10) | equal(inverse(sk_c6),sk_c8).
% 295687 [] equal(inverse(sk_c2),sk_c10) | equal(inverse(sk_c7),sk_c6).
% 295688 [] equal(multiply(sk_c8,sk_c10),sk_c11) | equal(inverse(sk_c2),sk_c10).
% 295689 [] equal(inverse(sk_c2),sk_c10) | equal(inverse(sk_c5),sk_c8).
% 295690 [?] ?
% 295695 [] equal(multiply(sk_c1,sk_c10),sk_c11) | equal(multiply(sk_c7,sk_c8),sk_c6).
% 295696 [] equal(multiply(sk_c1,sk_c10),sk_c11) | equal(inverse(sk_c6),sk_c8).
% 295697 [] equal(multiply(sk_c1,sk_c10),sk_c11) | equal(inverse(sk_c7),sk_c6).
% 295698 [] equal(multiply(sk_c1,sk_c10),sk_c11) | equal(multiply(sk_c8,sk_c10),sk_c11).
% 295699 [] equal(multiply(sk_c1,sk_c10),sk_c11) | equal(inverse(sk_c5),sk_c8).
% 295700 [] equal(multiply(sk_c1,sk_c10),sk_c11) | equal(multiply(sk_c5,sk_c8),sk_c11).
% 295705 [] equal(multiply(sk_c7,sk_c8),sk_c6) | equal(inverse(sk_c1),sk_c11).
% 295706 [] equal(inverse(sk_c1),sk_c11) | equal(inverse(sk_c6),sk_c8).
% 295707 [] equal(inverse(sk_c1),sk_c11) | equal(inverse(sk_c7),sk_c6).
% 295708 [] equal(multiply(sk_c8,sk_c10),sk_c11) | equal(inverse(sk_c1),sk_c11).
% 295709 [] equal(inverse(sk_c1),sk_c11) | equal(inverse(sk_c5),sk_c8).
% 295710 [?] ?
% 295715 [] equal(multiply(sk_c9,sk_c11),sk_c10) | equal(multiply(sk_c7,sk_c8),sk_c6).
% 295716 [] equal(multiply(sk_c9,sk_c11),sk_c10) | equal(inverse(sk_c6),sk_c8).
% 295717 [] equal(multiply(sk_c9,sk_c11),sk_c10) | equal(inverse(sk_c7),sk_c6).
% 295718 [] equal(multiply(sk_c9,sk_c11),sk_c10) | equal(multiply(sk_c8,sk_c10),sk_c11).
% 295719 [] equal(multiply(sk_c9,sk_c11),sk_c10) | equal(inverse(sk_c5),sk_c8).
% 295720 [] equal(multiply(sk_c9,sk_c11),sk_c10) | equal(multiply(sk_c5,sk_c8),sk_c11).
% 295725 [] equal(multiply(sk_c7,sk_c8),sk_c6) | equal(inverse(sk_c10),sk_c9).
% 295726 [] equal(inverse(sk_c10),sk_c9) | equal(inverse(sk_c6),sk_c8).
% 295727 [] equal(inverse(sk_c10),sk_c9) | equal(inverse(sk_c7),sk_c6).
% 295728 [] equal(multiply(sk_c8,sk_c10),sk_c11) | equal(inverse(sk_c10),sk_c9).
% 295729 [] equal(inverse(sk_c10),sk_c9) | equal(inverse(sk_c5),sk_c8).
% 295730 [?] ?
% 295735 [] equal(multiply(sk_c10,sk_c11),sk_c9) | equal(multiply(sk_c7,sk_c8),sk_c6).
% 295736 [] equal(multiply(sk_c10,sk_c11),sk_c9) | equal(inverse(sk_c6),sk_c8).
% 295737 [] equal(multiply(sk_c10,sk_c11),sk_c9) | equal(inverse(sk_c7),sk_c6).
% 295738 [] equal(multiply(sk_c10,sk_c11),sk_c9) | equal(multiply(sk_c8,sk_c10),sk_c11).
% 295739 [] equal(multiply(sk_c10,sk_c11),sk_c9) | equal(inverse(sk_c5),sk_c8).
% 295740 [] equal(multiply(sk_c10,sk_c11),sk_c9) | equal(multiply(sk_c5,sk_c8),sk_c11).
% 295811 [hyper:295672,295689,binarycut:295690] equal(inverse(sk_c2),sk_c10) | $spltprd1($spltcnst98,sk_c8).
% 295899 [hyper:295672,295709,binarycut:295710] equal(inverse(sk_c1),sk_c11) | $spltprd1($spltcnst98,sk_c8).
% 295987 [hyper:295672,295729,binarycut:295730] equal(inverse(sk_c10),sk_c9) | $spltprd1($spltcnst98,sk_c8).
% 296198 [hyper:295671,295685,295686,295687] equal(inverse(sk_c2),sk_c10) | $spltprd1($spltcnst97,sk_c8).
% 296229 [hyper:295673,295688] equal(inverse(sk_c2),sk_c10) | $spltprd1($spltcnst99,sk_c8).
% 296240 [hyper:295674,296229,296198,295811] equal(inverse(sk_c2),sk_c10).
% 296247 [para:296240.1.1,295598.1.1.1] equal(multiply(sk_c10,sk_c2),identity).
% 296477 [hyper:295671,295705,295706,295707] equal(inverse(sk_c1),sk_c11) | $spltprd1($spltcnst97,sk_c8).
% 296566 [hyper:295673,295708] equal(inverse(sk_c1),sk_c11) | $spltprd1($spltcnst99,sk_c8).
% 296604 [hyper:295674,296566,296477,295899] equal(inverse(sk_c1),sk_c11).
% 296638 [para:296604.1.1,295598.1.1.1] equal(multiply(sk_c11,sk_c1),identity).
% 296782 [hyper:295671,295725,295726,295727] equal(inverse(sk_c10),sk_c9) | $spltprd1($spltcnst97,sk_c8).
% 296860 [hyper:295673,295728] equal(inverse(sk_c10),sk_c9) | $spltprd1($spltcnst99,sk_c8).
% 296887 [hyper:295674,296860,296782,295987] equal(inverse(sk_c10),sk_c9).
% 296907 [para:296887.1.1,295598.1.1.1] equal(multiply(sk_c9,sk_c10),identity).
% 297191 [hyper:295670,295680,295678,295675,295677,295676,295679] equal(multiply(sk_c2,sk_c9),sk_c10).
% 297371 [hyper:295670,295700,295698,295699,295696,295695,295697] equal(multiply(sk_c1,sk_c10),sk_c11).
% 297482 [hyper:295670,295720,295718,295719,295716,295715,295717] equal(multiply(sk_c9,sk_c11),sk_c10).
% 297556 [hyper:295670,295740,295738,295739,295736,295735,295737] equal(multiply(sk_c10,sk_c11),sk_c9).
% 297561 [para:296247.1.1,295599.1.1.1,demod:295597] equal(X,multiply(sk_c10,multiply(sk_c2,X))).
% 297562 [para:296638.1.1,295599.1.1.1,demod:295597] equal(X,multiply(sk_c11,multiply(sk_c1,X))).
% 297563 [para:296907.1.1,295599.1.1.1,demod:295597] equal(X,multiply(sk_c9,multiply(sk_c10,X))).
% 297588 [para:297191.1.1,297561.1.2.2] equal(sk_c9,multiply(sk_c10,sk_c10)).
% 297606 [para:297371.1.1,297562.1.2.2] equal(sk_c10,multiply(sk_c11,sk_c11)).
% 297625 [para:297556.1.1,297563.1.2.2] equal(sk_c11,multiply(sk_c9,sk_c9)).
% 297626 [para:297561.1.2,297563.1.2.2] equal(multiply(sk_c2,X),multiply(sk_c9,X)).
% 297627 [para:297588.1.2,297563.1.2.2,demod:297625] equal(sk_c10,sk_c11).
% 297629 [para:297627.1.1,296887.1.1.1] equal(inverse(sk_c11),sk_c9).
% 297630 [para:297627.1.1,296907.1.1.2,demod:297482] equal(sk_c10,identity).
% 297632 [para:297627.1.1,297556.1.1.1,demod:297606] equal(sk_c10,sk_c9).
% 297634 [para:297627.1.1,297588.1.2.1] equal(sk_c9,multiply(sk_c11,sk_c10)).
% 297637 [para:297630.1.1,296887.1.1.1] equal(inverse(identity),sk_c9).
% 297639 [para:297630.1.1,297556.1.1.1,demod:295597] equal(sk_c11,sk_c9).
% 297640 [para:297630.1.1,297561.1.2.1,demod:295597,297626] equal(X,multiply(sk_c9,X)).
% 297645 [para:297632.1.1,296887.1.1.1] equal(inverse(sk_c9),sk_c9).
% 297647 [para:297632.1.1,297627.1.1] equal(sk_c9,sk_c11).
% 297649 [para:297639.1.1,296638.1.1.1,demod:297640] equal(sk_c1,identity).
% 297659 [para:297649.1.1,297562.1.2.2.1,demod:295597] equal(X,multiply(sk_c11,X)).
% 297675 [hyper:295670,297629,295597,demod:297645,297659,demod:297637,297634,cut:297647,cut:297647,cut:297647,cut:297639] 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 33
% 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_c10,sk_c11),sk_c9) | -equal(inverse(sk_c10),sk_c9) | -equal(multiply(sk_c9,sk_c11),sk_c10) | -equal(inverse(X),sk_c11) | -equal(multiply(X,sk_c10),sk_c11) | -equal(inverse(Y),sk_c10) | -equal(multiply(Y,sk_c9),sk_c10) | -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X1),X2) | -equal(inverse(X2),W) | -equal(multiply(X1,W),X2).
% Split part used next: -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 33
% 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 33
% clause depth limited to 4
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(75,40,1,159,0,1,97795,4,1147,102557,5,1502,102559,1,1502,102559,50,1502,102559,40,1502,102643,0,1502,103033,5,2116,103036,1,2117,103036,50,2117,103036,40,2117,103120,0,2117,103510,5,2725,103513,1,2727,103513,50,2727,103513,40,2727,103597,0,2727,121455,3,4228,123040,4,4978,124915,1,5728,124915,50,5728,124915,40,5728,124999,0,5728,138246,3,6483,139337,4,6854,140443,1,7229,140443,50,7229,140443,40,7229,140527,0,7229,141087,5,8732,141093,1,8733,141093,50,8733,141093,40,8733,141177,0,8733,182210,3,12636,183789,4,14584,185091,5,16534,185092,1,16534,185092,50,16535,185092,40,16535,185176,0,16535,221225,3,19087,222335,4,20361,223283,5,21636,223284,1,21636,223284,50,21637,223284,40,21637,223368,0,21637,252878,3,23138,253665,4,23888,254252,5,24638,254253,1,24638,254253,50,24639,254253,40,24639,254337,0,24639,254908,5,26145,254911,1,26146,254911,50,26146,254911,40,26146,254995,0,26146,276896,3,27347,277776,4,27947,278592,1,28547,278592,50,28548,278592,40,28548,278676,0,28548,294655,3,29299,295155,4,29674,295595,1,30049,295595,50,30051,295595,40,30051,295595,40,30051,295744,0,30052,297674,50,30071,297674,30,30071,297674,40,30071,297749,0,30071,297897,50,30072,297972,0,30076)
%
%
% START OF PROOF
% 297899 [] equal(multiply(identity,X),X).
% 297900 [] equal(multiply(inverse(X),X),identity).
% 297901 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 297902 [] -equal(multiply(X,sk_c10),sk_c9) | -equal(inverse(X),sk_c10).
% 297909 [] equal(multiply(sk_c2,sk_c9),sk_c10) | equal(inverse(sk_c4),sk_c10).
% 297910 [] equal(multiply(sk_c2,sk_c9),sk_c10) | equal(multiply(sk_c4,sk_c10),sk_c9).
% 297919 [] equal(inverse(sk_c2),sk_c10) | equal(inverse(sk_c4),sk_c10).
% 297920 [?] ?
% 297929 [] equal(multiply(sk_c1,sk_c10),sk_c11) | equal(inverse(sk_c4),sk_c10).
% 297930 [] equal(multiply(sk_c1,sk_c10),sk_c11) | equal(multiply(sk_c4,sk_c10),sk_c9).
% 297939 [] equal(inverse(sk_c1),sk_c11) | equal(inverse(sk_c4),sk_c10).
% 297940 [?] ?
% 297949 [] equal(multiply(sk_c9,sk_c11),sk_c10) | equal(inverse(sk_c4),sk_c10).
% 297950 [] equal(multiply(sk_c9,sk_c11),sk_c10) | equal(multiply(sk_c4,sk_c10),sk_c9).
% 297959 [] equal(inverse(sk_c10),sk_c9) | equal(inverse(sk_c4),sk_c10).
% 297960 [?] ?
% 297969 [] equal(multiply(sk_c10,sk_c11),sk_c9) | equal(inverse(sk_c4),sk_c10).
% 297970 [] equal(multiply(sk_c10,sk_c11),sk_c9) | equal(multiply(sk_c4,sk_c10),sk_c9).
% 297984 [hyper:297902,297919,binarycut:297920] equal(inverse(sk_c2),sk_c10).
% 297987 [para:297984.1.1,297900.1.1.1] equal(multiply(sk_c10,sk_c2),identity).
% 297995 [hyper:297902,297939,binarycut:297940] equal(inverse(sk_c1),sk_c11).
% 297996 [para:297995.1.1,297900.1.1.1] equal(multiply(sk_c11,sk_c1),identity).
% 298003 [hyper:297902,297959,binarycut:297960] equal(inverse(sk_c10),sk_c9).
% 298004 [para:298003.1.1,297900.1.1.1] equal(multiply(sk_c9,sk_c10),identity).
% 298028 [hyper:297902,297910,297909] equal(multiply(sk_c2,sk_c9),sk_c10).
% 298042 [hyper:297902,297930,297929] equal(multiply(sk_c1,sk_c10),sk_c11).
% 298048 [hyper:297902,297950,297949] equal(multiply(sk_c9,sk_c11),sk_c10).
% 298054 [hyper:297902,297970,297969] equal(multiply(sk_c10,sk_c11),sk_c9).
% 298055 [para:297900.1.1,297901.1.1.1,demod:297899] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 298056 [para:297987.1.1,297901.1.1.1,demod:297899] equal(X,multiply(sk_c10,multiply(sk_c2,X))).
% 298057 [para:297996.1.1,297901.1.1.1,demod:297899] equal(X,multiply(sk_c11,multiply(sk_c1,X))).
% 298063 [para:298028.1.1,298056.1.2.2] equal(sk_c9,multiply(sk_c10,sk_c10)).
% 298065 [para:298042.1.1,298057.1.2.2] equal(sk_c10,multiply(sk_c11,sk_c11)).
% 298068 [para:297900.1.1,298055.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 298073 [para:297901.1.1,298055.1.2.2] equal(X,multiply(inverse(multiply(Y,Z)),multiply(Y,multiply(Z,X)))).
% 298074 [para:298054.1.1,298055.1.2.2,demod:298003] equal(sk_c11,multiply(sk_c9,sk_c9)).
% 298075 [para:298056.1.2,298055.1.2.2,demod:298003] equal(multiply(sk_c2,X),multiply(sk_c9,X)).
% 298076 [para:298063.1.2,298055.1.2.2,demod:298074,298003] equal(sk_c10,sk_c11).
% 298078 [para:298055.1.2,298055.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 298081 [para:298076.1.1,298004.1.1.2,demod:298048] equal(sk_c10,identity).
% 298083 [para:298076.1.1,298054.1.1.1,demod:298065] equal(sk_c10,sk_c9).
% 298090 [para:298081.1.1,298056.1.2.1,demod:297899,298075] equal(X,multiply(sk_c9,X)).
% 298091 [para:298081.1.1,298063.1.2.1,demod:297899] equal(sk_c9,sk_c10).
% 298095 [para:298083.1.1,298003.1.1.1] equal(inverse(sk_c9),sk_c9).
% 298137 [para:298078.1.2,297900.1.1] equal(multiply(X,inverse(X)),identity).
% 298139 [para:298078.1.2,298068.1.2] equal(X,multiply(X,identity)).
% 298140 [para:298139.1.2,298068.1.2] equal(X,inverse(inverse(X))).
% 298141 [para:298137.1.1,298073.1.2.2.2,demod:298139] equal(inverse(X),multiply(inverse(multiply(Y,X)),Y)).
% 298143 [para:298056.1.2,298141.1.2.1.1,demod:298090,298075] equal(inverse(X),multiply(inverse(X),sk_c10)).
% 298153 [para:298143.1.2,298078.1.2,demod:298140] equal(multiply(X,sk_c10),X).
% 298154 [hyper:297902,298153,demod:298095,cut:298091] 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 33
% clause depth limited to 4
% seconds given: 2
%
%
% Split component 3 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c10,sk_c11),sk_c9) | -equal(inverse(sk_c10),sk_c9) | -equal(multiply(sk_c9,sk_c11),sk_c10) | -equal(inverse(X),sk_c11) | -equal(multiply(X,sk_c10),sk_c11) | -equal(inverse(Y),sk_c10) | -equal(multiply(Y,sk_c9),sk_c10) | -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X1),X2) | -equal(inverse(X2),W) | -equal(multiply(X1,W),X2).
% Split part used next: -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 33
% 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 33
% clause depth limited to 4
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(75,40,1,159,0,1,97795,4,1147,102557,5,1502,102559,1,1502,102559,50,1502,102559,40,1502,102643,0,1502,103033,5,2116,103036,1,2117,103036,50,2117,103036,40,2117,103120,0,2117,103510,5,2725,103513,1,2727,103513,50,2727,103513,40,2727,103597,0,2727,121455,3,4228,123040,4,4978,124915,1,5728,124915,50,5728,124915,40,5728,124999,0,5728,138246,3,6483,139337,4,6854,140443,1,7229,140443,50,7229,140443,40,7229,140527,0,7229,141087,5,8732,141093,1,8733,141093,50,8733,141093,40,8733,141177,0,8733,182210,3,12636,183789,4,14584,185091,5,16534,185092,1,16534,185092,50,16535,185092,40,16535,185176,0,16535,221225,3,19087,222335,4,20361,223283,5,21636,223284,1,21636,223284,50,21637,223284,40,21637,223368,0,21637,252878,3,23138,253665,4,23888,254252,5,24638,254253,1,24638,254253,50,24639,254253,40,24639,254337,0,24639,254908,5,26145,254911,1,26146,254911,50,26146,254911,40,26146,254995,0,26146,276896,3,27347,277776,4,27947,278592,1,28547,278592,50,28548,278592,40,28548,278676,0,28548,294655,3,29299,295155,4,29674,295595,1,30049,295595,50,30051,295595,40,30051,295595,40,30051,295744,0,30052,297674,50,30071,297674,30,30071,297674,40,30071,297749,0,30071,297897,50,30072,297972,0,30076,298153,50,30077,298153,30,30077,298153,40,30077,298228,0,30077,298409,50,30077,298484,0,30083)
%
%
% START OF PROOF
% 298411 [] equal(multiply(identity,X),X).
% 298412 [] equal(multiply(inverse(X),X),identity).
% 298413 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 298414 [] -equal(multiply(X,sk_c11),sk_c10) | -equal(inverse(X),sk_c11).
% 298423 [] equal(multiply(sk_c2,sk_c9),sk_c10) | equal(inverse(sk_c3),sk_c11).
% 298424 [] equal(multiply(sk_c2,sk_c9),sk_c10) | equal(multiply(sk_c3,sk_c11),sk_c10).
% 298433 [] equal(inverse(sk_c2),sk_c10) | equal(inverse(sk_c3),sk_c11).
% 298434 [?] ?
% 298443 [] equal(multiply(sk_c1,sk_c10),sk_c11) | equal(inverse(sk_c3),sk_c11).
% 298444 [] equal(multiply(sk_c1,sk_c10),sk_c11) | equal(multiply(sk_c3,sk_c11),sk_c10).
% 298453 [] equal(inverse(sk_c1),sk_c11) | equal(inverse(sk_c3),sk_c11).
% 298454 [?] ?
% 298463 [] equal(multiply(sk_c9,sk_c11),sk_c10) | equal(inverse(sk_c3),sk_c11).
% 298464 [] equal(multiply(sk_c9,sk_c11),sk_c10) | equal(multiply(sk_c3,sk_c11),sk_c10).
% 298473 [] equal(inverse(sk_c10),sk_c9) | equal(inverse(sk_c3),sk_c11).
% 298474 [?] ?
% 298483 [] equal(multiply(sk_c10,sk_c11),sk_c9) | equal(inverse(sk_c3),sk_c11).
% 298484 [] equal(multiply(sk_c10,sk_c11),sk_c9) | equal(multiply(sk_c3,sk_c11),sk_c10).
% 298492 [hyper:298414,298433,binarycut:298434] equal(inverse(sk_c2),sk_c10).
% 298493 [para:298492.1.1,298412.1.1.1] equal(multiply(sk_c10,sk_c2),identity).
% 298510 [hyper:298414,298453,binarycut:298454] equal(inverse(sk_c1),sk_c11).
% 298514 [para:298510.1.1,298412.1.1.1] equal(multiply(sk_c11,sk_c1),identity).
% 298523 [hyper:298414,298473,binarycut:298474] equal(inverse(sk_c10),sk_c9).
% 298524 [para:298523.1.1,298412.1.1.1] equal(multiply(sk_c9,sk_c10),identity).
% 298548 [hyper:298414,298424,298423] equal(multiply(sk_c2,sk_c9),sk_c10).
% 298573 [hyper:298414,298444,298443] equal(multiply(sk_c1,sk_c10),sk_c11).
% 298589 [hyper:298414,298464,298463] equal(multiply(sk_c9,sk_c11),sk_c10).
% 298599 [hyper:298414,298484,298483] equal(multiply(sk_c10,sk_c11),sk_c9).
% 298600 [para:298412.1.1,298413.1.1.1,demod:298411] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 298601 [para:298493.1.1,298413.1.1.1,demod:298411] equal(X,multiply(sk_c10,multiply(sk_c2,X))).
% 298602 [para:298514.1.1,298413.1.1.1,demod:298411] equal(X,multiply(sk_c11,multiply(sk_c1,X))).
% 298608 [para:298548.1.1,298601.1.2.2] equal(sk_c9,multiply(sk_c10,sk_c10)).
% 298610 [para:298573.1.1,298602.1.2.2] equal(sk_c10,multiply(sk_c11,sk_c11)).
% 298613 [para:298412.1.1,298600.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 298618 [para:298413.1.1,298600.1.2.2] equal(X,multiply(inverse(multiply(Y,Z)),multiply(Y,multiply(Z,X)))).
% 298619 [para:298599.1.1,298600.1.2.2,demod:298523] equal(sk_c11,multiply(sk_c9,sk_c9)).
% 298620 [para:298601.1.2,298600.1.2.2,demod:298523] equal(multiply(sk_c2,X),multiply(sk_c9,X)).
% 298621 [para:298608.1.2,298600.1.2.2,demod:298619,298523] equal(sk_c10,sk_c11).
% 298623 [para:298600.1.2,298600.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 298626 [para:298621.1.1,298524.1.1.2,demod:298589] equal(sk_c10,identity).
% 298628 [para:298621.1.1,298599.1.1.1,demod:298610] equal(sk_c10,sk_c9).
% 298635 [para:298626.1.1,298601.1.2.1,demod:298411,298620] equal(X,multiply(sk_c9,X)).
% 298644 [para:298628.1.1,298621.1.1] equal(sk_c9,sk_c11).
% 298682 [para:298623.1.2,298412.1.1] equal(multiply(X,inverse(X)),identity).
% 298684 [para:298623.1.2,298613.1.2] equal(X,multiply(X,identity)).
% 298685 [para:298684.1.2,298613.1.2] equal(X,inverse(inverse(X))).
% 298686 [para:298682.1.1,298618.1.2.2.2,demod:298684] equal(inverse(X),multiply(inverse(multiply(Y,X)),Y)).
% 298688 [para:298601.1.2,298686.1.2.1.1,demod:298635,298620] equal(inverse(X),multiply(inverse(X),sk_c10)).
% 298698 [para:298688.1.2,298623.1.2,demod:298685] equal(multiply(X,sk_c10),X).
% 298699 [para:298621.1.1,298698.1.1.2] equal(multiply(X,sk_c11),X).
% 298704 [hyper:298414,298699,demod:298523,cut:298644] 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 33
% clause depth limited to 4
% seconds given: 2
%
%
% Split component 4 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c10,sk_c11),sk_c9) | -equal(inverse(sk_c10),sk_c9) | -equal(multiply(sk_c9,sk_c11),sk_c10) | -equal(inverse(X),sk_c11) | -equal(multiply(X,sk_c10),sk_c11) | -equal(inverse(Y),sk_c10) | -equal(multiply(Y,sk_c9),sk_c10) | -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X1),X2) | -equal(inverse(X2),W) | -equal(multiply(X1,W),X2).
% Split part used next: -equal(inverse(Y),sk_c10) | -equal(multiply(Y,sk_c9),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 33
% clause depth limited to 3
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(75,40,1,159,0,1,97795,4,1147,102557,5,1502,102559,1,1502,102559,50,1502,102559,40,1502,102643,0,1502,103033,5,2116,103036,1,2117,103036,50,2117,103036,40,2117,103120,0,2117,103510,5,2725,103513,1,2727,103513,50,2727,103513,40,2727,103597,0,2727,121455,3,4228,123040,4,4978,124915,1,5728,124915,50,5728,124915,40,5728,124999,0,5728,138246,3,6483,139337,4,6854,140443,1,7229,140443,50,7229,140443,40,7229,140527,0,7229,141087,5,8732,141093,1,8733,141093,50,8733,141093,40,8733,141177,0,8733,182210,3,12636,183789,4,14584,185091,5,16534,185092,1,16534,185092,50,16535,185092,40,16535,185176,0,16535,221225,3,19087,222335,4,20361,223283,5,21636,223284,1,21636,223284,50,21637,223284,40,21637,223368,0,21637,252878,3,23138,253665,4,23888,254252,5,24638,254253,1,24638,254253,50,24639,254253,40,24639,254337,0,24639,254908,5,26145,254911,1,26146,254911,50,26146,254911,40,26146,254995,0,26146,276896,3,27347,277776,4,27947,278592,1,28547,278592,50,28548,278592,40,28548,278676,0,28548,294655,3,29299,295155,4,29674,295595,1,30049,295595,50,30051,295595,40,30051,295595,40,30051,295744,0,30052,297674,50,30071,297674,30,30071,297674,40,30071,297749,0,30071,297897,50,30072,297972,0,30076,298153,50,30077,298153,30,30077,298153,40,30077,298228,0,30077,298409,50,30077,298484,0,30083,298703,50,30084,298703,30,30084,298703,40,30084,298778,0,30084)
%
%
% START OF PROOF
% 298705 [] equal(multiply(identity,X),X).
% 298706 [] equal(multiply(inverse(X),X),identity).
% 298707 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 298708 [] -equal(multiply(X,sk_c9),sk_c10) | -equal(inverse(X),sk_c10).
% 298710 [?] ?
% 298711 [?] ?
% 298712 [] equal(multiply(sk_c2,sk_c9),sk_c10) | equal(multiply(sk_c8,sk_c10),sk_c11).
% 298713 [?] ?
% 298714 [] equal(multiply(sk_c2,sk_c9),sk_c10) | equal(multiply(sk_c5,sk_c8),sk_c11).
% 298715 [?] ?
% 298716 [] equal(multiply(sk_c2,sk_c9),sk_c10) | equal(multiply(sk_c4,sk_c10),sk_c9).
% 298717 [?] ?
% 298718 [] equal(multiply(sk_c2,sk_c9),sk_c10) | equal(multiply(sk_c3,sk_c11),sk_c10).
% 298720 [] equal(inverse(sk_c2),sk_c10) | equal(inverse(sk_c6),sk_c8).
% 298721 [] equal(inverse(sk_c2),sk_c10) | equal(inverse(sk_c7),sk_c6).
% 298722 [] equal(multiply(sk_c8,sk_c10),sk_c11) | equal(inverse(sk_c2),sk_c10).
% 298723 [] equal(inverse(sk_c2),sk_c10) | equal(inverse(sk_c5),sk_c8).
% 298724 [] equal(multiply(sk_c5,sk_c8),sk_c11) | equal(inverse(sk_c2),sk_c10).
% 298725 [] equal(inverse(sk_c2),sk_c10) | equal(inverse(sk_c4),sk_c10).
% 298726 [] equal(multiply(sk_c4,sk_c10),sk_c9) | equal(inverse(sk_c2),sk_c10).
% 298727 [] equal(inverse(sk_c2),sk_c10) | equal(inverse(sk_c3),sk_c11).
% 298728 [] equal(multiply(sk_c3,sk_c11),sk_c10) | equal(inverse(sk_c2),sk_c10).
% 298781 [hyper:298708,298720,binarycut:298710] equal(inverse(sk_c6),sk_c8).
% 298782 [para:298781.1.1,298706.1.1.1] equal(multiply(sk_c8,sk_c6),identity).
% 298786 [hyper:298708,298721,binarycut:298711] equal(inverse(sk_c7),sk_c6).
% 298787 [para:298786.1.1,298706.1.1.1] equal(multiply(sk_c6,sk_c7),identity).
% 298790 [hyper:298708,298723,binarycut:298713] equal(inverse(sk_c5),sk_c8).
% 298794 [para:298790.1.1,298706.1.1.1] equal(multiply(sk_c8,sk_c5),identity).
% 298797 [hyper:298708,298725,binarycut:298715] equal(inverse(sk_c4),sk_c10).
% 298804 [para:298797.1.1,298706.1.1.1] equal(multiply(sk_c10,sk_c4),identity).
% 298808 [hyper:298708,298727,binarycut:298717] equal(inverse(sk_c3),sk_c11).
% 298809 [para:298808.1.1,298706.1.1.1] equal(multiply(sk_c11,sk_c3),identity).
% 298818 [hyper:298708,298722,binarycut:298712] equal(multiply(sk_c8,sk_c10),sk_c11).
% 298824 [hyper:298708,298724,binarycut:298714] equal(multiply(sk_c5,sk_c8),sk_c11).
% 298827 [hyper:298708,298726,binarycut:298716] equal(multiply(sk_c4,sk_c10),sk_c9).
% 298833 [hyper:298708,298728,binarycut:298718] equal(multiply(sk_c3,sk_c11),sk_c10).
% 298834 [para:298706.1.1,298707.1.1.1,demod:298705] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 298835 [para:298782.1.1,298707.1.1.1,demod:298705] equal(X,multiply(sk_c8,multiply(sk_c6,X))).
% 298836 [para:298787.1.1,298707.1.1.1,demod:298705] equal(X,multiply(sk_c6,multiply(sk_c7,X))).
% 298842 [para:298824.1.1,298707.1.1.1] equal(multiply(sk_c11,X),multiply(sk_c5,multiply(sk_c8,X))).
% 298845 [para:298787.1.1,298835.1.2.2] equal(sk_c7,multiply(sk_c8,identity)).
% 298846 [para:298845.1.2,298707.1.1.1,demod:298705] equal(multiply(sk_c7,X),multiply(sk_c8,X)).
% 298852 [para:298782.1.1,298834.1.2.2] equal(sk_c6,multiply(inverse(sk_c8),identity)).
% 298854 [para:298794.1.1,298834.1.2.2,demod:298852] equal(sk_c5,sk_c6).
% 298858 [para:298824.1.1,298834.1.2.2,demod:298790] equal(sk_c8,multiply(sk_c8,sk_c11)).
% 298863 [para:298854.1.2,298836.1.2.1,demod:298842,298846] equal(X,multiply(sk_c11,X)).
% 298866 [para:298863.1.2,298809.1.1] equal(sk_c3,identity).
% 298869 [para:298866.1.1,298833.1.1.1,demod:298705] equal(sk_c11,sk_c10).
% 298870 [para:298869.1.2,298804.1.1.1,demod:298863] equal(sk_c4,identity).
% 298871 [para:298869.1.2,298818.1.1.2,demod:298858] equal(sk_c8,sk_c11).
% 298874 [para:298870.1.1,298827.1.1.1,demod:298705] equal(sk_c10,sk_c9).
% 298878 [para:298871.1.2,298863.1.2.1] equal(X,multiply(sk_c8,X)).
% 298880 [para:298874.1.1,298818.1.1.2,demod:298878] equal(sk_c9,sk_c11).
% 298884 [para:298880.1.2,298833.1.1.2] equal(multiply(sk_c3,sk_c9),sk_c10).
% 298974 [hyper:298708,298884,demod:298808,cut:298869] 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 33
% 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_c10,sk_c11),sk_c9) | -equal(inverse(sk_c10),sk_c9) | -equal(multiply(sk_c9,sk_c11),sk_c10) | -equal(inverse(X),sk_c11) | -equal(multiply(X,sk_c10),sk_c11) | -equal(inverse(Y),sk_c10) | -equal(multiply(Y,sk_c9),sk_c10) | -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X1),X2) | -equal(inverse(X2),W) | -equal(multiply(X1,W),X2).
% Split part used next: -equal(inverse(X),sk_c11) | -equal(multiply(X,sk_c10),sk_c11).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 33
% clause depth limited to 3
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(75,40,1,159,0,1,97795,4,1147,102557,5,1502,102559,1,1502,102559,50,1502,102559,40,1502,102643,0,1502,103033,5,2116,103036,1,2117,103036,50,2117,103036,40,2117,103120,0,2117,103510,5,2725,103513,1,2727,103513,50,2727,103513,40,2727,103597,0,2727,121455,3,4228,123040,4,4978,124915,1,5728,124915,50,5728,124915,40,5728,124999,0,5728,138246,3,6483,139337,4,6854,140443,1,7229,140443,50,7229,140443,40,7229,140527,0,7229,141087,5,8732,141093,1,8733,141093,50,8733,141093,40,8733,141177,0,8733,182210,3,12636,183789,4,14584,185091,5,16534,185092,1,16534,185092,50,16535,185092,40,16535,185176,0,16535,221225,3,19087,222335,4,20361,223283,5,21636,223284,1,21636,223284,50,21637,223284,40,21637,223368,0,21637,252878,3,23138,253665,4,23888,254252,5,24638,254253,1,24638,254253,50,24639,254253,40,24639,254337,0,24639,254908,5,26145,254911,1,26146,254911,50,26146,254911,40,26146,254995,0,26146,276896,3,27347,277776,4,27947,278592,1,28547,278592,50,28548,278592,40,28548,278676,0,28548,294655,3,29299,295155,4,29674,295595,1,30049,295595,50,30051,295595,40,30051,295595,40,30051,295744,0,30052,297674,50,30071,297674,30,30071,297674,40,30071,297749,0,30071,297897,50,30072,297972,0,30076,298153,50,30077,298153,30,30077,298153,40,30077,298228,0,30077,298409,50,30077,298484,0,30083,298703,50,30084,298703,30,30084,298703,40,30084,298778,0,30084,298973,50,30086,298973,30,30086,298973,40,30086,299048,0,30091)
%
%
% START OF PROOF
% 298975 [] equal(multiply(identity,X),X).
% 298976 [] equal(multiply(inverse(X),X),identity).
% 298977 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 298978 [] -equal(multiply(X,sk_c10),sk_c11) | -equal(inverse(X),sk_c11).
% 299000 [?] ?
% 299001 [?] ?
% 299002 [?] ?
% 299003 [?] ?
% 299004 [] equal(multiply(sk_c1,sk_c10),sk_c11) | equal(multiply(sk_c5,sk_c8),sk_c11).
% 299005 [?] ?
% 299006 [?] ?
% 299007 [?] ?
% 299008 [?] ?
% 299010 [] equal(inverse(sk_c1),sk_c11) | equal(inverse(sk_c6),sk_c8).
% 299011 [] equal(inverse(sk_c1),sk_c11) | equal(inverse(sk_c7),sk_c6).
% 299012 [] equal(multiply(sk_c8,sk_c10),sk_c11) | equal(inverse(sk_c1),sk_c11).
% 299013 [] equal(inverse(sk_c1),sk_c11) | equal(inverse(sk_c5),sk_c8).
% 299014 [] equal(multiply(sk_c5,sk_c8),sk_c11) | equal(inverse(sk_c1),sk_c11).
% 299015 [] equal(inverse(sk_c1),sk_c11) | equal(inverse(sk_c4),sk_c10).
% 299016 [] equal(multiply(sk_c4,sk_c10),sk_c9) | equal(inverse(sk_c1),sk_c11).
% 299017 [] equal(inverse(sk_c1),sk_c11) | equal(inverse(sk_c3),sk_c11).
% 299018 [] equal(multiply(sk_c3,sk_c11),sk_c10) | equal(inverse(sk_c1),sk_c11).
% 299059 [hyper:298978,299010,binarycut:299000] equal(inverse(sk_c6),sk_c8).
% 299060 [para:299059.1.1,298976.1.1.1] equal(multiply(sk_c8,sk_c6),identity).
% 299064 [hyper:298978,299011,binarycut:299001] equal(inverse(sk_c7),sk_c6).
% 299065 [para:299064.1.1,298976.1.1.1] equal(multiply(sk_c6,sk_c7),identity).
% 299071 [hyper:298978,299013,binarycut:299003] equal(inverse(sk_c5),sk_c8).
% 299072 [para:299071.1.1,298976.1.1.1] equal(multiply(sk_c8,sk_c5),identity).
% 299076 [hyper:298978,299015,binarycut:299005] equal(inverse(sk_c4),sk_c10).
% 299077 [para:299076.1.1,298976.1.1.1] equal(multiply(sk_c10,sk_c4),identity).
% 299080 [hyper:298978,299017,binarycut:299007] equal(inverse(sk_c3),sk_c11).
% 299085 [para:299080.1.1,298976.1.1.1] equal(multiply(sk_c11,sk_c3),identity).
% 299104 [hyper:298978,299012,binarycut:299002] equal(multiply(sk_c8,sk_c10),sk_c11).
% 299113 [hyper:298978,299014,binarycut:299004] equal(multiply(sk_c5,sk_c8),sk_c11).
% 299116 [hyper:298978,299016,binarycut:299006] equal(multiply(sk_c4,sk_c10),sk_c9).
% 299119 [hyper:298978,299018,binarycut:299008] equal(multiply(sk_c3,sk_c11),sk_c10).
% 299120 [para:298976.1.1,298977.1.1.1,demod:298975] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 299121 [para:299060.1.1,298977.1.1.1,demod:298975] equal(X,multiply(sk_c8,multiply(sk_c6,X))).
% 299122 [para:299065.1.1,298977.1.1.1,demod:298975] equal(X,multiply(sk_c6,multiply(sk_c7,X))).
% 299128 [para:299113.1.1,298977.1.1.1] equal(multiply(sk_c11,X),multiply(sk_c5,multiply(sk_c8,X))).
% 299131 [para:299065.1.1,299121.1.2.2] equal(sk_c7,multiply(sk_c8,identity)).
% 299132 [para:299131.1.2,298977.1.1.1,demod:298975] equal(multiply(sk_c7,X),multiply(sk_c8,X)).
% 299138 [para:299060.1.1,299120.1.2.2] equal(sk_c6,multiply(inverse(sk_c8),identity)).
% 299140 [para:299072.1.1,299120.1.2.2,demod:299138] equal(sk_c5,sk_c6).
% 299144 [para:299113.1.1,299120.1.2.2,demod:299071] equal(sk_c8,multiply(sk_c8,sk_c11)).
% 299149 [para:299140.1.2,299122.1.2.1,demod:299128,299132] equal(X,multiply(sk_c11,X)).
% 299152 [para:299149.1.2,299085.1.1] equal(sk_c3,identity).
% 299154 [para:299152.1.1,299080.1.1.1] equal(inverse(identity),sk_c11).
% 299155 [para:299152.1.1,299119.1.1.1,demod:298975] equal(sk_c11,sk_c10).
% 299156 [para:299155.1.2,299077.1.1.1,demod:299149] equal(sk_c4,identity).
% 299157 [para:299155.1.2,299104.1.1.2,demod:299144] equal(sk_c8,sk_c11).
% 299160 [para:299156.1.1,299116.1.1.1,demod:298975] equal(sk_c10,sk_c9).
% 299164 [para:299157.1.2,299149.1.2.1] equal(X,multiply(sk_c8,X)).
% 299166 [para:299160.1.1,299104.1.1.2,demod:299164] equal(sk_c9,sk_c11).
% 299171 [para:299166.1.2,299149.1.2.1] equal(X,multiply(sk_c9,X)).
% 299172 [para:299166.1.2,299157.1.2] equal(sk_c8,sk_c9).
% 299177 [para:299172.1.1,299104.1.1.1,demod:299171] equal(sk_c10,sk_c11).
% 299259 [hyper:298978,299154,demod:298975,cut:299177] 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 33
% 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_c10,sk_c11),sk_c9) | -equal(inverse(sk_c10),sk_c9) | -equal(multiply(sk_c9,sk_c11),sk_c10) | -equal(inverse(X),sk_c11) | -equal(multiply(X,sk_c10),sk_c11) | -equal(inverse(Y),sk_c10) | -equal(multiply(Y,sk_c9),sk_c10) | -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X1),X2) | -equal(inverse(X2),W) | -equal(multiply(X1,W),X2).
% Split part used next: -equal(multiply(sk_c10,sk_c11),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 33
% 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 33
% 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 33
% 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 33
% 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 33
% 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 33
% 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 33
% 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(75,40,1,159,0,1,97795,4,1147,102557,5,1502,102559,1,1502,102559,50,1502,102559,40,1502,102643,0,1502,103033,5,2116,103036,1,2117,103036,50,2117,103036,40,2117,103120,0,2117,103510,5,2725,103513,1,2727,103513,50,2727,103513,40,2727,103597,0,2727,121455,3,4228,123040,4,4978,124915,1,5728,124915,50,5728,124915,40,5728,124999,0,5728,138246,3,6483,139337,4,6854,140443,1,7229,140443,50,7229,140443,40,7229,140527,0,7229,141087,5,8732,141093,1,8733,141093,50,8733,141093,40,8733,141177,0,8733,182210,3,12636,183789,4,14584,185091,5,16534,185092,1,16534,185092,50,16535,185092,40,16535,185176,0,16535,221225,3,19087,222335,4,20361,223283,5,21636,223284,1,21636,223284,50,21637,223284,40,21637,223368,0,21637,252878,3,23138,253665,4,23888,254252,5,24638,254253,1,24638,254253,50,24639,254253,40,24639,254337,0,24639,254908,5,26145,254911,1,26146,254911,50,26146,254911,40,26146,254995,0,26146,276896,3,27347,277776,4,27947,278592,1,28547,278592,50,28548,278592,40,28548,278676,0,28548,294655,3,29299,295155,4,29674,295595,1,30049,295595,50,30051,295595,40,30051,295595,40,30051,295744,0,30052,297674,50,30071,297674,30,30071,297674,40,30071,297749,0,30071,297897,50,30072,297972,0,30076,298153,50,30077,298153,30,30077,298153,40,30077,298228,0,30077,298409,50,30077,298484,0,30083,298703,50,30084,298703,30,30084,298703,40,30084,298778,0,30084,298973,50,30086,298973,30,30086,298973,40,30086,299048,0,30091,299258,50,30092,299258,30,30092,299258,40,30092,299333,0,30093,299554,50,30095,299629,0,30099,299905,50,30103,299980,0,30103,300267,50,30109,300342,0,30115,300654,50,30126,300729,0,30126,301047,50,30141,301122,0,30145,301448,50,30168,301523,0,30168,301858,50,30209,301858,40,30209,301933,0,30213)
%
%
% START OF PROOF
% 301651 [?] ?
% 301860 [] equal(multiply(identity,X),X).
% 301861 [] equal(multiply(inverse(X),X),identity).
% 301862 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 301863 [] -equal(multiply(sk_c10,sk_c11),sk_c9).
% 301925 [?] ?
% 301926 [?] ?
% 301928 [?] ?
% 301929 [?] ?
% 301932 [?] ?
% 301933 [?] ?
% 302047 [input:301925,cut:301863] equal(inverse(sk_c6),sk_c8).
% 302048 [para:302047.1.1,301861.1.1.1] equal(multiply(sk_c8,sk_c6),identity).
% 302050 [input:301926,cut:301863] equal(inverse(sk_c7),sk_c6).
% 302051 [para:302050.1.1,301861.1.1.1] equal(multiply(sk_c6,sk_c7),identity).
% 302052 [input:301928,cut:301863] equal(inverse(sk_c5),sk_c8).
% 302053 [para:302052.1.1,301861.1.1.1] equal(multiply(sk_c8,sk_c5),identity).
% 302057 [input:301932,cut:301863] equal(inverse(sk_c3),sk_c11).
% 302058 [para:302057.1.1,301861.1.1.1] equal(multiply(sk_c11,sk_c3),identity).
% 302081 [input:301929,cut:301863] equal(multiply(sk_c5,sk_c8),sk_c11).
% 302083 [input:301933,cut:301863] equal(multiply(sk_c3,sk_c11),sk_c10).
% 302131 [para:302048.1.1,301862.1.1.1,demod:301860] equal(X,multiply(sk_c8,multiply(sk_c6,X))).
% 302134 [para:302051.1.1,301862.1.1.1,demod:301860] equal(X,multiply(sk_c6,multiply(sk_c7,X))).
% 302139 [para:302058.1.1,301862.1.1.1,demod:301860] equal(X,multiply(sk_c11,multiply(sk_c3,X))).
% 302167 [para:302081.1.1,301862.1.1.1] equal(multiply(sk_c11,X),multiply(sk_c5,multiply(sk_c8,X))).
% 302170 [para:302051.1.1,302131.1.2.2] equal(sk_c7,multiply(sk_c8,identity)).
% 302171 [para:302170.1.2,301862.1.1.1,demod:301860] equal(multiply(sk_c7,X),multiply(sk_c8,X)).
% 302205 [para:302083.1.1,302139.1.2.2] equal(sk_c11,multiply(sk_c11,sk_c10)).
% 302208 [para:302171.1.1,302134.1.2.2] equal(X,multiply(sk_c6,multiply(sk_c8,X))).
% 302214 [para:302048.1.1,302208.1.2.2] equal(sk_c6,multiply(sk_c6,identity)).
% 302215 [para:302053.1.1,302208.1.2.2,demod:302214] equal(sk_c5,sk_c6).
% 302222 [para:302215.1.2,302134.1.2.1,demod:302167,302171] equal(X,multiply(sk_c11,X)).
% 302233 [para:302222.1.2,302205.1.2] equal(sk_c11,sk_c10).
% 302242 [para:302233.1.2,301863.1.1.1,demod:302222,cut:301651] 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_c10,sk_c11),sk_c9) | -equal(inverse(sk_c10),sk_c9) | -equal(multiply(sk_c9,sk_c11),sk_c10) | -equal(inverse(X),sk_c11) | -equal(multiply(X,sk_c10),sk_c11) | -equal(inverse(Y),sk_c10) | -equal(multiply(Y,sk_c9),sk_c10) | -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X1),X2) | -equal(inverse(X2),W) | -equal(multiply(X1,W),X2).
% Split part used next: -equal(inverse(sk_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 33
% 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 33
% 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 33
% 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 33
% 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 33
% 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 33
% 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 33
% 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(75,40,1,159,0,1,97795,4,1147,102557,5,1502,102559,1,1502,102559,50,1502,102559,40,1502,102643,0,1502,103033,5,2116,103036,1,2117,103036,50,2117,103036,40,2117,103120,0,2117,103510,5,2725,103513,1,2727,103513,50,2727,103513,40,2727,103597,0,2727,121455,3,4228,123040,4,4978,124915,1,5728,124915,50,5728,124915,40,5728,124999,0,5728,138246,3,6483,139337,4,6854,140443,1,7229,140443,50,7229,140443,40,7229,140527,0,7229,141087,5,8732,141093,1,8733,141093,50,8733,141093,40,8733,141177,0,8733,182210,3,12636,183789,4,14584,185091,5,16534,185092,1,16534,185092,50,16535,185092,40,16535,185176,0,16535,221225,3,19087,222335,4,20361,223283,5,21636,223284,1,21636,223284,50,21637,223284,40,21637,223368,0,21637,252878,3,23138,253665,4,23888,254252,5,24638,254253,1,24638,254253,50,24639,254253,40,24639,254337,0,24639,254908,5,26145,254911,1,26146,254911,50,26146,254911,40,26146,254995,0,26146,276896,3,27347,277776,4,27947,278592,1,28547,278592,50,28548,278592,40,28548,278676,0,28548,294655,3,29299,295155,4,29674,295595,1,30049,295595,50,30051,295595,40,30051,295595,40,30051,295744,0,30052,297674,50,30071,297674,30,30071,297674,40,30071,297749,0,30071,297897,50,30072,297972,0,30076,298153,50,30077,298153,30,30077,298153,40,30077,298228,0,30077,298409,50,30077,298484,0,30083,298703,50,30084,298703,30,30084,298703,40,30084,298778,0,30084,298973,50,30086,298973,30,30086,298973,40,30086,299048,0,30091,299258,50,30092,299258,30,30092,299258,40,30092,299333,0,30093,299554,50,30095,299629,0,30099,299905,50,30103,299980,0,30103,300267,50,30109,300342,0,30115,300654,50,30126,300729,0,30126,301047,50,30141,301122,0,30145,301448,50,30168,301523,0,30168,301858,50,30209,301858,40,30209,301933,0,30213,302241,50,30214,302241,30,30214,302241,40,30214,302316,0,30214,302537,50,30216,302612,0,30220,302888,50,30225,302963,0,30225,303250,50,30232,303325,0,30237,303637,50,30248,303712,0,30248,304030,50,30264,304105,0,30268,304431,50,30292,304506,0,30292,304841,50,30333,304841,40,30333,304916,0,30338)
%
%
% START OF PROOF
% 304843 [] equal(multiply(identity,X),X).
% 304844 [] equal(multiply(inverse(X),X),identity).
% 304845 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 304846 [] -equal(inverse(sk_c10),sk_c9).
% 304897 [?] ?
% 304898 [?] ?
% 304899 [?] ?
% 304900 [?] ?
% 304901 [?] ?
% 304902 [?] ?
% 304903 [?] ?
% 304904 [?] ?
% 304905 [?] ?
% 304906 [?] ?
% 304950 [input:304898,cut:304846] equal(inverse(sk_c6),sk_c8).
% 304951 [para:304950.1.1,304844.1.1.1] equal(multiply(sk_c8,sk_c6),identity).
% 304954 [input:304899,cut:304846] equal(inverse(sk_c7),sk_c6).
% 304955 [para:304954.1.1,304844.1.1.1] equal(multiply(sk_c6,sk_c7),identity).
% 304956 [input:304901,cut:304846] equal(inverse(sk_c5),sk_c8).
% 304957 [para:304956.1.1,304844.1.1.1] equal(multiply(sk_c8,sk_c5),identity).
% 304959 [input:304903,cut:304846] equal(inverse(sk_c4),sk_c10).
% 304960 [para:304959.1.1,304844.1.1.1] equal(multiply(sk_c10,sk_c4),identity).
% 304961 [input:304905,cut:304846] equal(inverse(sk_c3),sk_c11).
% 304962 [para:304961.1.1,304844.1.1.1] equal(multiply(sk_c11,sk_c3),identity).
% 305002 [input:304897,cut:304846] equal(multiply(sk_c7,sk_c8),sk_c6).
% 305003 [input:304900,cut:304846] equal(multiply(sk_c8,sk_c10),sk_c11).
% 305005 [input:304902,cut:304846] equal(multiply(sk_c5,sk_c8),sk_c11).
% 305006 [input:304904,cut:304846] equal(multiply(sk_c4,sk_c10),sk_c9).
% 305007 [input:304906,cut:304846] equal(multiply(sk_c3,sk_c11),sk_c10).
% 305039 [para:304951.1.1,304845.1.1.1,demod:304843] equal(X,multiply(sk_c8,multiply(sk_c6,X))).
% 305040 [para:304955.1.1,304845.1.1.1,demod:304843] equal(X,multiply(sk_c6,multiply(sk_c7,X))).
% 305041 [para:304957.1.1,304845.1.1.1,demod:304843] equal(X,multiply(sk_c8,multiply(sk_c5,X))).
% 305044 [para:304960.1.1,304845.1.1.1,demod:304843] equal(X,multiply(sk_c10,multiply(sk_c4,X))).
% 305045 [para:304962.1.1,304845.1.1.1,demod:304843] equal(X,multiply(sk_c11,multiply(sk_c3,X))).
% 305085 [para:305005.1.1,304845.1.1.1] equal(multiply(sk_c11,X),multiply(sk_c5,multiply(sk_c8,X))).
% 305114 [para:304955.1.1,305039.1.2.2] equal(sk_c7,multiply(sk_c8,identity)).
% 305115 [para:305114.1.2,304845.1.1.1,demod:304843] equal(multiply(sk_c7,X),multiply(sk_c8,X)).
% 305120 [para:305002.1.1,305040.1.2.2] equal(sk_c8,multiply(sk_c6,sk_c6)).
% 305123 [para:305120.1.2,305039.1.2.2] equal(sk_c6,multiply(sk_c8,sk_c8)).
% 305130 [para:305005.1.1,305041.1.2.2] equal(sk_c8,multiply(sk_c8,sk_c11)).
% 305136 [para:305006.1.1,305044.1.2.2] equal(sk_c10,multiply(sk_c10,sk_c9)).
% 305141 [para:305007.1.1,305045.1.2.2] equal(sk_c11,multiply(sk_c11,sk_c10)).
% 305145 [para:305115.1.1,305040.1.2.2] equal(X,multiply(sk_c6,multiply(sk_c8,X))).
% 305146 [para:304951.1.1,305145.1.2.2] equal(sk_c6,multiply(sk_c6,identity)).
% 305147 [para:304957.1.1,305145.1.2.2,demod:305146] equal(sk_c5,sk_c6).
% 305153 [para:305041.1.2,305145.1.2.2] equal(multiply(sk_c5,X),multiply(sk_c6,X)).
% 305157 [para:305147.1.2,305040.1.2.1,demod:305085,305115] equal(X,multiply(sk_c11,X)).
% 305161 [para:305157.1.2,304962.1.1] equal(sk_c3,identity).
% 305166 [para:305157.1.2,305045.1.2] equal(X,multiply(sk_c3,X)).
% 305167 [para:305157.1.2,305141.1.2] equal(sk_c11,sk_c10).
% 305171 [para:305161.1.1,304961.1.1.1] equal(inverse(identity),sk_c11).
% 305186 [para:305167.1.2,305003.1.1.2,demod:305130] equal(sk_c8,sk_c11).
% 305201 [para:305167.1.2,305136.1.2.1,demod:305157] equal(sk_c10,sk_c9).
% 305215 [para:305186.1.2,305007.1.1.2,demod:305166] equal(sk_c8,sk_c10).
% 305226 [para:305186.1.2,305130.1.2.2,demod:305123] equal(sk_c8,sk_c6).
% 305248 [para:305201.1.1,305141.1.2.2,demod:305157] equal(sk_c11,sk_c9).
% 305261 [para:305215.1.2,305003.1.1.2,demod:305123] equal(sk_c6,sk_c11).
% 305271 [para:305226.1.2,305120.1.2.1,demod:304951] equal(sk_c8,identity).
% 305301 [para:305261.1.2,305045.1.2.1,demod:305153,305166] equal(X,multiply(sk_c5,X)).
% 305320 [para:305271.1.1,305005.1.1.2,demod:305301] equal(identity,sk_c11).
% 305360 [para:305320.1.2,305007.1.1.2,demod:305166] equal(identity,sk_c10).
% 305415 [para:305360.1.2,304846.1.1.1,demod:305171,cut:305248] 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_c10,sk_c11),sk_c9) | -equal(inverse(sk_c10),sk_c9) | -equal(multiply(sk_c9,sk_c11),sk_c10) | -equal(inverse(X),sk_c11) | -equal(multiply(X,sk_c10),sk_c11) | -equal(inverse(Y),sk_c10) | -equal(multiply(Y,sk_c9),sk_c10) | -equal(multiply(Z,sk_c11),sk_c10) | -equal(inverse(Z),sk_c11) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(V,W),sk_c11) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c11) | -equal(inverse(X1),X2) | -equal(inverse(X2),W) | -equal(multiply(X1,W),X2).
% Split part used next: -equal(multiply(sk_c9,sk_c11),sk_c10).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 33
% 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 33
% 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 33
% 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 33
% 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 33
% 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 33
% 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 33
% 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(75,40,1,159,0,1,97795,4,1147,102557,5,1502,102559,1,1502,102559,50,1502,102559,40,1502,102643,0,1502,103033,5,2116,103036,1,2117,103036,50,2117,103036,40,2117,103120,0,2117,103510,5,2725,103513,1,2727,103513,50,2727,103513,40,2727,103597,0,2727,121455,3,4228,123040,4,4978,124915,1,5728,124915,50,5728,124915,40,5728,124999,0,5728,138246,3,6483,139337,4,6854,140443,1,7229,140443,50,7229,140443,40,7229,140527,0,7229,141087,5,8732,141093,1,8733,141093,50,8733,141093,40,8733,141177,0,8733,182210,3,12636,183789,4,14584,185091,5,16534,185092,1,16534,185092,50,16535,185092,40,16535,185176,0,16535,221225,3,19087,222335,4,20361,223283,5,21636,223284,1,21636,223284,50,21637,223284,40,21637,223368,0,21637,252878,3,23138,253665,4,23888,254252,5,24638,254253,1,24638,254253,50,24639,254253,40,24639,254337,0,24639,254908,5,26145,254911,1,26146,254911,50,26146,254911,40,26146,254995,0,26146,276896,3,27347,277776,4,27947,278592,1,28547,278592,50,28548,278592,40,28548,278676,0,28548,294655,3,29299,295155,4,29674,295595,1,30049,295595,50,30051,295595,40,30051,295595,40,30051,295744,0,30052,297674,50,30071,297674,30,30071,297674,40,30071,297749,0,30071,297897,50,30072,297972,0,30076,298153,50,30077,298153,30,30077,298153,40,30077,298228,0,30077,298409,50,30077,298484,0,30083,298703,50,30084,298703,30,30084,298703,40,30084,298778,0,30084,298973,50,30086,298973,30,30086,298973,40,30086,299048,0,30091,299258,50,30092,299258,30,30092,299258,40,30092,299333,0,30093,299554,50,30095,299629,0,30099,299905,50,30103,299980,0,30103,300267,50,30109,300342,0,30115,300654,50,30126,300729,0,30126,301047,50,30141,301122,0,30145,301448,50,30168,301523,0,30168,301858,50,30209,301858,40,30209,301933,0,30213,302241,50,30214,302241,30,30214,302241,40,30214,302316,0,30214,302537,50,30216,302612,0,30220,302888,50,30225,302963,0,30225,303250,50,30232,303325,0,30237,303637,50,30248,303712,0,30248,304030,50,30264,304105,0,30268,304431,50,30292,304506,0,30292,304841,50,30333,304841,40,30333,304916,0,30338,305414,50,30341,305414,30,30341,305414,40,30341,305489,0,30341,305710,50,30343,305785,0,30348,306061,50,30352,306136,0,30353,306423,50,30360,306498,0,30364,306810,50,30376,306885,0,30376,307203,50,30391,307278,0,30395,307604,50,30419,307679,0,30419,308014,50,30462,308014,40,30462,308089,0,30466)
%
%
% START OF PROOF
% 307971 [?] ?
% 308016 [] equal(multiply(identity,X),X).
% 308017 [] equal(multiply(inverse(X),X),identity).
% 308018 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 308019 [] -equal(multiply(sk_c9,sk_c11),sk_c10).
% 308061 [?] ?
% 308062 [?] ?
% 308064 [?] ?
% 308065 [?] ?
% 308066 [?] ?
% 308067 [?] ?
% 308068 [?] ?
% 308069 [?] ?
% 308181 [input:308061,cut:308019] equal(inverse(sk_c6),sk_c8).
% 308182 [para:308181.1.1,308017.1.1.1] equal(multiply(sk_c8,sk_c6),identity).
% 308184 [input:308062,cut:308019] equal(inverse(sk_c7),sk_c6).
% 308185 [para:308184.1.1,308017.1.1.1] equal(multiply(sk_c6,sk_c7),identity).
% 308186 [input:308064,cut:308019] equal(inverse(sk_c5),sk_c8).
% 308187 [para:308186.1.1,308017.1.1.1] equal(multiply(sk_c8,sk_c5),identity).
% 308188 [input:308066,cut:308019] equal(inverse(sk_c4),sk_c10).
% 308189 [para:308188.1.1,308017.1.1.1] equal(multiply(sk_c10,sk_c4),identity).
% 308191 [input:308068,cut:308019] equal(inverse(sk_c3),sk_c11).
% 308192 [para:308191.1.1,308017.1.1.1] equal(multiply(sk_c11,sk_c3),identity).
% 308216 [input:308065,cut:308019] equal(multiply(sk_c5,sk_c8),sk_c11).
% 308219 [input:308067,cut:308019] equal(multiply(sk_c4,sk_c10),sk_c9).
% 308222 [input:308069,cut:308019] equal(multiply(sk_c3,sk_c11),sk_c10).
% 308268 [para:308182.1.1,308018.1.1.1,demod:308016] equal(X,multiply(sk_c8,multiply(sk_c6,X))).
% 308271 [para:308185.1.1,308018.1.1.1,demod:308016] equal(X,multiply(sk_c6,multiply(sk_c7,X))).
% 308275 [para:308189.1.1,308018.1.1.1,demod:308016] equal(X,multiply(sk_c10,multiply(sk_c4,X))).
% 308276 [para:308192.1.1,308018.1.1.1,demod:308016] equal(X,multiply(sk_c11,multiply(sk_c3,X))).
% 308297 [para:308216.1.1,308018.1.1.1] equal(multiply(sk_c11,X),multiply(sk_c5,multiply(sk_c8,X))).
% 308316 [para:308185.1.1,308268.1.2.2] equal(sk_c7,multiply(sk_c8,identity)).
% 308317 [para:308316.1.2,308018.1.1.1,demod:308016] equal(multiply(sk_c7,X),multiply(sk_c8,X)).
% 308340 [para:308219.1.1,308275.1.2.2] equal(sk_c10,multiply(sk_c10,sk_c9)).
% 308347 [para:308222.1.1,308276.1.2.2] equal(sk_c11,multiply(sk_c11,sk_c10)).
% 308350 [para:308317.1.1,308271.1.2.2] equal(X,multiply(sk_c6,multiply(sk_c8,X))).
% 308354 [para:308182.1.1,308350.1.2.2] equal(sk_c6,multiply(sk_c6,identity)).
% 308356 [para:308187.1.1,308350.1.2.2,demod:308354] equal(sk_c5,sk_c6).
% 308363 [para:308356.1.2,308271.1.2.1,demod:308297,308317] equal(X,multiply(sk_c11,X)).
% 308374 [para:308363.1.2,308347.1.2] equal(sk_c11,sk_c10).
% 308423 [para:308374.1.2,308340.1.2.1,demod:308363] equal(sk_c10,sk_c9).
% 308447 [para:308423.1.1,308019.1.2,cut:307971] 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: 40703
% derived clauses: 3225683
% kept clauses: 162533
% kept size sum: 237097
% kept mid-nuclei: 81142
% kept new demods: 5965
% forw unit-subs: 915380
% forw double-subs: 1846850
% forw overdouble-subs: 149962
% backward subs: 21541
% fast unit cutoff: 28422
% full unit cutoff: 0
% dbl unit cutoff: 24427
% real runtime : 305.89
% process. runtime: 304.67
% specific non-discr-tree subsumption statistics:
% tried: 30785709
% length fails: 5039454
% strength fails: 7370621
% predlist fails: 823633
% aux str. fails: 1672067
% by-lit fails: 6921986
% full subs tried: 4785784
% full subs fail: 4730991
%
% ; 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/GRP350-1+eq_r.in")
%
%------------------------------------------------------------------------------