%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : HEN005-2 : TPTP v3.4.2. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : faust %s
% Computer : art07.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 13:15:18 EDT 2009
% Result : Unsatisfiable 87.4s
% Output : Refutation 87.4s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 11
% Syntax : Number of formulae : 32 ( 19 unt; 0 def)
% Number of atoms : 70 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 79 ( 41 ~; 38 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 58 ( 2 sgn 19 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(closure,plain,
! [A,B] : quotient(A,B,divide(A,B)),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),
[] ).
cnf(174199992,plain,
quotient(A,B,divide(A,B)),
inference(rewrite,[status(thm)],[closure]),
[] ).
fof(zero_divide_anything_is_zero,plain,
! [A] : quotient(zero,A,zero),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),
[] ).
cnf(174212672,plain,
quotient(zero,A,zero),
inference(rewrite,[status(thm)],[zero_divide_anything_is_zero]),
[] ).
fof(less_equal_and_equal,plain,
! [A,B] :
( ~ less_equal(A,B)
| ~ less_equal(B,A)
| $equal(B,A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),
[] ).
cnf(174191400,plain,
( ~ less_equal(A,B)
| ~ less_equal(B,A)
| $equal(B,A) ),
inference(rewrite,[status(thm)],[less_equal_and_equal]),
[] ).
fof(quotient_property,plain,
! [A,B,C,D,E,F,G,H] :
( ~ quotient(A,B,C)
| ~ quotient(B,D,E)
| ~ quotient(A,D,F)
| ~ quotient(F,E,G)
| ~ quotient(C,D,H)
| less_equal(G,H) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),
[] ).
cnf(174173072,plain,
( ~ quotient(A,B,C)
| ~ quotient(B,D,E)
| ~ quotient(A,D,F)
| ~ quotient(F,E,G)
| ~ quotient(C,D,H)
| less_equal(G,H) ),
inference(rewrite,[status(thm)],[quotient_property]),
[] ).
cnf(190596808,plain,
( ~ less_equal(B,A)
| $equal(B,A)
| ~ quotient(C,D,E)
| ~ quotient(D,F,G)
| ~ quotient(C,F,H)
| ~ quotient(H,G,A)
| ~ quotient(E,F,B) ),
inference(resolution,[status(thm)],[174191400,174173072]),
[] ).
fof(x_divde_zero_is_x,plain,
! [A] : quotient(A,zero,A),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),
[] ).
cnf(174224360,plain,
quotient(A,zero,A),
inference(rewrite,[status(thm)],[x_divde_zero_is_x]),
[] ).
cnf(204193272,plain,
( ~ less_equal(B,A)
| $equal(B,A)
| ~ quotient(C,D,E)
| ~ quotient(D,F,zero)
| ~ quotient(C,F,A)
| ~ quotient(E,F,B) ),
inference(resolution,[status(thm)],[190596808,174224360]),
[] ).
fof(quotient_less_equal,plain,
! [A,B] :
( ~ less_equal(A,B)
| quotient(A,B,zero) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),
[] ).
cnf(174144952,plain,
( ~ less_equal(A,B)
| quotient(A,B,zero) ),
inference(rewrite,[status(thm)],[quotient_less_equal]),
[] ).
fof(xLEy,plain,
less_equal(x,y),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),
[] ).
cnf(174227864,plain,
less_equal(x,y),
inference(rewrite,[status(thm)],[xLEy]),
[] ).
cnf(182050704,plain,
quotient(x,y,zero),
inference(resolution,[status(thm)],[174144952,174227864]),
[] ).
cnf(233279560,plain,
( ~ less_equal(B,A)
| $equal(B,A)
| ~ quotient(y,C,zero)
| ~ quotient(x,C,A)
| ~ quotient(zero,C,B) ),
inference(resolution,[status(thm)],[204193272,182050704]),
[] ).
fof(yLEz,plain,
less_equal(y,z),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),
[] ).
cnf(174231656,plain,
less_equal(y,z),
inference(rewrite,[status(thm)],[yLEz]),
[] ).
cnf(182758600,plain,
quotient(y,z,zero),
inference(resolution,[status(thm)],[174144952,174231656]),
[] ).
cnf(234212536,plain,
( ~ less_equal(B,A)
| $equal(B,A)
| ~ quotient(x,z,A)
| ~ quotient(zero,z,B) ),
inference(resolution,[status(thm)],[233279560,182758600]),
[] ).
cnf(234332784,plain,
( ~ less_equal(A,divide(x,z))
| $equal(A,divide(x,z))
| ~ quotient(zero,z,A) ),
inference(resolution,[status(thm)],[234212536,174199992]),
[] ).
fof(zero_is_smallest,plain,
! [A] : less_equal(zero,A),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),
[] ).
cnf(174177512,plain,
less_equal(zero,A),
inference(rewrite,[status(thm)],[zero_is_smallest]),
[] ).
cnf(234381208,plain,
$equal(zero,divide(x,z)),
inference(forward_subsumption_resolution__resolution,[status(thm)],[174212672,234332784,174177512]),
[] ).
fof(less_equal_quotient,plain,
! [A,B] :
( ~ quotient(A,B,zero)
| less_equal(A,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),
[] ).
cnf(174155712,plain,
( ~ quotient(A,B,zero)
| less_equal(A,B) ),
inference(rewrite,[status(thm)],[less_equal_quotient]),
[] ).
fof(prove_transitivity_of_less_equal,plain,
~ less_equal(x,z),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),
[] ).
cnf(174235384,plain,
~ less_equal(x,z),
inference(rewrite,[status(thm)],[prove_transitivity_of_less_equal]),
[] ).
cnf(182576176,plain,
~ quotient(x,z,zero),
inference(resolution,[status(thm)],[174155712,174235384]),
[] ).
cnf(contradiction,plain,
$false,
inference(forward_subsumption_resolution__paramodulation,[status(thm)],[174199992,234381208,182576176,theory(equality)]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 87 seconds
% START OF PROOF SEQUENCE
% fof(closure,plain,(quotient(A,B,divide(A,B))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),[]).
%
% cnf(174199992,plain,(quotient(A,B,divide(A,B))),inference(rewrite,[status(thm)],[closure]),[]).
%
% fof(zero_divide_anything_is_zero,plain,(quotient(zero,A,zero)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),[]).
%
% cnf(174212672,plain,(quotient(zero,A,zero)),inference(rewrite,[status(thm)],[zero_divide_anything_is_zero]),[]).
%
% fof(less_equal_and_equal,plain,(~less_equal(A,B)|~less_equal(B,A)|$equal(B,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),[]).
%
% cnf(174191400,plain,(~less_equal(A,B)|~less_equal(B,A)|$equal(B,A)),inference(rewrite,[status(thm)],[less_equal_and_equal]),[]).
%
% fof(quotient_property,plain,(~quotient(A,B,C)|~quotient(B,D,E)|~quotient(A,D,F)|~quotient(F,E,G)|~quotient(C,D,H)|less_equal(G,H)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),[]).
%
% cnf(174173072,plain,(~quotient(A,B,C)|~quotient(B,D,E)|~quotient(A,D,F)|~quotient(F,E,G)|~quotient(C,D,H)|less_equal(G,H)),inference(rewrite,[status(thm)],[quotient_property]),[]).
%
% cnf(190596808,plain,(~less_equal(B,A)|$equal(B,A)|~quotient(C,D,E)|~quotient(D,F,G)|~quotient(C,F,H)|~quotient(H,G,A)|~quotient(E,F,B)),inference(resolution,[status(thm)],[174191400,174173072]),[]).
%
% fof(x_divde_zero_is_x,plain,(quotient(A,zero,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),[]).
%
% cnf(174224360,plain,(quotient(A,zero,A)),inference(rewrite,[status(thm)],[x_divde_zero_is_x]),[]).
%
% cnf(204193272,plain,(~less_equal(B,A)|$equal(B,A)|~quotient(C,D,E)|~quotient(D,F,zero)|~quotient(C,F,A)|~quotient(E,F,B)),inference(resolution,[status(thm)],[190596808,174224360]),[]).
%
% fof(quotient_less_equal,plain,(~less_equal(A,B)|quotient(A,B,zero)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),[]).
%
% cnf(174144952,plain,(~less_equal(A,B)|quotient(A,B,zero)),inference(rewrite,[status(thm)],[quotient_less_equal]),[]).
%
% fof(xLEy,plain,(less_equal(x,y)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),[]).
%
% cnf(174227864,plain,(less_equal(x,y)),inference(rewrite,[status(thm)],[xLEy]),[]).
%
% cnf(182050704,plain,(quotient(x,y,zero)),inference(resolution,[status(thm)],[174144952,174227864]),[]).
%
% cnf(233279560,plain,(~less_equal(B,A)|$equal(B,A)|~quotient(y,C,zero)|~quotient(x,C,A)|~quotient(zero,C,B)),inference(resolution,[status(thm)],[204193272,182050704]),[]).
%
% fof(yLEz,plain,(less_equal(y,z)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),[]).
%
% cnf(174231656,plain,(less_equal(y,z)),inference(rewrite,[status(thm)],[yLEz]),[]).
%
% cnf(182758600,plain,(quotient(y,z,zero)),inference(resolution,[status(thm)],[174144952,174231656]),[]).
%
% cnf(234212536,plain,(~less_equal(B,A)|$equal(B,A)|~quotient(x,z,A)|~quotient(zero,z,B)),inference(resolution,[status(thm)],[233279560,182758600]),[]).
%
% cnf(234332784,plain,(~less_equal(A,divide(x,z))|$equal(A,divide(x,z))|~quotient(zero,z,A)),inference(resolution,[status(thm)],[234212536,174199992]),[]).
%
% fof(zero_is_smallest,plain,(less_equal(zero,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),[]).
%
% cnf(174177512,plain,(less_equal(zero,A)),inference(rewrite,[status(thm)],[zero_is_smallest]),[]).
%
% cnf(234381208,plain,($equal(zero,divide(x,z))),inference(forward_subsumption_resolution__resolution,[status(thm)],[174212672,234332784,174177512]),[]).
%
% fof(less_equal_quotient,plain,(~quotient(A,B,zero)|less_equal(A,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),[]).
%
% cnf(174155712,plain,(~quotient(A,B,zero)|less_equal(A,B)),inference(rewrite,[status(thm)],[less_equal_quotient]),[]).
%
% fof(prove_transitivity_of_less_equal,plain,(~less_equal(x,z)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/HEN/HEN005-2.tptp',unknown),[]).
%
% cnf(174235384,plain,(~less_equal(x,z)),inference(rewrite,[status(thm)],[prove_transitivity_of_less_equal]),[]).
%
% cnf(182576176,plain,(~quotient(x,z,zero)),inference(resolution,[status(thm)],[174155712,174235384]),[]).
%
% cnf(contradiction,plain,$false,inference(forward_subsumption_resolution__paramodulation,[status(thm)],[174199992,234381208,182576176,theory(equality)]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------