%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : GRP130-4.003 : TPTP v3.4.2. Bugfixed v1.2.1.
% 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:27:46 EDT 2009
% Result : Unsatisfiable 1.0s
% Output : Refutation 1.0s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 12
% Syntax : Number of formulae : 60 ( 21 unt; 0 def)
% Number of atoms : 117 ( 0 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 125 ( 68 ~; 57 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 66 ( 6 sgn 22 !; 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/GRP130-4.003.tptp',unknown),
[] ).
cnf(153853320,plain,
group_element(e_1),
inference(rewrite,[status(thm)],[element_1]),
[] ).
fof(element_3,plain,
group_element(e_3),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),
[] ).
cnf(153864976,plain,
group_element(e_3),
inference(rewrite,[status(thm)],[element_3]),
[] ).
fof(row_surjectivity,plain,
! [A,B] :
( ~ group_element(A)
| ~ group_element(B)
| product(e_1,A,B)
| product(e_2,A,B)
| product(e_3,A,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),
[] ).
cnf(153829280,plain,
( ~ group_element(A)
| ~ group_element(B)
| product(e_1,A,B)
| product(e_2,A,B)
| product(e_3,A,B) ),
inference(rewrite,[status(thm)],[row_surjectivity]),
[] ).
fof(qg3_1,plain,
! [A,B,C,D] :
( product(A,B,C)
| ~ product(D,B,A)
| ~ product(A,C,D) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),
[] ).
cnf(153844832,plain,
( product(A,B,C)
| ~ product(D,B,A)
| ~ product(A,C,D) ),
inference(rewrite,[status(thm)],[qg3_1]),
[] ).
cnf(167493024,plain,
( ~ product(C,B,A)
| ~ product(A,A,C)
| product(A,B,B) ),
inference(resolution,[status(thm)],[153844832,153844832]),
[] ).
fof(qg3_2,plain,
! [A,B,C,D] :
( product(A,B,C)
| ~ product(C,D,A)
| ~ product(A,D,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),
[] ).
cnf(153849152,plain,
( product(A,B,C)
| ~ product(C,D,A)
| ~ product(A,D,B) ),
inference(rewrite,[status(thm)],[qg3_2]),
[] ).
cnf(167993280,plain,
( product(A,A,A)
| ~ product(A,B,A) ),
inference(resolution,[status(thm)],[167493024,153849152]),
[] ).
fof(product_right_cancellation,plain,
! [A,B,C,D] :
( ~ product(A,B,C)
| ~ product(A,D,C)
| equalish(B,D) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),
[] ).
cnf(153915600,plain,
( ~ product(A,B,C)
| ~ product(A,D,C)
| equalish(B,D) ),
inference(rewrite,[status(thm)],[product_right_cancellation]),
[] ).
fof(e_1_is_not_e_3,plain,
~ equalish(e_1,e_3),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),
[] ).
cnf(153873248,plain,
~ equalish(e_1,e_3),
inference(rewrite,[status(thm)],[e_1_is_not_e_3]),
[] ).
cnf(167302464,plain,
( ~ product(A,e_1,B)
| ~ product(A,e_3,B) ),
inference(resolution,[status(thm)],[153915600,153873248]),
[] ).
cnf(168163664,plain,
( ~ product(e_1,A,e_1)
| ~ product(e_1,e_3,e_1) ),
inference(resolution,[status(thm)],[167993280,167302464]),
[] ).
cnf(170471200,plain,
( product(e_2,e_3,e_1)
| product(e_3,e_3,e_1) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[153853320,153864976,153829280,168163664]),
[] ).
cnf(171539672,plain,
( product(e_3,e_3,e_1)
| ~ product(e_2,e_1,e_1) ),
inference(resolution,[status(thm)],[170471200,167302464]),
[] ).
fof(element_2,plain,
group_element(e_2),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),
[] ).
cnf(153861288,plain,
group_element(e_2),
inference(rewrite,[status(thm)],[element_2]),
[] ).
fof(e_1_is_not_e_2,plain,
~ equalish(e_1,e_2),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),
[] ).
cnf(153869328,plain,
~ equalish(e_1,e_2),
inference(rewrite,[status(thm)],[e_1_is_not_e_2]),
[] ).
cnf(167243200,plain,
( ~ product(A,e_1,B)
| ~ product(A,e_2,B) ),
inference(resolution,[status(thm)],[153915600,153869328]),
[] ).
cnf(168068952,plain,
( ~ product(e_1,A,e_1)
| ~ product(e_1,e_2,e_1) ),
inference(resolution,[status(thm)],[167993280,167243200]),
[] ).
cnf(170390360,plain,
( product(e_2,e_2,e_1)
| product(e_3,e_2,e_1) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[153853320,153861288,153829280,168068952]),
[] ).
cnf(170927944,plain,
( product(e_3,e_2,e_1)
| ~ product(e_2,e_1,e_1) ),
inference(resolution,[status(thm)],[170390360,167243200]),
[] ).
fof(e_2_is_not_e_3,plain,
~ equalish(e_2,e_3),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),
[] ).
cnf(153880592,plain,
~ equalish(e_2,e_3),
inference(rewrite,[status(thm)],[e_2_is_not_e_3]),
[] ).
cnf(167308480,plain,
( ~ product(A,e_2,B)
| ~ product(A,e_3,B) ),
inference(resolution,[status(thm)],[153915600,153880592]),
[] ).
cnf(173791432,plain,
~ product(e_2,e_1,e_1),
inference(forward_subsumption_resolution__resolution,[status(thm)],[171539672,170927944,167308480]),
[] ).
cnf(166978752,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_1,e_1)
| product(e_3,e_1,e_1) ),
inference(resolution,[status(thm)],[153829280,153853320]),
[] ).
cnf(173879456,plain,
( product(e_1,e_1,e_1)
| product(e_3,e_1,e_1) ),
inference(resolution,[status(thm)],[173791432,166978752]),
[] ).
fof(product_total_function2,plain,
! [A,B,C,D] :
( ~ product(A,B,C)
| ~ product(A,B,D)
| equalish(C,D) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),
[] ).
cnf(153911456,plain,
( ~ product(A,B,C)
| ~ product(A,B,D)
| equalish(C,D) ),
inference(rewrite,[status(thm)],[product_total_function2]),
[] ).
cnf(167228568,plain,
( ~ product(A,B,e_1)
| ~ product(A,B,e_2) ),
inference(resolution,[status(thm)],[153911456,153869328]),
[] ).
cnf(173934720,plain,
( product(e_3,e_1,e_1)
| ~ product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[173879456,167228568]),
[] ).
cnf(170931648,plain,
( product(e_2,e_2,e_1)
| ~ product(e_3,e_1,e_1) ),
inference(resolution,[status(thm)],[170390360,167243200]),
[] ).
cnf(168431848,plain,
( ~ product(A,e_2,e_1)
| ~ product(e_1,e_1,A) ),
inference(resolution,[status(thm)],[168068952,153844832]),
[] ).
cnf(174207552,plain,
~ product(e_1,e_1,e_2),
inference(forward_subsumption_resolution__resolution,[status(thm)],[173934720,170931648,168431848]),
[] ).
cnf(168076680,plain,
( ~ product(e_2,A,e_2)
| ~ product(e_2,e_1,e_2) ),
inference(resolution,[status(thm)],[167993280,167243200]),
[] ).
cnf(170398680,plain,
( product(e_1,e_1,e_2)
| product(e_3,e_1,e_2) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[153853320,153861288,153829280,168076680]),
[] ).
cnf(174435552,plain,
product(e_3,e_1,e_2),
inference(resolution,[status(thm)],[174207552,170398680]),
[] ).
cnf(174485776,plain,
~ product(e_3,e_3,e_2),
inference(resolution,[status(thm)],[174435552,167302464]),
[] ).
cnf(168189760,plain,
( ~ product(e_2,A,e_2)
| ~ product(e_2,e_3,e_2) ),
inference(resolution,[status(thm)],[167993280,167308480]),
[] ).
cnf(170491688,plain,
( product(e_1,e_3,e_2)
| product(e_3,e_3,e_2) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[153861288,153864976,153829280,168189760]),
[] ).
cnf(174875128,plain,
product(e_1,e_3,e_2),
inference(resolution,[status(thm)],[174485776,170491688]),
[] ).
fof(qg3,plain,
! [A,B,C,D] :
( ~ product(A,B,C)
| ~ product(A,C,D)
| product(D,B,A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),
[] ).
cnf(153923760,plain,
( ~ product(A,B,C)
| ~ product(A,C,D)
| product(D,B,A) ),
inference(rewrite,[status(thm)],[qg3]),
[] ).
cnf(175044064,plain,
( ~ product(e_1,A,e_3)
| product(e_2,A,e_1) ),
inference(resolution,[status(thm)],[174875128,153923760]),
[] ).
cnf(171547576,plain,
( product(e_3,e_3,e_1)
| ~ product(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[170471200,167308480]),
[] ).
cnf(168202424,plain,
( ~ product(e_3,A,e_3)
| ~ product(e_3,e_2,e_3) ),
inference(resolution,[status(thm)],[167993280,167308480]),
[] ).
cnf(168764720,plain,
( ~ product(A,e_2,e_3)
| ~ product(e_3,e_3,A) ),
inference(resolution,[status(thm)],[168202424,153844832]),
[] ).
cnf(192404472,plain,
~ product(e_1,e_2,e_3),
inference(forward_subsumption_resolution__resolution,[status(thm)],[175044064,171547576,168764720]),
[] ).
cnf(168450184,plain,
( ~ product(A,e_1,e_2)
| ~ product(e_2,e_2,A) ),
inference(resolution,[status(thm)],[168076680,153844832]),
[] ).
cnf(174581416,plain,
~ product(e_2,e_2,e_3),
inference(resolution,[status(thm)],[174435552,168450184]),
[] ).
cnf(170499936,plain,
( product(e_1,e_2,e_3)
| product(e_2,e_2,e_3) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[153861288,153864976,153829280,168202424]),
[] ).
cnf(175087104,plain,
product(e_1,e_2,e_3),
inference(resolution,[status(thm)],[174581416,170499936]),
[] ).
cnf(contradiction,plain,
$false,
inference(resolution,[status(thm)],[192404472,175087104]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 1 seconds
% START OF PROOF SEQUENCE
% fof(element_1,plain,(group_element(e_1)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),[]).
%
% cnf(153853320,plain,(group_element(e_1)),inference(rewrite,[status(thm)],[element_1]),[]).
%
% fof(element_3,plain,(group_element(e_3)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),[]).
%
% cnf(153864976,plain,(group_element(e_3)),inference(rewrite,[status(thm)],[element_3]),[]).
%
% fof(row_surjectivity,plain,(~group_element(A)|~group_element(B)|product(e_1,A,B)|product(e_2,A,B)|product(e_3,A,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),[]).
%
% cnf(153829280,plain,(~group_element(A)|~group_element(B)|product(e_1,A,B)|product(e_2,A,B)|product(e_3,A,B)),inference(rewrite,[status(thm)],[row_surjectivity]),[]).
%
% fof(qg3_1,plain,(product(A,B,C)|~product(D,B,A)|~product(A,C,D)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),[]).
%
% cnf(153844832,plain,(product(A,B,C)|~product(D,B,A)|~product(A,C,D)),inference(rewrite,[status(thm)],[qg3_1]),[]).
%
% cnf(167493024,plain,(~product(C,B,A)|~product(A,A,C)|product(A,B,B)),inference(resolution,[status(thm)],[153844832,153844832]),[]).
%
% fof(qg3_2,plain,(product(A,B,C)|~product(C,D,A)|~product(A,D,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),[]).
%
% cnf(153849152,plain,(product(A,B,C)|~product(C,D,A)|~product(A,D,B)),inference(rewrite,[status(thm)],[qg3_2]),[]).
%
% cnf(167993280,plain,(product(A,A,A)|~product(A,B,A)),inference(resolution,[status(thm)],[167493024,153849152]),[]).
%
% fof(product_right_cancellation,plain,(~product(A,B,C)|~product(A,D,C)|equalish(B,D)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),[]).
%
% cnf(153915600,plain,(~product(A,B,C)|~product(A,D,C)|equalish(B,D)),inference(rewrite,[status(thm)],[product_right_cancellation]),[]).
%
% fof(e_1_is_not_e_3,plain,(~equalish(e_1,e_3)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),[]).
%
% cnf(153873248,plain,(~equalish(e_1,e_3)),inference(rewrite,[status(thm)],[e_1_is_not_e_3]),[]).
%
% cnf(167302464,plain,(~product(A,e_1,B)|~product(A,e_3,B)),inference(resolution,[status(thm)],[153915600,153873248]),[]).
%
% cnf(168163664,plain,(~product(e_1,A,e_1)|~product(e_1,e_3,e_1)),inference(resolution,[status(thm)],[167993280,167302464]),[]).
%
% cnf(170471200,plain,(product(e_2,e_3,e_1)|product(e_3,e_3,e_1)),inference(forward_subsumption_resolution__resolution,[status(thm)],[153853320,153864976,153829280,168163664]),[]).
%
% cnf(171539672,plain,(product(e_3,e_3,e_1)|~product(e_2,e_1,e_1)),inference(resolution,[status(thm)],[170471200,167302464]),[]).
%
% fof(element_2,plain,(group_element(e_2)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),[]).
%
% cnf(153861288,plain,(group_element(e_2)),inference(rewrite,[status(thm)],[element_2]),[]).
%
% fof(e_1_is_not_e_2,plain,(~equalish(e_1,e_2)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),[]).
%
% cnf(153869328,plain,(~equalish(e_1,e_2)),inference(rewrite,[status(thm)],[e_1_is_not_e_2]),[]).
%
% cnf(167243200,plain,(~product(A,e_1,B)|~product(A,e_2,B)),inference(resolution,[status(thm)],[153915600,153869328]),[]).
%
% cnf(168068952,plain,(~product(e_1,A,e_1)|~product(e_1,e_2,e_1)),inference(resolution,[status(thm)],[167993280,167243200]),[]).
%
% cnf(170390360,plain,(product(e_2,e_2,e_1)|product(e_3,e_2,e_1)),inference(forward_subsumption_resolution__resolution,[status(thm)],[153853320,153861288,153829280,168068952]),[]).
%
% cnf(170927944,plain,(product(e_3,e_2,e_1)|~product(e_2,e_1,e_1)),inference(resolution,[status(thm)],[170390360,167243200]),[]).
%
% fof(e_2_is_not_e_3,plain,(~equalish(e_2,e_3)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),[]).
%
% cnf(153880592,plain,(~equalish(e_2,e_3)),inference(rewrite,[status(thm)],[e_2_is_not_e_3]),[]).
%
% cnf(167308480,plain,(~product(A,e_2,B)|~product(A,e_3,B)),inference(resolution,[status(thm)],[153915600,153880592]),[]).
%
% cnf(173791432,plain,(~product(e_2,e_1,e_1)),inference(forward_subsumption_resolution__resolution,[status(thm)],[171539672,170927944,167308480]),[]).
%
% cnf(166978752,plain,(product(e_1,e_1,e_1)|product(e_2,e_1,e_1)|product(e_3,e_1,e_1)),inference(resolution,[status(thm)],[153829280,153853320]),[]).
%
% cnf(173879456,plain,(product(e_1,e_1,e_1)|product(e_3,e_1,e_1)),inference(resolution,[status(thm)],[173791432,166978752]),[]).
%
% fof(product_total_function2,plain,(~product(A,B,C)|~product(A,B,D)|equalish(C,D)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),[]).
%
% cnf(153911456,plain,(~product(A,B,C)|~product(A,B,D)|equalish(C,D)),inference(rewrite,[status(thm)],[product_total_function2]),[]).
%
% cnf(167228568,plain,(~product(A,B,e_1)|~product(A,B,e_2)),inference(resolution,[status(thm)],[153911456,153869328]),[]).
%
% cnf(173934720,plain,(product(e_3,e_1,e_1)|~product(e_1,e_1,e_2)),inference(resolution,[status(thm)],[173879456,167228568]),[]).
%
% cnf(170931648,plain,(product(e_2,e_2,e_1)|~product(e_3,e_1,e_1)),inference(resolution,[status(thm)],[170390360,167243200]),[]).
%
% cnf(168431848,plain,(~product(A,e_2,e_1)|~product(e_1,e_1,A)),inference(resolution,[status(thm)],[168068952,153844832]),[]).
%
% cnf(174207552,plain,(~product(e_1,e_1,e_2)),inference(forward_subsumption_resolution__resolution,[status(thm)],[173934720,170931648,168431848]),[]).
%
% cnf(168076680,plain,(~product(e_2,A,e_2)|~product(e_2,e_1,e_2)),inference(resolution,[status(thm)],[167993280,167243200]),[]).
%
% cnf(170398680,plain,(product(e_1,e_1,e_2)|product(e_3,e_1,e_2)),inference(forward_subsumption_resolution__resolution,[status(thm)],[153853320,153861288,153829280,168076680]),[]).
%
% cnf(174435552,plain,(product(e_3,e_1,e_2)),inference(resolution,[status(thm)],[174207552,170398680]),[]).
%
% cnf(174485776,plain,(~product(e_3,e_3,e_2)),inference(resolution,[status(thm)],[174435552,167302464]),[]).
%
% cnf(168189760,plain,(~product(e_2,A,e_2)|~product(e_2,e_3,e_2)),inference(resolution,[status(thm)],[167993280,167308480]),[]).
%
% cnf(170491688,plain,(product(e_1,e_3,e_2)|product(e_3,e_3,e_2)),inference(forward_subsumption_resolution__resolution,[status(thm)],[153861288,153864976,153829280,168189760]),[]).
%
% cnf(174875128,plain,(product(e_1,e_3,e_2)),inference(resolution,[status(thm)],[174485776,170491688]),[]).
%
% fof(qg3,plain,(~product(A,B,C)|~product(A,C,D)|product(D,B,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRP/GRP130-4.003.tptp',unknown),[]).
%
% cnf(153923760,plain,(~product(A,B,C)|~product(A,C,D)|product(D,B,A)),inference(rewrite,[status(thm)],[qg3]),[]).
%
% cnf(175044064,plain,(~product(e_1,A,e_3)|product(e_2,A,e_1)),inference(resolution,[status(thm)],[174875128,153923760]),[]).
%
% cnf(171547576,plain,(product(e_3,e_3,e_1)|~product(e_2,e_2,e_1)),inference(resolution,[status(thm)],[170471200,167308480]),[]).
%
% cnf(168202424,plain,(~product(e_3,A,e_3)|~product(e_3,e_2,e_3)),inference(resolution,[status(thm)],[167993280,167308480]),[]).
%
% cnf(168764720,plain,(~product(A,e_2,e_3)|~product(e_3,e_3,A)),inference(resolution,[status(thm)],[168202424,153844832]),[]).
%
% cnf(192404472,plain,(~product(e_1,e_2,e_3)),inference(forward_subsumption_resolution__resolution,[status(thm)],[175044064,171547576,168764720]),[]).
%
% cnf(168450184,plain,(~product(A,e_1,e_2)|~product(e_2,e_2,A)),inference(resolution,[status(thm)],[168076680,153844832]),[]).
%
% cnf(174581416,plain,(~product(e_2,e_2,e_3)),inference(resolution,[status(thm)],[174435552,168450184]),[]).
%
% cnf(170499936,plain,(product(e_1,e_2,e_3)|product(e_2,e_2,e_3)),inference(forward_subsumption_resolution__resolution,[status(thm)],[153861288,153864976,153829280,168202424]),[]).
%
% cnf(175087104,plain,(product(e_1,e_2,e_3)),inference(resolution,[status(thm)],[174581416,170499936]),[]).
%
% cnf(contradiction,plain,$false,inference(resolution,[status(thm)],[192404472,175087104]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------