%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP240-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 : art04.cs.miami.edu
% Model : i686 unknown
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 1000MB
% OS : Linux 2.4.22-21mdk-i686-up-4GB
% CPULimit : 600s
% Result : Unsatisfiable 297.8s
% Output : Assurance 297.8s
% 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/GRP240-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 29)
% (binary-unit 12 #f)
% (binary-unit-uniteq 12 #f)
% (binary-posweight-kb-big-order 60 #f 3 29)
% (binary-posweight-lex-big-order 30 #f 3 29)
% (binary 30 #t)
% (binary-posweight-kb-big-order 156 #f)
% (binary-posweight-lex-big-order 102 #f)
% (binary-posweight-firstpref-order 60 #f)
% (binary-order 30 #f)
% (binary-posweight-kb-small-order 48 #f)
% (binary-posweight-lex-small-order 30 #f)
%
%
% SOS clause
% -equal(inverse(sk_c10),sk_c9) | -equal(inverse(sk_c9),sk_c10) | -equal(multiply(X,sk_c9),sk_c10) | -equal(inverse(X),sk_c9) | -equal(multiply(sk_c10,Y),sk_c9) | -equal(multiply(Z,sk_c10),Y) | -equal(inverse(Z),sk_c10) | -equal(inverse(U),sk_c10) | -equal(multiply(U,sk_c9),sk_c10) | -equal(multiply(V,W),sk_c9) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c9) | -equal(multiply(sk_c10,X1),sk_c9) | -equal(multiply(X2,sk_c10),X1) | -equal(inverse(X2),sk_c10).
% was split for some strategies as:
% -equal(multiply(sk_c10,X1),sk_c9) | -equal(multiply(X2,sk_c10),X1) | -equal(inverse(X2),sk_c10).
% -equal(multiply(V,W),sk_c9) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c9).
% -equal(inverse(U),sk_c10) | -equal(multiply(U,sk_c9),sk_c10).
% -equal(multiply(sk_c10,Y),sk_c9) | -equal(multiply(Z,sk_c10),Y) | -equal(inverse(Z),sk_c10).
% -equal(multiply(X,sk_c9),sk_c10) | -equal(inverse(X),sk_c9).
% -equal(inverse(sk_c10),sk_c9).
% -equal(inverse(sk_c9),sk_c10).
%
% 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(inverse(sk_c10),sk_c9) | -equal(inverse(sk_c9),sk_c10) | -equal(multiply(X,sk_c9),sk_c10) | -equal(inverse(X),sk_c9) | -equal(multiply(sk_c10,Y),sk_c9) | -equal(multiply(Z,sk_c10),Y) | -equal(inverse(Z),sk_c10) | -equal(inverse(U),sk_c10) | -equal(multiply(U,sk_c9),sk_c10) | -equal(multiply(V,W),sk_c9) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c9) | -equal(multiply(sk_c10,X1),sk_c9) | -equal(multiply(X2,sk_c10),X1) | -equal(inverse(X2),sk_c10).
% Split part used next: -equal(multiply(sk_c10,X1),sk_c9) | -equal(multiply(X2,sk_c10),X1) | -equal(inverse(X2),sk_c10).
% END OF PROOFPART
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(61,40,0,128,0,0,151699,5,1501,151700,1,1501,151700,50,1501,151700,40,1501,151767,0,1501,160250,3,1839,161070,4,1952,162012,1,2102,162012,50,2102,162012,40,2102,162079,0,2102,163845,3,2420,163855,4,2561,163993,5,2703,163993,1,2703,163993,50,2703,163993,40,2703,164060,0,2703,187431,3,4205,188147,4,4954,188772,1,5704,188772,50,5704,188772,40,5704,188839,0,5704,207174,3,6458,207600,4,6830,208003,5,7205,208004,1,7205,208004,50,7205,208004,40,7205,208071,0,7205,220020,3,7979,221263,4,8331,222940,5,8706,222941,5,8706,222942,1,8706,222942,50,8706,222942,40,8706,223009,0,8706,279616,3,12607,280151,4,14557,280461,1,16507,280461,50,16509,280461,40,16509,280528,0,16509,324782,3,19060,325193,4,20336,325212,1,21610,325212,50,21611,325212,40,21611,325279,0,21611,358127,3,23112,359020,4,23862,359618,5,24612,359619,1,24612,359619,50,24613,359619,40,24613,359686,0,24613,373832,3,25364,375042,4,25739,375694,5,26114,375695,1,26114,375695,50,26114,375695,40,26114,375762,0,26114,401169,3,27315,401949,4,27915,402734,5,28515,402735,1,28515,402735,50,28516,402735,40,28516,402802,0,28516,422787,3,29274,423402,4,29642,424012,1,30017,424012,50,30017,424012,40,30017,424012,40,30017,424073,0,30018)
%
%
% START OF PROOF
% 424013 [] equal(X,X).
% 424017 [] -equal(multiply(sk_c10,X),sk_c9) | -equal(multiply(Y,sk_c10),X) | -equal(inverse(Y),sk_c10).
% 424018 [] equal(inverse(sk_c2),sk_c10) | equal(inverse(sk_c7),sk_c10).
% 424019 [] equal(multiply(sk_c7,sk_c10),sk_c8) | equal(inverse(sk_c2),sk_c10).
% 424020 [?] ?
% 424026 [] equal(multiply(sk_c2,sk_c10),sk_c3) | equal(inverse(sk_c7),sk_c10).
% 424027 [] equal(multiply(sk_c2,sk_c10),sk_c3) | equal(multiply(sk_c7,sk_c10),sk_c8).
% 424028 [] equal(multiply(sk_c2,sk_c10),sk_c3) | equal(multiply(sk_c10,sk_c8),sk_c9).
% 424034 [?] ?
% 424035 [?] ?
% 424036 [?] ?
% 424118 [hyper:424017,424019,424018,binarycut:424020] equal(inverse(sk_c2),sk_c10).
% 424130 [hyper:424017,424026,demod:424118,cut:424013,binarycut:424034] equal(inverse(sk_c7),sk_c10).
% 424156 [hyper:424017,424027,demod:424118,cut:424013,binarycut:424035] equal(multiply(sk_c7,sk_c10),sk_c8).
% 424173 [hyper:424017,424028,demod:424118,cut:424013,binarycut:424036] equal(multiply(sk_c10,sk_c8),sk_c9).
% 424177 [hyper:424017,424173,424156,demod:424130,cut:424013] 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 29
% clause depth limited to 3
% seconds given: 4
%
%
% Split component 2 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(inverse(sk_c10),sk_c9) | -equal(inverse(sk_c9),sk_c10) | -equal(multiply(X,sk_c9),sk_c10) | -equal(inverse(X),sk_c9) | -equal(multiply(sk_c10,Y),sk_c9) | -equal(multiply(Z,sk_c10),Y) | -equal(inverse(Z),sk_c10) | -equal(inverse(U),sk_c10) | -equal(multiply(U,sk_c9),sk_c10) | -equal(multiply(V,W),sk_c9) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c9) | -equal(multiply(sk_c10,X1),sk_c9) | -equal(multiply(X2,sk_c10),X1) | -equal(inverse(X2),sk_c10).
% Split part used next: -equal(multiply(V,W),sk_c9) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c9).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 29
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(61,40,0,128,0,0,151699,5,1501,151700,1,1501,151700,50,1501,151700,40,1501,151767,0,1501,160250,3,1839,161070,4,1952,162012,1,2102,162012,50,2102,162012,40,2102,162079,0,2102,163845,3,2420,163855,4,2561,163993,5,2703,163993,1,2703,163993,50,2703,163993,40,2703,164060,0,2703,187431,3,4205,188147,4,4954,188772,1,5704,188772,50,5704,188772,40,5704,188839,0,5704,207174,3,6458,207600,4,6830,208003,5,7205,208004,1,7205,208004,50,7205,208004,40,7205,208071,0,7205,220020,3,7979,221263,4,8331,222940,5,8706,222941,5,8706,222942,1,8706,222942,50,8706,222942,40,8706,223009,0,8706,279616,3,12607,280151,4,14557,280461,1,16507,280461,50,16509,280461,40,16509,280528,0,16509,324782,3,19060,325193,4,20336,325212,1,21610,325212,50,21611,325212,40,21611,325279,0,21611,358127,3,23112,359020,4,23862,359618,5,24612,359619,1,24612,359619,50,24613,359619,40,24613,359686,0,24613,373832,3,25364,375042,4,25739,375694,5,26114,375695,1,26114,375695,50,26114,375695,40,26114,375762,0,26114,401169,3,27315,401949,4,27915,402734,5,28515,402735,1,28515,402735,50,28516,402735,40,28516,402802,0,28516,422787,3,29274,423402,4,29642,424012,1,30017,424012,50,30017,424012,40,30017,424012,40,30017,424073,0,30018,424176,50,30018,424176,30,30018,424176,40,30018,424237,0,30018)
%
%
% START OF PROOF
% 424178 [] equal(multiply(identity,X),X).
% 424179 [] equal(multiply(inverse(X),X),identity).
% 424180 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 424181 [] -equal(multiply(X,sk_c10),sk_c9) | -equal(multiply(Y,X),sk_c9) | -equal(inverse(Y),X).
% 424185 [?] ?
% 424186 [] equal(inverse(sk_c2),sk_c10) | equal(inverse(sk_c5),sk_c6).
% 424187 [?] ?
% 424193 [] equal(multiply(sk_c2,sk_c10),sk_c3) | equal(multiply(sk_c6,sk_c10),sk_c9).
% 424194 [] equal(multiply(sk_c2,sk_c10),sk_c3) | equal(inverse(sk_c5),sk_c6).
% 424195 [] equal(multiply(sk_c2,sk_c10),sk_c3) | equal(multiply(sk_c5,sk_c6),sk_c9).
% 424201 [] equal(multiply(sk_c10,sk_c3),sk_c9) | equal(multiply(sk_c6,sk_c10),sk_c9).
% 424202 [] equal(multiply(sk_c10,sk_c3),sk_c9) | equal(inverse(sk_c5),sk_c6).
% 424203 [] equal(multiply(sk_c10,sk_c3),sk_c9) | equal(multiply(sk_c5,sk_c6),sk_c9).
% 424209 [?] ?
% 424210 [] equal(inverse(sk_c1),sk_c9) | equal(inverse(sk_c5),sk_c6).
% 424211 [?] ?
% 424217 [] equal(multiply(sk_c1,sk_c9),sk_c10) | equal(multiply(sk_c6,sk_c10),sk_c9).
% 424218 [] equal(multiply(sk_c1,sk_c9),sk_c10) | equal(inverse(sk_c5),sk_c6).
% 424219 [] equal(multiply(sk_c1,sk_c9),sk_c10) | equal(multiply(sk_c5,sk_c6),sk_c9).
% 424225 [?] ?
% 424226 [] equal(inverse(sk_c9),sk_c10) | equal(inverse(sk_c5),sk_c6).
% 424227 [?] ?
% 424233 [?] ?
% 424234 [] equal(inverse(sk_c10),sk_c9) | equal(inverse(sk_c5),sk_c6).
% 424235 [?] ?
% 424246 [hyper:424181,424186,binarycut:424187,binarycut:424185] equal(inverse(sk_c2),sk_c10).
% 424249 [para:424246.1.1,424179.1.1.1] equal(multiply(sk_c10,sk_c2),identity).
% 424259 [hyper:424181,424210,binarycut:424211,binarycut:424209] equal(inverse(sk_c1),sk_c9).
% 424262 [para:424259.1.1,424179.1.1.1] equal(multiply(sk_c9,sk_c1),identity).
% 424275 [hyper:424181,424226,binarycut:424227,binarycut:424225] equal(inverse(sk_c9),sk_c10).
% 424289 [hyper:424181,424234,binarycut:424235,binarycut:424233] equal(inverse(sk_c10),sk_c9).
% 424292 [para:424289.1.1,424179.1.1.1] equal(multiply(sk_c9,sk_c10),identity).
% 424336 [hyper:424181,424195,424193,424194] equal(multiply(sk_c2,sk_c10),sk_c3).
% 424357 [hyper:424181,424203,424201,424202] equal(multiply(sk_c10,sk_c3),sk_c9).
% 424374 [hyper:424181,424219,424217,424218] equal(multiply(sk_c1,sk_c9),sk_c10).
% 424375 [para:424179.1.1,424180.1.1.1,demod:424178] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 424376 [para:424249.1.1,424180.1.1.1,demod:424178] equal(X,multiply(sk_c10,multiply(sk_c2,X))).
% 424377 [para:424262.1.1,424180.1.1.1,demod:424178] equal(X,multiply(sk_c9,multiply(sk_c1,X))).
% 424385 [para:424336.1.1,424376.1.2.2,demod:424357] equal(sk_c10,sk_c9).
% 424401 [para:424374.1.1,424375.1.2.2,demod:424292,424259] equal(sk_c9,identity).
% 424411 [para:424377.1.2,424375.1.2.2,demod:424275] equal(multiply(sk_c1,X),multiply(sk_c10,X)).
% 424418 [para:424401.1.1,424275.1.1.1] equal(inverse(identity),sk_c10).
% 424423 [para:424401.1.1,424377.1.2.1,demod:424178] equal(X,multiply(sk_c1,X)).
% 424447 [hyper:424181,424418,demod:424423,424411,424178,cut:424385,cut:424385] 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 29
% clause depth limited to 3
% seconds given: 4
%
%
% Split component 3 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(inverse(sk_c10),sk_c9) | -equal(inverse(sk_c9),sk_c10) | -equal(multiply(X,sk_c9),sk_c10) | -equal(inverse(X),sk_c9) | -equal(multiply(sk_c10,Y),sk_c9) | -equal(multiply(Z,sk_c10),Y) | -equal(inverse(Z),sk_c10) | -equal(inverse(U),sk_c10) | -equal(multiply(U,sk_c9),sk_c10) | -equal(multiply(V,W),sk_c9) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c9) | -equal(multiply(sk_c10,X1),sk_c9) | -equal(multiply(X2,sk_c10),X1) | -equal(inverse(X2),sk_c10).
% Split part used next: -equal(inverse(U),sk_c10) | -equal(multiply(U,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 29
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(61,40,0,128,0,0,151699,5,1501,151700,1,1501,151700,50,1501,151700,40,1501,151767,0,1501,160250,3,1839,161070,4,1952,162012,1,2102,162012,50,2102,162012,40,2102,162079,0,2102,163845,3,2420,163855,4,2561,163993,5,2703,163993,1,2703,163993,50,2703,163993,40,2703,164060,0,2703,187431,3,4205,188147,4,4954,188772,1,5704,188772,50,5704,188772,40,5704,188839,0,5704,207174,3,6458,207600,4,6830,208003,5,7205,208004,1,7205,208004,50,7205,208004,40,7205,208071,0,7205,220020,3,7979,221263,4,8331,222940,5,8706,222941,5,8706,222942,1,8706,222942,50,8706,222942,40,8706,223009,0,8706,279616,3,12607,280151,4,14557,280461,1,16507,280461,50,16509,280461,40,16509,280528,0,16509,324782,3,19060,325193,4,20336,325212,1,21610,325212,50,21611,325212,40,21611,325279,0,21611,358127,3,23112,359020,4,23862,359618,5,24612,359619,1,24612,359619,50,24613,359619,40,24613,359686,0,24613,373832,3,25364,375042,4,25739,375694,5,26114,375695,1,26114,375695,50,26114,375695,40,26114,375762,0,26114,401169,3,27315,401949,4,27915,402734,5,28515,402735,1,28515,402735,50,28516,402735,40,28516,402802,0,28516,422787,3,29274,423402,4,29642,424012,1,30017,424012,50,30017,424012,40,30017,424012,40,30017,424073,0,30018,424176,50,30018,424176,30,30018,424176,40,30018,424237,0,30018,424446,50,30018,424446,30,30018,424446,40,30018,424507,0,30023)
%
%
% START OF PROOF
% 424448 [] equal(multiply(identity,X),X).
% 424449 [] equal(multiply(inverse(X),X),identity).
% 424450 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 424451 [] -equal(multiply(X,sk_c9),sk_c10) | -equal(inverse(X),sk_c10).
% 424458 [?] ?
% 424459 [] equal(inverse(sk_c2),sk_c10) | equal(inverse(sk_c4),sk_c10).
% 424466 [] equal(multiply(sk_c2,sk_c10),sk_c3) | equal(multiply(sk_c4,sk_c9),sk_c10).
% 424467 [] equal(multiply(sk_c2,sk_c10),sk_c3) | equal(inverse(sk_c4),sk_c10).
% 424474 [] equal(multiply(sk_c10,sk_c3),sk_c9) | equal(multiply(sk_c4,sk_c9),sk_c10).
% 424475 [] equal(multiply(sk_c10,sk_c3),sk_c9) | equal(inverse(sk_c4),sk_c10).
% 424482 [?] ?
% 424483 [] equal(inverse(sk_c1),sk_c9) | equal(inverse(sk_c4),sk_c10).
% 424490 [] equal(multiply(sk_c1,sk_c9),sk_c10) | equal(multiply(sk_c4,sk_c9),sk_c10).
% 424491 [] equal(multiply(sk_c1,sk_c9),sk_c10) | equal(inverse(sk_c4),sk_c10).
% 424498 [?] ?
% 424499 [] equal(inverse(sk_c9),sk_c10) | equal(inverse(sk_c4),sk_c10).
% 424506 [?] ?
% 424507 [] equal(inverse(sk_c10),sk_c9) | equal(inverse(sk_c4),sk_c10).
% 424517 [hyper:424451,424459,binarycut:424458] equal(inverse(sk_c2),sk_c10).
% 424520 [para:424517.1.1,424449.1.1.1] equal(multiply(sk_c10,sk_c2),identity).
% 424528 [hyper:424451,424483,binarycut:424482] equal(inverse(sk_c1),sk_c9).
% 424532 [para:424528.1.1,424449.1.1.1] equal(multiply(sk_c9,sk_c1),identity).
% 424544 [hyper:424451,424499,binarycut:424498] equal(inverse(sk_c9),sk_c10).
% 424556 [hyper:424451,424507,binarycut:424506] equal(inverse(sk_c10),sk_c9).
% 424558 [para:424556.1.1,424449.1.1.1] equal(multiply(sk_c9,sk_c10),identity).
% 424582 [hyper:424451,424466,424467] equal(multiply(sk_c2,sk_c10),sk_c3).
% 424594 [hyper:424451,424474,424475] equal(multiply(sk_c10,sk_c3),sk_c9).
% 424610 [hyper:424451,424490,424491] equal(multiply(sk_c1,sk_c9),sk_c10).
% 424614 [para:424449.1.1,424450.1.1.1,demod:424448] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 424615 [para:424520.1.1,424450.1.1.1,demod:424448] equal(X,multiply(sk_c10,multiply(sk_c2,X))).
% 424622 [para:424582.1.1,424615.1.2.2,demod:424594] equal(sk_c10,sk_c9).
% 424623 [para:424622.1.1,424520.1.1.1] equal(multiply(sk_c9,sk_c2),identity).
% 424632 [para:424532.1.1,424614.1.2.2,demod:424544] equal(sk_c1,multiply(sk_c10,identity)).
% 424636 [para:424610.1.1,424614.1.2.2,demod:424558,424528] equal(sk_c9,identity).
% 424638 [para:424623.1.1,424614.1.2.2,demod:424632,424544] equal(sk_c2,sk_c1).
% 424651 [para:424636.1.1,424544.1.1.1] equal(inverse(identity),sk_c10).
% 424657 [para:424638.1.1,424517.1.1.1,demod:424528] equal(sk_c9,sk_c10).
% 424676 [hyper:424451,424651,demod:424448,cut:424657] 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 29
% clause depth limited to 3
% seconds given: 4
%
%
% Split component 4 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(inverse(sk_c10),sk_c9) | -equal(inverse(sk_c9),sk_c10) | -equal(multiply(X,sk_c9),sk_c10) | -equal(inverse(X),sk_c9) | -equal(multiply(sk_c10,Y),sk_c9) | -equal(multiply(Z,sk_c10),Y) | -equal(inverse(Z),sk_c10) | -equal(inverse(U),sk_c10) | -equal(multiply(U,sk_c9),sk_c10) | -equal(multiply(V,W),sk_c9) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c9) | -equal(multiply(sk_c10,X1),sk_c9) | -equal(multiply(X2,sk_c10),X1) | -equal(inverse(X2),sk_c10).
% Split part used next: -equal(multiply(sk_c10,Y),sk_c9) | -equal(multiply(Z,sk_c10),Y) | -equal(inverse(Z),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 29
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(61,40,0,128,0,0,151699,5,1501,151700,1,1501,151700,50,1501,151700,40,1501,151767,0,1501,160250,3,1839,161070,4,1952,162012,1,2102,162012,50,2102,162012,40,2102,162079,0,2102,163845,3,2420,163855,4,2561,163993,5,2703,163993,1,2703,163993,50,2703,163993,40,2703,164060,0,2703,187431,3,4205,188147,4,4954,188772,1,5704,188772,50,5704,188772,40,5704,188839,0,5704,207174,3,6458,207600,4,6830,208003,5,7205,208004,1,7205,208004,50,7205,208004,40,7205,208071,0,7205,220020,3,7979,221263,4,8331,222940,5,8706,222941,5,8706,222942,1,8706,222942,50,8706,222942,40,8706,223009,0,8706,279616,3,12607,280151,4,14557,280461,1,16507,280461,50,16509,280461,40,16509,280528,0,16509,324782,3,19060,325193,4,20336,325212,1,21610,325212,50,21611,325212,40,21611,325279,0,21611,358127,3,23112,359020,4,23862,359618,5,24612,359619,1,24612,359619,50,24613,359619,40,24613,359686,0,24613,373832,3,25364,375042,4,25739,375694,5,26114,375695,1,26114,375695,50,26114,375695,40,26114,375762,0,26114,401169,3,27315,401949,4,27915,402734,5,28515,402735,1,28515,402735,50,28516,402735,40,28516,402802,0,28516,422787,3,29274,423402,4,29642,424012,1,30017,424012,50,30017,424012,40,30017,424012,40,30017,424073,0,30018,424176,50,30018,424176,30,30018,424176,40,30018,424237,0,30018,424446,50,30018,424446,30,30018,424446,40,30018,424507,0,30023,424675,50,30023,424675,30,30023,424675,40,30023,424736,0,30023)
%
%
% START OF PROOF
% 424676 [] equal(X,X).
% 424680 [] -equal(multiply(sk_c10,X),sk_c9) | -equal(multiply(Y,sk_c10),X) | -equal(inverse(Y),sk_c10).
% 424681 [] equal(inverse(sk_c2),sk_c10) | equal(inverse(sk_c7),sk_c10).
% 424682 [] equal(multiply(sk_c7,sk_c10),sk_c8) | equal(inverse(sk_c2),sk_c10).
% 424683 [?] ?
% 424689 [] equal(multiply(sk_c2,sk_c10),sk_c3) | equal(inverse(sk_c7),sk_c10).
% 424690 [] equal(multiply(sk_c2,sk_c10),sk_c3) | equal(multiply(sk_c7,sk_c10),sk_c8).
% 424691 [] equal(multiply(sk_c2,sk_c10),sk_c3) | equal(multiply(sk_c10,sk_c8),sk_c9).
% 424697 [?] ?
% 424698 [?] ?
% 424699 [?] ?
% 424781 [hyper:424680,424682,424681,binarycut:424683] equal(inverse(sk_c2),sk_c10).
% 424793 [hyper:424680,424689,demod:424781,cut:424676,binarycut:424697] equal(inverse(sk_c7),sk_c10).
% 424819 [hyper:424680,424690,demod:424781,cut:424676,binarycut:424698] equal(multiply(sk_c7,sk_c10),sk_c8).
% 424836 [hyper:424680,424691,demod:424781,cut:424676,binarycut:424699] equal(multiply(sk_c10,sk_c8),sk_c9).
% 424840 [hyper:424680,424836,424819,demod:424793,cut:424676] 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 29
% clause depth limited to 3
% seconds given: 4
%
%
% Split component 5 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(inverse(sk_c10),sk_c9) | -equal(inverse(sk_c9),sk_c10) | -equal(multiply(X,sk_c9),sk_c10) | -equal(inverse(X),sk_c9) | -equal(multiply(sk_c10,Y),sk_c9) | -equal(multiply(Z,sk_c10),Y) | -equal(inverse(Z),sk_c10) | -equal(inverse(U),sk_c10) | -equal(multiply(U,sk_c9),sk_c10) | -equal(multiply(V,W),sk_c9) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c9) | -equal(multiply(sk_c10,X1),sk_c9) | -equal(multiply(X2,sk_c10),X1) | -equal(inverse(X2),sk_c10).
% Split part used next: -equal(multiply(X,sk_c9),sk_c10) | -equal(inverse(X),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 29
% 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 29
% clause depth limited to 4
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(61,40,0,128,0,0,151699,5,1501,151700,1,1501,151700,50,1501,151700,40,1501,151767,0,1501,160250,3,1839,161070,4,1952,162012,1,2102,162012,50,2102,162012,40,2102,162079,0,2102,163845,3,2420,163855,4,2561,163993,5,2703,163993,1,2703,163993,50,2703,163993,40,2703,164060,0,2703,187431,3,4205,188147,4,4954,188772,1,5704,188772,50,5704,188772,40,5704,188839,0,5704,207174,3,6458,207600,4,6830,208003,5,7205,208004,1,7205,208004,50,7205,208004,40,7205,208071,0,7205,220020,3,7979,221263,4,8331,222940,5,8706,222941,5,8706,222942,1,8706,222942,50,8706,222942,40,8706,223009,0,8706,279616,3,12607,280151,4,14557,280461,1,16507,280461,50,16509,280461,40,16509,280528,0,16509,324782,3,19060,325193,4,20336,325212,1,21610,325212,50,21611,325212,40,21611,325279,0,21611,358127,3,23112,359020,4,23862,359618,5,24612,359619,1,24612,359619,50,24613,359619,40,24613,359686,0,24613,373832,3,25364,375042,4,25739,375694,5,26114,375695,1,26114,375695,50,26114,375695,40,26114,375762,0,26114,401169,3,27315,401949,4,27915,402734,5,28515,402735,1,28515,402735,50,28516,402735,40,28516,402802,0,28516,422787,3,29274,423402,4,29642,424012,1,30017,424012,50,30017,424012,40,30017,424012,40,30017,424073,0,30018,424176,50,30018,424176,30,30018,424176,40,30018,424237,0,30018,424446,50,30018,424446,30,30018,424446,40,30018,424507,0,30023,424675,50,30023,424675,30,30023,424675,40,30023,424736,0,30023,424839,50,30023,424839,30,30023,424839,40,30023,424900,0,30028,425060,50,30029,425121,0,30029)
%
%
% START OF PROOF
% 424955 [?] ?
% 425065 [] -equal(multiply(X,sk_c9),sk_c10) | -equal(inverse(X),sk_c9).
% 425096 [] equal(multiply(sk_c4,sk_c9),sk_c10) | equal(inverse(sk_c1),sk_c9).
% 425097 [] equal(inverse(sk_c1),sk_c9) | equal(inverse(sk_c4),sk_c10).
% 425104 [?] ?
% 425105 [?] ?
% 425137 [hyper:425065,425097,binarycut:425105] equal(inverse(sk_c4),sk_c10).
% 425162 [hyper:425065,425096,binarycut:425104] equal(multiply(sk_c4,sk_c9),sk_c10).
% 425166 [hyper:425065,425162,demod:425137,cut:424955] 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 29
% clause depth limited to 4
% seconds given: 4
%
%
% Split component 6 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(inverse(sk_c10),sk_c9) | -equal(inverse(sk_c9),sk_c10) | -equal(multiply(X,sk_c9),sk_c10) | -equal(inverse(X),sk_c9) | -equal(multiply(sk_c10,Y),sk_c9) | -equal(multiply(Z,sk_c10),Y) | -equal(inverse(Z),sk_c10) | -equal(inverse(U),sk_c10) | -equal(multiply(U,sk_c9),sk_c10) | -equal(multiply(V,W),sk_c9) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c9) | -equal(multiply(sk_c10,X1),sk_c9) | -equal(multiply(X2,sk_c10),X1) | -equal(inverse(X2),sk_c10).
% Split part used next: -equal(inverse(sk_c10),sk_c9).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 29
% 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 29
% 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 29
% 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 29
% 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 29
% 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 29
% 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 29
% 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 29
% 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 29
% 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(61,40,0,128,0,0,151699,5,1501,151700,1,1501,151700,50,1501,151700,40,1501,151767,0,1501,160250,3,1839,161070,4,1952,162012,1,2102,162012,50,2102,162012,40,2102,162079,0,2102,163845,3,2420,163855,4,2561,163993,5,2703,163993,1,2703,163993,50,2703,163993,40,2703,164060,0,2703,187431,3,4205,188147,4,4954,188772,1,5704,188772,50,5704,188772,40,5704,188839,0,5704,207174,3,6458,207600,4,6830,208003,5,7205,208004,1,7205,208004,50,7205,208004,40,7205,208071,0,7205,220020,3,7979,221263,4,8331,222940,5,8706,222941,5,8706,222942,1,8706,222942,50,8706,222942,40,8706,223009,0,8706,279616,3,12607,280151,4,14557,280461,1,16507,280461,50,16509,280461,40,16509,280528,0,16509,324782,3,19060,325193,4,20336,325212,1,21610,325212,50,21611,325212,40,21611,325279,0,21611,358127,3,23112,359020,4,23862,359618,5,24612,359619,1,24612,359619,50,24613,359619,40,24613,359686,0,24613,373832,3,25364,375042,4,25739,375694,5,26114,375695,1,26114,375695,50,26114,375695,40,26114,375762,0,26114,401169,3,27315,401949,4,27915,402734,5,28515,402735,1,28515,402735,50,28516,402735,40,28516,402802,0,28516,422787,3,29274,423402,4,29642,424012,1,30017,424012,50,30017,424012,40,30017,424012,40,30017,424073,0,30018,424176,50,30018,424176,30,30018,424176,40,30018,424237,0,30018,424446,50,30018,424446,30,30018,424446,40,30018,424507,0,30023,424675,50,30023,424675,30,30023,424675,40,30023,424736,0,30023,424839,50,30023,424839,30,30023,424839,40,30023,424900,0,30028,425060,50,30029,425121,0,30029,425165,50,30029,425165,30,30029,425165,40,30029,425226,0,30033,425390,50,30034,425451,0,30034,425699,50,30037,425760,0,30042,426026,50,30046,426087,0,30046,426366,50,30051,426427,0,30057,426712,50,30065,426773,0,30065,427066,50,30080,427127,0,30085,427428,50,30113,427489,0,30113,427800,50,30173,427861,0,30174,428182,50,30288,428182,40,30288,428243,0,30288)
%
%
% START OF PROOF
% 427988 [?] ?
% 428184 [] equal(multiply(identity,X),X).
% 428185 [] equal(multiply(inverse(X),X),identity).
% 428186 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 428187 [] -equal(inverse(sk_c10),sk_c9).
% 428236 [?] ?
% 428237 [?] ?
% 428238 [?] ?
% 428239 [?] ?
% 428240 [?] ?
% 428241 [?] ?
% 428242 [?] ?
% 428243 [?] ?
% 428275 [input:428236,cut:428187] equal(inverse(sk_c7),sk_c10).
% 428276 [para:428275.1.1,428185.1.1.1] equal(multiply(sk_c10,sk_c7),identity).
% 428279 [input:428240,cut:428187] equal(inverse(sk_c5),sk_c6).
% 428280 [para:428279.1.1,428185.1.1.1] equal(multiply(sk_c6,sk_c5),identity).
% 428281 [input:428243,cut:428187] equal(inverse(sk_c4),sk_c10).
% 428282 [para:428281.1.1,428185.1.1.1] equal(multiply(sk_c10,sk_c4),identity).
% 428321 [input:428237,cut:428187] equal(multiply(sk_c7,sk_c10),sk_c8).
% 428322 [input:428238,cut:428187] equal(multiply(sk_c10,sk_c8),sk_c9).
% 428323 [input:428239,cut:428187] equal(multiply(sk_c6,sk_c10),sk_c9).
% 428324 [input:428241,cut:428187] equal(multiply(sk_c5,sk_c6),sk_c9).
% 428325 [input:428242,cut:428187] equal(multiply(sk_c4,sk_c9),sk_c10).
% 428347 [para:428185.1.1,428186.1.1.1,demod:428184] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 428350 [para:428276.1.1,428186.1.1.1,demod:428184] equal(X,multiply(sk_c10,multiply(sk_c7,X))).
% 428352 [para:428280.1.1,428186.1.1.1,demod:428184] equal(X,multiply(sk_c6,multiply(sk_c5,X))).
% 428353 [para:428282.1.1,428186.1.1.1,demod:428184] equal(X,multiply(sk_c10,multiply(sk_c4,X))).
% 428386 [para:428322.1.1,428186.1.1.1] equal(multiply(sk_c9,X),multiply(sk_c10,multiply(sk_c8,X))).
% 428415 [para:428321.1.1,428350.1.2.2] equal(sk_c10,multiply(sk_c10,sk_c8)).
% 428420 [para:428415.1.2,428322.1.1] equal(sk_c10,sk_c9).
% 428421 [para:428415.1.2,428186.1.1.1,demod:428386] equal(multiply(sk_c10,X),multiply(sk_c9,X)).
% 428449 [para:428420.1.1,428323.1.1.2] equal(multiply(sk_c6,sk_c9),sk_c9).
% 428474 [para:428324.1.1,428352.1.2.2,demod:428449] equal(sk_c6,sk_c9).
% 428475 [para:428474.1.2,428187.1.2] -equal(inverse(sk_c10),sk_c6).
% 428494 [para:428325.1.1,428353.1.2.2,demod:428421] equal(sk_c9,multiply(sk_c9,sk_c10)).
% 428520 [para:428494.1.2,428347.1.2.2,demod:428185] equal(sk_c10,identity).
% 428553 [para:428520.1.1,428475.1.1.1,cut:427988] 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(inverse(sk_c10),sk_c9) | -equal(inverse(sk_c9),sk_c10) | -equal(multiply(X,sk_c9),sk_c10) | -equal(inverse(X),sk_c9) | -equal(multiply(sk_c10,Y),sk_c9) | -equal(multiply(Z,sk_c10),Y) | -equal(inverse(Z),sk_c10) | -equal(inverse(U),sk_c10) | -equal(multiply(U,sk_c9),sk_c10) | -equal(multiply(V,W),sk_c9) | -equal(inverse(V),W) | -equal(multiply(W,sk_c10),sk_c9) | -equal(multiply(sk_c10,X1),sk_c9) | -equal(multiply(X2,sk_c10),X1) | -equal(inverse(X2),sk_c10).
% Split part used next: -equal(inverse(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 29
% 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 29
% 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 29
% 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 29
% 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 29
% 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 29
% 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 29
% 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 29
% 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 29
% 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(61,40,0,128,0,0,151699,5,1501,151700,1,1501,151700,50,1501,151700,40,1501,151767,0,1501,160250,3,1839,161070,4,1952,162012,1,2102,162012,50,2102,162012,40,2102,162079,0,2102,163845,3,2420,163855,4,2561,163993,5,2703,163993,1,2703,163993,50,2703,163993,40,2703,164060,0,2703,187431,3,4205,188147,4,4954,188772,1,5704,188772,50,5704,188772,40,5704,188839,0,5704,207174,3,6458,207600,4,6830,208003,5,7205,208004,1,7205,208004,50,7205,208004,40,7205,208071,0,7205,220020,3,7979,221263,4,8331,222940,5,8706,222941,5,8706,222942,1,8706,222942,50,8706,222942,40,8706,223009,0,8706,279616,3,12607,280151,4,14557,280461,1,16507,280461,50,16509,280461,40,16509,280528,0,16509,324782,3,19060,325193,4,20336,325212,1,21610,325212,50,21611,325212,40,21611,325279,0,21611,358127,3,23112,359020,4,23862,359618,5,24612,359619,1,24612,359619,50,24613,359619,40,24613,359686,0,24613,373832,3,25364,375042,4,25739,375694,5,26114,375695,1,26114,375695,50,26114,375695,40,26114,375762,0,26114,401169,3,27315,401949,4,27915,402734,5,28515,402735,1,28515,402735,50,28516,402735,40,28516,402802,0,28516,422787,3,29274,423402,4,29642,424012,1,30017,424012,50,30017,424012,40,30017,424012,40,30017,424073,0,30018,424176,50,30018,424176,30,30018,424176,40,30018,424237,0,30018,424446,50,30018,424446,30,30018,424446,40,30018,424507,0,30023,424675,50,30023,424675,30,30023,424675,40,30023,424736,0,30023,424839,50,30023,424839,30,30023,424839,40,30023,424900,0,30028,425060,50,30029,425121,0,30029,425165,50,30029,425165,30,30029,425165,40,30029,425226,0,30033,425390,50,30034,425451,0,30034,425699,50,30037,425760,0,30042,426026,50,30046,426087,0,30046,426366,50,30051,426427,0,30057,426712,50,30065,426773,0,30065,427066,50,30080,427127,0,30085,427428,50,30113,427489,0,30113,427800,50,30173,427861,0,30174,428182,50,30288,428182,40,30288,428243,0,30288,428552,50,30289,428552,30,30289,428552,40,30289,428613,0,30289,428777,50,30290,428838,0,30294,429086,50,30297,429147,0,30297,429413,50,30300,429474,0,30305,429753,50,30310,429814,0,30310,430099,50,30319,430160,0,30324,430453,50,30339,430514,0,30340,430815,50,30368,430876,0,30372,431187,50,30429,431248,0,30429,431569,50,30544,431569,40,30544,431630,0,30544)
%
%
% START OF PROOF
% 431471 [?] ?
% 431571 [] equal(multiply(identity,X),X).
% 431572 [] equal(multiply(inverse(X),X),identity).
% 431573 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 431574 [] -equal(inverse(sk_c9),sk_c10).
% 431615 [?] ?
% 431616 [?] ?
% 431617 [?] ?
% 431618 [?] ?
% 431619 [?] ?
% 431620 [?] ?
% 431653 [input:431615,cut:431574] equal(inverse(sk_c7),sk_c10).
% 431654 [para:431653.1.1,431572.1.1.1] equal(multiply(sk_c10,sk_c7),identity).
% 431655 [input:431619,cut:431574] equal(inverse(sk_c5),sk_c6).
% 431656 [para:431655.1.1,431572.1.1.1] equal(multiply(sk_c6,sk_c5),identity).
% 431694 [input:431616,cut:431574] equal(multiply(sk_c7,sk_c10),sk_c8).
% 431695 [input:431617,cut:431574] equal(multiply(sk_c10,sk_c8),sk_c9).
% 431696 [input:431618,cut:431574] equal(multiply(sk_c6,sk_c10),sk_c9).
% 431697 [input:431620,cut:431574] equal(multiply(sk_c5,sk_c6),sk_c9).
% 431733 [para:431654.1.1,431573.1.1.1,demod:431571] equal(X,multiply(sk_c10,multiply(sk_c7,X))).
% 431734 [para:431656.1.1,431573.1.1.1,demod:431571] equal(X,multiply(sk_c6,multiply(sk_c5,X))).
% 431790 [para:431694.1.1,431733.1.2.2] equal(sk_c10,multiply(sk_c10,sk_c8)).
% 431794 [para:431790.1.2,431695.1.1] equal(sk_c10,sk_c9).
% 431816 [para:431794.1.1,431696.1.1.2] equal(multiply(sk_c6,sk_c9),sk_c9).
% 431829 [para:431697.1.1,431734.1.2.2,demod:431816] equal(sk_c6,sk_c9).
% 431830 [para:431829.1.2,431574.1.1.1,cut:431471] 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: 27491
% derived clauses: 2656432
% kept clauses: 238815
% kept size sum: 734088
% kept mid-nuclei: 95968
% kept new demods: 3975
% forw unit-subs: 780299
% forw double-subs: 1202218
% forw overdouble-subs: 230930
% backward subs: 15124
% fast unit cutoff: 22938
% full unit cutoff: 0
% dbl unit cutoff: 62702
% real runtime : 308.7
% process. runtime: 305.44
% specific non-discr-tree subsumption statistics:
% tried: 100879746
% length fails: 9026163
% strength fails: 44973204
% predlist fails: 1971706
% aux str. fails: 3406867
% by-lit fails: 21535113
% full subs tried: 2462543
% full subs fail: 2283682
%
% ; 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/GRP240-1+eq_r.in")
%
%------------------------------------------------------------------------------