%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : KRS138+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:46:07 AM UTC 2026
% Result : Theorem 3.16s 0.85s
% Output : CNFRefutation 3.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 90
% Number of leaves : 10
% Syntax : Number of formulae : 365 ( 18 unt; 0 def)
% Number of atoms : 1615 ( 305 equ)
% Maximal formula atoms : 160 ( 4 avg)
% Number of connectives : 1971 ( 721 ~;1193 |; 45 &)
% ( 4 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 9 con; 0-0 aty)
% Number of variables : 98 ( 3 sgn 26 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(requalityOnA_substitution_1,axiom,
! [A,B,C] :
( ( requalityOnA(A,C)
& A = B )
=> requalityOnA(B,C) ),
file('theBenchmark.p',requalityOnA_substitution_1) ).
fof(requalityOnA_substitution_2,axiom,
! [A,B,C] :
( ( requalityOnA(C,A)
& A = B )
=> requalityOnA(C,B) ),
file('theBenchmark.p',requalityOnA_substitution_2) ).
fof(axiom_0,axiom,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
file('theBenchmark.p',axiom_0) ).
fof(axiom_1,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('theBenchmark.p',axiom_1) ).
fof(axiom_2,axiom,
! [X] :
( cA(X)
<=> ( X = ia
| X = ib ) ),
file('theBenchmark.p',axiom_2) ).
fof(axiom_3,axiom,
! [X,Y,Z] :
( ( requalityOnA(Z,X)
& requalityOnA(Y,X) )
=> Y = Z ),
file('theBenchmark.p',axiom_3) ).
fof(axiom_4,axiom,
! [X,Y] :
( requalityOnA(X,Y)
=> cA(Y) ),
file('theBenchmark.p',axiom_4) ).
fof(the_axiom,conjecture,
( cowlThing(ic)
& cowlThing(ib)
& requalityOnA(ia,ia)
& cowlThing(ia)
& ! [X,Y] :
( requalityOnA(X,Y)
=> requalityOnA(Y,X) )
& ! [X,Y] :
( requalityOnA(X,Y)
=> ( X = ic
| X = ib
| X = ia ) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('theBenchmark.p',the_axiom) ).
fof(the_axiom_neg,negated_conjecture,
~ ( cowlThing(ic)
& cowlThing(ib)
& requalityOnA(ia,ia)
& cowlThing(ia)
& ! [X,Y] :
( requalityOnA(X,Y)
=> requalityOnA(Y,X) )
& ! [X,Y] :
( requalityOnA(X,Y)
=> ( X = ic
| X = ib
| X = ia ) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(assume_negation,[status(cth)],[the_axiom]) ).
cnf(c_17,plain,
( requalityOnA(A,C)
| ~ requalityOnA(B,C)
| A != B ),
inference(clausify,[status(thm)],[requalityOnA_substitution_1]) ).
cnf(c_18,plain,
( requalityOnA(C,A)
| ~ requalityOnA(C,B)
| A != B ),
inference(clausify,[status(thm)],[requalityOnA_substitution_2]) ).
cnf(c_21,plain,
cowlThing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_22,plain,
~ cowlNothing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_23,plain,
( ~ xsd_integer(A)
| ~ xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_24,plain,
( xsd_integer(A)
| xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_25,plain,
( ia = A
| ib = A
| ~ cA(A) ),
inference(clausify,[status(thm)],[axiom_2]) ).
cnf(c_28,plain,
( C = A
| ~ requalityOnA(C,B)
| ~ requalityOnA(A,B) ),
inference(clausify,[status(thm)],[axiom_3]) ).
cnf(c_29,plain,
( cA(B)
| ~ requalityOnA(A,B) ),
inference(clausify,[status(thm)],[axiom_4]) ).
fof(axiom_6,axiom,
requalityOnA(ia,ia),
file('theBenchmark.p',axiom_6) ).
cnf(c_30,plain,
requalityOnA(ia,ia),
inference(clausify,[status(thm)],[axiom_6]) ).
fof(axiom_8,axiom,
requalityOnA(ib,ib),
file('theBenchmark.p',axiom_8) ).
cnf(c_31,plain,
requalityOnA(ib,ib),
inference(clausify,[status(thm)],[axiom_8]) ).
fof(nnf_13,plain,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ? [X,Y] :
( ~ requalityOnA(Y,X)
& requalityOnA(X,Y) )
| ? [X2,X3] :
( ic != X2
& ib != X2
& ia != X2
& requalityOnA(X2,X3) )
| ? [X1] :
( ( xsd_integer(X1)
| ~ xsd_string(X1) )
& ( ~ xsd_integer(X1)
| xsd_string(X1) ) )
| ? [X0] :
( cowlNothing(X0)
| ~ cowlThing(X0) ) ),
inference(fof_nnf,[status(thm)],[the_axiom_neg]) ).
fof(sk_the_axiom_neg_sk,plain,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ( ~ requalityOnA(sK5,sK4)
& requalityOnA(sK4,sK5) )
| ( ic != sK2
& ib != sK2
& ia != sK2
& requalityOnA(sK2,sK3) )
| ( ( xsd_integer(sK1)
| ~ xsd_string(sK1) )
& ( ~ xsd_integer(sK1)
| xsd_string(sK1) ) )
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X,sK4),skolemize(Y,sK5)],[nnf_13]) ).
fof(sk_the_axiom_neg,plain,
( ( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| ic != sK2
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| ic != sK2
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| ib != sK2
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| ib != sK2
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| ia != sK2
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| ia != sK2
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| ic != sK2
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| ic != sK2
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| ib != sK2
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| ib != sK2
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| ia != sK2
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| ia != sK2
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| requalityOnA(sK2,sK3)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ) ),
inference(cnf_transformation,[status(thm)],[sk_the_axiom_neg_sk]) ).
cnf(c_32,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_4275,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_21,c_32]) ).
cnf(c_4276,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_22,c_4275]) ).
cnf(c_4277,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4276]) ).
cnf(c_4278,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_30,c_4277]) ).
cnf(c_4279,negated_conjecture,
( ~ cowlThing(ic)
| requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4278]) ).
cnf(c_33,negated_conjecture,
( requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4279]) ).
cnf(c_34,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| requalityOnA(sK2,sK3)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_4280,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| requalityOnA(sK2,sK3)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_21,c_34]) ).
cnf(c_4281,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| requalityOnA(sK2,sK3)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_22,c_4280]) ).
cnf(c_4282,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ requalityOnA(sK5,sK4)
| requalityOnA(sK2,sK3)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4281]) ).
cnf(c_4283,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(sK5,sK4)
| requalityOnA(sK2,sK3)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_30,c_4282]) ).
cnf(c_4284,negated_conjecture,
( ~ cowlThing(ic)
| ~ requalityOnA(sK5,sK4)
| requalityOnA(sK2,sK3)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4283]) ).
cnf(c_35,negated_conjecture,
( ~ requalityOnA(sK5,sK4)
| requalityOnA(sK2,sK3)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4284]) ).
cnf(c_36,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| ia != sK2
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_4285,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| sK2 != ia
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(copy,[status(thm)],[c_36]) ).
cnf(c_4286,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| sK2 != ia
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_21,c_4285]) ).
cnf(c_4287,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| sK2 != ia
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_22,c_4286]) ).
cnf(c_4288,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| requalityOnA(sK4,sK5)
| sK2 != ia
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4287]) ).
cnf(c_4289,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| requalityOnA(sK4,sK5)
| sK2 != ia
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_30,c_4288]) ).
cnf(c_4290,negated_conjecture,
( ~ cowlThing(ic)
| requalityOnA(sK4,sK5)
| sK2 != ia
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4289]) ).
cnf(c_37,negated_conjecture,
( requalityOnA(sK4,sK5)
| sK2 != ia
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4290]) ).
cnf(c_38,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| ia != sK2
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_4291,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| sK2 != ia
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(copy,[status(thm)],[c_38]) ).
cnf(c_4292,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| sK2 != ia
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_21,c_4291]) ).
cnf(c_4293,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| sK2 != ia
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_22,c_4292]) ).
cnf(c_4294,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ requalityOnA(sK5,sK4)
| sK2 != ia
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4293]) ).
cnf(c_4295,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(sK5,sK4)
| sK2 != ia
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_30,c_4294]) ).
cnf(c_4296,negated_conjecture,
( ~ cowlThing(ic)
| ~ requalityOnA(sK5,sK4)
| sK2 != ia
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4295]) ).
cnf(c_39,negated_conjecture,
( ~ requalityOnA(sK5,sK4)
| sK2 != ia
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4296]) ).
cnf(c_40,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| ib != sK2
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_4297,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| sK2 != ib
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(copy,[status(thm)],[c_40]) ).
cnf(c_4298,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| sK2 != ib
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_21,c_4297]) ).
cnf(c_4299,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| sK2 != ib
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_22,c_4298]) ).
cnf(c_4300,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| requalityOnA(sK4,sK5)
| sK2 != ib
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4299]) ).
cnf(c_4301,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| requalityOnA(sK4,sK5)
| sK2 != ib
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_30,c_4300]) ).
cnf(c_4302,negated_conjecture,
( ~ cowlThing(ic)
| requalityOnA(sK4,sK5)
| sK2 != ib
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4301]) ).
cnf(c_41,negated_conjecture,
( requalityOnA(sK4,sK5)
| sK2 != ib
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4302]) ).
cnf(c_42,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| ib != sK2
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_4303,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| sK2 != ib
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(copy,[status(thm)],[c_42]) ).
cnf(c_4304,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| sK2 != ib
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_21,c_4303]) ).
cnf(c_4305,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| sK2 != ib
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_22,c_4304]) ).
cnf(c_4306,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ requalityOnA(sK5,sK4)
| sK2 != ib
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4305]) ).
cnf(c_4307,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(sK5,sK4)
| sK2 != ib
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_30,c_4306]) ).
cnf(c_4308,negated_conjecture,
( ~ cowlThing(ic)
| ~ requalityOnA(sK5,sK4)
| sK2 != ib
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4307]) ).
cnf(c_43,negated_conjecture,
( ~ requalityOnA(sK5,sK4)
| sK2 != ib
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4308]) ).
cnf(c_48,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_4309,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_21,c_48]) ).
cnf(c_4310,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_22,c_4309]) ).
cnf(c_4311,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4310]) ).
cnf(c_4312,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_30,c_4311]) ).
cnf(c_4313,negated_conjecture,
( ~ cowlThing(ic)
| requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4312]) ).
cnf(c_49,negated_conjecture,
( requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4313]) ).
cnf(c_50,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_4314,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_21,c_50]) ).
cnf(c_4315,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_22,c_4314]) ).
cnf(c_4316,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ requalityOnA(sK5,sK4)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4315]) ).
cnf(c_4317,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(sK5,sK4)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_30,c_4316]) ).
cnf(c_4318,negated_conjecture,
( ~ cowlThing(ic)
| ~ requalityOnA(sK5,sK4)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4317]) ).
cnf(c_51,negated_conjecture,
( ~ requalityOnA(sK5,sK4)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4318]) ).
cnf(c_52,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| ia != sK2
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_4319,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| sK2 != ia
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(copy,[status(thm)],[c_52]) ).
cnf(c_4320,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| sK2 != ia
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_21,c_4319]) ).
cnf(c_4321,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| sK2 != ia
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_22,c_4320]) ).
cnf(c_4322,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| requalityOnA(sK4,sK5)
| sK2 != ia
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4321]) ).
cnf(c_4323,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| requalityOnA(sK4,sK5)
| sK2 != ia
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_30,c_4322]) ).
cnf(c_4324,negated_conjecture,
( ~ cowlThing(ic)
| requalityOnA(sK4,sK5)
| sK2 != ia
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4323]) ).
cnf(c_53,negated_conjecture,
( requalityOnA(sK4,sK5)
| sK2 != ia
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4324]) ).
cnf(c_54,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| ia != sK2
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_4325,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| sK2 != ia
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(copy,[status(thm)],[c_54]) ).
cnf(c_4326,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| sK2 != ia
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_21,c_4325]) ).
cnf(c_4327,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| sK2 != ia
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_22,c_4326]) ).
cnf(c_4328,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ requalityOnA(sK5,sK4)
| sK2 != ia
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4327]) ).
cnf(c_4329,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(sK5,sK4)
| sK2 != ia
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_30,c_4328]) ).
cnf(c_4330,negated_conjecture,
( ~ cowlThing(ic)
| ~ requalityOnA(sK5,sK4)
| sK2 != ia
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4329]) ).
cnf(c_55,negated_conjecture,
( ~ requalityOnA(sK5,sK4)
| sK2 != ia
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4330]) ).
cnf(c_56,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| ib != sK2
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_4331,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| sK2 != ib
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(copy,[status(thm)],[c_56]) ).
cnf(c_4332,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| sK2 != ib
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_21,c_4331]) ).
cnf(c_4333,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| requalityOnA(sK4,sK5)
| sK2 != ib
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_22,c_4332]) ).
cnf(c_4334,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| requalityOnA(sK4,sK5)
| sK2 != ib
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4333]) ).
cnf(c_4335,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| requalityOnA(sK4,sK5)
| sK2 != ib
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_30,c_4334]) ).
cnf(c_4336,negated_conjecture,
( ~ cowlThing(ic)
| requalityOnA(sK4,sK5)
| sK2 != ib
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4335]) ).
cnf(c_57,negated_conjecture,
( requalityOnA(sK4,sK5)
| sK2 != ib
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4336]) ).
cnf(c_58,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| ib != sK2
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_4337,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| sK2 != ib
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(copy,[status(thm)],[c_58]) ).
cnf(c_4338,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| sK2 != ib
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_21,c_4337]) ).
cnf(c_4339,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ requalityOnA(sK5,sK4)
| sK2 != ib
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_22,c_4338]) ).
cnf(c_4340,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ requalityOnA(sK5,sK4)
| sK2 != ib
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4339]) ).
cnf(c_4341,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(sK5,sK4)
| sK2 != ib
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_30,c_4340]) ).
cnf(c_4342,negated_conjecture,
( ~ cowlThing(ic)
| ~ requalityOnA(sK5,sK4)
| sK2 != ib
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4341]) ).
cnf(c_59,negated_conjecture,
( ~ requalityOnA(sK5,sK4)
| sK2 != ib
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_21,c_4342]) ).
cnf(c_68,plain,
( ia = A
| ~ requalityOnA(A,ia) ),
inference(resolve,[status(thm)],[c_30,c_28]) ).
cnf(c_4343,plain,
( requalityOnA(ia,A)
| A != ia ),
inference(resolve,[status(thm)],[c_30,c_18]) ).
cnf(c_69,plain,
( requalityOnA(ia,A)
| ia != A ),
inference(copy,[status(thm)],[c_4343]) ).
cnf(c_4344,plain,
( requalityOnA(A,ia)
| A != ia ),
inference(resolve,[status(thm)],[c_30,c_17]) ).
cnf(c_70,plain,
( requalityOnA(A,ia)
| ia != A ),
inference(copy,[status(thm)],[c_4344]) ).
cnf(c_71,plain,
( ib = A
| ~ requalityOnA(A,ib) ),
inference(resolve,[status(thm)],[c_31,c_28]) ).
cnf(c_4345,plain,
( requalityOnA(ib,A)
| A != ib ),
inference(resolve,[status(thm)],[c_31,c_18]) ).
cnf(c_72,plain,
( requalityOnA(ib,A)
| ib != A ),
inference(copy,[status(thm)],[c_4345]) ).
cnf(c_4346,plain,
( requalityOnA(A,ib)
| A != ib ),
inference(resolve,[status(thm)],[c_31,c_17]) ).
cnf(c_73,plain,
( requalityOnA(A,ib)
| ib != A ),
inference(copy,[status(thm)],[c_4346]) ).
cnf(c_4347,negated_conjecture,
( xsd_string(sK1)
| requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_33,c_24]) ).
cnf(c_74,negated_conjecture,
( requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| xsd_string(sK1) ),
inference(copy,[status(thm)],[c_4347]) ).
cnf(c_4348,negated_conjecture,
( xsd_string(sK1)
| requalityOnA(sK4,sK5)
| sK2 != ia
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_37,c_24]) ).
cnf(c_75,negated_conjecture,
( requalityOnA(sK4,sK5)
| sK2 != ia
| xsd_string(sK1) ),
inference(copy,[status(thm)],[c_4348]) ).
cnf(c_4349,negated_conjecture,
( xsd_string(sK1)
| requalityOnA(sK4,sK5)
| sK2 != ib
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_41,c_24]) ).
cnf(c_76,negated_conjecture,
( requalityOnA(sK4,sK5)
| sK2 != ib
| xsd_string(sK1) ),
inference(copy,[status(thm)],[c_4349]) ).
cnf(c_4350,negated_conjecture,
( xsd_integer(sK1)
| requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_49,c_24]) ).
cnf(c_78,negated_conjecture,
( requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1) ),
inference(copy,[status(thm)],[c_4350]) ).
cnf(c_4351,negated_conjecture,
( xsd_integer(sK1)
| requalityOnA(sK4,sK5)
| sK2 != ia
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_53,c_24]) ).
cnf(c_79,negated_conjecture,
( requalityOnA(sK4,sK5)
| sK2 != ia
| xsd_integer(sK1) ),
inference(copy,[status(thm)],[c_4351]) ).
cnf(c_4352,negated_conjecture,
( xsd_integer(sK1)
| requalityOnA(sK4,sK5)
| sK2 != ib
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_57,c_24]) ).
cnf(c_80,negated_conjecture,
( requalityOnA(sK4,sK5)
| sK2 != ib
| xsd_integer(sK1) ),
inference(copy,[status(thm)],[c_4352]) ).
cnf(c_82,plain,
( ~ xsd_integer(sK1)
| requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3) ),
inference(resolve,[status(thm)],[c_74,c_23]) ).
cnf(c_84,plain,
( cA(sK3)
| requalityOnA(sK4,sK5)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_74,c_29]) ).
cnf(c_88,plain,
( cA(sK5)
| requalityOnA(sK2,sK3)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_74,c_29]) ).
cnf(c_92,plain,
( ~ xsd_integer(sK1)
| cA(sK3)
| requalityOnA(sK4,sK5) ),
inference(resolve,[status(thm)],[c_84,c_23]) ).
cnf(c_108,plain,
( ~ xsd_integer(sK1)
| cA(sK5)
| requalityOnA(sK2,sK3) ),
inference(resolve,[status(thm)],[c_88,c_23]) ).
cnf(c_118,plain,
( cA(sK3)
| requalityOnA(sK4,sK5)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_78,c_29]) ).
cnf(c_122,plain,
( cA(sK5)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_78,c_29]) ).
cnf(c_4353,plain,
( cA(sK3)
| requalityOnA(sK4,sK5)
| cA(sK3)
| requalityOnA(sK4,sK5) ),
inference(resolve,[status(thm)],[c_118,c_92]) ).
cnf(c_4354,plain,
( cA(sK3)
| cA(sK3)
| requalityOnA(sK4,sK5) ),
inference(copy,[status(thm)],[c_4353]) ).
cnf(c_128,plain,
( cA(sK3)
| requalityOnA(sK4,sK5) ),
inference(copy,[status(thm)],[c_4354]) ).
cnf(c_135,plain,
( cA(sK5)
| cA(sK3) ),
inference(resolve,[status(thm)],[c_128,c_29]) ).
cnf(c_4355,plain,
( requalityOnA(sK4,A)
| A != sK5
| cA(sK3) ),
inference(resolve,[status(thm)],[c_128,c_18]) ).
cnf(c_137,plain,
( requalityOnA(sK4,A)
| sK5 != A
| cA(sK3) ),
inference(copy,[status(thm)],[c_4355]) ).
cnf(c_4356,plain,
( ia = sK3
| ib = sK3
| requalityOnA(sK4,sK5) ),
inference(resolve,[status(thm)],[c_128,c_25]) ).
cnf(c_4357,plain,
( ia = sK3
| sK3 = ib
| requalityOnA(sK4,sK5) ),
inference(copy,[status(thm)],[c_4356]) ).
cnf(c_139,plain,
( sK3 = ia
| sK3 = ib
| requalityOnA(sK4,sK5) ),
inference(copy,[status(thm)],[c_4357]) ).
cnf(c_4358,plain,
( ia = sK3
| ib = sK3
| cA(sK5) ),
inference(resolve,[status(thm)],[c_135,c_25]) ).
cnf(c_4359,plain,
( ia = sK3
| sK3 = ib
| cA(sK5) ),
inference(copy,[status(thm)],[c_4358]) ).
cnf(c_141,plain,
( sK3 = ia
| sK3 = ib
| cA(sK5) ),
inference(copy,[status(thm)],[c_4359]) ).
cnf(c_4360,plain,
( ia = sK5
| ib = sK5
| cA(sK3) ),
inference(resolve,[status(thm)],[c_135,c_25]) ).
cnf(c_4361,plain,
( ia = sK5
| sK5 = ib
| cA(sK3) ),
inference(copy,[status(thm)],[c_4360]) ).
cnf(c_143,plain,
( sK5 = ia
| sK5 = ib
| cA(sK3) ),
inference(copy,[status(thm)],[c_4361]) ).
cnf(c_4362,plain,
( cA(sK5)
| requalityOnA(sK2,sK3)
| cA(sK5)
| requalityOnA(sK2,sK3) ),
inference(resolve,[status(thm)],[c_122,c_108]) ).
cnf(c_4363,plain,
( cA(sK5)
| cA(sK5)
| requalityOnA(sK2,sK3) ),
inference(copy,[status(thm)],[c_4362]) ).
cnf(c_147,plain,
( cA(sK5)
| requalityOnA(sK2,sK3) ),
inference(copy,[status(thm)],[c_4363]) ).
cnf(c_153,plain,
( sK2 = A
| ~ requalityOnA(A,sK3)
| cA(sK5) ),
inference(resolve,[status(thm)],[c_147,c_28]) ).
cnf(c_4364,plain,
( requalityOnA(sK2,A)
| A != sK3
| cA(sK5) ),
inference(resolve,[status(thm)],[c_147,c_18]) ).
cnf(c_154,plain,
( requalityOnA(sK2,A)
| sK3 != A
| cA(sK5) ),
inference(copy,[status(thm)],[c_4364]) ).
cnf(c_4365,plain,
( requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3)
| requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3) ),
inference(resolve,[status(thm)],[c_82,c_78]) ).
cnf(c_4366,plain,
( requalityOnA(sK4,sK5)
| requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3) ),
inference(copy,[status(thm)],[c_4365]) ).
cnf(c_158,plain,
( requalityOnA(sK4,sK5)
| requalityOnA(sK2,sK3) ),
inference(copy,[status(thm)],[c_4366]) ).
cnf(c_159,plain,
( sK2 = A
| ~ requalityOnA(A,sK3)
| requalityOnA(sK4,sK5) ),
inference(resolve,[status(thm)],[c_158,c_28]) ).
cnf(c_4367,plain,
( requalityOnA(sK2,A)
| A != sK3
| requalityOnA(sK4,sK5) ),
inference(resolve,[status(thm)],[c_158,c_18]) ).
cnf(c_160,plain,
( requalityOnA(sK2,A)
| sK3 != A
| requalityOnA(sK4,sK5) ),
inference(copy,[status(thm)],[c_4367]) ).
cnf(c_4368,plain,
( requalityOnA(A,ib)
| A != ib ),
inference(copy,[status(thm)],[c_73]) ).
cnf(c_169,plain,
( requalityOnA(sK3,ib)
| sK3 = ia
| cA(sK5) ),
inference(resolve,[status(thm)],[c_141,c_4368]) ).
cnf(c_4369,plain,
( requalityOnA(ib,A)
| A != ib ),
inference(copy,[status(thm)],[c_72]) ).
cnf(c_170,plain,
( requalityOnA(ib,sK3)
| sK3 = ia
| cA(sK5) ),
inference(resolve,[status(thm)],[c_141,c_4369]) ).
cnf(c_4370,plain,
( requalityOnA(ib,A)
| A != ib ),
inference(copy,[status(thm)],[c_72]) ).
cnf(c_181,plain,
( requalityOnA(ib,sK3)
| sK3 = ia
| requalityOnA(sK4,sK5) ),
inference(resolve,[status(thm)],[c_139,c_4370]) ).
cnf(c_4371,plain,
( requalityOnA(sK4,ib)
| cA(sK3)
| sK5 = ia
| cA(sK3) ),
inference(resolve,[status(thm)],[c_143,c_137]) ).
cnf(c_187,plain,
( requalityOnA(sK4,ib)
| sK5 = ia
| cA(sK3) ),
inference(copy,[status(thm)],[c_4371]) ).
cnf(c_4372,plain,
( requalityOnA(A,ib)
| A != ib ),
inference(copy,[status(thm)],[c_73]) ).
cnf(c_190,plain,
( requalityOnA(sK5,ib)
| sK5 = ia
| cA(sK3) ),
inference(resolve,[status(thm)],[c_143,c_4372]) ).
cnf(c_4373,plain,
( sK3 = ia
| cA(sK5)
| requalityOnA(sK2,ib)
| cA(sK5) ),
inference(resolve,[status(thm)],[c_154,c_141]) ).
cnf(c_198,plain,
( sK3 = ia
| requalityOnA(sK2,ib)
| cA(sK5) ),
inference(copy,[status(thm)],[c_4373]) ).
cnf(c_206,plain,
( sK3 = A
| ~ requalityOnA(A,ib)
| sK3 = ia
| cA(sK5) ),
inference(resolve,[status(thm)],[c_169,c_28]) ).
cnf(c_4374,plain,
( requalityOnA(sK3,A)
| A != ib
| sK3 = ia
| cA(sK5) ),
inference(resolve,[status(thm)],[c_169,c_18]) ).
cnf(c_207,plain,
( requalityOnA(sK3,A)
| ib != A
| sK3 = ia
| cA(sK5) ),
inference(copy,[status(thm)],[c_4374]) ).
cnf(c_4375,plain,
( sK2 = ib
| cA(sK5)
| sK3 = ia
| cA(sK5) ),
inference(resolve,[status(thm)],[c_170,c_153]) ).
cnf(c_217,plain,
( sK2 = ib
| sK3 = ia
| cA(sK5) ),
inference(copy,[status(thm)],[c_4375]) ).
cnf(c_4376,plain,
( ib = sK4
| sK5 = ia
| cA(sK3) ),
inference(resolve,[status(thm)],[c_187,c_71]) ).
cnf(c_261,plain,
( sK4 = ib
| sK5 = ia
| cA(sK3) ),
inference(copy,[status(thm)],[c_4376]) ).
cnf(c_4377,plain,
( requalityOnA(sK5,A)
| A != ib
| sK5 = ia
| cA(sK3) ),
inference(resolve,[status(thm)],[c_190,c_18]) ).
cnf(c_273,plain,
( requalityOnA(sK5,A)
| ib != A
| sK5 = ia
| cA(sK3) ),
inference(copy,[status(thm)],[c_4377]) ).
cnf(c_4378,plain,
( sK2 = ib
| requalityOnA(sK4,sK5)
| sK3 = ia
| requalityOnA(sK4,sK5) ),
inference(resolve,[status(thm)],[c_181,c_159]) ).
cnf(c_593,plain,
( sK2 = ib
| sK3 = ia
| requalityOnA(sK4,sK5) ),
inference(copy,[status(thm)],[c_4378]) ).
cnf(c_4379,plain,
( sK3 = ia
| cA(sK5)
| sK3 = sK2
| sK3 = ia
| cA(sK5) ),
inference(resolve,[status(thm)],[c_206,c_198]) ).
cnf(c_4380,plain,
( sK3 = ia
| sK3 = sK2
| sK3 = ia
| cA(sK5) ),
inference(copy,[status(thm)],[c_4379]) ).
cnf(c_854,plain,
( sK3 = sK2
| sK3 = ia
| cA(sK5) ),
inference(copy,[status(thm)],[c_4380]) ).
cnf(c_4381,plain,
( ib = sK2
| sK3 = ia
| cA(sK5) ),
inference(copy,[status(thm)],[c_217]) ).
cnf(c_4382,plain,
( sK3 = ia
| cA(sK5)
| requalityOnA(sK3,sK2)
| sK3 = ia
| cA(sK5) ),
inference(resolve,[status(thm)],[c_207,c_4381]) ).
cnf(c_4383,plain,
( sK3 = ia
| requalityOnA(sK3,sK2)
| sK3 = ia
| cA(sK5) ),
inference(copy,[status(thm)],[c_4382]) ).
cnf(c_859,plain,
( requalityOnA(sK3,sK2)
| sK3 = ia
| cA(sK5) ),
inference(copy,[status(thm)],[c_4383]) ).
cnf(c_4384,plain,
( requalityOnA(sK2,ia)
| cA(sK5)
| sK3 = sK2
| cA(sK5) ),
inference(resolve,[status(thm)],[c_854,c_154]) ).
cnf(c_1140,plain,
( requalityOnA(sK2,ia)
| sK3 = sK2
| cA(sK5) ),
inference(copy,[status(thm)],[c_4384]) ).
cnf(c_4385,plain,
( requalityOnA(A,ia)
| A != ia ),
inference(copy,[status(thm)],[c_70]) ).
cnf(c_1143,plain,
( requalityOnA(sK3,ia)
| sK3 = sK2
| cA(sK5) ),
inference(resolve,[status(thm)],[c_854,c_4385]) ).
cnf(c_4386,plain,
( requalityOnA(sK2,ia)
| cA(sK5)
| requalityOnA(sK3,sK2)
| cA(sK5) ),
inference(resolve,[status(thm)],[c_859,c_154]) ).
cnf(c_1152,plain,
( requalityOnA(sK2,ia)
| requalityOnA(sK3,sK2)
| cA(sK5) ),
inference(copy,[status(thm)],[c_4386]) ).
cnf(c_4387,plain,
( requalityOnA(A,ia)
| A != ia ),
inference(copy,[status(thm)],[c_70]) ).
cnf(c_1155,plain,
( requalityOnA(sK3,ia)
| requalityOnA(sK3,sK2)
| cA(sK5) ),
inference(resolve,[status(thm)],[c_859,c_4387]) ).
cnf(c_1513,plain,
( sK3 = A
| ~ requalityOnA(A,ia)
| sK3 = sK2
| cA(sK5) ),
inference(resolve,[status(thm)],[c_1143,c_28]) ).
cnf(c_1516,plain,
( ~ requalityOnA(sK2,ia)
| sK3 = sK2
| cA(sK5) ),
inference(factor,[status(thm)],[c_1513]) ).
cnf(c_4388,plain,
( ia = sK2
| requalityOnA(sK3,sK2)
| cA(sK5) ),
inference(resolve,[status(thm)],[c_1152,c_68]) ).
cnf(c_1539,plain,
( sK2 = ia
| requalityOnA(sK3,sK2)
| cA(sK5) ),
inference(copy,[status(thm)],[c_4388]) ).
cnf(c_4389,plain,
( requalityOnA(sK3,A)
| A != ia
| requalityOnA(sK3,sK2)
| cA(sK5) ),
inference(resolve,[status(thm)],[c_1155,c_18]) ).
cnf(c_1549,plain,
( requalityOnA(sK3,A)
| ia != A
| requalityOnA(sK3,sK2)
| cA(sK5) ),
inference(copy,[status(thm)],[c_4389]) ).
cnf(c_4390,plain,
( ia != sK2
| requalityOnA(sK3,sK2)
| cA(sK5) ),
inference(factor,[status(thm)],[c_1549]) ).
cnf(c_1552,plain,
( sK2 != ia
| requalityOnA(sK3,sK2)
| cA(sK5) ),
inference(copy,[status(thm)],[c_4390]) ).
cnf(c_4391,plain,
( ib = sK4
| sK5 = ia
| cA(sK3) ),
inference(copy,[status(thm)],[c_261]) ).
cnf(c_4392,plain,
( sK5 = ia
| cA(sK3)
| requalityOnA(sK5,sK4)
| sK5 = ia
| cA(sK3) ),
inference(resolve,[status(thm)],[c_273,c_4391]) ).
cnf(c_4393,plain,
( sK5 = ia
| requalityOnA(sK5,sK4)
| sK5 = ia
| cA(sK3) ),
inference(copy,[status(thm)],[c_4392]) ).
cnf(c_1812,plain,
( requalityOnA(sK5,sK4)
| sK5 = ia
| cA(sK3) ),
inference(copy,[status(thm)],[c_4393]) ).
cnf(c_4394,plain,
( sK3 = sK2
| cA(sK5)
| sK3 = sK2
| cA(sK5) ),
inference(resolve,[status(thm)],[c_1516,c_1140]) ).
cnf(c_4395,plain,
( sK3 = sK2
| sK3 = sK2
| cA(sK5) ),
inference(copy,[status(thm)],[c_4394]) ).
cnf(c_1922,plain,
( sK3 = sK2
| cA(sK5) ),
inference(copy,[status(thm)],[c_4395]) ).
cnf(c_4396,plain,
( requalityOnA(sK2,sK2)
| cA(sK5)
| cA(sK5) ),
inference(resolve,[status(thm)],[c_1922,c_154]) ).
cnf(c_1927,plain,
( requalityOnA(sK2,sK2)
| cA(sK5) ),
inference(copy,[status(thm)],[c_4396]) ).
cnf(c_1942,plain,
( sK2 = A
| ~ requalityOnA(A,sK2)
| cA(sK5) ),
inference(resolve,[status(thm)],[c_1927,c_28]) ).
cnf(c_4397,plain,
( requalityOnA(sK3,sK2)
| cA(sK5)
| requalityOnA(sK3,sK2)
| cA(sK5) ),
inference(resolve,[status(thm)],[c_1552,c_1539]) ).
cnf(c_4398,plain,
( requalityOnA(sK3,sK2)
| requalityOnA(sK3,sK2)
| cA(sK5) ),
inference(copy,[status(thm)],[c_4397]) ).
cnf(c_1985,plain,
( requalityOnA(sK3,sK2)
| cA(sK5) ),
inference(copy,[status(thm)],[c_4398]) ).
cnf(c_4399,plain,
( requalityOnA(A,sK2)
| A != sK3
| cA(sK5) ),
inference(resolve,[status(thm)],[c_1985,c_17]) ).
cnf(c_1990,plain,
( requalityOnA(A,sK2)
| sK3 != A
| cA(sK5) ),
inference(copy,[status(thm)],[c_4399]) ).
cnf(c_4400,plain,
( requalityOnA(sK4,ia)
| cA(sK3)
| requalityOnA(sK5,sK4)
| cA(sK3) ),
inference(resolve,[status(thm)],[c_1812,c_137]) ).
cnf(c_2072,plain,
( requalityOnA(sK4,ia)
| requalityOnA(sK5,sK4)
| cA(sK3) ),
inference(copy,[status(thm)],[c_4400]) ).
cnf(c_4401,plain,
( requalityOnA(A,ia)
| A != ia ),
inference(copy,[status(thm)],[c_70]) ).
cnf(c_2075,plain,
( requalityOnA(sK5,ia)
| requalityOnA(sK5,sK4)
| cA(sK3) ),
inference(resolve,[status(thm)],[c_1812,c_4401]) ).
cnf(c_4402,plain,
( ia = sK4
| requalityOnA(sK5,sK4)
| cA(sK3) ),
inference(resolve,[status(thm)],[c_2072,c_68]) ).
cnf(c_2248,plain,
( sK4 = ia
| requalityOnA(sK5,sK4)
| cA(sK3) ),
inference(copy,[status(thm)],[c_4402]) ).
cnf(c_4403,plain,
( requalityOnA(sK5,A)
| A != ia
| requalityOnA(sK5,sK4)
| cA(sK3) ),
inference(resolve,[status(thm)],[c_2075,c_18]) ).
cnf(c_2266,plain,
( requalityOnA(sK5,A)
| ia != A
| requalityOnA(sK5,sK4)
| cA(sK3) ),
inference(copy,[status(thm)],[c_4403]) ).
cnf(c_4404,plain,
( ia != sK4
| requalityOnA(sK5,sK4)
| cA(sK3) ),
inference(factor,[status(thm)],[c_2266]) ).
cnf(c_2269,plain,
( sK4 != ia
| requalityOnA(sK5,sK4)
| cA(sK3) ),
inference(copy,[status(thm)],[c_4404]) ).
cnf(c_4405,plain,
( requalityOnA(sK5,sK4)
| cA(sK3)
| requalityOnA(sK5,sK4)
| cA(sK3) ),
inference(resolve,[status(thm)],[c_2269,c_2248]) ).
cnf(c_4406,plain,
( requalityOnA(sK5,sK4)
| requalityOnA(sK5,sK4)
| cA(sK3) ),
inference(copy,[status(thm)],[c_4405]) ).
cnf(c_2470,plain,
( requalityOnA(sK5,sK4)
| cA(sK3) ),
inference(copy,[status(thm)],[c_4406]) ).
cnf(c_2476,plain,
( requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cA(sK3) ),
inference(resolve,[status(thm)],[c_2470,c_51]) ).
cnf(c_2480,plain,
( requalityOnA(sK2,sK3)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cA(sK3) ),
inference(resolve,[status(thm)],[c_2470,c_35]) ).
cnf(c_4407,plain,
( requalityOnA(sK4,sK5)
| xsd_integer(sK1)
| sK3 = ia
| requalityOnA(sK4,sK5) ),
inference(resolve,[status(thm)],[c_593,c_80]) ).
cnf(c_2714,plain,
( xsd_integer(sK1)
| sK3 = ia
| requalityOnA(sK4,sK5) ),
inference(copy,[status(thm)],[c_4407]) ).
cnf(c_4408,plain,
( requalityOnA(sK4,sK5)
| xsd_string(sK1)
| sK3 = ia
| requalityOnA(sK4,sK5) ),
inference(resolve,[status(thm)],[c_593,c_76]) ).
cnf(c_2715,plain,
( xsd_string(sK1)
| sK3 = ia
| requalityOnA(sK4,sK5) ),
inference(copy,[status(thm)],[c_4408]) ).
cnf(c_2720,plain,
( cA(sK5)
| xsd_integer(sK1)
| sK3 = ia ),
inference(resolve,[status(thm)],[c_2714,c_29]) ).
cnf(c_4409,plain,
( requalityOnA(ia,sK2)
| cA(sK5)
| cA(sK5)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_2720,c_1990]) ).
cnf(c_2731,plain,
( requalityOnA(ia,sK2)
| cA(sK5)
| xsd_integer(sK1) ),
inference(copy,[status(thm)],[c_4409]) ).
cnf(c_4410,plain,
( sK2 = ia
| cA(sK5)
| cA(sK5)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_2731,c_1942]) ).
cnf(c_2745,plain,
( sK2 = ia
| cA(sK5)
| xsd_integer(sK1) ),
inference(copy,[status(thm)],[c_4410]) ).
cnf(c_4411,plain,
( requalityOnA(sK4,sK5)
| xsd_integer(sK1)
| cA(sK5)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_2745,c_79]) ).
cnf(c_2776,plain,
( requalityOnA(sK4,sK5)
| cA(sK5)
| xsd_integer(sK1) ),
inference(copy,[status(thm)],[c_4411]) ).
cnf(c_4412,plain,
( cA(sK5)
| cA(sK5)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_2776,c_29]) ).
cnf(c_2782,plain,
( cA(sK5)
| xsd_integer(sK1) ),
inference(copy,[status(thm)],[c_4412]) ).
cnf(c_2804,plain,
( cA(sK5)
| xsd_string(sK1)
| sK3 = ia ),
inference(resolve,[status(thm)],[c_2715,c_29]) ).
cnf(c_2814,plain,
( ~ xsd_integer(sK1)
| sK3 = ia
| requalityOnA(sK4,sK5) ),
inference(resolve,[status(thm)],[c_2715,c_23]) ).
cnf(c_2824,plain,
( ~ xsd_integer(sK1)
| cA(sK5)
| sK3 = ia ),
inference(resolve,[status(thm)],[c_2804,c_23]) ).
cnf(c_4413,plain,
( cA(sK5)
| cA(sK5)
| sK3 = ia ),
inference(resolve,[status(thm)],[c_2824,c_2782]) ).
cnf(c_2866,plain,
( cA(sK5)
| sK3 = ia ),
inference(copy,[status(thm)],[c_4413]) ).
cnf(c_4414,plain,
( requalityOnA(ia,sK2)
| cA(sK5)
| cA(sK5) ),
inference(resolve,[status(thm)],[c_2866,c_1990]) ).
cnf(c_2867,plain,
( requalityOnA(ia,sK2)
| cA(sK5) ),
inference(copy,[status(thm)],[c_4414]) ).
cnf(c_4415,plain,
( sK2 = ia
| cA(sK5)
| cA(sK5) ),
inference(resolve,[status(thm)],[c_2867,c_1942]) ).
cnf(c_2880,plain,
( sK2 = ia
| cA(sK5) ),
inference(copy,[status(thm)],[c_4415]) ).
cnf(c_2918,plain,
( requalityOnA(sK4,sK5)
| xsd_string(sK1)
| cA(sK5) ),
inference(resolve,[status(thm)],[c_2880,c_75]) ).
cnf(c_4416,plain,
( cA(sK5)
| xsd_string(sK1)
| cA(sK5) ),
inference(resolve,[status(thm)],[c_2918,c_29]) ).
cnf(c_2955,plain,
( xsd_string(sK1)
| cA(sK5) ),
inference(copy,[status(thm)],[c_4416]) ).
cnf(c_2958,plain,
( ~ xsd_integer(sK1)
| cA(sK5) ),
inference(resolve,[status(thm)],[c_2955,c_23]) ).
cnf(c_4417,plain,
( cA(sK5)
| cA(sK5) ),
inference(resolve,[status(thm)],[c_2958,c_2782]) ).
cnf(c_2988,plain,
cA(sK5),
inference(copy,[status(thm)],[c_4417]) ).
cnf(c_4418,plain,
( ia = sK5
| ib = sK5 ),
inference(resolve,[status(thm)],[c_2988,c_25]) ).
cnf(c_4419,plain,
( ia = sK5
| sK5 = ib ),
inference(copy,[status(thm)],[c_4418]) ).
cnf(c_2989,plain,
( sK5 = ia
| sK5 = ib ),
inference(copy,[status(thm)],[c_4419]) ).
cnf(c_4420,plain,
( requalityOnA(A,ib)
| A != ib ),
inference(copy,[status(thm)],[c_73]) ).
cnf(c_2993,plain,
( requalityOnA(sK5,ib)
| sK5 = ia ),
inference(resolve,[status(thm)],[c_2989,c_4420]) ).
cnf(c_3004,plain,
( sK5 = A
| ~ requalityOnA(A,ib)
| sK5 = ia ),
inference(resolve,[status(thm)],[c_2993,c_28]) ).
cnf(c_4421,plain,
( sK3 = ia
| requalityOnA(sK4,sK5)
| sK3 = ia
| requalityOnA(sK4,sK5) ),
inference(resolve,[status(thm)],[c_2814,c_2714]) ).
cnf(c_4422,plain,
( sK3 = ia
| sK3 = ia
| requalityOnA(sK4,sK5) ),
inference(copy,[status(thm)],[c_4421]) ).
cnf(c_3313,plain,
( sK3 = ia
| requalityOnA(sK4,sK5) ),
inference(copy,[status(thm)],[c_4422]) ).
cnf(c_4423,plain,
( requalityOnA(sK2,ia)
| requalityOnA(sK4,sK5)
| requalityOnA(sK4,sK5) ),
inference(resolve,[status(thm)],[c_3313,c_160]) ).
cnf(c_3317,plain,
( requalityOnA(sK2,ia)
| requalityOnA(sK4,sK5) ),
inference(copy,[status(thm)],[c_4423]) ).
cnf(c_4424,plain,
( ia = sK2
| requalityOnA(sK4,sK5) ),
inference(resolve,[status(thm)],[c_3317,c_68]) ).
cnf(c_3337,plain,
( sK2 = ia
| requalityOnA(sK4,sK5) ),
inference(copy,[status(thm)],[c_4424]) ).
cnf(c_4425,plain,
( requalityOnA(sK4,sK5)
| xsd_integer(sK1)
| requalityOnA(sK4,sK5) ),
inference(resolve,[status(thm)],[c_3337,c_79]) ).
cnf(c_3356,plain,
( xsd_integer(sK1)
| requalityOnA(sK4,sK5) ),
inference(copy,[status(thm)],[c_4425]) ).
cnf(c_4426,plain,
( requalityOnA(sK4,sK5)
| xsd_string(sK1)
| requalityOnA(sK4,sK5) ),
inference(resolve,[status(thm)],[c_3337,c_75]) ).
cnf(c_3357,plain,
( xsd_string(sK1)
| requalityOnA(sK4,sK5) ),
inference(copy,[status(thm)],[c_4426]) ).
cnf(c_3369,plain,
( ~ xsd_integer(sK1)
| requalityOnA(sK4,sK5) ),
inference(resolve,[status(thm)],[c_3357,c_23]) ).
cnf(c_4427,plain,
( requalityOnA(sK4,sK5)
| requalityOnA(sK4,sK5) ),
inference(resolve,[status(thm)],[c_3369,c_3356]) ).
cnf(c_3375,plain,
requalityOnA(sK4,sK5),
inference(copy,[status(thm)],[c_4427]) ).
cnf(c_4428,plain,
( requalityOnA(sK4,A)
| A != sK5 ),
inference(resolve,[status(thm)],[c_3375,c_18]) ).
cnf(c_3377,plain,
( requalityOnA(sK4,A)
| sK5 != A ),
inference(copy,[status(thm)],[c_4428]) ).
cnf(c_4429,plain,
( requalityOnA(A,sK5)
| A != sK4 ),
inference(resolve,[status(thm)],[c_3375,c_17]) ).
cnf(c_3378,plain,
( requalityOnA(A,sK5)
| sK4 != A ),
inference(copy,[status(thm)],[c_4429]) ).
cnf(c_3398,plain,
( sK5 = ia
| requalityOnA(sK4,ib) ),
inference(resolve,[status(thm)],[c_3377,c_2989]) ).
cnf(c_4430,plain,
( xsd_integer(sK1)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| cA(sK3) ),
inference(resolve,[status(thm)],[c_2476,c_24]) ).
cnf(c_3883,plain,
( requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| cA(sK3) ),
inference(copy,[status(thm)],[c_4430]) ).
cnf(c_4431,plain,
( xsd_string(sK1)
| requalityOnA(sK2,sK3)
| xsd_string(sK1)
| cA(sK3) ),
inference(resolve,[status(thm)],[c_2480,c_24]) ).
cnf(c_3898,plain,
( requalityOnA(sK2,sK3)
| xsd_string(sK1)
| cA(sK3) ),
inference(copy,[status(thm)],[c_4431]) ).
cnf(c_4432,plain,
( sK5 = ia
| sK5 = sK4
| sK5 = ia ),
inference(resolve,[status(thm)],[c_3004,c_3398]) ).
cnf(c_3904,plain,
( sK5 = sK4
| sK5 = ia ),
inference(copy,[status(thm)],[c_4432]) ).
cnf(c_3905,plain,
( requalityOnA(sK4,ia)
| sK5 = sK4 ),
inference(resolve,[status(thm)],[c_3904,c_3377]) ).
cnf(c_4433,plain,
( requalityOnA(A,ia)
| A != ia ),
inference(copy,[status(thm)],[c_70]) ).
cnf(c_3908,plain,
( requalityOnA(sK5,ia)
| sK5 = sK4 ),
inference(resolve,[status(thm)],[c_3904,c_4433]) ).
cnf(c_3924,plain,
( sK5 = A
| ~ requalityOnA(A,ia)
| sK5 = sK4 ),
inference(resolve,[status(thm)],[c_3908,c_28]) ).
cnf(c_3927,plain,
( ~ requalityOnA(sK4,ia)
| sK5 = sK4 ),
inference(factor,[status(thm)],[c_3924]) ).
cnf(c_4434,plain,
( sK5 = sK4
| sK5 = sK4 ),
inference(resolve,[status(thm)],[c_3927,c_3905]) ).
cnf(c_3987,plain,
sK5 = sK4,
inference(copy,[status(thm)],[c_4434]) ).
cnf(c_4435,plain,
( requalityOnA(A,sK5)
| A != sK4 ),
inference(copy,[status(thm)],[c_3378]) ).
cnf(c_3991,plain,
requalityOnA(sK5,sK5),
inference(resolve,[status(thm)],[c_3987,c_4435]) ).
cnf(c_3998,plain,
requalityOnA(sK5,sK4),
inference(paramod,[status(thm)],[c_3987,c_3991]) ).
cnf(c_4000,negated_conjecture,
( sK2 != ib
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_3998,c_59]) ).
cnf(c_4001,negated_conjecture,
( sK2 != ia
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_3998,c_55]) ).
cnf(c_4002,negated_conjecture,
( requalityOnA(sK2,sK3)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_3998,c_51]) ).
cnf(c_4004,negated_conjecture,
( sK2 != ib
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_3998,c_43]) ).
cnf(c_4005,negated_conjecture,
( sK2 != ia
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_3998,c_39]) ).
cnf(c_4006,negated_conjecture,
( requalityOnA(sK2,sK3)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_3998,c_35]) ).
cnf(c_4436,plain,
( cA(sK3)
| xsd_integer(sK1)
| cA(sK3) ),
inference(resolve,[status(thm)],[c_3883,c_29]) ).
cnf(c_4019,plain,
( xsd_integer(sK1)
| cA(sK3) ),
inference(copy,[status(thm)],[c_4436]) ).
cnf(c_4437,plain,
( cA(sK3)
| xsd_string(sK1)
| cA(sK3) ),
inference(resolve,[status(thm)],[c_3898,c_29]) ).
cnf(c_4027,plain,
( xsd_string(sK1)
| cA(sK3) ),
inference(copy,[status(thm)],[c_4437]) ).
cnf(c_4030,plain,
( ~ xsd_integer(sK1)
| cA(sK3) ),
inference(resolve,[status(thm)],[c_4027,c_23]) ).
cnf(c_4438,plain,
( cA(sK3)
| cA(sK3) ),
inference(resolve,[status(thm)],[c_4030,c_4019]) ).
cnf(c_4032,plain,
cA(sK3),
inference(copy,[status(thm)],[c_4438]) ).
cnf(c_4439,plain,
( ia = sK3
| ib = sK3 ),
inference(resolve,[status(thm)],[c_4032,c_25]) ).
cnf(c_4440,plain,
( ia = sK3
| sK3 = ib ),
inference(copy,[status(thm)],[c_4439]) ).
cnf(c_4033,plain,
( sK3 = ia
| sK3 = ib ),
inference(copy,[status(thm)],[c_4440]) ).
cnf(c_4441,plain,
( requalityOnA(ib,A)
| A != ib ),
inference(copy,[status(thm)],[c_72]) ).
cnf(c_4045,plain,
( requalityOnA(ib,sK3)
| sK3 = ia ),
inference(resolve,[status(thm)],[c_4033,c_4441]) ).
cnf(c_4442,plain,
( requalityOnA(ia,A)
| A != ia ),
inference(copy,[status(thm)],[c_69]) ).
cnf(c_4083,plain,
( requalityOnA(ia,sK3)
| requalityOnA(ib,sK3) ),
inference(resolve,[status(thm)],[c_4045,c_4442]) ).
cnf(c_4443,negated_conjecture,
( xsd_integer(sK1)
| sK2 != ib
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_4000,c_24]) ).
cnf(c_4170,negated_conjecture,
( sK2 != ib
| xsd_integer(sK1) ),
inference(copy,[status(thm)],[c_4443]) ).
cnf(c_4444,negated_conjecture,
( xsd_integer(sK1)
| sK2 != ia
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_4001,c_24]) ).
cnf(c_4171,negated_conjecture,
( sK2 != ia
| xsd_integer(sK1) ),
inference(copy,[status(thm)],[c_4444]) ).
cnf(c_4445,negated_conjecture,
( xsd_integer(sK1)
| requalityOnA(sK2,sK3)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_4002,c_24]) ).
cnf(c_4178,negated_conjecture,
( requalityOnA(sK2,sK3)
| xsd_integer(sK1) ),
inference(copy,[status(thm)],[c_4445]) ).
cnf(c_4446,negated_conjecture,
( xsd_string(sK1)
| sK2 != ib
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_4004,c_24]) ).
cnf(c_4186,negated_conjecture,
( sK2 != ib
| xsd_string(sK1) ),
inference(copy,[status(thm)],[c_4446]) ).
cnf(c_4447,negated_conjecture,
( xsd_string(sK1)
| sK2 != ia
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_4005,c_24]) ).
cnf(c_4194,negated_conjecture,
( sK2 != ia
| xsd_string(sK1) ),
inference(copy,[status(thm)],[c_4447]) ).
cnf(c_4448,negated_conjecture,
( requalityOnA(sK2,sK3)
| requalityOnA(sK2,sK3)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_4006,c_4178]) ).
cnf(c_4195,negated_conjecture,
( requalityOnA(sK2,sK3)
| xsd_string(sK1) ),
inference(copy,[status(thm)],[c_4448]) ).
cnf(c_4196,plain,
( ~ xsd_integer(sK1)
| requalityOnA(sK2,sK3) ),
inference(resolve,[status(thm)],[c_4195,c_23]) ).
cnf(c_4449,plain,
( requalityOnA(sK2,sK3)
| requalityOnA(sK2,sK3) ),
inference(resolve,[status(thm)],[c_4196,c_4178]) ).
cnf(c_4201,plain,
requalityOnA(sK2,sK3),
inference(copy,[status(thm)],[c_4449]) ).
cnf(c_4205,plain,
( sK2 = A
| ~ requalityOnA(A,sK3) ),
inference(resolve,[status(thm)],[c_4201,c_28]) ).
cnf(c_4208,plain,
( requalityOnA(ib,sK3)
| sK2 = ia ),
inference(resolve,[status(thm)],[c_4205,c_4083]) ).
cnf(c_4220,plain,
( xsd_string(sK1)
| requalityOnA(ib,sK3) ),
inference(resolve,[status(thm)],[c_4208,c_4194]) ).
cnf(c_4221,plain,
( xsd_integer(sK1)
| requalityOnA(ib,sK3) ),
inference(resolve,[status(thm)],[c_4208,c_4171]) ).
cnf(c_4241,plain,
( sK2 = ib
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_4220,c_4205]) ).
cnf(c_4253,plain,
( sK2 = ib
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_4221,c_4205]) ).
cnf(c_4450,plain,
( xsd_string(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_4241,c_4186]) ).
cnf(c_4265,plain,
xsd_string(sK1),
inference(copy,[status(thm)],[c_4450]) ).
cnf(c_4266,plain,
~ xsd_integer(sK1),
inference(resolve,[status(thm)],[c_4265,c_23]) ).
cnf(c_4271,plain,
sK2 = ib,
inference(resolve,[status(thm)],[c_4266,c_4253]) ).
cnf(c_4451,negated_conjecture,
sK2 != ib,
inference(resolve,[status(thm)],[c_4266,c_4170]) ).
cnf(c_4274,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_4271,c_4451]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS138+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n017.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Fri Sep 25 19:36:19 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.36 % Process 2987013 was started by sandbox on n017,
% 0.13/0.36 % Fri Sep 25 19:36:19 2026
% 0.13/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.13/0.37
% 0.13/0.37 % From the command line: assign(max_seconds, 300).
% 3.16/0.85
% 3.16/0.85 % given #500 (W,wt=14): 424 cA(c6) | c4 = ia | xsd_integer(ib) | -xsd_integer(c4). [resolve(168,d,23,a)].
% 3.16/0.85
% 3.16/0.85 % SZS status Theorem for theBenchmark
% 3.16/0.85
% 3.16/0.85 % Proof 1 at 0.33 (+ 0.13) seconds.
% 3.16/0.85 % Length of proof is 182.
% 3.16/0.85 % Level of proof is 50.
% 3.16/0.85 % Maximum clause weight is 16.000.
% 3.16/0.85 % Given clauses 993.
% 3.16/0.85
% 3.16/0.85 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------