%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : KRS083+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:34 EDT 2009
% Result : Unsatisfiable 3.7s
% Output : Refutation 3.7s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 9
% Syntax : Number of formulae : 37 ( 10 unt; 0 def)
% Number of atoms : 105 ( 0 equ)
% Maximal formula atoms : 23 ( 2 avg)
% Number of connectives : 126 ( 58 ~; 56 |; 12 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 1 con; 0-2 aty)
% Number of variables : 58 ( 12 sgn 18 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(axiom_2,plain,
! [A,B,F,G] :
( ( ~ cc(A)
| ~ cunsatisfiable(A) )
& ( rinvf(A,y_nn_2(A,B))
| ~ cunsatisfiable(A) )
& ( cd(y_nn_2(A,B))
| ~ cunsatisfiable(A) )
& ( cd(z_nn_4(A,B))
| ~ rinvr(A,B)
| ~ cunsatisfiable(A) )
& ( rinvf(B,z_nn_4(A,B))
| ~ rinvr(A,B)
| ~ cunsatisfiable(A) )
& ( ~ rinvf(y_nn_1(A,B),F)
| ~ cd(F)
| cc(A)
| ~ rinvf(A,G)
| ~ cd(G)
| cunsatisfiable(A) )
& ( rinvr(A,y_nn_1(A,B))
| cc(A)
| ~ rinvf(A,G)
| ~ cd(G)
| cunsatisfiable(A) ) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS083+1.tptp',unknown),
[] ).
cnf(144025192,plain,
( cd(z_nn_4(A,B))
| ~ rinvr(A,B)
| ~ cunsatisfiable(A) ),
inference(rewrite,[status(thm)],[axiom_2]),
[] ).
fof(axiom_8,plain,
cunsatisfiable(i2003_11_14_17_19_32337),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS083+1.tptp',unknown),
[] ).
cnf(144139856,plain,
cunsatisfiable(i2003_11_14_17_19_32337),
inference(rewrite,[status(thm)],[axiom_8]),
[] ).
cnf(149430752,plain,
( cd(z_nn_4(i2003_11_14_17_19_32337,A))
| ~ rinvr(i2003_11_14_17_19_32337,A) ),
inference(resolution,[status(thm)],[144025192,144139856]),
[] ).
fof(axiom_6,plain,
! [A,B] :
( ( ~ rinvr(A,B)
| rr(B,A) )
& ( rinvr(A,B)
| ~ rr(B,A) ) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS083+1.tptp',unknown),
[] ).
cnf(143810072,plain,
( rinvr(A,B)
| ~ rr(B,A) ),
inference(rewrite,[status(thm)],[axiom_6]),
[] ).
fof(axiom_9,plain,
! [A,B] :
( ~ rf(A,B)
| rr(A,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS083+1.tptp',unknown),
[] ).
cnf(144149176,plain,
( ~ rf(A,B)
| rr(A,B) ),
inference(rewrite,[status(thm)],[axiom_9]),
[] ).
fof(axiom_5,plain,
! [A,B] :
( ( ~ rinvf(A,B)
| rf(B,A) )
& ( rinvf(A,B)
| ~ rf(B,A) ) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS083+1.tptp',unknown),
[] ).
cnf(144110232,plain,
( ~ rinvf(A,B)
| rf(B,A) ),
inference(rewrite,[status(thm)],[axiom_5]),
[] ).
cnf(144041424,plain,
( rinvf(A,y_nn_2(A,B))
| ~ cunsatisfiable(A) ),
inference(rewrite,[status(thm)],[axiom_2]),
[] ).
cnf(149393256,plain,
rinvf(i2003_11_14_17_19_32337,y_nn_2(i2003_11_14_17_19_32337,A)),
inference(resolution,[status(thm)],[144041424,144139856]),
[] ).
cnf(149657312,plain,
rf(y_nn_2(i2003_11_14_17_19_32337,A),i2003_11_14_17_19_32337),
inference(resolution,[status(thm)],[144110232,149393256]),
[] ).
cnf(149682656,plain,
rr(y_nn_2(i2003_11_14_17_19_32337,A),i2003_11_14_17_19_32337),
inference(resolution,[status(thm)],[144149176,149657312]),
[] ).
cnf(149726248,plain,
rinvr(i2003_11_14_17_19_32337,y_nn_2(i2003_11_14_17_19_32337,A)),
inference(resolution,[status(thm)],[143810072,149682656]),
[] ).
fof(axiom_4,plain,
! [A,B,C] :
( ~ cowlthing(A)
| ~ rf(A,B)
| ~ rf(A,C)
| $equal(C,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS083+1.tptp',unknown),
[] ).
fof(axiom_0,plain,
! [A] :
( cowlthing(A)
& ~ cowlnothing(A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS083+1.tptp',unknown),
[] ).
cnf(143943504,plain,
cowlthing(A),
inference(rewrite,[status(thm)],[axiom_0]),
[] ).
cnf(144098512,plain,
( ~ rf(A,B)
| ~ rf(A,C)
| $equal(C,B) ),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[axiom_4,143943504]),
[] ).
fof(axiom_3,plain,
! [A,C] :
( ( cc(A)
| ~ cd(A) )
& ( rf(A,y_nn_1(A))
| ~ cd(A) )
& ( ~ cc(y_nn_1(A))
| ~ cd(A) )
& ( cd(A)
| ~ rf(A,C)
| cc(C)
| ~ cc(A) ) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS083+1.tptp',unknown),
[] ).
cnf(144074920,plain,
( rf(A,y_nn_1(A))
| ~ cd(A) ),
inference(rewrite,[status(thm)],[axiom_3]),
[] ).
cnf(153510528,plain,
( ~ rf(A,B)
| $equal(y_nn_1(A),B)
| ~ cd(A) ),
inference(resolution,[status(thm)],[144098512,144074920]),
[] ).
fof(cc_substitution_1,plain,
! [B,A] :
( ~ $equal(B,A)
| ~ cc(A)
| cc(B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS083+1.tptp',unknown),
[] ).
cnf(143831048,plain,
( ~ $equal(B,A)
| ~ cc(A)
| cc(B) ),
inference(rewrite,[status(thm)],[cc_substitution_1]),
[] ).
cnf(144086120,plain,
( cc(A)
| ~ cd(A) ),
inference(rewrite,[status(thm)],[axiom_3]),
[] ).
cnf(144035400,plain,
( cd(y_nn_2(A,B))
| ~ cunsatisfiable(A) ),
inference(rewrite,[status(thm)],[axiom_2]),
[] ).
cnf(149379096,plain,
cd(y_nn_2(i2003_11_14_17_19_32337,A)),
inference(resolution,[status(thm)],[144035400,144139856]),
[] ).
cnf(149518032,plain,
cc(y_nn_2(i2003_11_14_17_19_32337,A)),
inference(resolution,[status(thm)],[144086120,149379096]),
[] ).
cnf(149641688,plain,
( ~ $equal(A,y_nn_2(i2003_11_14_17_19_32337,B))
| cc(A) ),
inference(resolution,[status(thm)],[143831048,149518032]),
[] ).
cnf(144067888,plain,
( ~ cc(y_nn_1(A))
| ~ cd(A) ),
inference(rewrite,[status(thm)],[axiom_3]),
[] ).
cnf(150921784,plain,
( ~ $equal(y_nn_1(B),y_nn_2(i2003_11_14_17_19_32337,A))
| ~ cd(B) ),
inference(resolution,[status(thm)],[149641688,144067888]),
[] ).
cnf(190363808,plain,
( ~ rf(A,y_nn_2(i2003_11_14_17_19_32337,B))
| ~ cd(A) ),
inference(resolution,[status(thm)],[153510528,150921784]),
[] ).
cnf(144016504,plain,
( rinvf(B,z_nn_4(A,B))
| ~ rinvr(A,B)
| ~ cunsatisfiable(A) ),
inference(rewrite,[status(thm)],[axiom_2]),
[] ).
cnf(149440376,plain,
( rinvf(A,z_nn_4(i2003_11_14_17_19_32337,A))
| ~ rinvr(i2003_11_14_17_19_32337,A) ),
inference(resolution,[status(thm)],[144016504,144139856]),
[] ).
cnf(158638768,plain,
( ~ rinvr(i2003_11_14_17_19_32337,A)
| rf(z_nn_4(i2003_11_14_17_19_32337,A),A) ),
inference(resolution,[status(thm)],[149440376,144110232]),
[] ).
cnf(contradiction,plain,
$false,
inference(forward_subsumption_resolution__resolution,[status(thm)],[149430752,149726248,190363808,158638768]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 4 seconds
% START OF PROOF SEQUENCE
% fof(axiom_2,plain,(((~cc(A)|~cunsatisfiable(A))&(rinvf(A,y_nn_2(A,B))|~cunsatisfiable(A))&(cd(y_nn_2(A,B))|~cunsatisfiable(A))&(cd(z_nn_4(A,B))|~rinvr(A,B)|~cunsatisfiable(A))&(rinvf(B,z_nn_4(A,B))|~rinvr(A,B)|~cunsatisfiable(A))&(~rinvf(y_nn_1(A,B),F)|~cd(F)|cc(A)|~rinvf(A,G)|~cd(G)|cunsatisfiable(A))&(rinvr(A,y_nn_1(A,B))|cc(A)|~rinvf(A,G)|~cd(G)|cunsatisfiable(A)))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS083+1.tptp',unknown),[]).
%
% cnf(144025192,plain,(cd(z_nn_4(A,B))|~rinvr(A,B)|~cunsatisfiable(A)),inference(rewrite,[status(thm)],[axiom_2]),[]).
%
% fof(axiom_8,plain,(cunsatisfiable(i2003_11_14_17_19_32337)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS083+1.tptp',unknown),[]).
%
% cnf(144139856,plain,(cunsatisfiable(i2003_11_14_17_19_32337)),inference(rewrite,[status(thm)],[axiom_8]),[]).
%
% cnf(149430752,plain,(cd(z_nn_4(i2003_11_14_17_19_32337,A))|~rinvr(i2003_11_14_17_19_32337,A)),inference(resolution,[status(thm)],[144025192,144139856]),[]).
%
% fof(axiom_6,plain,(((~rinvr(A,B)|rr(B,A))&(rinvr(A,B)|~rr(B,A)))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS083+1.tptp',unknown),[]).
%
% cnf(143810072,plain,(rinvr(A,B)|~rr(B,A)),inference(rewrite,[status(thm)],[axiom_6]),[]).
%
% fof(axiom_9,plain,(~rf(A,B)|rr(A,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS083+1.tptp',unknown),[]).
%
% cnf(144149176,plain,(~rf(A,B)|rr(A,B)),inference(rewrite,[status(thm)],[axiom_9]),[]).
%
% fof(axiom_5,plain,(((~rinvf(A,B)|rf(B,A))&(rinvf(A,B)|~rf(B,A)))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS083+1.tptp',unknown),[]).
%
% cnf(144110232,plain,(~rinvf(A,B)|rf(B,A)),inference(rewrite,[status(thm)],[axiom_5]),[]).
%
% cnf(144041424,plain,(rinvf(A,y_nn_2(A,B))|~cunsatisfiable(A)),inference(rewrite,[status(thm)],[axiom_2]),[]).
%
% cnf(149393256,plain,(rinvf(i2003_11_14_17_19_32337,y_nn_2(i2003_11_14_17_19_32337,A))),inference(resolution,[status(thm)],[144041424,144139856]),[]).
%
% cnf(149657312,plain,(rf(y_nn_2(i2003_11_14_17_19_32337,A),i2003_11_14_17_19_32337)),inference(resolution,[status(thm)],[144110232,149393256]),[]).
%
% cnf(149682656,plain,(rr(y_nn_2(i2003_11_14_17_19_32337,A),i2003_11_14_17_19_32337)),inference(resolution,[status(thm)],[144149176,149657312]),[]).
%
% cnf(149726248,plain,(rinvr(i2003_11_14_17_19_32337,y_nn_2(i2003_11_14_17_19_32337,A))),inference(resolution,[status(thm)],[143810072,149682656]),[]).
%
% fof(axiom_4,plain,(~cowlthing(A)|~rf(A,B)|~rf(A,C)|$equal(C,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS083+1.tptp',unknown),[]).
%
% fof(axiom_0,plain,((cowlthing(A)&~cowlnothing(A))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS083+1.tptp',unknown),[]).
%
% cnf(143943504,plain,(cowlthing(A)),inference(rewrite,[status(thm)],[axiom_0]),[]).
%
% cnf(144098512,plain,(~rf(A,B)|~rf(A,C)|$equal(C,B)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[axiom_4,143943504]),[]).
%
% fof(axiom_3,plain,(((cc(A)|~cd(A))&(rf(A,y_nn_1(A))|~cd(A))&(~cc(y_nn_1(A))|~cd(A))&(cd(A)|~rf(A,C)|cc(C)|~cc(A)))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS083+1.tptp',unknown),[]).
%
% cnf(144074920,plain,(rf(A,y_nn_1(A))|~cd(A)),inference(rewrite,[status(thm)],[axiom_3]),[]).
%
% cnf(153510528,plain,(~rf(A,B)|$equal(y_nn_1(A),B)|~cd(A)),inference(resolution,[status(thm)],[144098512,144074920]),[]).
%
% fof(cc_substitution_1,plain,(~$equal(B,A)|~cc(A)|cc(B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS083+1.tptp',unknown),[]).
%
% cnf(143831048,plain,(~$equal(B,A)|~cc(A)|cc(B)),inference(rewrite,[status(thm)],[cc_substitution_1]),[]).
%
% cnf(144086120,plain,(cc(A)|~cd(A)),inference(rewrite,[status(thm)],[axiom_3]),[]).
%
% cnf(144035400,plain,(cd(y_nn_2(A,B))|~cunsatisfiable(A)),inference(rewrite,[status(thm)],[axiom_2]),[]).
%
% cnf(149379096,plain,(cd(y_nn_2(i2003_11_14_17_19_32337,A))),inference(resolution,[status(thm)],[144035400,144139856]),[]).
%
% cnf(149518032,plain,(cc(y_nn_2(i2003_11_14_17_19_32337,A))),inference(resolution,[status(thm)],[144086120,149379096]),[]).
%
% cnf(149641688,plain,(~$equal(A,y_nn_2(i2003_11_14_17_19_32337,B))|cc(A)),inference(resolution,[status(thm)],[143831048,149518032]),[]).
%
% cnf(144067888,plain,(~cc(y_nn_1(A))|~cd(A)),inference(rewrite,[status(thm)],[axiom_3]),[]).
%
% cnf(150921784,plain,(~$equal(y_nn_1(B),y_nn_2(i2003_11_14_17_19_32337,A))|~cd(B)),inference(resolution,[status(thm)],[149641688,144067888]),[]).
%
% cnf(190363808,plain,(~rf(A,y_nn_2(i2003_11_14_17_19_32337,B))|~cd(A)),inference(resolution,[status(thm)],[153510528,150921784]),[]).
%
% cnf(144016504,plain,(rinvf(B,z_nn_4(A,B))|~rinvr(A,B)|~cunsatisfiable(A)),inference(rewrite,[status(thm)],[axiom_2]),[]).
%
% cnf(149440376,plain,(rinvf(A,z_nn_4(i2003_11_14_17_19_32337,A))|~rinvr(i2003_11_14_17_19_32337,A)),inference(resolution,[status(thm)],[144016504,144139856]),[]).
%
% cnf(158638768,plain,(~rinvr(i2003_11_14_17_19_32337,A)|rf(z_nn_4(i2003_11_14_17_19_32337,A),A)),inference(resolution,[status(thm)],[149440376,144110232]),[]).
%
% cnf(contradiction,plain,$false,inference(forward_subsumption_resolution__resolution,[status(thm)],[149430752,149726248,190363808,158638768]),[]).
%
% END OF PROOF SEQUENCE
% faust: ../JJParser/Signature.c:39: void FreeSignatureList(SymbolNodeType**): Assertion `(*Symbols)->NumberOfUses == 0' failed.
%
%------------------------------------------------------------------------------