%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN548+1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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 97.32s 13.01s
% Output : CNFRefutation 97.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 3
% Syntax : Number of formulae : 131 ( 16 unt; 0 def)
% Number of atoms : 476 ( 0 equ)
% Maximal formula atoms : 59 ( 3 avg)
% Number of connectives : 505 ( 160 ~; 296 |; 36 &)
% ( 2 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 4 avg)
% Maximal term depth : 3 ( 2 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 : 114 ( 0 sgn 46 !; 7 ?)
% 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] :
( reachable(Y,Z)
=> ( ! [V] :
( reachable(Z,V)
=> q(V) )
| p(Z) ) )
<=> ( ! [W] :
( reachable(Y,W)
=> q(W) )
| ! [W] :
( reachable(Y,W)
=> p(W) ) ) ) )
& reachable(initial_world,X) ),
file('theBenchmark.p',prove_this) ).
fof(prove_this_neg,negated_conjecture,
~ ? [X] :
( ! [Y] :
( reachable(X,Y)
=> ( ! [Z] :
( reachable(Y,Z)
=> ( ! [V] :
( reachable(Z,V)
=> q(V) )
| p(Z) ) )
<=> ( ! [W] :
( reachable(Y,W)
=> q(W) )
| ! [W] :
( reachable(Y,W)
=> p(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] :
( ( ( ( ~ 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)) ) )
& ( ! [X3] :
( q(X3)
| ~ reachable(sK0(X),X3) )
| ! [X2] :
( p(X2)
| ~ reachable(sK0(X),X2) )
| ! [X0] :
( ! [X1] :
( q(X1)
| ~ reachable(X0,X1) )
| p(X0)
| ~ reachable(sK0(X),X0) ) )
& 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(Z,sK1(X)),skolemize(V,sK4(X)),skolemize(X4,sK2(X)),skolemize(W,sK3(X))],[nnf_3]) ).
fof(sk_prove_this_neg,plain,
( ! [VAR_0] :
( ~ q(sK3(VAR_0))
| ~ q(sK4(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( reachable(sK0(VAR_0),sK3(VAR_0))
| ~ q(sK4(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( ~ p(sK2(VAR_0))
| ~ q(sK4(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( reachable(sK0(VAR_0),sK2(VAR_0))
| ~ q(sK4(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( ~ q(sK3(VAR_0))
| reachable(sK1(VAR_0),sK4(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( reachable(sK0(VAR_0),sK3(VAR_0))
| reachable(sK1(VAR_0),sK4(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( ~ p(sK2(VAR_0))
| reachable(sK1(VAR_0),sK4(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( reachable(sK0(VAR_0),sK2(VAR_0))
| reachable(sK1(VAR_0),sK4(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( ~ q(sK3(VAR_0))
| ~ p(sK1(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( reachable(sK0(VAR_0),sK3(VAR_0))
| ~ p(sK1(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( ~ p(sK2(VAR_0))
| ~ p(sK1(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( reachable(sK0(VAR_0),sK2(VAR_0))
| ~ p(sK1(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( ~ q(sK3(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),sK1(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( ~ p(sK2(VAR_0))
| reachable(sK0(VAR_0),sK1(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0] :
( reachable(sK0(VAR_0),sK2(VAR_0))
| reachable(sK0(VAR_0),sK1(VAR_0))
| ~ reachable(initial_world,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( q(VAR_4)
| ~ reachable(sK0(VAR_0),VAR_4)
| p(VAR_3)
| ~ reachable(sK0(VAR_0),VAR_3)
| q(VAR_2)
| ~ reachable(VAR_1,VAR_2)
| p(VAR_1)
| ~ reachable(sK0(VAR_0),VAR_1)
| ~ 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_6,negated_conjecture,
( reachable(A,sK0(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_7,negated_conjecture,
( q(E)
| ~ reachable(sK0(A),E)
| p(D)
| ~ reachable(sK0(A),D)
| q(C)
| ~ reachable(B,C)
| p(B)
| ~ reachable(sK0(A),B)
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_8,negated_conjecture,
( 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,
( ~ 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,
( reachable(sK0(A),sK3(A))
| reachable(sK0(A),sK1(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_11,negated_conjecture,
( ~ q(sK3(A))
| reachable(sK0(A),sK1(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_12,negated_conjecture,
( reachable(sK0(A),sK2(A))
| ~ p(sK1(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_13,negated_conjecture,
( ~ p(sK2(A))
| ~ p(sK1(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_16,negated_conjecture,
( reachable(sK0(A),sK2(A))
| reachable(sK1(A),sK4(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_17,negated_conjecture,
( ~ p(sK2(A))
| reachable(sK1(A),sK4(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_18,negated_conjecture,
( reachable(sK0(A),sK3(A))
| reachable(sK1(A),sK4(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_19,negated_conjecture,
( ~ q(sK3(A))
| reachable(sK1(A),sK4(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_20,negated_conjecture,
( reachable(sK0(A),sK2(A))
| ~ q(sK4(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_21,negated_conjecture,
( ~ p(sK2(A))
| ~ q(sK4(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_22,negated_conjecture,
( reachable(sK0(A),sK3(A))
| ~ q(sK4(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_23,negated_conjecture,
( ~ q(sK3(A))
| ~ q(sK4(A))
| ~ reachable(initial_world,A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_9535,plain,
( q(D)
| ~ reachable(sK0(A),D)
| p(B)
| q(C)
| ~ reachable(B,C)
| p(B)
| ~ reachable(sK0(A),B)
| ~ reachable(initial_world,A) ),
inference(factor,[status(thm)],[c_7]) ).
cnf(c_26,plain,
( q(D)
| ~ reachable(sK0(A),D)
| q(C)
| ~ reachable(B,C)
| p(B)
| ~ reachable(sK0(A),B)
| ~ reachable(initial_world,A) ),
inference(copy,[status(thm)],[c_9535]) ).
cnf(c_36,plain,
( ~ reachable(sK0(A),C)
| q(C)
| ~ reachable(B,C)
| p(B)
| ~ reachable(sK0(A),B)
| ~ reachable(initial_world,A) ),
inference(factor,[status(thm)],[c_26]) ).
cnf(c_44,plain,
reachable(initial_world,sK0(initial_world)),
inference(resolve,[status(thm)],[c_6,c_4]) ).
cnf(c_45,plain,
( reachable(sK0(initial_world),sK2(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_8,c_4]) ).
cnf(c_46,plain,
( ~ p(sK2(initial_world))
| reachable(sK0(initial_world),sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_9,c_4]) ).
cnf(c_49,plain,
( reachable(sK0(initial_world),sK2(initial_world))
| ~ p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_12,c_4]) ).
cnf(c_50,plain,
( ~ p(sK2(initial_world))
| ~ p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_13,c_4]) ).
cnf(c_53,plain,
( reachable(sK0(initial_world),sK2(initial_world))
| reachable(sK1(initial_world),sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_16,c_4]) ).
cnf(c_54,plain,
( ~ p(sK2(initial_world))
| reachable(sK1(initial_world),sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_17,c_4]) ).
cnf(c_57,plain,
( reachable(sK0(initial_world),sK2(initial_world))
| ~ q(sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_20,c_4]) ).
cnf(c_58,plain,
( ~ p(sK2(initial_world))
| ~ q(sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_21,c_4]) ).
cnf(c_86,plain,
( reachable(initial_world,A)
| ~ reachable(sK0(initial_world),A) ),
inference(resolve,[status(thm)],[c_44,c_5]) ).
cnf(c_9536,plain,
( reachable(sK0(initial_world),sK2(initial_world))
| reachable(sK0(initial_world),A)
| ~ reachable(sK1(initial_world),A) ),
inference(resolve,[status(thm)],[c_5,c_45]) ).
cnf(c_9537,plain,
( reachable(sK0(initial_world),sK2(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| reachable(sK0(initial_world),sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_9536,c_53]) ).
cnf(c_374,plain,
( reachable(sK0(initial_world),sK2(initial_world))
| reachable(sK0(initial_world),sK4(initial_world)) ),
inference(copy,[status(thm)],[c_9537]) ).
cnf(c_9538,plain,
( ~ reachable(sK0(initial_world),B)
| q(B)
| ~ reachable(A,B)
| p(A)
| ~ reachable(sK0(initial_world),A) ),
inference(resolve,[status(thm)],[c_36,c_4]) ).
cnf(c_9539,plain,
( reachable(sK0(initial_world),sK2(initial_world))
| ~ reachable(sK0(initial_world),A)
| q(A)
| ~ reachable(sK1(initial_world),A)
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_9538,c_45]) ).
cnf(c_9540,plain,
( reachable(sK0(initial_world),sK2(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| ~ reachable(sK0(initial_world),sK4(initial_world))
| q(sK4(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_9539,c_53]) ).
cnf(c_9541,plain,
( reachable(sK0(initial_world),sK2(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| q(sK4(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_9540,c_374]) ).
cnf(c_9542,plain,
( reachable(sK0(initial_world),sK2(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| q(sK4(initial_world))
| p(sK1(initial_world)) ),
inference(copy,[status(thm)],[c_9541]) ).
cnf(c_951,plain,
( reachable(sK0(initial_world),sK2(initial_world))
| q(sK4(initial_world))
| p(sK1(initial_world)) ),
inference(copy,[status(thm)],[c_9542]) ).
cnf(c_9543,plain,
( reachable(sK0(initial_world),sK2(initial_world))
| reachable(sK0(initial_world),sK2(initial_world))
| q(sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_951,c_49]) ).
cnf(c_1937,plain,
( reachable(sK0(initial_world),sK2(initial_world))
| q(sK4(initial_world)) ),
inference(copy,[status(thm)],[c_9543]) ).
cnf(c_9544,plain,
( reachable(sK0(initial_world),sK2(initial_world))
| reachable(sK0(initial_world),sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_1937,c_57]) ).
cnf(c_1953,plain,
reachable(sK0(initial_world),sK2(initial_world)),
inference(copy,[status(thm)],[c_9544]) ).
cnf(c_1968,plain,
reachable(initial_world,sK2(initial_world)),
inference(resolve,[status(thm)],[c_1953,c_86]) ).
cnf(c_9545,plain,
( q(B)
| ~ reachable(sK0(initial_world),B)
| q(A)
| ~ reachable(sK2(initial_world),A)
| p(sK2(initial_world))
| ~ reachable(initial_world,initial_world) ),
inference(resolve,[status(thm)],[c_1953,c_26]) ).
cnf(c_1975,plain,
( q(B)
| ~ reachable(sK0(initial_world),B)
| q(A)
| ~ reachable(sK2(initial_world),A)
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_4,c_9545]) ).
cnf(c_1977,plain,
( reachable(sK0(initial_world),A)
| ~ reachable(sK2(initial_world),A) ),
inference(resolve,[status(thm)],[c_1953,c_5]) ).
cnf(c_1982,plain,
( ~ q(sK3(sK2(initial_world)))
| ~ q(sK4(sK2(initial_world))) ),
inference(resolve,[status(thm)],[c_1968,c_23]) ).
cnf(c_1983,plain,
( reachable(sK0(sK2(initial_world)),sK3(sK2(initial_world)))
| ~ q(sK4(sK2(initial_world))) ),
inference(resolve,[status(thm)],[c_1968,c_22]) ).
cnf(c_1986,plain,
( ~ q(sK3(sK2(initial_world)))
| reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world))) ),
inference(resolve,[status(thm)],[c_1968,c_19]) ).
cnf(c_1987,plain,
( reachable(sK0(sK2(initial_world)),sK3(sK2(initial_world)))
| reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world))) ),
inference(resolve,[status(thm)],[c_1968,c_18]) ).
cnf(c_1994,plain,
( ~ q(sK3(sK2(initial_world)))
| reachable(sK0(sK2(initial_world)),sK1(sK2(initial_world))) ),
inference(resolve,[status(thm)],[c_1968,c_11]) ).
cnf(c_1995,plain,
( reachable(sK0(sK2(initial_world)),sK3(sK2(initial_world)))
| reachable(sK0(sK2(initial_world)),sK1(sK2(initial_world))) ),
inference(resolve,[status(thm)],[c_1968,c_10]) ).
cnf(c_1998,plain,
reachable(sK2(initial_world),sK0(sK2(initial_world))),
inference(resolve,[status(thm)],[c_1968,c_6]) ).
cnf(c_2121,plain,
reachable(sK0(initial_world),sK0(sK2(initial_world))),
inference(resolve,[status(thm)],[c_1998,c_1977]) ).
cnf(c_2127,plain,
( reachable(sK2(initial_world),A)
| ~ reachable(sK0(sK2(initial_world)),A) ),
inference(resolve,[status(thm)],[c_1998,c_5]) ).
cnf(c_2190,plain,
( reachable(sK0(initial_world),A)
| ~ reachable(sK0(sK2(initial_world)),A) ),
inference(resolve,[status(thm)],[c_2121,c_5]) ).
cnf(c_2475,plain,
( reachable(sK0(initial_world),sK3(sK2(initial_world)))
| reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world))) ),
inference(resolve,[status(thm)],[c_1987,c_2190]) ).
cnf(c_2477,plain,
( reachable(sK2(initial_world),sK3(sK2(initial_world)))
| reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world))) ),
inference(resolve,[status(thm)],[c_1987,c_2127]) ).
cnf(c_9546,plain,
( reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| q(A)
| ~ reachable(sK0(initial_world),A)
| q(sK3(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_1975,c_2477]) ).
cnf(c_9547,plain,
( reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| q(sK3(sK2(initial_world)))
| q(sK3(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_9546,c_2475]) ).
cnf(c_9548,plain,
( reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| q(sK3(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(copy,[status(thm)],[c_9547]) ).
cnf(c_2561,plain,
( reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| q(sK3(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(copy,[status(thm)],[c_9548]) ).
cnf(c_2580,plain,
( reachable(sK0(initial_world),sK3(sK2(initial_world)))
| reachable(sK0(sK2(initial_world)),sK1(sK2(initial_world))) ),
inference(resolve,[status(thm)],[c_1995,c_2190]) ).
cnf(c_2582,plain,
( reachable(sK2(initial_world),sK3(sK2(initial_world)))
| reachable(sK0(sK2(initial_world)),sK1(sK2(initial_world))) ),
inference(resolve,[status(thm)],[c_1995,c_2127]) ).
cnf(c_9549,plain,
( reachable(sK0(sK2(initial_world)),sK1(sK2(initial_world)))
| q(A)
| ~ reachable(sK0(initial_world),A)
| q(sK3(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_1975,c_2582]) ).
cnf(c_9550,plain,
( reachable(sK0(sK2(initial_world)),sK1(sK2(initial_world)))
| reachable(sK0(sK2(initial_world)),sK1(sK2(initial_world)))
| q(sK3(sK2(initial_world)))
| q(sK3(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_9549,c_2580]) ).
cnf(c_9551,plain,
( reachable(sK0(sK2(initial_world)),sK1(sK2(initial_world)))
| reachable(sK0(sK2(initial_world)),sK1(sK2(initial_world)))
| q(sK3(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(copy,[status(thm)],[c_9550]) ).
cnf(c_3706,plain,
( reachable(sK0(sK2(initial_world)),sK1(sK2(initial_world)))
| q(sK3(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(copy,[status(thm)],[c_9551]) ).
cnf(c_9552,plain,
( reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_2561,c_1986]) ).
cnf(c_6522,plain,
( reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(copy,[status(thm)],[c_9552]) ).
cnf(c_6525,plain,
( reachable(sK1(initial_world),sK4(initial_world))
| reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world))) ),
inference(resolve,[status(thm)],[c_6522,c_54]) ).
cnf(c_6526,plain,
( ~ p(sK1(initial_world))
| reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world))) ),
inference(resolve,[status(thm)],[c_6522,c_50]) ).
cnf(c_6527,plain,
( reachable(sK0(initial_world),sK1(initial_world))
| reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world))) ),
inference(resolve,[status(thm)],[c_6522,c_46]) ).
cnf(c_9553,plain,
( reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| reachable(sK0(initial_world),A)
| ~ reachable(sK1(initial_world),A) ),
inference(resolve,[status(thm)],[c_5,c_6527]) ).
cnf(c_9554,plain,
( reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| reachable(sK0(initial_world),sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_9553,c_6525]) ).
cnf(c_6605,plain,
( reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| reachable(sK0(initial_world),sK4(initial_world)) ),
inference(copy,[status(thm)],[c_9554]) ).
cnf(c_9555,plain,
( ~ reachable(sK0(initial_world),B)
| q(B)
| ~ reachable(A,B)
| p(A)
| ~ reachable(sK0(initial_world),A) ),
inference(resolve,[status(thm)],[c_36,c_4]) ).
cnf(c_9556,plain,
( reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| ~ reachable(sK0(initial_world),A)
| q(A)
| ~ reachable(sK1(initial_world),A)
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_9555,c_6527]) ).
cnf(c_9557,plain,
( reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| ~ reachable(sK0(initial_world),sK4(initial_world))
| q(sK4(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_9556,c_6525]) ).
cnf(c_9558,plain,
( reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| q(sK4(initial_world))
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_9557,c_6605]) ).
cnf(c_9559,plain,
( reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| q(sK4(initial_world))
| p(sK1(initial_world)) ),
inference(copy,[status(thm)],[c_9558]) ).
cnf(c_6719,plain,
( reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| q(sK4(initial_world))
| p(sK1(initial_world)) ),
inference(copy,[status(thm)],[c_9559]) ).
cnf(c_9560,plain,
( reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| q(sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_6719,c_6526]) ).
cnf(c_6948,plain,
( reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| q(sK4(initial_world)) ),
inference(copy,[status(thm)],[c_9560]) ).
cnf(c_9561,plain,
( reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| ~ p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_58,c_6948]) ).
cnf(c_9562,plain,
( reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world)))
| reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world))) ),
inference(resolve,[status(thm)],[c_9561,c_6522]) ).
cnf(c_6969,plain,
reachable(sK1(sK2(initial_world)),sK4(sK2(initial_world))),
inference(copy,[status(thm)],[c_9562]) ).
cnf(c_6977,plain,
( reachable(A,sK4(sK2(initial_world)))
| ~ reachable(A,sK1(sK2(initial_world))) ),
inference(resolve,[status(thm)],[c_6969,c_5]) ).
cnf(c_9563,plain,
( reachable(sK0(sK2(initial_world)),sK1(sK2(initial_world)))
| reachable(sK0(sK2(initial_world)),sK1(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_3706,c_1994]) ).
cnf(c_7995,plain,
( reachable(sK0(sK2(initial_world)),sK1(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(copy,[status(thm)],[c_9563]) ).
cnf(c_8008,plain,
( reachable(sK0(initial_world),sK1(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_7995,c_2190]) ).
cnf(c_8011,plain,
( reachable(sK2(initial_world),sK1(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_7995,c_2127]) ).
cnf(c_8086,plain,
( reachable(sK0(initial_world),sK4(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_8008,c_6977]) ).
cnf(c_8124,plain,
( reachable(sK2(initial_world),sK4(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_8011,c_6977]) ).
cnf(c_9564,plain,
( p(sK2(initial_world))
| q(A)
| ~ reachable(sK0(initial_world),A)
| q(sK4(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_1975,c_8124]) ).
cnf(c_9565,plain,
( p(sK2(initial_world))
| p(sK2(initial_world))
| q(sK4(sK2(initial_world)))
| q(sK4(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_9564,c_8086]) ).
cnf(c_9566,plain,
( p(sK2(initial_world))
| p(sK2(initial_world))
| q(sK4(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(copy,[status(thm)],[c_9565]) ).
cnf(c_9567,plain,
( p(sK2(initial_world))
| q(sK4(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(copy,[status(thm)],[c_9566]) ).
cnf(c_8174,plain,
( q(sK4(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(copy,[status(thm)],[c_9567]) ).
cnf(c_8179,plain,
( reachable(sK0(sK2(initial_world)),sK3(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_8174,c_1983]) ).
cnf(c_8954,plain,
( reachable(sK0(initial_world),sK3(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_8179,c_2190]) ).
cnf(c_8957,plain,
( reachable(sK2(initial_world),sK3(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_8179,c_2127]) ).
cnf(c_9568,plain,
( p(sK2(initial_world))
| q(A)
| ~ reachable(sK0(initial_world),A)
| q(sK3(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_1975,c_8957]) ).
cnf(c_9569,plain,
( p(sK2(initial_world))
| p(sK2(initial_world))
| q(sK3(sK2(initial_world)))
| q(sK3(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_9568,c_8954]) ).
cnf(c_9570,plain,
( p(sK2(initial_world))
| p(sK2(initial_world))
| q(sK3(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(copy,[status(thm)],[c_9569]) ).
cnf(c_9571,plain,
( p(sK2(initial_world))
| q(sK3(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(copy,[status(thm)],[c_9570]) ).
cnf(c_9139,plain,
( q(sK3(sK2(initial_world)))
| p(sK2(initial_world)) ),
inference(copy,[status(thm)],[c_9571]) ).
cnf(c_9572,plain,
( p(sK2(initial_world))
| ~ q(sK3(sK2(initial_world))) ),
inference(resolve,[status(thm)],[c_1982,c_8174]) ).
cnf(c_9573,plain,
( p(sK2(initial_world))
| p(sK2(initial_world)) ),
inference(resolve,[status(thm)],[c_9572,c_9139]) ).
cnf(c_9150,plain,
p(sK2(initial_world)),
inference(copy,[status(thm)],[c_9573]) ).
cnf(c_9151,plain,
~ q(sK4(initial_world)),
inference(resolve,[status(thm)],[c_9150,c_58]) ).
cnf(c_9152,plain,
reachable(sK1(initial_world),sK4(initial_world)),
inference(resolve,[status(thm)],[c_9150,c_54]) ).
cnf(c_9153,plain,
~ p(sK1(initial_world)),
inference(resolve,[status(thm)],[c_9150,c_50]) ).
cnf(c_9154,plain,
reachable(sK0(initial_world),sK1(initial_world)),
inference(resolve,[status(thm)],[c_9150,c_46]) ).
cnf(c_9574,plain,
( reachable(sK0(initial_world),A)
| ~ reachable(sK1(initial_world),A) ),
inference(resolve,[status(thm)],[c_5,c_9154]) ).
cnf(c_9533,plain,
reachable(sK0(initial_world),sK4(initial_world)),
inference(resolve,[status(thm)],[c_9574,c_9152]) ).
cnf(c_9575,plain,
( ~ reachable(sK0(initial_world),B)
| q(B)
| ~ reachable(A,B)
| p(A)
| ~ reachable(sK0(initial_world),A) ),
inference(resolve,[status(thm)],[c_36,c_4]) ).
cnf(c_9576,plain,
( ~ reachable(sK0(initial_world),A)
| q(A)
| ~ reachable(sK1(initial_world),A)
| p(sK1(initial_world)) ),
inference(resolve,[status(thm)],[c_9575,c_9154]) ).
cnf(c_9577,plain,
( ~ reachable(sK0(initial_world),A)
| q(A)
| ~ reachable(sK1(initial_world),A) ),
inference(resolve,[status(thm)],[c_9576,c_9153]) ).
cnf(c_9578,plain,
( ~ reachable(sK0(initial_world),sK4(initial_world))
| q(sK4(initial_world)) ),
inference(resolve,[status(thm)],[c_9577,c_9152]) ).
cnf(c_9579,plain,
~ reachable(sK0(initial_world),sK4(initial_world)),
inference(resolve,[status(thm)],[c_9578,c_9151]) ).
cnf(c_9534,plain,
$false,
inference(resolve,[status(thm)],[c_9533,c_9579]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN548+1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n026.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 18:15:55 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 1648766 was started by sandbox2 on n026,
% 0.10/0.37 % Sat Sep 26 18:15:55 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.37
% 0.10/0.37 % From the command line: assign(max_seconds, 300).
% 97.32/13.01
% 97.32/13.01 % given #500 (T,wt=28): 4019 q(f5(f4(initial_world))) | reachable(f1(initial_world),f3(f4(initial_world))) | -p(f2(initial_world)). [resolve(3495,a,50,b)].
% 97.32/13.01
% 97.32/13.01 % SZS status Theorem for theBenchmark
% 97.32/13.01
% 97.32/13.01 % Proof 1 at 3.54 (+ 1.02) seconds.
% 97.32/13.01 % Length of proof is 82.
% 97.32/13.01 % Level of proof is 28.
% 97.32/13.01 % Maximum clause weight is 36.000.
% 97.32/13.01 % Given clauses 818.
% 97.32/13.01
% 97.32/13.01 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------