%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KRS114+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 : n002.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:05 PM UTC 2026
% Result : Unsatisfiable 1.92s 1.30s
% Output : Proof 1.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 12
% Syntax : Number of formulae : 83 ( 35 unt; 0 def)
% Number of atoms : 219 ( 40 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 225 ( 89 ~; 77 |; 47 &)
% ( 9 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 18 ( 16 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 3 con; 0-4 aty)
% Number of variables : 116 ( 4 sgn 59 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f24,axiom,
! [X] :
( cUnsatisfiable(X)
<=> ( ? [Y] :
( ca_Ax3(Y)
& rs(X,Y) )
& ? [Y] :
( ca_Ax4(Y)
& rr(X,Y) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2) ).
fof(f24_nnf,plain,
! [X] :
( ( ! [Y] :
( ~ ca_Ax3(Y)
| ~ rs(X,Y) )
| ! [Y] :
( ~ ca_Ax4(Y)
| ~ rr(X,Y) )
| cUnsatisfiable(X) )
& ( ( ? [Y] :
( ca_Ax3(Y)
& rs(X,Y) )
& ? [Y] :
( ca_Ax4(Y)
& rr(X,Y) ) )
| ~ cUnsatisfiable(X) ) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [X,Y] :
( ( ~ ca_Ax3(Y)
| ~ rs(X,Y)
| ~ ca_Ax4(Y)
| ~ rr(X,Y)
| cUnsatisfiable(X) )
& ( ( ca_Ax3(sk1(X))
& rs(X,sk1(X))
& ca_Ax4(sk0(X))
& rr(X,sk0(X)) )
| ~ cUnsatisfiable(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f24_nnf]) ).
cnf(c29,plain,
( ca_Ax3(sk1(X0))
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(hi28,axiom,
ifeq(cUnsatisfiable(X0),true,ca_Ax3(sk1(X0)),true) = true,
inference(equality_encoding,[status(esa)],[c29]) ).
fof(f33,axiom,
cUnsatisfiable(i2003_11_14_17_21_262),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_11) ).
fof(f33_nnf,plain,
cUnsatisfiable(i2003_11_14_17_21_262),
inference(nnf_transformation,[status(thm)],[f33]) ).
cnf(c53,plain,
cUnsatisfiable(i2003_11_14_17_21_262),
inference(cnf_transformation,[status(esa)],[f33_nnf]) ).
cnf(hi50,axiom,
cUnsatisfiable(i2003_11_14_17_21_262) = true,
inference(equality_encoding,[status(esa)],[c53]) ).
cnf(h0,plain,
ca_Ax3(sk1(i2003_11_14_17_21_262)) = true,
inference(hyper_resolution,[status(thm)],[hi28,hi50]) ).
fof(f29,axiom,
! [X] :
( ca_Ax3(X)
<=> ( cpxcomp(X)
& cqxcomp(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_7) ).
fof(f29_nnf,plain,
! [X] :
( ( ~ cpxcomp(X)
| ~ cqxcomp(X)
| ca_Ax3(X) )
& ( ( cpxcomp(X)
& cqxcomp(X) )
| ~ ca_Ax3(X) ) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [X] :
( ( ~ cpxcomp(X)
| ~ cqxcomp(X)
| ca_Ax3(X) )
& ( ( cpxcomp(X)
& cqxcomp(X) )
| ~ ca_Ax3(X) ) ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c40,plain,
( cpxcomp(X0)
| ~ ca_Ax3(X0) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(hi37,axiom,
ifeq(ca_Ax3(X0),true,cpxcomp(X0),true) = true,
inference(equality_encoding,[status(esa)],[c40]) ).
cnf(h6,plain,
cpxcomp(sk1(i2003_11_14_17_21_262)) = true,
inference(hyper_resolution,[status(thm)],[hi37,h0]) ).
fof(f26,axiom,
! [X] :
( cpxcomp(X)
<=> ? [Y0] : ra_Px1(X,Y0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_4) ).
fof(f26_nnf,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px1(X,Y0)
| cpxcomp(X) )
& ( ? [Y0] : ra_Px1(X,Y0)
| ~ cpxcomp(X) ) ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [X,Y0] :
( ( ~ ra_Px1(X,Y0)
| cpxcomp(X) )
& ( ra_Px1(X,sk3(X))
| ~ cpxcomp(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk3])],[f26_nnf]) ).
cnf(c33,plain,
( ra_Px1(X0,sk3(X0))
| ~ cpxcomp(X0) ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(hi31,axiom,
ifeq(cpxcomp(X0),true,ra_Px1(X0,sk3(X0)),true) = true,
inference(equality_encoding,[status(esa)],[c33]) ).
cnf(h14,plain,
ra_Px1(sk1(i2003_11_14_17_21_262),sk3(sk1(i2003_11_14_17_21_262))) = true,
inference(hyper_resolution,[status(thm)],[hi31,h6]) ).
cnf(c28,plain,
( rs(X0,sk1(X0))
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(hi27,axiom,
ifeq(cUnsatisfiable(X0),true,rs(X0,sk1(X0)),true) = true,
inference(equality_encoding,[status(esa)],[c28]) ).
cnf(h1,plain,
rs(i2003_11_14_17_21_262,sk1(i2003_11_14_17_21_262)) = true,
inference(hyper_resolution,[status(thm)],[hi27,hi50]) ).
cnf(c27,plain,
( ca_Ax4(sk0(X0))
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(hi26,axiom,
ifeq(cUnsatisfiable(X0),true,ca_Ax4(sk0(X0)),true) = true,
inference(equality_encoding,[status(esa)],[c27]) ).
cnf(h2,plain,
ca_Ax4(sk0(i2003_11_14_17_21_262)) = true,
inference(hyper_resolution,[status(thm)],[hi26,hi50]) ).
fof(f30,axiom,
! [X] :
( ca_Ax4(X)
<=> ( ? [Y] :
( ca_Vx5(Y)
& rinvR(X,Y) )
& ! [Y0,Y1] :
( ( rinvR(X,Y1)
& rinvR(X,Y0) )
=> Y0 = Y1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_8) ).
fof(f30_nnf,plain,
! [X] :
( ( ! [Y] :
( ~ ca_Vx5(Y)
| ~ rinvR(X,Y) )
| ? [Y0,Y1] :
( Y0 != Y1
& rinvR(X,Y1)
& rinvR(X,Y0) )
| ca_Ax4(X) )
& ( ( ? [Y] :
( ca_Vx5(Y)
& rinvR(X,Y) )
& ! [Y0,Y1] :
( Y0 = Y1
| ~ rinvR(X,Y1)
| ~ rinvR(X,Y0) ) )
| ~ ca_Ax4(X) ) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [X,Y0,Y1,Y] :
( ( ~ ca_Vx5(Y)
| ~ rinvR(X,Y)
| ( sk7(X) != sk8(X)
& rinvR(X,sk8(X))
& rinvR(X,sk7(X)) )
| ca_Ax4(X) )
& ( ( ca_Vx5(sk6(X))
& rinvR(X,sk6(X))
& ( Y0 = Y1
| ~ rinvR(X,Y1)
| ~ rinvR(X,Y0) ) )
| ~ ca_Ax4(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk6,sk7,sk8])],[f30_nnf]) ).
cnf(c44,plain,
( ca_Vx5(sk6(X0))
| ~ ca_Ax4(X0) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(hi41,axiom,
ifeq(ca_Ax4(X0),true,ca_Vx5(sk6(X0)),true) = true,
inference(equality_encoding,[status(esa)],[c44]) ).
cnf(h10,plain,
ca_Vx5(sk6(sk0(i2003_11_14_17_21_262))) = true,
inference(hyper_resolution,[status(thm)],[hi41,h2]) ).
cnf(c43,plain,
( rinvR(X0,sk6(X0))
| ~ ca_Ax4(X0) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(hi40,axiom,
ifeq(ca_Ax4(X0),true,rinvR(X0,sk6(X0)),true) = true,
inference(equality_encoding,[status(esa)],[c43]) ).
cnf(h11,plain,
rinvR(sk0(i2003_11_14_17_21_262),sk6(sk0(i2003_11_14_17_21_262))) = true,
inference(hyper_resolution,[status(thm)],[hi40,h2]) ).
cnf(c26,plain,
( rr(X0,sk0(X0))
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(hi25,axiom,
ifeq(cUnsatisfiable(X0),true,rr(X0,sk0(X0)),true) = true,
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(h3,plain,
rr(i2003_11_14_17_21_262,sk0(i2003_11_14_17_21_262)) = true,
inference(hyper_resolution,[status(thm)],[hi25,hi50]) ).
fof(f32,axiom,
! [X,Y] :
( rinvR(X,Y)
<=> rr(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_10) ).
fof(f32_nnf,plain,
! [X,Y] :
( ( ~ rr(Y,X)
| rinvR(X,Y) )
& ( rr(Y,X)
| ~ rinvR(X,Y) ) ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [X,Y] :
( ( ~ rr(Y,X)
| rinvR(X,Y) )
& ( rr(Y,X)
| ~ rinvR(X,Y) ) ),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c52,plain,
( ~ rr(X1,X0)
| rinvR(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(hi49,axiom,
ifeq(rr(X0,X1),true,rinvR(X1,X0),true) = true,
inference(equality_encoding,[status(esa)],[c52]) ).
cnf(h23,plain,
rinvR(sk0(i2003_11_14_17_21_262),i2003_11_14_17_21_262) = true,
inference(hyper_resolution,[status(thm)],[hi49,h3]) ).
cnf(c42,plain,
( X1 = X2
| ~ rinvR(X0,X2)
| ~ rinvR(X0,X1)
| ~ ca_Ax4(X0) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(hi39,axiom,
ifeq(ca_Ax4(X0),true,ifeq(rinvR(X0,X1),true,ifeq(rinvR(X0,X2),true,X1,X2),X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c42]) ).
cnf(h97,plain,
i2003_11_14_17_21_262 = sk6(sk0(i2003_11_14_17_21_262)),
inference(hyper_resolution,[status(thm)],[hi39,h2,h23,h11]) ).
fof(f3,axiom,
! [A,B] :
( ( ca_Vx5(A)
& A = B )
=> ca_Vx5(B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ca_Vx5_substitution_1) ).
fof(f3_nnf,plain,
! [A,B] :
( ca_Vx5(B)
| ~ ca_Vx5(A)
| A != B ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,B] :
( ca_Vx5(B)
| ~ ca_Vx5(A)
| A != B ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( ca_Vx5(X1)
| ~ ca_Vx5(X0)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(hi3,axiom,
ifeq(X0,X1,ifeq(ca_Vx5(X0),true,ca_Vx5(X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(h104,plain,
ca_Vx5(i2003_11_14_17_21_262) = true,
inference(hyper_resolution,[status(thm)],[hi3,h97,h10]) ).
fof(f31,axiom,
! [X] :
( ca_Vx5(X)
<=> ! [Y] :
( rs(X,Y)
=> cp(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_9) ).
fof(f31_nnf,plain,
! [X] :
( ( ? [Y] :
( ~ cp(Y)
& rs(X,Y) )
| ca_Vx5(X) )
& ( ! [Y] :
( cp(Y)
| ~ rs(X,Y) )
| ~ ca_Vx5(X) ) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [X,Y] :
( ( ( ~ cp(sk9(X))
& rs(X,sk9(X)) )
| ca_Vx5(X) )
& ( cp(Y)
| ~ rs(X,Y)
| ~ ca_Vx5(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk9])],[f31_nnf]) ).
cnf(c48,plain,
( cp(X1)
| ~ rs(X0,X1)
| ~ ca_Vx5(X0) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(hi45,axiom,
ifeq(ca_Vx5(X0),true,ifeq(rs(X0,X1),true,cp(X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c48]) ).
cnf(h105,plain,
cp(sk1(i2003_11_14_17_21_262)) = true,
inference(hyper_resolution,[status(thm)],[hi45,h104,h1]) ).
fof(f25,axiom,
! [X] :
( cp(X)
<=> ~ ? [Y] : ra_Px1(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3) ).
fof(f25_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px1(X,Y)
| cp(X) )
& ( ! [Y] : ~ ra_Px1(X,Y)
| ~ cp(X) ) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [X,Y] :
( ( ra_Px1(X,sk2(X))
| cp(X) )
& ( ~ ra_Px1(X,Y)
| ~ cp(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk2])],[f25_nnf]) ).
cnf(c31,plain,
( ~ ra_Px1(X0,X1)
| ~ cp(X0) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(hi53,axiom,
ifeq(cp(X0),true,ifeq(ra_Px1(X0,X1),true,false,true),true) = true,
inference(equality_encoding,[status(esa)],[c31]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi53,h105,h14]) ).
cnf(t219,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
fof(f22,axiom,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_0) ).
fof(f22_nnf,plain,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c23,plain,
~ cowlNothing(X0),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
fof(f23,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
fof(f23_nnf,plain,
! [X] :
( ( xsd_integer(X)
| xsd_string(X) )
& ( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [X] :
( ( xsd_integer(X)
| xsd_string(X) )
& ( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c24,plain,
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
fof(f28,axiom,
! [X] :
( cqxcomp(X)
<=> ~ ? [Y] : ra_Px2(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_6) ).
fof(f28_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px2(X,Y)
| cqxcomp(X) )
& ( ! [Y] : ~ ra_Px2(X,Y)
| ~ cqxcomp(X) ) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [X,Y] :
( ( ra_Px2(X,sk5(X))
| cqxcomp(X) )
& ( ~ ra_Px2(X,Y)
| ~ cqxcomp(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk5])],[f28_nnf]) ).
cnf(c37,plain,
( ~ ra_Px2(X0,X1)
| ~ cqxcomp(X0) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c23,c24,c31,c37]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t219]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS114+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n002.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Wed Sep 23 19:28:04 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 1.92/1.30 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.92/1.30 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------