%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : KRS128+1 : TPTP v3.4.2. Released v3.1.0.
% Transfm : none
% Format : tptp
% Command : faust %s
% Computer : art02.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 1003MB
% OS : Linux 2.6.11-1.1369_FC4
% CPULimit : 600s
% DateTime : Wed May 6 13:28:30 EDT 2009
% Result : Unsatisfiable 0.0s
% Output : Refutation 0.0s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 5
% Syntax : Number of formulae : 23 ( 9 unt; 0 def)
% Number of atoms : 77 ( 0 equ)
% Maximal formula atoms : 30 ( 3 avg)
% Number of connectives : 95 ( 41 ~; 43 |; 11 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-4 aty)
% Number of variables : 22 ( 2 sgn 9 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(axiom_2,plain,
! [A,C,D,E] :
( ( ~ rr(A,C)
| cd(C)
| ~ cunsatisfiable(A) )
& ( ~ rr(A,D)
| ca_cx4(D)
| ~ cunsatisfiable(A) )
& ( rr(A,y_nn_5(A))
| ~ cunsatisfiable(A) )
& ( cexcomp(y_nn_5(A))
| ~ cunsatisfiable(A) )
& ( ~ ca_cx4(y(A,C,D,E))
| rr(A,y_nn_1(A,C,D,E))
| ~ rr(A,E)
| ~ cexcomp(E)
| cunsatisfiable(A) )
& ( rr(A,y(A,C,D,E))
| rr(A,y_nn_1(A,C,D,E))
| ~ rr(A,E)
| ~ cexcomp(E)
| cunsatisfiable(A) )
& ( ~ ca_cx4(y(A,C,D,E))
| ~ cd(y_nn_1(A,C,D,E))
| ~ rr(A,E)
| ~ cexcomp(E)
| cunsatisfiable(A) )
& ( rr(A,y(A,C,D,E))
| ~ cd(y_nn_1(A,C,D,E))
| ~ rr(A,E)
| ~ cexcomp(E)
| cunsatisfiable(A) ) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS128+1.tptp',unknown),
[] ).
cnf(164646640,plain,
( ~ rr(A,D)
| ca_cx4(D)
| ~ cunsatisfiable(A) ),
inference(rewrite,[status(thm)],[axiom_2]),
[] ).
fof(axiom_11,plain,
cunsatisfiable(i2003_11_14_17_22_31584),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS128+1.tptp',unknown),
[] ).
cnf(164797408,plain,
cunsatisfiable(i2003_11_14_17_22_31584),
inference(rewrite,[status(thm)],[axiom_11]),
[] ).
cnf(170088960,plain,
( ~ rr(i2003_11_14_17_22_31584,C)
| ca_cx4(C) ),
inference(resolution,[status(thm)],[164646640,164797408]),
[] ).
cnf(164483024,plain,
( rr(A,y_nn_5(A))
| ~ cunsatisfiable(A) ),
inference(rewrite,[status(thm)],[axiom_2]),
[] ).
cnf(170068856,plain,
rr(i2003_11_14_17_22_31584,y_nn_5(i2003_11_14_17_22_31584)),
inference(resolution,[status(thm)],[164483024,164797408]),
[] ).
cnf(170238424,plain,
ca_cx4(y_nn_5(i2003_11_14_17_22_31584)),
inference(resolution,[status(thm)],[170088960,170068856]),
[] ).
fof(axiom_8,plain,
! [A,C] :
( ( ~ ca_cx4(A)
| ra_px4(A,y0_nn_1(A)) )
& ( ca_cx4(A)
| ~ ra_px4(A,C) ) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS128+1.tptp',unknown),
[] ).
cnf(164751296,plain,
( ~ ca_cx4(A)
| ra_px4(A,y0_nn_1(A)) ),
inference(rewrite,[status(thm)],[axiom_8]),
[] ).
fof(axiom_9,plain,
! [A,B] :
( ( ~ ca_cx4xcomp(A)
| ~ ra_px4(A,B) )
& ( ca_cx4xcomp(A)
| ra_px4(A,y(A,B)) ) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS128+1.tptp',unknown),
[] ).
cnf(164769800,plain,
( ~ ca_cx4xcomp(A)
| ~ ra_px4(A,B) ),
inference(rewrite,[status(thm)],[axiom_9]),
[] ).
fof(axiom_10,plain,
! [A] :
( ( cexcomp(A)
| ~ ca_cx4xcomp(A) )
& ( cd(A)
| ~ ca_cx4xcomp(A) )
& ( ca_cx4xcomp(A)
| ~ cd(A)
| ~ cexcomp(A) ) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS128+1.tptp',unknown),
[] ).
cnf(164776720,plain,
( ca_cx4xcomp(A)
| ~ cd(A)
| ~ cexcomp(A) ),
inference(rewrite,[status(thm)],[axiom_10]),
[] ).
cnf(164627248,plain,
( cexcomp(y_nn_5(A))
| ~ cunsatisfiable(A) ),
inference(rewrite,[status(thm)],[axiom_2]),
[] ).
cnf(170057672,plain,
cexcomp(y_nn_5(i2003_11_14_17_22_31584)),
inference(resolution,[status(thm)],[164627248,164797408]),
[] ).
cnf(170136200,plain,
( ca_cx4xcomp(y_nn_5(i2003_11_14_17_22_31584))
| ~ cd(y_nn_5(i2003_11_14_17_22_31584)) ),
inference(resolution,[status(thm)],[164776720,170057672]),
[] ).
cnf(164653896,plain,
( ~ rr(A,C)
| cd(C)
| ~ cunsatisfiable(A) ),
inference(rewrite,[status(thm)],[axiom_2]),
[] ).
cnf(170095160,plain,
( ~ rr(i2003_11_14_17_22_31584,B)
| cd(B) ),
inference(resolution,[status(thm)],[164653896,164797408]),
[] ).
cnf(170243928,plain,
cd(y_nn_5(i2003_11_14_17_22_31584)),
inference(resolution,[status(thm)],[170095160,170068856]),
[] ).
cnf(170290856,plain,
ca_cx4xcomp(y_nn_5(i2003_11_14_17_22_31584)),
inference(resolution,[status(thm)],[170136200,170243928]),
[] ).
cnf(170311552,plain,
~ ra_px4(y_nn_5(i2003_11_14_17_22_31584),A),
inference(resolution,[status(thm)],[164769800,170290856]),
[] ).
cnf(contradiction,plain,
$false,
inference(forward_subsumption_resolution__resolution,[status(thm)],[170238424,164751296,170311552]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 0 seconds
% START OF PROOF SEQUENCE
% fof(axiom_2,plain,(((~rr(A,C)|cd(C)|~cunsatisfiable(A))&(~rr(A,D)|ca_cx4(D)|~cunsatisfiable(A))&(rr(A,y_nn_5(A))|~cunsatisfiable(A))&(cexcomp(y_nn_5(A))|~cunsatisfiable(A))&(~ca_cx4(y(A,C,D,E))|rr(A,y_nn_1(A,C,D,E))|~rr(A,E)|~cexcomp(E)|cunsatisfiable(A))&(rr(A,y(A,C,D,E))|rr(A,y_nn_1(A,C,D,E))|~rr(A,E)|~cexcomp(E)|cunsatisfiable(A))&(~ca_cx4(y(A,C,D,E))|~cd(y_nn_1(A,C,D,E))|~rr(A,E)|~cexcomp(E)|cunsatisfiable(A))&(rr(A,y(A,C,D,E))|~cd(y_nn_1(A,C,D,E))|~rr(A,E)|~cexcomp(E)|cunsatisfiable(A)))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS128+1.tptp',unknown),[]).
%
% cnf(164646640,plain,(~rr(A,D)|ca_cx4(D)|~cunsatisfiable(A)),inference(rewrite,[status(thm)],[axiom_2]),[]).
%
% fof(axiom_11,plain,(cunsatisfiable(i2003_11_14_17_22_31584)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS128+1.tptp',unknown),[]).
%
% cnf(164797408,plain,(cunsatisfiable(i2003_11_14_17_22_31584)),inference(rewrite,[status(thm)],[axiom_11]),[]).
%
% cnf(170088960,plain,(~rr(i2003_11_14_17_22_31584,C)|ca_cx4(C)),inference(resolution,[status(thm)],[164646640,164797408]),[]).
%
% cnf(164483024,plain,(rr(A,y_nn_5(A))|~cunsatisfiable(A)),inference(rewrite,[status(thm)],[axiom_2]),[]).
%
% cnf(170068856,plain,(rr(i2003_11_14_17_22_31584,y_nn_5(i2003_11_14_17_22_31584))),inference(resolution,[status(thm)],[164483024,164797408]),[]).
%
% cnf(170238424,plain,(ca_cx4(y_nn_5(i2003_11_14_17_22_31584))),inference(resolution,[status(thm)],[170088960,170068856]),[]).
%
% fof(axiom_8,plain,(((~ca_cx4(A)|ra_px4(A,y0_nn_1(A)))&(ca_cx4(A)|~ra_px4(A,C)))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS128+1.tptp',unknown),[]).
%
% cnf(164751296,plain,(~ca_cx4(A)|ra_px4(A,y0_nn_1(A))),inference(rewrite,[status(thm)],[axiom_8]),[]).
%
% fof(axiom_9,plain,(((~ca_cx4xcomp(A)|~ra_px4(A,B))&(ca_cx4xcomp(A)|ra_px4(A,y(A,B))))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS128+1.tptp',unknown),[]).
%
% cnf(164769800,plain,(~ca_cx4xcomp(A)|~ra_px4(A,B)),inference(rewrite,[status(thm)],[axiom_9]),[]).
%
% fof(axiom_10,plain,(((cexcomp(A)|~ca_cx4xcomp(A))&(cd(A)|~ca_cx4xcomp(A))&(ca_cx4xcomp(A)|~cd(A)|~cexcomp(A)))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS128+1.tptp',unknown),[]).
%
% cnf(164776720,plain,(ca_cx4xcomp(A)|~cd(A)|~cexcomp(A)),inference(rewrite,[status(thm)],[axiom_10]),[]).
%
% cnf(164627248,plain,(cexcomp(y_nn_5(A))|~cunsatisfiable(A)),inference(rewrite,[status(thm)],[axiom_2]),[]).
%
% cnf(170057672,plain,(cexcomp(y_nn_5(i2003_11_14_17_22_31584))),inference(resolution,[status(thm)],[164627248,164797408]),[]).
%
% cnf(170136200,plain,(ca_cx4xcomp(y_nn_5(i2003_11_14_17_22_31584))|~cd(y_nn_5(i2003_11_14_17_22_31584))),inference(resolution,[status(thm)],[164776720,170057672]),[]).
%
% cnf(164653896,plain,(~rr(A,C)|cd(C)|~cunsatisfiable(A)),inference(rewrite,[status(thm)],[axiom_2]),[]).
%
% cnf(170095160,plain,(~rr(i2003_11_14_17_22_31584,B)|cd(B)),inference(resolution,[status(thm)],[164653896,164797408]),[]).
%
% cnf(170243928,plain,(cd(y_nn_5(i2003_11_14_17_22_31584))),inference(resolution,[status(thm)],[170095160,170068856]),[]).
%
% cnf(170290856,plain,(ca_cx4xcomp(y_nn_5(i2003_11_14_17_22_31584))),inference(resolution,[status(thm)],[170136200,170243928]),[]).
%
% cnf(170311552,plain,(~ra_px4(y_nn_5(i2003_11_14_17_22_31584),A)),inference(resolution,[status(thm)],[164769800,170290856]),[]).
%
% cnf(contradiction,plain,$false,inference(forward_subsumption_resolution__resolution,[status(thm)],[170238424,164751296,170311552]),[]).
%
% END OF PROOF SEQUENCE
% faust: ../JJParser/Signature.c:39: void FreeSignatureList(SymbolNodeType**): Assertion `(*Symbols)->NumberOfUses == 0' failed.
%
%------------------------------------------------------------------------------