%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP349-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 : art01.cs.miami.edu
% Model : i686 unknown
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 1000MB
% OS : Linux 2.4.22-21mdk-i686-up-4GB
% CPULimit : 600s
% Result : Unsatisfiable 298.7s
% Output : Assurance 298.7s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----NO SOLUTION OUTPUT BY SYSTEM
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
%
% Gandalf c-2.6 r1 starting to prove: /home/graph/tptp/TSTP/PreparedTPTP/otter:hypothesis:set(auto),clear(print_given)---add_equality:r/GRP/GRP349-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 31)
% (binary-unit 12 #f)
% (binary-unit-uniteq 12 #f)
% (binary-posweight-kb-big-order 60 #f 3 31)
% (binary-posweight-lex-big-order 30 #f 3 31)
% (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_c9,sk_c10),sk_c8) | -equal(multiply(sk_c9,sk_c8),sk_c10) | -equal(inverse(sk_c10),sk_c8) | -equal(multiply(X,Y),sk_c9) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c8),sk_c9) | -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c9),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c10) | -equal(multiply(V,sk_c9),sk_c10) | -equal(multiply(W,X1),sk_c9) | -equal(inverse(W),X1) | -equal(multiply(X1,sk_c8),sk_c9).
% was split for some strategies as:
% -equal(multiply(W,X1),sk_c9) | -equal(inverse(W),X1) | -equal(multiply(X1,sk_c8),sk_c9).
% -equal(inverse(V),sk_c10) | -equal(multiply(V,sk_c9),sk_c10).
% -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10).
% -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c9),sk_c8).
% -equal(multiply(X,Y),sk_c9) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c8),sk_c9).
% -equal(multiply(sk_c9,sk_c10),sk_c8).
% -equal(multiply(sk_c9,sk_c8),sk_c10).
% -equal(inverse(sk_c10),sk_c8).
% -equal(multiply(sk_c10,sk_c8),sk_c9).
%
% Starting a split proof attempt with 9 components.
%
% Split component 1 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c9,sk_c10),sk_c8) | -equal(multiply(sk_c9,sk_c8),sk_c10) | -equal(inverse(sk_c10),sk_c8) | -equal(multiply(X,Y),sk_c9) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c8),sk_c9) | -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c9),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c10) | -equal(multiply(V,sk_c9),sk_c10) | -equal(multiply(W,X1),sk_c9) | -equal(inverse(W),X1) | -equal(multiply(X1,sk_c8),sk_c9).
% Split part used next: -equal(multiply(W,X1),sk_c9) | -equal(inverse(W),X1) | -equal(multiply(X1,sk_c8),sk_c9).
% END OF PROOFPART
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(69,40,0,144,0,0,2753,50,35,2828,0,35,8202,50,100,8277,0,100,13657,50,172,13732,0,172,20118,50,271,20193,0,271,27336,50,397,27411,0,397,35812,50,574,35887,0,574,45297,50,813,45297,40,813,45372,0,813,58218,3,1114,58835,4,1264,59386,5,1414,59387,1,1414,59387,50,1414,59387,40,1414,59462,0,1414,59696,3,1722,59705,4,1875,59712,5,2015,59712,1,2015,59712,50,2015,59712,40,2015,59787,0,2015,82870,3,3516,83752,4,4266,85106,5,5016,85107,1,5016,85107,50,5016,85107,40,5016,85182,0,5016,96504,3,5767,97775,4,6142,99577,50,6421,99577,40,6421,99652,0,6421,115598,3,7174,116227,4,7547,116875,1,7922,116875,50,7922,116875,40,7922,116950,0,7922,174318,3,11824,175091,4,13773,175919,1,15723,175919,50,15725,175919,40,15725,175994,0,15725,216808,3,18276,217578,4,19551,218307,1,20826,218307,50,20827,218307,40,20827,218382,0,20827,264485,3,22332,265133,4,23078,265759,5,23828,265760,1,23828,265760,50,23829,265760,40,23829,265835,0,23829,285656,3,24580,286208,4,24955,286650,5,25330,286651,1,25330,286651,50,25330,286651,40,25330,286726,0,25330,318765,3,26532,319348,4,27131,319839,5,27731,319840,1,27731,319840,50,27732,319840,40,27732,319915,0,27732,342606,3,28490,343133,4,28858,343553,5,29233,343554,1,29233,343554,50,29234,343554,40,29234,343554,40,29234,343623,0,29234)
%
%
% START OF PROOF
% 343555 [] equal(X,X).
% 343559 [] -equal(multiply(X,sk_c8),sk_c9) | -equal(multiply(Y,X),sk_c9) | -equal(inverse(Y),X).
% 343576 [] equal(multiply(sk_c2,sk_c8),sk_c9) | equal(multiply(sk_c7,sk_c8),sk_c9).
% 343577 [?] ?
% 343578 [] equal(multiply(sk_c2,sk_c8),sk_c9) | equal(multiply(sk_c6,sk_c7),sk_c9).
% 343584 [?] ?
% 343585 [] equal(inverse(sk_c1),sk_c2) | equal(inverse(sk_c6),sk_c7).
% 343586 [?] ?
% 343592 [] equal(multiply(sk_c1,sk_c2),sk_c9) | equal(multiply(sk_c7,sk_c8),sk_c9).
% 343593 [?] ?
% 343594 [] equal(multiply(sk_c1,sk_c2),sk_c9) | equal(multiply(sk_c6,sk_c7),sk_c9).
% 343635 [hyper:343559,343585,binarycut:343593,binarycut:343577] equal(inverse(sk_c6),sk_c7).
% 343637 [hyper:343559,343585,binarycut:343586,binarycut:343584] equal(inverse(sk_c1),sk_c2).
% 343702 [hyper:343559,343578,343576,demod:343635,cut:343555] equal(multiply(sk_c2,sk_c8),sk_c9).
% 343717 [hyper:343559,343592,demod:343637,343702,cut:343555,cut:343555] equal(multiply(sk_c7,sk_c8),sk_c9).
% 343727 [hyper:343559,343594,demod:343637,343702,cut:343555,cut:343555] equal(multiply(sk_c6,sk_c7),sk_c9).
% 343729 [hyper:343559,343727,demod:343635,343717,cut:343555,cut:343555] 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 31
% clause depth limited to 3
% seconds given: 2
%
%
% Split component 2 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c9,sk_c10),sk_c8) | -equal(multiply(sk_c9,sk_c8),sk_c10) | -equal(inverse(sk_c10),sk_c8) | -equal(multiply(X,Y),sk_c9) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c8),sk_c9) | -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c9),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c10) | -equal(multiply(V,sk_c9),sk_c10) | -equal(multiply(W,X1),sk_c9) | -equal(inverse(W),X1) | -equal(multiply(X1,sk_c8),sk_c9).
% Split part used next: -equal(inverse(V),sk_c10) | -equal(multiply(V,sk_c9),sk_c10).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 3
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 4
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(69,40,0,144,0,0,2753,50,35,2828,0,35,8202,50,100,8277,0,100,13657,50,172,13732,0,172,20118,50,271,20193,0,271,27336,50,397,27411,0,397,35812,50,574,35887,0,574,45297,50,813,45297,40,813,45372,0,813,58218,3,1114,58835,4,1264,59386,5,1414,59387,1,1414,59387,50,1414,59387,40,1414,59462,0,1414,59696,3,1722,59705,4,1875,59712,5,2015,59712,1,2015,59712,50,2015,59712,40,2015,59787,0,2015,82870,3,3516,83752,4,4266,85106,5,5016,85107,1,5016,85107,50,5016,85107,40,5016,85182,0,5016,96504,3,5767,97775,4,6142,99577,50,6421,99577,40,6421,99652,0,6421,115598,3,7174,116227,4,7547,116875,1,7922,116875,50,7922,116875,40,7922,116950,0,7922,174318,3,11824,175091,4,13773,175919,1,15723,175919,50,15725,175919,40,15725,175994,0,15725,216808,3,18276,217578,4,19551,218307,1,20826,218307,50,20827,218307,40,20827,218382,0,20827,264485,3,22332,265133,4,23078,265759,5,23828,265760,1,23828,265760,50,23829,265760,40,23829,265835,0,23829,285656,3,24580,286208,4,24955,286650,5,25330,286651,1,25330,286651,50,25330,286651,40,25330,286726,0,25330,318765,3,26532,319348,4,27131,319839,5,27731,319840,1,27731,319840,50,27732,319840,40,27732,319915,0,27732,342606,3,28490,343133,4,28858,343553,5,29233,343554,1,29233,343554,50,29234,343554,40,29234,343554,40,29234,343623,0,29234,343728,50,29234,343728,30,29234,343728,40,29234,343797,0,29234,343950,50,29235,344019,0,29240)
%
%
% START OF PROOF
% 343952 [] equal(multiply(identity,X),X).
% 343953 [] equal(multiply(inverse(X),X),identity).
% 343954 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 343955 [] -equal(multiply(X,sk_c9),sk_c10) | -equal(inverse(X),sk_c10).
% 343959 [] equal(multiply(sk_c3,sk_c9),sk_c8) | equal(multiply(sk_c5,sk_c9),sk_c10).
% 343960 [] equal(multiply(sk_c3,sk_c9),sk_c8) | equal(inverse(sk_c5),sk_c10).
% 343967 [?] ?
% 343968 [] equal(inverse(sk_c3),sk_c8) | equal(inverse(sk_c5),sk_c10).
% 343975 [] equal(multiply(sk_c2,sk_c8),sk_c9) | equal(multiply(sk_c5,sk_c9),sk_c10).
% 343976 [] equal(multiply(sk_c2,sk_c8),sk_c9) | equal(inverse(sk_c5),sk_c10).
% 343983 [?] ?
% 343984 [] equal(inverse(sk_c1),sk_c2) | equal(inverse(sk_c5),sk_c10).
% 343991 [] equal(multiply(sk_c1,sk_c2),sk_c9) | equal(multiply(sk_c5,sk_c9),sk_c10).
% 343992 [] equal(multiply(sk_c1,sk_c2),sk_c9) | equal(inverse(sk_c5),sk_c10).
% 343999 [?] ?
% 344000 [] equal(inverse(sk_c10),sk_c8) | equal(inverse(sk_c5),sk_c10).
% 344007 [] equal(multiply(sk_c9,sk_c8),sk_c10) | equal(multiply(sk_c5,sk_c9),sk_c10).
% 344008 [] equal(multiply(sk_c9,sk_c8),sk_c10) | equal(inverse(sk_c5),sk_c10).
% 344015 [] equal(multiply(sk_c9,sk_c10),sk_c8) | equal(multiply(sk_c5,sk_c9),sk_c10).
% 344016 [] equal(multiply(sk_c9,sk_c10),sk_c8) | equal(inverse(sk_c5),sk_c10).
% 344023 [hyper:343955,343968,binarycut:343967] equal(inverse(sk_c3),sk_c8).
% 344025 [para:344023.1.1,343953.1.1.1] equal(multiply(sk_c8,sk_c3),identity).
% 344029 [hyper:343955,343984,binarycut:343983] equal(inverse(sk_c1),sk_c2).
% 344030 [para:344029.1.1,343953.1.1.1] equal(multiply(sk_c2,sk_c1),identity).
% 344035 [hyper:343955,344000,binarycut:343999] equal(inverse(sk_c10),sk_c8).
% 344036 [para:344035.1.1,343953.1.1.1] equal(multiply(sk_c8,sk_c10),identity).
% 344065 [hyper:343955,343959,343960] equal(multiply(sk_c3,sk_c9),sk_c8).
% 344080 [hyper:343955,343975,343976] equal(multiply(sk_c2,sk_c8),sk_c9).
% 344085 [hyper:343955,343991,343992] equal(multiply(sk_c1,sk_c2),sk_c9).
% 344090 [hyper:343955,344007,344008] equal(multiply(sk_c9,sk_c8),sk_c10).
% 344095 [hyper:343955,344015,344016] equal(multiply(sk_c9,sk_c10),sk_c8).
% 344096 [para:343953.1.1,343954.1.1.1,demod:343952] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 344097 [para:344025.1.1,343954.1.1.1,demod:343952] equal(X,multiply(sk_c8,multiply(sk_c3,X))).
% 344098 [para:344030.1.1,343954.1.1.1,demod:343952] equal(X,multiply(sk_c2,multiply(sk_c1,X))).
% 344099 [para:344036.1.1,343954.1.1.1,demod:343952] equal(X,multiply(sk_c8,multiply(sk_c10,X))).
% 344100 [para:344065.1.1,343954.1.1.1] equal(multiply(sk_c8,X),multiply(sk_c3,multiply(sk_c9,X))).
% 344101 [para:344080.1.1,343954.1.1.1] equal(multiply(sk_c9,X),multiply(sk_c2,multiply(sk_c8,X))).
% 344105 [para:344065.1.1,344097.1.2.2] equal(sk_c9,multiply(sk_c8,sk_c8)).
% 344106 [para:344105.1.2,343954.1.1.1] equal(multiply(sk_c9,X),multiply(sk_c8,multiply(sk_c8,X))).
% 344107 [para:344085.1.1,344098.1.2.2] equal(sk_c2,multiply(sk_c2,sk_c9)).
% 344109 [para:343953.1.1,344096.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 344110 [para:344025.1.1,344096.1.2.2] equal(sk_c3,multiply(inverse(sk_c8),identity)).
% 344112 [para:344036.1.1,344096.1.2.2,demod:344110] equal(sk_c10,sk_c3).
% 344116 [para:343954.1.1,344096.1.2.2] equal(X,multiply(inverse(multiply(Y,Z)),multiply(Y,multiply(Z,X)))).
% 344119 [para:344096.1.2,344096.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 344120 [para:344112.1.1,344095.1.1.2] equal(multiply(sk_c9,sk_c3),sk_c8).
% 344122 [para:344120.1.1,343954.1.1.1] equal(multiply(sk_c8,X),multiply(sk_c9,multiply(sk_c3,X))).
% 344129 [para:344090.1.1,344100.1.2.2,demod:344105] equal(sk_c9,multiply(sk_c3,sk_c10)).
% 344138 [para:344097.1.2,344101.1.2.2,demod:344122] equal(multiply(sk_c8,X),multiply(sk_c2,X)).
% 344139 [para:344105.1.2,344101.1.2.2,demod:344107,344090] equal(sk_c10,sk_c2).
% 344145 [para:344139.1.1,344112.1.1] equal(sk_c2,sk_c3).
% 344147 [para:344139.1.1,344099.1.2.2.1,demod:344106,344138] equal(X,multiply(sk_c9,X)).
% 344151 [para:344145.1.2,344129.1.2.1,demod:344036,344138] equal(sk_c9,identity).
% 344159 [para:344151.1.1,344090.1.1.1,demod:343952] equal(sk_c8,sk_c10).
% 344195 [para:344119.1.2,343953.1.1] equal(multiply(X,inverse(X)),identity).
% 344197 [para:344119.1.2,344109.1.2] equal(X,multiply(X,identity)).
% 344199 [para:344197.1.2,344109.1.2] equal(X,inverse(inverse(X))).
% 344201 [para:344195.1.1,344116.1.2.2.2,demod:344197] equal(inverse(X),multiply(inverse(multiply(Y,X)),Y)).
% 344208 [para:344147.1.2,344201.1.2.1.1] equal(inverse(X),multiply(inverse(X),sk_c9)).
% 344212 [para:344208.1.2,344119.1.2,demod:344199] equal(multiply(X,sk_c9),X).
% 344213 [hyper:343955,344212,demod:344035,cut:344159] 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 31
% clause depth limited to 4
% seconds given: 2
%
%
% Split component 3 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c9,sk_c10),sk_c8) | -equal(multiply(sk_c9,sk_c8),sk_c10) | -equal(inverse(sk_c10),sk_c8) | -equal(multiply(X,Y),sk_c9) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c8),sk_c9) | -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c9),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c10) | -equal(multiply(V,sk_c9),sk_c10) | -equal(multiply(W,X1),sk_c9) | -equal(inverse(W),X1) | -equal(multiply(X1,sk_c8),sk_c9).
% Split part used next: -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 3
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 4
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 5
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 6
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 7
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 8
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 9
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(69,40,0,144,0,0,2753,50,35,2828,0,35,8202,50,100,8277,0,100,13657,50,172,13732,0,172,20118,50,271,20193,0,271,27336,50,397,27411,0,397,35812,50,574,35887,0,574,45297,50,813,45297,40,813,45372,0,813,58218,3,1114,58835,4,1264,59386,5,1414,59387,1,1414,59387,50,1414,59387,40,1414,59462,0,1414,59696,3,1722,59705,4,1875,59712,5,2015,59712,1,2015,59712,50,2015,59712,40,2015,59787,0,2015,82870,3,3516,83752,4,4266,85106,5,5016,85107,1,5016,85107,50,5016,85107,40,5016,85182,0,5016,96504,3,5767,97775,4,6142,99577,50,6421,99577,40,6421,99652,0,6421,115598,3,7174,116227,4,7547,116875,1,7922,116875,50,7922,116875,40,7922,116950,0,7922,174318,3,11824,175091,4,13773,175919,1,15723,175919,50,15725,175919,40,15725,175994,0,15725,216808,3,18276,217578,4,19551,218307,1,20826,218307,50,20827,218307,40,20827,218382,0,20827,264485,3,22332,265133,4,23078,265759,5,23828,265760,1,23828,265760,50,23829,265760,40,23829,265835,0,23829,285656,3,24580,286208,4,24955,286650,5,25330,286651,1,25330,286651,50,25330,286651,40,25330,286726,0,25330,318765,3,26532,319348,4,27131,319839,5,27731,319840,1,27731,319840,50,27732,319840,40,27732,319915,0,27732,342606,3,28490,343133,4,28858,343553,5,29233,343554,1,29233,343554,50,29234,343554,40,29234,343554,40,29234,343623,0,29234,343728,50,29234,343728,30,29234,343728,40,29234,343797,0,29234,343950,50,29235,344019,0,29240,344212,50,29242,344212,30,29242,344212,40,29242,344281,0,29242,344452,50,29243,344521,0,29248,344746,50,29252,344815,0,29252,345050,50,29259,345119,0,29263,345364,50,29273,345433,0,29273,345689,50,29288,345758,0,29293,346030,50,29321,346099,0,29321,346387,50,29375,346387,40,29375,346456,0,29375)
%
%
% START OF PROOF
% 346250 [?] ?
% 346388 [] equal(X,X).
% 346389 [] equal(multiply(identity,X),X).
% 346390 [] equal(multiply(inverse(X),X),identity).
% 346391 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 346392 [] -equal(multiply(X,sk_c10),sk_c9) | -equal(inverse(X),sk_c10).
% 346465 [para:346390.1.1,346392.1.1,cut:346250] -equal(inverse(inverse(sk_c10)),sk_c10).
% 346624 [para:346390.1.1,346391.1.1.1,demod:346389] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 346737 [para:346390.1.1,346624.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 346895 [para:346624.1.2,346624.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 347016 [para:346895.1.2,346737.1.2] equal(X,multiply(X,identity)).
% 347030 [para:347016.1.2,346737.1.2] equal(X,inverse(inverse(X))).
% 347037 [para:347030.1.2,346465.1.1,cut:346388] 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 4 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c9,sk_c10),sk_c8) | -equal(multiply(sk_c9,sk_c8),sk_c10) | -equal(inverse(sk_c10),sk_c8) | -equal(multiply(X,Y),sk_c9) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c8),sk_c9) | -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c9),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c10) | -equal(multiply(V,sk_c9),sk_c10) | -equal(multiply(W,X1),sk_c9) | -equal(inverse(W),X1) | -equal(multiply(X1,sk_c8),sk_c9).
% Split part used next: -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c9),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 31
% clause depth limited to 3
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 4
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(69,40,0,144,0,0,2753,50,35,2828,0,35,8202,50,100,8277,0,100,13657,50,172,13732,0,172,20118,50,271,20193,0,271,27336,50,397,27411,0,397,35812,50,574,35887,0,574,45297,50,813,45297,40,813,45372,0,813,58218,3,1114,58835,4,1264,59386,5,1414,59387,1,1414,59387,50,1414,59387,40,1414,59462,0,1414,59696,3,1722,59705,4,1875,59712,5,2015,59712,1,2015,59712,50,2015,59712,40,2015,59787,0,2015,82870,3,3516,83752,4,4266,85106,5,5016,85107,1,5016,85107,50,5016,85107,40,5016,85182,0,5016,96504,3,5767,97775,4,6142,99577,50,6421,99577,40,6421,99652,0,6421,115598,3,7174,116227,4,7547,116875,1,7922,116875,50,7922,116875,40,7922,116950,0,7922,174318,3,11824,175091,4,13773,175919,1,15723,175919,50,15725,175919,40,15725,175994,0,15725,216808,3,18276,217578,4,19551,218307,1,20826,218307,50,20827,218307,40,20827,218382,0,20827,264485,3,22332,265133,4,23078,265759,5,23828,265760,1,23828,265760,50,23829,265760,40,23829,265835,0,23829,285656,3,24580,286208,4,24955,286650,5,25330,286651,1,25330,286651,50,25330,286651,40,25330,286726,0,25330,318765,3,26532,319348,4,27131,319839,5,27731,319840,1,27731,319840,50,27732,319840,40,27732,319915,0,27732,342606,3,28490,343133,4,28858,343553,5,29233,343554,1,29233,343554,50,29234,343554,40,29234,343554,40,29234,343623,0,29234,343728,50,29234,343728,30,29234,343728,40,29234,343797,0,29234,343950,50,29235,344019,0,29240,344212,50,29242,344212,30,29242,344212,40,29242,344281,0,29242,344452,50,29243,344521,0,29248,344746,50,29252,344815,0,29252,345050,50,29259,345119,0,29263,345364,50,29273,345433,0,29273,345689,50,29288,345758,0,29293,346030,50,29321,346099,0,29321,346387,50,29375,346387,40,29375,346456,0,29375,347036,50,29376,347036,30,29376,347036,40,29376,347105,0,29376,347243,50,29377,347312,0,29383)
%
%
% START OF PROOF
% 347245 [] equal(multiply(identity,X),X).
% 347246 [] equal(multiply(inverse(X),X),identity).
% 347247 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 347248 [] -equal(multiply(X,sk_c9),sk_c8) | -equal(inverse(X),sk_c8).
% 347249 [] equal(multiply(sk_c3,sk_c9),sk_c8) | equal(multiply(sk_c7,sk_c8),sk_c9).
% 347250 [?] ?
% 347251 [] equal(multiply(sk_c3,sk_c9),sk_c8) | equal(multiply(sk_c6,sk_c7),sk_c9).
% 347252 [?] ?
% 347253 [?] ?
% 347254 [] equal(multiply(sk_c3,sk_c9),sk_c8) | equal(multiply(sk_c10,sk_c8),sk_c9).
% 347255 [?] ?
% 347256 [?] ?
% 347257 [] equal(multiply(sk_c7,sk_c8),sk_c9) | equal(inverse(sk_c3),sk_c8).
% 347258 [] equal(inverse(sk_c3),sk_c8) | equal(inverse(sk_c6),sk_c7).
% 347259 [] equal(multiply(sk_c6,sk_c7),sk_c9) | equal(inverse(sk_c3),sk_c8).
% 347260 [] equal(multiply(sk_c5,sk_c9),sk_c10) | equal(inverse(sk_c3),sk_c8).
% 347261 [] equal(inverse(sk_c3),sk_c8) | equal(inverse(sk_c5),sk_c10).
% 347262 [] equal(multiply(sk_c10,sk_c8),sk_c9) | equal(inverse(sk_c3),sk_c8).
% 347263 [] equal(inverse(sk_c3),sk_c8) | equal(inverse(sk_c4),sk_c10).
% 347264 [] equal(multiply(sk_c4,sk_c10),sk_c9) | equal(inverse(sk_c3),sk_c8).
% 347315 [hyper:347248,347258,binarycut:347250] equal(inverse(sk_c6),sk_c7).
% 347316 [para:347315.1.1,347246.1.1.1] equal(multiply(sk_c7,sk_c6),identity).
% 347320 [hyper:347248,347261,binarycut:347253] equal(inverse(sk_c5),sk_c10).
% 347321 [para:347320.1.1,347246.1.1.1] equal(multiply(sk_c10,sk_c5),identity).
% 347324 [hyper:347248,347263,binarycut:347255] equal(inverse(sk_c4),sk_c10).
% 347328 [para:347324.1.1,347246.1.1.1] equal(multiply(sk_c10,sk_c4),identity).
% 347331 [hyper:347248,347257,binarycut:347249] equal(multiply(sk_c7,sk_c8),sk_c9).
% 347337 [hyper:347248,347259,binarycut:347251] equal(multiply(sk_c6,sk_c7),sk_c9).
% 347340 [hyper:347248,347260,binarycut:347252] equal(multiply(sk_c5,sk_c9),sk_c10).
% 347346 [hyper:347248,347262,binarycut:347254] equal(multiply(sk_c10,sk_c8),sk_c9).
% 347349 [hyper:347248,347264,binarycut:347256] equal(multiply(sk_c4,sk_c10),sk_c9).
% 347350 [para:347246.1.1,347247.1.1.1,demod:347245] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 347351 [para:347316.1.1,347247.1.1.1,demod:347245] equal(X,multiply(sk_c7,multiply(sk_c6,X))).
% 347352 [para:347321.1.1,347247.1.1.1,demod:347245] equal(X,multiply(sk_c10,multiply(sk_c5,X))).
% 347353 [para:347328.1.1,347247.1.1.1,demod:347245] equal(X,multiply(sk_c10,multiply(sk_c4,X))).
% 347354 [para:347331.1.1,347247.1.1.1] equal(multiply(sk_c9,X),multiply(sk_c7,multiply(sk_c8,X))).
% 347355 [para:347337.1.1,347247.1.1.1] equal(multiply(sk_c9,X),multiply(sk_c6,multiply(sk_c7,X))).
% 347356 [para:347340.1.1,347247.1.1.1] equal(multiply(sk_c10,X),multiply(sk_c5,multiply(sk_c9,X))).
% 347357 [para:347346.1.1,347247.1.1.1] equal(multiply(sk_c9,X),multiply(sk_c10,multiply(sk_c8,X))).
% 347358 [para:347349.1.1,347247.1.1.1] equal(multiply(sk_c9,X),multiply(sk_c4,multiply(sk_c10,X))).
% 347359 [para:347337.1.1,347351.1.2.2] equal(sk_c7,multiply(sk_c7,sk_c9)).
% 347360 [para:347359.1.2,347247.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c7,multiply(sk_c9,X))).
% 347361 [para:347340.1.1,347352.1.2.2] equal(sk_c9,multiply(sk_c10,sk_c10)).
% 347363 [para:347246.1.1,347350.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 347364 [para:347316.1.1,347350.1.2.2] equal(sk_c6,multiply(inverse(sk_c7),identity)).
% 347367 [para:347331.1.1,347350.1.2.2] equal(sk_c8,multiply(inverse(sk_c7),sk_c9)).
% 347368 [para:347346.1.1,347350.1.2.2] equal(sk_c8,multiply(inverse(sk_c10),sk_c9)).
% 347369 [para:347349.1.1,347350.1.2.2,demod:347324] equal(sk_c10,multiply(sk_c10,sk_c9)).
% 347370 [para:347247.1.1,347350.1.2.2] equal(X,multiply(inverse(multiply(Y,Z)),multiply(Y,multiply(Z,X)))).
% 347371 [para:347351.1.2,347350.1.2.2] equal(multiply(sk_c6,X),multiply(inverse(sk_c7),X)).
% 347372 [para:347352.1.2,347350.1.2.2] equal(multiply(sk_c5,X),multiply(inverse(sk_c10),X)).
% 347373 [para:347350.1.2,347350.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 347376 [para:347361.1.2,347350.1.2.2,demod:347368] equal(sk_c10,sk_c8).
% 347379 [para:347376.1.1,347346.1.1.1] equal(multiply(sk_c8,sk_c8),sk_c9).
% 347381 [para:347376.1.1,347352.1.2.1] equal(X,multiply(sk_c8,multiply(sk_c5,X))).
% 347385 [para:347376.1.1,347369.1.2.1] equal(sk_c10,multiply(sk_c8,sk_c9)).
% 347387 [para:347353.1.2,347350.1.2.2,demod:347372] equal(multiply(sk_c4,X),multiply(sk_c5,X)).
% 347390 [para:347379.1.1,347247.1.1.1] equal(multiply(sk_c9,X),multiply(sk_c8,multiply(sk_c8,X))).
% 347391 [para:347379.1.1,347350.1.2.2] equal(sk_c8,multiply(inverse(sk_c8),sk_c9)).
% 347394 [para:347354.1.2,347350.1.2.2,demod:347371] equal(multiply(sk_c8,X),multiply(sk_c6,multiply(sk_c9,X))).
% 347397 [para:347379.1.1,347354.1.2.2,demod:347359] equal(multiply(sk_c9,sk_c8),sk_c7).
% 347403 [para:347397.1.1,347247.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c9,multiply(sk_c8,X))).
% 347407 [para:347331.1.1,347355.1.2.2,demod:347397] equal(sk_c7,multiply(sk_c6,sk_c9)).
% 347410 [para:347354.1.2,347355.1.2.2,demod:347394,347403] equal(multiply(sk_c7,X),multiply(sk_c8,X)).
% 347411 [para:347407.1.2,347351.1.2.2,demod:347410] equal(sk_c9,multiply(sk_c8,sk_c7)).
% 347412 [para:347411.1.2,347350.1.2.2,demod:347391] equal(sk_c7,sk_c8).
% 347417 [para:347412.1.1,347359.1.2.1,demod:347385] equal(sk_c7,sk_c10).
% 347419 [para:347417.1.2,347349.1.1.2] equal(multiply(sk_c4,sk_c7),sk_c9).
% 347425 [para:347357.1.2,347350.1.2.2,demod:347356,347372] equal(multiply(sk_c8,X),multiply(sk_c10,X)).
% 347427 [para:347352.1.2,347358.1.2.2,demod:347387] equal(multiply(sk_c9,multiply(sk_c4,X)),multiply(sk_c4,X)).
% 347433 [para:347381.1.2,347354.1.2.2,demod:347410,347427,347387] equal(multiply(sk_c4,X),multiply(sk_c8,X)).
% 347434 [para:347387.1.2,347381.1.2.2,demod:347390,347433] equal(X,multiply(sk_c9,X)).
% 347435 [para:347434.1.2,347350.1.2.2] equal(X,multiply(inverse(sk_c9),X)).
% 347436 [para:347435.1.2,347246.1.1] equal(sk_c9,identity).
% 347438 [para:347436.1.1,347367.1.2.2,demod:347364] equal(sk_c8,sk_c6).
% 347440 [para:347438.1.2,347315.1.1.1] equal(inverse(sk_c8),sk_c7).
% 347450 [para:347351.1.2,347370.1.2.2.2] equal(multiply(sk_c6,X),multiply(inverse(multiply(Y,sk_c7)),multiply(Y,X))).
% 347455 [para:347354.1.2,347370.1.2.2.2,demod:347450,347434] equal(multiply(sk_c8,X),multiply(sk_c6,X)).
% 347476 [para:347373.1.2,347246.1.1] equal(multiply(X,inverse(X)),identity).
% 347478 [para:347373.1.2,347363.1.2] equal(X,multiply(X,identity)).
% 347482 [para:347478.1.2,347363.1.2] equal(X,inverse(inverse(X))).
% 347484 [para:347476.1.1,347370.1.2.2.2,demod:347478] equal(inverse(X),multiply(inverse(multiply(Y,X)),Y)).
% 347493 [para:347351.1.2,347484.1.2.1.1,demod:347455] equal(inverse(multiply(sk_c8,X)),multiply(inverse(X),sk_c7)).
% 347496 [para:347355.1.2,347484.1.2.1.1,demod:347434,347493,347410] equal(multiply(inverse(X),sk_c7),multiply(inverse(X),sk_c6)).
% 347497 [para:347358.1.2,347484.1.2.1.1,demod:347434,347496,347493,347425] equal(multiply(inverse(X),sk_c6),multiply(inverse(X),sk_c4)).
% 347498 [para:347360.1.2,347484.1.2.1.1,demod:347419,347247,347497,347496,347493,347410,347434] equal(inverse(X),multiply(inverse(X),sk_c9)).
% 347502 [para:347498.1.2,347373.1.2,demod:347482] equal(multiply(X,sk_c9),X).
% 347503 [hyper:347248,347502,demod:347440,cut:347412] 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 31
% clause depth limited to 4
% seconds given: 2
%
%
% Split component 5 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c9,sk_c10),sk_c8) | -equal(multiply(sk_c9,sk_c8),sk_c10) | -equal(inverse(sk_c10),sk_c8) | -equal(multiply(X,Y),sk_c9) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c8),sk_c9) | -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c9),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c10) | -equal(multiply(V,sk_c9),sk_c10) | -equal(multiply(W,X1),sk_c9) | -equal(inverse(W),X1) | -equal(multiply(X1,sk_c8),sk_c9).
% Split part used next: -equal(multiply(X,Y),sk_c9) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c8),sk_c9).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 3
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(69,40,0,144,0,0,2753,50,35,2828,0,35,8202,50,100,8277,0,100,13657,50,172,13732,0,172,20118,50,271,20193,0,271,27336,50,397,27411,0,397,35812,50,574,35887,0,574,45297,50,813,45297,40,813,45372,0,813,58218,3,1114,58835,4,1264,59386,5,1414,59387,1,1414,59387,50,1414,59387,40,1414,59462,0,1414,59696,3,1722,59705,4,1875,59712,5,2015,59712,1,2015,59712,50,2015,59712,40,2015,59787,0,2015,82870,3,3516,83752,4,4266,85106,5,5016,85107,1,5016,85107,50,5016,85107,40,5016,85182,0,5016,96504,3,5767,97775,4,6142,99577,50,6421,99577,40,6421,99652,0,6421,115598,3,7174,116227,4,7547,116875,1,7922,116875,50,7922,116875,40,7922,116950,0,7922,174318,3,11824,175091,4,13773,175919,1,15723,175919,50,15725,175919,40,15725,175994,0,15725,216808,3,18276,217578,4,19551,218307,1,20826,218307,50,20827,218307,40,20827,218382,0,20827,264485,3,22332,265133,4,23078,265759,5,23828,265760,1,23828,265760,50,23829,265760,40,23829,265835,0,23829,285656,3,24580,286208,4,24955,286650,5,25330,286651,1,25330,286651,50,25330,286651,40,25330,286726,0,25330,318765,3,26532,319348,4,27131,319839,5,27731,319840,1,27731,319840,50,27732,319840,40,27732,319915,0,27732,342606,3,28490,343133,4,28858,343553,5,29233,343554,1,29233,343554,50,29234,343554,40,29234,343554,40,29234,343623,0,29234,343728,50,29234,343728,30,29234,343728,40,29234,343797,0,29234,343950,50,29235,344019,0,29240,344212,50,29242,344212,30,29242,344212,40,29242,344281,0,29242,344452,50,29243,344521,0,29248,344746,50,29252,344815,0,29252,345050,50,29259,345119,0,29263,345364,50,29273,345433,0,29273,345689,50,29288,345758,0,29293,346030,50,29321,346099,0,29321,346387,50,29375,346387,40,29375,346456,0,29375,347036,50,29376,347036,30,29376,347036,40,29376,347105,0,29376,347243,50,29377,347312,0,29383,347502,50,29385,347502,30,29385,347502,40,29385,347571,0,29385)
%
%
% START OF PROOF
% 347503 [] equal(X,X).
% 347507 [] -equal(multiply(X,sk_c8),sk_c9) | -equal(multiply(Y,X),sk_c9) | -equal(inverse(Y),X).
% 347524 [] equal(multiply(sk_c2,sk_c8),sk_c9) | equal(multiply(sk_c7,sk_c8),sk_c9).
% 347525 [?] ?
% 347526 [] equal(multiply(sk_c2,sk_c8),sk_c9) | equal(multiply(sk_c6,sk_c7),sk_c9).
% 347532 [?] ?
% 347533 [] equal(inverse(sk_c1),sk_c2) | equal(inverse(sk_c6),sk_c7).
% 347534 [?] ?
% 347540 [] equal(multiply(sk_c1,sk_c2),sk_c9) | equal(multiply(sk_c7,sk_c8),sk_c9).
% 347541 [?] ?
% 347542 [] equal(multiply(sk_c1,sk_c2),sk_c9) | equal(multiply(sk_c6,sk_c7),sk_c9).
% 347583 [hyper:347507,347533,binarycut:347541,binarycut:347525] equal(inverse(sk_c6),sk_c7).
% 347585 [hyper:347507,347533,binarycut:347534,binarycut:347532] equal(inverse(sk_c1),sk_c2).
% 347650 [hyper:347507,347526,347524,demod:347583,cut:347503] equal(multiply(sk_c2,sk_c8),sk_c9).
% 347665 [hyper:347507,347540,demod:347585,347650,cut:347503,cut:347503] equal(multiply(sk_c7,sk_c8),sk_c9).
% 347675 [hyper:347507,347542,demod:347585,347650,cut:347503,cut:347503] equal(multiply(sk_c6,sk_c7),sk_c9).
% 347677 [hyper:347507,347675,demod:347583,347665,cut:347503,cut:347503] 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 31
% clause depth limited to 3
% seconds given: 2
%
%
% Split component 6 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c9,sk_c10),sk_c8) | -equal(multiply(sk_c9,sk_c8),sk_c10) | -equal(inverse(sk_c10),sk_c8) | -equal(multiply(X,Y),sk_c9) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c8),sk_c9) | -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c9),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c10) | -equal(multiply(V,sk_c9),sk_c10) | -equal(multiply(W,X1),sk_c9) | -equal(inverse(W),X1) | -equal(multiply(X1,sk_c8),sk_c9).
% Split part used next: -equal(multiply(sk_c9,sk_c10),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 31
% clause depth limited to 3
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 4
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 5
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 6
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 7
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 8
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 9
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(69,40,0,144,0,0,2753,50,35,2828,0,35,8202,50,100,8277,0,100,13657,50,172,13732,0,172,20118,50,271,20193,0,271,27336,50,397,27411,0,397,35812,50,574,35887,0,574,45297,50,813,45297,40,813,45372,0,813,58218,3,1114,58835,4,1264,59386,5,1414,59387,1,1414,59387,50,1414,59387,40,1414,59462,0,1414,59696,3,1722,59705,4,1875,59712,5,2015,59712,1,2015,59712,50,2015,59712,40,2015,59787,0,2015,82870,3,3516,83752,4,4266,85106,5,5016,85107,1,5016,85107,50,5016,85107,40,5016,85182,0,5016,96504,3,5767,97775,4,6142,99577,50,6421,99577,40,6421,99652,0,6421,115598,3,7174,116227,4,7547,116875,1,7922,116875,50,7922,116875,40,7922,116950,0,7922,174318,3,11824,175091,4,13773,175919,1,15723,175919,50,15725,175919,40,15725,175994,0,15725,216808,3,18276,217578,4,19551,218307,1,20826,218307,50,20827,218307,40,20827,218382,0,20827,264485,3,22332,265133,4,23078,265759,5,23828,265760,1,23828,265760,50,23829,265760,40,23829,265835,0,23829,285656,3,24580,286208,4,24955,286650,5,25330,286651,1,25330,286651,50,25330,286651,40,25330,286726,0,25330,318765,3,26532,319348,4,27131,319839,5,27731,319840,1,27731,319840,50,27732,319840,40,27732,319915,0,27732,342606,3,28490,343133,4,28858,343553,5,29233,343554,1,29233,343554,50,29234,343554,40,29234,343554,40,29234,343623,0,29234,343728,50,29234,343728,30,29234,343728,40,29234,343797,0,29234,343950,50,29235,344019,0,29240,344212,50,29242,344212,30,29242,344212,40,29242,344281,0,29242,344452,50,29243,344521,0,29248,344746,50,29252,344815,0,29252,345050,50,29259,345119,0,29263,345364,50,29273,345433,0,29273,345689,50,29288,345758,0,29293,346030,50,29321,346099,0,29321,346387,50,29375,346387,40,29375,346456,0,29375,347036,50,29376,347036,30,29376,347036,40,29376,347105,0,29376,347243,50,29377,347312,0,29383,347502,50,29385,347502,30,29385,347502,40,29385,347571,0,29385,347676,50,29385,347676,30,29385,347676,40,29385,347745,0,29389,347933,50,29390,348002,0,29390,348249,50,29396,348318,0,29401,348575,50,29410,348644,0,29410,348911,50,29424,348980,0,29429,349258,50,29449,349327,0,29449,349619,50,29481,349688,0,29486,349996,50,29543,349996,40,29543,350065,0,29543)
%
%
% START OF PROOF
% 349828 [?] ?
% 349998 [] equal(multiply(identity,X),X).
% 349999 [] equal(multiply(inverse(X),X),identity).
% 350000 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 350001 [] -equal(multiply(sk_c9,sk_c10),sk_c8).
% 350058 [?] ?
% 350059 [?] ?
% 350060 [?] ?
% 350061 [?] ?
% 350062 [?] ?
% 350063 [?] ?
% 350064 [?] ?
% 350065 [?] ?
% 350155 [input:350059,cut:350001] equal(inverse(sk_c6),sk_c7).
% 350156 [para:350155.1.1,349999.1.1.1] equal(multiply(sk_c7,sk_c6),identity).
% 350157 [input:350062,cut:350001] equal(inverse(sk_c5),sk_c10).
% 350158 [para:350157.1.1,349999.1.1.1] equal(multiply(sk_c10,sk_c5),identity).
% 350159 [input:350064,cut:350001] equal(inverse(sk_c4),sk_c10).
% 350160 [para:350159.1.1,349999.1.1.1] equal(multiply(sk_c10,sk_c4),identity).
% 350182 [input:350058,cut:350001] equal(multiply(sk_c7,sk_c8),sk_c9).
% 350183 [input:350060,cut:350001] equal(multiply(sk_c6,sk_c7),sk_c9).
% 350184 [input:350061,cut:350001] equal(multiply(sk_c5,sk_c9),sk_c10).
% 350185 [input:350063,cut:350001] equal(multiply(sk_c10,sk_c8),sk_c9).
% 350186 [input:350065,cut:350001] equal(multiply(sk_c4,sk_c10),sk_c9).
% 350187 [para:349999.1.1,350000.1.1.1,demod:349998] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 350231 [para:350156.1.1,350000.1.1.1,demod:349998] equal(X,multiply(sk_c7,multiply(sk_c6,X))).
% 350232 [para:350158.1.1,350000.1.1.1,demod:349998] equal(X,multiply(sk_c10,multiply(sk_c5,X))).
% 350235 [para:350160.1.1,350000.1.1.1,demod:349998] equal(X,multiply(sk_c10,multiply(sk_c4,X))).
% 350267 [para:350182.1.1,350000.1.1.1] equal(multiply(sk_c9,X),multiply(sk_c7,multiply(sk_c8,X))).
% 350279 [para:350183.1.1,350231.1.2.2] equal(sk_c7,multiply(sk_c7,sk_c9)).
% 350288 [para:350184.1.1,350232.1.2.2] equal(sk_c9,multiply(sk_c10,sk_c10)).
% 350297 [para:350186.1.1,350235.1.2.2] equal(sk_c10,multiply(sk_c10,sk_c9)).
% 350404 [para:350185.1.1,350187.1.2.2] equal(sk_c8,multiply(inverse(sk_c10),sk_c9)).
% 350410 [para:350288.1.2,350187.1.2.2,demod:350404] equal(sk_c10,sk_c8).
% 350447 [para:350410.1.1,350185.1.1.1] equal(multiply(sk_c8,sk_c8),sk_c9).
% 350448 [para:350410.1.1,350186.1.1.2] equal(multiply(sk_c4,sk_c8),sk_c9).
% 350461 [para:350447.1.1,350267.1.2.2,demod:350279] equal(multiply(sk_c9,sk_c8),sk_c7).
% 350464 [para:350448.1.1,350235.1.2.2,demod:350297] equal(sk_c8,sk_c10).
% 350465 [para:350464.1.2,350001.1.1.2,demod:350461,cut:349828] 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_c9,sk_c10),sk_c8) | -equal(multiply(sk_c9,sk_c8),sk_c10) | -equal(inverse(sk_c10),sk_c8) | -equal(multiply(X,Y),sk_c9) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c8),sk_c9) | -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c9),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c10) | -equal(multiply(V,sk_c9),sk_c10) | -equal(multiply(W,X1),sk_c9) | -equal(inverse(W),X1) | -equal(multiply(X1,sk_c8),sk_c9).
% Split part used next: -equal(multiply(sk_c9,sk_c8),sk_c10).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 3
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 4
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 5
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 6
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 7
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 8
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 9
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(69,40,0,144,0,0,2753,50,35,2828,0,35,8202,50,100,8277,0,100,13657,50,172,13732,0,172,20118,50,271,20193,0,271,27336,50,397,27411,0,397,35812,50,574,35887,0,574,45297,50,813,45297,40,813,45372,0,813,58218,3,1114,58835,4,1264,59386,5,1414,59387,1,1414,59387,50,1414,59387,40,1414,59462,0,1414,59696,3,1722,59705,4,1875,59712,5,2015,59712,1,2015,59712,50,2015,59712,40,2015,59787,0,2015,82870,3,3516,83752,4,4266,85106,5,5016,85107,1,5016,85107,50,5016,85107,40,5016,85182,0,5016,96504,3,5767,97775,4,6142,99577,50,6421,99577,40,6421,99652,0,6421,115598,3,7174,116227,4,7547,116875,1,7922,116875,50,7922,116875,40,7922,116950,0,7922,174318,3,11824,175091,4,13773,175919,1,15723,175919,50,15725,175919,40,15725,175994,0,15725,216808,3,18276,217578,4,19551,218307,1,20826,218307,50,20827,218307,40,20827,218382,0,20827,264485,3,22332,265133,4,23078,265759,5,23828,265760,1,23828,265760,50,23829,265760,40,23829,265835,0,23829,285656,3,24580,286208,4,24955,286650,5,25330,286651,1,25330,286651,50,25330,286651,40,25330,286726,0,25330,318765,3,26532,319348,4,27131,319839,5,27731,319840,1,27731,319840,50,27732,319840,40,27732,319915,0,27732,342606,3,28490,343133,4,28858,343553,5,29233,343554,1,29233,343554,50,29234,343554,40,29234,343554,40,29234,343623,0,29234,343728,50,29234,343728,30,29234,343728,40,29234,343797,0,29234,343950,50,29235,344019,0,29240,344212,50,29242,344212,30,29242,344212,40,29242,344281,0,29242,344452,50,29243,344521,0,29248,344746,50,29252,344815,0,29252,345050,50,29259,345119,0,29263,345364,50,29273,345433,0,29273,345689,50,29288,345758,0,29293,346030,50,29321,346099,0,29321,346387,50,29375,346387,40,29375,346456,0,29375,347036,50,29376,347036,30,29376,347036,40,29376,347105,0,29376,347243,50,29377,347312,0,29383,347502,50,29385,347502,30,29385,347502,40,29385,347571,0,29385,347676,50,29385,347676,30,29385,347676,40,29385,347745,0,29389,347933,50,29390,348002,0,29390,348249,50,29396,348318,0,29401,348575,50,29410,348644,0,29410,348911,50,29424,348980,0,29429,349258,50,29449,349327,0,29449,349619,50,29481,349688,0,29486,349996,50,29543,349996,40,29543,350065,0,29543,350464,50,29544,350464,30,29544,350464,40,29544,350533,0,29548,350721,50,29550,350790,0,29550,351037,50,29556,351106,0,29561,351363,50,29570,351432,0,29570,351699,50,29584,351768,0,29588,352046,50,29608,352115,0,29609,352407,50,29641,352476,0,29646,352784,50,29704,352784,40,29704,352853,0,29704)
%
%
% START OF PROOF
% 352616 [?] ?
% 352786 [] equal(multiply(identity,X),X).
% 352787 [] equal(multiply(inverse(X),X),identity).
% 352788 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 352789 [] -equal(multiply(sk_c9,sk_c8),sk_c10).
% 352838 [?] ?
% 352839 [?] ?
% 352840 [?] ?
% 352841 [?] ?
% 352842 [?] ?
% 352843 [?] ?
% 352844 [?] ?
% 352845 [?] ?
% 352936 [input:352839,cut:352789] equal(inverse(sk_c6),sk_c7).
% 352937 [para:352936.1.1,352787.1.1.1] equal(multiply(sk_c7,sk_c6),identity).
% 352938 [input:352842,cut:352789] equal(inverse(sk_c5),sk_c10).
% 352939 [para:352938.1.1,352787.1.1.1] equal(multiply(sk_c10,sk_c5),identity).
% 352941 [input:352844,cut:352789] equal(inverse(sk_c4),sk_c10).
% 352942 [para:352941.1.1,352787.1.1.1] equal(multiply(sk_c10,sk_c4),identity).
% 352962 [input:352838,cut:352789] equal(multiply(sk_c7,sk_c8),sk_c9).
% 352963 [input:352840,cut:352789] equal(multiply(sk_c6,sk_c7),sk_c9).
% 352964 [input:352841,cut:352789] equal(multiply(sk_c5,sk_c9),sk_c10).
% 352965 [input:352843,cut:352789] equal(multiply(sk_c10,sk_c8),sk_c9).
% 352966 [input:352845,cut:352789] equal(multiply(sk_c4,sk_c10),sk_c9).
% 352972 [para:352787.1.1,352788.1.1.1,demod:352786] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 353011 [para:352937.1.1,352788.1.1.1,demod:352786] equal(X,multiply(sk_c7,multiply(sk_c6,X))).
% 353014 [para:352939.1.1,352788.1.1.1,demod:352786] equal(X,multiply(sk_c10,multiply(sk_c5,X))).
% 353015 [para:352942.1.1,352788.1.1.1,demod:352786] equal(X,multiply(sk_c10,multiply(sk_c4,X))).
% 353042 [para:352962.1.1,352788.1.1.1] equal(multiply(sk_c9,X),multiply(sk_c7,multiply(sk_c8,X))).
% 353058 [para:352963.1.1,353011.1.2.2] equal(sk_c7,multiply(sk_c7,sk_c9)).
% 353066 [para:352964.1.1,353014.1.2.2] equal(sk_c9,multiply(sk_c10,sk_c10)).
% 353074 [para:352966.1.1,353015.1.2.2] equal(sk_c10,multiply(sk_c10,sk_c9)).
% 353171 [para:352965.1.1,352972.1.2.2] equal(sk_c8,multiply(inverse(sk_c10),sk_c9)).
% 353182 [para:353066.1.2,352972.1.2.2,demod:353171] equal(sk_c10,sk_c8).
% 353216 [para:353182.1.1,352965.1.1.1] equal(multiply(sk_c8,sk_c8),sk_c9).
% 353217 [para:353182.1.1,352966.1.1.2] equal(multiply(sk_c4,sk_c8),sk_c9).
% 353228 [para:353216.1.1,353042.1.2.2,demod:353058] equal(multiply(sk_c9,sk_c8),sk_c7).
% 353231 [para:353217.1.1,353015.1.2.2,demod:353074] equal(sk_c8,sk_c10).
% 353232 [para:353231.1.2,352789.1.2,demod:353228,cut:352616] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% Split component 8 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c9,sk_c10),sk_c8) | -equal(multiply(sk_c9,sk_c8),sk_c10) | -equal(inverse(sk_c10),sk_c8) | -equal(multiply(X,Y),sk_c9) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c8),sk_c9) | -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c9),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c10) | -equal(multiply(V,sk_c9),sk_c10) | -equal(multiply(W,X1),sk_c9) | -equal(inverse(W),X1) | -equal(multiply(X1,sk_c8),sk_c9).
% Split part used next: -equal(inverse(sk_c10),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 31
% clause depth limited to 3
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 4
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 5
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 6
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 7
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 8
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 9
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(69,40,0,144,0,0,2753,50,35,2828,0,35,8202,50,100,8277,0,100,13657,50,172,13732,0,172,20118,50,271,20193,0,271,27336,50,397,27411,0,397,35812,50,574,35887,0,574,45297,50,813,45297,40,813,45372,0,813,58218,3,1114,58835,4,1264,59386,5,1414,59387,1,1414,59387,50,1414,59387,40,1414,59462,0,1414,59696,3,1722,59705,4,1875,59712,5,2015,59712,1,2015,59712,50,2015,59712,40,2015,59787,0,2015,82870,3,3516,83752,4,4266,85106,5,5016,85107,1,5016,85107,50,5016,85107,40,5016,85182,0,5016,96504,3,5767,97775,4,6142,99577,50,6421,99577,40,6421,99652,0,6421,115598,3,7174,116227,4,7547,116875,1,7922,116875,50,7922,116875,40,7922,116950,0,7922,174318,3,11824,175091,4,13773,175919,1,15723,175919,50,15725,175919,40,15725,175994,0,15725,216808,3,18276,217578,4,19551,218307,1,20826,218307,50,20827,218307,40,20827,218382,0,20827,264485,3,22332,265133,4,23078,265759,5,23828,265760,1,23828,265760,50,23829,265760,40,23829,265835,0,23829,285656,3,24580,286208,4,24955,286650,5,25330,286651,1,25330,286651,50,25330,286651,40,25330,286726,0,25330,318765,3,26532,319348,4,27131,319839,5,27731,319840,1,27731,319840,50,27732,319840,40,27732,319915,0,27732,342606,3,28490,343133,4,28858,343553,5,29233,343554,1,29233,343554,50,29234,343554,40,29234,343554,40,29234,343623,0,29234,343728,50,29234,343728,30,29234,343728,40,29234,343797,0,29234,343950,50,29235,344019,0,29240,344212,50,29242,344212,30,29242,344212,40,29242,344281,0,29242,344452,50,29243,344521,0,29248,344746,50,29252,344815,0,29252,345050,50,29259,345119,0,29263,345364,50,29273,345433,0,29273,345689,50,29288,345758,0,29293,346030,50,29321,346099,0,29321,346387,50,29375,346387,40,29375,346456,0,29375,347036,50,29376,347036,30,29376,347036,40,29376,347105,0,29376,347243,50,29377,347312,0,29383,347502,50,29385,347502,30,29385,347502,40,29385,347571,0,29385,347676,50,29385,347676,30,29385,347676,40,29385,347745,0,29389,347933,50,29390,348002,0,29390,348249,50,29396,348318,0,29401,348575,50,29410,348644,0,29410,348911,50,29424,348980,0,29429,349258,50,29449,349327,0,29449,349619,50,29481,349688,0,29486,349996,50,29543,349996,40,29543,350065,0,29543,350464,50,29544,350464,30,29544,350464,40,29544,350533,0,29548,350721,50,29550,350790,0,29550,351037,50,29556,351106,0,29561,351363,50,29570,351432,0,29570,351699,50,29584,351768,0,29588,352046,50,29608,352115,0,29609,352407,50,29641,352476,0,29646,352784,50,29704,352784,40,29704,352853,0,29704,353231,50,29705,353231,30,29705,353231,40,29705,353300,0,29709,353488,50,29711,353557,0,29711,353805,50,29717,353874,0,29722,354132,50,29732,354201,0,29732,354469,50,29745,354538,0,29750,354817,50,29770,354886,0,29770,355180,50,29804,355249,0,29808,355559,50,29866,355559,40,29866,355628,0,29866)
%
%
% START OF PROOF
% 355561 [] equal(multiply(identity,X),X).
% 355562 [] equal(multiply(inverse(X),X),identity).
% 355563 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 355564 [] -equal(inverse(sk_c10),sk_c8).
% 355605 [?] ?
% 355606 [?] ?
% 355608 [?] ?
% 355609 [?] ?
% 355610 [?] ?
% 355611 [?] ?
% 355612 [?] ?
% 355650 [input:355606,cut:355564] equal(inverse(sk_c6),sk_c7).
% 355651 [para:355650.1.1,355562.1.1.1] equal(multiply(sk_c7,sk_c6),identity).
% 355652 [input:355609,cut:355564] equal(inverse(sk_c5),sk_c10).
% 355653 [para:355652.1.1,355562.1.1.1] equal(multiply(sk_c10,sk_c5),identity).
% 355654 [input:355611,cut:355564] equal(inverse(sk_c4),sk_c10).
% 355655 [para:355654.1.1,355562.1.1.1] equal(multiply(sk_c10,sk_c4),identity).
% 355690 [input:355605,cut:355564] equal(multiply(sk_c7,sk_c8),sk_c9).
% 355692 [input:355608,cut:355564] equal(multiply(sk_c5,sk_c9),sk_c10).
% 355693 [input:355610,cut:355564] equal(multiply(sk_c10,sk_c8),sk_c9).
% 355694 [input:355612,cut:355564] equal(multiply(sk_c4,sk_c10),sk_c9).
% 355725 [para:355562.1.1,355563.1.1.1,demod:355561] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 355730 [para:355653.1.1,355563.1.1.1,demod:355561] equal(X,multiply(sk_c10,multiply(sk_c5,X))).
% 355733 [para:355655.1.1,355563.1.1.1,demod:355561] equal(X,multiply(sk_c10,multiply(sk_c4,X))).
% 355764 [para:355692.1.1,355563.1.1.1] equal(multiply(sk_c10,X),multiply(sk_c5,multiply(sk_c9,X))).
% 355806 [para:355692.1.1,355730.1.2.2] equal(sk_c9,multiply(sk_c10,sk_c10)).
% 355818 [para:355651.1.1,355725.1.2.2] equal(sk_c6,multiply(inverse(sk_c7),identity)).
% 355819 [para:355653.1.1,355725.1.2.2] equal(sk_c5,multiply(inverse(sk_c10),identity)).
% 355861 [para:355690.1.1,355725.1.2.2] equal(sk_c8,multiply(inverse(sk_c7),sk_c9)).
% 355864 [para:355693.1.1,355725.1.2.2] equal(sk_c8,multiply(inverse(sk_c10),sk_c9)).
% 355899 [para:355730.1.2,355725.1.2.2] equal(multiply(sk_c5,X),multiply(inverse(sk_c10),X)).
% 355900 [para:355806.1.2,355725.1.2.2,demod:355864] equal(sk_c10,sk_c8).
% 355901 [para:355733.1.2,355725.1.2.2,demod:355899] equal(multiply(sk_c4,X),multiply(sk_c5,X)).
% 355909 [para:355900.1.1,355564.1.1.1] -equal(inverse(sk_c8),sk_c8).
% 355919 [para:355900.1.1,355694.1.1.2] equal(multiply(sk_c4,sk_c8),sk_c9).
% 355935 [para:355919.1.1,355563.1.1.1] equal(multiply(sk_c9,X),multiply(sk_c4,multiply(sk_c8,X))).
% 355949 [para:355864.1.2,355563.1.1.1,demod:355764,355899] equal(multiply(sk_c8,X),multiply(sk_c10,X)).
% 355955 [para:355949.1.2,355725.1.2.2,demod:355935,355901,355899] equal(X,multiply(sk_c9,X)).
% 355956 [para:355955.1.2,355725.1.2.2] equal(X,multiply(inverse(sk_c9),X)).
% 355958 [para:355956.1.2,355562.1.1] equal(sk_c9,identity).
% 355967 [para:355958.1.1,355861.1.2.2,demod:355818] equal(sk_c8,sk_c6).
% 355969 [para:355958.1.1,355864.1.2.2,demod:355819] equal(sk_c8,sk_c5).
% 355973 [para:355967.1.2,355650.1.1.1] equal(inverse(sk_c8),sk_c7).
% 355981 [para:355969.1.2,355652.1.1.1,demod:355973] equal(sk_c7,sk_c10).
% 355992 [para:355981.1.2,355900.1.1] equal(sk_c7,sk_c8).
% 356023 [para:355973.1.1,355909.1.1,cut:355992] 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 9 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c9,sk_c10),sk_c8) | -equal(multiply(sk_c9,sk_c8),sk_c10) | -equal(inverse(sk_c10),sk_c8) | -equal(multiply(X,Y),sk_c9) | -equal(inverse(X),Y) | -equal(multiply(Y,sk_c8),sk_c9) | -equal(inverse(Z),sk_c8) | -equal(multiply(Z,sk_c9),sk_c8) | -equal(multiply(U,sk_c10),sk_c9) | -equal(inverse(U),sk_c10) | -equal(multiply(sk_c10,sk_c8),sk_c9) | -equal(inverse(V),sk_c10) | -equal(multiply(V,sk_c9),sk_c10) | -equal(multiply(W,X1),sk_c9) | -equal(inverse(W),X1) | -equal(multiply(X1,sk_c8),sk_c9).
% Split part used next: -equal(multiply(sk_c10,sk_c8),sk_c9).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 3
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 4
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 5
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 6
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 7
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 8
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 31
% clause depth limited to 9
% seconds given: 2
%
%
% proof attempt stopped: sos exhausted
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(69,40,0,144,0,0,2753,50,35,2828,0,35,8202,50,100,8277,0,100,13657,50,172,13732,0,172,20118,50,271,20193,0,271,27336,50,397,27411,0,397,35812,50,574,35887,0,574,45297,50,813,45297,40,813,45372,0,813,58218,3,1114,58835,4,1264,59386,5,1414,59387,1,1414,59387,50,1414,59387,40,1414,59462,0,1414,59696,3,1722,59705,4,1875,59712,5,2015,59712,1,2015,59712,50,2015,59712,40,2015,59787,0,2015,82870,3,3516,83752,4,4266,85106,5,5016,85107,1,5016,85107,50,5016,85107,40,5016,85182,0,5016,96504,3,5767,97775,4,6142,99577,50,6421,99577,40,6421,99652,0,6421,115598,3,7174,116227,4,7547,116875,1,7922,116875,50,7922,116875,40,7922,116950,0,7922,174318,3,11824,175091,4,13773,175919,1,15723,175919,50,15725,175919,40,15725,175994,0,15725,216808,3,18276,217578,4,19551,218307,1,20826,218307,50,20827,218307,40,20827,218382,0,20827,264485,3,22332,265133,4,23078,265759,5,23828,265760,1,23828,265760,50,23829,265760,40,23829,265835,0,23829,285656,3,24580,286208,4,24955,286650,5,25330,286651,1,25330,286651,50,25330,286651,40,25330,286726,0,25330,318765,3,26532,319348,4,27131,319839,5,27731,319840,1,27731,319840,50,27732,319840,40,27732,319915,0,27732,342606,3,28490,343133,4,28858,343553,5,29233,343554,1,29233,343554,50,29234,343554,40,29234,343554,40,29234,343623,0,29234,343728,50,29234,343728,30,29234,343728,40,29234,343797,0,29234,343950,50,29235,344019,0,29240,344212,50,29242,344212,30,29242,344212,40,29242,344281,0,29242,344452,50,29243,344521,0,29248,344746,50,29252,344815,0,29252,345050,50,29259,345119,0,29263,345364,50,29273,345433,0,29273,345689,50,29288,345758,0,29293,346030,50,29321,346099,0,29321,346387,50,29375,346387,40,29375,346456,0,29375,347036,50,29376,347036,30,29376,347036,40,29376,347105,0,29376,347243,50,29377,347312,0,29383,347502,50,29385,347502,30,29385,347502,40,29385,347571,0,29385,347676,50,29385,347676,30,29385,347676,40,29385,347745,0,29389,347933,50,29390,348002,0,29390,348249,50,29396,348318,0,29401,348575,50,29410,348644,0,29410,348911,50,29424,348980,0,29429,349258,50,29449,349327,0,29449,349619,50,29481,349688,0,29486,349996,50,29543,349996,40,29543,350065,0,29543,350464,50,29544,350464,30,29544,350464,40,29544,350533,0,29548,350721,50,29550,350790,0,29550,351037,50,29556,351106,0,29561,351363,50,29570,351432,0,29570,351699,50,29584,351768,0,29588,352046,50,29608,352115,0,29609,352407,50,29641,352476,0,29646,352784,50,29704,352784,40,29704,352853,0,29704,353231,50,29705,353231,30,29705,353231,40,29705,353300,0,29709,353488,50,29711,353557,0,29711,353805,50,29717,353874,0,29722,354132,50,29732,354201,0,29732,354469,50,29745,354538,0,29750,354817,50,29770,354886,0,29770,355180,50,29804,355249,0,29808,355559,50,29866,355559,40,29866,355628,0,29866,356022,50,29868,356022,30,29868,356022,40,29868,356091,0,29873,356246,50,29874,356315,0,29874,356524,50,29879,356593,0,29883,356812,50,29890,356881,0,29890,357110,50,29901,357179,0,29906,357420,50,29922,357489,0,29922,357743,50,29950,357812,0,29954,358082,50,30005,358082,40,30005,358151,0,30005)
%
%
% START OF PROOF
% 357949 [?] ?
% 358084 [] equal(multiply(identity,X),X).
% 358085 [] equal(multiply(inverse(X),X),identity).
% 358086 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 358087 [] -equal(multiply(sk_c10,sk_c8),sk_c9).
% 358101 [?] ?
% 358133 [?] ?
% 358193 [input:358101,cut:358087] equal(inverse(sk_c3),sk_c8).
% 358194 [para:358193.1.1,358085.1.1.1] equal(multiply(sk_c8,sk_c3),identity).
% 358228 [input:358133,cut:358087] equal(inverse(sk_c10),sk_c8).
% 358229 [para:358228.1.1,358085.1.1.1] equal(multiply(sk_c8,sk_c10),identity).
% 358270 [para:358085.1.1,358086.1.1.1,demod:358084] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 358281 [para:358194.1.1,358086.1.1.1,demod:358084] equal(X,multiply(sk_c8,multiply(sk_c3,X))).
% 358388 [para:358194.1.1,358270.1.2.2] equal(sk_c3,multiply(inverse(sk_c8),identity)).
% 358418 [para:358229.1.1,358270.1.2.2,demod:358388] equal(sk_c10,sk_c3).
% 358470 [para:358281.1.2,358270.1.2.2] equal(multiply(sk_c3,X),multiply(inverse(sk_c8),X)).
% 358476 [para:358418.1.1,358087.1.1.1] -equal(multiply(sk_c3,sk_c8),sk_c9).
% 358512 [para:358470.1.2,358085.1.1] equal(multiply(sk_c3,sk_c8),identity).
% 358516 [para:358512.1.1,358476.1.1,cut:357949] 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: 46371
% derived clauses: 4362689
% kept clauses: 262467
% kept size sum: 74423
% kept mid-nuclei: 27130
% kept new demods: 7982
% forw unit-subs: 1412274
% forw double-subs: 2404965
% forw overdouble-subs: 194341
% backward subs: 28103
% fast unit cutoff: 27845
% full unit cutoff: 0
% dbl unit cutoff: 24069
% real runtime : 301.62
% process. runtime: 300.6
% specific non-discr-tree subsumption statistics:
% tried: 25460641
% length fails: 2415133
% strength fails: 7649265
% predlist fails: 2003982
% aux str. fails: 3533015
% by-lit fails: 6164554
% full subs tried: 660891
% full subs fail: 575865
%
% ; 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/GRP349-1+eq_r.in")
%
%------------------------------------------------------------------------------