%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP345-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 : art10.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.0s
% Output : Assurance 298.0s
% 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/GRP345-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_c6,sk_c7),sk_c5) | -equal(inverse(X),sk_c7) | -equal(multiply(X,sk_c6),sk_c7) | -equal(inverse(Y),sk_c6) | -equal(multiply(Y,sk_c5),sk_c6) | -equal(multiply(sk_c6,sk_c5),sk_c7) | -equal(multiply(Z,sk_c7),sk_c6) | -equal(inverse(Z),sk_c7) | -equal(inverse(sk_c6),sk_c5) | -equal(multiply(U,sk_c6),sk_c5) | -equal(inverse(U),sk_c6).
% was split for some strategies as:
% -equal(multiply(U,sk_c6),sk_c5) | -equal(inverse(U),sk_c6).
% -equal(multiply(Z,sk_c7),sk_c6) | -equal(inverse(Z),sk_c7).
% -equal(inverse(Y),sk_c6) | -equal(multiply(Y,sk_c5),sk_c6).
% -equal(inverse(X),sk_c7) | -equal(multiply(X,sk_c6),sk_c7).
% -equal(multiply(sk_c6,sk_c7),sk_c5).
% -equal(multiply(sk_c6,sk_c5),sk_c7).
% -equal(inverse(sk_c6),sk_c5).
%
% Starting a split proof attempt with 7 components.
%
% Split component 1 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(inverse(X),sk_c7) | -equal(multiply(X,sk_c6),sk_c7) | -equal(inverse(Y),sk_c6) | -equal(multiply(Y,sk_c5),sk_c6) | -equal(multiply(sk_c6,sk_c5),sk_c7) | -equal(multiply(Z,sk_c7),sk_c6) | -equal(inverse(Z),sk_c7) | -equal(inverse(sk_c6),sk_c5) | -equal(multiply(U,sk_c6),sk_c5) | -equal(inverse(U),sk_c6).
% Split part used next: -equal(multiply(U,sk_c6),sk_c5) | -equal(inverse(U),sk_c6).
% END OF PROOFPART
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,0,75,0,0,551,50,3,591,0,3,1082,50,6,1122,0,6,1619,50,11,1659,0,11,2162,50,17,2202,0,17,2712,50,23,2752,0,23,3270,50,35,3310,0,35,3837,50,59,3877,0,59,4414,50,113,4454,0,113,5001,50,232,5041,0,232,5600,50,429,5640,0,429,6211,50,803,6211,40,803,6251,0,803,16629,3,1104,17373,4,1254,18067,1,1404,18067,50,1404,18067,40,1404,18107,0,1404,18263,3,1712,18271,4,1855,18279,5,2005,18279,1,2005,18279,50,2005,18279,40,2005,18319,0,2005,43168,3,3512,44423,4,4256,45601,5,5006,45602,1,5006,45602,50,5006,45602,40,5006,45642,0,5007,61173,3,5759,62089,4,6133,62987,1,6508,62987,50,6508,62987,40,6508,63027,0,6508,71721,3,7260,72927,4,7634,74007,5,8009,74008,1,8009,74008,50,8009,74008,40,8009,74048,0,8009,129135,3,11910,130436,4,13860,131553,1,15810,131553,50,15812,131553,40,15812,131593,0,15812,177735,3,18364,178787,4,19638,179656,1,20913,179656,50,20915,179656,40,20915,179696,0,20915,214348,3,22416,215322,4,23166,216206,5,23916,216207,1,23916,216207,50,23918,216207,40,23918,216247,0,23918,226572,3,24669,227471,4,25045,227561,5,25419,227561,1,25419,227561,50,25419,227561,40,25419,227601,0,25419,257011,3,26621,257867,4,27220,258372,1,27820,258372,50,27821,258372,40,27821,258412,0,27821,278065,3,28572,278831,4,28947,279134,1,29322,279134,50,29322,279134,40,29322,279134,40,29322,279169,0,29322)
%
%
% START OF PROOF
% 279136 [] equal(multiply(identity,X),X).
% 279137 [] equal(multiply(inverse(X),X),identity).
% 279138 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 279139 [] -equal(multiply(X,sk_c6),sk_c5) | -equal(inverse(X),sk_c6).
% 279140 [] equal(multiply(sk_c2,sk_c5),sk_c6) | equal(inverse(sk_c4),sk_c6).
% 279141 [] equal(multiply(sk_c2,sk_c5),sk_c6) | equal(multiply(sk_c4,sk_c6),sk_c5).
% 279146 [] equal(inverse(sk_c2),sk_c6) | equal(inverse(sk_c4),sk_c6).
% 279147 [?] ?
% 279152 [] equal(multiply(sk_c1,sk_c6),sk_c7) | equal(inverse(sk_c4),sk_c6).
% 279153 [] equal(multiply(sk_c1,sk_c6),sk_c7) | equal(multiply(sk_c4,sk_c6),sk_c5).
% 279158 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c4),sk_c6).
% 279159 [?] ?
% 279164 [] equal(multiply(sk_c6,sk_c7),sk_c5) | equal(inverse(sk_c4),sk_c6).
% 279165 [] equal(multiply(sk_c6,sk_c7),sk_c5) | equal(multiply(sk_c4,sk_c6),sk_c5).
% 279173 [hyper:279139,279146,binarycut:279147] equal(inverse(sk_c2),sk_c6).
% 279175 [para:279173.1.1,279137.1.1.1] equal(multiply(sk_c6,sk_c2),identity).
% 279179 [hyper:279139,279158,binarycut:279159] equal(inverse(sk_c1),sk_c7).
% 279180 [para:279179.1.1,279137.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 279186 [hyper:279139,279141,279140] equal(multiply(sk_c2,sk_c5),sk_c6).
% 279192 [hyper:279139,279153,279152] equal(multiply(sk_c1,sk_c6),sk_c7).
% 279198 [hyper:279139,279165,279164] equal(multiply(sk_c6,sk_c7),sk_c5).
% 279199 [para:279137.1.1,279138.1.1.1,demod:279136] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 279200 [para:279175.1.1,279138.1.1.1,demod:279136] equal(X,multiply(sk_c6,multiply(sk_c2,X))).
% 279201 [para:279180.1.1,279138.1.1.1,demod:279136] equal(X,multiply(sk_c7,multiply(sk_c1,X))).
% 279203 [para:279192.1.1,279138.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c1,multiply(sk_c6,X))).
% 279205 [para:279186.1.1,279200.1.2.2] equal(sk_c5,multiply(sk_c6,sk_c6)).
% 279207 [para:279192.1.1,279201.1.2.2] equal(sk_c6,multiply(sk_c7,sk_c7)).
% 279211 [para:279180.1.1,279199.1.2.2] equal(sk_c1,multiply(inverse(sk_c7),identity)).
% 279212 [para:279198.1.1,279199.1.2.2] equal(sk_c7,multiply(inverse(sk_c6),sk_c5)).
% 279214 [para:279205.1.2,279199.1.2.2,demod:279212] equal(sk_c6,sk_c7).
% 279216 [para:279214.1.1,279175.1.1.1] equal(multiply(sk_c7,sk_c2),identity).
% 279218 [para:279214.1.1,279198.1.1.1,demod:279207] equal(sk_c6,sk_c5).
% 279219 [para:279214.1.1,279200.1.2.1] equal(X,multiply(sk_c7,multiply(sk_c2,X))).
% 279232 [para:279216.1.1,279199.1.2.2,demod:279211] equal(sk_c2,sk_c1).
% 279234 [para:279200.1.2,279203.1.2.2,demod:279219] equal(X,multiply(sk_c1,X)).
% 279238 [para:279232.1.1,279200.1.2.2.1,demod:279234] equal(X,multiply(sk_c6,X)).
% 279240 [para:279238.1.2,279175.1.1] equal(sk_c2,identity).
% 279243 [para:279240.1.1,279173.1.1.1] equal(inverse(identity),sk_c6).
% 279246 [hyper:279139,279243,demod:279136,cut:279218] 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_c6,sk_c7),sk_c5) | -equal(inverse(X),sk_c7) | -equal(multiply(X,sk_c6),sk_c7) | -equal(inverse(Y),sk_c6) | -equal(multiply(Y,sk_c5),sk_c6) | -equal(multiply(sk_c6,sk_c5),sk_c7) | -equal(multiply(Z,sk_c7),sk_c6) | -equal(inverse(Z),sk_c7) | -equal(inverse(sk_c6),sk_c5) | -equal(multiply(U,sk_c6),sk_c5) | -equal(inverse(U),sk_c6).
% Split part used next: -equal(multiply(Z,sk_c7),sk_c6) | -equal(inverse(Z),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,551,50,3,591,0,3,1082,50,6,1122,0,6,1619,50,11,1659,0,11,2162,50,17,2202,0,17,2712,50,23,2752,0,23,3270,50,35,3310,0,35,3837,50,59,3877,0,59,4414,50,113,4454,0,113,5001,50,232,5041,0,232,5600,50,429,5640,0,429,6211,50,803,6211,40,803,6251,0,803,16629,3,1104,17373,4,1254,18067,1,1404,18067,50,1404,18067,40,1404,18107,0,1404,18263,3,1712,18271,4,1855,18279,5,2005,18279,1,2005,18279,50,2005,18279,40,2005,18319,0,2005,43168,3,3512,44423,4,4256,45601,5,5006,45602,1,5006,45602,50,5006,45602,40,5006,45642,0,5007,61173,3,5759,62089,4,6133,62987,1,6508,62987,50,6508,62987,40,6508,63027,0,6508,71721,3,7260,72927,4,7634,74007,5,8009,74008,1,8009,74008,50,8009,74008,40,8009,74048,0,8009,129135,3,11910,130436,4,13860,131553,1,15810,131553,50,15812,131553,40,15812,131593,0,15812,177735,3,18364,178787,4,19638,179656,1,20913,179656,50,20915,179656,40,20915,179696,0,20915,214348,3,22416,215322,4,23166,216206,5,23916,216207,1,23916,216207,50,23918,216207,40,23918,216247,0,23918,226572,3,24669,227471,4,25045,227561,5,25419,227561,1,25419,227561,50,25419,227561,40,25419,227601,0,25419,257011,3,26621,257867,4,27220,258372,1,27820,258372,50,27821,258372,40,27821,258412,0,27821,278065,3,28572,278831,4,28947,279134,1,29322,279134,50,29322,279134,40,29322,279134,40,29322,279169,0,29322,279245,50,29323,279245,30,29323,279245,40,29323,279280,0,29323,279391,50,29324,279426,0,29329)
%
%
% START OF PROOF
% 279393 [] equal(multiply(identity,X),X).
% 279394 [] equal(multiply(inverse(X),X),identity).
% 279395 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 279396 [] -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7).
% 279400 [] equal(multiply(sk_c2,sk_c5),sk_c6) | equal(inverse(sk_c3),sk_c7).
% 279401 [] equal(multiply(sk_c2,sk_c5),sk_c6) | equal(multiply(sk_c3,sk_c7),sk_c6).
% 279406 [] equal(inverse(sk_c2),sk_c6) | equal(inverse(sk_c3),sk_c7).
% 279407 [?] ?
% 279412 [] equal(multiply(sk_c1,sk_c6),sk_c7) | equal(inverse(sk_c3),sk_c7).
% 279413 [] equal(multiply(sk_c1,sk_c6),sk_c7) | equal(multiply(sk_c3,sk_c7),sk_c6).
% 279418 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c3),sk_c7).
% 279419 [?] ?
% 279424 [] equal(multiply(sk_c6,sk_c7),sk_c5) | equal(inverse(sk_c3),sk_c7).
% 279425 [] equal(multiply(sk_c6,sk_c7),sk_c5) | equal(multiply(sk_c3,sk_c7),sk_c6).
% 279432 [hyper:279396,279406,binarycut:279407] equal(inverse(sk_c2),sk_c6).
% 279433 [para:279432.1.1,279394.1.1.1] equal(multiply(sk_c6,sk_c2),identity).
% 279444 [hyper:279396,279418,binarycut:279419] equal(inverse(sk_c1),sk_c7).
% 279447 [para:279444.1.1,279394.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 279463 [hyper:279396,279401,279400] equal(multiply(sk_c2,sk_c5),sk_c6).
% 279470 [hyper:279396,279413,279412] equal(multiply(sk_c1,sk_c6),sk_c7).
% 279474 [hyper:279396,279425,279424] equal(multiply(sk_c6,sk_c7),sk_c5).
% 279475 [para:279394.1.1,279395.1.1.1,demod:279393] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 279476 [para:279433.1.1,279395.1.1.1,demod:279393] equal(X,multiply(sk_c6,multiply(sk_c2,X))).
% 279478 [para:279463.1.1,279395.1.1.1] equal(multiply(sk_c6,X),multiply(sk_c2,multiply(sk_c5,X))).
% 279479 [para:279470.1.1,279395.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c1,multiply(sk_c6,X))).
% 279481 [para:279463.1.1,279476.1.2.2] equal(sk_c5,multiply(sk_c6,sk_c6)).
% 279486 [para:279394.1.1,279475.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 279487 [para:279433.1.1,279475.1.2.2] equal(sk_c2,multiply(inverse(sk_c6),identity)).
% 279488 [para:279447.1.1,279475.1.2.2] equal(sk_c1,multiply(inverse(sk_c7),identity)).
% 279489 [para:279474.1.1,279475.1.2.2] equal(sk_c7,multiply(inverse(sk_c6),sk_c5)).
% 279490 [para:279395.1.1,279475.1.2.2] equal(X,multiply(inverse(multiply(Y,Z)),multiply(Y,multiply(Z,X)))).
% 279492 [para:279481.1.2,279475.1.2.2,demod:279489] equal(sk_c6,sk_c7).
% 279494 [para:279475.1.2,279475.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 279495 [para:279492.1.1,279433.1.1.1] equal(multiply(sk_c7,sk_c2),identity).
% 279496 [para:279492.1.1,279470.1.1.2] equal(multiply(sk_c1,sk_c7),sk_c7).
% 279498 [para:279492.1.1,279476.1.2.1] equal(X,multiply(sk_c7,multiply(sk_c2,X))).
% 279511 [para:279495.1.1,279475.1.2.2,demod:279488] equal(sk_c2,sk_c1).
% 279513 [para:279476.1.2,279479.1.2.2,demod:279498] equal(X,multiply(sk_c1,X)).
% 279517 [para:279511.1.1,279476.1.2.2.1,demod:279513] equal(X,multiply(sk_c6,X)).
% 279518 [para:279511.1.1,279478.1.2.1,demod:279513,279517] equal(X,multiply(sk_c5,X)).
% 279520 [para:279517.1.2,279476.1.2] equal(X,multiply(sk_c2,X)).
% 279525 [para:279518.1.2,279475.1.2.2] equal(X,multiply(inverse(sk_c5),X)).
% 279528 [para:279525.1.2,279394.1.1] equal(sk_c5,identity).
% 279534 [para:279528.1.1,279489.1.2.2,demod:279487] equal(sk_c7,sk_c2).
% 279537 [para:279534.1.1,279496.1.1.2,demod:279513] equal(sk_c2,sk_c7).
% 279547 [para:279476.1.2,279490.1.2.2.2,demod:279520] equal(X,multiply(inverse(multiply(Y,sk_c6)),multiply(Y,X))).
% 279554 [para:279494.1.2,279486.1.2] equal(X,multiply(X,identity)).
% 279555 [para:279394.1.1,279547.1.2.2,demod:279554] equal(X,inverse(multiply(inverse(X),sk_c6))).
% 279557 [para:279554.1.2,279486.1.2] equal(X,inverse(inverse(X))).
% 279558 [para:279554.1.2,279487.1.2] equal(sk_c2,inverse(sk_c6)).
% 279566 [para:279555.1.2,279486.1.2.1.1,demod:279554] equal(multiply(inverse(X),sk_c6),inverse(X)).
% 279581 [para:279566.1.1,279494.1.2,demod:279557] equal(multiply(X,sk_c6),X).
% 279582 [para:279492.1.1,279581.1.1.2] equal(multiply(X,sk_c7),X).
% 279583 [hyper:279396,279582,demod:279558,cut:279537] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 4
% seconds given: 4
%
%
% Split component 3 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(inverse(X),sk_c7) | -equal(multiply(X,sk_c6),sk_c7) | -equal(inverse(Y),sk_c6) | -equal(multiply(Y,sk_c5),sk_c6) | -equal(multiply(sk_c6,sk_c5),sk_c7) | -equal(multiply(Z,sk_c7),sk_c6) | -equal(inverse(Z),sk_c7) | -equal(inverse(sk_c6),sk_c5) | -equal(multiply(U,sk_c6),sk_c5) | -equal(inverse(U),sk_c6).
% Split part used next: -equal(inverse(Y),sk_c6) | -equal(multiply(Y,sk_c5),sk_c6).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,0,75,0,0,551,50,3,591,0,3,1082,50,6,1122,0,6,1619,50,11,1659,0,11,2162,50,17,2202,0,17,2712,50,23,2752,0,23,3270,50,35,3310,0,35,3837,50,59,3877,0,59,4414,50,113,4454,0,113,5001,50,232,5041,0,232,5600,50,429,5640,0,429,6211,50,803,6211,40,803,6251,0,803,16629,3,1104,17373,4,1254,18067,1,1404,18067,50,1404,18067,40,1404,18107,0,1404,18263,3,1712,18271,4,1855,18279,5,2005,18279,1,2005,18279,50,2005,18279,40,2005,18319,0,2005,43168,3,3512,44423,4,4256,45601,5,5006,45602,1,5006,45602,50,5006,45602,40,5006,45642,0,5007,61173,3,5759,62089,4,6133,62987,1,6508,62987,50,6508,62987,40,6508,63027,0,6508,71721,3,7260,72927,4,7634,74007,5,8009,74008,1,8009,74008,50,8009,74008,40,8009,74048,0,8009,129135,3,11910,130436,4,13860,131553,1,15810,131553,50,15812,131553,40,15812,131593,0,15812,177735,3,18364,178787,4,19638,179656,1,20913,179656,50,20915,179656,40,20915,179696,0,20915,214348,3,22416,215322,4,23166,216206,5,23916,216207,1,23916,216207,50,23918,216207,40,23918,216247,0,23918,226572,3,24669,227471,4,25045,227561,5,25419,227561,1,25419,227561,50,25419,227561,40,25419,227601,0,25419,257011,3,26621,257867,4,27220,258372,1,27820,258372,50,27821,258372,40,27821,258412,0,27821,278065,3,28572,278831,4,28947,279134,1,29322,279134,50,29322,279134,40,29322,279134,40,29322,279169,0,29322,279245,50,29323,279245,30,29323,279245,40,29323,279280,0,29323,279391,50,29324,279426,0,29329,279582,50,29330,279582,30,29330,279582,40,29330,279617,0,29330)
%
%
% START OF PROOF
% 279584 [] equal(multiply(identity,X),X).
% 279585 [] equal(multiply(inverse(X),X),identity).
% 279586 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 279587 [] -equal(multiply(X,sk_c5),sk_c6) | -equal(inverse(X),sk_c6).
% 279588 [?] ?
% 279589 [] equal(multiply(sk_c2,sk_c5),sk_c6) | equal(multiply(sk_c4,sk_c6),sk_c5).
% 279590 [?] ?
% 279593 [?] ?
% 279594 [] equal(inverse(sk_c2),sk_c6) | equal(inverse(sk_c4),sk_c6).
% 279595 [] equal(multiply(sk_c4,sk_c6),sk_c5) | equal(inverse(sk_c2),sk_c6).
% 279596 [] equal(inverse(sk_c2),sk_c6) | equal(inverse(sk_c6),sk_c5).
% 279599 [] equal(multiply(sk_c6,sk_c5),sk_c7) | equal(inverse(sk_c2),sk_c6).
% 279620 [hyper:279587,279594,binarycut:279588] equal(inverse(sk_c4),sk_c6).
% 279623 [para:279620.1.1,279585.1.1.1] equal(multiply(sk_c6,sk_c4),identity).
% 279627 [hyper:279587,279596,binarycut:279590] equal(inverse(sk_c6),sk_c5).
% 279628 [para:279627.1.1,279585.1.1.1] equal(multiply(sk_c5,sk_c6),identity).
% 279641 [hyper:279587,279595,binarycut:279589] equal(multiply(sk_c4,sk_c6),sk_c5).
% 279647 [hyper:279587,279599,binarycut:279593] equal(multiply(sk_c6,sk_c5),sk_c7).
% 279648 [para:279585.1.1,279586.1.1.1,demod:279584] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 279649 [para:279623.1.1,279586.1.1.1,demod:279584] equal(X,multiply(sk_c6,multiply(sk_c4,X))).
% 279655 [para:279641.1.1,279649.1.2.2,demod:279647] equal(sk_c6,sk_c7).
% 279658 [para:279655.1.1,279628.1.1.2] equal(multiply(sk_c5,sk_c7),identity).
% 279663 [para:279623.1.1,279648.1.2.2,demod:279627] equal(sk_c4,multiply(sk_c5,identity)).
% 279667 [para:279647.1.1,279648.1.2.2,demod:279658,279627] equal(sk_c5,identity).
% 279668 [para:279649.1.2,279648.1.2.2,demod:279627] equal(multiply(sk_c4,X),multiply(sk_c5,X)).
% 279674 [para:279667.1.1,279628.1.1.1,demod:279584] equal(sk_c6,identity).
% 279677 [para:279674.1.1,279623.1.1.1,demod:279584] equal(sk_c4,identity).
% 279678 [para:279674.1.1,279627.1.1.1] equal(inverse(identity),sk_c5).
% 279679 [para:279674.1.1,279641.1.1.2,demod:279663,279668] equal(sk_c4,sk_c5).
% 279681 [para:279674.1.1,279649.1.2.1,demod:279584,279668] equal(X,multiply(sk_c5,X)).
% 279684 [para:279677.1.1,279620.1.1.1,demod:279678] equal(sk_c5,sk_c6).
% 279689 [para:279679.1.1,279620.1.1.1] equal(inverse(sk_c5),sk_c6).
% 279699 [hyper:279587,279689,demod:279681,cut:279684] 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_c6,sk_c7),sk_c5) | -equal(inverse(X),sk_c7) | -equal(multiply(X,sk_c6),sk_c7) | -equal(inverse(Y),sk_c6) | -equal(multiply(Y,sk_c5),sk_c6) | -equal(multiply(sk_c6,sk_c5),sk_c7) | -equal(multiply(Z,sk_c7),sk_c6) | -equal(inverse(Z),sk_c7) | -equal(inverse(sk_c6),sk_c5) | -equal(multiply(U,sk_c6),sk_c5) | -equal(inverse(U),sk_c6).
% Split part used next: -equal(inverse(X),sk_c7) | -equal(multiply(X,sk_c6),sk_c7).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 4
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,0,75,0,0,551,50,3,591,0,3,1082,50,6,1122,0,6,1619,50,11,1659,0,11,2162,50,17,2202,0,17,2712,50,23,2752,0,23,3270,50,35,3310,0,35,3837,50,59,3877,0,59,4414,50,113,4454,0,113,5001,50,232,5041,0,232,5600,50,429,5640,0,429,6211,50,803,6211,40,803,6251,0,803,16629,3,1104,17373,4,1254,18067,1,1404,18067,50,1404,18067,40,1404,18107,0,1404,18263,3,1712,18271,4,1855,18279,5,2005,18279,1,2005,18279,50,2005,18279,40,2005,18319,0,2005,43168,3,3512,44423,4,4256,45601,5,5006,45602,1,5006,45602,50,5006,45602,40,5006,45642,0,5007,61173,3,5759,62089,4,6133,62987,1,6508,62987,50,6508,62987,40,6508,63027,0,6508,71721,3,7260,72927,4,7634,74007,5,8009,74008,1,8009,74008,50,8009,74008,40,8009,74048,0,8009,129135,3,11910,130436,4,13860,131553,1,15810,131553,50,15812,131553,40,15812,131593,0,15812,177735,3,18364,178787,4,19638,179656,1,20913,179656,50,20915,179656,40,20915,179696,0,20915,214348,3,22416,215322,4,23166,216206,5,23916,216207,1,23916,216207,50,23918,216207,40,23918,216247,0,23918,226572,3,24669,227471,4,25045,227561,5,25419,227561,1,25419,227561,50,25419,227561,40,25419,227601,0,25419,257011,3,26621,257867,4,27220,258372,1,27820,258372,50,27821,258372,40,27821,258412,0,27821,278065,3,28572,278831,4,28947,279134,1,29322,279134,50,29322,279134,40,29322,279134,40,29322,279169,0,29322,279245,50,29323,279245,30,29323,279245,40,29323,279280,0,29323,279391,50,29324,279426,0,29329,279582,50,29330,279582,30,29330,279582,40,29330,279617,0,29330,279698,50,29330,279698,30,29330,279698,40,29330,279733,0,29330,279828,50,29331,279863,0,29335)
%
%
% START OF PROOF
% 279830 [] equal(multiply(identity,X),X).
% 279831 [] equal(multiply(inverse(X),X),identity).
% 279832 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 279833 [] -equal(multiply(X,sk_c6),sk_c7) | -equal(inverse(X),sk_c7).
% 279846 [?] ?
% 279847 [?] ?
% 279848 [?] ?
% 279851 [?] ?
% 279852 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c4),sk_c6).
% 279853 [] equal(multiply(sk_c4,sk_c6),sk_c5) | equal(inverse(sk_c1),sk_c7).
% 279854 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c6),sk_c5).
% 279857 [] equal(multiply(sk_c6,sk_c5),sk_c7) | equal(inverse(sk_c1),sk_c7).
% 279872 [hyper:279833,279852,binarycut:279846] equal(inverse(sk_c4),sk_c6).
% 279873 [para:279872.1.1,279831.1.1.1] equal(multiply(sk_c6,sk_c4),identity).
% 279877 [hyper:279833,279854,binarycut:279848] equal(inverse(sk_c6),sk_c5).
% 279878 [para:279877.1.1,279831.1.1.1] equal(multiply(sk_c5,sk_c6),identity).
% 279893 [hyper:279833,279853,binarycut:279847] equal(multiply(sk_c4,sk_c6),sk_c5).
% 279899 [hyper:279833,279857,binarycut:279851] equal(multiply(sk_c6,sk_c5),sk_c7).
% 279900 [para:279831.1.1,279832.1.1.1,demod:279830] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 279901 [para:279873.1.1,279832.1.1.1,demod:279830] equal(X,multiply(sk_c6,multiply(sk_c4,X))).
% 279907 [para:279893.1.1,279901.1.2.2,demod:279899] equal(sk_c6,sk_c7).
% 279909 [para:279907.1.1,279877.1.1.1] equal(inverse(sk_c7),sk_c5).
% 279910 [para:279907.1.1,279878.1.1.2] equal(multiply(sk_c5,sk_c7),identity).
% 279915 [para:279831.1.1,279900.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 279920 [para:279899.1.1,279900.1.2.2,demod:279910,279877] equal(sk_c5,identity).
% 279921 [para:279832.1.1,279900.1.2.2] equal(X,multiply(inverse(multiply(Y,Z)),multiply(Y,multiply(Z,X)))).
% 279922 [para:279901.1.2,279900.1.2.2,demod:279877] equal(multiply(sk_c4,X),multiply(sk_c5,X)).
% 279924 [para:279900.1.2,279900.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 279929 [para:279920.1.1,279878.1.1.1,demod:279830] equal(sk_c6,identity).
% 279935 [para:279929.1.1,279899.1.1.1,demod:279830] equal(sk_c5,sk_c7).
% 279936 [para:279929.1.1,279901.1.2.1,demod:279830,279922] equal(X,multiply(sk_c5,X)).
% 279969 [para:279901.1.2,279921.1.2.2.2,demod:279936,279922] equal(X,multiply(inverse(multiply(Y,sk_c6)),multiply(Y,X))).
% 279975 [para:279924.1.2,279831.1.1] equal(multiply(X,inverse(X)),identity).
% 279977 [para:279924.1.2,279915.1.2] equal(X,multiply(X,identity)).
% 279980 [para:279977.1.2,279915.1.2] equal(X,inverse(inverse(X))).
% 279989 [para:279975.1.1,279969.1.2.2,demod:279977] equal(inverse(X),inverse(multiply(X,sk_c6))).
% 279998 [para:279989.1.2,279915.1.2.1.1,demod:279977,279980] equal(multiply(X,sk_c6),X).
% 280001 [hyper:279833,279998,demod:279909,cut:279935] 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_c6,sk_c7),sk_c5) | -equal(inverse(X),sk_c7) | -equal(multiply(X,sk_c6),sk_c7) | -equal(inverse(Y),sk_c6) | -equal(multiply(Y,sk_c5),sk_c6) | -equal(multiply(sk_c6,sk_c5),sk_c7) | -equal(multiply(Z,sk_c7),sk_c6) | -equal(inverse(Z),sk_c7) | -equal(inverse(sk_c6),sk_c5) | -equal(multiply(U,sk_c6),sk_c5) | -equal(inverse(U),sk_c6).
% Split part used next: -equal(multiply(sk_c6,sk_c7),sk_c5).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 4
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 5
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 6
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 7
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 8
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 9
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 10
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 11
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,0,75,0,0,551,50,3,591,0,3,1082,50,6,1122,0,6,1619,50,11,1659,0,11,2162,50,17,2202,0,17,2712,50,23,2752,0,23,3270,50,35,3310,0,35,3837,50,59,3877,0,59,4414,50,113,4454,0,113,5001,50,232,5041,0,232,5600,50,429,5640,0,429,6211,50,803,6211,40,803,6251,0,803,16629,3,1104,17373,4,1254,18067,1,1404,18067,50,1404,18067,40,1404,18107,0,1404,18263,3,1712,18271,4,1855,18279,5,2005,18279,1,2005,18279,50,2005,18279,40,2005,18319,0,2005,43168,3,3512,44423,4,4256,45601,5,5006,45602,1,5006,45602,50,5006,45602,40,5006,45642,0,5007,61173,3,5759,62089,4,6133,62987,1,6508,62987,50,6508,62987,40,6508,63027,0,6508,71721,3,7260,72927,4,7634,74007,5,8009,74008,1,8009,74008,50,8009,74008,40,8009,74048,0,8009,129135,3,11910,130436,4,13860,131553,1,15810,131553,50,15812,131553,40,15812,131593,0,15812,177735,3,18364,178787,4,19638,179656,1,20913,179656,50,20915,179656,40,20915,179696,0,20915,214348,3,22416,215322,4,23166,216206,5,23916,216207,1,23916,216207,50,23918,216207,40,23918,216247,0,23918,226572,3,24669,227471,4,25045,227561,5,25419,227561,1,25419,227561,50,25419,227561,40,25419,227601,0,25419,257011,3,26621,257867,4,27220,258372,1,27820,258372,50,27821,258372,40,27821,258412,0,27821,278065,3,28572,278831,4,28947,279134,1,29322,279134,50,29322,279134,40,29322,279134,40,29322,279169,0,29322,279245,50,29323,279245,30,29323,279245,40,29323,279280,0,29323,279391,50,29324,279426,0,29329,279582,50,29330,279582,30,29330,279582,40,29330,279617,0,29330,279698,50,29330,279698,30,29330,279698,40,29330,279733,0,29330,279828,50,29331,279863,0,29335,280000,50,29336,280000,30,29336,280000,40,29336,280035,0,29336,280134,50,29337,280169,0,29342,280315,50,29344,280350,0,29344,280506,50,29348,280541,0,29348,280709,50,29355,280744,0,29360,280918,50,29370,280953,0,29370,281135,50,29388,281170,0,29392,281361,50,29425,281396,0,29425,281597,50,29492,281632,0,29492,281844,50,29625,281844,40,29625,281879,0,29625)
%
%
% START OF PROOF
% 281716 [?] ?
% 281846 [] equal(multiply(identity,X),X).
% 281847 [] equal(multiply(inverse(X),X),identity).
% 281848 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 281849 [] -equal(multiply(sk_c6,sk_c7),sk_c5).
% 281874 [?] ?
% 281875 [?] ?
% 281876 [?] ?
% 281879 [?] ?
% 281925 [input:281874,cut:281849] equal(inverse(sk_c4),sk_c6).
% 281926 [para:281925.1.1,281847.1.1.1] equal(multiply(sk_c6,sk_c4),identity).
% 281927 [input:281876,cut:281849] equal(inverse(sk_c6),sk_c5).
% 281928 [para:281927.1.1,281847.1.1.1] equal(multiply(sk_c5,sk_c6),identity).
% 281938 [input:281875,cut:281849] equal(multiply(sk_c4,sk_c6),sk_c5).
% 281942 [input:281879,cut:281849] equal(multiply(sk_c6,sk_c5),sk_c7).
% 281963 [para:281926.1.1,281848.1.1.1,demod:281846] equal(X,multiply(sk_c6,multiply(sk_c4,X))).
% 281964 [para:281928.1.1,281848.1.1.1,demod:281846] equal(X,multiply(sk_c5,multiply(sk_c6,X))).
% 281986 [para:281938.1.1,281963.1.2.2] equal(sk_c6,multiply(sk_c6,sk_c5)).
% 281991 [para:281986.1.2,281942.1.1] equal(sk_c6,sk_c7).
% 282009 [para:281991.1.1,281928.1.1.2] equal(multiply(sk_c5,sk_c7),identity).
% 282037 [para:281942.1.1,281964.1.2.2,demod:282009] equal(sk_c5,identity).
% 282050 [para:282037.1.1,281928.1.1.1,demod:281846] equal(sk_c6,identity).
% 282055 [para:282050.1.1,281849.1.1.1,demod:281846,cut:281716] 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_c6,sk_c7),sk_c5) | -equal(inverse(X),sk_c7) | -equal(multiply(X,sk_c6),sk_c7) | -equal(inverse(Y),sk_c6) | -equal(multiply(Y,sk_c5),sk_c6) | -equal(multiply(sk_c6,sk_c5),sk_c7) | -equal(multiply(Z,sk_c7),sk_c6) | -equal(inverse(Z),sk_c7) | -equal(inverse(sk_c6),sk_c5) | -equal(multiply(U,sk_c6),sk_c5) | -equal(inverse(U),sk_c6).
% Split part used next: -equal(multiply(sk_c6,sk_c5),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
%
%
% 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,551,50,3,591,0,3,1082,50,6,1122,0,6,1619,50,11,1659,0,11,2162,50,17,2202,0,17,2712,50,23,2752,0,23,3270,50,35,3310,0,35,3837,50,59,3877,0,59,4414,50,113,4454,0,113,5001,50,232,5041,0,232,5600,50,429,5640,0,429,6211,50,803,6211,40,803,6251,0,803,16629,3,1104,17373,4,1254,18067,1,1404,18067,50,1404,18067,40,1404,18107,0,1404,18263,3,1712,18271,4,1855,18279,5,2005,18279,1,2005,18279,50,2005,18279,40,2005,18319,0,2005,43168,3,3512,44423,4,4256,45601,5,5006,45602,1,5006,45602,50,5006,45602,40,5006,45642,0,5007,61173,3,5759,62089,4,6133,62987,1,6508,62987,50,6508,62987,40,6508,63027,0,6508,71721,3,7260,72927,4,7634,74007,5,8009,74008,1,8009,74008,50,8009,74008,40,8009,74048,0,8009,129135,3,11910,130436,4,13860,131553,1,15810,131553,50,15812,131553,40,15812,131593,0,15812,177735,3,18364,178787,4,19638,179656,1,20913,179656,50,20915,179656,40,20915,179696,0,20915,214348,3,22416,215322,4,23166,216206,5,23916,216207,1,23916,216207,50,23918,216207,40,23918,216247,0,23918,226572,3,24669,227471,4,25045,227561,5,25419,227561,1,25419,227561,50,25419,227561,40,25419,227601,0,25419,257011,3,26621,257867,4,27220,258372,1,27820,258372,50,27821,258372,40,27821,258412,0,27821,278065,3,28572,278831,4,28947,279134,1,29322,279134,50,29322,279134,40,29322,279134,40,29322,279169,0,29322,279245,50,29323,279245,30,29323,279245,40,29323,279280,0,29323,279391,50,29324,279426,0,29329,279582,50,29330,279582,30,29330,279582,40,29330,279617,0,29330,279698,50,29330,279698,30,29330,279698,40,29330,279733,0,29330,279828,50,29331,279863,0,29335,280000,50,29336,280000,30,29336,280000,40,29336,280035,0,29336,280134,50,29337,280169,0,29342,280315,50,29344,280350,0,29344,280506,50,29348,280541,0,29348,280709,50,29355,280744,0,29360,280918,50,29370,280953,0,29370,281135,50,29388,281170,0,29392,281361,50,29425,281396,0,29425,281597,50,29492,281632,0,29492,281844,50,29625,281844,40,29625,281879,0,29625,282054,50,29625,282054,30,29625,282054,40,29625,282089,0,29625,282194,50,29626,282229,0,29631,282378,50,29633,282413,0,29633,282570,50,29637,282605,0,29637,282770,50,29643,282805,0,29647,282976,50,29656,283011,0,29656,283190,50,29672,283225,0,29676,283412,50,29706,283447,0,29706,283644,50,29768,283679,0,29768,283886,50,29887,283886,40,29887,283921,0,29887)
%
%
% START OF PROOF
% 283831 [?] ?
% 283888 [] equal(multiply(identity,X),X).
% 283889 [] equal(multiply(inverse(X),X),identity).
% 283890 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 283891 [] -equal(multiply(sk_c6,sk_c5),sk_c7).
% 283897 [?] ?
% 283903 [?] ?
% 283921 [?] ?
% 283951 [input:283903,cut:283891] equal(inverse(sk_c2),sk_c6).
% 283952 [para:283951.1.1,283889.1.1.1] equal(multiply(sk_c6,sk_c2),identity).
% 283962 [input:283897,cut:283891] equal(multiply(sk_c2,sk_c5),sk_c6).
% 283984 [input:283921,cut:283891] equal(multiply(sk_c6,sk_c7),sk_c5).
% 283988 [para:283889.1.1,283890.1.1.1,demod:283888] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 283998 [para:283952.1.1,283890.1.1.1,demod:283888] equal(X,multiply(sk_c6,multiply(sk_c2,X))).
% 284033 [para:283962.1.1,283998.1.2.2] equal(sk_c5,multiply(sk_c6,sk_c6)).
% 284085 [para:283984.1.1,283988.1.2.2] equal(sk_c7,multiply(inverse(sk_c6),sk_c5)).
% 284091 [para:284033.1.2,283988.1.2.2,demod:284085] equal(sk_c6,sk_c7).
% 284096 [para:284091.1.1,283891.1.1.1,cut:283831] 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_c6,sk_c7),sk_c5) | -equal(inverse(X),sk_c7) | -equal(multiply(X,sk_c6),sk_c7) | -equal(inverse(Y),sk_c6) | -equal(multiply(Y,sk_c5),sk_c6) | -equal(multiply(sk_c6,sk_c5),sk_c7) | -equal(multiply(Z,sk_c7),sk_c6) | -equal(inverse(Z),sk_c7) | -equal(inverse(sk_c6),sk_c5) | -equal(multiply(U,sk_c6),sk_c5) | -equal(inverse(U),sk_c6).
% Split part used next: -equal(inverse(sk_c6),sk_c5).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 4
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 5
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 6
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 7
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 8
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 9
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 10
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 11
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,0,75,0,0,551,50,3,591,0,3,1082,50,6,1122,0,6,1619,50,11,1659,0,11,2162,50,17,2202,0,17,2712,50,23,2752,0,23,3270,50,35,3310,0,35,3837,50,59,3877,0,59,4414,50,113,4454,0,113,5001,50,232,5041,0,232,5600,50,429,5640,0,429,6211,50,803,6211,40,803,6251,0,803,16629,3,1104,17373,4,1254,18067,1,1404,18067,50,1404,18067,40,1404,18107,0,1404,18263,3,1712,18271,4,1855,18279,5,2005,18279,1,2005,18279,50,2005,18279,40,2005,18319,0,2005,43168,3,3512,44423,4,4256,45601,5,5006,45602,1,5006,45602,50,5006,45602,40,5006,45642,0,5007,61173,3,5759,62089,4,6133,62987,1,6508,62987,50,6508,62987,40,6508,63027,0,6508,71721,3,7260,72927,4,7634,74007,5,8009,74008,1,8009,74008,50,8009,74008,40,8009,74048,0,8009,129135,3,11910,130436,4,13860,131553,1,15810,131553,50,15812,131553,40,15812,131593,0,15812,177735,3,18364,178787,4,19638,179656,1,20913,179656,50,20915,179656,40,20915,179696,0,20915,214348,3,22416,215322,4,23166,216206,5,23916,216207,1,23916,216207,50,23918,216207,40,23918,216247,0,23918,226572,3,24669,227471,4,25045,227561,5,25419,227561,1,25419,227561,50,25419,227561,40,25419,227601,0,25419,257011,3,26621,257867,4,27220,258372,1,27820,258372,50,27821,258372,40,27821,258412,0,27821,278065,3,28572,278831,4,28947,279134,1,29322,279134,50,29322,279134,40,29322,279134,40,29322,279169,0,29322,279245,50,29323,279245,30,29323,279245,40,29323,279280,0,29323,279391,50,29324,279426,0,29329,279582,50,29330,279582,30,29330,279582,40,29330,279617,0,29330,279698,50,29330,279698,30,29330,279698,40,29330,279733,0,29330,279828,50,29331,279863,0,29335,280000,50,29336,280000,30,29336,280000,40,29336,280035,0,29336,280134,50,29337,280169,0,29342,280315,50,29344,280350,0,29344,280506,50,29348,280541,0,29348,280709,50,29355,280744,0,29360,280918,50,29370,280953,0,29370,281135,50,29388,281170,0,29392,281361,50,29425,281396,0,29425,281597,50,29492,281632,0,29492,281844,50,29625,281844,40,29625,281879,0,29625,282054,50,29625,282054,30,29625,282054,40,29625,282089,0,29625,282194,50,29626,282229,0,29631,282378,50,29633,282413,0,29633,282570,50,29637,282605,0,29637,282770,50,29643,282805,0,29647,282976,50,29656,283011,0,29656,283190,50,29672,283225,0,29676,283412,50,29706,283447,0,29706,283644,50,29768,283679,0,29768,283886,50,29887,283886,40,29887,283921,0,29887,284095,50,29887,284095,30,29887,284095,40,29887,284130,0,29887,284235,50,29888,284270,0,29892,284419,50,29895,284454,0,29895,284611,50,29899,284646,0,29899,284811,50,29904,284846,0,29909,285017,50,29917,285052,0,29918,285231,50,29933,285266,0,29938,285453,50,29967,285488,0,29967,285685,50,30029,285720,0,30030,285927,50,30146,285927,40,30146,285962,0,30146)
%
%
% START OF PROOF
% 285929 [] equal(multiply(identity,X),X).
% 285930 [] equal(multiply(inverse(X),X),identity).
% 285931 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 285932 [] -equal(inverse(sk_c6),sk_c5).
% 285935 [?] ?
% 285941 [?] ?
% 285947 [?] ?
% 285953 [?] ?
% 285959 [?] ?
% 285968 [input:285941,cut:285932] equal(inverse(sk_c2),sk_c6).
% 285969 [para:285968.1.1,285930.1.1.1] equal(multiply(sk_c6,sk_c2),identity).
% 285975 [input:285953,cut:285932] equal(inverse(sk_c1),sk_c7).
% 285976 [para:285975.1.1,285930.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 285980 [input:285935,cut:285932] equal(multiply(sk_c2,sk_c5),sk_c6).
% 285989 [input:285947,cut:285932] equal(multiply(sk_c1,sk_c6),sk_c7).
% 285998 [input:285959,cut:285932] equal(multiply(sk_c6,sk_c7),sk_c5).
% 286016 [para:285930.1.1,285931.1.1.1,demod:285929] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 286018 [para:285969.1.1,285931.1.1.1,demod:285929] equal(X,multiply(sk_c6,multiply(sk_c2,X))).
% 286021 [para:285976.1.1,285931.1.1.1,demod:285929] equal(X,multiply(sk_c7,multiply(sk_c1,X))).
% 286052 [para:285980.1.1,286018.1.2.2] equal(sk_c5,multiply(sk_c6,sk_c6)).
% 286055 [para:285989.1.1,286021.1.2.2] equal(sk_c6,multiply(sk_c7,sk_c7)).
% 286076 [para:285998.1.1,286016.1.2.2] equal(sk_c7,multiply(inverse(sk_c6),sk_c5)).
% 286095 [para:286052.1.2,286016.1.2.2,demod:286076] equal(sk_c6,sk_c7).
% 286112 [para:286095.1.1,285998.1.1.1,demod:286055] equal(sk_c6,sk_c5).
% 286122 [para:286112.1.1,285932.1.1.1] -equal(inverse(sk_c5),sk_c5).
% 286133 [para:286112.1.1,285998.1.1.1] equal(multiply(sk_c5,sk_c7),sk_c5).
% 286140 [para:286112.1.1,286095.1.1] equal(sk_c5,sk_c7).
% 286141 [para:286095.1.1,286112.1.1] equal(sk_c7,sk_c5).
% 286171 [para:286133.1.1,286016.1.2.2,demod:285930] equal(sk_c7,identity).
% 286173 [para:286171.1.1,285976.1.1.1,demod:285929] equal(sk_c1,identity).
% 286182 [para:286171.1.1,286140.1.2] equal(sk_c5,identity).
% 286189 [para:286173.1.1,285975.1.1.1] equal(inverse(identity),sk_c7).
% 286202 [para:286182.1.1,286122.1.1.1,demod:286189,cut:286141] 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: 38199
% derived clauses: 6707493
% kept clauses: 242819
% kept size sum: 276985
% kept mid-nuclei: 3045
% kept new demods: 5543
% forw unit-subs: 2539845
% forw double-subs: 3620715
% forw overdouble-subs: 257500
% backward subs: 11061
% fast unit cutoff: 17339
% full unit cutoff: 0
% dbl unit cutoff: 4926
% real runtime : 303.78
% process. runtime: 301.47
% specific non-discr-tree subsumption statistics:
% tried: 38176152
% length fails: 5263868
% strength fails: 9199511
% predlist fails: 1427553
% aux str. fails: 6073067
% by-lit fails: 8998217
% full subs tried: 1325560
% full subs fail: 1244858
%
% ; 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/GRP345-1+eq_r.in")
%
%------------------------------------------------------------------------------