%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : NUM014-1 : TPTP v3.4.2. Released v1.0.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 @ 2793MHz
% Memory : 1003MB
% OS : Linux 2.6.17-1.2142_FC4
% CPULimit : 600s
% DateTime : Wed May 6 14:50:28 EDT 2009
% Result : Unsatisfiable 0.0s
% Output : Refutation 0.0s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 6
% Syntax : Number of formulae : 17 ( 11 unt; 0 def)
% Number of atoms : 32 ( 0 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 30 ( 15 ~; 15 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-1 aty)
% Number of variables : 21 ( 1 sgn 8 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(divides,plain,
! [A,B,C] :
( ~ product(A,B,C)
| divides(A,C) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NUM/NUM014-1.tptp',unknown),
[] ).
cnf(173523528,plain,
( ~ product(A,B,C)
| divides(A,C) ),
inference(rewrite,[status(thm)],[divides]),
[] ).
fof(a_equals_b_squared_by_c_squared,plain,
product(a,square(c),square(b)),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NUM/NUM014-1.tptp',unknown),
[] ).
cnf(173509736,plain,
product(a,square(c),square(b)),
inference(rewrite,[status(thm)],[a_equals_b_squared_by_c_squared]),
[] ).
cnf(181523336,plain,
divides(a,square(b)),
inference(resolution,[status(thm)],[173523528,173509736]),
[] ).
fof(prove_a_divides_b,plain,
~ divides(a,b),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NUM/NUM014-1.tptp',unknown),
[] ).
cnf(173556736,plain,
~ divides(a,b),
inference(rewrite,[status(thm)],[prove_a_divides_b]),
[] ).
fof(remainder,plain,
! [A,B,C,D] :
( ~ prime(A)
| ~ product(B,C,D)
| ~ divides(A,D)
| divides(A,B)
| divides(A,C) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NUM/NUM014-1.tptp',unknown),
[] ).
cnf(173539448,plain,
( ~ prime(A)
| ~ product(B,C,D)
| ~ divides(A,D)
| divides(A,B)
| divides(A,C) ),
inference(rewrite,[status(thm)],[remainder]),
[] ).
fof(a_is_prime,plain,
prime(a),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NUM/NUM014-1.tptp',unknown),
[] ).
cnf(173543984,plain,
prime(a),
inference(rewrite,[status(thm)],[a_is_prime]),
[] ).
cnf(181350440,plain,
( ~ product(A,B,C)
| ~ divides(a,C)
| divides(a,A)
| divides(a,B) ),
inference(resolution,[status(thm)],[173539448,173543984]),
[] ).
cnf(181422664,plain,
( ~ product(A,b,B)
| ~ divides(a,B)
| divides(a,A) ),
inference(resolution,[status(thm)],[181350440,173556736]),
[] ).
fof(square,plain,
! [A] : product(A,A,square(A)),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NUM/NUM014-1.tptp',unknown),
[] ).
cnf(173512160,plain,
product(A,A,square(A)),
inference(rewrite,[status(thm)],[square]),
[] ).
cnf(181436864,plain,
~ divides(a,square(b)),
inference(forward_subsumption_resolution__resolution,[status(thm)],[173556736,181422664,173512160]),
[] ).
cnf(contradiction,plain,
$false,
inference(resolution,[status(thm)],[181523336,181436864]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 0 seconds
% START OF PROOF SEQUENCE
% fof(divides,plain,(~product(A,B,C)|divides(A,C)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NUM/NUM014-1.tptp',unknown),[]).
%
% cnf(173523528,plain,(~product(A,B,C)|divides(A,C)),inference(rewrite,[status(thm)],[divides]),[]).
%
% fof(a_equals_b_squared_by_c_squared,plain,(product(a,square(c),square(b))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NUM/NUM014-1.tptp',unknown),[]).
%
% cnf(173509736,plain,(product(a,square(c),square(b))),inference(rewrite,[status(thm)],[a_equals_b_squared_by_c_squared]),[]).
%
% cnf(181523336,plain,(divides(a,square(b))),inference(resolution,[status(thm)],[173523528,173509736]),[]).
%
% fof(prove_a_divides_b,plain,(~divides(a,b)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NUM/NUM014-1.tptp',unknown),[]).
%
% cnf(173556736,plain,(~divides(a,b)),inference(rewrite,[status(thm)],[prove_a_divides_b]),[]).
%
% fof(remainder,plain,(~prime(A)|~product(B,C,D)|~divides(A,D)|divides(A,B)|divides(A,C)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NUM/NUM014-1.tptp',unknown),[]).
%
% cnf(173539448,plain,(~prime(A)|~product(B,C,D)|~divides(A,D)|divides(A,B)|divides(A,C)),inference(rewrite,[status(thm)],[remainder]),[]).
%
% fof(a_is_prime,plain,(prime(a)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NUM/NUM014-1.tptp',unknown),[]).
%
% cnf(173543984,plain,(prime(a)),inference(rewrite,[status(thm)],[a_is_prime]),[]).
%
% cnf(181350440,plain,(~product(A,B,C)|~divides(a,C)|divides(a,A)|divides(a,B)),inference(resolution,[status(thm)],[173539448,173543984]),[]).
%
% cnf(181422664,plain,(~product(A,b,B)|~divides(a,B)|divides(a,A)),inference(resolution,[status(thm)],[181350440,173556736]),[]).
%
% fof(square,plain,(product(A,A,square(A))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NUM/NUM014-1.tptp',unknown),[]).
%
% cnf(173512160,plain,(product(A,A,square(A))),inference(rewrite,[status(thm)],[square]),[]).
%
% cnf(181436864,plain,(~divides(a,square(b))),inference(forward_subsumption_resolution__resolution,[status(thm)],[173556736,181422664,173512160]),[]).
%
% cnf(contradiction,plain,$false,inference(resolution,[status(thm)],[181523336,181436864]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------