%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : GRP124-8.004 : TPTP v3.4.2. Released v1.2.0.
% Transfm : none
% Format : tptp
% Command : faust %s
% Computer : art10.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2794MHz
% Memory : 1003MB
% OS : Linux 2.6.11-1.1369_FC4
% CPULimit : 600s
% DateTime : Wed May 6 12:25:43 EDT 2009
% Result : Unsatisfiable 7.1s
% Output : Refutation 7.1s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 21
% Syntax : Number of formulae : 85 ( 53 unt; 0 def)
% Number of atoms : 134 ( 0 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 138 ( 89 ~; 49 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 58 ( 0 sgn 20 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(element_1,plain,
group_element(e_1),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155196952,plain,
group_element(e_1),
inference(rewrite,[status(thm)],[element_1]),
[] ).
fof(element_2,plain,
group_element(e_2),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155201152,plain,
group_element(e_2),
inference(rewrite,[status(thm)],[element_2]),
[] ).
fof(product1_total_function1,plain,
! [A,B] :
( ~ group_element(A)
| ~ group_element(B)
| product1(A,B,e_1)
| product1(A,B,e_2)
| product1(A,B,e_3)
| product1(A,B,e_4) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155278112,plain,
( ~ group_element(A)
| ~ group_element(B)
| product1(A,B,e_1)
| product1(A,B,e_2)
| product1(A,B,e_3)
| product1(A,B,e_4) ),
inference(rewrite,[status(thm)],[product1_total_function1]),
[] ).
fof(product1_right_cancellation,plain,
! [A,B,C,D] :
( ~ product1(A,B,C)
| ~ product1(A,D,C)
| equalish(B,D) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155294992,plain,
( ~ product1(A,B,C)
| ~ product1(A,D,C)
| equalish(B,D) ),
inference(rewrite,[status(thm)],[product1_right_cancellation]),
[] ).
fof(product1_idempotence,plain,
! [A] : product1(A,A,A),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155303000,plain,
product1(A,A,A),
inference(rewrite,[status(thm)],[product1_idempotence]),
[] ).
cnf(165351592,plain,
( ~ product1(A,B,A)
| equalish(A,B) ),
inference(resolution,[status(thm)],[155294992,155303000]),
[] ).
fof(e_1_is_not_e_2,plain,
~ equalish(e_1,e_2),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155217016,plain,
~ equalish(e_1,e_2),
inference(rewrite,[status(thm)],[e_1_is_not_e_2]),
[] ).
cnf(165367584,plain,
~ product1(e_1,e_2,e_1),
inference(resolution,[status(thm)],[165351592,155217016]),
[] ).
cnf(193887512,plain,
( product1(e_1,e_2,e_2)
| product1(e_1,e_2,e_3)
| product1(e_1,e_2,e_4) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[155196952,155201152,155278112,165367584]),
[] ).
fof(product1_left_cancellation,plain,
! [A,B,C,D] :
( ~ product1(A,B,C)
| ~ product1(D,B,C)
| equalish(A,D) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155298624,plain,
( ~ product1(A,B,C)
| ~ product1(D,B,C)
| equalish(A,D) ),
inference(rewrite,[status(thm)],[product1_left_cancellation]),
[] ).
cnf(165597928,plain,
( ~ product1(B,A,A)
| equalish(A,B) ),
inference(resolution,[status(thm)],[155298624,155303000]),
[] ).
fof(e_2_is_not_e_1,plain,
~ equalish(e_2,e_1),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155228808,plain,
~ equalish(e_2,e_1),
inference(rewrite,[status(thm)],[e_2_is_not_e_1]),
[] ).
cnf(165647528,plain,
~ product1(e_1,e_2,e_2),
inference(resolution,[status(thm)],[165597928,155228808]),
[] ).
cnf(230624552,plain,
( product1(e_1,e_2,e_3)
| product1(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[193887512,165647528]),
[] ).
cnf(165401936,plain,
~ product1(e_2,e_1,e_2),
inference(resolution,[status(thm)],[165351592,155228808]),
[] ).
cnf(165613928,plain,
~ product1(e_2,e_1,e_1),
inference(resolution,[status(thm)],[165597928,155217016]),
[] ).
fof(e_3_is_not_e_1,plain,
~ equalish(e_3,e_1),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155244000,plain,
~ equalish(e_3,e_1),
inference(rewrite,[status(thm)],[e_3_is_not_e_1]),
[] ).
cnf(165690072,plain,
~ product1(e_1,e_3,e_3),
inference(resolution,[status(thm)],[165597928,155244000]),
[] ).
fof(e_1_is_not_e_3,plain,
~ equalish(e_1,e_3),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155221304,plain,
~ equalish(e_1,e_3),
inference(rewrite,[status(thm)],[e_1_is_not_e_3]),
[] ).
cnf(165379328,plain,
~ product1(e_1,e_3,e_1),
inference(resolution,[status(thm)],[165351592,155221304]),
[] ).
fof(element_3,plain,
group_element(e_3),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155204872,plain,
group_element(e_3),
inference(rewrite,[status(thm)],[element_3]),
[] ).
fof(qg2a,plain,
! [A,B,C,D] :
( ~ product1(A,B,C)
| ~ product1(C,A,D)
| product2(D,B,A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155343184,plain,
( ~ product1(A,B,C)
| ~ product1(C,A,D)
| product2(D,B,A) ),
inference(rewrite,[status(thm)],[qg2a]),
[] ).
fof(product2_total_function2,plain,
! [A,B,C,D] :
( ~ product2(A,B,C)
| ~ product2(A,B,D)
| equalish(C,D) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155325600,plain,
( ~ product2(A,B,C)
| ~ product2(A,B,D)
| equalish(C,D) ),
inference(rewrite,[status(thm)],[product2_total_function2]),
[] ).
cnf(164712368,plain,
( ~ product2(A,B,e_3)
| ~ product2(A,B,e_1) ),
inference(resolution,[status(thm)],[155325600,155244000]),
[] ).
fof(product2_idempotence,plain,
! [A] : product2(A,A,A),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155338016,plain,
product2(A,A,A),
inference(rewrite,[status(thm)],[product2_idempotence]),
[] ).
cnf(164803320,plain,
~ product2(e_3,e_3,e_1),
inference(resolution,[status(thm)],[164712368,155338016]),
[] ).
cnf(166389032,plain,
( ~ product1(e_1,e_3,A)
| ~ product1(A,e_1,e_3) ),
inference(resolution,[status(thm)],[155343184,164803320]),
[] ).
cnf(194417128,plain,
( product1(e_1,e_3,e_4)
| ~ product1(e_2,e_1,e_3) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[165690072,165379328,155204872,155196952,155278112,166389032]),
[] ).
cnf(164575784,plain,
( ~ product1(e_1,A,B)
| ~ product1(e_2,A,B) ),
inference(resolution,[status(thm)],[155298624,155217016]),
[] ).
cnf(196984168,plain,
( ~ product1(e_2,e_1,e_3)
| ~ product1(e_2,e_3,e_4) ),
inference(resolution,[status(thm)],[194417128,164575784]),
[] ).
cnf(202796360,plain,
( ~ product1(e_2,e_3,e_4)
| product1(e_2,e_1,e_4) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[165401936,165613928,155196952,155201152,196984168,155278112]),
[] ).
cnf(164684640,plain,
( ~ product1(A,e_3,B)
| ~ product1(A,e_1,B) ),
inference(resolution,[status(thm)],[155294992,155244000]),
[] ).
cnf(202849392,plain,
~ product1(e_2,e_3,e_4),
inference(resolution,[status(thm)],[202796360,164684640]),
[] ).
fof(e_3_is_not_e_2,plain,
~ equalish(e_3,e_2),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155247648,plain,
~ equalish(e_3,e_2),
inference(rewrite,[status(thm)],[e_3_is_not_e_2]),
[] ).
cnf(165703448,plain,
~ product1(e_2,e_3,e_3),
inference(resolution,[status(thm)],[165597928,155247648]),
[] ).
fof(e_2_is_not_e_3,plain,
~ equalish(e_2,e_3),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155232376,plain,
~ equalish(e_2,e_3),
inference(rewrite,[status(thm)],[e_2_is_not_e_3]),
[] ).
cnf(165416072,plain,
~ product1(e_2,e_3,e_2),
inference(resolution,[status(thm)],[165351592,155232376]),
[] ).
cnf(165830912,plain,
( ~ product2(A,A,B)
| equalish(A,B) ),
inference(resolution,[status(thm)],[155325600,155338016]),
[] ).
cnf(165895072,plain,
~ product2(e_3,e_3,e_2),
inference(resolution,[status(thm)],[165830912,155247648]),
[] ).
cnf(166578496,plain,
( ~ product1(e_2,e_3,A)
| ~ product1(A,e_2,e_3) ),
inference(resolution,[status(thm)],[155343184,165895072]),
[] ).
cnf(194474888,plain,
( product1(e_2,e_3,e_4)
| ~ product1(e_1,e_2,e_3) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[165703448,165416072,155201152,155204872,155278112,166578496]),
[] ).
cnf(203097104,plain,
~ product1(e_1,e_2,e_3),
inference(resolution,[status(thm)],[202849392,194474888]),
[] ).
cnf(231081744,plain,
product1(e_1,e_2,e_4),
inference(resolution,[status(thm)],[230624552,203097104]),
[] ).
fof(e_4_is_not_e_2,plain,
~ equalish(e_4,e_2),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155258808,plain,
~ equalish(e_4,e_2),
inference(rewrite,[status(thm)],[e_4_is_not_e_2]),
[] ).
cnf(165743576,plain,
~ product1(e_2,e_4,e_4),
inference(resolution,[status(thm)],[165597928,155258808]),
[] ).
fof(e_2_is_not_e_4,plain,
~ equalish(e_2,e_4),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155236136,plain,
~ equalish(e_2,e_4),
inference(rewrite,[status(thm)],[e_2_is_not_e_4]),
[] ).
cnf(165430240,plain,
~ product1(e_2,e_4,e_2),
inference(resolution,[status(thm)],[165351592,155236136]),
[] ).
fof(element_4,plain,
group_element(e_4),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155208456,plain,
group_element(e_4),
inference(rewrite,[status(thm)],[element_4]),
[] ).
cnf(165934720,plain,
~ product2(e_4,e_4,e_2),
inference(resolution,[status(thm)],[165830912,155258808]),
[] ).
cnf(166645320,plain,
( ~ product1(e_2,e_4,A)
| ~ product1(A,e_2,e_4) ),
inference(resolution,[status(thm)],[155343184,165934720]),
[] ).
cnf(194518504,plain,
( product1(e_2,e_4,e_3)
| ~ product1(e_1,e_2,e_4) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[165743576,165430240,155201152,155208456,155278112,166645320]),
[] ).
cnf(165334304,plain,
( ~ product1(A,e_2,B)
| ~ product1(A,e_3,B) ),
inference(resolution,[status(thm)],[155294992,155232376]),
[] ).
cnf(197001656,plain,
( ~ product1(e_2,e_1,e_3)
| ~ product1(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[194417128,165334304]),
[] ).
cnf(203837976,plain,
( ~ product1(e_1,e_2,e_4)
| product1(e_2,e_1,e_4) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[165401936,165613928,155201152,155196952,197001656,155278112]),
[] ).
fof(e_4_is_not_e_1,plain,
~ equalish(e_4,e_1),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155255160,plain,
~ equalish(e_4,e_1),
inference(rewrite,[status(thm)],[e_4_is_not_e_1]),
[] ).
cnf(165730200,plain,
~ product1(e_1,e_4,e_4),
inference(resolution,[status(thm)],[165597928,155255160]),
[] ).
fof(e_1_is_not_e_4,plain,
~ equalish(e_1,e_4),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),
[] ).
cnf(155225016,plain,
~ equalish(e_1,e_4),
inference(rewrite,[status(thm)],[e_1_is_not_e_4]),
[] ).
cnf(165393464,plain,
~ product1(e_1,e_4,e_1),
inference(resolution,[status(thm)],[165351592,155225016]),
[] ).
cnf(165922888,plain,
~ product2(e_4,e_4,e_1),
inference(resolution,[status(thm)],[165830912,155255160]),
[] ).
cnf(166626064,plain,
( ~ product1(e_1,e_4,A)
| ~ product1(A,e_1,e_4) ),
inference(resolution,[status(thm)],[155343184,165922888]),
[] ).
cnf(194508248,plain,
( product1(e_1,e_4,e_3)
| ~ product1(e_2,e_1,e_4) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[165730200,165393464,155208456,155196952,155278112,166626064]),
[] ).
cnf(185768128,plain,
( ~ product1(e_1,e_2,e_4)
| product1(e_1,e_4,e_3) ),
inference(resolution,[status(thm)],[203837976,194508248]),
[] ).
cnf(204217264,plain,
~ product1(e_1,e_2,e_4),
inference(forward_subsumption_resolution__resolution,[status(thm)],[194518504,185768128,164575784]),
[] ).
cnf(contradiction,plain,
$false,
inference(resolution,[status(thm)],[231081744,204217264]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 7 seconds
% START OF PROOF SEQUENCE
% fof(element_1,plain,(group_element(e_1)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155196952,plain,(group_element(e_1)),inference(rewrite,[status(thm)],[element_1]),[]).
%
% fof(element_2,plain,(group_element(e_2)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155201152,plain,(group_element(e_2)),inference(rewrite,[status(thm)],[element_2]),[]).
%
% fof(product1_total_function1,plain,(~group_element(A)|~group_element(B)|product1(A,B,e_1)|product1(A,B,e_2)|product1(A,B,e_3)|product1(A,B,e_4)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155278112,plain,(~group_element(A)|~group_element(B)|product1(A,B,e_1)|product1(A,B,e_2)|product1(A,B,e_3)|product1(A,B,e_4)),inference(rewrite,[status(thm)],[product1_total_function1]),[]).
%
% fof(product1_right_cancellation,plain,(~product1(A,B,C)|~product1(A,D,C)|equalish(B,D)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155294992,plain,(~product1(A,B,C)|~product1(A,D,C)|equalish(B,D)),inference(rewrite,[status(thm)],[product1_right_cancellation]),[]).
%
% fof(product1_idempotence,plain,(product1(A,A,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155303000,plain,(product1(A,A,A)),inference(rewrite,[status(thm)],[product1_idempotence]),[]).
%
% cnf(165351592,plain,(~product1(A,B,A)|equalish(A,B)),inference(resolution,[status(thm)],[155294992,155303000]),[]).
%
% fof(e_1_is_not_e_2,plain,(~equalish(e_1,e_2)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155217016,plain,(~equalish(e_1,e_2)),inference(rewrite,[status(thm)],[e_1_is_not_e_2]),[]).
%
% cnf(165367584,plain,(~product1(e_1,e_2,e_1)),inference(resolution,[status(thm)],[165351592,155217016]),[]).
%
% cnf(193887512,plain,(product1(e_1,e_2,e_2)|product1(e_1,e_2,e_3)|product1(e_1,e_2,e_4)),inference(forward_subsumption_resolution__resolution,[status(thm)],[155196952,155201152,155278112,165367584]),[]).
%
% fof(product1_left_cancellation,plain,(~product1(A,B,C)|~product1(D,B,C)|equalish(A,D)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155298624,plain,(~product1(A,B,C)|~product1(D,B,C)|equalish(A,D)),inference(rewrite,[status(thm)],[product1_left_cancellation]),[]).
%
% cnf(165597928,plain,(~product1(B,A,A)|equalish(A,B)),inference(resolution,[status(thm)],[155298624,155303000]),[]).
%
% fof(e_2_is_not_e_1,plain,(~equalish(e_2,e_1)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155228808,plain,(~equalish(e_2,e_1)),inference(rewrite,[status(thm)],[e_2_is_not_e_1]),[]).
%
% cnf(165647528,plain,(~product1(e_1,e_2,e_2)),inference(resolution,[status(thm)],[165597928,155228808]),[]).
%
% cnf(230624552,plain,(product1(e_1,e_2,e_3)|product1(e_1,e_2,e_4)),inference(resolution,[status(thm)],[193887512,165647528]),[]).
%
% cnf(165401936,plain,(~product1(e_2,e_1,e_2)),inference(resolution,[status(thm)],[165351592,155228808]),[]).
%
% cnf(165613928,plain,(~product1(e_2,e_1,e_1)),inference(resolution,[status(thm)],[165597928,155217016]),[]).
%
% fof(e_3_is_not_e_1,plain,(~equalish(e_3,e_1)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155244000,plain,(~equalish(e_3,e_1)),inference(rewrite,[status(thm)],[e_3_is_not_e_1]),[]).
%
% cnf(165690072,plain,(~product1(e_1,e_3,e_3)),inference(resolution,[status(thm)],[165597928,155244000]),[]).
%
% fof(e_1_is_not_e_3,plain,(~equalish(e_1,e_3)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155221304,plain,(~equalish(e_1,e_3)),inference(rewrite,[status(thm)],[e_1_is_not_e_3]),[]).
%
% cnf(165379328,plain,(~product1(e_1,e_3,e_1)),inference(resolution,[status(thm)],[165351592,155221304]),[]).
%
% fof(element_3,plain,(group_element(e_3)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155204872,plain,(group_element(e_3)),inference(rewrite,[status(thm)],[element_3]),[]).
%
% fof(qg2a,plain,(~product1(A,B,C)|~product1(C,A,D)|product2(D,B,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155343184,plain,(~product1(A,B,C)|~product1(C,A,D)|product2(D,B,A)),inference(rewrite,[status(thm)],[qg2a]),[]).
%
% fof(product2_total_function2,plain,(~product2(A,B,C)|~product2(A,B,D)|equalish(C,D)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155325600,plain,(~product2(A,B,C)|~product2(A,B,D)|equalish(C,D)),inference(rewrite,[status(thm)],[product2_total_function2]),[]).
%
% cnf(164712368,plain,(~product2(A,B,e_3)|~product2(A,B,e_1)),inference(resolution,[status(thm)],[155325600,155244000]),[]).
%
% fof(product2_idempotence,plain,(product2(A,A,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155338016,plain,(product2(A,A,A)),inference(rewrite,[status(thm)],[product2_idempotence]),[]).
%
% cnf(164803320,plain,(~product2(e_3,e_3,e_1)),inference(resolution,[status(thm)],[164712368,155338016]),[]).
%
% cnf(166389032,plain,(~product1(e_1,e_3,A)|~product1(A,e_1,e_3)),inference(resolution,[status(thm)],[155343184,164803320]),[]).
%
% cnf(194417128,plain,(product1(e_1,e_3,e_4)|~product1(e_2,e_1,e_3)),inference(forward_subsumption_resolution__resolution,[status(thm)],[165690072,165379328,155204872,155196952,155278112,166389032]),[]).
%
% cnf(164575784,plain,(~product1(e_1,A,B)|~product1(e_2,A,B)),inference(resolution,[status(thm)],[155298624,155217016]),[]).
%
% cnf(196984168,plain,(~product1(e_2,e_1,e_3)|~product1(e_2,e_3,e_4)),inference(resolution,[status(thm)],[194417128,164575784]),[]).
%
% cnf(202796360,plain,(~product1(e_2,e_3,e_4)|product1(e_2,e_1,e_4)),inference(forward_subsumption_resolution__resolution,[status(thm)],[165401936,165613928,155196952,155201152,196984168,155278112]),[]).
%
% cnf(164684640,plain,(~product1(A,e_3,B)|~product1(A,e_1,B)),inference(resolution,[status(thm)],[155294992,155244000]),[]).
%
% cnf(202849392,plain,(~product1(e_2,e_3,e_4)),inference(resolution,[status(thm)],[202796360,164684640]),[]).
%
% fof(e_3_is_not_e_2,plain,(~equalish(e_3,e_2)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155247648,plain,(~equalish(e_3,e_2)),inference(rewrite,[status(thm)],[e_3_is_not_e_2]),[]).
%
% cnf(165703448,plain,(~product1(e_2,e_3,e_3)),inference(resolution,[status(thm)],[165597928,155247648]),[]).
%
% fof(e_2_is_not_e_3,plain,(~equalish(e_2,e_3)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155232376,plain,(~equalish(e_2,e_3)),inference(rewrite,[status(thm)],[e_2_is_not_e_3]),[]).
%
% cnf(165416072,plain,(~product1(e_2,e_3,e_2)),inference(resolution,[status(thm)],[165351592,155232376]),[]).
%
% cnf(165830912,plain,(~product2(A,A,B)|equalish(A,B)),inference(resolution,[status(thm)],[155325600,155338016]),[]).
%
% cnf(165895072,plain,(~product2(e_3,e_3,e_2)),inference(resolution,[status(thm)],[165830912,155247648]),[]).
%
% cnf(166578496,plain,(~product1(e_2,e_3,A)|~product1(A,e_2,e_3)),inference(resolution,[status(thm)],[155343184,165895072]),[]).
%
% cnf(194474888,plain,(product1(e_2,e_3,e_4)|~product1(e_1,e_2,e_3)),inference(forward_subsumption_resolution__resolution,[status(thm)],[165703448,165416072,155201152,155204872,155278112,166578496]),[]).
%
% cnf(203097104,plain,(~product1(e_1,e_2,e_3)),inference(resolution,[status(thm)],[202849392,194474888]),[]).
%
% cnf(231081744,plain,(product1(e_1,e_2,e_4)),inference(resolution,[status(thm)],[230624552,203097104]),[]).
%
% fof(e_4_is_not_e_2,plain,(~equalish(e_4,e_2)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155258808,plain,(~equalish(e_4,e_2)),inference(rewrite,[status(thm)],[e_4_is_not_e_2]),[]).
%
% cnf(165743576,plain,(~product1(e_2,e_4,e_4)),inference(resolution,[status(thm)],[165597928,155258808]),[]).
%
% fof(e_2_is_not_e_4,plain,(~equalish(e_2,e_4)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155236136,plain,(~equalish(e_2,e_4)),inference(rewrite,[status(thm)],[e_2_is_not_e_4]),[]).
%
% cnf(165430240,plain,(~product1(e_2,e_4,e_2)),inference(resolution,[status(thm)],[165351592,155236136]),[]).
%
% fof(element_4,plain,(group_element(e_4)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155208456,plain,(group_element(e_4)),inference(rewrite,[status(thm)],[element_4]),[]).
%
% cnf(165934720,plain,(~product2(e_4,e_4,e_2)),inference(resolution,[status(thm)],[165830912,155258808]),[]).
%
% cnf(166645320,plain,(~product1(e_2,e_4,A)|~product1(A,e_2,e_4)),inference(resolution,[status(thm)],[155343184,165934720]),[]).
%
% cnf(194518504,plain,(product1(e_2,e_4,e_3)|~product1(e_1,e_2,e_4)),inference(forward_subsumption_resolution__resolution,[status(thm)],[165743576,165430240,155201152,155208456,155278112,166645320]),[]).
%
% cnf(165334304,plain,(~product1(A,e_2,B)|~product1(A,e_3,B)),inference(resolution,[status(thm)],[155294992,155232376]),[]).
%
% cnf(197001656,plain,(~product1(e_2,e_1,e_3)|~product1(e_1,e_2,e_4)),inference(resolution,[status(thm)],[194417128,165334304]),[]).
%
% cnf(203837976,plain,(~product1(e_1,e_2,e_4)|product1(e_2,e_1,e_4)),inference(forward_subsumption_resolution__resolution,[status(thm)],[165401936,165613928,155201152,155196952,197001656,155278112]),[]).
%
% fof(e_4_is_not_e_1,plain,(~equalish(e_4,e_1)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155255160,plain,(~equalish(e_4,e_1)),inference(rewrite,[status(thm)],[e_4_is_not_e_1]),[]).
%
% cnf(165730200,plain,(~product1(e_1,e_4,e_4)),inference(resolution,[status(thm)],[165597928,155255160]),[]).
%
% fof(e_1_is_not_e_4,plain,(~equalish(e_1,e_4)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP124-8.004.tptp',unknown),[]).
%
% cnf(155225016,plain,(~equalish(e_1,e_4)),inference(rewrite,[status(thm)],[e_1_is_not_e_4]),[]).
%
% cnf(165393464,plain,(~product1(e_1,e_4,e_1)),inference(resolution,[status(thm)],[165351592,155225016]),[]).
%
% cnf(165922888,plain,(~product2(e_4,e_4,e_1)),inference(resolution,[status(thm)],[165830912,155255160]),[]).
%
% cnf(166626064,plain,(~product1(e_1,e_4,A)|~product1(A,e_1,e_4)),inference(resolution,[status(thm)],[155343184,165922888]),[]).
%
% cnf(194508248,plain,(product1(e_1,e_4,e_3)|~product1(e_2,e_1,e_4)),inference(forward_subsumption_resolution__resolution,[status(thm)],[165730200,165393464,155208456,155196952,155278112,166626064]),[]).
%
% cnf(185768128,plain,(~product1(e_1,e_2,e_4)|product1(e_1,e_4,e_3)),inference(resolution,[status(thm)],[203837976,194508248]),[]).
%
% cnf(204217264,plain,(~product1(e_1,e_2,e_4)),inference(forward_subsumption_resolution__resolution,[status(thm)],[194518504,185768128,164575784]),[]).
%
% cnf(contradiction,plain,$false,inference(resolution,[status(thm)],[231081744,204217264]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------