%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : KRS090+1 : TPTP v3.4.2. Released v3.1.0.
% Transfm : none
% Format : tptp
% Command : faust %s
% Computer : art05.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:26:54 EDT 2009
% Result : Unsatisfiable 0.1s
% Output : Refutation 0.1s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 6
% Syntax : Number of formulae : 25 ( 10 unt; 0 def)
% Number of atoms : 60 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 64 ( 29 ~; 30 |; 5 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-2 aty)
% Number of functors : 2 ( 2 usr; 1 con; 0-1 aty)
% Number of variables : 16 ( 0 sgn 6 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(axiom_3,plain,
! [A] :
( ( cb(A)
| ca(A)
| ~ cc2(A) )
& ( ~ cb(A)
| ca(A)
| ~ cc2(A) ) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS090+1.tptp',unknown),
[] ).
cnf(167044760,plain,
( cb(A)
| ca(A)
| ~ cc2(A) ),
inference(rewrite,[status(thm)],[axiom_3]),
[] ).
fof(axiom_5,plain,
! [A] :
( ( cc2(y(A))
| ~ cc4(A) )
& ( rr(A,y(A))
| ~ cc4(A) ) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS090+1.tptp',unknown),
[] ).
cnf(167090720,plain,
( cc2(y(A))
| ~ cc4(A) ),
inference(rewrite,[status(thm)],[axiom_5]),
[] ).
fof(axiom_7,plain,
! [A] :
( ( cc1(A)
| ~ ctest(A) )
& ( cc5(A)
| ~ ctest(A) )
& ( cc4(A)
| ~ ctest(A) ) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS090+1.tptp',unknown),
[] ).
cnf(167118560,plain,
( cc4(A)
| ~ ctest(A) ),
inference(rewrite,[status(thm)],[axiom_7]),
[] ).
fof(axiom_8,plain,
ctest(i2003_11_14_17_19_57994),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS090+1.tptp',unknown),
[] ).
cnf(167155696,plain,
ctest(i2003_11_14_17_19_57994),
inference(rewrite,[status(thm)],[axiom_8]),
[] ).
cnf(172782008,plain,
cc4(i2003_11_14_17_19_57994),
inference(resolution,[status(thm)],[167118560,167155696]),
[] ).
cnf(172829240,plain,
cc2(y(i2003_11_14_17_19_57994)),
inference(resolution,[status(thm)],[167090720,172782008]),
[] ).
cnf(173513784,plain,
( cb(y(i2003_11_14_17_19_57994))
| ca(y(i2003_11_14_17_19_57994)) ),
inference(resolution,[status(thm)],[167044760,172829240]),
[] ).
cnf(167027680,plain,
( ~ cb(A)
| ca(A)
| ~ cc2(A) ),
inference(rewrite,[status(thm)],[axiom_3]),
[] ).
cnf(173525968,plain,
ca(y(i2003_11_14_17_19_57994)),
inference(forward_subsumption_resolution__resolution,[status(thm)],[173513784,167027680,172829240]),
[] ).
fof(axiom_4,plain,
! [A] :
( ( cb(A)
| ~ ca(A)
| ~ cc3(A) )
& ( ~ cb(A)
| ~ ca(A)
| ~ cc3(A) ) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS090+1.tptp',unknown),
[] ).
cnf(167069640,plain,
( cb(A)
| ~ ca(A)
| ~ cc3(A) ),
inference(rewrite,[status(thm)],[axiom_4]),
[] ).
cnf(167131488,plain,
( cc5(A)
| ~ ctest(A) ),
inference(rewrite,[status(thm)],[axiom_7]),
[] ).
cnf(172796216,plain,
cc5(i2003_11_14_17_19_57994),
inference(resolution,[status(thm)],[167131488,167155696]),
[] ).
fof(axiom_6,plain,
! [A,B] :
( ~ cc5(A)
| ~ rr(A,B)
| cc3(B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS090+1.tptp',unknown),
[] ).
cnf(167105488,plain,
( ~ cc5(A)
| ~ rr(A,B)
| cc3(B) ),
inference(rewrite,[status(thm)],[axiom_6]),
[] ).
cnf(167077648,plain,
( rr(A,y(A))
| ~ cc4(A) ),
inference(rewrite,[status(thm)],[axiom_5]),
[] ).
cnf(172846200,plain,
rr(i2003_11_14_17_19_57994,y(i2003_11_14_17_19_57994)),
inference(resolution,[status(thm)],[167077648,172782008]),
[] ).
cnf(173571696,plain,
cc3(y(i2003_11_14_17_19_57994)),
inference(forward_subsumption_resolution__resolution,[status(thm)],[172796216,167105488,172846200]),
[] ).
cnf(173581320,plain,
cb(y(i2003_11_14_17_19_57994)),
inference(forward_subsumption_resolution__resolution,[status(thm)],[173513784,167069640,173571696]),
[] ).
cnf(167056424,plain,
( ~ cb(A)
| ~ ca(A)
| ~ cc3(A) ),
inference(rewrite,[status(thm)],[axiom_4]),
[] ).
cnf(contradiction,plain,
$false,
inference(forward_subsumption_resolution__resolution,[status(thm)],[173525968,173581320,167056424,173571696]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 0 seconds
% START OF PROOF SEQUENCE
% fof(axiom_3,plain,(((cb(A)|ca(A)|~cc2(A))&(~cb(A)|ca(A)|~cc2(A)))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS090+1.tptp',unknown),[]).
%
% cnf(167044760,plain,(cb(A)|ca(A)|~cc2(A)),inference(rewrite,[status(thm)],[axiom_3]),[]).
%
% fof(axiom_5,plain,(((cc2(y(A))|~cc4(A))&(rr(A,y(A))|~cc4(A)))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS090+1.tptp',unknown),[]).
%
% cnf(167090720,plain,(cc2(y(A))|~cc4(A)),inference(rewrite,[status(thm)],[axiom_5]),[]).
%
% fof(axiom_7,plain,(((cc1(A)|~ctest(A))&(cc5(A)|~ctest(A))&(cc4(A)|~ctest(A)))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS090+1.tptp',unknown),[]).
%
% cnf(167118560,plain,(cc4(A)|~ctest(A)),inference(rewrite,[status(thm)],[axiom_7]),[]).
%
% fof(axiom_8,plain,(ctest(i2003_11_14_17_19_57994)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS090+1.tptp',unknown),[]).
%
% cnf(167155696,plain,(ctest(i2003_11_14_17_19_57994)),inference(rewrite,[status(thm)],[axiom_8]),[]).
%
% cnf(172782008,plain,(cc4(i2003_11_14_17_19_57994)),inference(resolution,[status(thm)],[167118560,167155696]),[]).
%
% cnf(172829240,plain,(cc2(y(i2003_11_14_17_19_57994))),inference(resolution,[status(thm)],[167090720,172782008]),[]).
%
% cnf(173513784,plain,(cb(y(i2003_11_14_17_19_57994))|ca(y(i2003_11_14_17_19_57994))),inference(resolution,[status(thm)],[167044760,172829240]),[]).
%
% cnf(167027680,plain,(~cb(A)|ca(A)|~cc2(A)),inference(rewrite,[status(thm)],[axiom_3]),[]).
%
% cnf(173525968,plain,(ca(y(i2003_11_14_17_19_57994))),inference(forward_subsumption_resolution__resolution,[status(thm)],[173513784,167027680,172829240]),[]).
%
% fof(axiom_4,plain,(((cb(A)|~ca(A)|~cc3(A))&(~cb(A)|~ca(A)|~cc3(A)))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS090+1.tptp',unknown),[]).
%
% cnf(167069640,plain,(cb(A)|~ca(A)|~cc3(A)),inference(rewrite,[status(thm)],[axiom_4]),[]).
%
% cnf(167131488,plain,(cc5(A)|~ctest(A)),inference(rewrite,[status(thm)],[axiom_7]),[]).
%
% cnf(172796216,plain,(cc5(i2003_11_14_17_19_57994)),inference(resolution,[status(thm)],[167131488,167155696]),[]).
%
% fof(axiom_6,plain,(~cc5(A)|~rr(A,B)|cc3(B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS090+1.tptp',unknown),[]).
%
% cnf(167105488,plain,(~cc5(A)|~rr(A,B)|cc3(B)),inference(rewrite,[status(thm)],[axiom_6]),[]).
%
% cnf(167077648,plain,(rr(A,y(A))|~cc4(A)),inference(rewrite,[status(thm)],[axiom_5]),[]).
%
% cnf(172846200,plain,(rr(i2003_11_14_17_19_57994,y(i2003_11_14_17_19_57994))),inference(resolution,[status(thm)],[167077648,172782008]),[]).
%
% cnf(173571696,plain,(cc3(y(i2003_11_14_17_19_57994))),inference(forward_subsumption_resolution__resolution,[status(thm)],[172796216,167105488,172846200]),[]).
%
% cnf(173581320,plain,(cb(y(i2003_11_14_17_19_57994))),inference(forward_subsumption_resolution__resolution,[status(thm)],[173513784,167069640,173571696]),[]).
%
% cnf(167056424,plain,(~cb(A)|~ca(A)|~cc3(A)),inference(rewrite,[status(thm)],[axiom_4]),[]).
%
% cnf(contradiction,plain,$false,inference(forward_subsumption_resolution__resolution,[status(thm)],[173525968,173581320,167056424,173571696]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------