%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP332-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 : art03.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.5s
% Output : Assurance 298.5s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----NO SOLUTION OUTPUT BY SYSTEM
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
%
% Gandalf c-2.6 r1 starting to prove: /home/graph/tptp/TSTP/PreparedTPTP/otter:hypothesis:set(auto),clear(print_given)---add_equality:r/GRP/GRP332-1+eq_r.in
% Using automatic strategy selection.
% Time limit in seconds: 600
%
% prove-all-passes started
%
% detected problem class: peq
%
% strategies selected:
% (hyper 30 #f 3 21)
% (binary-unit 12 #f)
% (binary-unit-uniteq 12 #f)
% (binary-posweight-kb-big-order 60 #f 3 21)
% (binary-posweight-lex-big-order 30 #f 3 21)
% (binary 30 #t)
% (binary-posweight-kb-big-order 156 #f)
% (binary-posweight-lex-big-order 102 #f)
% (binary-posweight-firstpref-order 60 #f)
% (binary-order 30 #f)
% (binary-posweight-kb-small-order 48 #f)
% (binary-posweight-lex-small-order 30 #f)
%
%
% SOS clause
% -equal(multiply(sk_c7,sk_c8),sk_c6) | -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7) | -equal(inverse(Y),sk_c7) | -equal(multiply(Y,sk_c6),sk_c7) | -equal(multiply(sk_c8,sk_c7),sk_c6) | -equal(multiply(Z,sk_c8),sk_c7) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c8,U),sk_c7) | -equal(multiply(V,sk_c8),U) | -equal(inverse(V),sk_c8).
% was split for some strategies as:
% -equal(multiply(sk_c8,U),sk_c7) | -equal(multiply(V,sk_c8),U) | -equal(inverse(V),sk_c8).
% -equal(multiply(Z,sk_c8),sk_c7) | -equal(inverse(Z),sk_c8).
% -equal(inverse(Y),sk_c7) | -equal(multiply(Y,sk_c6),sk_c7).
% -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7).
% -equal(multiply(sk_c7,sk_c8),sk_c6).
% -equal(multiply(sk_c8,sk_c7),sk_c6).
%
% Starting a split proof attempt with 6 components.
%
% Split component 1 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c8),sk_c6) | -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7) | -equal(inverse(Y),sk_c7) | -equal(multiply(Y,sk_c6),sk_c7) | -equal(multiply(sk_c8,sk_c7),sk_c6) | -equal(multiply(Z,sk_c8),sk_c7) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c8,U),sk_c7) | -equal(multiply(V,sk_c8),U) | -equal(inverse(V),sk_c8).
% Split part used next: -equal(multiply(sk_c8,U),sk_c7) | -equal(multiply(V,sk_c8),U) | -equal(inverse(V),sk_c8).
% END OF PROOFPART
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,1,75,0,1,706,50,6,746,0,6,1731,50,19,1771,0,20,2937,50,37,2977,0,37,4237,50,52,4277,0,52,5632,50,72,5672,0,72,7167,50,101,7207,0,101,8842,50,147,8882,0,147,10703,50,229,10743,0,229,12750,50,383,12790,0,383,15029,50,622,15069,0,622,17540,50,1041,17540,40,1041,17580,0,1041,28290,3,1344,28975,4,1492,29669,1,1642,29669,50,1642,29669,40,1642,29709,0,1642,29996,3,1953,30005,4,2096,30018,5,2243,30018,1,2244,30018,50,2244,30018,40,2244,30058,0,2244,52294,3,3746,53206,4,4495,53871,5,5245,53872,1,5245,53872,50,5246,53872,40,5246,53912,0,5246,71380,3,5998,71869,4,6372,72459,1,6747,72459,50,6747,72459,40,6747,72499,0,6747,83531,3,7498,84499,4,7873,85929,5,8248,85930,5,8248,85931,1,8248,85931,50,8248,85931,40,8248,85971,0,8248,125927,3,12149,127846,4,14099,129344,5,16049,129345,1,16049,129345,50,16051,129345,40,16051,129385,0,16051,164157,3,18602,165533,4,19877,166544,5,21152,166545,1,21152,166545,50,21153,166545,40,21153,166585,0,21153,198860,3,22654,199563,4,23404,200451,5,24154,200452,1,24154,200452,50,24156,200452,40,24156,200492,0,24156,210035,3,24918,211163,4,25282,211512,5,25657,211513,1,25657,211513,50,25657,211513,40,25657,211553,0,25657,235871,3,26858,236780,4,27458,237513,1,28058,237513,50,28059,237513,40,28059,237553,0,28059,254586,3,28810,255240,4,29185,255695,5,29560,255696,1,29560,255696,50,29560,255696,40,29560,255696,40,29560,255731,0,29560)
%
%
% START OF PROOF
% 255698 [] equal(multiply(identity,X),X).
% 255699 [] equal(multiply(inverse(X),X),identity).
% 255700 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 255701 [] -equal(multiply(sk_c8,X),sk_c7) | -equal(multiply(Y,sk_c8),X) | -equal(inverse(Y),sk_c8).
% 255702 [] equal(multiply(sk_c2,sk_c6),sk_c7) | equal(inverse(sk_c4),sk_c8).
% 255703 [] equal(multiply(sk_c2,sk_c6),sk_c7) | equal(multiply(sk_c4,sk_c8),sk_c5).
% 255704 [] equal(multiply(sk_c2,sk_c6),sk_c7) | equal(multiply(sk_c8,sk_c5),sk_c7).
% 255708 [] equal(inverse(sk_c2),sk_c7) | equal(inverse(sk_c4),sk_c8).
% 255709 [] equal(multiply(sk_c4,sk_c8),sk_c5) | equal(inverse(sk_c2),sk_c7).
% 255710 [?] ?
% 255714 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c4),sk_c8).
% 255715 [] equal(multiply(sk_c4,sk_c8),sk_c5) | equal(inverse(sk_c1),sk_c7).
% 255716 [?] ?
% 255720 [] equal(multiply(sk_c1,sk_c7),sk_c8) | equal(inverse(sk_c4),sk_c8).
% 255721 [] equal(multiply(sk_c1,sk_c7),sk_c8) | equal(multiply(sk_c4,sk_c8),sk_c5).
% 255722 [] equal(multiply(sk_c1,sk_c7),sk_c8) | equal(multiply(sk_c8,sk_c5),sk_c7).
% 255726 [] equal(multiply(sk_c7,sk_c8),sk_c6) | equal(inverse(sk_c4),sk_c8).
% 255727 [] equal(multiply(sk_c7,sk_c8),sk_c6) | equal(multiply(sk_c4,sk_c8),sk_c5).
% 255728 [] equal(multiply(sk_c7,sk_c8),sk_c6) | equal(multiply(sk_c8,sk_c5),sk_c7).
% 255765 [hyper:255701,255709,255708,binarycut:255710] equal(inverse(sk_c2),sk_c7).
% 255769 [para:255765.1.1,255699.1.1.1] equal(multiply(sk_c7,sk_c2),identity).
% 255773 [hyper:255701,255715,255714,binarycut:255716] equal(inverse(sk_c1),sk_c7).
% 255774 [para:255773.1.1,255699.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 255779 [hyper:255701,255704,255703,255702] equal(multiply(sk_c2,sk_c6),sk_c7).
% 255813 [hyper:255701,255722,255721,255720] equal(multiply(sk_c1,sk_c7),sk_c8).
% 255824 [hyper:255701,255728,255727,255726] equal(multiply(sk_c7,sk_c8),sk_c6).
% 255828 [para:255699.1.1,255700.1.1.1,demod:255698] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 255829 [para:255769.1.1,255700.1.1.1,demod:255698] equal(X,multiply(sk_c7,multiply(sk_c2,X))).
% 255830 [para:255774.1.1,255700.1.1.1,demod:255698] equal(X,multiply(sk_c7,multiply(sk_c1,X))).
% 255831 [para:255779.1.1,255700.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c2,multiply(sk_c6,X))).
% 255836 [para:255779.1.1,255829.1.2.2] equal(sk_c6,multiply(sk_c7,sk_c7)).
% 255840 [para:255813.1.1,255830.1.2.2,demod:255824] equal(sk_c7,sk_c6).
% 255844 [para:255840.1.1,255824.1.1.1] equal(multiply(sk_c6,sk_c8),sk_c6).
% 255854 [para:255824.1.1,255828.1.2.2] equal(sk_c8,multiply(inverse(sk_c7),sk_c6)).
% 255856 [para:255836.1.2,255828.1.2.2,demod:255854] equal(sk_c7,sk_c8).
% 255862 [para:255856.1.1,255813.1.1.2] equal(multiply(sk_c1,sk_c8),sk_c8).
% 255863 [para:255856.1.1,255824.1.1.1] equal(multiply(sk_c8,sk_c8),sk_c6).
% 255878 [para:255844.1.1,255831.1.2.2,demod:255779,255824] equal(sk_c6,sk_c7).
% 255907 [hyper:255701,255862,demod:255773,255863,cut:255878,cut:255856] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% Split component 2 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c8),sk_c6) | -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7) | -equal(inverse(Y),sk_c7) | -equal(multiply(Y,sk_c6),sk_c7) | -equal(multiply(sk_c8,sk_c7),sk_c6) | -equal(multiply(Z,sk_c8),sk_c7) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c8,U),sk_c7) | -equal(multiply(V,sk_c8),U) | -equal(inverse(V),sk_c8).
% Split part used next: -equal(multiply(Z,sk_c8),sk_c7) | -equal(inverse(Z),sk_c8).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 4
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,1,75,0,1,706,50,6,746,0,6,1731,50,19,1771,0,20,2937,50,37,2977,0,37,4237,50,52,4277,0,52,5632,50,72,5672,0,72,7167,50,101,7207,0,101,8842,50,147,8882,0,147,10703,50,229,10743,0,229,12750,50,383,12790,0,383,15029,50,622,15069,0,622,17540,50,1041,17540,40,1041,17580,0,1041,28290,3,1344,28975,4,1492,29669,1,1642,29669,50,1642,29669,40,1642,29709,0,1642,29996,3,1953,30005,4,2096,30018,5,2243,30018,1,2244,30018,50,2244,30018,40,2244,30058,0,2244,52294,3,3746,53206,4,4495,53871,5,5245,53872,1,5245,53872,50,5246,53872,40,5246,53912,0,5246,71380,3,5998,71869,4,6372,72459,1,6747,72459,50,6747,72459,40,6747,72499,0,6747,83531,3,7498,84499,4,7873,85929,5,8248,85930,5,8248,85931,1,8248,85931,50,8248,85931,40,8248,85971,0,8248,125927,3,12149,127846,4,14099,129344,5,16049,129345,1,16049,129345,50,16051,129345,40,16051,129385,0,16051,164157,3,18602,165533,4,19877,166544,5,21152,166545,1,21152,166545,50,21153,166545,40,21153,166585,0,21153,198860,3,22654,199563,4,23404,200451,5,24154,200452,1,24154,200452,50,24156,200452,40,24156,200492,0,24156,210035,3,24918,211163,4,25282,211512,5,25657,211513,1,25657,211513,50,25657,211513,40,25657,211553,0,25657,235871,3,26858,236780,4,27458,237513,1,28058,237513,50,28059,237513,40,28059,237553,0,28059,254586,3,28810,255240,4,29185,255695,5,29560,255696,1,29560,255696,50,29560,255696,40,29560,255696,40,29560,255731,0,29560,255906,50,29561,255906,30,29561,255906,40,29561,255941,0,29561,256054,50,29562,256089,0,29567)
%
%
% START OF PROOF
% 256056 [] equal(multiply(identity,X),X).
% 256057 [] equal(multiply(inverse(X),X),identity).
% 256058 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 256059 [] -equal(multiply(X,sk_c8),sk_c7) | -equal(inverse(X),sk_c8).
% 256063 [] equal(multiply(sk_c2,sk_c6),sk_c7) | equal(inverse(sk_c3),sk_c8).
% 256064 [] equal(multiply(sk_c2,sk_c6),sk_c7) | equal(multiply(sk_c3,sk_c8),sk_c7).
% 256069 [] equal(inverse(sk_c2),sk_c7) | equal(inverse(sk_c3),sk_c8).
% 256070 [?] ?
% 256075 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c3),sk_c8).
% 256076 [?] ?
% 256081 [] equal(multiply(sk_c1,sk_c7),sk_c8) | equal(inverse(sk_c3),sk_c8).
% 256082 [] equal(multiply(sk_c1,sk_c7),sk_c8) | equal(multiply(sk_c3,sk_c8),sk_c7).
% 256087 [] equal(multiply(sk_c7,sk_c8),sk_c6) | equal(inverse(sk_c3),sk_c8).
% 256088 [] equal(multiply(sk_c7,sk_c8),sk_c6) | equal(multiply(sk_c3,sk_c8),sk_c7).
% 256094 [hyper:256059,256069,binarycut:256070] equal(inverse(sk_c2),sk_c7).
% 256096 [para:256094.1.1,256057.1.1.1] equal(multiply(sk_c7,sk_c2),identity).
% 256102 [hyper:256059,256075,binarycut:256076] equal(inverse(sk_c1),sk_c7).
% 256103 [para:256102.1.1,256057.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 256126 [hyper:256059,256064,256063] equal(multiply(sk_c2,sk_c6),sk_c7).
% 256131 [hyper:256059,256082,256081] equal(multiply(sk_c1,sk_c7),sk_c8).
% 256136 [hyper:256059,256088,256087] equal(multiply(sk_c7,sk_c8),sk_c6).
% 256137 [para:256057.1.1,256058.1.1.1,demod:256056] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 256138 [para:256096.1.1,256058.1.1.1,demod:256056] equal(X,multiply(sk_c7,multiply(sk_c2,X))).
% 256139 [para:256103.1.1,256058.1.1.1,demod:256056] equal(X,multiply(sk_c7,multiply(sk_c1,X))).
% 256140 [para:256126.1.1,256058.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c2,multiply(sk_c6,X))).
% 256141 [para:256131.1.1,256058.1.1.1] equal(multiply(sk_c8,X),multiply(sk_c1,multiply(sk_c7,X))).
% 256143 [para:256126.1.1,256138.1.2.2] equal(sk_c6,multiply(sk_c7,sk_c7)).
% 256145 [para:256131.1.1,256139.1.2.2,demod:256136] equal(sk_c7,sk_c6).
% 256146 [para:256145.1.1,256096.1.1.1] equal(multiply(sk_c6,sk_c2),identity).
% 256148 [para:256145.1.1,256131.1.1.2] equal(multiply(sk_c1,sk_c6),sk_c8).
% 256149 [para:256145.1.1,256136.1.1.1] equal(multiply(sk_c6,sk_c8),sk_c6).
% 256155 [para:256057.1.1,256137.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 256156 [para:256096.1.1,256137.1.2.2] equal(sk_c2,multiply(inverse(sk_c7),identity)).
% 256157 [para:256103.1.1,256137.1.2.2,demod:256156] equal(sk_c1,sk_c2).
% 256158 [para:256136.1.1,256137.1.2.2] equal(sk_c8,multiply(inverse(sk_c7),sk_c6)).
% 256159 [para:256058.1.1,256137.1.2.2] equal(X,multiply(inverse(multiply(Y,Z)),multiply(Y,multiply(Z,X)))).
% 256160 [para:256138.1.2,256137.1.2.2] equal(multiply(sk_c2,X),multiply(inverse(sk_c7),X)).
% 256161 [para:256143.1.2,256137.1.2.2,demod:256158] equal(sk_c7,sk_c8).
% 256162 [para:256139.1.2,256137.1.2.2,demod:256160] equal(multiply(sk_c1,X),multiply(sk_c2,X)).
% 256164 [para:256137.1.2,256137.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 256168 [para:256161.1.1,256131.1.1.2] equal(multiply(sk_c1,sk_c8),sk_c8).
% 256170 [para:256161.1.1,256138.1.2.1,demod:256162] equal(X,multiply(sk_c8,multiply(sk_c1,X))).
% 256172 [para:256161.1.1,256145.1.1] equal(sk_c8,sk_c6).
% 256174 [?] ?
% 256175 [para:256157.1.2,256140.1.2.1] equal(multiply(sk_c7,X),multiply(sk_c1,multiply(sk_c6,X))).
% 256176 [para:256148.1.1,256058.1.1.1,demod:256175] equal(multiply(sk_c8,X),multiply(sk_c7,X)).
% 256178 [para:256149.1.1,256137.1.2.2,demod:256057] equal(sk_c8,identity).
% 256181 [para:256178.1.1,256136.1.1.2,demod:256176] equal(multiply(sk_c8,identity),sk_c6).
% 256182 [para:256178.1.1,256172.1.1] equal(identity,sk_c6).
% 256186 [para:256138.1.2,256141.1.2.2,demod:256170,256162] equal(X,multiply(sk_c1,X)).
% 256189 [para:256182.1.2,256126.1.1.2,demod:256174,256162] equal(identity,sk_c7).
% 256190 [para:256182.1.2,256146.1.1.1,demod:256056] equal(sk_c2,identity).
% 256193 [para:256190.1.1,256094.1.1.1] equal(inverse(identity),sk_c7).
% 256199 [para:256189.1.2,256156.1.2.1.1,demod:256181,256176,256193] equal(sk_c2,sk_c6).
% 256204 [para:256182.1.2,256158.1.2.2,demod:256156] equal(sk_c8,sk_c2).
% 256205 [para:256204.1.1,256168.1.1.2,demod:256186] equal(sk_c2,sk_c8).
% 256208 [para:256096.1.1,256159.1.2.2.2] equal(sk_c2,multiply(inverse(multiply(X,sk_c7)),multiply(X,identity))).
% 256209 [para:256126.1.1,256159.1.2.2.2] equal(sk_c6,multiply(inverse(multiply(X,sk_c2)),multiply(X,sk_c7))).
% 256212 [para:256138.1.2,256159.1.2.2.2,demod:256186,256162] equal(X,multiply(inverse(multiply(Y,sk_c7)),multiply(Y,X))).
% 256220 [para:256164.1.2,256057.1.1] equal(multiply(X,inverse(X)),identity).
% 256222 [para:256164.1.2,256155.1.2] equal(X,multiply(X,identity)).
% 256224 [para:256222.1.2,256156.1.2] equal(sk_c2,inverse(sk_c7)).
% 256225 [para:256222.1.2,256155.1.2] equal(X,inverse(inverse(X))).
% 256232 [para:256220.1.1,256212.1.2.2,demod:256222] equal(inverse(X),inverse(multiply(X,sk_c7))).
% 256242 [para:256208.1.2,256137.1.2.2,demod:256225,256232,256222] equal(X,multiply(X,sk_c2)).
% 256244 [para:256199.1.1,256242.1.2.2] equal(X,multiply(X,sk_c6)).
% 256246 [para:256209.1.2,256137.1.2.2,demod:256244,256225,256242] equal(multiply(X,sk_c7),X).
% 256247 [para:256161.1.1,256246.1.1.2] equal(multiply(X,sk_c8),X).
% 256248 [hyper:256059,256247,demod:256224,cut:256205] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 4
% seconds given: 4
%
%
% Split component 3 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c8),sk_c6) | -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7) | -equal(inverse(Y),sk_c7) | -equal(multiply(Y,sk_c6),sk_c7) | -equal(multiply(sk_c8,sk_c7),sk_c6) | -equal(multiply(Z,sk_c8),sk_c7) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c8,U),sk_c7) | -equal(multiply(V,sk_c8),U) | -equal(inverse(V),sk_c8).
% Split part used next: -equal(inverse(Y),sk_c7) | -equal(multiply(Y,sk_c6),sk_c7).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 4
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,1,75,0,1,706,50,6,746,0,6,1731,50,19,1771,0,20,2937,50,37,2977,0,37,4237,50,52,4277,0,52,5632,50,72,5672,0,72,7167,50,101,7207,0,101,8842,50,147,8882,0,147,10703,50,229,10743,0,229,12750,50,383,12790,0,383,15029,50,622,15069,0,622,17540,50,1041,17540,40,1041,17580,0,1041,28290,3,1344,28975,4,1492,29669,1,1642,29669,50,1642,29669,40,1642,29709,0,1642,29996,3,1953,30005,4,2096,30018,5,2243,30018,1,2244,30018,50,2244,30018,40,2244,30058,0,2244,52294,3,3746,53206,4,4495,53871,5,5245,53872,1,5245,53872,50,5246,53872,40,5246,53912,0,5246,71380,3,5998,71869,4,6372,72459,1,6747,72459,50,6747,72459,40,6747,72499,0,6747,83531,3,7498,84499,4,7873,85929,5,8248,85930,5,8248,85931,1,8248,85931,50,8248,85931,40,8248,85971,0,8248,125927,3,12149,127846,4,14099,129344,5,16049,129345,1,16049,129345,50,16051,129345,40,16051,129385,0,16051,164157,3,18602,165533,4,19877,166544,5,21152,166545,1,21152,166545,50,21153,166545,40,21153,166585,0,21153,198860,3,22654,199563,4,23404,200451,5,24154,200452,1,24154,200452,50,24156,200452,40,24156,200492,0,24156,210035,3,24918,211163,4,25282,211512,5,25657,211513,1,25657,211513,50,25657,211513,40,25657,211553,0,25657,235871,3,26858,236780,4,27458,237513,1,28058,237513,50,28059,237513,40,28059,237553,0,28059,254586,3,28810,255240,4,29185,255695,5,29560,255696,1,29560,255696,50,29560,255696,40,29560,255696,40,29560,255731,0,29560,255906,50,29561,255906,30,29561,255906,40,29561,255941,0,29561,256054,50,29562,256089,0,29567,256247,50,29568,256247,30,29568,256247,40,29568,256282,0,29568,256389,50,29569,256424,0,29569)
%
%
% START OF PROOF
% 256391 [] equal(multiply(identity,X),X).
% 256392 [] equal(multiply(inverse(X),X),identity).
% 256393 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 256394 [] -equal(multiply(X,sk_c6),sk_c7) | -equal(inverse(X),sk_c7).
% 256395 [?] ?
% 256396 [] equal(multiply(sk_c2,sk_c6),sk_c7) | equal(multiply(sk_c4,sk_c8),sk_c5).
% 256397 [?] ?
% 256398 [?] ?
% 256399 [] equal(multiply(sk_c2,sk_c6),sk_c7) | equal(multiply(sk_c3,sk_c8),sk_c7).
% 256400 [?] ?
% 256401 [] equal(inverse(sk_c2),sk_c7) | equal(inverse(sk_c4),sk_c8).
% 256402 [] equal(multiply(sk_c4,sk_c8),sk_c5) | equal(inverse(sk_c2),sk_c7).
% 256403 [] equal(multiply(sk_c8,sk_c5),sk_c7) | equal(inverse(sk_c2),sk_c7).
% 256404 [] equal(inverse(sk_c2),sk_c7) | equal(inverse(sk_c3),sk_c8).
% 256405 [] equal(multiply(sk_c3,sk_c8),sk_c7) | equal(inverse(sk_c2),sk_c7).
% 256406 [] equal(multiply(sk_c8,sk_c7),sk_c6) | equal(inverse(sk_c2),sk_c7).
% 256427 [hyper:256394,256401,binarycut:256395] equal(inverse(sk_c4),sk_c8).
% 256428 [para:256427.1.1,256392.1.1.1] equal(multiply(sk_c8,sk_c4),identity).
% 256432 [hyper:256394,256404,binarycut:256398] equal(inverse(sk_c3),sk_c8).
% 256433 [para:256432.1.1,256392.1.1.1] equal(multiply(sk_c8,sk_c3),identity).
% 256439 [hyper:256394,256402,binarycut:256396] equal(multiply(sk_c4,sk_c8),sk_c5).
% 256442 [hyper:256394,256403,binarycut:256397] equal(multiply(sk_c8,sk_c5),sk_c7).
% 256448 [hyper:256394,256405,binarycut:256399] equal(multiply(sk_c3,sk_c8),sk_c7).
% 256451 [hyper:256394,256406,binarycut:256400] equal(multiply(sk_c8,sk_c7),sk_c6).
% 256452 [para:256392.1.1,256393.1.1.1,demod:256391] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 256453 [para:256428.1.1,256393.1.1.1,demod:256391] equal(X,multiply(sk_c8,multiply(sk_c4,X))).
% 256454 [para:256433.1.1,256393.1.1.1,demod:256391] equal(X,multiply(sk_c8,multiply(sk_c3,X))).
% 256455 [para:256439.1.1,256393.1.1.1] equal(multiply(sk_c5,X),multiply(sk_c4,multiply(sk_c8,X))).
% 256456 [para:256442.1.1,256393.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c8,multiply(sk_c5,X))).
% 256457 [para:256448.1.1,256393.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c3,multiply(sk_c8,X))).
% 256459 [para:256439.1.1,256453.1.2.2,demod:256442] equal(sk_c8,sk_c7).
% 256462 [para:256448.1.1,256454.1.2.2,demod:256451] equal(sk_c8,sk_c6).
% 256464 [para:256392.1.1,256452.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 256465 [para:256428.1.1,256452.1.2.2] equal(sk_c4,multiply(inverse(sk_c8),identity)).
% 256466 [para:256433.1.1,256452.1.2.2,demod:256465] equal(sk_c3,sk_c4).
% 256468 [para:256393.1.1,256452.1.2.2] equal(X,multiply(inverse(multiply(Y,Z)),multiply(Y,multiply(Z,X)))).
% 256470 [para:256453.1.2,256452.1.2.2] equal(multiply(sk_c4,X),multiply(inverse(sk_c8),X)).
% 256471 [para:256454.1.2,256452.1.2.2,demod:256470] equal(multiply(sk_c3,X),multiply(sk_c4,X)).
% 256472 [para:256452.1.2,256452.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 256475 [para:256462.1.1,256439.1.1.2,demod:256471] equal(multiply(sk_c3,sk_c6),sk_c5).
% 256477 [para:256462.1.1,256448.1.1.2,demod:256475] equal(sk_c5,sk_c7).
% 256484 [para:256477.1.2,256459.1.2] equal(sk_c8,sk_c5).
% 256492 [para:256455.1.2,256453.1.2.2,demod:256456] equal(multiply(sk_c8,X),multiply(sk_c7,X)).
% 256493 [para:256453.1.2,256455.1.2.2,demod:256471] equal(multiply(sk_c5,multiply(sk_c3,X)),multiply(sk_c3,X)).
% 256496 [para:256466.1.2,256455.1.2.1,demod:256492,256457] equal(multiply(sk_c5,X),multiply(sk_c8,X)).
% 256500 [para:256484.1.1,256453.1.2.1,demod:256493,256471] equal(X,multiply(sk_c3,X)).
% 256501 [para:256484.1.1,256454.1.2.1,demod:256500] equal(X,multiply(sk_c5,X)).
% 256505 [para:256501.1.2,256452.1.2.2] equal(X,multiply(inverse(sk_c5),X)).
% 256512 [para:256505.1.2,256392.1.1] equal(sk_c5,identity).
% 256513 [para:256512.1.1,256442.1.1.2,demod:256501,256496] equal(identity,sk_c7).
% 256531 [para:256442.1.1,256468.1.2.1.1,demod:256496,256501] equal(X,multiply(inverse(sk_c7),X)).
% 256567 [para:256472.1.2,256392.1.1] equal(multiply(X,inverse(X)),identity).
% 256569 [para:256472.1.2,256464.1.2] equal(X,multiply(X,identity)).
% 256570 [para:256569.1.2,256464.1.2] equal(X,inverse(inverse(X))).
% 256572 [para:256569.1.2,256531.1.2] equal(identity,inverse(sk_c7)).
% 256575 [para:256567.1.1,256468.1.2.2.2,demod:256569] equal(inverse(X),multiply(inverse(multiply(Y,X)),Y)).
% 256579 [para:256453.1.2,256575.1.2.1.1,demod:256500,256471] equal(inverse(X),multiply(inverse(X),sk_c8)).
% 256589 [para:256579.1.2,256472.1.2,demod:256570] equal(multiply(X,sk_c8),X).
% 256592 [para:256462.1.1,256589.1.1.2] equal(multiply(X,sk_c6),X).
% 256598 [hyper:256394,256592,demod:256572,cut:256513] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 4
% seconds given: 4
%
%
% Split component 4 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c8),sk_c6) | -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7) | -equal(inverse(Y),sk_c7) | -equal(multiply(Y,sk_c6),sk_c7) | -equal(multiply(sk_c8,sk_c7),sk_c6) | -equal(multiply(Z,sk_c8),sk_c7) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c8,U),sk_c7) | -equal(multiply(V,sk_c8),U) | -equal(inverse(V),sk_c8).
% Split part used next: -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 4
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,1,75,0,1,706,50,6,746,0,6,1731,50,19,1771,0,20,2937,50,37,2977,0,37,4237,50,52,4277,0,52,5632,50,72,5672,0,72,7167,50,101,7207,0,101,8842,50,147,8882,0,147,10703,50,229,10743,0,229,12750,50,383,12790,0,383,15029,50,622,15069,0,622,17540,50,1041,17540,40,1041,17580,0,1041,28290,3,1344,28975,4,1492,29669,1,1642,29669,50,1642,29669,40,1642,29709,0,1642,29996,3,1953,30005,4,2096,30018,5,2243,30018,1,2244,30018,50,2244,30018,40,2244,30058,0,2244,52294,3,3746,53206,4,4495,53871,5,5245,53872,1,5245,53872,50,5246,53872,40,5246,53912,0,5246,71380,3,5998,71869,4,6372,72459,1,6747,72459,50,6747,72459,40,6747,72499,0,6747,83531,3,7498,84499,4,7873,85929,5,8248,85930,5,8248,85931,1,8248,85931,50,8248,85931,40,8248,85971,0,8248,125927,3,12149,127846,4,14099,129344,5,16049,129345,1,16049,129345,50,16051,129345,40,16051,129385,0,16051,164157,3,18602,165533,4,19877,166544,5,21152,166545,1,21152,166545,50,21153,166545,40,21153,166585,0,21153,198860,3,22654,199563,4,23404,200451,5,24154,200452,1,24154,200452,50,24156,200452,40,24156,200492,0,24156,210035,3,24918,211163,4,25282,211512,5,25657,211513,1,25657,211513,50,25657,211513,40,25657,211553,0,25657,235871,3,26858,236780,4,27458,237513,1,28058,237513,50,28059,237513,40,28059,237553,0,28059,254586,3,28810,255240,4,29185,255695,5,29560,255696,1,29560,255696,50,29560,255696,40,29560,255696,40,29560,255731,0,29560,255906,50,29561,255906,30,29561,255906,40,29561,255941,0,29561,256054,50,29562,256089,0,29567,256247,50,29568,256247,30,29568,256247,40,29568,256282,0,29568,256389,50,29569,256424,0,29569,256597,50,29570,256597,30,29570,256597,40,29570,256632,0,29575,256752,50,29575,256787,0,29575)
%
%
% START OF PROOF
% 256754 [] equal(multiply(identity,X),X).
% 256755 [] equal(multiply(inverse(X),X),identity).
% 256756 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 256757 [] -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7).
% 256770 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c4),sk_c8).
% 256771 [] equal(multiply(sk_c4,sk_c8),sk_c5) | equal(inverse(sk_c1),sk_c7).
% 256772 [] equal(multiply(sk_c8,sk_c5),sk_c7) | equal(inverse(sk_c1),sk_c7).
% 256773 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c3),sk_c8).
% 256774 [] equal(multiply(sk_c3,sk_c8),sk_c7) | equal(inverse(sk_c1),sk_c7).
% 256775 [] equal(multiply(sk_c8,sk_c7),sk_c6) | equal(inverse(sk_c1),sk_c7).
% 256776 [?] ?
% 256777 [?] ?
% 256778 [?] ?
% 256779 [?] ?
% 256780 [?] ?
% 256781 [?] ?
% 256795 [hyper:256757,256770,binarycut:256776] equal(inverse(sk_c4),sk_c8).
% 256796 [para:256795.1.1,256755.1.1.1] equal(multiply(sk_c8,sk_c4),identity).
% 256799 [hyper:256757,256773,binarycut:256779] equal(inverse(sk_c3),sk_c8).
% 256801 [para:256799.1.1,256755.1.1.1] equal(multiply(sk_c8,sk_c3),identity).
% 256817 [hyper:256757,256771,binarycut:256777] equal(multiply(sk_c4,sk_c8),sk_c5).
% 256820 [hyper:256757,256772,binarycut:256778] equal(multiply(sk_c8,sk_c5),sk_c7).
% 256824 [hyper:256757,256774,binarycut:256780] equal(multiply(sk_c3,sk_c8),sk_c7).
% 256827 [hyper:256757,256775,binarycut:256781] equal(multiply(sk_c8,sk_c7),sk_c6).
% 256828 [para:256755.1.1,256756.1.1.1,demod:256754] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 256829 [para:256796.1.1,256756.1.1.1,demod:256754] equal(X,multiply(sk_c8,multiply(sk_c4,X))).
% 256830 [para:256801.1.1,256756.1.1.1,demod:256754] equal(X,multiply(sk_c8,multiply(sk_c3,X))).
% 256831 [para:256817.1.1,256756.1.1.1] equal(multiply(sk_c5,X),multiply(sk_c4,multiply(sk_c8,X))).
% 256832 [para:256820.1.1,256756.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c8,multiply(sk_c5,X))).
% 256833 [para:256824.1.1,256756.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c3,multiply(sk_c8,X))).
% 256835 [para:256817.1.1,256829.1.2.2,demod:256820] equal(sk_c8,sk_c7).
% 256838 [para:256824.1.1,256830.1.2.2,demod:256827] equal(sk_c8,sk_c6).
% 256840 [para:256755.1.1,256828.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 256841 [para:256796.1.1,256828.1.2.2] equal(sk_c4,multiply(inverse(sk_c8),identity)).
% 256842 [para:256801.1.1,256828.1.2.2,demod:256841] equal(sk_c3,sk_c4).
% 256844 [para:256756.1.1,256828.1.2.2] equal(X,multiply(inverse(multiply(Y,Z)),multiply(Y,multiply(Z,X)))).
% 256845 [para:256827.1.1,256828.1.2.2] equal(sk_c7,multiply(inverse(sk_c8),sk_c6)).
% 256846 [para:256829.1.2,256828.1.2.2] equal(multiply(sk_c4,X),multiply(inverse(sk_c8),X)).
% 256847 [para:256830.1.2,256828.1.2.2,demod:256846] equal(multiply(sk_c3,X),multiply(sk_c4,X)).
% 256848 [para:256828.1.2,256828.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 256851 [para:256838.1.1,256817.1.1.2,demod:256847] equal(multiply(sk_c3,sk_c6),sk_c5).
% 256853 [para:256838.1.1,256824.1.1.2,demod:256851] equal(sk_c5,sk_c7).
% 256859 [para:256853.1.2,256827.1.1.2,demod:256820] equal(sk_c7,sk_c6).
% 256860 [para:256853.1.2,256835.1.2] equal(sk_c8,sk_c5).
% 256862 [para:256859.1.1,256853.1.2] equal(sk_c5,sk_c6).
% 256866 [para:256820.1.1,256831.1.2.2,demod:256847] equal(multiply(sk_c5,sk_c5),multiply(sk_c3,sk_c7)).
% 256868 [para:256831.1.2,256829.1.2.2,demod:256832] equal(multiply(sk_c8,X),multiply(sk_c7,X)).
% 256869 [para:256829.1.2,256831.1.2.2,demod:256847] equal(multiply(sk_c5,multiply(sk_c3,X)),multiply(sk_c3,X)).
% 256872 [para:256842.1.2,256831.1.2.1,demod:256868,256833] equal(multiply(sk_c5,X),multiply(sk_c8,X)).
% 256875 [para:256860.1.1,256820.1.1.1,demod:256866] equal(multiply(sk_c3,sk_c7),sk_c7).
% 256876 [para:256860.1.1,256829.1.2.1,demod:256869,256847] equal(X,multiply(sk_c3,X)).
% 256877 [para:256860.1.1,256830.1.2.1,demod:256876] equal(X,multiply(sk_c5,X)).
% 256881 [para:256877.1.2,256828.1.2.2] equal(X,multiply(inverse(sk_c5),X)).
% 256888 [para:256881.1.2,256755.1.1] equal(sk_c5,identity).
% 256890 [para:256888.1.1,256862.1.1] equal(identity,sk_c6).
% 256934 [para:256890.1.2,256845.1.2.2,demod:256841] equal(sk_c7,sk_c4).
% 256938 [para:256934.1.1,256875.1.1.2,demod:256876] equal(sk_c4,sk_c7).
% 256943 [para:256848.1.2,256755.1.1] equal(multiply(X,inverse(X)),identity).
% 256945 [para:256848.1.2,256840.1.2] equal(X,multiply(X,identity)).
% 256946 [para:256945.1.2,256840.1.2] equal(X,inverse(inverse(X))).
% 256947 [para:256945.1.2,256841.1.2] equal(sk_c4,inverse(sk_c8)).
% 256951 [para:256943.1.1,256844.1.2.2.2,demod:256945] equal(inverse(X),multiply(inverse(multiply(Y,X)),Y)).
% 256961 [para:256868.1.2,256951.1.2.1.1,demod:256877,256872] equal(inverse(X),multiply(inverse(X),sk_c7)).
% 256974 [para:256961.1.2,256848.1.2,demod:256946] equal(multiply(X,sk_c7),X).
% 256975 [hyper:256757,256974,demod:256947,cut:256938] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 4
% seconds given: 4
%
%
% Split component 5 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c8),sk_c6) | -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7) | -equal(inverse(Y),sk_c7) | -equal(multiply(Y,sk_c6),sk_c7) | -equal(multiply(sk_c8,sk_c7),sk_c6) | -equal(multiply(Z,sk_c8),sk_c7) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c8,U),sk_c7) | -equal(multiply(V,sk_c8),U) | -equal(inverse(V),sk_c8).
% Split part used next: -equal(multiply(sk_c7,sk_c8),sk_c6).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 4
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 5
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 6
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 7
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 8
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 9
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 10
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 11
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,1,75,0,1,706,50,6,746,0,6,1731,50,19,1771,0,20,2937,50,37,2977,0,37,4237,50,52,4277,0,52,5632,50,72,5672,0,72,7167,50,101,7207,0,101,8842,50,147,8882,0,147,10703,50,229,10743,0,229,12750,50,383,12790,0,383,15029,50,622,15069,0,622,17540,50,1041,17540,40,1041,17580,0,1041,28290,3,1344,28975,4,1492,29669,1,1642,29669,50,1642,29669,40,1642,29709,0,1642,29996,3,1953,30005,4,2096,30018,5,2243,30018,1,2244,30018,50,2244,30018,40,2244,30058,0,2244,52294,3,3746,53206,4,4495,53871,5,5245,53872,1,5245,53872,50,5246,53872,40,5246,53912,0,5246,71380,3,5998,71869,4,6372,72459,1,6747,72459,50,6747,72459,40,6747,72499,0,6747,83531,3,7498,84499,4,7873,85929,5,8248,85930,5,8248,85931,1,8248,85931,50,8248,85931,40,8248,85971,0,8248,125927,3,12149,127846,4,14099,129344,5,16049,129345,1,16049,129345,50,16051,129345,40,16051,129385,0,16051,164157,3,18602,165533,4,19877,166544,5,21152,166545,1,21152,166545,50,21153,166545,40,21153,166585,0,21153,198860,3,22654,199563,4,23404,200451,5,24154,200452,1,24154,200452,50,24156,200452,40,24156,200492,0,24156,210035,3,24918,211163,4,25282,211512,5,25657,211513,1,25657,211513,50,25657,211513,40,25657,211553,0,25657,235871,3,26858,236780,4,27458,237513,1,28058,237513,50,28059,237513,40,28059,237553,0,28059,254586,3,28810,255240,4,29185,255695,5,29560,255696,1,29560,255696,50,29560,255696,40,29560,255696,40,29560,255731,0,29560,255906,50,29561,255906,30,29561,255906,40,29561,255941,0,29561,256054,50,29562,256089,0,29567,256247,50,29568,256247,30,29568,256247,40,29568,256282,0,29568,256389,50,29569,256424,0,29569,256597,50,29570,256597,30,29570,256597,40,29570,256632,0,29575,256752,50,29575,256787,0,29575,256974,50,29577,256974,30,29577,256974,40,29577,257009,0,29582,257135,50,29583,257170,0,29583,257361,50,29586,257396,0,29586,257604,50,29589,257639,0,29594,257860,50,29599,257895,0,29599,258122,50,29606,258157,0,29611,258392,50,29625,258427,0,29625,258670,50,29652,258705,0,29652,258958,50,29712,258993,0,29712,259256,50,29826,259256,40,29826,259291,0,29826)
%
%
% START OF PROOF
% 259048 [?] ?
% 259258 [] equal(multiply(identity,X),X).
% 259259 [] equal(multiply(inverse(X),X),identity).
% 259260 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 259261 [] -equal(multiply(sk_c7,sk_c8),sk_c6).
% 259286 [?] ?
% 259287 [?] ?
% 259288 [?] ?
% 259330 [input:259286,cut:259261] equal(inverse(sk_c4),sk_c8).
% 259331 [para:259330.1.1,259259.1.1.1] equal(multiply(sk_c8,sk_c4),identity).
% 259344 [input:259287,cut:259261] equal(multiply(sk_c4,sk_c8),sk_c5).
% 259345 [input:259288,cut:259261] equal(multiply(sk_c8,sk_c5),sk_c7).
% 259368 [para:259331.1.1,259260.1.1.1,demod:259258] equal(X,multiply(sk_c8,multiply(sk_c4,X))).
% 259393 [para:259344.1.1,259368.1.2.2] equal(sk_c8,multiply(sk_c8,sk_c5)).
% 259398 [para:259393.1.2,259345.1.1] equal(sk_c8,sk_c7).
% 259400 [para:259398.1.2,259261.1.1.1,cut:259048] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% Split component 6 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c8),sk_c6) | -equal(multiply(X,sk_c7),sk_c8) | -equal(inverse(X),sk_c7) | -equal(inverse(Y),sk_c7) | -equal(multiply(Y,sk_c6),sk_c7) | -equal(multiply(sk_c8,sk_c7),sk_c6) | -equal(multiply(Z,sk_c8),sk_c7) | -equal(inverse(Z),sk_c8) | -equal(multiply(sk_c8,U),sk_c7) | -equal(multiply(V,sk_c8),U) | -equal(inverse(V),sk_c8).
% Split part used next: -equal(multiply(sk_c8,sk_c7),sk_c6).
% END OF PROOFPART
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 3
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 4
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 5
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 6
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 7
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 8
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 9
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 10
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 21
% clause depth limited to 11
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(35,40,1,75,0,1,706,50,6,746,0,6,1731,50,19,1771,0,20,2937,50,37,2977,0,37,4237,50,52,4277,0,52,5632,50,72,5672,0,72,7167,50,101,7207,0,101,8842,50,147,8882,0,147,10703,50,229,10743,0,229,12750,50,383,12790,0,383,15029,50,622,15069,0,622,17540,50,1041,17540,40,1041,17580,0,1041,28290,3,1344,28975,4,1492,29669,1,1642,29669,50,1642,29669,40,1642,29709,0,1642,29996,3,1953,30005,4,2096,30018,5,2243,30018,1,2244,30018,50,2244,30018,40,2244,30058,0,2244,52294,3,3746,53206,4,4495,53871,5,5245,53872,1,5245,53872,50,5246,53872,40,5246,53912,0,5246,71380,3,5998,71869,4,6372,72459,1,6747,72459,50,6747,72459,40,6747,72499,0,6747,83531,3,7498,84499,4,7873,85929,5,8248,85930,5,8248,85931,1,8248,85931,50,8248,85931,40,8248,85971,0,8248,125927,3,12149,127846,4,14099,129344,5,16049,129345,1,16049,129345,50,16051,129345,40,16051,129385,0,16051,164157,3,18602,165533,4,19877,166544,5,21152,166545,1,21152,166545,50,21153,166545,40,21153,166585,0,21153,198860,3,22654,199563,4,23404,200451,5,24154,200452,1,24154,200452,50,24156,200452,40,24156,200492,0,24156,210035,3,24918,211163,4,25282,211512,5,25657,211513,1,25657,211513,50,25657,211513,40,25657,211553,0,25657,235871,3,26858,236780,4,27458,237513,1,28058,237513,50,28059,237513,40,28059,237553,0,28059,254586,3,28810,255240,4,29185,255695,5,29560,255696,1,29560,255696,50,29560,255696,40,29560,255696,40,29560,255731,0,29560,255906,50,29561,255906,30,29561,255906,40,29561,255941,0,29561,256054,50,29562,256089,0,29567,256247,50,29568,256247,30,29568,256247,40,29568,256282,0,29568,256389,50,29569,256424,0,29569,256597,50,29570,256597,30,29570,256597,40,29570,256632,0,29575,256752,50,29575,256787,0,29575,256974,50,29577,256974,30,29577,256974,40,29577,257009,0,29582,257135,50,29583,257170,0,29583,257361,50,29586,257396,0,29586,257604,50,29589,257639,0,29594,257860,50,29599,257895,0,29599,258122,50,29606,258157,0,29611,258392,50,29625,258427,0,29625,258670,50,29652,258705,0,29652,258958,50,29712,258993,0,29712,259256,50,29826,259256,40,29826,259291,0,29826,259399,50,29826,259399,30,29826,259399,40,29826,259434,0,29826,259534,50,29827,259569,0,29831,259736,50,29833,259771,0,29833,259955,50,29835,259990,0,29835,260187,50,29839,260222,0,29843,260425,50,29850,260460,0,29850,260671,50,29864,260706,0,29868,260925,50,29894,260960,0,29894,261189,50,29953,261224,0,29953,261463,50,30091,261463,40,30091,261498,0,30092)
%
%
% START OF PROOF
% 261304 [?] ?
% 261465 [] equal(multiply(identity,X),X).
% 261466 [] equal(multiply(inverse(X),X),identity).
% 261467 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 261468 [] -equal(multiply(sk_c8,sk_c7),sk_c6).
% 261486 [?] ?
% 261492 [?] ?
% 261498 [?] ?
% 261531 [input:261486,cut:261468] equal(inverse(sk_c1),sk_c7).
% 261532 [para:261531.1.1,261466.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 261550 [input:261492,cut:261468] equal(multiply(sk_c1,sk_c7),sk_c8).
% 261554 [input:261498,cut:261468] equal(multiply(sk_c7,sk_c8),sk_c6).
% 261571 [para:261532.1.1,261467.1.1.1,demod:261465] equal(X,multiply(sk_c7,multiply(sk_c1,X))).
% 261611 [para:261550.1.1,261571.1.2.2] equal(sk_c7,multiply(sk_c7,sk_c8)).
% 261617 [para:261611.1.2,261554.1.1] equal(sk_c7,sk_c6).
% 261619 [para:261617.1.1,261468.1.1.2,cut:261304] 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: 35852
% derived clauses: 7329123
% kept clauses: 205800
% kept size sum: 878237
% kept mid-nuclei: 14181
% kept new demods: 4403
% forw unit-subs: 3411390
% forw double-subs: 3508562
% forw overdouble-subs: 149989
% backward subs: 13567
% fast unit cutoff: 28415
% full unit cutoff: 0
% dbl unit cutoff: 6416
% real runtime : 302.89
% process. runtime: 300.91
% specific non-discr-tree subsumption statistics:
% tried: 39442478
% length fails: 4337965
% strength fails: 12885934
% predlist fails: 4208433
% aux str. fails: 6017465
% by-lit fails: 6560571
% full subs tried: 1492513
% full subs fail: 1401246
%
% ; 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/GRP332-1+eq_r.in")
%
%------------------------------------------------------------------------------