%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP323-1 : TPTP v3.4.2. Released v2.5.0.
% Transfm : add_equality:r
% Format : otter:hypothesis:set(auto),clear(print_given)
% Command : gandalf-wrapper -time %d %s
% Computer : art07.cs.miami.edu
% Model : i686 unknown
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 1000MB
% OS : Linux 2.4.22-21mdk-i686-up-4GB
% CPULimit : 600s
% Result : Unsatisfiable 298.2s
% Output : Assurance 298.2s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----NO SOLUTION OUTPUT BY SYSTEM
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
%
% Gandalf c-2.6 r1 starting to prove: /home/graph/tptp/TSTP/PreparedTPTP/otter:hypothesis:set(auto),clear(print_given)---add_equality:r/GRP/GRP323-1+eq_r.in
% Using automatic strategy selection.
% Time limit in seconds: 600
%
% prove-all-passes started
%
% detected problem class: peq
%
% strategies selected:
% (hyper 30 #f 3 21)
% (binary-unit 12 #f)
% (binary-unit-uniteq 12 #f)
% (binary-posweight-kb-big-order 60 #f 3 21)
% (binary-posweight-lex-big-order 30 #f 3 21)
% (binary 30 #t)
% (binary-posweight-kb-big-order 156 #f)
% (binary-posweight-lex-big-order 102 #f)
% (binary-posweight-firstpref-order 60 #f)
% (binary-order 30 #f)
% (binary-posweight-kb-small-order 48 #f)
% (binary-posweight-lex-small-order 30 #f)
%
%
% SOS clause
% -equal(multiply(sk_c7,sk_c8),sk_c6) | -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7) | -equal(multiply(sk_c8,Y),sk_c7) | -equal(multiply(Z,sk_c8),Y) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c8,sk_c7),sk_c6) | -equal(multiply(U,sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(V,sk_c8),sk_c6) | -equal(inverse(V),sk_c8).
% was split for some strategies as:
% -equal(multiply(V,sk_c8),sk_c6) | -equal(inverse(V),sk_c8).
% -equal(multiply(U,sk_c8),sk_c7) | -equal(inverse(U),sk_c8).
% -equal(multiply(sk_c8,Y),sk_c7) | -equal(multiply(Z,sk_c8),Y) | -equal(inverse(Z),sk_c8).
% -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7).
% -equal(multiply(sk_c7,sk_c8),sk_c6).
% -equal(multiply(sk_c8,sk_c7),sk_c6).
%
% 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(multiply(sk_c7,sk_c8),sk_c6) | -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7) | -equal(multiply(sk_c8,Y),sk_c7) | -equal(multiply(Z,sk_c8),Y) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c8,sk_c7),sk_c6) | -equal(multiply(U,sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(V,sk_c8),sk_c6) | -equal(inverse(V),sk_c8).
% Split part used next: -equal(multiply(V,sk_c8),sk_c6) | -equal(inverse(V),sk_c8).
% END OF PROOFPART
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,0,75,0,0,848,50,7,888,0,7,1864,50,19,1904,0,19,2981,50,35,3021,0,35,4152,50,48,4192,0,48,5378,50,65,5418,0,65,6684,50,91,6724,0,91,8071,50,132,8111,0,132,9564,50,207,9604,0,207,11163,50,354,11203,0,354,12894,50,584,12934,0,584,14757,50,997,14757,40,997,14797,0,997,24679,3,1298,25447,4,1448,26209,5,1598,26210,1,1598,26210,50,1598,26210,40,1598,26250,0,1598,26603,3,1901,26614,4,2062,26635,5,2199,26635,1,2199,26635,50,2199,26635,40,2199,26675,0,2199,52435,3,3701,53177,4,4450,54185,5,5200,54186,1,5200,54186,50,5201,54186,40,5201,54226,0,5201,73854,3,5953,74207,4,6327,74879,5,6702,74880,1,6702,74880,50,6702,74880,40,6702,74920,0,6703,85526,3,7460,86802,4,7829,88458,5,8204,88459,1,8204,88459,50,8204,88459,40,8204,88499,0,8204,155539,3,12107,156422,4,14055,157270,5,16005,157271,1,16005,157271,50,16007,157271,40,16007,157311,0,16008,207191,3,18560,208134,4,19834,208807,1,21109,208807,50,21111,208807,40,21111,208847,0,21111,242199,3,22625,243000,4,23362,243884,5,24112,243885,1,24112,243885,50,24114,243885,40,24114,243925,0,24114,253503,3,24871,254667,4,25240,255397,5,25615,255397,1,25615,255397,50,25615,255397,40,25615,255437,0,25615,284976,3,26817,285768,4,27416,286394,5,28016,286395,1,28016,286395,50,28017,286395,40,28017,286435,0,28017,308887,3,28774,309553,4,29143,310133,1,29518,310133,50,29518,310133,40,29518,310133,40,29518,310168,0,29518)
%
%
% START OF PROOF
% 310134 [] equal(X,X).
% 310135 [] equal(multiply(identity,X),X).
% 310136 [] equal(multiply(inverse(X),X),identity).
% 310137 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 310138 [] -equal(multiply(X,sk_c8),sk_c6) | -equal(inverse(X),sk_c8).
% 310139 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c5),sk_c8).
% 310140 [?] ?
% 310144 [] equal(multiply(sk_c2,sk_c8),sk_c3) | equal(inverse(sk_c5),sk_c8).
% 310145 [] equal(multiply(sk_c2,sk_c8),sk_c3) | equal(multiply(sk_c5,sk_c8),sk_c6).
% 310149 [] equal(multiply(sk_c8,sk_c3),sk_c7) | equal(inverse(sk_c5),sk_c8).
% 310150 [] equal(multiply(sk_c8,sk_c3),sk_c7) | equal(multiply(sk_c5,sk_c8),sk_c6).
% 310154 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c5),sk_c8).
% 310155 [?] ?
% 310159 [] equal(multiply(sk_c1,sk_c7),sk_c8) | equal(inverse(sk_c5),sk_c8).
% 310160 [] equal(multiply(sk_c1,sk_c7),sk_c8) | equal(multiply(sk_c5,sk_c8),sk_c6).
% 310164 [] equal(multiply(sk_c7,sk_c8),sk_c6) | equal(inverse(sk_c5),sk_c8).
% 310165 [] equal(multiply(sk_c7,sk_c8),sk_c6) | equal(multiply(sk_c5,sk_c8),sk_c6).
% 310172 [hyper:310138,310139,binarycut:310140] equal(inverse(sk_c2),sk_c8).
% 310174 [para:310172.1.1,310136.1.1.1] equal(multiply(sk_c8,sk_c2),identity).
% 310181 [hyper:310138,310154,binarycut:310155] equal(inverse(sk_c1),sk_c7).
% 310182 [para:310181.1.1,310136.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 310191 [hyper:310138,310145,310144] equal(multiply(sk_c2,sk_c8),sk_c3).
% 310200 [hyper:310138,310150,310149] equal(multiply(sk_c8,sk_c3),sk_c7).
% 310216 [hyper:310138,310160,310159] equal(multiply(sk_c1,sk_c7),sk_c8).
% 310220 [hyper:310138,310165,310164] equal(multiply(sk_c7,sk_c8),sk_c6).
% 310222 [para:310136.1.1,310137.1.1.1,demod:310135] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 310223 [para:310174.1.1,310137.1.1.1,demod:310135] equal(X,multiply(sk_c8,multiply(sk_c2,X))).
% 310225 [para:310191.1.1,310137.1.1.1] equal(multiply(sk_c3,X),multiply(sk_c2,multiply(sk_c8,X))).
% 310231 [para:310191.1.1,310223.1.2.2,demod:310200] equal(sk_c8,sk_c7).
% 310232 [para:310231.1.2,310182.1.1.1] equal(multiply(sk_c8,sk_c1),identity).
% 310233 [para:310231.1.2,310216.1.1.2] equal(multiply(sk_c1,sk_c8),sk_c8).
% 310234 [para:310231.1.2,310220.1.1.1] equal(multiply(sk_c8,sk_c8),sk_c6).
% 310236 [?] ?
% 310238 [para:310174.1.1,310222.1.2.2] equal(sk_c2,multiply(inverse(sk_c8),identity)).
% 310240 [para:310200.1.1,310222.1.2.2] equal(sk_c3,multiply(inverse(sk_c8),sk_c7)).
% 310244 [para:310232.1.1,310222.1.2.2,demod:310238] equal(sk_c1,sk_c2).
% 310245 [para:310233.1.1,310222.1.2.2,demod:310220,310181] equal(sk_c8,sk_c6).
% 310250 [para:310244.1.2,310191.1.1.1,demod:310233] equal(sk_c8,sk_c3).
% 310261 [para:310250.1.1,310223.1.2.1] equal(X,multiply(sk_c3,multiply(sk_c2,X))).
% 310264 [para:310250.1.1,310245.1.1] equal(sk_c3,sk_c6).
% 310268 [para:310264.1.1,310200.1.1.2] equal(multiply(sk_c8,sk_c6),sk_c7).
% 310272 [para:310250.1.1,310234.1.1.1] equal(multiply(sk_c3,sk_c8),sk_c6).
% 310277 [para:310223.1.2,310225.1.2.2,demod:310261] equal(X,multiply(sk_c2,X)).
% 310278 [para:310244.1.2,310225.1.2.1,demod:310236] equal(multiply(sk_c3,X),multiply(sk_c8,X)).
% 310279 [para:310245.1.1,310225.1.2.2.1,demod:310277] equal(multiply(sk_c3,X),multiply(sk_c6,X)).
% 310280 [para:310277.1.2,310223.1.2.2,demod:310279,310278] equal(X,multiply(sk_c6,X)).
% 310282 [para:310280.1.2,310222.1.2.2] equal(X,multiply(inverse(sk_c6),X)).
% 310298 [para:310282.1.2,310136.1.1] equal(sk_c6,identity).
% 310302 [para:310298.1.1,310268.1.1.2,demod:310280,310279,310278] equal(identity,sk_c7).
% 310305 [para:310302.1.2,310240.1.2.2,demod:310238] equal(sk_c3,sk_c2).
% 310306 [para:310305.1.2,310172.1.1.1] equal(inverse(sk_c3),sk_c8).
% 310317 [hyper:310138,310306,demod:310272,cut:310134] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% Split component 2 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c8),sk_c6) | -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7) | -equal(multiply(sk_c8,Y),sk_c7) | -equal(multiply(Z,sk_c8),Y) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c8,sk_c7),sk_c6) | -equal(multiply(U,sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(V,sk_c8),sk_c6) | -equal(inverse(V),sk_c8).
% Split part used next: -equal(multiply(U,sk_c8),sk_c7) | -equal(inverse(U),sk_c8).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,0,75,0,0,848,50,7,888,0,7,1864,50,19,1904,0,19,2981,50,35,3021,0,35,4152,50,48,4192,0,48,5378,50,65,5418,0,65,6684,50,91,6724,0,91,8071,50,132,8111,0,132,9564,50,207,9604,0,207,11163,50,354,11203,0,354,12894,50,584,12934,0,584,14757,50,997,14757,40,997,14797,0,997,24679,3,1298,25447,4,1448,26209,5,1598,26210,1,1598,26210,50,1598,26210,40,1598,26250,0,1598,26603,3,1901,26614,4,2062,26635,5,2199,26635,1,2199,26635,50,2199,26635,40,2199,26675,0,2199,52435,3,3701,53177,4,4450,54185,5,5200,54186,1,5200,54186,50,5201,54186,40,5201,54226,0,5201,73854,3,5953,74207,4,6327,74879,5,6702,74880,1,6702,74880,50,6702,74880,40,6702,74920,0,6703,85526,3,7460,86802,4,7829,88458,5,8204,88459,1,8204,88459,50,8204,88459,40,8204,88499,0,8204,155539,3,12107,156422,4,14055,157270,5,16005,157271,1,16005,157271,50,16007,157271,40,16007,157311,0,16008,207191,3,18560,208134,4,19834,208807,1,21109,208807,50,21111,208807,40,21111,208847,0,21111,242199,3,22625,243000,4,23362,243884,5,24112,243885,1,24112,243885,50,24114,243885,40,24114,243925,0,24114,253503,3,24871,254667,4,25240,255397,5,25615,255397,1,25615,255397,50,25615,255397,40,25615,255437,0,25615,284976,3,26817,285768,4,27416,286394,5,28016,286395,1,28016,286395,50,28017,286395,40,28017,286435,0,28017,308887,3,28774,309553,4,29143,310133,1,29518,310133,50,29518,310133,40,29518,310133,40,29518,310168,0,29518,310316,50,29518,310316,30,29518,310316,40,29518,310351,0,29518)
%
%
% START OF PROOF
% 310318 [] equal(multiply(identity,X),X).
% 310319 [] equal(multiply(inverse(X),X),identity).
% 310320 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 310321 [] -equal(multiply(X,sk_c8),sk_c7) | -equal(inverse(X),sk_c8).
% 310324 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c4),sk_c8).
% 310325 [?] ?
% 310329 [] equal(multiply(sk_c2,sk_c8),sk_c3) | equal(inverse(sk_c4),sk_c8).
% 310330 [] equal(multiply(sk_c2,sk_c8),sk_c3) | equal(multiply(sk_c4,sk_c8),sk_c7).
% 310334 [] equal(multiply(sk_c8,sk_c3),sk_c7) | equal(inverse(sk_c4),sk_c8).
% 310335 [] equal(multiply(sk_c8,sk_c3),sk_c7) | equal(multiply(sk_c4,sk_c8),sk_c7).
% 310339 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c4),sk_c8).
% 310340 [?] ?
% 310344 [] equal(multiply(sk_c1,sk_c7),sk_c8) | equal(inverse(sk_c4),sk_c8).
% 310345 [] equal(multiply(sk_c1,sk_c7),sk_c8) | equal(multiply(sk_c4,sk_c8),sk_c7).
% 310349 [] equal(multiply(sk_c7,sk_c8),sk_c6) | equal(inverse(sk_c4),sk_c8).
% 310350 [] equal(multiply(sk_c7,sk_c8),sk_c6) | equal(multiply(sk_c4,sk_c8),sk_c7).
% 310358 [hyper:310321,310324,binarycut:310325] equal(inverse(sk_c2),sk_c8).
% 310361 [para:310358.1.1,310319.1.1.1] equal(multiply(sk_c8,sk_c2),identity).
% 310371 [hyper:310321,310339,binarycut:310340] equal(inverse(sk_c1),sk_c7).
% 310372 [para:310371.1.1,310319.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 310394 [hyper:310321,310330,310329] equal(multiply(sk_c2,sk_c8),sk_c3).
% 310401 [hyper:310321,310335,310334] equal(multiply(sk_c8,sk_c3),sk_c7).
% 310405 [hyper:310321,310345,310344] equal(multiply(sk_c1,sk_c7),sk_c8).
% 310409 [hyper:310321,310350,310349] equal(multiply(sk_c7,sk_c8),sk_c6).
% 310410 [para:310319.1.1,310320.1.1.1,demod:310318] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 310411 [para:310361.1.1,310320.1.1.1,demod:310318] equal(X,multiply(sk_c8,multiply(sk_c2,X))).
% 310413 [para:310394.1.1,310320.1.1.1] equal(multiply(sk_c3,X),multiply(sk_c2,multiply(sk_c8,X))).
% 310417 [para:310394.1.1,310411.1.2.2,demod:310401] equal(sk_c8,sk_c7).
% 310418 [para:310417.1.2,310372.1.1.1] equal(multiply(sk_c8,sk_c1),identity).
% 310419 [para:310417.1.2,310405.1.1.2] equal(multiply(sk_c1,sk_c8),sk_c8).
% 310420 [para:310417.1.2,310409.1.1.1] equal(multiply(sk_c8,sk_c8),sk_c6).
% 310422 [?] ?
% 310424 [para:310361.1.1,310410.1.2.2] equal(sk_c2,multiply(inverse(sk_c8),identity)).
% 310426 [para:310401.1.1,310410.1.2.2] equal(sk_c3,multiply(inverse(sk_c8),sk_c7)).
% 310430 [para:310418.1.1,310410.1.2.2,demod:310424] equal(sk_c1,sk_c2).
% 310431 [para:310419.1.1,310410.1.2.2,demod:310409,310371] equal(sk_c8,sk_c6).
% 310436 [para:310430.1.2,310394.1.1.1,demod:310419] equal(sk_c8,sk_c3).
% 310438 [para:310431.1.1,310394.1.1.2] equal(multiply(sk_c2,sk_c6),sk_c3).
% 310447 [para:310436.1.1,310411.1.2.1] equal(X,multiply(sk_c3,multiply(sk_c2,X))).
% 310450 [para:310436.1.1,310431.1.1] equal(sk_c3,sk_c6).
% 310454 [para:310450.1.1,310401.1.1.2] equal(multiply(sk_c8,sk_c6),sk_c7).
% 310456 [para:310436.1.1,310420.1.1.1] equal(multiply(sk_c3,sk_c8),sk_c6).
% 310461 [para:310411.1.2,310413.1.2.2,demod:310447] equal(X,multiply(sk_c2,X)).
% 310462 [para:310430.1.2,310413.1.2.1,demod:310422] equal(multiply(sk_c3,X),multiply(sk_c8,X)).
% 310463 [para:310431.1.1,310413.1.2.2.1,demod:310461] equal(multiply(sk_c3,X),multiply(sk_c6,X)).
% 310464 [para:310461.1.2,310411.1.2.2,demod:310463,310462] equal(X,multiply(sk_c6,X)).
% 310466 [para:310464.1.2,310410.1.2.2] equal(X,multiply(inverse(sk_c6),X)).
% 310472 [para:310438.1.1,310411.1.2.2,demod:310401] equal(sk_c6,sk_c7).
% 310478 [para:310466.1.2,310319.1.1] equal(sk_c6,identity).
% 310482 [para:310478.1.1,310454.1.1.2,demod:310464,310463,310462] equal(identity,sk_c7).
% 310485 [para:310482.1.2,310426.1.2.2,demod:310424] equal(sk_c3,sk_c2).
% 310486 [para:310485.1.2,310358.1.1.1] equal(inverse(sk_c3),sk_c8).
% 310497 [hyper:310321,310486,demod:310456,cut:310472] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% Split component 3 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c8),sk_c6) | -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7) | -equal(multiply(sk_c8,Y),sk_c7) | -equal(multiply(Z,sk_c8),Y) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c8,sk_c7),sk_c6) | -equal(multiply(U,sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(V,sk_c8),sk_c6) | -equal(inverse(V),sk_c8).
% Split part used next: -equal(multiply(sk_c8,Y),sk_c7) | -equal(multiply(Z,sk_c8),Y) | -equal(inverse(Z),sk_c8).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,0,75,0,0,848,50,7,888,0,7,1864,50,19,1904,0,19,2981,50,35,3021,0,35,4152,50,48,4192,0,48,5378,50,65,5418,0,65,6684,50,91,6724,0,91,8071,50,132,8111,0,132,9564,50,207,9604,0,207,11163,50,354,11203,0,354,12894,50,584,12934,0,584,14757,50,997,14757,40,997,14797,0,997,24679,3,1298,25447,4,1448,26209,5,1598,26210,1,1598,26210,50,1598,26210,40,1598,26250,0,1598,26603,3,1901,26614,4,2062,26635,5,2199,26635,1,2199,26635,50,2199,26635,40,2199,26675,0,2199,52435,3,3701,53177,4,4450,54185,5,5200,54186,1,5200,54186,50,5201,54186,40,5201,54226,0,5201,73854,3,5953,74207,4,6327,74879,5,6702,74880,1,6702,74880,50,6702,74880,40,6702,74920,0,6703,85526,3,7460,86802,4,7829,88458,5,8204,88459,1,8204,88459,50,8204,88459,40,8204,88499,0,8204,155539,3,12107,156422,4,14055,157270,5,16005,157271,1,16005,157271,50,16007,157271,40,16007,157311,0,16008,207191,3,18560,208134,4,19834,208807,1,21109,208807,50,21111,208807,40,21111,208847,0,21111,242199,3,22625,243000,4,23362,243884,5,24112,243885,1,24112,243885,50,24114,243885,40,24114,243925,0,24114,253503,3,24871,254667,4,25240,255397,5,25615,255397,1,25615,255397,50,25615,255397,40,25615,255437,0,25615,284976,3,26817,285768,4,27416,286394,5,28016,286395,1,28016,286395,50,28017,286395,40,28017,286435,0,28017,308887,3,28774,309553,4,29143,310133,1,29518,310133,50,29518,310133,40,29518,310133,40,29518,310168,0,29518,310316,50,29518,310316,30,29518,310316,40,29518,310351,0,29518,310496,50,29518,310496,30,29518,310496,40,29518,310531,0,29523)
%
%
% START OF PROOF
% 310497 [] equal(X,X).
% 310498 [] equal(multiply(identity,X),X).
% 310499 [] equal(multiply(inverse(X),X),identity).
% 310500 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 310501 [] -equal(multiply(sk_c8,X),sk_c7) | -equal(multiply(Y,sk_c8),X) | -equal(inverse(Y),sk_c8).
% 310502 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c5),sk_c8).
% 310503 [] equal(multiply(sk_c5,sk_c8),sk_c6) | equal(inverse(sk_c2),sk_c8).
% 310504 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c4),sk_c8).
% 310505 [] equal(multiply(sk_c4,sk_c8),sk_c7) | equal(inverse(sk_c2),sk_c8).
% 310506 [] equal(multiply(sk_c8,sk_c7),sk_c6) | equal(inverse(sk_c2),sk_c8).
% 310507 [] equal(multiply(sk_c2,sk_c8),sk_c3) | equal(inverse(sk_c5),sk_c8).
% 310508 [] equal(multiply(sk_c2,sk_c8),sk_c3) | equal(multiply(sk_c5,sk_c8),sk_c6).
% 310509 [] equal(multiply(sk_c2,sk_c8),sk_c3) | equal(inverse(sk_c4),sk_c8).
% 310510 [] equal(multiply(sk_c2,sk_c8),sk_c3) | equal(multiply(sk_c4,sk_c8),sk_c7).
% 310511 [] equal(multiply(sk_c2,sk_c8),sk_c3) | equal(multiply(sk_c8,sk_c7),sk_c6).
% 310512 [?] ?
% 310513 [?] ?
% 310514 [?] ?
% 310515 [?] ?
% 310516 [?] ?
% 310577 [hyper:310501,310507,binarycut:310512,binarycut:310502] equal(inverse(sk_c5),sk_c8).
% 310587 [para:310577.1.1,310499.1.1.1] equal(multiply(sk_c8,sk_c5),identity).
% 310593 [hyper:310501,310509,binarycut:310514,binarycut:310504] equal(inverse(sk_c4),sk_c8).
% 310603 [para:310593.1.1,310499.1.1.1] equal(multiply(sk_c8,sk_c4),identity).
% 310610 [hyper:310501,310508,310503,binarycut:310513] equal(multiply(sk_c5,sk_c8),sk_c6).
% 310622 [hyper:310501,310510,310505,binarycut:310515] equal(multiply(sk_c4,sk_c8),sk_c7).
% 310630 [hyper:310501,310511,310506,binarycut:310516] equal(multiply(sk_c8,sk_c7),sk_c6).
% 310631 [para:310499.1.1,310500.1.1.1,demod:310498] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 310632 [para:310587.1.1,310500.1.1.1,demod:310498] equal(X,multiply(sk_c8,multiply(sk_c5,X))).
% 310633 [para:310603.1.1,310500.1.1.1,demod:310498] equal(X,multiply(sk_c8,multiply(sk_c4,X))).
% 310634 [para:310610.1.1,310500.1.1.1] equal(multiply(sk_c6,X),multiply(sk_c5,multiply(sk_c8,X))).
% 310643 [para:310622.1.1,310633.1.2.2,demod:310630] equal(sk_c8,sk_c6).
% 310644 [para:310643.1.1,310587.1.1.1] equal(multiply(sk_c6,sk_c5),identity).
% 310651 [para:310643.1.1,310633.1.2.1] equal(X,multiply(sk_c6,multiply(sk_c4,X))).
% 310658 [para:310632.1.2,310631.1.2.2] equal(multiply(sk_c5,X),multiply(inverse(sk_c8),X)).
% 310659 [para:310633.1.2,310631.1.2.2,demod:310658] equal(multiply(sk_c4,X),multiply(sk_c5,X)).
% 310667 [para:310632.1.2,310634.1.2.2,demod:310651,310659] equal(X,multiply(sk_c4,X)).
% 310668 [para:310633.1.2,310634.1.2.2,demod:310659,310667] equal(multiply(sk_c6,X),X).
% 310672 [para:310667.1.2,310622.1.1] equal(sk_c8,sk_c7).
% 310673 [para:310667.1.2,310633.1.2.2] equal(X,multiply(sk_c8,X)).
% 310676 [para:310668.1.1,310644.1.1] equal(sk_c5,identity).
% 310681 [para:310676.1.1,310577.1.1.1] equal(inverse(identity),sk_c8).
% 310686 [hyper:310501,310681,310497,demod:310673,310498,cut:310672] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% Split component 4 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c8),sk_c6) | -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7) | -equal(multiply(sk_c8,Y),sk_c7) | -equal(multiply(Z,sk_c8),Y) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c8,sk_c7),sk_c6) | -equal(multiply(U,sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(V,sk_c8),sk_c6) | -equal(inverse(V),sk_c8).
% Split part used next: -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 4
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,0,75,0,0,848,50,7,888,0,7,1864,50,19,1904,0,19,2981,50,35,3021,0,35,4152,50,48,4192,0,48,5378,50,65,5418,0,65,6684,50,91,6724,0,91,8071,50,132,8111,0,132,9564,50,207,9604,0,207,11163,50,354,11203,0,354,12894,50,584,12934,0,584,14757,50,997,14757,40,997,14797,0,997,24679,3,1298,25447,4,1448,26209,5,1598,26210,1,1598,26210,50,1598,26210,40,1598,26250,0,1598,26603,3,1901,26614,4,2062,26635,5,2199,26635,1,2199,26635,50,2199,26635,40,2199,26675,0,2199,52435,3,3701,53177,4,4450,54185,5,5200,54186,1,5200,54186,50,5201,54186,40,5201,54226,0,5201,73854,3,5953,74207,4,6327,74879,5,6702,74880,1,6702,74880,50,6702,74880,40,6702,74920,0,6703,85526,3,7460,86802,4,7829,88458,5,8204,88459,1,8204,88459,50,8204,88459,40,8204,88499,0,8204,155539,3,12107,156422,4,14055,157270,5,16005,157271,1,16005,157271,50,16007,157271,40,16007,157311,0,16008,207191,3,18560,208134,4,19834,208807,1,21109,208807,50,21111,208807,40,21111,208847,0,21111,242199,3,22625,243000,4,23362,243884,5,24112,243885,1,24112,243885,50,24114,243885,40,24114,243925,0,24114,253503,3,24871,254667,4,25240,255397,5,25615,255397,1,25615,255397,50,25615,255397,40,25615,255437,0,25615,284976,3,26817,285768,4,27416,286394,5,28016,286395,1,28016,286395,50,28017,286395,40,28017,286435,0,28017,308887,3,28774,309553,4,29143,310133,1,29518,310133,50,29518,310133,40,29518,310133,40,29518,310168,0,29518,310316,50,29518,310316,30,29518,310316,40,29518,310351,0,29518,310496,50,29518,310496,30,29518,310496,40,29518,310531,0,29523,310685,50,29524,310685,30,29524,310685,40,29524,310720,0,29524,310801,50,29525,310836,0,29525)
%
%
% START OF PROOF
% 310803 [] equal(multiply(identity,X),X).
% 310804 [] equal(multiply(inverse(X),X),identity).
% 310805 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 310806 [] -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7).
% 310822 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c5),sk_c8).
% 310823 [] equal(multiply(sk_c5,sk_c8),sk_c6) | equal(inverse(sk_c1),sk_c7).
% 310824 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c4),sk_c8).
% 310825 [] equal(multiply(sk_c4,sk_c8),sk_c7) | equal(inverse(sk_c1),sk_c7).
% 310826 [] equal(multiply(sk_c8,sk_c7),sk_c6) | equal(inverse(sk_c1),sk_c7).
% 310827 [?] ?
% 310828 [?] ?
% 310829 [?] ?
% 310830 [?] ?
% 310831 [?] ?
% 310842 [hyper:310806,310822,binarycut:310827] equal(inverse(sk_c5),sk_c8).
% 310843 [para:310842.1.1,310804.1.1.1] equal(multiply(sk_c8,sk_c5),identity).
% 310846 [hyper:310806,310824,binarycut:310829] equal(inverse(sk_c4),sk_c8).
% 310847 [para:310846.1.1,310804.1.1.1] equal(multiply(sk_c8,sk_c4),identity).
% 310853 [hyper:310806,310823,binarycut:310828] equal(multiply(sk_c5,sk_c8),sk_c6).
% 310856 [hyper:310806,310825,binarycut:310830] equal(multiply(sk_c4,sk_c8),sk_c7).
% 310860 [hyper:310806,310826,binarycut:310831] equal(multiply(sk_c8,sk_c7),sk_c6).
% 310861 [para:310804.1.1,310805.1.1.1,demod:310803] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 310862 [para:310843.1.1,310805.1.1.1,demod:310803] equal(X,multiply(sk_c8,multiply(sk_c5,X))).
% 310863 [para:310847.1.1,310805.1.1.1,demod:310803] equal(X,multiply(sk_c8,multiply(sk_c4,X))).
% 310864 [para:310853.1.1,310805.1.1.1] equal(multiply(sk_c6,X),multiply(sk_c5,multiply(sk_c8,X))).
% 310869 [para:310856.1.1,310863.1.2.2,demod:310860] equal(sk_c8,sk_c6).
% 310877 [para:310869.1.1,310863.1.2.1] equal(X,multiply(sk_c6,multiply(sk_c4,X))).
% 310879 [para:310804.1.1,310861.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 310880 [para:310843.1.1,310861.1.2.2] equal(sk_c5,multiply(inverse(sk_c8),identity)).
% 310882 [para:310860.1.1,310861.1.2.2] equal(sk_c7,multiply(inverse(sk_c8),sk_c6)).
% 310883 [para:310805.1.1,310861.1.2.2] equal(X,multiply(inverse(multiply(Y,Z)),multiply(Y,multiply(Z,X)))).
% 310884 [para:310862.1.2,310861.1.2.2] equal(multiply(sk_c5,X),multiply(inverse(sk_c8),X)).
% 310885 [para:310863.1.2,310861.1.2.2,demod:310884] equal(multiply(sk_c4,X),multiply(sk_c5,X)).
% 310887 [para:310861.1.2,310861.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 310892 [para:310862.1.2,310864.1.2.2,demod:310877,310885] equal(X,multiply(sk_c4,X)).
% 310893 [para:310863.1.2,310864.1.2.2,demod:310885,310892] equal(multiply(sk_c6,X),X).
% 310895 [para:310892.1.2,310856.1.1] equal(sk_c8,sk_c7).
% 310899 [para:310893.1.1,310861.1.2.2] equal(X,multiply(inverse(sk_c6),X)).
% 310905 [para:310899.1.2,310804.1.1] equal(sk_c6,identity).
% 310911 [para:310905.1.1,310882.1.2.2,demod:310880] equal(sk_c7,sk_c5).
% 310915 [para:310911.1.1,310895.1.2] equal(sk_c8,sk_c5).
% 310922 [para:310856.1.1,310883.1.2.2.2] equal(sk_c8,multiply(inverse(multiply(X,sk_c4)),multiply(X,sk_c7))).
% 310924 [para:310862.1.2,310883.1.2.2.2,demod:310892,310885] equal(X,multiply(inverse(multiply(Y,sk_c8)),multiply(Y,X))).
% 310931 [para:310915.1.1,310856.1.1.2,demod:310892] equal(sk_c5,sk_c7).
% 310932 [para:310887.1.2,310804.1.1] equal(multiply(X,inverse(X)),identity).
% 310934 [para:310887.1.2,310879.1.2] equal(X,multiply(X,identity)).
% 310936 [para:310934.1.2,310879.1.2] equal(X,inverse(inverse(X))).
% 310937 [para:310934.1.2,310880.1.2] equal(sk_c5,inverse(sk_c8)).
% 310940 [para:310932.1.1,310924.1.2.2,demod:310934] equal(inverse(X),inverse(multiply(X,sk_c8))).
% 310946 [para:310940.1.2,310879.1.2.1.1,demod:310934,310936] equal(multiply(X,sk_c8),X).
% 310951 [para:310946.1.1,310892.1.2] equal(sk_c8,sk_c4).
% 310957 [para:310951.1.1,310946.1.1.2] equal(multiply(X,sk_c4),X).
% 310958 [para:310922.1.2,310861.1.2.2,demod:310946,310936,310957] equal(multiply(X,sk_c7),X).
% 310959 [hyper:310806,310958,demod:310937,cut:310931] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 4
% seconds given: 4
%
%
% Split component 5 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c8),sk_c6) | -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7) | -equal(multiply(sk_c8,Y),sk_c7) | -equal(multiply(Z,sk_c8),Y) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c8,sk_c7),sk_c6) | -equal(multiply(U,sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(V,sk_c8),sk_c6) | -equal(inverse(V),sk_c8).
% Split part used next: -equal(multiply(sk_c7,sk_c8),sk_c6).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 4
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 5
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 6
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 7
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 8
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 9
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 10
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 11
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,0,75,0,0,848,50,7,888,0,7,1864,50,19,1904,0,19,2981,50,35,3021,0,35,4152,50,48,4192,0,48,5378,50,65,5418,0,65,6684,50,91,6724,0,91,8071,50,132,8111,0,132,9564,50,207,9604,0,207,11163,50,354,11203,0,354,12894,50,584,12934,0,584,14757,50,997,14757,40,997,14797,0,997,24679,3,1298,25447,4,1448,26209,5,1598,26210,1,1598,26210,50,1598,26210,40,1598,26250,0,1598,26603,3,1901,26614,4,2062,26635,5,2199,26635,1,2199,26635,50,2199,26635,40,2199,26675,0,2199,52435,3,3701,53177,4,4450,54185,5,5200,54186,1,5200,54186,50,5201,54186,40,5201,54226,0,5201,73854,3,5953,74207,4,6327,74879,5,6702,74880,1,6702,74880,50,6702,74880,40,6702,74920,0,6703,85526,3,7460,86802,4,7829,88458,5,8204,88459,1,8204,88459,50,8204,88459,40,8204,88499,0,8204,155539,3,12107,156422,4,14055,157270,5,16005,157271,1,16005,157271,50,16007,157271,40,16007,157311,0,16008,207191,3,18560,208134,4,19834,208807,1,21109,208807,50,21111,208807,40,21111,208847,0,21111,242199,3,22625,243000,4,23362,243884,5,24112,243885,1,24112,243885,50,24114,243885,40,24114,243925,0,24114,253503,3,24871,254667,4,25240,255397,5,25615,255397,1,25615,255397,50,25615,255397,40,25615,255437,0,25615,284976,3,26817,285768,4,27416,286394,5,28016,286395,1,28016,286395,50,28017,286395,40,28017,286435,0,28017,308887,3,28774,309553,4,29143,310133,1,29518,310133,50,29518,310133,40,29518,310133,40,29518,310168,0,29518,310316,50,29518,310316,30,29518,310316,40,29518,310351,0,29518,310496,50,29518,310496,30,29518,310496,40,29518,310531,0,29523,310685,50,29524,310685,30,29524,310685,40,29524,310720,0,29524,310801,50,29525,310836,0,29525,310958,50,29526,310958,30,29526,310958,40,29526,310993,0,29531,311086,50,29531,311121,0,29531,311257,50,29534,311292,0,29538,311436,50,29541,311471,0,29541,311623,50,29547,311658,0,29547,311816,50,29555,311851,0,29559,312017,50,29574,312052,0,29574,312226,50,29601,312261,0,29606,312445,50,29661,312480,0,29662,312674,50,29775,312674,40,29775,312709,0,29775)
%
%
% START OF PROOF
% 312676 [] equal(multiply(identity,X),X).
% 312677 [] equal(multiply(inverse(X),X),identity).
% 312678 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 312679 [] -equal(multiply(sk_c7,sk_c8),sk_c6).
% 312705 [?] ?
% 312706 [?] ?
% 312707 [?] ?
% 312708 [?] ?
% 312709 [?] ?
% 312747 [input:312705,cut:312679] equal(inverse(sk_c5),sk_c8).
% 312748 [para:312747.1.1,312677.1.1.1] equal(multiply(sk_c8,sk_c5),identity).
% 312750 [input:312707,cut:312679] equal(inverse(sk_c4),sk_c8).
% 312751 [para:312750.1.1,312677.1.1.1] equal(multiply(sk_c8,sk_c4),identity).
% 312763 [input:312706,cut:312679] equal(multiply(sk_c5,sk_c8),sk_c6).
% 312764 [input:312708,cut:312679] equal(multiply(sk_c4,sk_c8),sk_c7).
% 312765 [input:312709,cut:312679] equal(multiply(sk_c8,sk_c7),sk_c6).
% 312769 [para:312677.1.1,312678.1.1.1,demod:312676] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 312784 [para:312748.1.1,312678.1.1.1,demod:312676] equal(X,multiply(sk_c8,multiply(sk_c5,X))).
% 312787 [para:312751.1.1,312678.1.1.1,demod:312676] equal(X,multiply(sk_c8,multiply(sk_c4,X))).
% 312808 [para:312765.1.1,312678.1.1.1] equal(multiply(sk_c6,X),multiply(sk_c8,multiply(sk_c7,X))).
% 312817 [para:312763.1.1,312784.1.2.2] equal(sk_c8,multiply(sk_c8,sk_c6)).
% 312824 [para:312764.1.1,312787.1.2.2] equal(sk_c8,multiply(sk_c8,sk_c7)).
% 312830 [para:312824.1.2,312765.1.1] equal(sk_c8,sk_c6).
% 312831 [para:312824.1.2,312678.1.1.1,demod:312808] equal(multiply(sk_c8,X),multiply(sk_c6,X)).
% 312860 [para:312830.1.1,312763.1.1.2] equal(multiply(sk_c5,sk_c6),sk_c6).
% 312868 [para:312860.1.1,312678.1.1.1] equal(multiply(sk_c6,X),multiply(sk_c5,multiply(sk_c6,X))).
% 312928 [para:312784.1.2,312769.1.2.2] equal(multiply(sk_c5,X),multiply(inverse(sk_c8),X)).
% 312929 [para:312817.1.2,312769.1.2.2,demod:312928] equal(sk_c6,multiply(sk_c5,sk_c8)).
% 312931 [para:312824.1.2,312769.1.2.2,demod:312929,312928] equal(sk_c7,sk_c6).
% 312935 [para:312831.1.1,312769.1.2.2,demod:312868,312928] equal(X,multiply(sk_c6,X)).
% 312946 [para:312931.1.1,312679.1.1.1,demod:312935,cut:312830] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% Split component 6 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c8),sk_c6) | -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7) | -equal(multiply(sk_c8,Y),sk_c7) | -equal(multiply(Z,sk_c8),Y) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c8,sk_c7),sk_c6) | -equal(multiply(U,sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(V,sk_c8),sk_c6) | -equal(inverse(V),sk_c8).
% Split part used next: -equal(multiply(sk_c8,sk_c7),sk_c6).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 4
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 5
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 6
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 7
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 8
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 9
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 10
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 11
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,0,75,0,0,848,50,7,888,0,7,1864,50,19,1904,0,19,2981,50,35,3021,0,35,4152,50,48,4192,0,48,5378,50,65,5418,0,65,6684,50,91,6724,0,91,8071,50,132,8111,0,132,9564,50,207,9604,0,207,11163,50,354,11203,0,354,12894,50,584,12934,0,584,14757,50,997,14757,40,997,14797,0,997,24679,3,1298,25447,4,1448,26209,5,1598,26210,1,1598,26210,50,1598,26210,40,1598,26250,0,1598,26603,3,1901,26614,4,2062,26635,5,2199,26635,1,2199,26635,50,2199,26635,40,2199,26675,0,2199,52435,3,3701,53177,4,4450,54185,5,5200,54186,1,5200,54186,50,5201,54186,40,5201,54226,0,5201,73854,3,5953,74207,4,6327,74879,5,6702,74880,1,6702,74880,50,6702,74880,40,6702,74920,0,6703,85526,3,7460,86802,4,7829,88458,5,8204,88459,1,8204,88459,50,8204,88459,40,8204,88499,0,8204,155539,3,12107,156422,4,14055,157270,5,16005,157271,1,16005,157271,50,16007,157271,40,16007,157311,0,16008,207191,3,18560,208134,4,19834,208807,1,21109,208807,50,21111,208807,40,21111,208847,0,21111,242199,3,22625,243000,4,23362,243884,5,24112,243885,1,24112,243885,50,24114,243885,40,24114,243925,0,24114,253503,3,24871,254667,4,25240,255397,5,25615,255397,1,25615,255397,50,25615,255397,40,25615,255437,0,25615,284976,3,26817,285768,4,27416,286394,5,28016,286395,1,28016,286395,50,28017,286395,40,28017,286435,0,28017,308887,3,28774,309553,4,29143,310133,1,29518,310133,50,29518,310133,40,29518,310133,40,29518,310168,0,29518,310316,50,29518,310316,30,29518,310316,40,29518,310351,0,29518,310496,50,29518,310496,30,29518,310496,40,29518,310531,0,29523,310685,50,29524,310685,30,29524,310685,40,29524,310720,0,29524,310801,50,29525,310836,0,29525,310958,50,29526,310958,30,29526,310958,40,29526,310993,0,29531,311086,50,29531,311121,0,29531,311257,50,29534,311292,0,29538,311436,50,29541,311471,0,29541,311623,50,29547,311658,0,29547,311816,50,29555,311851,0,29559,312017,50,29574,312052,0,29574,312226,50,29601,312261,0,29606,312445,50,29661,312480,0,29662,312674,50,29775,312674,40,29775,312709,0,29775,312945,50,29775,312945,30,29775,312945,40,29775,312980,0,29775,313099,50,29776,313134,0,29781,313305,50,29784,313340,0,29784,313519,50,29788,313554,0,29788,313741,50,29794,313776,0,29799,313969,50,29808,314004,0,29808,314205,50,29825,314240,0,29829,314449,50,29860,314484,0,29860,314703,50,29925,314738,0,29925,314967,50,30046,314967,40,30046,315002,0,30046)
%
%
% START OF PROOF
% 314795 [?] ?
% 314969 [] equal(multiply(identity,X),X).
% 314970 [] equal(multiply(inverse(X),X),identity).
% 314971 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 314972 [] -equal(multiply(sk_c8,sk_c7),sk_c6).
% 314977 [?] ?
% 314982 [?] ?
% 314987 [?] ?
% 315019 [input:314977,cut:314972] equal(inverse(sk_c2),sk_c8).
% 315020 [para:315019.1.1,314970.1.1.1] equal(multiply(sk_c8,sk_c2),identity).
% 315046 [input:314982,cut:314972] equal(multiply(sk_c2,sk_c8),sk_c3).
% 315052 [input:314987,cut:314972] equal(multiply(sk_c8,sk_c3),sk_c7).
% 315064 [para:315020.1.1,314971.1.1.1,demod:314969] equal(X,multiply(sk_c8,multiply(sk_c2,X))).
% 315104 [para:315046.1.1,315064.1.2.2] equal(sk_c8,multiply(sk_c8,sk_c3)).
% 315109 [para:315104.1.2,315052.1.1] equal(sk_c8,sk_c7).
% 315111 [para:315109.1.2,314972.1.1.2,cut:314795] 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: 34092
% derived clauses: 6807104
% kept clauses: 264779
% kept size sum: 303545
% kept mid-nuclei: 11214
% kept new demods: 4180
% forw unit-subs: 3233575
% forw double-subs: 2898929
% forw overdouble-subs: 360064
% backward subs: 10847
% fast unit cutoff: 21790
% full unit cutoff: 0
% dbl unit cutoff: 6458
% real runtime : 302.58
% process. runtime: 300.46
% specific non-discr-tree subsumption statistics:
% tried: 44422526
% length fails: 4810681
% strength fails: 15525627
% predlist fails: 4405796
% aux str. fails: 5153061
% by-lit fails: 7495672
% full subs tried: 2232143
% full subs fail: 2124203
%
% ; 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/GRP323-1+eq_r.in")
%
%------------------------------------------------------------------------------