%------------------------------------------------------------------------------
% File       : Otter---3.2
% Problem    : Unknown : TPTP Unknown
% Transform  : rm_equality:stfp
% Format     : otter:hypothesis:set(auto),clear(print_given)
% Command    : otter-script %s

% Computer   : Unknown
% Model      : Unknown
% CPU        : Unknown @ Unknown
% Memory     : Unknown
% OS         : Unknown
% CPULimit   : Unknowns

% Result     : Unsatisfiable 7.5s
% Output     : Refutation 7.5s
% Statistics : TBA
% Verified   : 

% Comments   : 
%------------------------------------------------------------------------------
%----TSTP SOLUTION
% 1 [] -product(A,B,C)| -product(A,B,D)|equal(C,D).
cnf(1,inital,
    ( ~product(A,B,C)
    | ~product(A,B,D)
    | equal(C,D) ),
    file('Unknown',unknown),
    []).

% 2 [] -product(A,B,C)| -product(B,D,E)| -product(C,D,F)|product(A,E,F).
cnf(2,inital,
    ( ~product(A,B,C)
    | ~product(B,D,E)
    | ~product(C,D,F)
    | product(A,E,F) ),
    file('Unknown',unknown),
    []).

% 3 [] -product(A,B,C)| -product(B,D,E)| -product(A,E,F)|product(C,D,F).
cnf(3,inital,
    ( ~product(A,B,C)
    | ~product(B,D,E)
    | ~product(A,E,F)
    | product(C,D,F) ),
    file('Unknown',unknown),
    []).

% 4 [] -subgroup1_member(A)|subgroup1_member(inverse(A)).
cnf(4,inital,
    ( ~subgroup1_member(A)
    | subgroup1_member(inverse(A)) ),
    file('Unknown',unknown),
    []).

% 5 [] -subgroup1_member(A)| -subgroup1_member(B)| -product(A,B,C)|subgroup1_member(C).
cnf(5,inital,
    ( ~subgroup1_member(A)
    | ~subgroup1_member(B)
    | ~product(A,B,C)
    | subgroup1_member(C) ),
    file('Unknown',unknown),
    []).

% 6 [] -subgroup2_member(A)|subgroup2_member(inverse(A)).
cnf(6,inital,
    ( ~subgroup2_member(A)
    | subgroup2_member(inverse(A)) ),
    file('Unknown',unknown),
    []).

% 7 [] -subgroup2_member(A)| -subgroup2_member(B)| -product(A,B,C)|subgroup2_member(C).
cnf(7,inital,
    ( ~subgroup2_member(A)
    | ~subgroup2_member(B)
    | ~product(A,B,C)
    | subgroup2_member(C) ),
    file('Unknown',unknown),
    []).

% 8 [] -subgroup1_member(A)|subgroup1_member(multiply(B,multiply(A,inverse(B)))).
cnf(8,inital,
    ( ~subgroup1_member(A)
    | subgroup1_member(multiply(B,multiply(A,inverse(B)))) ),
    file('Unknown',unknown),
    []).

% 9 [] -subgroup2_member(A)|subgroup2_member(multiply(B,multiply(A,inverse(B)))).
cnf(9,inital,
    ( ~subgroup2_member(A)
    | subgroup2_member(multiply(B,multiply(A,inverse(B)))) ),
    file('Unknown',unknown),
    []).

% 10 [] -subgroup1_member(A)| -subgroup2_member(A)|equal(A,identity).
cnf(10,inital,
    ( ~subgroup1_member(A)
    | ~subgroup2_member(A)
    | equal(A,identity) ),
    file('Unknown',unknown),
    []).

% 11 [] -equal(multiply(v,u),multiply(u,v)).
cnf(11,inital,
    ( ~equal(multiply(v,u),multiply(u,v)) ),
    file('Unknown',unknown),
    []).

% 13 [] product(identity,A,A).
cnf(13,inital,
    ( product(identity,A,A) ),
    file('Unknown',unknown),
    []).

% 14 [] product(A,identity,A).
cnf(14,inital,
    ( product(A,identity,A) ),
    file('Unknown',unknown),
    []).

% 15 [] product(inverse(A),A,identity).
cnf(15,inital,
    ( product(inverse(A),A,identity) ),
    file('Unknown',unknown),
    []).

% 16 [] product(A,inverse(A),identity).
cnf(16,inital,
    ( product(A,inverse(A),identity) ),
    file('Unknown',unknown),
    []).

% 17 [] product(A,B,multiply(A,B)).
cnf(17,inital,
    ( product(A,B,multiply(A,B)) ),
    file('Unknown',unknown),
    []).

% 18 [] subgroup1_member(v).
cnf(18,inital,
    ( subgroup1_member(v) ),
    file('Unknown',unknown),
    []).

% 19 [] subgroup2_member(u).
cnf(19,inital,
    ( subgroup2_member(u) ),
    file('Unknown',unknown),
    []).

% 20 [hyper,18,8] subgroup1_member(multiply(A,multiply(v,inverse(A)))).
cnf(20,derived,
    ( subgroup1_member(multiply(A,multiply(v,inverse(A)))) ),
    inference(hyper,'',[18,8]),
    [iquote('hyper,18,8')]).

% 21 [hyper,18,4] subgroup1_member(inverse(v)).
cnf(21,derived,
    ( subgroup1_member(inverse(v)) ),
    inference(hyper,'',[18,4]),
    [iquote('hyper,18,4')]).

% 25 [hyper,19,6] subgroup2_member(inverse(u)).
cnf(25,derived,
    ( subgroup2_member(inverse(u)) ),
    inference(hyper,'',[19,6]),
    [iquote('hyper,19,6')]).

% 34 [hyper,25,9] subgroup2_member(multiply(A,multiply(inverse(u),inverse(A)))).
cnf(34,derived,
    ( subgroup2_member(multiply(A,multiply(inverse(u),inverse(A)))) ),
    inference(hyper,'',[25,9]),
    [iquote('hyper,25,9')]).

% 60 [hyper,15,3,15,14] product(identity,A,inverse(inverse(A))).
cnf(60,derived,
    ( product(identity,A,inverse(inverse(A))) ),
    inference(hyper,'',[15,3,15,14]),
    [iquote('hyper,15,3,15,14')]).

% 129 [hyper,17,3,17,17] product(multiply(A,B),C,multiply(A,multiply(B,C))).
cnf(129,derived,
    ( product(multiply(A,B),C,multiply(A,multiply(B,C))) ),
    inference(hyper,'',[17,3,17,17]),
    [iquote('hyper,17,3,17,17')]).

% 149 [hyper,17,3,16,14] product(multiply(A,B),inverse(B),A).
cnf(149,derived,
    ( product(multiply(A,B),inverse(B),A) ),
    inference(hyper,'',[17,3,16,14]),
    [iquote('hyper,17,3,16,14')]).

% 172 [hyper,17,2,16,13] product(A,multiply(inverse(A),B),B).
cnf(172,derived,
    ( product(A,multiply(inverse(A),B),B) ),
    inference(hyper,'',[17,2,16,13]),
    [iquote('hyper,17,2,16,13')]).

% 188,187 [hyper,17,1,14,flip.1] equal(multiply(A,identity),A).
cnf(188,derived,
    ( equal(multiply(A,identity),A) ),
    inference(hyper+flip,'',[17,1,14,theory(equality)]),
    [iquote('hyper,17,1,14,flip.1')]).

% 190,189 [hyper,17,1,13,flip.1] equal(multiply(identity,A),A).
cnf(190,derived,
    ( equal(multiply(identity,A),A) ),
    inference(hyper+flip,'',[17,1,13,theory(equality)]),
    [iquote('hyper,17,1,13,flip.1')]).

% 191 [para_into,17.1.3,10.3.1] product(A,B,identity)| -subgroup1_member(multiply(A,B))| -subgroup2_member(multiply(A,B)).
cnf(191,derived,
    ( product(A,B,identity)
    | ~subgroup1_member(multiply(A,B))
    | ~subgroup2_member(multiply(A,B)) ),
    inference(para_into,'',[17,10,theory(equality)]),
    [iquote('para_into,17.1.3,10.3.1')]).

% 306,305 [hyper,60,1,17,demod,190,flip.1] equal(inverse(inverse(A)),A).
cnf(306,derived,
    ( equal(inverse(inverse(A)),A) ),
    inference(hyper+demod+flip,'',[60,1,17,190,theory(equality)]),
    [iquote('hyper,60,1,17,demod,190,flip.1')]).

% 466 [hyper,149,2,15,17,demod,190] product(inverse(multiply(A,B)),A,inverse(B)).
cnf(466,derived,
    ( product(inverse(multiply(A,B)),A,inverse(B)) ),
    inference(hyper+demod,'',[149,2,15,17,190,theory(equality)]),
    [iquote('hyper,149,2,15,17,demod,190')]).

% 835 [hyper,34,7,19,17] subgroup2_member(multiply(u,multiply(A,multiply(inverse(u),inverse(A))))).
cnf(835,derived,
    ( subgroup2_member(multiply(u,multiply(A,multiply(inverse(u),inverse(A))))) ),
    inference(hyper,'',[34,7,19,17]),
    [iquote('hyper,34,7,19,17')]).

% 1764 [hyper,466,3,172,14,demod,188] product(inverse(A),inverse(B),inverse(multiply(B,A))).
cnf(1764,derived,
    ( product(inverse(A),inverse(B),inverse(multiply(B,A))) ),
    inference(hyper+demod,'',[466,3,172,14,188,theory(equality)]),
    [iquote('hyper,466,3,172,14,demod,188')]).

% 4171 [hyper,129,5,20,21] subgroup1_member(multiply(A,multiply(multiply(v,inverse(A)),inverse(v)))).
cnf(4171,derived,
    ( subgroup1_member(multiply(A,multiply(multiply(v,inverse(A)),inverse(v)))) ),
    inference(hyper,'',[129,5,20,21]),
    [iquote('hyper,129,5,20,21')]).

% 4369,4368 [hyper,129,1,17] equal(multiply(multiply(A,B),C),multiply(A,multiply(B,C))).
cnf(4369,derived,
    ( equal(multiply(multiply(A,B),C),multiply(A,multiply(B,C))) ),
    inference(hyper,'',[129,1,17]),
    [iquote('hyper,129,1,17')]).

% 4397 [back_demod,4171,demod,4369] subgroup1_member(multiply(A,multiply(v,multiply(inverse(A),inverse(v))))).
cnf(4397,derived,
    ( subgroup1_member(multiply(A,multiply(v,multiply(inverse(A),inverse(v))))) ),
    inference(back_demod+demod,'',[4171,4369,theory(equality)]),
    [iquote('back_demod,4171,demod,4369')]).

% 6634,6633 [hyper,1764,1,17,flip.1] equal(inverse(multiply(A,B)),multiply(inverse(B),inverse(A))).
cnf(6634,derived,
    ( equal(inverse(multiply(A,B)),multiply(inverse(B),inverse(A))) ),
    inference(hyper+flip,'',[1764,1,17,theory(equality)]),
    [iquote('hyper,1764,1,17,flip.1')]).

% 7696 [hyper,4397,191,835] product(u,multiply(v,multiply(inverse(u),inverse(v))),identity).
cnf(7696,derived,
    ( product(u,multiply(v,multiply(inverse(u),inverse(v))),identity) ),
    inference(hyper,'',[4397,191,835]),
    [iquote('hyper,4397,191,835')]).

% 8405 [hyper,7696,2,149,17,demod,6634,306,306,190] product(u,v,multiply(v,u)).
cnf(8405,derived,
    ( product(u,v,multiply(v,u)) ),
    inference(hyper+demod,'',[7696,2,149,17,6634,306,306,190,theory(equality)]),
    [iquote('hyper,7696,2,149,17,demod,6634,306,306,190')]).

% 8455 [hyper,8405,1,17,flip.1] equal(multiply(v,u),multiply(u,v)).
cnf(8455,derived,
    ( equal(multiply(v,u),multiply(u,v)) ),
    inference(hyper+flip,'',[8405,1,17,theory(equality)]),
    [iquote('hyper,8405,1,17,flip.1')]).

% 8457 [binary,8455.1,11.1] $F.
cnf(8457,derived,
    ( false ),
    inference(binary,'',[8455,11]),
    [iquote('binary,8455.1,11.1')]).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% ----- Otter 3.2-beta3, May 2001 -----
% The process was started by tptp on diver,
% Wed Sep 25 00:33:53 2002
% The command was "/home/tptp/Systems/Otter-MACE---3.2-2.0/otter".  The process ID is 29767.
% 
% set(prolog_style_variables).
% set(tptp_eq).
% set(auto).
%    dependent: set(auto1).
%    dependent: set(process_input).
%    dependent: clear(print_kept).
%    dependent: clear(print_new_demod).
%    dependent: clear(print_back_demod).
%    dependent: clear(print_back_sub).
%    dependent: set(control_memory).
%    dependent: assign(max_mem, 12000).
%    dependent: assign(pick_given_ratio, 4).
%    dependent: assign(stats_level, 1).
%    dependent: assign(max_seconds, 10800).
% clear(print_given).
% 
% list(usable).
% 0 [] equal(X,X).
% 0 [] product(identity,X,X).
% 0 [] product(X,identity,X).
% 0 [] product(inverse(X),X,identity).
% 0 [] product(X,inverse(X),identity).
% 0 [] product(X,Y,multiply(X,Y)).
% 0 [] -product(X,Y,Z)| -product(X,Y,W)|equal(Z,W).
% 0 [] -product(X,Y,U)| -product(Y,Z,V)| -product(U,Z,W)|product(X,V,W).
% 0 [] -product(X,Y,U)| -product(Y,Z,V)| -product(X,V,W)|product(U,Z,W).
% 0 [] -subgroup1_member(X)|subgroup1_member(inverse(X)).
% 0 [] -subgroup1_member(A)| -subgroup1_member(B)| -product(A,B,C)|subgroup1_member(C).
% 0 [] -subgroup2_member(X)|subgroup2_member(inverse(X)).
% 0 [] -subgroup2_member(A)| -subgroup2_member(B)| -product(A,B,C)|subgroup2_member(C).
% end_of_list.
% 
% list(sos).
% 0 [] -subgroup1_member(X)|subgroup1_member(multiply(A,multiply(X,inverse(A)))).
% 0 [] -subgroup2_member(X)|subgroup2_member(multiply(A,multiply(X,inverse(A)))).
% 0 [] -subgroup1_member(X)| -subgroup2_member(X)|equal(X,identity).
% 0 [] subgroup1_member(v).
% 0 [] subgroup2_member(u).
% 0 [] -equal(multiply(v,u),multiply(u,v)).
% end_of_list.
% WARNING: Sos list not accepted in auto1 mode:
%          sos clauses are being moved to usable list.
% 
% SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=4.
% 
% This is a Horn set with equality.  The strategy will be
% Knuth-Bendix and hyper_res, with positive clauses in
% sos and nonpositive clauses in usable.
% 
%    dependent: set(knuth_bendix).
%    dependent: set(para_from).
%    dependent: set(para_into).
%    dependent: clear(para_from_right).
%    dependent: clear(para_into_right).
%    dependent: set(para_from_vars).
%    dependent: set(eq_units_both_ways).
%    dependent: set(dynamic_demod_all).
%    dependent: set(dynamic_demod).
%    dependent: set(order_eq).
%    dependent: set(back_demod).
%    dependent: set(lrpo).
%    dependent: set(hyper_res).
%    dependent: clear(order_hyper).
% 
% ------------> process usable:
% ** KEPT (pick-wt=11): 1 [] -product(A,B,C)| -product(A,B,D)|equal(C,D).
% ** KEPT (pick-wt=16): 2 [] -product(A,B,C)| -product(B,D,E)| -product(C,D,F)|product(A,E,F).
% ** KEPT (pick-wt=16): 3 [] -product(A,B,C)| -product(B,D,E)| -product(A,E,F)|product(C,D,F).
% ** KEPT (pick-wt=5): 4 [] -subgroup1_member(A)|subgroup1_member(inverse(A)).
% ** KEPT (pick-wt=10): 5 [] -subgroup1_member(A)| -subgroup1_member(B)| -product(A,B,C)|subgroup1_member(C).
% ** KEPT (pick-wt=5): 6 [] -subgroup2_member(A)|subgroup2_member(inverse(A)).
% ** KEPT (pick-wt=10): 7 [] -subgroup2_member(A)| -subgroup2_member(B)| -product(A,B,C)|subgroup2_member(C).
% ** KEPT (pick-wt=9): 8 [] -subgroup1_member(A)|subgroup1_member(multiply(B,multiply(A,inverse(B)))).
% ** KEPT (pick-wt=9): 9 [] -subgroup2_member(A)|subgroup2_member(multiply(B,multiply(A,inverse(B)))).
% ** KEPT (pick-wt=7): 10 [] -subgroup1_member(A)| -subgroup2_member(A)|equal(A,identity).
% ** KEPT (pick-wt=7): 11 [] -equal(multiply(v,u),multiply(u,v)).
% 
% ------------> process sos:
% ** KEPT (pick-wt=3): 12 [] equal(A,A).
% ** KEPT (pick-wt=4): 13 [] product(identity,A,A).
% ** KEPT (pick-wt=4): 14 [] product(A,identity,A).
% ** KEPT (pick-wt=5): 15 [] product(inverse(A),A,identity).
% ** KEPT (pick-wt=5): 16 [] product(A,inverse(A),identity).
% ** KEPT (pick-wt=6): 17 [] product(A,B,multiply(A,B)).
% ** KEPT (pick-wt=2): 18 [] subgroup1_member(v).
% ** KEPT (pick-wt=2): 19 [] subgroup2_member(u).
%   Following clause subsumed by 12 during input processing: 0 [copy,12,flip.1] equal(A,A).
% 
% ======= end of input processing =======
% 
% =========== start of search ===========
% 
% -------- PROOF -------- 
% 
% ----> UNIT CONFLICT at   7.46 sec ----> 8457 [binary,8455.1,11.1] $F.
% 
% Length of proof is 22.  Level of proof is 6.
% 
% ---------------- PROOF ----------------
% 
% 1 [] -product(A,B,C)| -product(A,B,D)|equal(C,D).
% 2 [] -product(A,B,C)| -product(B,D,E)| -product(C,D,F)|product(A,E,F).
% 3 [] -product(A,B,C)| -product(B,D,E)| -product(A,E,F)|product(C,D,F).
% 4 [] -subgroup1_member(A)|subgroup1_member(inverse(A)).
% 5 [] -subgroup1_member(A)| -subgroup1_member(B)| -product(A,B,C)|subgroup1_member(C).
% 6 [] -subgroup2_member(A)|subgroup2_member(inverse(A)).
% 7 [] -subgroup2_member(A)| -subgroup2_member(B)| -product(A,B,C)|subgroup2_member(C).
% 8 [] -subgroup1_member(A)|subgroup1_member(multiply(B,multiply(A,inverse(B)))).
% 9 [] -subgroup2_member(A)|subgroup2_member(multiply(B,multiply(A,inverse(B)))).
% 10 [] -subgroup1_member(A)| -subgroup2_member(A)|equal(A,identity).
% 11 [] -equal(multiply(v,u),multiply(u,v)).
% 13 [] product(identity,A,A).
% 14 [] product(A,identity,A).
% 15 [] product(inverse(A),A,identity).
% 16 [] product(A,inverse(A),identity).
% 17 [] product(A,B,multiply(A,B)).
% 18 [] subgroup1_member(v).
% 19 [] subgroup2_member(u).
% 20 [hyper,18,8] subgroup1_member(multiply(A,multiply(v,inverse(A)))).
% 21 [hyper,18,4] subgroup1_member(inverse(v)).
% 25 [hyper,19,6] subgroup2_member(inverse(u)).
% 34 [hyper,25,9] subgroup2_member(multiply(A,multiply(inverse(u),inverse(A)))).
% 60 [hyper,15,3,15,14] product(identity,A,inverse(inverse(A))).
% 129 [hyper,17,3,17,17] product(multiply(A,B),C,multiply(A,multiply(B,C))).
% 149 [hyper,17,3,16,14] product(multiply(A,B),inverse(B),A).
% 172 [hyper,17,2,16,13] product(A,multiply(inverse(A),B),B).
% 188,187 [hyper,17,1,14,flip.1] equal(multiply(A,identity),A).
% 190,189 [hyper,17,1,13,flip.1] equal(multiply(identity,A),A).
% 191 [para_into,17.1.3,10.3.1] product(A,B,identity)| -subgroup1_member(multiply(A,B))| -subgroup2_member(multiply(A,B)).
% 306,305 [hyper,60,1,17,demod,190,flip.1] equal(inverse(inverse(A)),A).
% 466 [hyper,149,2,15,17,demod,190] product(inverse(multiply(A,B)),A,inverse(B)).
% 835 [hyper,34,7,19,17] subgroup2_member(multiply(u,multiply(A,multiply(inverse(u),inverse(A))))).
% 1764 [hyper,466,3,172,14,demod,188] product(inverse(A),inverse(B),inverse(multiply(B,A))).
% 4171 [hyper,129,5,20,21] subgroup1_member(multiply(A,multiply(multiply(v,inverse(A)),inverse(v)))).
% 4369,4368 [hyper,129,1,17] equal(multiply(multiply(A,B),C),multiply(A,multiply(B,C))).
% 4397 [back_demod,4171,demod,4369] subgroup1_member(multiply(A,multiply(v,multiply(inverse(A),inverse(v))))).
% 6634,6633 [hyper,1764,1,17,flip.1] equal(inverse(multiply(A,B)),multiply(inverse(B),inverse(A))).
% 7696 [hyper,4397,191,835] product(u,multiply(v,multiply(inverse(u),inverse(v))),identity).
% 8405 [hyper,7696,2,149,17,demod,6634,306,306,190] product(u,v,multiply(v,u)).
% 8455 [hyper,8405,1,17,flip.1] equal(multiply(v,u),multiply(u,v)).
% 8457 [binary,8455.1,11.1] $F.
% 
% ------------ end of proof -------------
% 
% 
% Search stopped by max_proofs option.
% 
% 
% Search stopped by max_proofs option.
% 
% ============ end of search ============
% 
% -------------- statistics -------------
% clauses given                263
% clauses generated          23018
% clauses kept                8421
% clauses forward subsumed   20076
% clauses back subsumed        138
% Kbytes malloced             3959
% 
% ----------- times (seconds) -----------
% user CPU time          7.46          (0 hr, 0 min, 7 sec)
% system CPU time        0.05          (0 hr, 0 min, 0 sec)
% wall-clock time        8             (0 hr, 0 min, 8 sec)
% hyper_res time         0.00
% para_into time         0.00
% para_from time         0.00
% for_sub time           0.00
% back_sub time          0.00
% conflict time          0.00
% demod time             0.00
% 
% That finishes the proof of the theorem.
% 
% Process 29767 finished Wed Sep 25 00:34:01 2002
% PROOF FOUND
%------------------------------------------------------------------------------