%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN549+1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 09:38:48 AM UTC 2026
% Result : Theorem 0.13s 0.39s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 3
% Syntax : Number of formulae : 126 ( 12 unt; 0 def)
% Number of atoms : 524 ( 0 equ)
% Maximal formula atoms : 80 ( 4 avg)
% Number of connectives : 559 ( 161 ~; 350 |; 43 &)
% ( 2 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-1 aty)
% Number of variables : 96 ( 0 sgn 43 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(reflexivity_of_reachable,axiom,
! [X] : reachable(X,X),
file('theBenchmark.p',reflexivity_of_reachable) ).
fof(transitivity_of_reachable,axiom,
! [X,Y,Z] :
( ( reachable(Y,Z)
& reachable(X,Y) )
=> reachable(X,Z) ),
file('theBenchmark.p',transitivity_of_reachable) ).
fof(prove_this,conjecture,
? [X] :
( ! [Y] :
( reachable(X,Y)
=> ( ? [Z] :
( ( ? [V] :
( q(V)
& reachable(Z,V) )
| p(Z) )
& reachable(Y,Z) )
<=> ( ? [W] :
( q(W)
& reachable(Y,W) )
| ? [W] :
( p(W)
& reachable(Y,W) ) ) ) )
& reachable(initial_world,X) ),
file('theBenchmark.p',prove_this) ).
fof(prove_this_neg,negated_conjecture,
~ ? [X] :
( ! [Y] :
( reachable(X,Y)
=> ( ? [Z] :
( ( ? [V] :
( q(V)
& reachable(Z,V) )
| p(Z) )
& reachable(Y,Z) )
<=> ( ? [W] :
( q(W)
& reachable(Y,W) )
| ? [W] :
( p(W)
& reachable(Y,W) ) ) ) )
& reachable(initial_world,X) ),
inference(assume_negation,[status(cth)],[prove_this]) ).
cnf(c_4,plain,
reachable(A,A),
inference(clausify,[status(thm)],[reflexivity_of_reachable]) ).
cnf(c_5,plain,
( reachable(A,C)
| ~ reachable(B,C)
| ~ reachable(A,B) ),
inference(clausify,[status(thm)],[transitivity_of_reachable]) ).
fof(nnf_3,plain,
! [X] :
( ? [Y] :
( ( ( ! [W] :
( ~ q(W)
| ~ reachable(Y,W) )
& ! [X4] :
( ~ p(X4)
| ~ reachable(Y,X4) ) )
| ! [Z] :
( ( ! [V] :
( ~ q(V)
| ~ reachable(Z,V) )
& ~ p(Z) )
| ~ reachable(Y,Z) ) )
& ( ? [X3] :
( q(X3)
& reachable(Y,X3) )
| ? [X2] :
( p(X2)
& reachable(Y,X2) )
| ? [X0] :
( ( ? [X1] :
( q(X1)
& reachable(X0,X1) )
| p(X0) )
& reachable(Y,X0) ) )
& reachable(X,Y) )
| ~ reachable(initial_world,X) ),
inference(fof_nnf,[status(thm)],[prove_this_neg]) ).
fof(sk_prove_this_neg_sk,plain,
! [X] :
( ( ( ( ! [W] :
( ~ q(W)
| ~ reachable(sK0(X),W) )
& ! [X4] :
( ~ p(X4)
| ~ reachable(sK0(X),X4) ) )
| ! [Z] :
( ( ! [V] :
( ~ q(V)
| ~ reachable(Z,V) )
& ~ p(Z) )
| ~ reachable(sK0(X),Z) ) )
& ( ( q(sK3(X))
& reachable(sK0(X),sK3(X)) )
| ( p(sK2(X))
& reachable(sK0(X),sK2(X)) )
| ( ( ( q(sK4(X))
& reachable(sK1(X),sK4(X)) )
| p(sK1(X)) )
& reachable(sK0(X),sK1(X)) ) )
& reachable(X,sK0(X)) )
| ~ reachable(initial_world,X) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK4,sK2,sK3]),skolemize(Y,sK0(X)),skolemize(X0,sK1(X)),skolemize(X1,sK4(X)),skolemize(X2,sK2(X)),skolemize(X3,sK3(X))],[nnf_3]) ).
fof(sk_prove_this_neg,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ q(VAR_3)
| ~ reachable(sK0(VAR_0),VAR_3)
| ~ q(VAR_2)
| ~ reachable(VAR_1,VAR_2)
| ~ reachable(sK0(VAR_0),VAR_1)
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p(VAR_3)
| ~ reachable(sK0(VAR_0),VAR_3)
| ~ q(VAR_2)
| ~ reachable(VAR_1,VAR_2)
| ~ reachable(sK0(VAR_0),VAR_1)
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ q(VAR_2)
| ~ reachable(sK0(VAR_0),VAR_2)
| ~ p(VAR_1)
| ~ reachable(sK0(VAR_0),VAR_1)
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p(VAR_2)
| ~ reachable(sK0(VAR_0),VAR_2)
| ~ p(VAR_1)
| ~ reachable(sK0(VAR_0),VAR_1)
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( q(sK3(VAR_0))
| p(sK2(VAR_0))
| q(sK4(VAR_0))
| p(sK1(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( reachable(sK0(VAR_0),sK3(VAR_0))
| p(sK2(VAR_0))
| q(sK4(VAR_0))
| p(sK1(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( q(sK3(VAR_0))
| reachable(sK0(VAR_0),sK2(VAR_0))
| q(sK4(VAR_0))
| p(sK1(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( reachable(sK0(VAR_0),sK3(VAR_0))
| reachable(sK0(VAR_0),sK2(VAR_0))
| q(sK4(VAR_0))
| p(sK1(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( q(sK3(VAR_0))
| p(sK2(VAR_0))
| reachable(sK1(VAR_0),sK4(VAR_0))
| p(sK1(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( reachable(sK0(VAR_0),sK3(VAR_0))
| p(sK2(VAR_0))
| reachable(sK1(VAR_0),sK4(VAR_0))
| p(sK1(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( q(sK3(VAR_0))
| reachable(sK0(VAR_0),sK2(VAR_0))
| reachable(sK1(VAR_0),sK4(VAR_0))
| p(sK1(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( reachable(sK0(VAR_0),sK3(VAR_0))
| reachable(sK0(VAR_0),sK2(VAR_0))
| reachable(sK1(VAR_0),sK4(VAR_0))
| p(sK1(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( q(sK3(VAR_0))
| p(sK2(VAR_0))
| reachable(sK0(VAR_0),sK1(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( reachable(sK0(VAR_0),sK3(VAR_0))
| p(sK2(VAR_0))
| reachable(sK0(VAR_0),sK1(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( q(sK3(VAR_0))
| reachable(sK0(VAR_0),sK2(VAR_0))
| reachable(sK0(VAR_0),sK1(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( reachable(sK0(VAR_0),sK3(VAR_0))
| reachable(sK0(VAR_0),sK2(VAR_0))
| reachable(sK0(VAR_0),sK1(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( reachable(VAR_0,sK0(VAR_0))
| ~ reachable(initial_world,VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_prove_this_neg_sk]) ).
cnf(c_7,negated_conjecture,
( reachable(sK0(A),sK3(A))
| reachable(sK0(A),sK2(A))
| reachable(sK0(A),sK1(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_8,negated_conjecture,
( q(sK3(A))
| reachable(sK0(A),sK2(A))
| reachable(sK0(A),sK1(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_9,negated_conjecture,
( reachable(sK0(A),sK3(A))
| p(sK2(A))
| reachable(sK0(A),sK1(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_10,negated_conjecture,
( q(sK3(A))
| p(sK2(A))
| reachable(sK0(A),sK1(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_11,negated_conjecture,
( reachable(sK0(A),sK3(A))
| reachable(sK0(A),sK2(A))
| reachable(sK1(A),sK4(A))
| p(sK1(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_12,negated_conjecture,
( q(sK3(A))
| reachable(sK0(A),sK2(A))
| reachable(sK1(A),sK4(A))
| p(sK1(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_13,negated_conjecture,
( reachable(sK0(A),sK3(A))
| p(sK2(A))
| reachable(sK1(A),sK4(A))
| p(sK1(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_14,negated_conjecture,
( q(sK3(A))
| p(sK2(A))
| reachable(sK1(A),sK4(A))
| p(sK1(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_15,negated_conjecture,
( reachable(sK0(A),sK3(A))
| reachable(sK0(A),sK2(A))
| q(sK4(A))
| p(sK1(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_16,negated_conjecture,
( q(sK3(A))
| reachable(sK0(A),sK2(A))
| q(sK4(A))
| p(sK1(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_17,negated_conjecture,
( reachable(sK0(A),sK3(A))
| p(sK2(A))
| q(sK4(A))
| p(sK1(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_18,negated_conjecture,
( q(sK3(A))
| p(sK2(A))
| q(sK4(A))
| p(sK1(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_19,negated_conjecture,
( ~ p(C)
| ~ reachable(sK0(A),C)
| ~ p(B)
| ~ reachable(sK0(A),B)
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_22,negated_conjecture,
( ~ q(D)
| ~ reachable(sK0(A),D)
| ~ q(C)
| ~ reachable(B,C)
| ~ reachable(sK0(A),B)
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_653,plain,
( ~ p(B)
| ~ p(B)
| ~ reachable(sK0(A),B)
| ~ reachable(initial_world,A) ),
inference(factor,[status(thm)],[c_19]) ).
cnf(c_23,plain,
( ~ p(B)
| ~ reachable(sK0(A),B)
| ~ reachable(initial_world,A) ),
inference(copy,[status(thm)],[c_653]) ).
cnf(c_654,plain,
( ~ q(B)
| ~ q(B)
| ~ reachable(sK0(A),B)
| ~ reachable(sK0(A),sK0(A))
| ~ reachable(initial_world,A) ),
inference(factor,[status(thm)],[c_22]) ).
cnf(c_655,plain,
( ~ q(B)
| ~ reachable(sK0(A),B)
| ~ reachable(sK0(A),sK0(A))
| ~ reachable(initial_world,A) ),
inference(copy,[status(thm)],[c_654]) ).
cnf(c_27,plain,
( ~ q(B)
| ~ reachable(sK0(A),B)
| ~ reachable(initial_world,A) ),
inference(resolve,[status(thm)],[c_4,c_655]) ).
cnf(c_30,plain,
( reachable(sK0(initial_world),sK3(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_7,c_4]) ).
cnf(c_31,plain,
( q(sK3(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_8,c_4]) ).
cnf(c_32,plain,
( reachable(sK0(initial_world),sK3(initial_world))
| p(sK2(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_9,c_4]) ).
cnf(c_33,plain,
( q(sK3(initial_world))
| p(sK2(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_10,c_4]) ).
cnf(c_34,plain,
( reachable(sK0(initial_world),sK3(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| reachable(sK1(initial_world),sK4(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_11,c_4]) ).
cnf(c_35,plain,
( q(sK3(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| reachable(sK1(initial_world),sK4(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_12,c_4]) ).
cnf(c_36,plain,
( reachable(sK0(initial_world),sK3(initial_world))
| p(sK2(initial_world))
| reachable(sK1(initial_world),sK4(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_13,c_4]) ).
cnf(c_37,plain,
( q(sK3(initial_world))
| p(sK2(initial_world))
| reachable(sK1(initial_world),sK4(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_14,c_4]) ).
cnf(c_38,plain,
( reachable(sK0(initial_world),sK3(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| q(sK4(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_15,c_4]) ).
cnf(c_39,plain,
( q(sK3(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| q(sK4(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_16,c_4]) ).
cnf(c_40,plain,
( reachable(sK0(initial_world),sK3(initial_world))
| p(sK2(initial_world))
| q(sK4(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_17,c_4]) ).
cnf(c_41,plain,
( q(sK3(initial_world))
| p(sK2(initial_world))
| q(sK4(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_18,c_4]) ).
cnf(c_656,plain,
( ~ p(sK2(initial_world))
| ~ reachable(initial_world,initial_world)
| reachable(sK0(initial_world),sK3(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_30,c_23]) ).
cnf(c_67,plain,
( ~ p(sK2(initial_world))
| reachable(sK0(initial_world),sK3(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_4,c_656]) ).
cnf(c_657,plain,
( ~ p(sK2(initial_world))
| ~ reachable(initial_world,initial_world)
| q(sK3(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_31,c_23]) ).
cnf(c_85,plain,
( ~ p(sK2(initial_world))
| q(sK3(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_4,c_657]) ).
cnf(c_658,plain,
( ~ p(sK1(initial_world))
| ~ reachable(initial_world,initial_world)
| q(sK3(initial_world))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_33,c_23]) ).
cnf(c_97,plain,
( ~ p(sK1(initial_world))
| q(sK3(initial_world))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_4,c_658]) ).
cnf(c_659,plain,
( ~ p(sK1(initial_world))
| ~ reachable(initial_world,initial_world)
| reachable(sK0(initial_world),sK3(initial_world))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_32,c_23]) ).
cnf(c_102,plain,
( ~ p(sK1(initial_world))
| reachable(sK0(initial_world),sK3(initial_world))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_4,c_659]) ).
cnf(c_660,plain,
( ~ q(sK3(initial_world))
| ~ reachable(initial_world,initial_world)
| p(sK2(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_32,c_27]) ).
cnf(c_106,plain,
( ~ q(sK3(initial_world))
| p(sK2(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_4,c_660]) ).
cnf(c_113,plain,
( reachable(A,sK4(initial_world))
| ~ reachable(A,sK1(initial_world))
| reachable(sK0(initial_world),sK3(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_34,c_5]) ).
cnf(c_661,plain,
( ~ p(sK2(initial_world))
| ~ reachable(initial_world,initial_world)
| q(sK3(initial_world))
| reachable(sK1(initial_world),sK4(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_35,c_23]) ).
cnf(c_132,plain,
( ~ p(sK2(initial_world))
| q(sK3(initial_world))
| reachable(sK1(initial_world),sK4(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_4,c_661]) ).
cnf(c_662,plain,
( ~ q(sK3(initial_world))
| ~ reachable(initial_world,initial_world)
| p(sK2(initial_world))
| reachable(sK1(initial_world),sK4(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_36,c_27]) ).
cnf(c_177,plain,
( ~ q(sK3(initial_world))
| p(sK2(initial_world))
| reachable(sK1(initial_world),sK4(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_4,c_662]) ).
cnf(c_663,plain,
( q(sK3(initial_world))
| p(sK2(initial_world))
| q(sK3(initial_world))
| p(sK2(initial_world))
| reachable(sK1(initial_world),sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_37,c_97]) ).
cnf(c_664,plain,
( q(sK3(initial_world))
| q(sK3(initial_world))
| p(sK2(initial_world))
| reachable(sK1(initial_world),sK4(initial_world)) ),
inference(copy,[status(thm)],[c_663]) ).
cnf(c_181,plain,
( q(sK3(initial_world))
| p(sK2(initial_world))
| reachable(sK1(initial_world),sK4(initial_world)) ),
inference(copy,[status(thm)],[c_664]) ).
cnf(c_665,plain,
( ~ q(sK3(initial_world))
| ~ reachable(initial_world,initial_world)
| reachable(sK0(initial_world),sK2(initial_world))
| q(sK4(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_38,c_27]) ).
cnf(c_192,plain,
( ~ q(sK3(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| q(sK4(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_4,c_665]) ).
cnf(c_666,plain,
( q(sK3(initial_world))
| reachable(sK0(initial_world),sK1(initial_world))
| q(sK3(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_85,c_33]) ).
cnf(c_667,plain,
( q(sK3(initial_world))
| q(sK3(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(copy,[status(thm)],[c_666]) ).
cnf(c_200,plain,
( q(sK3(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(copy,[status(thm)],[c_667]) ).
cnf(c_668,plain,
( ~ p(sK1(initial_world))
| ~ reachable(initial_world,initial_world)
| q(sK3(initial_world)) ),
inference(resolve,[status(thm)],[c_200,c_23]) ).
cnf(c_203,plain,
( ~ p(sK1(initial_world))
| q(sK3(initial_world)) ),
inference(resolve,[status(thm)],[c_4,c_668]) ).
cnf(c_205,plain,
( reachable(sK0(initial_world),A)
| ~ reachable(sK1(initial_world),A)
| q(sK3(initial_world)) ),
inference(resolve,[status(thm)],[c_200,c_5]) ).
cnf(c_669,plain,
( q(sK3(initial_world))
| q(sK3(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| q(sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_39,c_203]) ).
cnf(c_223,plain,
( q(sK3(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| q(sK4(initial_world)) ),
inference(copy,[status(thm)],[c_669]) ).
cnf(c_670,plain,
( q(sK3(initial_world))
| q(sK3(initial_world))
| p(sK2(initial_world))
| q(sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_41,c_203]) ).
cnf(c_235,plain,
( q(sK3(initial_world))
| p(sK2(initial_world))
| q(sK4(initial_world)) ),
inference(copy,[status(thm)],[c_670]) ).
cnf(c_671,plain,
( reachable(sK0(initial_world),sK3(initial_world))
| p(sK2(initial_world))
| q(sK4(initial_world))
| reachable(sK0(initial_world),sK3(initial_world))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_102,c_40]) ).
cnf(c_672,plain,
( reachable(sK0(initial_world),sK3(initial_world))
| q(sK4(initial_world))
| reachable(sK0(initial_world),sK3(initial_world))
| p(sK2(initial_world)) ),
inference(copy,[status(thm)],[c_671]) ).
cnf(c_238,plain,
( q(sK4(initial_world))
| reachable(sK0(initial_world),sK3(initial_world))
| p(sK2(initial_world)) ),
inference(copy,[status(thm)],[c_672]) ).
cnf(c_673,plain,
( reachable(sK0(initial_world),sK1(initial_world))
| p(sK2(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_106,c_200]) ).
cnf(c_242,plain,
( p(sK2(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(copy,[status(thm)],[c_673]) ).
cnf(c_674,plain,
( q(sK3(initial_world))
| p(sK2(initial_world))
| reachable(sK0(initial_world),sK4(initial_world))
| q(sK3(initial_world)) ),
inference(resolve,[status(thm)],[c_205,c_181]) ).
cnf(c_312,plain,
( p(sK2(initial_world))
| reachable(sK0(initial_world),sK4(initial_world))
| q(sK3(initial_world)) ),
inference(copy,[status(thm)],[c_674]) ).
cnf(c_675,plain,
( ~ p(sK2(initial_world))
| ~ reachable(initial_world,initial_world)
| q(sK3(initial_world))
| q(sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_223,c_23]) ).
cnf(c_316,plain,
( ~ p(sK2(initial_world))
| q(sK3(initial_world))
| q(sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_4,c_675]) ).
cnf(c_676,plain,
( q(sK3(initial_world))
| q(sK4(initial_world))
| q(sK3(initial_world))
| q(sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_316,c_235]) ).
cnf(c_677,plain,
( q(sK3(initial_world))
| q(sK3(initial_world))
| q(sK4(initial_world)) ),
inference(copy,[status(thm)],[c_676]) ).
cnf(c_320,plain,
( q(sK3(initial_world))
| q(sK4(initial_world)) ),
inference(copy,[status(thm)],[c_677]) ).
cnf(c_678,plain,
( ~ q(sK3(initial_world))
| ~ reachable(initial_world,initial_world)
| q(sK4(initial_world))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_238,c_27]) ).
cnf(c_344,plain,
( ~ q(sK3(initial_world))
| q(sK4(initial_world))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_4,c_678]) ).
cnf(c_679,plain,
( q(sK4(initial_world))
| q(sK4(initial_world))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_344,c_320]) ).
cnf(c_348,plain,
( q(sK4(initial_world))
| p(sK2(initial_world)) ),
inference(copy,[status(thm)],[c_679]) ).
cnf(c_680,plain,
( ~ q(sK4(initial_world))
| ~ reachable(initial_world,initial_world)
| p(sK2(initial_world))
| q(sK3(initial_world)) ),
inference(resolve,[status(thm)],[c_312,c_27]) ).
cnf(c_388,plain,
( ~ q(sK4(initial_world))
| p(sK2(initial_world))
| q(sK3(initial_world)) ),
inference(resolve,[status(thm)],[c_4,c_680]) ).
cnf(c_681,plain,
( p(sK2(initial_world))
| p(sK2(initial_world))
| q(sK3(initial_world)) ),
inference(resolve,[status(thm)],[c_388,c_348]) ).
cnf(c_392,plain,
( p(sK2(initial_world))
| q(sK3(initial_world)) ),
inference(copy,[status(thm)],[c_681]) ).
cnf(c_682,plain,
( reachable(sK0(initial_world),sK1(initial_world))
| reachable(sK0(initial_world),sK3(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_67,c_242]) ).
cnf(c_397,plain,
( reachable(sK0(initial_world),sK3(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(copy,[status(thm)],[c_682]) ).
cnf(c_683,plain,
( ~ q(sK3(initial_world))
| ~ reachable(initial_world,initial_world)
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_397,c_27]) ).
cnf(c_404,plain,
( ~ q(sK3(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_4,c_683]) ).
cnf(c_684,plain,
( reachable(sK0(initial_world),sK3(initial_world))
| reachable(sK0(initial_world),sK4(initial_world))
| reachable(sK0(initial_world),sK3(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_113,c_397]) ).
cnf(c_410,plain,
( reachable(sK0(initial_world),sK4(initial_world))
| reachable(sK0(initial_world),sK3(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| p(sK1(initial_world)) ),
inference(copy,[status(thm)],[c_684]) ).
cnf(c_685,plain,
( reachable(sK0(initial_world),sK1(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_404,c_200]) ).
cnf(c_442,plain,
reachable(sK0(initial_world),sK1(initial_world)),
inference(copy,[status(thm)],[c_685]) ).
cnf(c_686,plain,
( ~ p(sK1(initial_world))
| ~ reachable(initial_world,initial_world) ),
inference(resolve,[status(thm)],[c_442,c_23]) ).
cnf(c_445,plain,
~ p(sK1(initial_world)),
inference(resolve,[status(thm)],[c_4,c_686]) ).
cnf(c_447,plain,
( reachable(sK0(initial_world),A)
| ~ reachable(sK1(initial_world),A) ),
inference(resolve,[status(thm)],[c_442,c_5]) ).
cnf(c_476,plain,
( reachable(sK0(initial_world),sK4(initial_world))
| reachable(sK0(initial_world),sK3(initial_world))
| reachable(sK0(initial_world),sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_445,c_410]) ).
cnf(c_484,plain,
( ~ q(sK3(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| q(sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_445,c_192]) ).
cnf(c_494,plain,
( ~ q(sK3(initial_world))
| p(sK2(initial_world))
| reachable(sK1(initial_world),sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_445,c_177]) ).
cnf(c_500,plain,
( ~ p(sK2(initial_world))
| q(sK3(initial_world))
| reachable(sK1(initial_world),sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_445,c_132]) ).
cnf(c_687,plain,
( q(sK4(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| q(sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_484,c_320]) ).
cnf(c_551,plain,
( reachable(sK0(initial_world),sK2(initial_world))
| q(sK4(initial_world)) ),
inference(copy,[status(thm)],[c_687]) ).
cnf(c_688,plain,
( ~ p(sK2(initial_world))
| ~ reachable(initial_world,initial_world)
| q(sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_551,c_23]) ).
cnf(c_554,plain,
( ~ p(sK2(initial_world))
| q(sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_4,c_688]) ).
cnf(c_689,plain,
( q(sK4(initial_world))
| q(sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_554,c_348]) ).
cnf(c_575,plain,
q(sK4(initial_world)),
inference(copy,[status(thm)],[c_689]) ).
cnf(c_690,plain,
( ~ q(A)
| ~ reachable(sK0(initial_world),A) ),
inference(resolve,[status(thm)],[c_27,c_4]) ).
cnf(c_579,plain,
~ reachable(sK0(initial_world),sK4(initial_world)),
inference(resolve,[status(thm)],[c_690,c_575]) ).
cnf(c_580,plain,
( reachable(sK0(initial_world),sK3(initial_world))
| reachable(sK0(initial_world),sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_579,c_476]) ).
cnf(c_691,plain,
( ~ p(sK2(initial_world))
| ~ reachable(initial_world,initial_world)
| reachable(sK0(initial_world),sK3(initial_world)) ),
inference(resolve,[status(thm)],[c_580,c_23]) ).
cnf(c_585,plain,
( ~ p(sK2(initial_world))
| reachable(sK0(initial_world),sK3(initial_world)) ),
inference(resolve,[status(thm)],[c_4,c_691]) ).
cnf(c_595,plain,
~ reachable(sK1(initial_world),sK4(initial_world)),
inference(resolve,[status(thm)],[c_447,c_579]) ).
cnf(c_598,plain,
( ~ p(sK2(initial_world))
| q(sK3(initial_world)) ),
inference(resolve,[status(thm)],[c_595,c_500]) ).
cnf(c_602,plain,
( ~ q(sK3(initial_world))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_595,c_494]) ).
cnf(c_692,plain,
( q(sK3(initial_world))
| q(sK3(initial_world)) ),
inference(resolve,[status(thm)],[c_598,c_392]) ).
cnf(c_644,plain,
q(sK3(initial_world)),
inference(copy,[status(thm)],[c_692]) ).
cnf(c_646,plain,
p(sK2(initial_world)),
inference(resolve,[status(thm)],[c_644,c_602]) ).
cnf(c_648,plain,
reachable(sK0(initial_world),sK3(initial_world)),
inference(resolve,[status(thm)],[c_646,c_585]) ).
cnf(c_693,plain,
( ~ q(A)
| ~ reachable(sK0(initial_world),A) ),
inference(resolve,[status(thm)],[c_27,c_4]) ).
cnf(c_694,plain,
~ reachable(sK0(initial_world),sK3(initial_world)),
inference(resolve,[status(thm)],[c_693,c_644]) ).
cnf(c_652,plain,
$false,
inference(resolve,[status(thm)],[c_648,c_694]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN549+1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n001.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sat Sep 26 18:18:43 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.35 % Process 2403618 was started by sandbox on n001,
% 0.07/0.35 % Sat Sep 26 18:18:43 2026
% 0.07/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.07/0.35
% 0.07/0.35 % From the command line: assign(max_seconds, 300).
% 0.13/0.39
% 0.13/0.39 % SZS status Theorem for theBenchmark
% 0.13/0.39
% 0.13/0.39 % Proof 1 at 0.02 (+ 0.00) seconds.
% 0.13/0.39 % Length of proof is 80.
% 0.13/0.39 % Level of proof is 20.
% 0.13/0.39 % Maximum clause weight is 31.000.
% 0.13/0.39 % Given clauses 143.
% 0.13/0.39
% 0.13/0.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------