%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : KRS261+1 : TPTP v9.3.1. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:23 AM UTC 2026
% Result : Theorem 35.62s 10.18s
% Output : CNFRefutation 35.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 5
% Syntax : Number of formulae : 35 ( 10 unt; 0 def)
% Number of atoms : 136 ( 0 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 156 ( 55 ~; 66 |; 30 &)
% ( 4 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-2 aty)
% Number of variables : 96 ( 9 sgn 49 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(thm,axiom,
! [Ax,C] :
( ! [I1] :
( model(I1,Ax)
=> model(I1,C) )
<=> status(Ax,C,thm) ),
file('theBenchmark.p',thm) ).
fof(eth,axiom,
! [Ax,C] :
( ( ! [I3] :
( model(I3,Ax)
<=> model(I3,C) )
& ? [I2] : ~ model(I2,Ax)
& ? [I1] : model(I1,Ax) )
<=> status(Ax,C,eth) ),
file('theBenchmark.p',eth) ).
fof(mighta,axiom,
! [S1,S2] :
( ? [Ax,C] :
( status(Ax,C,S2)
& status(Ax,C,S1) )
<=> mighta(S1,S2) ),
file('theBenchmark.p',mighta) ).
fof(non_thm_spt,axiom,
? [I1,Ax,C] :
( ? [I2] : model(I2,C)
& ~ model(I1,C)
& model(I1,Ax) ),
file('theBenchmark.p',non_thm_spt) ).
fof(mighta_eth_thm,conjecture,
mighta(eth,thm),
file('theBenchmark.p',mighta_eth_thm) ).
fof(mighta_eth_thm_neg,negated_conjecture,
~ mighta(eth,thm),
inference(assume_negation,[status(cth)],[mighta_eth_thm]) ).
cnf(c_35,plain,
( mighta(C,D)
| ~ status(A,B,D)
| ~ status(A,B,C) ),
inference(clausify,[status(thm)],[mighta]) ).
cnf(c_37,negated_conjecture,
~ mighta(eth,thm),
inference(clausify,[status(thm)],[mighta_eth_thm_neg]) ).
cnf(c_57,negated_conjecture,
( ~ status(A,B,thm)
| ~ status(A,B,eth) ),
inference(resolve,[status(thm)],[c_37,c_35]) ).
fof(nnf_32,plain,
? [I1,Ax,C] :
( ? [I2] : model(I2,C)
& ~ model(I1,C)
& model(I1,Ax) ),
inference(fof_nnf,[status(thm)],[non_thm_spt]) ).
fof(sk_non_thm_spt,plain,
( model(sK0,sK1)
& ~ model(sK2,sK1)
& model(sK2,sK7) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK7,sK1,sK0]),skolemize(I1,sK2),skolemize(Ax,sK7),skolemize(C,sK1),skolemize(I2,sK0)],[nnf_32]) ).
cnf(c_60,plain,
model(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_non_thm_spt]) ).
cnf(c_61,plain,
~ model(sK2,sK1),
inference(split_conjunct,[status(thm)],[sk_non_thm_spt]) ).
fof(nnf_9,plain,
! [Ax,C] :
( ( ~ status(Ax,C,eth)
| ( ! [I3] :
( ( ~ model(I3,C)
| model(I3,Ax) )
& ( model(I3,C)
| ~ model(I3,Ax) ) )
& ? [I2] : ~ model(I2,Ax)
& ? [I1] : model(I1,Ax) ) )
& ( status(Ax,C,eth)
| ? [X0] :
( ( ~ model(X0,C)
| ~ model(X0,Ax) )
& ( model(X0,C)
| model(X0,Ax) ) )
| ! [X1] : model(X1,Ax)
| ! [X2] : ~ model(X2,Ax) ) ),
inference(fof_nnf,[status(thm)],[eth]) ).
fof(sk_eth_sk,plain,
! [Ax,C] :
( ( ~ status(Ax,C,eth)
| ( ! [I3] :
( ( ~ model(I3,C)
| model(I3,Ax) )
& ( model(I3,C)
| ~ model(I3,Ax) ) )
& ~ model(sK9(Ax,C),Ax)
& model(sK8(Ax,C),Ax) ) )
& ( status(Ax,C,eth)
| ( ( ~ model(sK3(Ax,C),C)
| ~ model(sK3(Ax,C),Ax) )
& ( model(sK3(Ax,C),C)
| model(sK3(Ax,C),Ax) ) )
| ! [X1] : model(X1,Ax)
| ! [X2] : ~ model(X2,Ax) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK8,sK9]),skolemize(X0,sK3(Ax,C)),skolemize(I1,sK8(Ax,C)),skolemize(I2,sK9(Ax,C))],[nnf_9]) ).
fof(sk_eth,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ status(VAR_1,VAR_2,eth)
| ~ model(VAR_0,VAR_2)
| model(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ status(VAR_1,VAR_2,eth)
| model(VAR_0,VAR_2)
| ~ model(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( ~ status(VAR_0,VAR_1,eth)
| ~ model(sK9(VAR_0,VAR_1),VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ status(VAR_0,VAR_1,eth)
| model(sK8(VAR_0,VAR_1),VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( status(VAR_1,VAR_3,eth)
| ~ model(sK3(VAR_1,VAR_3),VAR_3)
| ~ model(sK3(VAR_1,VAR_3),VAR_1)
| model(VAR_2,VAR_1)
| ~ model(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( status(VAR_1,VAR_3,eth)
| model(sK3(VAR_1,VAR_3),VAR_3)
| model(sK3(VAR_1,VAR_3),VAR_1)
| model(VAR_2,VAR_1)
| ~ model(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_eth_sk]) ).
cnf(c_118,plain,
( status(B,D,eth)
| ~ model(sK3(B,D),D)
| ~ model(sK3(B,D),B)
| model(C,B)
| ~ model(A,B) ),
inference(split_conjunct,[status(thm)],[sk_eth]) ).
cnf(c_119,plain,
( status(B,D,eth)
| model(sK3(B,D),D)
| model(sK3(B,D),B)
| model(C,B)
| ~ model(A,B) ),
inference(split_conjunct,[status(thm)],[sk_eth]) ).
fof(nnf_5,plain,
! [Ax,C] :
( ( ~ status(Ax,C,thm)
| ! [I1] :
( model(I1,C)
| ~ model(I1,Ax) ) )
& ( status(Ax,C,thm)
| ? [X0] :
( ~ model(X0,C)
& model(X0,Ax) ) ) ),
inference(fof_nnf,[status(thm)],[thm]) ).
fof(sk_thm_sk,plain,
! [Ax,C] :
( ( ~ status(Ax,C,thm)
| ! [I1] :
( model(I1,C)
| ~ model(I1,Ax) ) )
& ( status(Ax,C,thm)
| ( ~ model(sK4(Ax,C),C)
& model(sK4(Ax,C),Ax) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X0,sK4(Ax,C))],[nnf_5]) ).
fof(sk_thm,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ status(VAR_1,VAR_2,thm)
| model(VAR_0,VAR_2)
| ~ model(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( status(VAR_0,VAR_1,thm)
| ~ model(sK4(VAR_0,VAR_1),VAR_1) )
& ! [VAR_0,VAR_1] :
( status(VAR_0,VAR_1,thm)
| model(sK4(VAR_0,VAR_1),VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_thm_sk]) ).
cnf(c_135,plain,
( status(A,B,thm)
| ~ model(sK4(A,B),B) ),
inference(split_conjunct,[status(thm)],[sk_thm]) ).
cnf(c_136,plain,
( status(A,B,thm)
| model(sK4(A,B),A) ),
inference(split_conjunct,[status(thm)],[sk_thm]) ).
cnf(c_160,plain,
( status(A,B,eth)
| ~ model(sK3(A,B),B)
| model(C,A)
| ~ model(sK3(A,B),A) ),
inference(factor,[status(thm)],[c_118]) ).
cnf(c_162,plain,
( status(B,C,eth)
| model(sK3(B,C),C)
| model(sK3(B,C),B)
| ~ model(A,B) ),
inference(factor,[status(thm)],[c_119]) ).
cnf(c_12602,plain,
( status(A,A,thm)
| status(A,A,thm) ),
inference(resolve,[status(thm)],[c_136,c_135]) ).
cnf(c_625,plain,
status(A,A,thm),
inference(copy,[status(thm)],[c_12602]) ).
cnf(c_1104,plain,
( status(sK1,A,eth)
| model(sK3(sK1,A),A)
| model(sK3(sK1,A),sK1) ),
inference(resolve,[status(thm)],[c_162,c_60]) ).
cnf(c_1119,plain,
( status(sK1,sK1,eth)
| model(sK3(sK1,sK1),sK1) ),
inference(factor,[status(thm)],[c_1104]) ).
cnf(c_1288,plain,
~ status(A,A,eth),
inference(resolve,[status(thm)],[c_625,c_57]) ).
cnf(c_1296,plain,
model(sK3(sK1,sK1),sK1),
inference(resolve,[status(thm)],[c_1288,c_1119]) ).
cnf(c_12603,plain,
( status(sK1,sK1,eth)
| model(A,sK1)
| ~ model(sK3(sK1,sK1),sK1) ),
inference(resolve,[status(thm)],[c_1296,c_160]) ).
cnf(c_12604,plain,
( status(sK1,sK1,eth)
| model(A,sK1) ),
inference(resolve,[status(thm)],[c_1296,c_12603]) ).
cnf(c_12600,plain,
model(A,sK1),
inference(resolve,[status(thm)],[c_1288,c_12604]) ).
cnf(c_12601,plain,
$false,
inference(resolve,[status(thm)],[c_12600,c_61]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS261+1 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.59 % Computer : n004.cluster.edu
% 0.10/5.59 % Model : x86_64 x86_64
% 0.10/5.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.59 % Memory : 8046.5625MB
% 0.10/5.59 % OS : Linux 6.8.0-71-generic
% 0.10/5.59 % CPULimit : 300
% 0.10/5.59 % WCLimit : 300
% 0.10/5.59 % DateTime : Fri Sep 25 19:50:42 UTC 2026
% 0.10/5.59 % CPUTime :
% 0.10/5.59 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/5.59 % Process 3937463 was started by sandbox2 on n004,
% 0.10/5.59 % Fri Sep 25 19:50:42 2026
% 0.10/5.59 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.14/5.61
% 0.14/5.61 % From the command line: assign(max_seconds, 300).
% 35.62/10.18
% 35.62/10.18 % given #500 (T,wt=6): 8790 status(c11,c1,esa). [resolve(738,a,74,a)].
% 35.62/10.18
% 35.62/10.18 % SZS status Theorem for theBenchmark
% 35.62/10.18
% 35.62/10.18 % Proof 1 at 3.90 (+ 0.53) seconds.
% 35.62/10.18 % Length of proof is 23.
% 35.62/10.18 % Level of proof is 7.
% 35.62/10.18 % Maximum clause weight is 24.000.
% 35.62/10.18 % Given clauses 564.
% 35.62/10.18
% 35.62/10.18 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------