%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP377-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 : art06.cs.miami.edu
% Model : i686 unknown
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 1000MB
% OS : Linux 2.4.22-21mdk-i686-up-4GB
% CPULimit : 600s
% Result : Unsatisfiable 298.7s
% Output : Assurance 298.7s
% 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/GRP377-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 27)
% (binary-unit 12 #f)
% (binary-unit-uniteq 12 #f)
% (binary-posweight-kb-big-order 60 #f 3 27)
% (binary-posweight-lex-big-order 30 #f 3 27)
% (binary 30 #t)
% (binary-posweight-kb-big-order 156 #f)
% (binary-posweight-lex-big-order 102 #f)
% (binary-posweight-firstpref-order 60 #f)
% (binary-order 30 #f)
% (binary-posweight-kb-small-order 48 #f)
% (binary-posweight-lex-small-order 30 #f)
%
%
% SOS clause
% -equal(inverse(sk_c10),sk_c9) | -equal(multiply(X,sk_c10),sk_c9) | -equal(inverse(X),sk_c10) | -equal(multiply(sk_c8,sk_c9),sk_c10) | -equal(multiply(Y,sk_c10),sk_c9) | -equal(inverse(Y),sk_c10) | -equal(multiply(Z,sk_c9),sk_c8) | -equal(inverse(Z),sk_c9) | -equal(multiply(U,V),sk_c10) | -equal(inverse(U),V) | -equal(multiply(V,sk_c9),sk_c10) | -equal(inverse(W),X1) | -equal(inverse(X1),V) | -equal(multiply(W,V),X1).
% was split for some strategies as:
% -equal(multiply(U,V),sk_c10) | -equal(inverse(U),V) | -equal(multiply(V,sk_c9),sk_c10) | -equal(inverse(X1),V) | -equal(inverse(W),X1) | -equal(multiply(W,V),X1).
% -equal(multiply(Z,sk_c9),sk_c8) | -equal(inverse(Z),sk_c9).
% -equal(multiply(Y,sk_c10),sk_c9) | -equal(inverse(Y),sk_c10).
% -equal(multiply(X,sk_c10),sk_c9) | -equal(inverse(X),sk_c10).
% -equal(inverse(sk_c10),sk_c9).
% -equal(multiply(sk_c8,sk_c9),sk_c10).
%
% Starting a split proof attempt with 6 components.
%
% Split component 1 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(inverse(sk_c10),sk_c9) | -equal(multiply(X,sk_c10),sk_c9) | -equal(inverse(X),sk_c10) | -equal(multiply(sk_c8,sk_c9),sk_c10) | -equal(multiply(Y,sk_c10),sk_c9) | -equal(inverse(Y),sk_c10) | -equal(multiply(Z,sk_c9),sk_c8) | -equal(inverse(Z),sk_c9) | -equal(multiply(U,V),sk_c10) | -equal(inverse(U),V) | -equal(multiply(V,sk_c9),sk_c10) | -equal(inverse(W),X1) | -equal(inverse(X1),V) | -equal(multiply(W,V),X1).
% Split part used next: -equal(multiply(U,V),sk_c10) | -equal(inverse(U),V) | -equal(multiply(V,sk_c9),sk_c10) | -equal(inverse(X1),V) | -equal(inverse(W),X1) | -equal(multiply(W,V),X1).
% END OF PROOFPART
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(45,40,1,98,0,1,163757,5,1502,163757,1,1502,163757,50,1502,163757,40,1502,163810,0,1502,172303,3,1813,173235,4,1953,174147,5,2103,174148,1,2103,174148,50,2103,174148,40,2103,174201,0,2103,176092,3,2404,176129,4,2569,176165,5,2704,176165,1,2704,176165,50,2704,176165,40,2704,176218,0,2704,204227,3,4205,205146,4,4955,205955,5,5705,205956,1,5705,205956,50,5706,205956,40,5706,206009,0,5706,224419,3,6457,225101,4,6832,225654,1,7207,225654,50,7207,225654,40,7207,225707,0,7207,240667,3,7991,241970,4,8333,243514,5,8708,243515,1,8708,243515,50,8708,243515,40,8708,243568,0,8708,312103,3,12610,312799,4,14560,313609,5,16509,313610,1,16509,313610,50,16511,313610,40,16511,313663,0,16511,368521,3,19062,369093,4,20337,369543,5,21612,369544,1,21612,369544,50,21614,369544,40,21614,369597,0,21614,410976,3,23118,411660,4,23865,412481,5,24615,412482,1,24615,412482,50,24616,412482,40,24616,412535,0,24616,424468,3,25377,426322,4,25742,428440,5,26117,428441,1,26117,428441,50,26117,428441,40,26117,428494,0,26117,461245,3,27321,461800,4,27918,462255,5,28518,462256,1,28518,462256,50,28519,462256,40,28519,462309,0,28519,491373,3,29270,491809,4,29645,492180,5,30020,492181,1,30020,492181,50,30021,492181,40,30021,492181,40,30021,492270,0,30021)
%
%
% START OF PROOF
% 492182 [] equal(X,X).
% 492183 [] equal(multiply(identity,X),X).
% 492184 [] equal(multiply(inverse(X),X),identity).
% 492185 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 492226 [] -equal(multiply(X,sk_c9),sk_c10) | -equal(multiply(Y,X),sk_c10) | -equal(multiply(Z,X),U) | -equal(inverse(Z),U) | -equal(inverse(U),X) | -equal(inverse(Y),X).
% 492227 [] -equal(multiply(X,Y),Z) | -equal(inverse(X),Z) | -equal(inverse(Z),Y) | $spltprd1($spltcnst85,Y).
% 492228 [] -equal(multiply(X,Y),sk_c10) | -equal(inverse(X),Y) | $spltprd1($spltcnst86,Y).
% 492229 [] -equal(multiply(X,sk_c9),sk_c10) | $spltprd1($spltcnst87,X).
% 492230 [] -$spltprd1($spltcnst86,X) | -$spltprd1($spltcnst85,X) | -$spltprd1($spltcnst87,X).
% 492241 [] equal(multiply(sk_c6,sk_c7),sk_c5) | equal(inverse(sk_c1),sk_c10).
% 492242 [] equal(inverse(sk_c1),sk_c10) | equal(inverse(sk_c5),sk_c7).
% 492243 [] equal(inverse(sk_c1),sk_c10) | equal(inverse(sk_c6),sk_c5).
% 492244 [] equal(multiply(sk_c7,sk_c9),sk_c10) | equal(inverse(sk_c1),sk_c10).
% 492245 [] equal(inverse(sk_c1),sk_c10) | equal(inverse(sk_c4),sk_c7).
% 492246 [?] ?
% 492251 [] equal(multiply(sk_c1,sk_c10),sk_c9) | equal(multiply(sk_c6,sk_c7),sk_c5).
% 492252 [] equal(multiply(sk_c1,sk_c10),sk_c9) | equal(inverse(sk_c5),sk_c7).
% 492253 [] equal(multiply(sk_c1,sk_c10),sk_c9) | equal(inverse(sk_c6),sk_c5).
% 492254 [] equal(multiply(sk_c1,sk_c10),sk_c9) | equal(multiply(sk_c7,sk_c9),sk_c10).
% 492255 [] equal(multiply(sk_c1,sk_c10),sk_c9) | equal(inverse(sk_c4),sk_c7).
% 492256 [] equal(multiply(sk_c1,sk_c10),sk_c9) | equal(multiply(sk_c4,sk_c7),sk_c10).
% 492261 [] equal(multiply(sk_c6,sk_c7),sk_c5) | equal(inverse(sk_c10),sk_c9).
% 492262 [] equal(inverse(sk_c10),sk_c9) | equal(inverse(sk_c5),sk_c7).
% 492263 [] equal(inverse(sk_c10),sk_c9) | equal(inverse(sk_c6),sk_c5).
% 492264 [] equal(multiply(sk_c7,sk_c9),sk_c10) | equal(inverse(sk_c10),sk_c9).
% 492265 [] equal(inverse(sk_c10),sk_c9) | equal(inverse(sk_c4),sk_c7).
% 492266 [?] ?
% 492337 [hyper:492228,492245,binarycut:492246] equal(inverse(sk_c1),sk_c10) | $spltprd1($spltcnst86,sk_c7).
% 492425 [hyper:492228,492265,binarycut:492266] equal(inverse(sk_c10),sk_c9) | $spltprd1($spltcnst86,sk_c7).
% 492639 [hyper:492227,492241,492242,492243] equal(inverse(sk_c1),sk_c10) | $spltprd1($spltcnst85,sk_c7).
% 492660 [hyper:492229,492244] equal(inverse(sk_c1),sk_c10) | $spltprd1($spltcnst87,sk_c7).
% 492694 [hyper:492230,492660,492639,492337] equal(inverse(sk_c1),sk_c10).
% 492706 [para:492694.1.1,492184.1.1.1] equal(multiply(sk_c10,sk_c1),identity).
% 492810 [hyper:492227,492261,492262,492263] equal(inverse(sk_c10),sk_c9) | $spltprd1($spltcnst85,sk_c7).
% 492908 [hyper:492229,492264] equal(inverse(sk_c10),sk_c9) | $spltprd1($spltcnst87,sk_c7).
% 492944 [hyper:492230,492908,492810,492425] equal(inverse(sk_c10),sk_c9).
% 492974 [para:492944.1.1,492184.1.1.1] equal(multiply(sk_c9,sk_c10),identity).
% 493304 [hyper:492226,492256,492254,492255,492252,492251,492253] equal(multiply(sk_c1,sk_c10),sk_c9).
% 493313 [para:492706.1.1,492185.1.1.1,demod:492183] equal(X,multiply(sk_c10,multiply(sk_c1,X))).
% 493314 [para:492974.1.1,492185.1.1.1,demod:492183] equal(X,multiply(sk_c9,multiply(sk_c10,X))).
% 493333 [para:493304.1.1,493313.1.2.2] equal(sk_c10,multiply(sk_c10,sk_c9)).
% 493353 [para:493333.1.2,493314.1.2.2,demod:492974] equal(sk_c9,identity).
% 493354 [para:493353.1.1,492974.1.1.1,demod:492183] equal(sk_c10,identity).
% 493358 [para:493354.1.1,492706.1.1.1,demod:492183] equal(sk_c1,identity).
% 493359 [para:493354.1.1,492944.1.1.1] equal(inverse(identity),sk_c9).
% 493362 [para:493354.1.1,493333.1.2.1,demod:492183] equal(sk_c10,sk_c9).
% 493363 [para:493358.1.1,492694.1.1.1,demod:493359] equal(sk_c9,sk_c10).
% 493364 [para:493362.1.1,492944.1.1.1] equal(inverse(sk_c9),sk_c9).
% 493375 [hyper:492226,493359,492183,demod:493364,492183,demod:493359,493333,cut:492182,cut:493363,cut:493363,cut:493362] 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 27
% 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(inverse(sk_c10),sk_c9) | -equal(multiply(X,sk_c10),sk_c9) | -equal(inverse(X),sk_c10) | -equal(multiply(sk_c8,sk_c9),sk_c10) | -equal(multiply(Y,sk_c10),sk_c9) | -equal(inverse(Y),sk_c10) | -equal(multiply(Z,sk_c9),sk_c8) | -equal(inverse(Z),sk_c9) | -equal(multiply(U,V),sk_c10) | -equal(inverse(U),V) | -equal(multiply(V,sk_c9),sk_c10) | -equal(inverse(W),X1) | -equal(inverse(X1),V) | -equal(multiply(W,V),X1).
% Split part used next: -equal(multiply(Z,sk_c9),sk_c8) | -equal(inverse(Z),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 27
% 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 27
% 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 27
% clause depth limited to 5
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(45,40,1,98,0,1,163757,5,1502,163757,1,1502,163757,50,1502,163757,40,1502,163810,0,1502,172303,3,1813,173235,4,1953,174147,5,2103,174148,1,2103,174148,50,2103,174148,40,2103,174201,0,2103,176092,3,2404,176129,4,2569,176165,5,2704,176165,1,2704,176165,50,2704,176165,40,2704,176218,0,2704,204227,3,4205,205146,4,4955,205955,5,5705,205956,1,5705,205956,50,5706,205956,40,5706,206009,0,5706,224419,3,6457,225101,4,6832,225654,1,7207,225654,50,7207,225654,40,7207,225707,0,7207,240667,3,7991,241970,4,8333,243514,5,8708,243515,1,8708,243515,50,8708,243515,40,8708,243568,0,8708,312103,3,12610,312799,4,14560,313609,5,16509,313610,1,16509,313610,50,16511,313610,40,16511,313663,0,16511,368521,3,19062,369093,4,20337,369543,5,21612,369544,1,21612,369544,50,21614,369544,40,21614,369597,0,21614,410976,3,23118,411660,4,23865,412481,5,24615,412482,1,24615,412482,50,24616,412482,40,24616,412535,0,24616,424468,3,25377,426322,4,25742,428440,5,26117,428441,1,26117,428441,50,26117,428441,40,26117,428494,0,26117,461245,3,27321,461800,4,27918,462255,5,28518,462256,1,28518,462256,50,28519,462256,40,28519,462309,0,28519,491373,3,29270,491809,4,29645,492180,5,30020,492181,1,30020,492181,50,30021,492181,40,30021,492181,40,30021,492270,0,30021,493374,50,30024,493374,30,30024,493374,40,30024,493419,0,30024,493509,50,30024,493554,0,30030,493682,50,30031,493727,0,30032)
%
%
% START OF PROOF
% 493664 [?] ?
% 493684 [] equal(multiply(identity,X),X).
% 493685 [] equal(multiply(inverse(X),X),identity).
% 493686 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 493687 [] -equal(multiply(X,sk_c9),sk_c8) | -equal(inverse(X),sk_c9).
% 493704 [] equal(inverse(sk_c1),sk_c10) | equal(inverse(sk_c3),sk_c9).
% 493705 [?] ?
% 493714 [] equal(multiply(sk_c1,sk_c10),sk_c9) | equal(inverse(sk_c3),sk_c9).
% 493715 [] equal(multiply(sk_c1,sk_c10),sk_c9) | equal(multiply(sk_c3,sk_c9),sk_c8).
% 493724 [] equal(inverse(sk_c10),sk_c9) | equal(inverse(sk_c3),sk_c9).
% 493725 [?] ?
% 493734 [hyper:493687,493704,binarycut:493705] equal(inverse(sk_c1),sk_c10).
% 493735 [para:493734.1.1,493685.1.1.1] equal(multiply(sk_c10,sk_c1),identity).
% 493749 [hyper:493687,493724,binarycut:493725] equal(inverse(sk_c10),sk_c9).
% 493752 [para:493749.1.1,493685.1.1.1] equal(multiply(sk_c9,sk_c10),identity).
% 493778 [hyper:493687,493715,493714] equal(multiply(sk_c1,sk_c10),sk_c9).
% 493779 [para:493685.1.1,493686.1.1.1,demod:493684] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 493780 [para:493735.1.1,493686.1.1.1,demod:493684] equal(X,multiply(sk_c10,multiply(sk_c1,X))).
% 493784 [para:493778.1.1,493780.1.2.2] equal(sk_c10,multiply(sk_c10,sk_c9)).
% 493793 [para:493784.1.2,493779.1.2.2,demod:493752,493749] equal(sk_c9,identity).
% 493795 [para:493793.1.1,493752.1.1.1,demod:493684] equal(sk_c10,identity).
% 493799 [para:493795.1.1,493749.1.1.1] equal(inverse(identity),sk_c9).
% 493807 [hyper:493687,493799,demod:493684,cut:493664] 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 27
% clause depth limited to 5
% seconds given: 4
%
%
% Split component 3 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(inverse(sk_c10),sk_c9) | -equal(multiply(X,sk_c10),sk_c9) | -equal(inverse(X),sk_c10) | -equal(multiply(sk_c8,sk_c9),sk_c10) | -equal(multiply(Y,sk_c10),sk_c9) | -equal(inverse(Y),sk_c10) | -equal(multiply(Z,sk_c9),sk_c8) | -equal(inverse(Z),sk_c9) | -equal(multiply(U,V),sk_c10) | -equal(inverse(U),V) | -equal(multiply(V,sk_c9),sk_c10) | -equal(inverse(W),X1) | -equal(inverse(X1),V) | -equal(multiply(W,V),X1).
% Split part used next: -equal(multiply(Y,sk_c10),sk_c9) | -equal(inverse(Y),sk_c10).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 27
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(45,40,1,98,0,1,163757,5,1502,163757,1,1502,163757,50,1502,163757,40,1502,163810,0,1502,172303,3,1813,173235,4,1953,174147,5,2103,174148,1,2103,174148,50,2103,174148,40,2103,174201,0,2103,176092,3,2404,176129,4,2569,176165,5,2704,176165,1,2704,176165,50,2704,176165,40,2704,176218,0,2704,204227,3,4205,205146,4,4955,205955,5,5705,205956,1,5705,205956,50,5706,205956,40,5706,206009,0,5706,224419,3,6457,225101,4,6832,225654,1,7207,225654,50,7207,225654,40,7207,225707,0,7207,240667,3,7991,241970,4,8333,243514,5,8708,243515,1,8708,243515,50,8708,243515,40,8708,243568,0,8708,312103,3,12610,312799,4,14560,313609,5,16509,313610,1,16509,313610,50,16511,313610,40,16511,313663,0,16511,368521,3,19062,369093,4,20337,369543,5,21612,369544,1,21612,369544,50,21614,369544,40,21614,369597,0,21614,410976,3,23118,411660,4,23865,412481,5,24615,412482,1,24615,412482,50,24616,412482,40,24616,412535,0,24616,424468,3,25377,426322,4,25742,428440,5,26117,428441,1,26117,428441,50,26117,428441,40,26117,428494,0,26117,461245,3,27321,461800,4,27918,462255,5,28518,462256,1,28518,462256,50,28519,462256,40,28519,462309,0,28519,491373,3,29270,491809,4,29645,492180,5,30020,492181,1,30020,492181,50,30021,492181,40,30021,492181,40,30021,492270,0,30021,493374,50,30024,493374,30,30024,493374,40,30024,493419,0,30024,493509,50,30024,493554,0,30030,493682,50,30031,493727,0,30032,493806,50,30032,493806,30,30032,493806,40,30032,493851,0,30032)
%
%
% START OF PROOF
% 493807 [] equal(X,X).
% 493811 [] -equal(multiply(X,sk_c10),sk_c9) | -equal(inverse(X),sk_c10).
% 493830 [] equal(inverse(sk_c1),sk_c10) | equal(inverse(sk_c2),sk_c10).
% 493831 [?] ?
% 493840 [?] ?
% 493841 [] equal(multiply(sk_c1,sk_c10),sk_c9) | equal(multiply(sk_c2,sk_c10),sk_c9).
% 493873 [hyper:493811,493830,binarycut:493840] equal(inverse(sk_c2),sk_c10).
% 493875 [hyper:493811,493830,binarycut:493831] equal(inverse(sk_c1),sk_c10).
% 493902 [hyper:493811,493841,demod:493875,cut:493807] equal(multiply(sk_c2,sk_c10),sk_c9).
% 493904 [hyper:493811,493902,demod:493873,cut:493807] 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 27
% 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(inverse(sk_c10),sk_c9) | -equal(multiply(X,sk_c10),sk_c9) | -equal(inverse(X),sk_c10) | -equal(multiply(sk_c8,sk_c9),sk_c10) | -equal(multiply(Y,sk_c10),sk_c9) | -equal(inverse(Y),sk_c10) | -equal(multiply(Z,sk_c9),sk_c8) | -equal(inverse(Z),sk_c9) | -equal(multiply(U,V),sk_c10) | -equal(inverse(U),V) | -equal(multiply(V,sk_c9),sk_c10) | -equal(inverse(W),X1) | -equal(inverse(X1),V) | -equal(multiply(W,V),X1).
% Split part used next: -equal(multiply(X,sk_c10),sk_c9) | -equal(inverse(X),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 27
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(45,40,1,98,0,1,163757,5,1502,163757,1,1502,163757,50,1502,163757,40,1502,163810,0,1502,172303,3,1813,173235,4,1953,174147,5,2103,174148,1,2103,174148,50,2103,174148,40,2103,174201,0,2103,176092,3,2404,176129,4,2569,176165,5,2704,176165,1,2704,176165,50,2704,176165,40,2704,176218,0,2704,204227,3,4205,205146,4,4955,205955,5,5705,205956,1,5705,205956,50,5706,205956,40,5706,206009,0,5706,224419,3,6457,225101,4,6832,225654,1,7207,225654,50,7207,225654,40,7207,225707,0,7207,240667,3,7991,241970,4,8333,243514,5,8708,243515,1,8708,243515,50,8708,243515,40,8708,243568,0,8708,312103,3,12610,312799,4,14560,313609,5,16509,313610,1,16509,313610,50,16511,313610,40,16511,313663,0,16511,368521,3,19062,369093,4,20337,369543,5,21612,369544,1,21612,369544,50,21614,369544,40,21614,369597,0,21614,410976,3,23118,411660,4,23865,412481,5,24615,412482,1,24615,412482,50,24616,412482,40,24616,412535,0,24616,424468,3,25377,426322,4,25742,428440,5,26117,428441,1,26117,428441,50,26117,428441,40,26117,428494,0,26117,461245,3,27321,461800,4,27918,462255,5,28518,462256,1,28518,462256,50,28519,462256,40,28519,462309,0,28519,491373,3,29270,491809,4,29645,492180,5,30020,492181,1,30020,492181,50,30021,492181,40,30021,492181,40,30021,492270,0,30021,493374,50,30024,493374,30,30024,493374,40,30024,493419,0,30024,493509,50,30024,493554,0,30030,493682,50,30031,493727,0,30032,493806,50,30032,493806,30,30032,493806,40,30032,493851,0,30032,493903,50,30032,493903,30,30032,493903,40,30032,493948,0,30037)
%
%
% START OF PROOF
% 493904 [] equal(X,X).
% 493908 [] -equal(multiply(X,sk_c10),sk_c9) | -equal(inverse(X),sk_c10).
% 493927 [] equal(inverse(sk_c1),sk_c10) | equal(inverse(sk_c2),sk_c10).
% 493928 [?] ?
% 493937 [?] ?
% 493938 [] equal(multiply(sk_c1,sk_c10),sk_c9) | equal(multiply(sk_c2,sk_c10),sk_c9).
% 493970 [hyper:493908,493927,binarycut:493937] equal(inverse(sk_c2),sk_c10).
% 493972 [hyper:493908,493927,binarycut:493928] equal(inverse(sk_c1),sk_c10).
% 493999 [hyper:493908,493938,demod:493972,cut:493904] equal(multiply(sk_c2,sk_c10),sk_c9).
% 494001 [hyper:493908,493999,demod:493970,cut:493904] 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 27
% clause depth limited to 3
% seconds given: 4
%
%
% Split component 5 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(inverse(sk_c10),sk_c9) | -equal(multiply(X,sk_c10),sk_c9) | -equal(inverse(X),sk_c10) | -equal(multiply(sk_c8,sk_c9),sk_c10) | -equal(multiply(Y,sk_c10),sk_c9) | -equal(inverse(Y),sk_c10) | -equal(multiply(Z,sk_c9),sk_c8) | -equal(inverse(Z),sk_c9) | -equal(multiply(U,V),sk_c10) | -equal(inverse(U),V) | -equal(multiply(V,sk_c9),sk_c10) | -equal(inverse(W),X1) | -equal(inverse(X1),V) | -equal(multiply(W,V),X1).
% 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 27
% 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 27
% 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 27
% 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 27
% 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 27
% 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 27
% 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 27
% 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 27
% 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 27
% 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(45,40,1,98,0,1,163757,5,1502,163757,1,1502,163757,50,1502,163757,40,1502,163810,0,1502,172303,3,1813,173235,4,1953,174147,5,2103,174148,1,2103,174148,50,2103,174148,40,2103,174201,0,2103,176092,3,2404,176129,4,2569,176165,5,2704,176165,1,2704,176165,50,2704,176165,40,2704,176218,0,2704,204227,3,4205,205146,4,4955,205955,5,5705,205956,1,5705,205956,50,5706,205956,40,5706,206009,0,5706,224419,3,6457,225101,4,6832,225654,1,7207,225654,50,7207,225654,40,7207,225707,0,7207,240667,3,7991,241970,4,8333,243514,5,8708,243515,1,8708,243515,50,8708,243515,40,8708,243568,0,8708,312103,3,12610,312799,4,14560,313609,5,16509,313610,1,16509,313610,50,16511,313610,40,16511,313663,0,16511,368521,3,19062,369093,4,20337,369543,5,21612,369544,1,21612,369544,50,21614,369544,40,21614,369597,0,21614,410976,3,23118,411660,4,23865,412481,5,24615,412482,1,24615,412482,50,24616,412482,40,24616,412535,0,24616,424468,3,25377,426322,4,25742,428440,5,26117,428441,1,26117,428441,50,26117,428441,40,26117,428494,0,26117,461245,3,27321,461800,4,27918,462255,5,28518,462256,1,28518,462256,50,28519,462256,40,28519,462309,0,28519,491373,3,29270,491809,4,29645,492180,5,30020,492181,1,30020,492181,50,30021,492181,40,30021,492181,40,30021,492270,0,30021,493374,50,30024,493374,30,30024,493374,40,30024,493419,0,30024,493509,50,30024,493554,0,30030,493682,50,30031,493727,0,30032,493806,50,30032,493806,30,30032,493806,40,30032,493851,0,30032,493903,50,30032,493903,30,30032,493903,40,30032,493948,0,30037,494000,50,30038,494000,30,30038,494000,40,30038,494045,0,30038,494237,50,30039,494282,0,30045,494537,50,30050,494582,0,30050,494845,50,30056,494890,0,30056,495161,50,30065,495206,0,30070,495483,50,30082,495528,0,30082,495813,50,30103,495858,0,30108,496151,50,30143,496196,0,30143,496499,50,30214,496544,0,30214,496857,50,30345,496857,40,30345,496902,0,30345)
%
%
% START OF PROOF
% 496859 [] equal(multiply(identity,X),X).
% 496860 [] equal(multiply(inverse(X),X),identity).
% 496861 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 496862 [] -equal(inverse(sk_c10),sk_c9).
% 496893 [?] ?
% 496894 [?] ?
% 496895 [?] ?
% 496896 [?] ?
% 496897 [?] ?
% 496898 [?] ?
% 496899 [?] ?
% 496900 [?] ?
% 496901 [?] ?
% 496902 [?] ?
% 496919 [input:496894,cut:496862] equal(inverse(sk_c5),sk_c7).
% 496920 [para:496919.1.1,496860.1.1.1] equal(multiply(sk_c7,sk_c5),identity).
% 496922 [input:496895,cut:496862] equal(inverse(sk_c6),sk_c5).
% 496923 [para:496922.1.1,496860.1.1.1] equal(multiply(sk_c5,sk_c6),identity).
% 496924 [input:496897,cut:496862] equal(inverse(sk_c4),sk_c7).
% 496925 [para:496924.1.1,496860.1.1.1] equal(multiply(sk_c7,sk_c4),identity).
% 496927 [input:496899,cut:496862] equal(inverse(sk_c3),sk_c9).
% 496928 [para:496927.1.1,496860.1.1.1] equal(multiply(sk_c9,sk_c3),identity).
% 496929 [input:496901,cut:496862] equal(inverse(sk_c2),sk_c10).
% 496930 [para:496929.1.1,496860.1.1.1] equal(multiply(sk_c10,sk_c2),identity).
% 496952 [input:496893,cut:496862] equal(multiply(sk_c6,sk_c7),sk_c5).
% 496954 [input:496896,cut:496862] equal(multiply(sk_c7,sk_c9),sk_c10).
% 496956 [input:496898,cut:496862] equal(multiply(sk_c4,sk_c7),sk_c10).
% 496957 [input:496900,cut:496862] equal(multiply(sk_c3,sk_c9),sk_c8).
% 496958 [input:496902,cut:496862] equal(multiply(sk_c2,sk_c10),sk_c9).
% 496972 [para:496920.1.1,496861.1.1.1,demod:496859] equal(X,multiply(sk_c7,multiply(sk_c5,X))).
% 496973 [para:496923.1.1,496861.1.1.1,demod:496859] equal(X,multiply(sk_c5,multiply(sk_c6,X))).
% 496974 [para:496925.1.1,496861.1.1.1,demod:496859] equal(X,multiply(sk_c7,multiply(sk_c4,X))).
% 496976 [para:496928.1.1,496861.1.1.1,demod:496859] equal(X,multiply(sk_c9,multiply(sk_c3,X))).
% 496977 [para:496930.1.1,496861.1.1.1,demod:496859] equal(X,multiply(sk_c10,multiply(sk_c2,X))).
% 497002 [para:496956.1.1,496861.1.1.1] equal(multiply(sk_c10,X),multiply(sk_c4,multiply(sk_c7,X))).
% 497014 [para:496923.1.1,496972.1.2.2] equal(sk_c6,multiply(sk_c7,identity)).
% 497015 [para:497014.1.2,496861.1.1.1,demod:496859] equal(multiply(sk_c6,X),multiply(sk_c7,X)).
% 497018 [para:496952.1.1,496973.1.2.2] equal(sk_c7,multiply(sk_c5,sk_c5)).
% 497021 [para:497018.1.2,496972.1.2.2] equal(sk_c5,multiply(sk_c7,sk_c7)).
% 497026 [para:496956.1.1,496974.1.2.2] equal(sk_c7,multiply(sk_c7,sk_c10)).
% 497030 [para:496957.1.1,496976.1.2.2] equal(sk_c9,multiply(sk_c9,sk_c8)).
% 497034 [para:496958.1.1,496977.1.2.2] equal(sk_c10,multiply(sk_c10,sk_c9)).
% 497038 [para:497015.1.1,496973.1.2.2] equal(X,multiply(sk_c5,multiply(sk_c7,X))).
% 497039 [para:496920.1.1,497038.1.2.2] equal(sk_c5,multiply(sk_c5,identity)).
% 497040 [para:496925.1.1,497038.1.2.2,demod:497039] equal(sk_c4,sk_c5).
% 497048 [para:497040.1.2,496973.1.2.1,demod:497002,497015] equal(X,multiply(sk_c10,X)).
% 497057 [para:497048.1.2,496977.1.2] equal(X,multiply(sk_c2,X)).
% 497059 [para:497048.1.2,497034.1.2] equal(sk_c10,sk_c9).
% 497078 [para:497059.1.1,497026.1.2.2] equal(sk_c7,multiply(sk_c7,sk_c9)).
% 497079 [para:497059.1.1,496977.1.2.1,demod:497057] equal(X,multiply(sk_c9,X)).
% 497085 [para:497079.1.2,497030.1.2] equal(sk_c9,sk_c8).
% 497141 [para:497085.1.1,496954.1.1.2] equal(multiply(sk_c7,sk_c8),sk_c10).
% 497143 [para:497085.1.1,497034.1.2.2,demod:497048] equal(sk_c10,sk_c8).
% 497156 [para:497143.1.1,497026.1.2.2,demod:497141] equal(sk_c7,sk_c10).
% 497164 [para:497156.1.2,496958.1.1.2,demod:497057] equal(sk_c7,sk_c9).
% 497169 [para:497156.1.2,497026.1.2.2,demod:497021] equal(sk_c7,sk_c5).
% 497171 [para:497156.1.2,497034.1.2.1,demod:497078] equal(sk_c10,sk_c7).
% 497181 [para:497169.1.2,496919.1.1.1] equal(inverse(sk_c7),sk_c7).
% 497187 [para:497171.1.1,496862.1.1.1,demod:497181,cut:497164] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% Split component 6 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(inverse(sk_c10),sk_c9) | -equal(multiply(X,sk_c10),sk_c9) | -equal(inverse(X),sk_c10) | -equal(multiply(sk_c8,sk_c9),sk_c10) | -equal(multiply(Y,sk_c10),sk_c9) | -equal(inverse(Y),sk_c10) | -equal(multiply(Z,sk_c9),sk_c8) | -equal(inverse(Z),sk_c9) | -equal(multiply(U,V),sk_c10) | -equal(inverse(U),V) | -equal(multiply(V,sk_c9),sk_c10) | -equal(inverse(W),X1) | -equal(inverse(X1),V) | -equal(multiply(W,V),X1).
% Split part used next: -equal(multiply(sk_c8,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 27
% 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 27
% 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 27
% 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 27
% 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 27
% 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 27
% 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 27
% 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 27
% 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 27
% 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(45,40,1,98,0,1,163757,5,1502,163757,1,1502,163757,50,1502,163757,40,1502,163810,0,1502,172303,3,1813,173235,4,1953,174147,5,2103,174148,1,2103,174148,50,2103,174148,40,2103,174201,0,2103,176092,3,2404,176129,4,2569,176165,5,2704,176165,1,2704,176165,50,2704,176165,40,2704,176218,0,2704,204227,3,4205,205146,4,4955,205955,5,5705,205956,1,5705,205956,50,5706,205956,40,5706,206009,0,5706,224419,3,6457,225101,4,6832,225654,1,7207,225654,50,7207,225654,40,7207,225707,0,7207,240667,3,7991,241970,4,8333,243514,5,8708,243515,1,8708,243515,50,8708,243515,40,8708,243568,0,8708,312103,3,12610,312799,4,14560,313609,5,16509,313610,1,16509,313610,50,16511,313610,40,16511,313663,0,16511,368521,3,19062,369093,4,20337,369543,5,21612,369544,1,21612,369544,50,21614,369544,40,21614,369597,0,21614,410976,3,23118,411660,4,23865,412481,5,24615,412482,1,24615,412482,50,24616,412482,40,24616,412535,0,24616,424468,3,25377,426322,4,25742,428440,5,26117,428441,1,26117,428441,50,26117,428441,40,26117,428494,0,26117,461245,3,27321,461800,4,27918,462255,5,28518,462256,1,28518,462256,50,28519,462256,40,28519,462309,0,28519,491373,3,29270,491809,4,29645,492180,5,30020,492181,1,30020,492181,50,30021,492181,40,30021,492181,40,30021,492270,0,30021,493374,50,30024,493374,30,30024,493374,40,30024,493419,0,30024,493509,50,30024,493554,0,30030,493682,50,30031,493727,0,30032,493806,50,30032,493806,30,30032,493806,40,30032,493851,0,30032,493903,50,30032,493903,30,30032,493903,40,30032,493948,0,30037,494000,50,30038,494000,30,30038,494000,40,30038,494045,0,30038,494237,50,30039,494282,0,30045,494537,50,30050,494582,0,30050,494845,50,30056,494890,0,30056,495161,50,30065,495206,0,30070,495483,50,30082,495528,0,30082,495813,50,30103,495858,0,30108,496151,50,30143,496196,0,30143,496499,50,30214,496544,0,30214,496857,50,30345,496857,40,30345,496902,0,30345,497186,50,30346,497186,30,30346,497186,40,30346,497231,0,30346,497430,50,30349,497475,0,30353,497732,50,30358,497777,0,30358,498042,50,30365,498087,0,30365,498360,50,30374,498405,0,30379,498684,50,30392,498729,0,30392,499016,50,30413,499061,0,30418,499356,50,30454,499401,0,30454,499706,50,30528,499751,0,30528,500066,50,30661,500066,40,30661,500111,0,30661)
%
%
% START OF PROOF
% 499935 [?] ?
% 500068 [] equal(multiply(identity,X),X).
% 500069 [] equal(multiply(inverse(X),X),identity).
% 500070 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 500071 [] -equal(multiply(sk_c8,sk_c9),sk_c10).
% 500073 [?] ?
% 500074 [?] ?
% 500076 [?] ?
% 500077 [?] ?
% 500078 [?] ?
% 500079 [?] ?
% 500080 [?] ?
% 500081 [?] ?
% 500131 [input:500073,cut:500071] equal(inverse(sk_c5),sk_c7).
% 500132 [para:500131.1.1,500069.1.1.1] equal(multiply(sk_c7,sk_c5),identity).
% 500145 [input:500074,cut:500071] equal(inverse(sk_c6),sk_c5).
% 500146 [para:500145.1.1,500069.1.1.1] equal(multiply(sk_c5,sk_c6),identity).
% 500147 [input:500076,cut:500071] equal(inverse(sk_c4),sk_c7).
% 500148 [para:500147.1.1,500069.1.1.1] equal(multiply(sk_c7,sk_c4),identity).
% 500149 [input:500078,cut:500071] equal(inverse(sk_c3),sk_c9).
% 500150 [para:500149.1.1,500069.1.1.1] equal(multiply(sk_c9,sk_c3),identity).
% 500152 [input:500080,cut:500071] equal(inverse(sk_c2),sk_c10).
% 500153 [para:500152.1.1,500069.1.1.1] equal(multiply(sk_c10,sk_c2),identity).
% 500160 [input:500077,cut:500071] equal(multiply(sk_c4,sk_c7),sk_c10).
% 500168 [input:500079,cut:500071] equal(multiply(sk_c3,sk_c9),sk_c8).
% 500173 [input:500081,cut:500071] equal(multiply(sk_c2,sk_c10),sk_c9).
% 500201 [para:500132.1.1,500070.1.1.1,demod:500068] equal(X,multiply(sk_c7,multiply(sk_c5,X))).
% 500202 [para:500146.1.1,500070.1.1.1,demod:500068] equal(X,multiply(sk_c5,multiply(sk_c6,X))).
% 500204 [para:500150.1.1,500070.1.1.1,demod:500068] equal(X,multiply(sk_c9,multiply(sk_c3,X))).
% 500206 [para:500153.1.1,500070.1.1.1,demod:500068] equal(X,multiply(sk_c10,multiply(sk_c2,X))).
% 500208 [para:500160.1.1,500070.1.1.1] equal(multiply(sk_c10,X),multiply(sk_c4,multiply(sk_c7,X))).
% 500235 [para:500146.1.1,500201.1.2.2] equal(sk_c6,multiply(sk_c7,identity)).
% 500236 [para:500235.1.2,500070.1.1.1,demod:500068] equal(multiply(sk_c6,X),multiply(sk_c7,X)).
% 500250 [para:500168.1.1,500204.1.2.2] equal(sk_c9,multiply(sk_c9,sk_c8)).
% 500255 [para:500173.1.1,500206.1.2.2] equal(sk_c10,multiply(sk_c10,sk_c9)).
% 500257 [para:500236.1.1,500202.1.2.2] equal(X,multiply(sk_c5,multiply(sk_c7,X))).
% 500258 [para:500132.1.1,500257.1.2.2] equal(sk_c5,multiply(sk_c5,identity)).
% 500259 [para:500148.1.1,500257.1.2.2,demod:500258] equal(sk_c4,sk_c5).
% 500265 [para:500259.1.2,500202.1.2.1,demod:500208,500236] equal(X,multiply(sk_c10,X)).
% 500277 [para:500265.1.2,500206.1.2] equal(X,multiply(sk_c2,X)).
% 500278 [para:500265.1.2,500255.1.2] equal(sk_c10,sk_c9).
% 500308 [para:500278.1.1,500206.1.2.1,demod:500277] equal(X,multiply(sk_c9,X)).
% 500324 [para:500308.1.2,500204.1.2] equal(X,multiply(sk_c3,X)).
% 500325 [para:500308.1.2,500250.1.2] equal(sk_c9,sk_c8).
% 500326 [para:500250.1.2,500308.1.2] equal(sk_c8,sk_c9).
% 500335 [para:500325.1.1,500204.1.2.1,demod:500324] equal(X,multiply(sk_c8,X)).
% 500338 [para:500326.1.2,500071.1.1.2,demod:500335,cut:499935] 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: 32007
% derived clauses: 4461314
% kept clauses: 292226
% kept size sum: 33167
% kept mid-nuclei: 145026
% kept new demods: 5136
% forw unit-subs: 1880588
% forw double-subs: 1837743
% forw overdouble-subs: 225171
% backward subs: 12816
% fast unit cutoff: 29680
% full unit cutoff: 0
% dbl unit cutoff: 30413
% real runtime : 308.27
% process. runtime: 306.61
% specific non-discr-tree subsumption statistics:
% tried: 63072942
% length fails: 5510381
% strength fails: 17055146
% predlist fails: 5416537
% aux str. fails: 4995227
% by-lit fails: 11819857
% full subs tried: 2622453
% full subs fail: 2504374
%
% ; 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/GRP377-1+eq_r.in")
%
%------------------------------------------------------------------------------