%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : KRS142+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:29:14 EDT 2009
% Result : Theorem 3.7s
% Output : Refutation 3.7s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 5
% Syntax : Number of formulae : 62 ( 6 unt; 0 def)
% Number of atoms : 370 ( 0 equ)
% Maximal formula atoms : 192 ( 5 avg)
% Number of connectives : 456 ( 148 ~; 274 |; 34 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 39 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-1 aty)
% Number of variables : 69 ( 7 sgn 9 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(the_axiom,plain,
! [D] :
( ( rp(x(D),y0(D))
| ~ rp(x_nn_1,D)
| ~ xsd_integer(x_nn_2)
| xsd_integer(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( rp(x(D),y1(D))
| ~ rp(x_nn_1,D)
| ~ xsd_integer(x_nn_2)
| xsd_integer(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( ~ $equal(y1(D),y0(D))
| ~ rp(x_nn_1,D)
| ~ xsd_integer(x_nn_2)
| xsd_integer(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( cc(x(D))
| ~ rp(x_nn_1,D)
| ~ xsd_integer(x_nn_2)
| xsd_integer(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( rp(x(D),y0(D))
| cc(x_nn_1)
| ~ xsd_integer(x_nn_2)
| xsd_integer(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( rp(x(D),y1(D))
| cc(x_nn_1)
| ~ xsd_integer(x_nn_2)
| xsd_integer(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( ~ $equal(y1(D),y0(D))
| cc(x_nn_1)
| ~ xsd_integer(x_nn_2)
| xsd_integer(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( cc(x(D))
| cc(x_nn_1)
| ~ xsd_integer(x_nn_2)
| xsd_integer(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( rp(x(D),y0(D))
| ~ rp(x_nn_1,D)
| ~ xsd_string(x_nn_2)
| xsd_integer(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( rp(x(D),y1(D))
| ~ rp(x_nn_1,D)
| ~ xsd_string(x_nn_2)
| xsd_integer(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( ~ $equal(y1(D),y0(D))
| ~ rp(x_nn_1,D)
| ~ xsd_string(x_nn_2)
| xsd_integer(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( cc(x(D))
| ~ rp(x_nn_1,D)
| ~ xsd_string(x_nn_2)
| xsd_integer(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( rp(x(D),y0(D))
| cc(x_nn_1)
| ~ xsd_string(x_nn_2)
| xsd_integer(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( rp(x(D),y1(D))
| cc(x_nn_1)
| ~ xsd_string(x_nn_2)
| xsd_integer(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( ~ $equal(y1(D),y0(D))
| cc(x_nn_1)
| ~ xsd_string(x_nn_2)
| xsd_integer(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( cc(x(D))
| cc(x_nn_1)
| ~ xsd_string(x_nn_2)
| xsd_integer(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( rp(x(D),y0(D))
| ~ rp(x_nn_1,D)
| ~ xsd_integer(x_nn_2)
| xsd_string(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( rp(x(D),y1(D))
| ~ rp(x_nn_1,D)
| ~ xsd_integer(x_nn_2)
| xsd_string(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( ~ $equal(y1(D),y0(D))
| ~ rp(x_nn_1,D)
| ~ xsd_integer(x_nn_2)
| xsd_string(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( cc(x(D))
| ~ rp(x_nn_1,D)
| ~ xsd_integer(x_nn_2)
| xsd_string(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( rp(x(D),y0(D))
| cc(x_nn_1)
| ~ xsd_integer(x_nn_2)
| xsd_string(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( rp(x(D),y1(D))
| cc(x_nn_1)
| ~ xsd_integer(x_nn_2)
| xsd_string(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( ~ $equal(y1(D),y0(D))
| cc(x_nn_1)
| ~ xsd_integer(x_nn_2)
| xsd_string(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( cc(x(D))
| cc(x_nn_1)
| ~ xsd_integer(x_nn_2)
| xsd_string(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( rp(x(D),y0(D))
| ~ rp(x_nn_1,D)
| ~ xsd_string(x_nn_2)
| xsd_string(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( rp(x(D),y1(D))
| ~ rp(x_nn_1,D)
| ~ xsd_string(x_nn_2)
| xsd_string(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( ~ $equal(y1(D),y0(D))
| ~ rp(x_nn_1,D)
| ~ xsd_string(x_nn_2)
| xsd_string(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( cc(x(D))
| ~ rp(x_nn_1,D)
| ~ xsd_string(x_nn_2)
| xsd_string(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( rp(x(D),y0(D))
| cc(x_nn_1)
| ~ xsd_string(x_nn_2)
| xsd_string(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( rp(x(D),y1(D))
| cc(x_nn_1)
| ~ xsd_string(x_nn_2)
| xsd_string(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( ~ $equal(y1(D),y0(D))
| cc(x_nn_1)
| ~ xsd_string(x_nn_2)
| xsd_string(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) )
& ( cc(x(D))
| cc(x_nn_1)
| ~ xsd_string(x_nn_2)
| xsd_string(x_nn_2)
| ~ cowlthing(x_nn_3)
| cowlnothing(x_nn_3) ) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS142+1.tptp',unknown),
[] ).
fof(axiom_1,plain,
! [A] :
( ( ~ xsd_string(A)
| ~ xsd_integer(A) )
& ( xsd_string(A)
| xsd_integer(A) ) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS142+1.tptp',unknown),
[] ).
cnf(166864376,plain,
( xsd_string(A)
| xsd_integer(A) ),
inference(rewrite,[status(thm)],[axiom_1]),
[] ).
fof(axiom_0,plain,
! [A] :
( cowlthing(A)
& ~ cowlnothing(A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS142+1.tptp',unknown),
[] ).
cnf(166853832,plain,
cowlthing(A),
inference(rewrite,[status(thm)],[axiom_0]),
[] ).
cnf(167373096,plain,
( cc(x(D))
| cc(x_nn_1)
| xsd_string(x_nn_2)
| cowlnothing(x_nn_3) ),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,166864376,166853832]),
[] ).
cnf(167487760,plain,
( cc(x(D))
| cc(x_nn_1)
| xsd_integer(x_nn_2)
| cowlnothing(x_nn_3) ),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,167373096,166853832]),
[] ).
cnf(166844760,plain,
~ cowlnothing(A),
inference(rewrite,[status(thm)],[axiom_0]),
[] ).
cnf(215072040,plain,
( cc(x(D))
| cc(x_nn_1)
| xsd_integer(x_nn_2) ),
inference(resolution,[status(thm)],[167487760,166844760]),
[] ).
cnf(215063200,plain,
( cc(x(D))
| cc(x_nn_1)
| xsd_string(x_nn_2) ),
inference(resolution,[status(thm)],[167373096,166844760]),
[] ).
cnf(166870968,plain,
( ~ xsd_string(A)
| ~ xsd_integer(A) ),
inference(rewrite,[status(thm)],[axiom_1]),
[] ).
cnf(215169256,plain,
( cc(x(D))
| cc(x_nn_1) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[215072040,215063200,166870968]),
[] ).
cnf(167431992,plain,
( rp(x(D),y0(D))
| cc(x_nn_1)
| xsd_string(x_nn_2)
| cowlnothing(x_nn_3) ),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,166864376,166853832]),
[] ).
cnf(167511568,plain,
( rp(x(D),y0(D))
| cc(x_nn_1)
| xsd_integer(x_nn_2)
| cowlnothing(x_nn_3) ),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,167431992,166853832]),
[] ).
cnf(215098952,plain,
( rp(x(D),y0(D))
| cc(x_nn_1)
| xsd_integer(x_nn_2) ),
inference(resolution,[status(thm)],[167511568,166844760]),
[] ).
cnf(215085504,plain,
( rp(x(D),y0(D))
| cc(x_nn_1)
| xsd_string(x_nn_2) ),
inference(resolution,[status(thm)],[167431992,166844760]),
[] ).
cnf(215482984,plain,
( rp(x(D),y0(D))
| cc(x_nn_1) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[215098952,215085504,166870968]),
[] ).
cnf(167481632,plain,
( rp(x(D),y0(D))
| ~ rp(x_nn_1,D)
| xsd_string(x_nn_2)
| cowlnothing(x_nn_3) ),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,166864376,166853832]),
[] ).
cnf(167541512,plain,
( rp(x(D),y0(D))
| ~ rp(x_nn_1,D)
| xsd_integer(x_nn_2)
| cowlnothing(x_nn_3) ),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,167481632,166853832]),
[] ).
cnf(215134872,plain,
( rp(x(D),y0(D))
| ~ rp(x_nn_1,D)
| xsd_integer(x_nn_2) ),
inference(resolution,[status(thm)],[167541512,166844760]),
[] ).
cnf(215125888,plain,
( rp(x(D),y0(D))
| ~ rp(x_nn_1,D)
| xsd_string(x_nn_2) ),
inference(resolution,[status(thm)],[167481632,166844760]),
[] ).
cnf(216501328,plain,
( rp(x(D),y0(D))
| ~ rp(x_nn_1,D) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[215134872,215125888,166870968]),
[] ).
fof(axiom_2,plain,
! [A,C,D] :
( ( ~ rp(A,C)
| ~ rp(A,D)
| $equal(D,C)
| ~ cc(A) )
& ( rp(A,y0_nn_1(A))
| ~ cc(A) ) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS142+1.tptp',unknown),
[] ).
cnf(166877152,plain,
( rp(A,y0_nn_1(A))
| ~ cc(A) ),
inference(rewrite,[status(thm)],[axiom_2]),
[] ).
cnf(216574520,plain,
rp(x(y0_nn_1(x_nn_1)),y0(y0_nn_1(x_nn_1))),
inference(forward_subsumption_resolution__resolution,[status(thm)],[215482984,216501328,166877152]),
[] ).
cnf(167460960,plain,
( ~ $equal(y1(D),y0(D))
| ~ rp(x_nn_1,D)
| xsd_string(x_nn_2)
| cowlnothing(x_nn_3) ),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,166864376,166853832]),
[] ).
cnf(167524264,plain,
( ~ $equal(y1(D),y0(D))
| ~ rp(x_nn_1,D)
| xsd_integer(x_nn_2)
| cowlnothing(x_nn_3) ),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,167460960,166853832]),
[] ).
cnf(215147920,plain,
( ~ $equal(y1(D),y0(D))
| ~ rp(x_nn_1,D)
| xsd_integer(x_nn_2) ),
inference(resolution,[status(thm)],[167524264,166844760]),
[] ).
cnf(215139152,plain,
( ~ $equal(y1(D),y0(D))
| ~ rp(x_nn_1,D)
| xsd_string(x_nn_2) ),
inference(resolution,[status(thm)],[167460960,166844760]),
[] ).
cnf(218677168,plain,
( ~ $equal(y1(D),y0(D))
| ~ rp(x_nn_1,D) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[215147920,215139152,166870968]),
[] ).
fof(rp_substitution_2,plain,
! [B,A,C] :
( ~ $equal(B,A)
| ~ rp(C,A)
| rp(C,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS142+1.tptp',unknown),
[] ).
cnf(166823272,plain,
( ~ $equal(B,A)
| ~ rp(C,A)
| rp(C,B) ),
inference(rewrite,[status(thm)],[rp_substitution_2]),
[] ).
cnf(215772184,plain,
( ~ $equal(A,y0_nn_1(B))
| rp(B,A)
| ~ cc(B) ),
inference(resolution,[status(thm)],[166823272,166877152]),
[] ).
cnf(167452944,plain,
( cc(x(D))
| ~ rp(x_nn_1,D)
| xsd_string(x_nn_2)
| cowlnothing(x_nn_3) ),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,166864376,166853832]),
[] ).
cnf(167517816,plain,
( cc(x(D))
| ~ rp(x_nn_1,D)
| xsd_integer(x_nn_2)
| cowlnothing(x_nn_3) ),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,167452944,166853832]),
[] ).
cnf(215103312,plain,
( cc(x(D))
| ~ rp(x_nn_1,D)
| xsd_integer(x_nn_2) ),
inference(resolution,[status(thm)],[167517816,166844760]),
[] ).
cnf(215089848,plain,
( cc(x(D))
| ~ rp(x_nn_1,D)
| xsd_string(x_nn_2) ),
inference(resolution,[status(thm)],[167452944,166844760]),
[] ).
cnf(215545656,plain,
( cc(x(D))
| ~ rp(x_nn_1,D) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[215103312,215089848,166870968]),
[] ).
cnf(218418680,plain,
( ~ $equal(A,y0_nn_1(x_nn_1))
| cc(x(A)) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[215169256,215772184,215545656]),
[] ).
cnf(218475712,plain,
( ~ $equal(A,y0_nn_1(x_nn_1))
| rp(x(A),y0(A)) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[215482984,215772184,216501328]),
[] ).
cnf(166887224,plain,
( ~ rp(A,C)
| ~ rp(A,D)
| $equal(D,C)
| ~ cc(A) ),
inference(rewrite,[status(thm)],[axiom_2]),
[] ).
cnf(220029816,plain,
( ~ $equal(A,y0_nn_1(x_nn_1))
| ~ rp(x(A),C)
| $equal(C,y0(A)) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[218418680,218475712,166887224]),
[] ).
cnf(167469208,plain,
( rp(x(D),y1(D))
| ~ rp(x_nn_1,D)
| xsd_string(x_nn_2)
| cowlnothing(x_nn_3) ),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,166864376,166853832]),
[] ).
cnf(167534928,plain,
( rp(x(D),y1(D))
| ~ rp(x_nn_1,D)
| xsd_integer(x_nn_2)
| cowlnothing(x_nn_3) ),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,167469208,166853832]),
[] ).
cnf(215130160,plain,
( rp(x(D),y1(D))
| ~ rp(x_nn_1,D)
| xsd_integer(x_nn_2) ),
inference(resolution,[status(thm)],[167534928,166844760]),
[] ).
cnf(215121144,plain,
( rp(x(D),y1(D))
| ~ rp(x_nn_1,D)
| xsd_string(x_nn_2) ),
inference(resolution,[status(thm)],[167469208,166844760]),
[] ).
cnf(216339648,plain,
( rp(x(D),y1(D))
| ~ rp(x_nn_1,D) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[215130160,215121144,166870968]),
[] ).
cnf(221030592,plain,
( ~ $equal(A,y0_nn_1(x_nn_1))
| ~ rp(x_nn_1,A) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[218677168,220029816,216339648]),
[] ).
cnf(221066336,plain,
~ cc(x_nn_1),
inference(resolution,[status(thm)],[221030592,166877152]),
[] ).
cnf(167402968,plain,
( ~ $equal(y1(D),y0(D))
| cc(x_nn_1)
| xsd_string(x_nn_2)
| cowlnothing(x_nn_3) ),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,166864376,166853832]),
[] ).
cnf(167498512,plain,
( ~ $equal(y1(D),y0(D))
| cc(x_nn_1)
| xsd_integer(x_nn_2)
| cowlnothing(x_nn_3) ),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,167402968,166853832]),
[] ).
cnf(215116488,plain,
( ~ $equal(y1(D),y0(D))
| cc(x_nn_1)
| xsd_integer(x_nn_2) ),
inference(resolution,[status(thm)],[167498512,166844760]),
[] ).
cnf(215107880,plain,
( ~ $equal(y1(D),y0(D))
| cc(x_nn_1)
| xsd_string(x_nn_2) ),
inference(resolution,[status(thm)],[167402968,166844760]),
[] ).
cnf(216124112,plain,
( ~ $equal(y1(D),y0(D))
| cc(x_nn_1) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[215116488,215107880,166870968]),
[] ).
cnf(217682200,plain,
( ~ rp(A,y0(F))
| ~ rp(A,y1(F))
| ~ cc(A)
| cc(x_nn_1) ),
inference(resolution,[status(thm)],[166887224,216124112]),
[] ).
cnf(167417856,plain,
( rp(x(D),y1(D))
| cc(x_nn_1)
| xsd_string(x_nn_2)
| cowlnothing(x_nn_3) ),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,166864376,166853832]),
[] ).
cnf(167505000,plain,
( rp(x(D),y1(D))
| cc(x_nn_1)
| xsd_integer(x_nn_2)
| cowlnothing(x_nn_3) ),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,167417856,166853832]),
[] ).
cnf(215094320,plain,
( rp(x(D),y1(D))
| cc(x_nn_1)
| xsd_integer(x_nn_2) ),
inference(resolution,[status(thm)],[167505000,166844760]),
[] ).
cnf(215076720,plain,
( rp(x(D),y1(D))
| cc(x_nn_1)
| xsd_string(x_nn_2) ),
inference(resolution,[status(thm)],[167417856,166844760]),
[] ).
cnf(215377072,plain,
( rp(x(D),y1(D))
| cc(x_nn_1) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[215094320,215076720,166870968]),
[] ).
cnf(216406640,plain,
rp(x(y0_nn_1(x_nn_1)),y1(y0_nn_1(x_nn_1))),
inference(forward_subsumption_resolution__resolution,[status(thm)],[215377072,216339648,166877152]),
[] ).
cnf(contradiction,plain,
$false,
inference(forward_subsumption_resolution__resolution,[status(thm)],[215169256,216574520,221066336,217682200,216406640]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 4 seconds
% START OF PROOF SEQUENCE
% fof(the_axiom,plain,(((rp(x(D),y0(D))|~rp(x_nn_1,D)|~xsd_integer(x_nn_2)|xsd_integer(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(rp(x(D),y1(D))|~rp(x_nn_1,D)|~xsd_integer(x_nn_2)|xsd_integer(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(~$equal(y1(D),y0(D))|~rp(x_nn_1,D)|~xsd_integer(x_nn_2)|xsd_integer(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(cc(x(D))|~rp(x_nn_1,D)|~xsd_integer(x_nn_2)|xsd_integer(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(rp(x(D),y0(D))|cc(x_nn_1)|~xsd_integer(x_nn_2)|xsd_integer(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(rp(x(D),y1(D))|cc(x_nn_1)|~xsd_integer(x_nn_2)|xsd_integer(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(~$equal(y1(D),y0(D))|cc(x_nn_1)|~xsd_integer(x_nn_2)|xsd_integer(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(cc(x(D))|cc(x_nn_1)|~xsd_integer(x_nn_2)|xsd_integer(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(rp(x(D),y0(D))|~rp(x_nn_1,D)|~xsd_string(x_nn_2)|xsd_integer(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(rp(x(D),y1(D))|~rp(x_nn_1,D)|~xsd_string(x_nn_2)|xsd_integer(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(~$equal(y1(D),y0(D))|~rp(x_nn_1,D)|~xsd_string(x_nn_2)|xsd_integer(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(cc(x(D))|~rp(x_nn_1,D)|~xsd_string(x_nn_2)|xsd_integer(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(rp(x(D),y0(D))|cc(x_nn_1)|~xsd_string(x_nn_2)|xsd_integer(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(rp(x(D),y1(D))|cc(x_nn_1)|~xsd_string(x_nn_2)|xsd_integer(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(~$equal(y1(D),y0(D))|cc(x_nn_1)|~xsd_string(x_nn_2)|xsd_integer(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(cc(x(D))|cc(x_nn_1)|~xsd_string(x_nn_2)|xsd_integer(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(rp(x(D),y0(D))|~rp(x_nn_1,D)|~xsd_integer(x_nn_2)|xsd_string(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(rp(x(D),y1(D))|~rp(x_nn_1,D)|~xsd_integer(x_nn_2)|xsd_string(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(~$equal(y1(D),y0(D))|~rp(x_nn_1,D)|~xsd_integer(x_nn_2)|xsd_string(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(cc(x(D))|~rp(x_nn_1,D)|~xsd_integer(x_nn_2)|xsd_string(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(rp(x(D),y0(D))|cc(x_nn_1)|~xsd_integer(x_nn_2)|xsd_string(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(rp(x(D),y1(D))|cc(x_nn_1)|~xsd_integer(x_nn_2)|xsd_string(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(~$equal(y1(D),y0(D))|cc(x_nn_1)|~xsd_integer(x_nn_2)|xsd_string(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(cc(x(D))|cc(x_nn_1)|~xsd_integer(x_nn_2)|xsd_string(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(rp(x(D),y0(D))|~rp(x_nn_1,D)|~xsd_string(x_nn_2)|xsd_string(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(rp(x(D),y1(D))|~rp(x_nn_1,D)|~xsd_string(x_nn_2)|xsd_string(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(~$equal(y1(D),y0(D))|~rp(x_nn_1,D)|~xsd_string(x_nn_2)|xsd_string(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(cc(x(D))|~rp(x_nn_1,D)|~xsd_string(x_nn_2)|xsd_string(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(rp(x(D),y0(D))|cc(x_nn_1)|~xsd_string(x_nn_2)|xsd_string(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(rp(x(D),y1(D))|cc(x_nn_1)|~xsd_string(x_nn_2)|xsd_string(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(~$equal(y1(D),y0(D))|cc(x_nn_1)|~xsd_string(x_nn_2)|xsd_string(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3))&(cc(x(D))|cc(x_nn_1)|~xsd_string(x_nn_2)|xsd_string(x_nn_2)|~cowlthing(x_nn_3)|cowlnothing(x_nn_3)))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS142+1.tptp',unknown),[]).
%
% fof(axiom_1,plain,(((~xsd_string(A)|~xsd_integer(A))&(xsd_string(A)|xsd_integer(A)))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS142+1.tptp',unknown),[]).
%
% cnf(166864376,plain,(xsd_string(A)|xsd_integer(A)),inference(rewrite,[status(thm)],[axiom_1]),[]).
%
% fof(axiom_0,plain,((cowlthing(A)&~cowlnothing(A))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS142+1.tptp',unknown),[]).
%
% cnf(166853832,plain,(cowlthing(A)),inference(rewrite,[status(thm)],[axiom_0]),[]).
%
% cnf(167373096,plain,(cc(x(D))|cc(x_nn_1)|xsd_string(x_nn_2)|cowlnothing(x_nn_3)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,166864376,166853832]),[]).
%
% cnf(167487760,plain,(cc(x(D))|cc(x_nn_1)|xsd_integer(x_nn_2)|cowlnothing(x_nn_3)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,167373096,166853832]),[]).
%
% cnf(166844760,plain,(~cowlnothing(A)),inference(rewrite,[status(thm)],[axiom_0]),[]).
%
% cnf(215072040,plain,(cc(x(D))|cc(x_nn_1)|xsd_integer(x_nn_2)),inference(resolution,[status(thm)],[167487760,166844760]),[]).
%
% cnf(215063200,plain,(cc(x(D))|cc(x_nn_1)|xsd_string(x_nn_2)),inference(resolution,[status(thm)],[167373096,166844760]),[]).
%
% cnf(166870968,plain,(~xsd_string(A)|~xsd_integer(A)),inference(rewrite,[status(thm)],[axiom_1]),[]).
%
% cnf(215169256,plain,(cc(x(D))|cc(x_nn_1)),inference(forward_subsumption_resolution__resolution,[status(thm)],[215072040,215063200,166870968]),[]).
%
% cnf(167431992,plain,(rp(x(D),y0(D))|cc(x_nn_1)|xsd_string(x_nn_2)|cowlnothing(x_nn_3)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,166864376,166853832]),[]).
%
% cnf(167511568,plain,(rp(x(D),y0(D))|cc(x_nn_1)|xsd_integer(x_nn_2)|cowlnothing(x_nn_3)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,167431992,166853832]),[]).
%
% cnf(215098952,plain,(rp(x(D),y0(D))|cc(x_nn_1)|xsd_integer(x_nn_2)),inference(resolution,[status(thm)],[167511568,166844760]),[]).
%
% cnf(215085504,plain,(rp(x(D),y0(D))|cc(x_nn_1)|xsd_string(x_nn_2)),inference(resolution,[status(thm)],[167431992,166844760]),[]).
%
% cnf(215482984,plain,(rp(x(D),y0(D))|cc(x_nn_1)),inference(forward_subsumption_resolution__resolution,[status(thm)],[215098952,215085504,166870968]),[]).
%
% cnf(167481632,plain,(rp(x(D),y0(D))|~rp(x_nn_1,D)|xsd_string(x_nn_2)|cowlnothing(x_nn_3)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,166864376,166853832]),[]).
%
% cnf(167541512,plain,(rp(x(D),y0(D))|~rp(x_nn_1,D)|xsd_integer(x_nn_2)|cowlnothing(x_nn_3)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,167481632,166853832]),[]).
%
% cnf(215134872,plain,(rp(x(D),y0(D))|~rp(x_nn_1,D)|xsd_integer(x_nn_2)),inference(resolution,[status(thm)],[167541512,166844760]),[]).
%
% cnf(215125888,plain,(rp(x(D),y0(D))|~rp(x_nn_1,D)|xsd_string(x_nn_2)),inference(resolution,[status(thm)],[167481632,166844760]),[]).
%
% cnf(216501328,plain,(rp(x(D),y0(D))|~rp(x_nn_1,D)),inference(forward_subsumption_resolution__resolution,[status(thm)],[215134872,215125888,166870968]),[]).
%
% fof(axiom_2,plain,(((~rp(A,C)|~rp(A,D)|$equal(D,C)|~cc(A))&(rp(A,y0_nn_1(A))|~cc(A)))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS142+1.tptp',unknown),[]).
%
% cnf(166877152,plain,(rp(A,y0_nn_1(A))|~cc(A)),inference(rewrite,[status(thm)],[axiom_2]),[]).
%
% cnf(216574520,plain,(rp(x(y0_nn_1(x_nn_1)),y0(y0_nn_1(x_nn_1)))),inference(forward_subsumption_resolution__resolution,[status(thm)],[215482984,216501328,166877152]),[]).
%
% cnf(167460960,plain,(~$equal(y1(D),y0(D))|~rp(x_nn_1,D)|xsd_string(x_nn_2)|cowlnothing(x_nn_3)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,166864376,166853832]),[]).
%
% cnf(167524264,plain,(~$equal(y1(D),y0(D))|~rp(x_nn_1,D)|xsd_integer(x_nn_2)|cowlnothing(x_nn_3)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,167460960,166853832]),[]).
%
% cnf(215147920,plain,(~$equal(y1(D),y0(D))|~rp(x_nn_1,D)|xsd_integer(x_nn_2)),inference(resolution,[status(thm)],[167524264,166844760]),[]).
%
% cnf(215139152,plain,(~$equal(y1(D),y0(D))|~rp(x_nn_1,D)|xsd_string(x_nn_2)),inference(resolution,[status(thm)],[167460960,166844760]),[]).
%
% cnf(218677168,plain,(~$equal(y1(D),y0(D))|~rp(x_nn_1,D)),inference(forward_subsumption_resolution__resolution,[status(thm)],[215147920,215139152,166870968]),[]).
%
% fof(rp_substitution_2,plain,(~$equal(B,A)|~rp(C,A)|rp(C,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS142+1.tptp',unknown),[]).
%
% cnf(166823272,plain,(~$equal(B,A)|~rp(C,A)|rp(C,B)),inference(rewrite,[status(thm)],[rp_substitution_2]),[]).
%
% cnf(215772184,plain,(~$equal(A,y0_nn_1(B))|rp(B,A)|~cc(B)),inference(resolution,[status(thm)],[166823272,166877152]),[]).
%
% cnf(167452944,plain,(cc(x(D))|~rp(x_nn_1,D)|xsd_string(x_nn_2)|cowlnothing(x_nn_3)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,166864376,166853832]),[]).
%
% cnf(167517816,plain,(cc(x(D))|~rp(x_nn_1,D)|xsd_integer(x_nn_2)|cowlnothing(x_nn_3)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,167452944,166853832]),[]).
%
% cnf(215103312,plain,(cc(x(D))|~rp(x_nn_1,D)|xsd_integer(x_nn_2)),inference(resolution,[status(thm)],[167517816,166844760]),[]).
%
% cnf(215089848,plain,(cc(x(D))|~rp(x_nn_1,D)|xsd_string(x_nn_2)),inference(resolution,[status(thm)],[167452944,166844760]),[]).
%
% cnf(215545656,plain,(cc(x(D))|~rp(x_nn_1,D)),inference(forward_subsumption_resolution__resolution,[status(thm)],[215103312,215089848,166870968]),[]).
%
% cnf(218418680,plain,(~$equal(A,y0_nn_1(x_nn_1))|cc(x(A))),inference(forward_subsumption_resolution__resolution,[status(thm)],[215169256,215772184,215545656]),[]).
%
% cnf(218475712,plain,(~$equal(A,y0_nn_1(x_nn_1))|rp(x(A),y0(A))),inference(forward_subsumption_resolution__resolution,[status(thm)],[215482984,215772184,216501328]),[]).
%
% cnf(166887224,plain,(~rp(A,C)|~rp(A,D)|$equal(D,C)|~cc(A)),inference(rewrite,[status(thm)],[axiom_2]),[]).
%
% cnf(220029816,plain,(~$equal(A,y0_nn_1(x_nn_1))|~rp(x(A),C)|$equal(C,y0(A))),inference(forward_subsumption_resolution__resolution,[status(thm)],[218418680,218475712,166887224]),[]).
%
% cnf(167469208,plain,(rp(x(D),y1(D))|~rp(x_nn_1,D)|xsd_string(x_nn_2)|cowlnothing(x_nn_3)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,166864376,166853832]),[]).
%
% cnf(167534928,plain,(rp(x(D),y1(D))|~rp(x_nn_1,D)|xsd_integer(x_nn_2)|cowlnothing(x_nn_3)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,167469208,166853832]),[]).
%
% cnf(215130160,plain,(rp(x(D),y1(D))|~rp(x_nn_1,D)|xsd_integer(x_nn_2)),inference(resolution,[status(thm)],[167534928,166844760]),[]).
%
% cnf(215121144,plain,(rp(x(D),y1(D))|~rp(x_nn_1,D)|xsd_string(x_nn_2)),inference(resolution,[status(thm)],[167469208,166844760]),[]).
%
% cnf(216339648,plain,(rp(x(D),y1(D))|~rp(x_nn_1,D)),inference(forward_subsumption_resolution__resolution,[status(thm)],[215130160,215121144,166870968]),[]).
%
% cnf(221030592,plain,(~$equal(A,y0_nn_1(x_nn_1))|~rp(x_nn_1,A)),inference(forward_subsumption_resolution__resolution,[status(thm)],[218677168,220029816,216339648]),[]).
%
% cnf(221066336,plain,(~cc(x_nn_1)),inference(resolution,[status(thm)],[221030592,166877152]),[]).
%
% cnf(167402968,plain,(~$equal(y1(D),y0(D))|cc(x_nn_1)|xsd_string(x_nn_2)|cowlnothing(x_nn_3)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,166864376,166853832]),[]).
%
% cnf(167498512,plain,(~$equal(y1(D),y0(D))|cc(x_nn_1)|xsd_integer(x_nn_2)|cowlnothing(x_nn_3)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,167402968,166853832]),[]).
%
% cnf(215116488,plain,(~$equal(y1(D),y0(D))|cc(x_nn_1)|xsd_integer(x_nn_2)),inference(resolution,[status(thm)],[167498512,166844760]),[]).
%
% cnf(215107880,plain,(~$equal(y1(D),y0(D))|cc(x_nn_1)|xsd_string(x_nn_2)),inference(resolution,[status(thm)],[167402968,166844760]),[]).
%
% cnf(216124112,plain,(~$equal(y1(D),y0(D))|cc(x_nn_1)),inference(forward_subsumption_resolution__resolution,[status(thm)],[215116488,215107880,166870968]),[]).
%
% cnf(217682200,plain,(~rp(A,y0(F))|~rp(A,y1(F))|~cc(A)|cc(x_nn_1)),inference(resolution,[status(thm)],[166887224,216124112]),[]).
%
% cnf(167417856,plain,(rp(x(D),y1(D))|cc(x_nn_1)|xsd_string(x_nn_2)|cowlnothing(x_nn_3)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,166864376,166853832]),[]).
%
% cnf(167505000,plain,(rp(x(D),y1(D))|cc(x_nn_1)|xsd_integer(x_nn_2)|cowlnothing(x_nn_3)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[the_axiom,167417856,166853832]),[]).
%
% cnf(215094320,plain,(rp(x(D),y1(D))|cc(x_nn_1)|xsd_integer(x_nn_2)),inference(resolution,[status(thm)],[167505000,166844760]),[]).
%
% cnf(215076720,plain,(rp(x(D),y1(D))|cc(x_nn_1)|xsd_string(x_nn_2)),inference(resolution,[status(thm)],[167417856,166844760]),[]).
%
% cnf(215377072,plain,(rp(x(D),y1(D))|cc(x_nn_1)),inference(forward_subsumption_resolution__resolution,[status(thm)],[215094320,215076720,166870968]),[]).
%
% cnf(216406640,plain,(rp(x(y0_nn_1(x_nn_1)),y1(y0_nn_1(x_nn_1)))),inference(forward_subsumption_resolution__resolution,[status(thm)],[215377072,216339648,166877152]),[]).
%
% cnf(contradiction,plain,$false,inference(forward_subsumption_resolution__resolution,[status(thm)],[215169256,216574520,221066336,217682200,216406640]),[]).
%
% END OF PROOF SEQUENCE
% faust: ../JJParser/Signature.c:39: void FreeSignatureList(SymbolNodeType**): Assertion `(*Symbols)->NumberOfUses == 0' failed.
%
%------------------------------------------------------------------------------