%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP327-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 : art09.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 297.5s
% Output : Assurance 297.5s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----NO SOLUTION OUTPUT BY SYSTEM
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
%
% Gandalf c-2.6 r1 starting to prove: /home/graph/tptp/TSTP/PreparedTPTP/otter:hypothesis:set(auto),clear(print_given)---add_equality:r/GRP/GRP327-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 23)
% (binary-unit 12 #f)
% (binary-unit-uniteq 12 #f)
% (binary-posweight-kb-big-order 60 #f 3 23)
% (binary-posweight-lex-big-order 30 #f 3 23)
% (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(inverse(sk_c7),sk_c6) | -equal(multiply(sk_c6,sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8) | -equal(inverse(V),sk_c7) | -equal(multiply(V,sk_c6),sk_c7).
% was split for some strategies as:
% -equal(inverse(V),sk_c7) | -equal(multiply(V,sk_c6),sk_c7).
% -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),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(inverse(sk_c7),sk_c6).
% -equal(multiply(sk_c6,sk_c8),sk_c7).
%
% Starting a split proof attempt with 7 components.
%
% Split component 1 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_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(inverse(sk_c7),sk_c6) | -equal(multiply(sk_c6,sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8) | -equal(inverse(V),sk_c7) | -equal(multiply(V,sk_c6),sk_c7).
% Split part used next: -equal(inverse(V),sk_c7) | -equal(multiply(V,sk_c6),sk_c7).
% END OF PROOFPART
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(36,40,1,77,0,2,101989,5,1503,101989,1,1503,101989,50,1503,101989,40,1503,102030,0,1503,113421,3,1805,114086,4,1954,114699,5,2104,114700,1,2104,114700,50,2104,114700,40,2104,114741,0,2104,115159,3,2408,115179,4,2575,115187,5,2705,115187,1,2705,115187,50,2705,115187,40,2705,115228,0,2705,142059,3,4206,142784,4,4956,143371,1,5706,143371,50,5707,143371,40,5707,143412,0,5707,159834,3,6458,160538,4,6833,160854,1,7208,160854,50,7208,160854,40,7208,160895,0,7208,176689,3,7961,177371,4,8334,178151,1,8713,178151,50,8714,178151,40,8714,178192,0,8714,256553,3,12616,257538,4,14565,258150,1,16516,258150,50,16518,258150,40,16518,258191,0,16518,306680,3,19071,307543,4,20344,308445,1,21619,308445,50,21620,308445,40,21620,308486,0,21620,355704,3,23123,356393,4,23871,357119,5,24621,357120,1,24621,357120,50,24623,357120,40,24623,357161,0,24623,367926,3,25376,368877,4,25749,369393,5,26124,369394,1,26124,369394,50,26124,369394,40,26124,369435,0,26124,413406,3,27325,413945,4,27925,414458,5,28525,414459,1,28525,414459,50,28527,414459,40,28527,414500,0,28527,439944,3,29278,440563,4,29653,441142,5,30028,441143,1,30028,441143,50,30029,441143,40,30029,441143,40,30029,441179,0,30029)
%
%
% START OF PROOF
% 441145 [] equal(multiply(identity,X),X).
% 441146 [] equal(multiply(inverse(X),X),identity).
% 441147 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 441148 [] -equal(multiply(X,sk_c6),sk_c7) | -equal(inverse(X),sk_c7).
% 441149 [?] ?
% 441150 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c5),sk_c7).
% 441155 [] equal(multiply(sk_c2,sk_c8),sk_c3) | equal(multiply(sk_c5,sk_c6),sk_c7).
% 441156 [] equal(multiply(sk_c2,sk_c8),sk_c3) | equal(inverse(sk_c5),sk_c7).
% 441161 [] equal(multiply(sk_c8,sk_c3),sk_c7) | equal(multiply(sk_c5,sk_c6),sk_c7).
% 441162 [] equal(multiply(sk_c8,sk_c3),sk_c7) | equal(inverse(sk_c5),sk_c7).
% 441167 [?] ?
% 441168 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c5),sk_c7).
% 441173 [] equal(multiply(sk_c1,sk_c7),sk_c8) | equal(multiply(sk_c5,sk_c6),sk_c7).
% 441174 [] equal(multiply(sk_c1,sk_c7),sk_c8) | equal(inverse(sk_c5),sk_c7).
% 441179 [] equal(multiply(sk_c7,sk_c8),sk_c6).
% 441182 [hyper:441148,441150,binarycut:441149] equal(inverse(sk_c2),sk_c8).
% 441187 [para:441182.1.1,441146.1.1.1] equal(multiply(sk_c8,sk_c2),identity).
% 441191 [hyper:441148,441168,binarycut:441167] equal(inverse(sk_c1),sk_c7).
% 441194 [para:441191.1.1,441146.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 441198 [hyper:441148,441156,441155] equal(multiply(sk_c2,sk_c8),sk_c3).
% 441204 [hyper:441148,441162,441161] equal(multiply(sk_c8,sk_c3),sk_c7).
% 441210 [hyper:441148,441174,441173] equal(multiply(sk_c1,sk_c7),sk_c8).
% 441211 [para:441179.1.1,441147.1.1.1] equal(multiply(sk_c6,X),multiply(sk_c7,multiply(sk_c8,X))).
% 441212 [para:441146.1.1,441147.1.1.1,demod:441145] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 441213 [para:441187.1.1,441147.1.1.1,demod:441145] equal(X,multiply(sk_c8,multiply(sk_c2,X))).
% 441214 [para:441194.1.1,441147.1.1.1,demod:441145] equal(X,multiply(sk_c7,multiply(sk_c1,X))).
% 441218 [para:441198.1.1,441213.1.2.2,demod:441204] equal(sk_c8,sk_c7).
% 441219 [para:441218.1.2,441179.1.1.1] equal(multiply(sk_c8,sk_c8),sk_c6).
% 441221 [para:441218.1.2,441210.1.1.2] equal(multiply(sk_c1,sk_c8),sk_c8).
% 441226 [para:441213.1.2,441211.1.2.2] equal(multiply(sk_c6,multiply(sk_c2,X)),multiply(sk_c7,X)).
% 441231 [para:441221.1.1,441214.1.2.2,demod:441179] equal(sk_c8,sk_c6).
% 441237 [para:441231.1.1,441198.1.1.2] equal(multiply(sk_c2,sk_c6),sk_c3).
% 441239 [para:441231.1.1,441213.1.2.1,demod:441226] equal(X,multiply(sk_c7,X)).
% 441240 [para:441231.1.1,441219.1.1.2] equal(multiply(sk_c8,sk_c6),sk_c6).
% 441241 [para:441239.1.2,441194.1.1] equal(sk_c1,identity).
% 441250 [para:441213.1.2,441212.1.2.2] equal(multiply(sk_c2,X),multiply(inverse(sk_c8),X)).
% 441251 [para:441219.1.1,441212.1.2.2,demod:441237,441250] equal(sk_c8,sk_c3).
% 441254 [para:441241.1.1,441191.1.1.1] equal(inverse(identity),sk_c7).
% 441256 [para:441251.1.1,441179.1.1.2,demod:441239] equal(sk_c3,sk_c6).
% 441267 [para:441256.1.1,441204.1.1.2,demod:441240] equal(sk_c6,sk_c7).
% 441272 [hyper:441148,441254,demod:441145,cut:441267] 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 23
% 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(inverse(sk_c7),sk_c6) | -equal(multiply(sk_c6,sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8) | -equal(inverse(V),sk_c7) | -equal(multiply(V,sk_c6),sk_c7).
% Split part used next: -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),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 23
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(36,40,1,77,0,2,101989,5,1503,101989,1,1503,101989,50,1503,101989,40,1503,102030,0,1503,113421,3,1805,114086,4,1954,114699,5,2104,114700,1,2104,114700,50,2104,114700,40,2104,114741,0,2104,115159,3,2408,115179,4,2575,115187,5,2705,115187,1,2705,115187,50,2705,115187,40,2705,115228,0,2705,142059,3,4206,142784,4,4956,143371,1,5706,143371,50,5707,143371,40,5707,143412,0,5707,159834,3,6458,160538,4,6833,160854,1,7208,160854,50,7208,160854,40,7208,160895,0,7208,176689,3,7961,177371,4,8334,178151,1,8713,178151,50,8714,178151,40,8714,178192,0,8714,256553,3,12616,257538,4,14565,258150,1,16516,258150,50,16518,258150,40,16518,258191,0,16518,306680,3,19071,307543,4,20344,308445,1,21619,308445,50,21620,308445,40,21620,308486,0,21620,355704,3,23123,356393,4,23871,357119,5,24621,357120,1,24621,357120,50,24623,357120,40,24623,357161,0,24623,367926,3,25376,368877,4,25749,369393,5,26124,369394,1,26124,369394,50,26124,369394,40,26124,369435,0,26124,413406,3,27325,413945,4,27925,414458,5,28525,414459,1,28525,414459,50,28527,414459,40,28527,414500,0,28527,439944,3,29278,440563,4,29653,441142,5,30028,441143,1,30028,441143,50,30029,441143,40,30029,441143,40,30029,441179,0,30029,441271,50,30029,441271,30,30029,441271,40,30029,441307,0,30029)
%
%
% START OF PROOF
% 441273 [] equal(multiply(identity,X),X).
% 441274 [] equal(multiply(inverse(X),X),identity).
% 441275 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 441276 [] -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c8).
% 441279 [?] ?
% 441280 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c4),sk_c8).
% 441285 [] equal(multiply(sk_c2,sk_c8),sk_c3) | equal(multiply(sk_c4,sk_c7),sk_c8).
% 441286 [] equal(multiply(sk_c2,sk_c8),sk_c3) | equal(inverse(sk_c4),sk_c8).
% 441291 [] equal(multiply(sk_c8,sk_c3),sk_c7) | equal(multiply(sk_c4,sk_c7),sk_c8).
% 441292 [] equal(multiply(sk_c8,sk_c3),sk_c7) | equal(inverse(sk_c4),sk_c8).
% 441297 [?] ?
% 441298 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c4),sk_c8).
% 441303 [] equal(multiply(sk_c1,sk_c7),sk_c8) | equal(multiply(sk_c4,sk_c7),sk_c8).
% 441304 [] equal(multiply(sk_c1,sk_c7),sk_c8) | equal(inverse(sk_c4),sk_c8).
% 441307 [] equal(multiply(sk_c7,sk_c8),sk_c6).
% 441314 [hyper:441276,441280,binarycut:441279] equal(inverse(sk_c2),sk_c8).
% 441318 [para:441314.1.1,441274.1.1.1] equal(multiply(sk_c8,sk_c2),identity).
% 441323 [hyper:441276,441298,binarycut:441297] equal(inverse(sk_c1),sk_c7).
% 441324 [para:441323.1.1,441274.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 441336 [hyper:441276,441285,441286] equal(multiply(sk_c2,sk_c8),sk_c3).
% 441352 [hyper:441276,441291,441292] equal(multiply(sk_c8,sk_c3),sk_c7).
% 441359 [hyper:441276,441303,441304] equal(multiply(sk_c1,sk_c7),sk_c8).
% 441361 [para:441307.1.1,441275.1.1.1] equal(multiply(sk_c6,X),multiply(sk_c7,multiply(sk_c8,X))).
% 441362 [para:441274.1.1,441275.1.1.1,demod:441273] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 441363 [para:441318.1.1,441275.1.1.1,demod:441273] equal(X,multiply(sk_c8,multiply(sk_c2,X))).
% 441364 [para:441324.1.1,441275.1.1.1,demod:441273] equal(X,multiply(sk_c7,multiply(sk_c1,X))).
% 441370 [para:441336.1.1,441363.1.2.2,demod:441352] equal(sk_c8,sk_c7).
% 441371 [para:441370.1.2,441307.1.1.1] equal(multiply(sk_c8,sk_c8),sk_c6).
% 441373 [para:441370.1.2,441359.1.1.2] equal(multiply(sk_c1,sk_c8),sk_c8).
% 441378 [para:441363.1.2,441361.1.2.2] equal(multiply(sk_c6,multiply(sk_c2,X)),multiply(sk_c7,X)).
% 441383 [para:441373.1.1,441364.1.2.2,demod:441307] equal(sk_c8,sk_c6).
% 441389 [para:441383.1.1,441336.1.1.2] equal(multiply(sk_c2,sk_c6),sk_c3).
% 441391 [para:441383.1.1,441363.1.2.1,demod:441378] equal(X,multiply(sk_c7,X)).
% 441393 [para:441391.1.2,441324.1.1] equal(sk_c1,identity).
% 441394 [para:441370.1.2,441391.1.2.1] equal(X,multiply(sk_c8,X)).
% 441395 [para:441391.1.2,441361.1.2,demod:441394] equal(multiply(sk_c6,X),X).
% 441399 [para:441318.1.1,441362.1.2.2] equal(sk_c2,multiply(inverse(sk_c8),identity)).
% 441401 [para:441352.1.1,441362.1.2.2] equal(sk_c3,multiply(inverse(sk_c8),sk_c7)).
% 441402 [para:441363.1.2,441362.1.2.2] equal(multiply(sk_c2,X),multiply(inverse(sk_c8),X)).
% 441403 [para:441371.1.1,441362.1.2.2,demod:441389,441402] equal(sk_c8,sk_c3).
% 441405 [para:441361.1.2,441362.1.2.2,demod:441395,441394] equal(X,multiply(inverse(sk_c7),X)).
% 441407 [para:441393.1.1,441359.1.1.1,demod:441273] equal(sk_c7,sk_c8).
% 441415 [para:441403.1.1,441361.1.2.2.1,demod:441391,441395] equal(X,multiply(sk_c3,X)).
% 441430 [para:441405.1.2,441274.1.1] equal(sk_c7,identity).
% 441446 [para:441430.1.1,441401.1.2.2,demod:441399] equal(sk_c3,sk_c2).
% 441447 [para:441446.1.2,441314.1.1.1] equal(inverse(sk_c3),sk_c8).
% 441448 [hyper:441276,441447,demod:441415,cut:441407] 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 23
% 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(inverse(sk_c7),sk_c6) | -equal(multiply(sk_c6,sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8) | -equal(inverse(V),sk_c7) | -equal(multiply(V,sk_c6),sk_c7).
% 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 23
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(36,40,1,77,0,2,101989,5,1503,101989,1,1503,101989,50,1503,101989,40,1503,102030,0,1503,113421,3,1805,114086,4,1954,114699,5,2104,114700,1,2104,114700,50,2104,114700,40,2104,114741,0,2104,115159,3,2408,115179,4,2575,115187,5,2705,115187,1,2705,115187,50,2705,115187,40,2705,115228,0,2705,142059,3,4206,142784,4,4956,143371,1,5706,143371,50,5707,143371,40,5707,143412,0,5707,159834,3,6458,160538,4,6833,160854,1,7208,160854,50,7208,160854,40,7208,160895,0,7208,176689,3,7961,177371,4,8334,178151,1,8713,178151,50,8714,178151,40,8714,178192,0,8714,256553,3,12616,257538,4,14565,258150,1,16516,258150,50,16518,258150,40,16518,258191,0,16518,306680,3,19071,307543,4,20344,308445,1,21619,308445,50,21620,308445,40,21620,308486,0,21620,355704,3,23123,356393,4,23871,357119,5,24621,357120,1,24621,357120,50,24623,357120,40,24623,357161,0,24623,367926,3,25376,368877,4,25749,369393,5,26124,369394,1,26124,369394,50,26124,369394,40,26124,369435,0,26124,413406,3,27325,413945,4,27925,414458,5,28525,414459,1,28525,414459,50,28527,414459,40,28527,414500,0,28527,439944,3,29278,440563,4,29653,441142,5,30028,441143,1,30028,441143,50,30029,441143,40,30029,441143,40,30029,441179,0,30029,441271,50,30029,441271,30,30029,441271,40,30029,441307,0,30029,441447,50,30029,441447,30,30029,441447,40,30029,441483,0,30035)
%
%
% START OF PROOF
% 441448 [] equal(X,X).
% 441449 [] equal(multiply(identity,X),X).
% 441450 [] equal(multiply(inverse(X),X),identity).
% 441451 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 441452 [] -equal(multiply(sk_c8,X),sk_c7) | -equal(multiply(Y,sk_c8),X) | -equal(inverse(Y),sk_c8).
% 441453 [] equal(multiply(sk_c5,sk_c6),sk_c7) | equal(inverse(sk_c2),sk_c8).
% 441454 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c5),sk_c7).
% 441455 [] equal(multiply(sk_c4,sk_c7),sk_c8) | equal(inverse(sk_c2),sk_c8).
% 441456 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c4),sk_c8).
% 441457 [] equal(multiply(sk_c6,sk_c8),sk_c7) | equal(inverse(sk_c2),sk_c8).
% 441458 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c7),sk_c6).
% 441459 [] equal(multiply(sk_c2,sk_c8),sk_c3) | equal(multiply(sk_c5,sk_c6),sk_c7).
% 441460 [] equal(multiply(sk_c2,sk_c8),sk_c3) | equal(inverse(sk_c5),sk_c7).
% 441461 [] equal(multiply(sk_c2,sk_c8),sk_c3) | equal(multiply(sk_c4,sk_c7),sk_c8).
% 441462 [] equal(multiply(sk_c2,sk_c8),sk_c3) | equal(inverse(sk_c4),sk_c8).
% 441463 [] equal(multiply(sk_c2,sk_c8),sk_c3) | equal(multiply(sk_c6,sk_c8),sk_c7).
% 441464 [] equal(multiply(sk_c2,sk_c8),sk_c3) | equal(inverse(sk_c7),sk_c6).
% 441465 [?] ?
% 441466 [?] ?
% 441467 [?] ?
% 441468 [?] ?
% 441469 [?] ?
% 441470 [?] ?
% 441483 [] equal(multiply(sk_c7,sk_c8),sk_c6).
% 441532 [hyper:441452,441460,binarycut:441466,binarycut:441454] equal(inverse(sk_c5),sk_c7).
% 441533 [para:441532.1.1,441450.1.1.1] equal(multiply(sk_c7,sk_c5),identity).
% 441539 [hyper:441452,441459,441453,binarycut:441465] equal(multiply(sk_c5,sk_c6),sk_c7).
% 441542 [hyper:441452,441462,binarycut:441468,binarycut:441456] equal(inverse(sk_c4),sk_c8).
% 441549 [para:441542.1.1,441450.1.1.1] equal(multiply(sk_c8,sk_c4),identity).
% 441554 [hyper:441452,441464,binarycut:441470,binarycut:441458] equal(inverse(sk_c7),sk_c6).
% 441558 [hyper:441452,441461,441455,binarycut:441467] equal(multiply(sk_c4,sk_c7),sk_c8).
% 441559 [para:441554.1.1,441450.1.1.1] equal(multiply(sk_c6,sk_c7),identity).
% 441566 [hyper:441452,441463,441457,binarycut:441469] equal(multiply(sk_c6,sk_c8),sk_c7).
% 441571 [para:441483.1.1,441451.1.1.1] equal(multiply(sk_c6,X),multiply(sk_c7,multiply(sk_c8,X))).
% 441572 [para:441450.1.1,441451.1.1.1,demod:441449] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 441573 [para:441533.1.1,441451.1.1.1,demod:441449] equal(X,multiply(sk_c7,multiply(sk_c5,X))).
% 441575 [para:441549.1.1,441451.1.1.1,demod:441449] equal(X,multiply(sk_c8,multiply(sk_c4,X))).
% 441576 [para:441558.1.1,441451.1.1.1] equal(multiply(sk_c8,X),multiply(sk_c4,multiply(sk_c7,X))).
% 441584 [para:441539.1.1,441573.1.2.2] equal(sk_c6,multiply(sk_c7,sk_c7)).
% 441588 [para:441558.1.1,441575.1.2.2] equal(sk_c7,multiply(sk_c8,sk_c8)).
% 441591 [para:441588.1.2,441571.1.2.2,demod:441584,441566] equal(sk_c7,sk_c6).
% 441594 [para:441591.1.1,441558.1.1.2] equal(multiply(sk_c4,sk_c6),sk_c8).
% 441595 [para:441591.1.1,441559.1.1.2] equal(multiply(sk_c6,sk_c6),identity).
% 441598 [para:441591.1.1,441584.1.2.1,demod:441559] equal(sk_c6,identity).
% 441601 [para:441483.1.1,441572.1.2.2,demod:441595,441554] equal(sk_c8,identity).
% 441609 [para:441584.1.2,441572.1.2.2,demod:441595,441554] equal(sk_c7,identity).
% 441612 [para:441598.1.1,441566.1.1.1,demod:441449] equal(sk_c8,sk_c7).
% 441614 [para:441601.1.1,441549.1.1.1,demod:441449] equal(sk_c4,identity).
% 441623 [para:441609.1.1,441554.1.1.1] equal(inverse(identity),sk_c6).
% 441630 [para:441612.1.2,441554.1.1.1] equal(inverse(sk_c8),sk_c6).
% 441632 [para:441614.1.1,441542.1.1.1,demod:441623] equal(sk_c6,sk_c8).
% 441634 [hyper:441452,441576,demod:441630,441588,441594,441483,cut:441448,cut:441632] 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 23
% 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(inverse(sk_c7),sk_c6) | -equal(multiply(sk_c6,sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8) | -equal(inverse(V),sk_c7) | -equal(multiply(V,sk_c6),sk_c7).
% 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 23
% 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 23
% clause depth limited to 4
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(36,40,1,77,0,2,101989,5,1503,101989,1,1503,101989,50,1503,101989,40,1503,102030,0,1503,113421,3,1805,114086,4,1954,114699,5,2104,114700,1,2104,114700,50,2104,114700,40,2104,114741,0,2104,115159,3,2408,115179,4,2575,115187,5,2705,115187,1,2705,115187,50,2705,115187,40,2705,115228,0,2705,142059,3,4206,142784,4,4956,143371,1,5706,143371,50,5707,143371,40,5707,143412,0,5707,159834,3,6458,160538,4,6833,160854,1,7208,160854,50,7208,160854,40,7208,160895,0,7208,176689,3,7961,177371,4,8334,178151,1,8713,178151,50,8714,178151,40,8714,178192,0,8714,256553,3,12616,257538,4,14565,258150,1,16516,258150,50,16518,258150,40,16518,258191,0,16518,306680,3,19071,307543,4,20344,308445,1,21619,308445,50,21620,308445,40,21620,308486,0,21620,355704,3,23123,356393,4,23871,357119,5,24621,357120,1,24621,357120,50,24623,357120,40,24623,357161,0,24623,367926,3,25376,368877,4,25749,369393,5,26124,369394,1,26124,369394,50,26124,369394,40,26124,369435,0,26124,413406,3,27325,413945,4,27925,414458,5,28525,414459,1,28525,414459,50,28527,414459,40,28527,414500,0,28527,439944,3,29278,440563,4,29653,441142,5,30028,441143,1,30028,441143,50,30029,441143,40,30029,441143,40,30029,441179,0,30029,441271,50,30029,441271,30,30029,441271,40,30029,441307,0,30029,441447,50,30029,441447,30,30029,441447,40,30029,441483,0,30035,441633,50,30036,441633,30,30036,441633,40,30036,441669,0,30036,441764,50,30036,441800,0,30036)
%
%
% START OF PROOF
% 441737 [?] ?
% 441769 [] -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7).
% 441790 [] equal(multiply(sk_c4,sk_c7),sk_c8) | equal(inverse(sk_c1),sk_c7).
% 441791 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c4),sk_c8).
% 441796 [?] ?
% 441797 [?] ?
% 441817 [hyper:441769,441791,binarycut:441797] equal(inverse(sk_c4),sk_c8).
% 441832 [hyper:441769,441790,binarycut:441796] equal(multiply(sk_c4,sk_c7),sk_c8).
% 441838 [hyper:441769,441832,demod:441817,cut:441737] 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 23
% 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(inverse(sk_c7),sk_c6) | -equal(multiply(sk_c6,sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8) | -equal(inverse(V),sk_c7) | -equal(multiply(V,sk_c6),sk_c7).
% 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 23
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(36,40,1,77,0,2,101989,5,1503,101989,1,1503,101989,50,1503,101989,40,1503,102030,0,1503,113421,3,1805,114086,4,1954,114699,5,2104,114700,1,2104,114700,50,2104,114700,40,2104,114741,0,2104,115159,3,2408,115179,4,2575,115187,5,2705,115187,1,2705,115187,50,2705,115187,40,2705,115228,0,2705,142059,3,4206,142784,4,4956,143371,1,5706,143371,50,5707,143371,40,5707,143412,0,5707,159834,3,6458,160538,4,6833,160854,1,7208,160854,50,7208,160854,40,7208,160895,0,7208,176689,3,7961,177371,4,8334,178151,1,8713,178151,50,8714,178151,40,8714,178192,0,8714,256553,3,12616,257538,4,14565,258150,1,16516,258150,50,16518,258150,40,16518,258191,0,16518,306680,3,19071,307543,4,20344,308445,1,21619,308445,50,21620,308445,40,21620,308486,0,21620,355704,3,23123,356393,4,23871,357119,5,24621,357120,1,24621,357120,50,24623,357120,40,24623,357161,0,24623,367926,3,25376,368877,4,25749,369393,5,26124,369394,1,26124,369394,50,26124,369394,40,26124,369435,0,26124,413406,3,27325,413945,4,27925,414458,5,28525,414459,1,28525,414459,50,28527,414459,40,28527,414500,0,28527,439944,3,29278,440563,4,29653,441142,5,30028,441143,1,30028,441143,50,30029,441143,40,30029,441143,40,30029,441179,0,30029,441271,50,30029,441271,30,30029,441271,40,30029,441307,0,30029,441447,50,30029,441447,30,30029,441447,40,30029,441483,0,30035,441633,50,30036,441633,30,30036,441633,40,30036,441669,0,30036,441764,50,30036,441800,0,30036,441837,50,30036,441837,30,30036,441837,40,30036,441873,0,30041)
%
%
% START OF PROOF
% 441842 [] -equal(multiply(sk_c7,sk_c8),sk_c6).
% 441873 [] equal(multiply(sk_c7,sk_c8),sk_c6).
% 441874 [hyper:441842,441873] 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 23
% clause depth limited to 3
% seconds given: 4
%
%
% 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(inverse(sk_c7),sk_c6) | -equal(multiply(sk_c6,sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8) | -equal(inverse(V),sk_c7) | -equal(multiply(V,sk_c6),sk_c7).
% Split part used next: -equal(inverse(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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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(36,40,1,77,0,2,101989,5,1503,101989,1,1503,101989,50,1503,101989,40,1503,102030,0,1503,113421,3,1805,114086,4,1954,114699,5,2104,114700,1,2104,114700,50,2104,114700,40,2104,114741,0,2104,115159,3,2408,115179,4,2575,115187,5,2705,115187,1,2705,115187,50,2705,115187,40,2705,115228,0,2705,142059,3,4206,142784,4,4956,143371,1,5706,143371,50,5707,143371,40,5707,143412,0,5707,159834,3,6458,160538,4,6833,160854,1,7208,160854,50,7208,160854,40,7208,160895,0,7208,176689,3,7961,177371,4,8334,178151,1,8713,178151,50,8714,178151,40,8714,178192,0,8714,256553,3,12616,257538,4,14565,258150,1,16516,258150,50,16518,258150,40,16518,258191,0,16518,306680,3,19071,307543,4,20344,308445,1,21619,308445,50,21620,308445,40,21620,308486,0,21620,355704,3,23123,356393,4,23871,357119,5,24621,357120,1,24621,357120,50,24623,357120,40,24623,357161,0,24623,367926,3,25376,368877,4,25749,369393,5,26124,369394,1,26124,369394,50,26124,369394,40,26124,369435,0,26124,413406,3,27325,413945,4,27925,414458,5,28525,414459,1,28525,414459,50,28527,414459,40,28527,414500,0,28527,439944,3,29278,440563,4,29653,441142,5,30028,441143,1,30028,441143,50,30029,441143,40,30029,441143,40,30029,441179,0,30029,441271,50,30029,441271,30,30029,441271,40,30029,441307,0,30029,441447,50,30029,441447,30,30029,441447,40,30029,441483,0,30035,441633,50,30036,441633,30,30036,441633,40,30036,441669,0,30036,441764,50,30036,441800,0,30036,441837,50,30036,441837,30,30036,441837,40,30036,441873,0,30041,441873,50,30041,441873,30,30041,441873,40,30041,441909,0,30041,442044,50,30042,442080,0,30046,442259,50,30050,442295,0,30050,442482,50,30054,442518,0,30054,442713,50,30061,442749,0,30065,442950,50,30074,442986,0,30074,443195,50,30092,443231,0,30096,443448,50,30128,443484,0,30128,443711,50,30195,443747,0,30195,443984,50,30319,443984,40,30319,444020,0,30319)
%
%
% START OF PROOF
% 443986 [] equal(multiply(identity,X),X).
% 443987 [] equal(multiply(inverse(X),X),identity).
% 443988 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 443989 [] -equal(inverse(sk_c7),sk_c6).
% 443995 [?] ?
% 444001 [?] ?
% 444007 [?] ?
% 444013 [?] ?
% 444019 [?] ?
% 444020 [] equal(multiply(sk_c7,sk_c8),sk_c6).
% 444029 [input:443995,cut:443989] equal(inverse(sk_c2),sk_c8).
% 444030 [para:444029.1.1,443987.1.1.1] equal(multiply(sk_c8,sk_c2),identity).
% 444038 [input:444013,cut:443989] equal(inverse(sk_c1),sk_c7).
% 444039 [para:444038.1.1,443987.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 444046 [input:444001,cut:443989] equal(multiply(sk_c2,sk_c8),sk_c3).
% 444051 [input:444007,cut:443989] equal(multiply(sk_c8,sk_c3),sk_c7).
% 444061 [input:444019,cut:443989] equal(multiply(sk_c1,sk_c7),sk_c8).
% 444073 [para:444020.1.1,443988.1.1.1] equal(multiply(sk_c6,X),multiply(sk_c7,multiply(sk_c8,X))).
% 444074 [para:443987.1.1,443988.1.1.1,demod:443986] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 444076 [para:444030.1.1,443988.1.1.1,demod:443986] equal(X,multiply(sk_c8,multiply(sk_c2,X))).
% 444078 [para:444039.1.1,443988.1.1.1,demod:443986] equal(X,multiply(sk_c7,multiply(sk_c1,X))).
% 444087 [para:444051.1.1,443988.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c8,multiply(sk_c3,X))).
% 444110 [para:444046.1.1,444076.1.2.2] equal(sk_c8,multiply(sk_c8,sk_c3)).
% 444113 [para:444110.1.2,444051.1.1] equal(sk_c8,sk_c7).
% 444114 [para:444110.1.2,443988.1.1.1,demod:444087] equal(multiply(sk_c8,X),multiply(sk_c7,X)).
% 444115 [para:444113.1.2,443989.1.1.1] -equal(inverse(sk_c8),sk_c6).
% 444123 [para:444113.1.2,444061.1.1.2] equal(multiply(sk_c1,sk_c8),sk_c8).
% 444135 [para:444061.1.1,444078.1.2.2,demod:444020] equal(sk_c7,sk_c6).
% 444136 [para:444123.1.1,444078.1.2.2,demod:444020] equal(sk_c8,sk_c6).
% 444138 [para:444135.1.1,444020.1.1.1] equal(multiply(sk_c6,sk_c8),sk_c6).
% 444140 [para:444135.1.1,444039.1.1.1] equal(multiply(sk_c6,sk_c1),identity).
% 444166 [para:444136.1.1,444076.1.2.1] equal(X,multiply(sk_c6,multiply(sk_c2,X))).
% 444186 [para:444135.1.1,444114.1.2.1] equal(multiply(sk_c8,X),multiply(sk_c6,X)).
% 444199 [para:444076.1.2,444073.1.2.2,demod:444186,444114,444166] equal(X,multiply(sk_c6,X)).
% 444202 [para:444199.1.2,444140.1.1] equal(sk_c1,identity).
% 444209 [para:444202.1.1,444038.1.1.1] equal(inverse(identity),sk_c7).
% 444251 [para:444138.1.1,444074.1.2.2,demod:443987] equal(sk_c8,identity).
% 444284 [para:444251.1.1,444115.1.1.1,demod:444209,cut:444135] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% Split component 7 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_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(inverse(sk_c7),sk_c6) | -equal(multiply(sk_c6,sk_c8),sk_c7) | -equal(inverse(U),sk_c8) | -equal(multiply(U,sk_c7),sk_c8) | -equal(inverse(V),sk_c7) | -equal(multiply(V,sk_c6),sk_c7).
% Split part used next: -equal(multiply(sk_c6,sk_c8),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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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(36,40,1,77,0,2,101989,5,1503,101989,1,1503,101989,50,1503,101989,40,1503,102030,0,1503,113421,3,1805,114086,4,1954,114699,5,2104,114700,1,2104,114700,50,2104,114700,40,2104,114741,0,2104,115159,3,2408,115179,4,2575,115187,5,2705,115187,1,2705,115187,50,2705,115187,40,2705,115228,0,2705,142059,3,4206,142784,4,4956,143371,1,5706,143371,50,5707,143371,40,5707,143412,0,5707,159834,3,6458,160538,4,6833,160854,1,7208,160854,50,7208,160854,40,7208,160895,0,7208,176689,3,7961,177371,4,8334,178151,1,8713,178151,50,8714,178151,40,8714,178192,0,8714,256553,3,12616,257538,4,14565,258150,1,16516,258150,50,16518,258150,40,16518,258191,0,16518,306680,3,19071,307543,4,20344,308445,1,21619,308445,50,21620,308445,40,21620,308486,0,21620,355704,3,23123,356393,4,23871,357119,5,24621,357120,1,24621,357120,50,24623,357120,40,24623,357161,0,24623,367926,3,25376,368877,4,25749,369393,5,26124,369394,1,26124,369394,50,26124,369394,40,26124,369435,0,26124,413406,3,27325,413945,4,27925,414458,5,28525,414459,1,28525,414459,50,28527,414459,40,28527,414500,0,28527,439944,3,29278,440563,4,29653,441142,5,30028,441143,1,30028,441143,50,30029,441143,40,30029,441143,40,30029,441179,0,30029,441271,50,30029,441271,30,30029,441271,40,30029,441307,0,30029,441447,50,30029,441447,30,30029,441447,40,30029,441483,0,30035,441633,50,30036,441633,30,30036,441633,40,30036,441669,0,30036,441764,50,30036,441800,0,30036,441837,50,30036,441837,30,30036,441837,40,30036,441873,0,30041,441873,50,30041,441873,30,30041,441873,40,30041,441909,0,30041,442044,50,30042,442080,0,30046,442259,50,30050,442295,0,30050,442482,50,30054,442518,0,30054,442713,50,30061,442749,0,30065,442950,50,30074,442986,0,30074,443195,50,30092,443231,0,30096,443448,50,30128,443484,0,30128,443711,50,30195,443747,0,30195,443984,50,30319,443984,40,30319,444020,0,30319,444283,50,30320,444283,30,30320,444283,40,30320,444319,0,30320,444454,50,30321,444490,0,30326,444669,50,30329,444705,0,30329,444892,50,30334,444928,0,30334,445123,50,30340,445159,0,30345,445360,50,30355,445396,0,30355,445605,50,30372,445641,0,30377,445858,50,30408,445894,0,30408,446121,50,30475,446157,0,30475,446394,50,30598,446394,40,30598,446430,0,30598)
%
%
% START OF PROOF
% 446245 [?] ?
% 446396 [] equal(multiply(identity,X),X).
% 446397 [] equal(multiply(inverse(X),X),identity).
% 446398 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 446399 [] -equal(multiply(sk_c6,sk_c8),sk_c7).
% 446404 [?] ?
% 446410 [?] ?
% 446416 [?] ?
% 446453 [input:446404,cut:446399] equal(inverse(sk_c2),sk_c8).
% 446454 [para:446453.1.1,446397.1.1.1] equal(multiply(sk_c8,sk_c2),identity).
% 446479 [input:446410,cut:446399] equal(multiply(sk_c2,sk_c8),sk_c3).
% 446488 [input:446416,cut:446399] equal(multiply(sk_c8,sk_c3),sk_c7).
% 446500 [para:446454.1.1,446398.1.1.1,demod:446396] equal(X,multiply(sk_c8,multiply(sk_c2,X))).
% 446541 [para:446479.1.1,446500.1.2.2] equal(sk_c8,multiply(sk_c8,sk_c3)).
% 446547 [para:446541.1.2,446488.1.1] equal(sk_c8,sk_c7).
% 446549 [para:446547.1.2,446399.1.2,cut:446245] 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: 31210
% derived clauses: 5680876
% kept clauses: 310551
% kept size sum: 27798
% kept mid-nuclei: 101475
% kept new demods: 4295
% forw unit-subs: 1838817
% forw double-subs: 3013136
% forw overdouble-subs: 374182
% backward subs: 11059
% fast unit cutoff: 25459
% full unit cutoff: 0
% dbl unit cutoff: 4663
% real runtime : 308.90
% process. runtime: 305.98
% specific non-discr-tree subsumption statistics:
% tried: 33867961
% length fails: 4176277
% strength fails: 12501734
% predlist fails: 1367280
% aux str. fails: 2826929
% by-lit fails: 6389108
% full subs tried: 1816017
% full subs fail: 1655826
%
% ; 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/GRP327-1+eq_r.in")
%
%------------------------------------------------------------------------------