%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KRS162+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n008.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 : Fri Sep 25 01:53:22 PM UTC 2026
% Result : Theorem 6.51s 11.53s
% Output : Proof 6.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 97
% Number of leaves : 8
% Syntax : Number of formulae : 263 ( 13 unt; 0 def)
% Number of atoms : 1653 ( 699 equ)
% Maximal formula atoms : 30 ( 6 avg)
% Number of connectives : 1692 ( 302 ~;1303 |; 78 &)
% ( 3 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 33 ( 7 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 8 con; 0-0 aty)
% Number of variables : 190 ( 4 sgn 49 !; 28 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [X,Y] :
( rp(X,Y)
=> rr(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_6) ).
fof(f18_nnf,plain,
! [X,Y] :
( rr(X,Y)
| ~ rp(X,Y) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [X,Y] :
( rr(X,Y)
| ~ rp(X,Y) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c20,plain,
( rr(X0,X1)
| ~ rp(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
fof(f13,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
fof(f13_nnf,plain,
! [X] :
( ( xsd_integer(X)
| xsd_string(X) )
& ( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [X] :
( ( xsd_integer(X)
| xsd_string(X) )
& ( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c15,plain,
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
fof(f12,axiom,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_0) ).
fof(f12_nnf,plain,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
cowlThing(X0),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
fof(f19,conjecture,
( ! [X] :
( ( ? [Y0,Y1,Y2] :
( Y1 != Y2
& Y0 != Y2
& Y0 != Y1
& rq(X,Y2)
& rq(X,Y1)
& rq(X,Y0) )
& ? [Y0,Y1] :
( Y0 != Y1
& rp(X,Y1)
& rp(X,Y0) ) )
=> ? [Y0,Y1,Y2,Y3,Y4] :
( Y3 != Y4
& Y2 != Y4
& Y2 != Y3
& Y1 != Y4
& Y1 != Y3
& Y1 != Y2
& Y0 != Y4
& Y0 != Y3
& Y0 != Y2
& Y0 != Y1
& rr(X,Y4)
& rr(X,Y3)
& rr(X,Y2)
& rr(X,Y1)
& rr(X,Y0) ) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',the_axiom) ).
fof(f19_neg,negated_conjecture,
~ ( ! [X] :
( ( ? [Y0,Y1,Y2] :
( Y1 != Y2
& Y0 != Y2
& Y0 != Y1
& rq(X,Y2)
& rq(X,Y1)
& rq(X,Y0) )
& ? [Y0,Y1] :
( Y0 != Y1
& rp(X,Y1)
& rp(X,Y0) ) )
=> ? [Y0,Y1,Y2,Y3,Y4] :
( Y3 != Y4
& Y2 != Y4
& Y2 != Y3
& Y1 != Y4
& Y1 != Y3
& Y1 != Y2
& Y0 != Y4
& Y0 != Y3
& Y0 != Y2
& Y0 != Y1
& rr(X,Y4)
& rr(X,Y3)
& rr(X,Y2)
& rr(X,Y1)
& rr(X,Y0) ) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negated_conjecture,[status(cth)],[f19]) ).
fof(f19_nnf,plain,
( ? [X] :
( ! [Y0,Y1,Y2,Y3,Y4] :
( Y3 = Y4
| Y2 = Y4
| Y2 = Y3
| Y1 = Y4
| Y1 = Y3
| Y1 = Y2
| Y0 = Y4
| Y0 = Y3
| Y0 = Y2
| Y0 = Y1
| ~ rr(X,Y4)
| ~ rr(X,Y3)
| ~ rr(X,Y2)
| ~ rr(X,Y1)
| ~ rr(X,Y0) )
& ? [Y0,Y1,Y2] :
( Y1 != Y2
& Y0 != Y2
& Y0 != Y1
& rq(X,Y2)
& rq(X,Y1)
& rq(X,Y0) )
& ? [Y0,Y1] :
( Y0 != Y1
& rp(X,Y1)
& rp(X,Y0) ) )
| ? [X] :
( ( ~ xsd_integer(X)
& ~ xsd_string(X) )
| ( xsd_integer(X)
& xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(nnf_transformation,[status(thm)],[f19_neg]) ).
fof(f19_sk,plain,
! [Y0,Y1,Y2,Y3,Y4] :
( ( ( Y3 = Y4
| Y2 = Y4
| Y2 = Y3
| Y1 = Y4
| Y1 = Y3
| Y1 = Y2
| Y0 = Y4
| Y0 = Y3
| Y0 = Y2
| Y0 = Y1
| ~ rr(sk2,Y4)
| ~ rr(sk2,Y3)
| ~ rr(sk2,Y2)
| ~ rr(sk2,Y1)
| ~ rr(sk2,Y0) )
& sk6 != sk7
& sk5 != sk7
& sk5 != sk6
& rq(sk2,sk7)
& rq(sk2,sk6)
& rq(sk2,sk5)
& sk3 != sk4
& rp(sk2,sk4)
& rp(sk2,sk3) )
| ( ~ xsd_integer(sk1)
& ~ xsd_string(sk1) )
| ( xsd_integer(sk1)
& xsd_string(sk1) )
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3,sk4,sk5,sk6,sk7])],[f19_nnf]) ).
cnf(c41,plain,
( rp(sk2,sk3)
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p164,plain,
( rp(sk2,sk3)
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c41]) ).
cnf(p177,plain,
( rp(sk2,sk3)
| xsd_integer(sk1)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[c15,p164]) ).
cnf(p188,plain,
( rp(sk2,sk3)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p177]) ).
cnf(p413,plain,
( cowlNothing(sk0)
| xsd_integer(sk1)
| rr(sk2,sk3) ),
inference(resolution,[status(thm)],[c20,p188]) ).
fof(f17,axiom,
! [X,Y] :
( rq(X,Y)
=> rr(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_5) ).
fof(f17_nnf,plain,
! [X,Y] :
( rr(X,Y)
| ~ rq(X,Y) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [X,Y] :
( rr(X,Y)
| ~ rq(X,Y) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c19,plain,
( rr(X0,X1)
| ~ rq(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c45,plain,
( rq(sk2,sk6)
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p166,plain,
( rq(sk2,sk6)
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c45]) ).
cnf(p179,plain,
( rq(sk2,sk6)
| xsd_integer(sk1)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[c15,p166]) ).
cnf(p190,plain,
( rq(sk2,sk6)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p179]) ).
cnf(p326,plain,
( cowlNothing(sk0)
| xsd_integer(sk1)
| rr(sk2,sk6) ),
inference(resolution,[status(thm)],[c19,p190]) ).
cnf(c50,plain,
( X4 = X5
| X3 = X5
| X3 = X4
| X2 = X5
| X2 = X4
| X2 = X3
| X1 = X5
| X1 = X4
| X1 = X3
| X1 = X2
| ~ rr(sk2,X5)
| ~ rr(sk2,X4)
| ~ rr(sk2,X3)
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p174,plain,
( X3 = X4
| X2 = X4
| X2 = X3
| X1 = X4
| X1 = X3
| X1 = X2
| X0 = X4
| X0 = X3
| X0 = X2
| X0 = X1
| ~ rr(sk2,X4)
| ~ rr(sk2,X3)
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c50]) ).
cnf(p187,plain,
( X3 = X4
| X2 = X4
| X2 = X3
| X1 = X4
| X1 = X3
| X1 = X2
| X0 = X4
| X0 = X3
| X0 = X2
| X0 = X1
| ~ rr(sk2,X4)
| ~ rr(sk2,X3)
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| xsd_integer(sk1)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[c15,p174]) ).
cnf(p198,plain,
( X3 = X4
| X2 = X4
| X2 = X3
| X1 = X4
| X1 = X3
| X1 = X2
| X0 = X4
| X0 = X3
| X0 = X2
| X0 = X1
| ~ rr(sk2,X4)
| ~ rr(sk2,X3)
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p187]) ).
cnf(p330,plain,
( X2 = X3
| X1 = X3
| X1 = X2
| X0 = X3
| X0 = X2
| X0 = X1
| sk6 = X3
| sk6 = X2
| sk6 = X1
| sk6 = X0
| ~ rr(sk2,X3)
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| cowlNothing(sk0)
| xsd_integer(sk1)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[p326,p198]) ).
cnf(p356,plain,
( X2 = X3
| X1 = X3
| X1 = X2
| X0 = X3
| X0 = X2
| X0 = X1
| sk6 = X3
| sk6 = X2
| sk6 = X1
| sk6 = X0
| ~ rr(sk2,X3)
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| cowlNothing(sk0)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p330]) ).
cnf(p358,plain,
( X2 = X3
| X1 = X3
| X1 = X2
| X0 = X3
| X0 = X2
| X0 = X1
| sk6 = X3
| sk6 = X2
| sk6 = X1
| sk6 = X0
| ~ rr(sk2,X3)
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p356]) ).
cnf(c44,plain,
( rq(sk2,sk5)
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p167,plain,
( rq(sk2,sk5)
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c44]) ).
cnf(p180,plain,
( rq(sk2,sk5)
| xsd_integer(sk1)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[c15,p167]) ).
cnf(p191,plain,
( rq(sk2,sk5)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p180]) ).
cnf(p327,plain,
( cowlNothing(sk0)
| xsd_integer(sk1)
| rr(sk2,sk5) ),
inference(resolution,[status(thm)],[c19,p191]) ).
cnf(p359,plain,
( cowlNothing(sk0)
| xsd_integer(sk1)
| X1 = X2
| X0 = X2
| X0 = X1
| sk5 = X2
| sk5 = X1
| sk5 = X0
| sk6 = X2
| sk6 = X1
| sk6 = X0
| sk6 = sk5
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[p358,p327]) ).
cnf(p361,plain,
( cowlNothing(sk0)
| X1 = X2
| X0 = X2
| X0 = X1
| sk5 = X2
| sk5 = X1
| sk5 = X0
| sk6 = X2
| sk6 = X1
| sk6 = X0
| sk6 = sk5
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p359]) ).
cnf(p363,plain,
( X1 = X2
| X0 = X2
| X0 = X1
| sk5 = X2
| sk5 = X1
| sk5 = X0
| sk6 = X2
| sk6 = X1
| sk6 = X0
| sk6 = sk5
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p361]) ).
cnf(c46,plain,
( rq(sk2,sk7)
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p169,plain,
( rq(sk2,sk7)
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c46]) ).
cnf(p182,plain,
( rq(sk2,sk7)
| xsd_integer(sk1)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[c15,p169]) ).
cnf(p193,plain,
( rq(sk2,sk7)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p182]) ).
cnf(p328,plain,
( cowlNothing(sk0)
| xsd_integer(sk1)
| rr(sk2,sk7) ),
inference(resolution,[status(thm)],[c19,p193]) ).
cnf(p364,plain,
( cowlNothing(sk0)
| xsd_integer(sk1)
| X0 = X1
| sk7 = X1
| sk7 = X0
| sk5 = X1
| sk5 = X0
| sk5 = sk7
| sk6 = X1
| sk6 = X0
| sk6 = sk7
| sk6 = sk5
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[p363,p328]) ).
cnf(p365,plain,
( cowlNothing(sk0)
| X0 = X1
| sk7 = X1
| sk7 = X0
| sk5 = X1
| sk5 = X0
| sk5 = sk7
| sk6 = X1
| sk6 = X0
| sk6 = sk7
| sk6 = sk5
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p364]) ).
cnf(p367,plain,
( X0 = X1
| sk7 = X1
| sk7 = X0
| sk5 = X1
| sk5 = X0
| sk5 = sk7
| sk6 = X1
| sk6 = X0
| sk6 = sk7
| sk6 = sk5
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p365]) ).
cnf(p422,plain,
( sk3 = X0
| sk7 = X0
| sk7 = sk3
| sk5 = X0
| sk5 = sk3
| sk5 = sk7
| sk6 = X0
| sk6 = sk3
| sk6 = sk7
| sk6 = sk5
| ~ rr(sk2,X0)
| cowlNothing(sk0)
| xsd_integer(sk1)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[p413,p367]) ).
cnf(p507,plain,
( sk3 = X0
| sk7 = X0
| sk7 = sk3
| sk5 = X0
| sk5 = sk3
| sk5 = sk7
| sk6 = X0
| sk6 = sk3
| sk6 = sk7
| sk6 = sk5
| ~ rr(sk2,X0)
| cowlNothing(sk0)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p422]) ).
cnf(p509,plain,
( sk3 = X0
| sk7 = X0
| sk7 = sk3
| sk5 = X0
| sk5 = sk3
| sk5 = sk7
| sk6 = X0
| sk6 = sk3
| sk6 = sk7
| sk6 = sk5
| ~ rr(sk2,X0)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p507]) ).
cnf(c42,plain,
( rp(sk2,sk4)
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p168,plain,
( rp(sk2,sk4)
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c42]) ).
cnf(p181,plain,
( rp(sk2,sk4)
| xsd_integer(sk1)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[c15,p168]) ).
cnf(p192,plain,
( rp(sk2,sk4)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p181]) ).
cnf(p414,plain,
( cowlNothing(sk0)
| xsd_integer(sk1)
| rr(sk2,sk4) ),
inference(resolution,[status(thm)],[c20,p192]) ).
cnf(p510,plain,
( cowlNothing(sk0)
| xsd_integer(sk1)
| sk3 = sk4
| sk7 = sk4
| sk7 = sk3
| sk5 = sk4
| sk5 = sk3
| sk5 = sk7
| sk6 = sk4
| sk6 = sk3
| sk6 = sk7
| sk6 = sk5
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[p509,p414]) ).
cnf(p511,plain,
( cowlNothing(sk0)
| sk3 = sk4
| sk7 = sk4
| sk7 = sk3
| sk5 = sk4
| sk5 = sk3
| sk5 = sk7
| sk6 = sk4
| sk6 = sk3
| sk6 = sk7
| sk6 = sk5
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p510]) ).
cnf(p513,plain,
( sk3 = sk4
| sk7 = sk4
| sk7 = sk3
| sk5 = sk4
| sk5 = sk3
| sk5 = sk7
| sk6 = sk4
| sk6 = sk3
| sk6 = sk7
| sk6 = sk5
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p511]) ).
fof(f15,axiom,
! [X,Y] :
( rq(X,Y)
=> cB(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3) ).
fof(f15_nnf,plain,
! [X,Y] :
( cB(Y)
| ~ rq(X,Y) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [X,Y] :
( cB(Y)
| ~ rq(X,Y) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c17,plain,
( cB(X1)
| ~ rq(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p246,plain,
( cowlNothing(sk0)
| xsd_integer(sk1)
| cB(sk7) ),
inference(resolution,[status(thm)],[c17,p193]) ).
cnf(c36,plain,
( rq(sk2,sk7)
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p161,plain,
( rq(sk2,sk7)
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c36]) ).
cnf(p275,plain,
( rq(sk2,sk7)
| xsd_string(sk1)
| cowlNothing(sk0)
| cowlNothing(sk0)
| cB(sk7) ),
inference(resolution,[status(thm)],[p246,p161]) ).
cnf(p316,plain,
( rq(sk2,sk7)
| xsd_string(sk1)
| cowlNothing(sk0)
| cB(sk7) ),
inference(factoring,[status(thm)],[p275]) ).
cnf(p317,plain,
( cB(sk7)
| xsd_string(sk1)
| cowlNothing(sk0)
| cB(sk7) ),
inference(resolution,[status(thm)],[p316,c17]) ).
cnf(p318,plain,
( xsd_string(sk1)
| cowlNothing(sk0)
| cB(sk7) ),
inference(factoring,[status(thm)],[p317]) ).
cnf(c14,plain,
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p319,plain,
( ~ xsd_integer(sk1)
| cowlNothing(sk0)
| cB(sk7) ),
inference(resolution,[status(thm)],[p318,c14]) ).
cnf(p320,plain,
( cowlNothing(sk0)
| cB(sk7)
| cowlNothing(sk0)
| cB(sk7) ),
inference(resolution,[status(thm)],[p319,p246]) ).
cnf(p321,plain,
( cowlNothing(sk0)
| cowlNothing(sk0)
| cB(sk7) ),
inference(factoring,[status(thm)],[p320]) ).
cnf(p323,plain,
( cowlNothing(sk0)
| cB(sk7) ),
inference(factoring,[status(thm)],[p321]) ).
cnf(c13,plain,
~ cowlNothing(X0),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p324,plain,
cB(sk7),
inference(resolution,[status(thm)],[p323,c13]) ).
fof(f16,axiom,
! [X] :
~ ( cA(X)
& cB(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_4) ).
fof(f16_nnf,plain,
! [X] :
( ~ cA(X)
| ~ cB(X) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [X] :
( ~ cA(X)
| ~ cB(X) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c18,plain,
( ~ cA(X0)
| ~ cB(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p325,plain,
~ cA(sk7),
inference(resolution,[status(thm)],[p324,c18]) ).
cnf(p516,plain,
( ~ cA(sk4)
| sk3 = sk4
| sk7 = sk3
| sk5 = sk4
| sk5 = sk3
| sk5 = sk7
| sk6 = sk4
| sk6 = sk3
| sk6 = sk7
| sk6 = sk5
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(superposition,[status(thm)],[p513,p325]) ).
fof(f14,axiom,
! [X,Y] :
( rp(X,Y)
=> cA(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2) ).
fof(f14_nnf,plain,
! [X,Y] :
( cA(Y)
| ~ rp(X,Y) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [X,Y] :
( cA(Y)
| ~ rp(X,Y) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c16,plain,
( cA(X1)
| ~ rp(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p200,plain,
( cowlNothing(sk0)
| xsd_integer(sk1)
| cA(sk4) ),
inference(resolution,[status(thm)],[c16,p192]) ).
cnf(c32,plain,
( rp(sk2,sk4)
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p157,plain,
( rp(sk2,sk4)
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c32]) ).
cnf(p214,plain,
( rp(sk2,sk4)
| xsd_string(sk1)
| cowlNothing(sk0)
| cowlNothing(sk0)
| cA(sk4) ),
inference(resolution,[status(thm)],[p200,p157]) ).
cnf(p235,plain,
( rp(sk2,sk4)
| xsd_string(sk1)
| cowlNothing(sk0)
| cA(sk4) ),
inference(factoring,[status(thm)],[p214]) ).
cnf(p236,plain,
( cA(sk4)
| xsd_string(sk1)
| cowlNothing(sk0)
| cA(sk4) ),
inference(resolution,[status(thm)],[p235,c16]) ).
cnf(p237,plain,
( xsd_string(sk1)
| cowlNothing(sk0)
| cA(sk4) ),
inference(factoring,[status(thm)],[p236]) ).
cnf(p238,plain,
( ~ xsd_integer(sk1)
| cowlNothing(sk0)
| cA(sk4) ),
inference(resolution,[status(thm)],[p237,c14]) ).
cnf(p239,plain,
( cowlNothing(sk0)
| cA(sk4)
| cowlNothing(sk0)
| cA(sk4) ),
inference(resolution,[status(thm)],[p238,p200]) ).
cnf(p240,plain,
( cowlNothing(sk0)
| cowlNothing(sk0)
| cA(sk4) ),
inference(factoring,[status(thm)],[p239]) ).
cnf(p242,plain,
( cowlNothing(sk0)
| cA(sk4) ),
inference(factoring,[status(thm)],[p240]) ).
cnf(p243,plain,
cA(sk4),
inference(resolution,[status(thm)],[p242,c13]) ).
cnf(p931,plain,
( sk3 = sk4
| sk7 = sk3
| sk5 = sk4
| sk5 = sk3
| sk5 = sk7
| sk6 = sk4
| sk6 = sk3
| sk6 = sk7
| sk6 = sk5
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[p516,p243]) ).
cnf(p938,plain,
( ~ cA(sk3)
| sk3 = sk4
| sk5 = sk4
| sk5 = sk3
| sk5 = sk7
| sk6 = sk4
| sk6 = sk3
| sk6 = sk7
| sk6 = sk5
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(superposition,[status(thm)],[p931,p325]) ).
cnf(p199,plain,
( cowlNothing(sk0)
| xsd_integer(sk1)
| cA(sk3) ),
inference(resolution,[status(thm)],[c16,p188]) ).
cnf(c31,plain,
( rp(sk2,sk3)
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p155,plain,
( rp(sk2,sk3)
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c31]) ).
cnf(p201,plain,
( rp(sk2,sk3)
| xsd_string(sk1)
| cowlNothing(sk0)
| cowlNothing(sk0)
| cA(sk3) ),
inference(resolution,[status(thm)],[p199,p155]) ).
cnf(p223,plain,
( rp(sk2,sk3)
| xsd_string(sk1)
| cowlNothing(sk0)
| cA(sk3) ),
inference(factoring,[status(thm)],[p201]) ).
cnf(p224,plain,
( cA(sk3)
| xsd_string(sk1)
| cowlNothing(sk0)
| cA(sk3) ),
inference(resolution,[status(thm)],[p223,c16]) ).
cnf(p225,plain,
( xsd_string(sk1)
| cowlNothing(sk0)
| cA(sk3) ),
inference(factoring,[status(thm)],[p224]) ).
cnf(p226,plain,
( ~ xsd_integer(sk1)
| cowlNothing(sk0)
| cA(sk3) ),
inference(resolution,[status(thm)],[p225,c14]) ).
cnf(p227,plain,
( cowlNothing(sk0)
| cA(sk3)
| cowlNothing(sk0)
| cA(sk3) ),
inference(resolution,[status(thm)],[p226,p199]) ).
cnf(p229,plain,
( cowlNothing(sk0)
| cowlNothing(sk0)
| cA(sk3) ),
inference(factoring,[status(thm)],[p227]) ).
cnf(p231,plain,
( cowlNothing(sk0)
| cA(sk3) ),
inference(factoring,[status(thm)],[p229]) ).
cnf(p232,plain,
cA(sk3),
inference(resolution,[status(thm)],[p231,c13]) ).
cnf(p957,plain,
( sk3 = sk4
| sk5 = sk4
| sk5 = sk3
| sk5 = sk7
| sk6 = sk4
| sk6 = sk3
| sk6 = sk7
| sk6 = sk5
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[p938,p232]) ).
cnf(c49,plain,
( sk6 != sk7
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p172,plain,
( sk6 != sk7
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c49]) ).
cnf(p185,plain,
( sk6 != sk7
| xsd_integer(sk1)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[c15,p172]) ).
cnf(p196,plain,
( sk6 != sk7
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p185]) ).
cnf(p966,plain,
( cowlNothing(sk0)
| xsd_integer(sk1)
| sk3 = sk4
| sk5 = sk4
| sk5 = sk3
| sk5 = sk7
| sk6 = sk4
| sk6 = sk3
| sk6 = sk5
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[p957,p196]) ).
cnf(p1081,plain,
( cowlNothing(sk0)
| sk3 = sk4
| sk5 = sk4
| sk5 = sk3
| sk5 = sk7
| sk6 = sk4
| sk6 = sk3
| sk6 = sk5
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p966]) ).
cnf(p1083,plain,
( sk3 = sk4
| sk5 = sk4
| sk5 = sk3
| sk5 = sk7
| sk6 = sk4
| sk6 = sk3
| sk6 = sk5
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p1081]) ).
cnf(c47,plain,
( sk5 != sk6
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p170,plain,
( sk5 != sk6
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c47]) ).
cnf(p183,plain,
( sk5 != sk6
| xsd_integer(sk1)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[c15,p170]) ).
cnf(p194,plain,
( sk5 != sk6
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p183]) ).
cnf(p1086,plain,
( sk5 != sk5
| cowlNothing(sk0)
| xsd_integer(sk1)
| sk3 = sk4
| sk5 = sk4
| sk5 = sk3
| sk5 = sk7
| sk6 = sk4
| sk6 = sk3
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(superposition,[status(thm)],[p1083,p194]) ).
cnf(p1100,plain,
( sk5 != sk5
| cowlNothing(sk0)
| sk3 = sk4
| sk5 = sk4
| sk5 = sk3
| sk5 = sk7
| sk6 = sk4
| sk6 = sk3
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p1086]) ).
cnf(p1102,plain,
( sk5 != sk5
| sk3 = sk4
| sk5 = sk4
| sk5 = sk3
| sk5 = sk7
| sk6 = sk4
| sk6 = sk3
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p1100]) ).
cnf(p1103,plain,
( sk3 = sk4
| sk5 = sk4
| sk5 = sk3
| sk5 = sk7
| sk6 = sk4
| sk6 = sk3
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(equality_resolution,[status(thm)],[p1102]) ).
cnf(p244,plain,
( cowlNothing(sk0)
| xsd_integer(sk1)
| cB(sk6) ),
inference(resolution,[status(thm)],[c17,p190]) ).
cnf(c35,plain,
( rq(sk2,sk6)
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p158,plain,
( rq(sk2,sk6)
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c35]) ).
cnf(p250,plain,
( rq(sk2,sk6)
| xsd_string(sk1)
| cowlNothing(sk0)
| cowlNothing(sk0)
| cB(sk6) ),
inference(resolution,[status(thm)],[p244,p158]) ).
cnf(p283,plain,
( rq(sk2,sk6)
| xsd_string(sk1)
| cowlNothing(sk0)
| cB(sk6) ),
inference(factoring,[status(thm)],[p250]) ).
cnf(p284,plain,
( cB(sk6)
| xsd_string(sk1)
| cowlNothing(sk0)
| cB(sk6) ),
inference(resolution,[status(thm)],[p283,c17]) ).
cnf(p285,plain,
( xsd_string(sk1)
| cowlNothing(sk0)
| cB(sk6) ),
inference(factoring,[status(thm)],[p284]) ).
cnf(p286,plain,
( ~ xsd_integer(sk1)
| cowlNothing(sk0)
| cB(sk6) ),
inference(resolution,[status(thm)],[p285,c14]) ).
cnf(p287,plain,
( cowlNothing(sk0)
| cB(sk6)
| cowlNothing(sk0)
| cB(sk6) ),
inference(resolution,[status(thm)],[p286,p244]) ).
cnf(p290,plain,
( cowlNothing(sk0)
| cowlNothing(sk0)
| cB(sk6) ),
inference(factoring,[status(thm)],[p287]) ).
cnf(p292,plain,
( cowlNothing(sk0)
| cB(sk6) ),
inference(factoring,[status(thm)],[p290]) ).
cnf(p293,plain,
cB(sk6),
inference(resolution,[status(thm)],[p292,c13]) ).
cnf(p294,plain,
~ cA(sk6),
inference(resolution,[status(thm)],[p293,c18]) ).
cnf(p1110,plain,
( ~ cA(sk4)
| sk3 = sk4
| sk5 = sk4
| sk5 = sk3
| sk5 = sk7
| sk6 = sk3
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(superposition,[status(thm)],[p1103,p294]) ).
cnf(p1117,plain,
( sk3 = sk4
| sk5 = sk4
| sk5 = sk3
| sk5 = sk7
| sk6 = sk3
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[p1110,p243]) ).
cnf(p1125,plain,
( ~ cA(sk3)
| sk3 = sk4
| sk5 = sk4
| sk5 = sk3
| sk5 = sk7
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(superposition,[status(thm)],[p1117,p294]) ).
cnf(p1137,plain,
( sk3 = sk4
| sk5 = sk4
| sk5 = sk3
| sk5 = sk7
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[p1125,p232]) ).
cnf(c48,plain,
( sk5 != sk7
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p171,plain,
( sk5 != sk7
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c48]) ).
cnf(p184,plain,
( sk5 != sk7
| xsd_integer(sk1)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[c15,p171]) ).
cnf(p195,plain,
( sk5 != sk7
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p184]) ).
cnf(p1142,plain,
( cowlNothing(sk0)
| xsd_integer(sk1)
| sk3 = sk4
| sk5 = sk4
| sk5 = sk3
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[p1137,p195]) ).
cnf(p1146,plain,
( cowlNothing(sk0)
| sk3 = sk4
| sk5 = sk4
| sk5 = sk3
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p1142]) ).
cnf(p1148,plain,
( sk3 = sk4
| sk5 = sk4
| sk5 = sk3
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p1146]) ).
cnf(p245,plain,
( cowlNothing(sk0)
| xsd_integer(sk1)
| cB(sk5) ),
inference(resolution,[status(thm)],[c17,p191]) ).
cnf(c34,plain,
( rq(sk2,sk5)
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p159,plain,
( rq(sk2,sk5)
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c34]) ).
cnf(p262,plain,
( rq(sk2,sk5)
| xsd_string(sk1)
| cowlNothing(sk0)
| cowlNothing(sk0)
| cB(sk5) ),
inference(resolution,[status(thm)],[p245,p159]) ).
cnf(p299,plain,
( rq(sk2,sk5)
| xsd_string(sk1)
| cowlNothing(sk0)
| cB(sk5) ),
inference(factoring,[status(thm)],[p262]) ).
cnf(p300,plain,
( cB(sk5)
| xsd_string(sk1)
| cowlNothing(sk0)
| cB(sk5) ),
inference(resolution,[status(thm)],[p299,c17]) ).
cnf(p301,plain,
( xsd_string(sk1)
| cowlNothing(sk0)
| cB(sk5) ),
inference(factoring,[status(thm)],[p300]) ).
cnf(p302,plain,
( ~ xsd_integer(sk1)
| cowlNothing(sk0)
| cB(sk5) ),
inference(resolution,[status(thm)],[p301,c14]) ).
cnf(p303,plain,
( cowlNothing(sk0)
| cB(sk5)
| cowlNothing(sk0)
| cB(sk5) ),
inference(resolution,[status(thm)],[p302,p245]) ).
cnf(p305,plain,
( cowlNothing(sk0)
| cowlNothing(sk0)
| cB(sk5) ),
inference(factoring,[status(thm)],[p303]) ).
cnf(p307,plain,
( cowlNothing(sk0)
| cB(sk5) ),
inference(factoring,[status(thm)],[p305]) ).
cnf(p308,plain,
cB(sk5),
inference(resolution,[status(thm)],[p307,c13]) ).
cnf(p309,plain,
~ cA(sk5),
inference(resolution,[status(thm)],[p308,c18]) ).
cnf(p1152,plain,
( ~ cA(sk4)
| sk3 = sk4
| sk5 = sk3
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(superposition,[status(thm)],[p1148,p309]) ).
cnf(p1155,plain,
( sk3 = sk4
| sk5 = sk3
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[p1152,p243]) ).
cnf(p1160,plain,
( ~ cA(sk3)
| sk3 = sk4
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(superposition,[status(thm)],[p1155,p309]) ).
cnf(p1165,plain,
( sk3 = sk4
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[p1160,p232]) ).
cnf(c43,plain,
( sk3 != sk4
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p165,plain,
( sk3 != sk4
| ~ xsd_string(sk1)
| xsd_integer(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c43]) ).
cnf(p178,plain,
( sk3 != sk4
| xsd_integer(sk1)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[c15,p165]) ).
cnf(p189,plain,
( sk3 != sk4
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p178]) ).
cnf(p1166,plain,
( cowlNothing(sk0)
| xsd_integer(sk1)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(resolution,[status(thm)],[p1165,p189]) ).
cnf(p1167,plain,
( cowlNothing(sk0)
| cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p1166]) ).
cnf(p1169,plain,
( cowlNothing(sk0)
| xsd_integer(sk1) ),
inference(factoring,[status(thm)],[p1167]) ).
cnf(c40,plain,
( X4 = X5
| X3 = X5
| X3 = X4
| X2 = X5
| X2 = X4
| X2 = X3
| X1 = X5
| X1 = X4
| X1 = X3
| X1 = X2
| ~ rr(sk2,X5)
| ~ rr(sk2,X4)
| ~ rr(sk2,X3)
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p173,plain,
( X3 = X4
| X2 = X4
| X2 = X3
| X1 = X4
| X1 = X3
| X1 = X2
| X0 = X4
| X0 = X3
| X0 = X2
| X0 = X1
| ~ rr(sk2,X4)
| ~ rr(sk2,X3)
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c40]) ).
cnf(p1180,plain,
( X3 = X4
| X2 = X4
| X2 = X3
| X1 = X4
| X1 = X3
| X1 = X2
| X0 = X4
| X0 = X3
| X0 = X2
| X0 = X1
| ~ rr(sk2,X4)
| ~ rr(sk2,X3)
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| xsd_string(sk1)
| cowlNothing(sk0)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1169,p173]) ).
cnf(p1280,plain,
( X3 = X4
| X2 = X4
| X2 = X3
| X1 = X4
| X1 = X3
| X1 = X2
| X0 = X4
| X0 = X3
| X0 = X2
| X0 = X1
| ~ rr(sk2,X4)
| ~ rr(sk2,X3)
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1180]) ).
cnf(p1170,plain,
( rp(sk2,sk3)
| xsd_string(sk1)
| cowlNothing(sk0)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1169,p155]) ).
cnf(p1181,plain,
( rp(sk2,sk3)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1170]) ).
cnf(p1182,plain,
( rr(sk2,sk3)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1181,c20]) ).
cnf(p1281,plain,
( xsd_string(sk1)
| cowlNothing(sk0)
| X2 = X3
| X1 = X3
| X1 = X2
| X0 = X3
| X0 = X2
| X0 = X1
| sk3 = X3
| sk3 = X2
| sk3 = X1
| sk3 = X0
| ~ rr(sk2,X3)
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1280,p1182]) ).
cnf(p1286,plain,
( xsd_string(sk1)
| X2 = X3
| X1 = X3
| X1 = X2
| X0 = X3
| X0 = X2
| X0 = X1
| sk3 = X3
| sk3 = X2
| sk3 = X1
| sk3 = X0
| ~ rr(sk2,X3)
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1281]) ).
cnf(p1288,plain,
( X2 = X3
| X1 = X3
| X1 = X2
| X0 = X3
| X0 = X2
| X0 = X1
| sk3 = X3
| sk3 = X2
| sk3 = X1
| sk3 = X0
| ~ rr(sk2,X3)
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1286]) ).
cnf(p1172,plain,
( rp(sk2,sk4)
| xsd_string(sk1)
| cowlNothing(sk0)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1169,p157]) ).
cnf(p1184,plain,
( rp(sk2,sk4)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1172]) ).
cnf(p1185,plain,
( rr(sk2,sk4)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1184,c20]) ).
cnf(p1289,plain,
( xsd_string(sk1)
| cowlNothing(sk0)
| X1 = X2
| X0 = X2
| X0 = X1
| sk4 = X2
| sk4 = X1
| sk4 = X0
| sk3 = X2
| sk3 = X1
| sk3 = X0
| sk3 = sk4
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1288,p1185]) ).
cnf(p1293,plain,
( xsd_string(sk1)
| X1 = X2
| X0 = X2
| X0 = X1
| sk4 = X2
| sk4 = X1
| sk4 = X0
| sk3 = X2
| sk3 = X1
| sk3 = X0
| sk3 = sk4
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1289]) ).
cnf(p1295,plain,
( X1 = X2
| X0 = X2
| X0 = X1
| sk4 = X2
| sk4 = X1
| sk4 = X0
| sk3 = X2
| sk3 = X1
| sk3 = X0
| sk3 = sk4
| ~ rr(sk2,X2)
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1293]) ).
cnf(p1173,plain,
( rq(sk2,sk6)
| xsd_string(sk1)
| cowlNothing(sk0)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1169,p158]) ).
cnf(p1186,plain,
( rq(sk2,sk6)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1173]) ).
cnf(p1187,plain,
( rr(sk2,sk6)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1186,c19]) ).
cnf(p1296,plain,
( xsd_string(sk1)
| cowlNothing(sk0)
| X0 = X1
| sk6 = X1
| sk6 = X0
| sk4 = X1
| sk4 = X0
| sk4 = sk6
| sk3 = X1
| sk3 = X0
| sk3 = sk6
| sk3 = sk4
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1295,p1187]) ).
cnf(p1299,plain,
( xsd_string(sk1)
| X0 = X1
| sk6 = X1
| sk6 = X0
| sk4 = X1
| sk4 = X0
| sk4 = sk6
| sk3 = X1
| sk3 = X0
| sk3 = sk6
| sk3 = sk4
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1296]) ).
cnf(p1301,plain,
( X0 = X1
| sk6 = X1
| sk6 = X0
| sk4 = X1
| sk4 = X0
| sk4 = sk6
| sk3 = X1
| sk3 = X0
| sk3 = sk6
| sk3 = sk4
| ~ rr(sk2,X1)
| ~ rr(sk2,X0)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1299]) ).
cnf(p1174,plain,
( rq(sk2,sk5)
| xsd_string(sk1)
| cowlNothing(sk0)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1169,p159]) ).
cnf(p1188,plain,
( rq(sk2,sk5)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1174]) ).
cnf(p1189,plain,
( rr(sk2,sk5)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1188,c19]) ).
cnf(p1302,plain,
( xsd_string(sk1)
| cowlNothing(sk0)
| sk5 = X0
| sk6 = X0
| sk6 = sk5
| sk4 = X0
| sk4 = sk5
| sk4 = sk6
| sk3 = X0
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| ~ rr(sk2,X0)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1301,p1189]) ).
cnf(p1304,plain,
( xsd_string(sk1)
| sk5 = X0
| sk6 = X0
| sk6 = sk5
| sk4 = X0
| sk4 = sk5
| sk4 = sk6
| sk3 = X0
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| ~ rr(sk2,X0)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1302]) ).
cnf(p1306,plain,
( sk5 = X0
| sk6 = X0
| sk6 = sk5
| sk4 = X0
| sk4 = sk5
| sk4 = sk6
| sk3 = X0
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| ~ rr(sk2,X0)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1304]) ).
cnf(p1176,plain,
( rq(sk2,sk7)
| xsd_string(sk1)
| cowlNothing(sk0)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1169,p161]) ).
cnf(p1191,plain,
( rq(sk2,sk7)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1176]) ).
cnf(p1192,plain,
( rr(sk2,sk7)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1191,c19]) ).
cnf(p1307,plain,
( xsd_string(sk1)
| cowlNothing(sk0)
| sk5 = sk7
| sk6 = sk7
| sk6 = sk5
| sk4 = sk7
| sk4 = sk5
| sk4 = sk6
| sk3 = sk7
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1306,p1192]) ).
cnf(p1308,plain,
( xsd_string(sk1)
| sk5 = sk7
| sk6 = sk7
| sk6 = sk5
| sk4 = sk7
| sk4 = sk5
| sk4 = sk6
| sk3 = sk7
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1307]) ).
cnf(p1310,plain,
( sk5 = sk7
| sk6 = sk7
| sk6 = sk5
| sk4 = sk7
| sk4 = sk5
| sk4 = sk6
| sk3 = sk7
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1308]) ).
cnf(c39,plain,
( sk6 != sk7
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p162,plain,
( sk6 != sk7
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c39]) ).
cnf(p1177,plain,
( sk6 != sk7
| xsd_string(sk1)
| cowlNothing(sk0)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1169,p162]) ).
cnf(p1193,plain,
( sk6 != sk7
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1177]) ).
cnf(p1311,plain,
( xsd_string(sk1)
| cowlNothing(sk0)
| sk5 = sk7
| sk6 = sk5
| sk4 = sk7
| sk4 = sk5
| sk4 = sk6
| sk3 = sk7
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1310,p1193]) ).
cnf(p1312,plain,
( xsd_string(sk1)
| sk5 = sk7
| sk6 = sk5
| sk4 = sk7
| sk4 = sk5
| sk4 = sk6
| sk3 = sk7
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1311]) ).
cnf(p1314,plain,
( sk5 = sk7
| sk6 = sk5
| sk4 = sk7
| sk4 = sk5
| sk4 = sk6
| sk3 = sk7
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1312]) ).
cnf(c37,plain,
( sk5 != sk6
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p160,plain,
( sk5 != sk6
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c37]) ).
cnf(p1175,plain,
( sk5 != sk6
| xsd_string(sk1)
| cowlNothing(sk0)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1169,p160]) ).
cnf(p1190,plain,
( sk5 != sk6
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1175]) ).
cnf(p1317,plain,
( sk5 != sk5
| xsd_string(sk1)
| cowlNothing(sk0)
| sk5 = sk7
| sk4 = sk7
| sk4 = sk5
| sk4 = sk6
| sk3 = sk7
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(superposition,[status(thm)],[p1314,p1190]) ).
cnf(p1325,plain,
( sk5 != sk5
| xsd_string(sk1)
| sk5 = sk7
| sk4 = sk7
| sk4 = sk5
| sk4 = sk6
| sk3 = sk7
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1317]) ).
cnf(p1327,plain,
( sk5 != sk5
| sk5 = sk7
| sk4 = sk7
| sk4 = sk5
| sk4 = sk6
| sk3 = sk7
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1325]) ).
cnf(p1328,plain,
( sk5 = sk7
| sk4 = sk7
| sk4 = sk5
| sk4 = sk6
| sk3 = sk7
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(equality_resolution,[status(thm)],[p1327]) ).
cnf(c38,plain,
( sk5 != sk7
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p163,plain,
( sk5 != sk7
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c38]) ).
cnf(p1178,plain,
( sk5 != sk7
| xsd_string(sk1)
| cowlNothing(sk0)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1169,p163]) ).
cnf(p1194,plain,
( sk5 != sk7
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1178]) ).
cnf(p1334,plain,
( xsd_string(sk1)
| cowlNothing(sk0)
| sk4 = sk7
| sk4 = sk5
| sk4 = sk6
| sk3 = sk7
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1328,p1194]) ).
cnf(p1367,plain,
( xsd_string(sk1)
| sk4 = sk7
| sk4 = sk5
| sk4 = sk6
| sk3 = sk7
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1334]) ).
cnf(p1369,plain,
( sk4 = sk7
| sk4 = sk5
| sk4 = sk6
| sk3 = sk7
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1367]) ).
cnf(p1376,plain,
( cB(sk4)
| sk4 = sk5
| sk4 = sk6
| sk3 = sk7
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(superposition,[status(thm)],[p1369,p324]) ).
cnf(p1386,plain,
( cB(sk4)
| cB(sk4)
| sk4 = sk5
| sk3 = sk7
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(superposition,[status(thm)],[p1376,p293]) ).
cnf(p1392,plain,
( cB(sk4)
| sk4 = sk5
| sk3 = sk7
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1386]) ).
cnf(p1400,plain,
( cB(sk4)
| cB(sk4)
| sk3 = sk7
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(superposition,[status(thm)],[p1392,p308]) ).
cnf(p1411,plain,
( cB(sk4)
| sk3 = sk7
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1400]) ).
cnf(p1421,plain,
( cB(sk3)
| cB(sk4)
| sk3 = sk5
| sk3 = sk6
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(superposition,[status(thm)],[p1411,p324]) ).
cnf(p1430,plain,
( cB(sk3)
| cB(sk3)
| cB(sk4)
| sk3 = sk5
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(superposition,[status(thm)],[p1421,p293]) ).
cnf(p1436,plain,
( cB(sk3)
| cB(sk4)
| sk3 = sk5
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1430]) ).
cnf(p1439,plain,
( cB(sk3)
| cB(sk3)
| cB(sk4)
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(superposition,[status(thm)],[p1436,p308]) ).
cnf(p1450,plain,
( cB(sk3)
| cB(sk4)
| sk3 = sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1439]) ).
cnf(c33,plain,
( sk3 != sk4
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0)
| ~ cowlThing(sk0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p156,plain,
( sk3 != sk4
| ~ xsd_integer(sk1)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[c12,c33]) ).
cnf(p1171,plain,
( sk3 != sk4
| xsd_string(sk1)
| cowlNothing(sk0)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1169,p156]) ).
cnf(p1183,plain,
( sk3 != sk4
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1171]) ).
cnf(p1451,plain,
( xsd_string(sk1)
| cowlNothing(sk0)
| cB(sk3)
| cB(sk4)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1450,p1183]) ).
cnf(p1452,plain,
( xsd_string(sk1)
| cB(sk3)
| cB(sk4)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1451]) ).
cnf(p1454,plain,
( cB(sk3)
| cB(sk4)
| xsd_string(sk1)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1452]) ).
cnf(p1455,plain,
( ~ xsd_integer(sk1)
| cB(sk3)
| cB(sk4)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1454,c14]) ).
cnf(p1456,plain,
( cowlNothing(sk0)
| cB(sk3)
| cB(sk4)
| cowlNothing(sk0) ),
inference(resolution,[status(thm)],[p1455,p1169]) ).
cnf(p1457,plain,
( cB(sk3)
| cB(sk4)
| cowlNothing(sk0) ),
inference(factoring,[status(thm)],[p1456]) ).
cnf(p1458,plain,
( cB(sk3)
| cB(sk4) ),
inference(resolution,[status(thm)],[p1457,c13]) ).
cnf(p1459,plain,
( ~ cA(sk4)
| cB(sk3) ),
inference(resolution,[status(thm)],[p1458,c18]) ).
cnf(p1460,plain,
cB(sk3),
inference(resolution,[status(thm)],[p1459,p243]) ).
cnf(p1461,plain,
~ cA(sk3),
inference(resolution,[status(thm)],[p1460,c18]) ).
cnf(p1462,plain,
$false,
inference(resolution,[status(thm)],[p1461,p232]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS162+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/10.37 % Computer : n008.cluster.edu
% 0.08/10.37 % Model : x86_64 x86_64
% 0.08/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/10.37 % Memory : 8046.5625MB
% 0.08/10.37 % OS : Linux 6.8.0-71-generic
% 0.08/10.37 % CPULimit : 300
% 0.08/10.37 % WCLimit : 300
% 0.08/10.37 % DateTime : Wed Sep 23 19:34:37 UTC 2026
% 0.08/10.38 % CPUTime :
% 0.08/10.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 6.51/11.53 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.51/11.53 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------