%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : KRS013-1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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:45:54 AM UTC 2026
% Result : Unsatisfiable 0.07s 15.45s
% Output : CNFRefutation 0.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 16
% Syntax : Number of formulae : 56 ( 15 unt; 0 def)
% Number of atoms : 120 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 122 ( 58 ~; 64 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 13 ( 12 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-1 aty)
% Number of variables : 54 ( 0 sgn 20 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(clause_15,axiom,
! [VAR_0,VAR_1] :
( ~ r(VAR_1,VAR_0)
| ~ e(VAR_1)
| d(VAR_0) ),
file('theBenchmark.p',clause_15) ).
cnf(c_1,plain,
( ~ r(B,A)
| ~ e(B)
| d(A) ),
inference(clausify,[status(thm)],[clause_15]) ).
fof(clause_1,axiom,
e(exist),
file('theBenchmark.p',clause_1) ).
cnf(c_2,plain,
e(exist),
inference(clausify,[status(thm)],[clause_1]) ).
fof(clause_16,axiom,
! [VAR_0,VAR_1] :
( ~ s2least(VAR_0)
| ~ r(VAR_1,VAR_0)
| ~ e(VAR_1)
| c(VAR_0) ),
file('theBenchmark.p',clause_16) ).
cnf(c_3,plain,
( ~ s2least(A)
| ~ r(B,A)
| ~ e(B)
| c(A) ),
inference(clausify,[status(thm)],[clause_16]) ).
fof(clause_28,axiom,
! [VAR_0] :
( ~ s1most(u6r1(VAR_0))
| f(VAR_0) ),
file('theBenchmark.p',clause_28) ).
cnf(c_11,plain,
( ~ s1most(u6r1(A))
| f(A) ),
inference(clausify,[status(thm)],[clause_28]) ).
fof(clause_29,axiom,
! [VAR_0] :
( r(VAR_0,u6r1(VAR_0))
| f(VAR_0) ),
file('theBenchmark.p',clause_29) ).
cnf(c_12,plain,
( r(A,u6r1(A))
| f(A) ),
inference(clausify,[status(thm)],[clause_29]) ).
fof(clause_2,axiom,
~ f(exist),
file('theBenchmark.p',clause_2) ).
cnf(c_13,plain,
~ f(exist),
inference(clausify,[status(thm)],[clause_2]) ).
fof(clause_3,axiom,
! [VAR_0] :
( ~ c(VAR_0)
| t2least(VAR_0) ),
file('theBenchmark.p',clause_3) ).
cnf(c_15,plain,
( ~ c(A)
| t2least(A) ),
inference(clausify,[status(thm)],[clause_3]) ).
fof(clause_5,axiom,
! [VAR_0] :
( ~ equalish(u1r2(VAR_0),u1r1(VAR_0))
| ~ t2least(VAR_0) ),
file('theBenchmark.p',clause_5) ).
cnf(c_16,plain,
( ~ equalish(u1r2(A),u1r1(A))
| ~ t2least(A) ),
inference(clausify,[status(thm)],[clause_5]) ).
fof(clause_6,axiom,
! [VAR_0] :
( ~ t2least(VAR_0)
| t(VAR_0,u1r1(VAR_0)) ),
file('theBenchmark.p',clause_6) ).
cnf(c_17,plain,
( ~ t2least(A)
| t(A,u1r1(A)) ),
inference(clausify,[status(thm)],[clause_6]) ).
fof(clause_7,axiom,
! [VAR_0] :
( ~ t2least(VAR_0)
| t(VAR_0,u1r2(VAR_0)) ),
file('theBenchmark.p',clause_7) ).
cnf(c_18,plain,
( ~ t2least(A)
| t(A,u1r2(A)) ),
inference(clausify,[status(thm)],[clause_7]) ).
fof(clause_11,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ t(VAR_2,VAR_1)
| ~ t(VAR_2,VAR_0)
| ~ t1most(VAR_2)
| equalish(VAR_0,VAR_1) ),
file('theBenchmark.p',clause_11) ).
cnf(c_20,plain,
( ~ t(C,B)
| ~ t(C,A)
| ~ t1most(C)
| equalish(A,B) ),
inference(clausify,[status(thm)],[clause_11]) ).
fof(clause_9,axiom,
! [VAR_0] :
( ~ d(VAR_0)
| t1most(VAR_0) ),
file('theBenchmark.p',clause_9) ).
cnf(c_25,plain,
( ~ d(A)
| t1most(A) ),
inference(clausify,[status(thm)],[clause_9]) ).
cnf(c_26,plain,
( ~ t(A,C)
| ~ t(A,B)
| equalish(B,C)
| ~ d(A) ),
inference(resolve,[status(thm)],[c_25,c_20]) ).
cnf(c_33,plain,
r(exist,u6r1(exist)),
inference(resolve,[status(thm)],[c_13,c_12]) ).
cnf(c_34,plain,
~ s1most(u6r1(exist)),
inference(resolve,[status(thm)],[c_13,c_11]) ).
fof(clause_26,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ s(VAR_0,VAR_2)
| ~ s(VAR_0,VAR_1)
| equalish(VAR_1,VAR_2)
| s2least(VAR_0) ),
file('theBenchmark.p',clause_26) ).
cnf(c_40,plain,
( ~ s(A,C)
| ~ s(A,B)
| equalish(B,C)
| s2least(A) ),
inference(clausify,[status(thm)],[clause_26]) ).
fof(clause_31,axiom,
! [VAR_0] :
( ~ equalish(u7r2(VAR_0),u7r1(VAR_0))
| s1most(VAR_0) ),
file('theBenchmark.p',clause_31) ).
cnf(c_42,plain,
( ~ equalish(u7r2(A),u7r1(A))
| s1most(A) ),
inference(clausify,[status(thm)],[clause_31]) ).
fof(clause_32,axiom,
! [VAR_0] :
( s(VAR_0,u7r1(VAR_0))
| s1most(VAR_0) ),
file('theBenchmark.p',clause_32) ).
cnf(c_43,plain,
( s(A,u7r1(A))
| s1most(A) ),
inference(clausify,[status(thm)],[clause_32]) ).
fof(clause_33,axiom,
! [VAR_0] :
( s(VAR_0,u7r2(VAR_0))
| s1most(VAR_0) ),
file('theBenchmark.p',clause_33) ).
cnf(c_44,plain,
( s(A,u7r2(A))
| s1most(A) ),
inference(clausify,[status(thm)],[clause_33]) ).
cnf(c_45,plain,
( ~ r(exist,A)
| d(A) ),
inference(resolve,[status(thm)],[c_1,c_2]) ).
cnf(c_46,plain,
( ~ s2least(A)
| ~ r(exist,A)
| c(A) ),
inference(resolve,[status(thm)],[c_3,c_2]) ).
cnf(c_59,plain,
( ~ c(A)
| ~ equalish(u1r2(A),u1r1(A)) ),
inference(resolve,[status(thm)],[c_16,c_15]) ).
cnf(c_60,plain,
( ~ c(A)
| t(A,u1r1(A)) ),
inference(resolve,[status(thm)],[c_17,c_15]) ).
cnf(c_61,plain,
( ~ c(A)
| t(A,u1r2(A)) ),
inference(resolve,[status(thm)],[c_18,c_15]) ).
cnf(c_76,plain,
~ equalish(u7r2(u6r1(exist)),u7r1(u6r1(exist))),
inference(resolve,[status(thm)],[c_42,c_34]) ).
cnf(c_77,plain,
( ~ s(A,B)
| equalish(B,u7r1(A))
| s2least(A)
| s1most(A) ),
inference(resolve,[status(thm)],[c_43,c_40]) ).
cnf(c_81,plain,
d(u6r1(exist)),
inference(resolve,[status(thm)],[c_45,c_33]) ).
cnf(c_82,plain,
( ~ s2least(u6r1(exist))
| c(u6r1(exist)) ),
inference(resolve,[status(thm)],[c_46,c_33]) ).
cnf(c_125,plain,
( s1most(A)
| equalish(u7r2(A),u7r1(A))
| s2least(A)
| s1most(A) ),
inference(resolve,[status(thm)],[c_77,c_44]) ).
cnf(c_103,plain,
( equalish(u7r2(A),u7r1(A))
| s2least(A)
| s1most(A) ),
inference(copy,[status(thm)],[c_125]) ).
cnf(c_126,plain,
( s2least(u6r1(exist))
| s1most(u6r1(exist)) ),
inference(resolve,[status(thm)],[c_103,c_76]) ).
cnf(c_104,plain,
s2least(u6r1(exist)),
inference(resolve,[status(thm)],[c_34,c_126]) ).
cnf(c_106,plain,
c(u6r1(exist)),
inference(resolve,[status(thm)],[c_104,c_82]) ).
cnf(c_111,plain,
t(u6r1(exist),u1r2(u6r1(exist))),
inference(resolve,[status(thm)],[c_106,c_61]) ).
cnf(c_112,plain,
t(u6r1(exist),u1r1(u6r1(exist))),
inference(resolve,[status(thm)],[c_106,c_60]) ).
cnf(c_113,plain,
~ equalish(u1r2(u6r1(exist)),u1r1(u6r1(exist))),
inference(resolve,[status(thm)],[c_59,c_106]) ).
cnf(c_127,plain,
( ~ t(u6r1(exist),B)
| ~ t(u6r1(exist),A)
| equalish(A,B) ),
inference(resolve,[status(thm)],[c_26,c_81]) ).
cnf(c_128,plain,
( ~ t(u6r1(exist),u1r1(u6r1(exist)))
| ~ t(u6r1(exist),u1r2(u6r1(exist))) ),
inference(resolve,[status(thm)],[c_127,c_113]) ).
cnf(c_129,plain,
~ t(u6r1(exist),u1r1(u6r1(exist))),
inference(resolve,[status(thm)],[c_128,c_111]) ).
cnf(c_124,plain,
$false,
inference(resolve,[status(thm)],[c_112,c_129]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS013-1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n016.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.07/15.42 % CPULimit : 300
% 0.07/15.42 % WCLimit : 300
% 0.07/15.42 % DateTime : Fri Sep 25 19:33:21 UTC 2026
% 0.07/15.42 % CPUTime :
% 0.07/15.42 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/15.42 % Process 3892980 was started by sandbox on n004,
% 0.07/15.42 % Fri Sep 25 19:33:21 2026
% 0.07/15.42 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.07/15.43
% 0.07/15.43 % From the command line: assign(max_seconds, 300).
% 0.07/15.45
% 0.07/15.45 % SZS status Unsatisfiable for theBenchmark
% 0.07/15.45
% 0.07/15.45 % Proof 1 at 0.01 (+ 0.01) seconds.
% 0.07/15.45 % Length of proof is 35.
% 0.07/15.45 % Level of proof is 6.
% 0.07/15.45 % Maximum clause weight is 11.000.
% 0.07/15.45 % Given clauses 69.
% 0.07/15.45
% 0.07/15.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------