%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN415+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 : n013.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:37:50 AM UTC 2026
% Result : Theorem 0.86s 0.58s
% Output : CNFRefutation 0.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 1
% Syntax : Number of formulae : 149 ( 13 unt; 0 def)
% Number of atoms : 482 ( 136 equ)
% Maximal formula atoms : 38 ( 3 avg)
% Number of connectives : 470 ( 137 ~; 300 |; 27 &)
% ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-1 aty)
% Number of variables : 86 ( 6 sgn 34 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(kalish317,conjecture,
( ( ! [Y,Z] :
( ( f(Z)
& f(Y) )
=> Y = Z )
& ? [X] : f(X) )
<=> ? [U] :
( ! [V] :
( f(V)
=> U = V )
& f(U) ) ),
file('theBenchmark.p',kalish317) ).
fof(kalish317_neg,negated_conjecture,
~ ( ( ! [Y,Z] :
( ( f(Z)
& f(Y) )
=> Y = Z )
& ? [X] : f(X) )
<=> ? [U] :
( ! [V] :
( f(V)
=> U = V )
& f(U) ) ),
inference(assume_negation,[status(cth)],[kalish317]) ).
fof(nnf_1,plain,
( ( ! [U] :
( ? [V] :
( V != U
& f(V) )
| ~ f(U) )
| ? [Y,Z] :
( Z != Y
& f(Z)
& f(Y) )
| ! [X] : ~ f(X) )
& ( ? [X3] :
( ! [X4] :
( X4 = X3
| ~ f(X4) )
& f(X3) )
| ( ! [X1,X2] :
( X2 = X1
| ~ f(X2)
| ~ f(X1) )
& ? [X0] : f(X0) ) ) ),
inference(fof_nnf,[status(thm)],[kalish317_neg]) ).
fof(sk_kalish317_neg_sk,plain,
( ( ! [U] :
( ( sK3(U) != U
& f(sK3(U)) )
| ~ f(U) )
| ( sK4 != sK2
& f(sK4)
& f(sK2) )
| ! [X] : ~ f(X) )
& ( ( ! [X4] :
( X4 = sK1
| ~ f(X4) )
& f(sK1) )
| ( ! [X1,X2] :
( X2 = X1
| ~ f(X2)
| ~ f(X1) )
& f(sK0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK4,sK3]),skolemize(X0,sK0),skolemize(X3,sK1),skolemize(Y,sK2),skolemize(Z,sK4),skolemize(V,sK3(U))],[nnf_1]) ).
fof(sk_kalish317_neg,plain,
( ! [VAR_0,VAR_1] :
( sK3(VAR_1) != VAR_1
| ~ f(VAR_1)
| sK4 != sK2
| ~ f(VAR_0) )
& ! [VAR_0,VAR_1] :
( f(sK3(VAR_1))
| ~ f(VAR_1)
| sK4 != sK2
| ~ f(VAR_0) )
& ! [VAR_0,VAR_1] :
( sK3(VAR_1) != VAR_1
| ~ f(VAR_1)
| f(sK4)
| ~ f(VAR_0) )
& ! [VAR_0,VAR_1] :
( f(sK3(VAR_1))
| ~ f(VAR_1)
| f(sK4)
| ~ f(VAR_0) )
& ! [VAR_0,VAR_1] :
( sK3(VAR_1) != VAR_1
| ~ f(VAR_1)
| f(sK2)
| ~ f(VAR_0) )
& ! [VAR_0,VAR_1] :
( f(sK3(VAR_1))
| ~ f(VAR_1)
| f(sK2)
| ~ f(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( VAR_2 = sK1
| ~ f(VAR_2)
| VAR_1 = VAR_0
| ~ f(VAR_1)
| ~ f(VAR_0) )
& ! [VAR_0,VAR_1] :
( f(sK1)
| VAR_1 = VAR_0
| ~ f(VAR_1)
| ~ f(VAR_0) )
& ! [VAR_0] :
( VAR_0 = sK1
| ~ f(VAR_0)
| f(sK0) )
& ( f(sK1)
| f(sK0) ) ),
inference(cnf_transformation,[status(thm)],[sk_kalish317_neg_sk]) ).
cnf(c_2,negated_conjecture,
( f(sK1)
| f(sK0) ),
inference(split_conjunct,[status(thm)],[sk_kalish317_neg]) ).
cnf(c_3,negated_conjecture,
( A = sK1
| ~ f(A)
| f(sK0) ),
inference(split_conjunct,[status(thm)],[sk_kalish317_neg]) ).
cnf(c_4,negated_conjecture,
( sK1 = A
| ~ f(A)
| f(sK0) ),
inference(copy,[status(thm)],[c_3]) ).
cnf(c_5,negated_conjecture,
( f(sK1)
| B = A
| ~ f(B)
| ~ f(A) ),
inference(split_conjunct,[status(thm)],[sk_kalish317_neg]) ).
cnf(c_6,negated_conjecture,
( C = sK1
| ~ f(C)
| B = A
| ~ f(B)
| ~ f(A) ),
inference(split_conjunct,[status(thm)],[sk_kalish317_neg]) ).
cnf(c_7,negated_conjecture,
( sK1 = C
| ~ f(C)
| B = A
| ~ f(B)
| ~ f(A) ),
inference(copy,[status(thm)],[c_6]) ).
cnf(c_8,negated_conjecture,
( f(sK3(B))
| ~ f(B)
| f(sK2)
| ~ f(A) ),
inference(split_conjunct,[status(thm)],[sk_kalish317_neg]) ).
cnf(c_9,negated_conjecture,
( sK3(B) != B
| ~ f(B)
| f(sK2)
| ~ f(A) ),
inference(split_conjunct,[status(thm)],[sk_kalish317_neg]) ).
cnf(c_10,negated_conjecture,
( f(sK3(B))
| ~ f(B)
| f(sK4)
| ~ f(A) ),
inference(split_conjunct,[status(thm)],[sk_kalish317_neg]) ).
cnf(c_11,negated_conjecture,
( sK3(B) != B
| ~ f(B)
| f(sK4)
| ~ f(A) ),
inference(split_conjunct,[status(thm)],[sk_kalish317_neg]) ).
cnf(c_12,negated_conjecture,
( f(sK3(B))
| ~ f(B)
| sK4 != sK2
| ~ f(A) ),
inference(split_conjunct,[status(thm)],[sk_kalish317_neg]) ).
cnf(c_13,negated_conjecture,
( sK3(B) != B
| ~ f(B)
| sK4 != sK2
| ~ f(A) ),
inference(split_conjunct,[status(thm)],[sk_kalish317_neg]) ).
cnf(c_800,plain,
( ~ f(A)
| sK1 = A
| ~ f(sK1)
| ~ f(A) ),
inference(factor,[status(thm)],[c_7]) ).
cnf(c_16,plain,
( sK1 = A
| ~ f(sK1)
| ~ f(A) ),
inference(copy,[status(thm)],[c_800]) ).
cnf(c_17,plain,
( f(sK3(A))
| f(sK2)
| ~ f(A) ),
inference(factor,[status(thm)],[c_8]) ).
cnf(c_18,plain,
( sK3(A) != A
| f(sK2)
| ~ f(A) ),
inference(factor,[status(thm)],[c_9]) ).
cnf(c_19,plain,
( f(sK3(A))
| f(sK4)
| ~ f(A) ),
inference(factor,[status(thm)],[c_10]) ).
cnf(c_20,plain,
( sK3(A) != A
| f(sK4)
| ~ f(A) ),
inference(factor,[status(thm)],[c_11]) ).
cnf(c_21,plain,
( f(sK3(A))
| sK4 != sK2
| ~ f(A) ),
inference(factor,[status(thm)],[c_12]) ).
cnf(c_22,plain,
( sK3(A) != A
| sK4 != sK2
| ~ f(A) ),
inference(factor,[status(thm)],[c_13]) ).
cnf(c_801,negated_conjecture,
( f(sK1)
| f(sK1)
| A = sK0
| ~ f(A) ),
inference(resolve,[status(thm)],[c_5,c_2]) ).
cnf(c_802,negated_conjecture,
( f(sK1)
| f(sK1)
| sK0 = A
| ~ f(A) ),
inference(copy,[status(thm)],[c_801]) ).
cnf(c_23,negated_conjecture,
( f(sK1)
| sK0 = A
| ~ f(A) ),
inference(copy,[status(thm)],[c_802]) ).
cnf(c_24,plain,
( f(sK0)
| f(sK3(sK1))
| f(sK2) ),
inference(resolve,[status(thm)],[c_17,c_2]) ).
cnf(c_25,plain,
( f(sK1)
| f(sK3(sK0))
| f(sK2) ),
inference(resolve,[status(thm)],[c_17,c_2]) ).
cnf(c_26,plain,
( f(sK0)
| sK3(sK1) != sK1
| f(sK2) ),
inference(resolve,[status(thm)],[c_18,c_2]) ).
cnf(c_28,plain,
( f(sK0)
| f(sK3(sK1))
| f(sK4) ),
inference(resolve,[status(thm)],[c_19,c_2]) ).
cnf(c_29,plain,
( f(sK1)
| f(sK3(sK0))
| f(sK4) ),
inference(resolve,[status(thm)],[c_19,c_2]) ).
cnf(c_30,plain,
( f(sK0)
| sK3(sK1) != sK1
| f(sK4) ),
inference(resolve,[status(thm)],[c_20,c_2]) ).
cnf(c_32,plain,
( f(sK0)
| f(sK3(sK1))
| sK4 != sK2 ),
inference(resolve,[status(thm)],[c_21,c_2]) ).
cnf(c_33,plain,
( f(sK1)
| f(sK3(sK0))
| sK4 != sK2 ),
inference(resolve,[status(thm)],[c_21,c_2]) ).
cnf(c_35,plain,
( f(sK1)
| sK3(sK0) != sK0
| sK4 != sK2 ),
inference(resolve,[status(thm)],[c_22,c_2]) ).
cnf(c_803,negated_conjecture,
( sK1 = sK2
| f(sK0)
| f(sK0)
| f(sK3(sK1)) ),
inference(resolve,[status(thm)],[c_24,c_4]) ).
cnf(c_804,negated_conjecture,
( sK2 = sK1
| f(sK0)
| f(sK0)
| f(sK3(sK1)) ),
inference(copy,[status(thm)],[c_803]) ).
cnf(c_39,negated_conjecture,
( sK2 = sK1
| f(sK0)
| f(sK3(sK1)) ),
inference(copy,[status(thm)],[c_804]) ).
cnf(c_805,negated_conjecture,
( sK1 = sK3(sK1)
| f(sK0)
| f(sK0)
| f(sK2) ),
inference(resolve,[status(thm)],[c_24,c_4]) ).
cnf(c_806,negated_conjecture,
( sK3(sK1) = sK1
| f(sK0)
| f(sK0)
| f(sK2) ),
inference(copy,[status(thm)],[c_805]) ).
cnf(c_49,negated_conjecture,
( sK3(sK1) = sK1
| f(sK0)
| f(sK2) ),
inference(copy,[status(thm)],[c_806]) ).
cnf(c_807,plain,
( f(sK1)
| sK0 = sK3(sK0)
| f(sK1)
| f(sK2) ),
inference(resolve,[status(thm)],[c_25,c_23]) ).
cnf(c_808,plain,
( f(sK1)
| sK3(sK0) = sK0
| f(sK1)
| f(sK2) ),
inference(copy,[status(thm)],[c_807]) ).
cnf(c_65,plain,
( sK3(sK0) = sK0
| f(sK1)
| f(sK2) ),
inference(copy,[status(thm)],[c_808]) ).
cnf(c_809,negated_conjecture,
( sK1 = sK3(sK1)
| f(sK0)
| f(sK0)
| f(sK4) ),
inference(resolve,[status(thm)],[c_28,c_4]) ).
cnf(c_810,negated_conjecture,
( sK3(sK1) = sK1
| f(sK0)
| f(sK0)
| f(sK4) ),
inference(copy,[status(thm)],[c_809]) ).
cnf(c_91,negated_conjecture,
( sK3(sK1) = sK1
| f(sK0)
| f(sK4) ),
inference(copy,[status(thm)],[c_810]) ).
cnf(c_811,plain,
( f(sK1)
| sK0 = sK3(sK0)
| f(sK1)
| f(sK4) ),
inference(resolve,[status(thm)],[c_29,c_23]) ).
cnf(c_812,plain,
( f(sK1)
| sK3(sK0) = sK0
| f(sK1)
| f(sK4) ),
inference(copy,[status(thm)],[c_811]) ).
cnf(c_105,plain,
( sK3(sK0) = sK0
| f(sK1)
| f(sK4) ),
inference(copy,[status(thm)],[c_812]) ).
cnf(c_813,plain,
( f(sK0)
| f(sK3(sK1))
| sK4 != sK1
| f(sK0)
| f(sK3(sK1)) ),
inference(paramod,[status(thm)],[c_39,c_32]) ).
cnf(c_814,plain,
( f(sK0)
| sK4 != sK1
| f(sK0)
| f(sK3(sK1)) ),
inference(copy,[status(thm)],[c_813]) ).
cnf(c_132,plain,
( sK4 != sK1
| f(sK0)
| f(sK3(sK1)) ),
inference(copy,[status(thm)],[c_814]) ).
cnf(c_815,plain,
( f(sK0)
| f(sK2)
| f(sK0)
| f(sK2) ),
inference(resolve,[status(thm)],[c_49,c_26]) ).
cnf(c_816,plain,
( f(sK0)
| f(sK0)
| f(sK2) ),
inference(copy,[status(thm)],[c_815]) ).
cnf(c_147,plain,
( f(sK0)
| f(sK2) ),
inference(copy,[status(thm)],[c_816]) ).
cnf(c_817,negated_conjecture,
( sK1 = sK2
| f(sK0)
| f(sK0) ),
inference(resolve,[status(thm)],[c_147,c_4]) ).
cnf(c_818,negated_conjecture,
( sK2 = sK1
| f(sK0)
| f(sK0) ),
inference(copy,[status(thm)],[c_817]) ).
cnf(c_155,negated_conjecture,
( sK2 = sK1
| f(sK0) ),
inference(copy,[status(thm)],[c_818]) ).
cnf(c_819,plain,
( sK3(sK0) != sK0
| f(sK2)
| f(sK2) ),
inference(resolve,[status(thm)],[c_147,c_18]) ).
cnf(c_160,plain,
( sK3(sK0) != sK0
| f(sK2) ),
inference(copy,[status(thm)],[c_819]) ).
cnf(c_168,plain,
( f(sK3(sK0))
| sK4 != sK2
| sK2 = sK1 ),
inference(resolve,[status(thm)],[c_155,c_21]) ).
cnf(c_820,plain,
( f(sK2)
| f(sK1)
| f(sK2) ),
inference(resolve,[status(thm)],[c_65,c_160]) ).
cnf(c_248,plain,
( f(sK1)
| f(sK2) ),
inference(copy,[status(thm)],[c_820]) ).
cnf(c_821,negated_conjecture,
( f(sK1)
| sK2 = A
| ~ f(A)
| f(sK1) ),
inference(resolve,[status(thm)],[c_248,c_5]) ).
cnf(c_257,negated_conjecture,
( sK2 = A
| ~ f(A)
| f(sK1) ),
inference(copy,[status(thm)],[c_821]) ).
cnf(c_822,plain,
( sK3(sK1) != sK1
| f(sK2)
| f(sK2) ),
inference(resolve,[status(thm)],[c_248,c_18]) ).
cnf(c_264,plain,
( sK3(sK1) != sK1
| f(sK2) ),
inference(copy,[status(thm)],[c_822]) ).
cnf(c_823,plain,
( f(sK3(sK1))
| f(sK2)
| f(sK2) ),
inference(resolve,[status(thm)],[c_248,c_17]) ).
cnf(c_265,plain,
( f(sK3(sK1))
| f(sK2) ),
inference(copy,[status(thm)],[c_823]) ).
cnf(c_266,plain,
( sK1 = A
| ~ f(A)
| f(sK2) ),
inference(resolve,[status(thm)],[c_248,c_16]) ).
cnf(c_824,plain,
( f(sK2)
| sK1 = sK3(sK1)
| f(sK2) ),
inference(resolve,[status(thm)],[c_266,c_265]) ).
cnf(c_825,plain,
( f(sK2)
| sK3(sK1) = sK1
| f(sK2) ),
inference(copy,[status(thm)],[c_824]) ).
cnf(c_319,plain,
( sK3(sK1) = sK1
| f(sK2) ),
inference(copy,[status(thm)],[c_825]) ).
cnf(c_826,plain,
( f(sK0)
| f(sK4)
| f(sK0)
| f(sK4) ),
inference(resolve,[status(thm)],[c_91,c_30]) ).
cnf(c_827,plain,
( f(sK0)
| f(sK0)
| f(sK4) ),
inference(copy,[status(thm)],[c_826]) ).
cnf(c_365,plain,
( f(sK0)
| f(sK4) ),
inference(copy,[status(thm)],[c_827]) ).
cnf(c_828,negated_conjecture,
( sK1 = sK4
| f(sK0)
| f(sK0) ),
inference(resolve,[status(thm)],[c_365,c_4]) ).
cnf(c_829,negated_conjecture,
( sK4 = sK1
| f(sK0)
| f(sK0) ),
inference(copy,[status(thm)],[c_828]) ).
cnf(c_372,negated_conjecture,
( sK4 = sK1
| f(sK0) ),
inference(copy,[status(thm)],[c_829]) ).
cnf(c_830,plain,
( f(sK2)
| f(sK2) ),
inference(resolve,[status(thm)],[c_319,c_264]) ).
cnf(c_422,plain,
f(sK2),
inference(copy,[status(thm)],[c_830]) ).
cnf(c_831,plain,
( sK1 = sK2
| ~ f(sK1) ),
inference(resolve,[status(thm)],[c_422,c_16]) ).
cnf(c_443,plain,
( sK2 = sK1
| ~ f(sK1) ),
inference(copy,[status(thm)],[c_831]) ).
cnf(c_832,plain,
( f(sK4)
| ~ f(sK0)
| f(sK1)
| f(sK4) ),
inference(resolve,[status(thm)],[c_105,c_20]) ).
cnf(c_493,plain,
( ~ f(sK0)
| f(sK1)
| f(sK4) ),
inference(copy,[status(thm)],[c_832]) ).
cnf(c_833,plain,
( f(sK4)
| f(sK1)
| f(sK4) ),
inference(resolve,[status(thm)],[c_493,c_365]) ).
cnf(c_514,plain,
( f(sK1)
| f(sK4) ),
inference(copy,[status(thm)],[c_833]) ).
cnf(c_834,plain,
( sK2 = sK4
| f(sK1)
| f(sK1) ),
inference(resolve,[status(thm)],[c_514,c_257]) ).
cnf(c_835,plain,
( sK4 = sK2
| f(sK1)
| f(sK1) ),
inference(copy,[status(thm)],[c_834]) ).
cnf(c_515,plain,
( sK4 = sK2
| f(sK1) ),
inference(copy,[status(thm)],[c_835]) ).
cnf(c_836,plain,
( f(sK1)
| sK0 = sK4
| f(sK1) ),
inference(resolve,[status(thm)],[c_514,c_23]) ).
cnf(c_837,plain,
( f(sK1)
| sK4 = sK0
| f(sK1) ),
inference(copy,[status(thm)],[c_836]) ).
cnf(c_516,plain,
( sK4 = sK0
| f(sK1) ),
inference(copy,[status(thm)],[c_837]) ).
cnf(c_838,negated_conjecture,
( f(sK1)
| sK4 = A
| ~ f(A)
| f(sK1) ),
inference(resolve,[status(thm)],[c_514,c_5]) ).
cnf(c_522,negated_conjecture,
( sK4 = A
| ~ f(A)
| f(sK1) ),
inference(copy,[status(thm)],[c_838]) ).
cnf(c_839,plain,
( sK3(sK1) != sK1
| f(sK4)
| f(sK4) ),
inference(resolve,[status(thm)],[c_514,c_20]) ).
cnf(c_527,plain,
( sK3(sK1) != sK1
| f(sK4) ),
inference(copy,[status(thm)],[c_839]) ).
cnf(c_840,plain,
( f(sK3(sK1))
| f(sK4)
| f(sK4) ),
inference(resolve,[status(thm)],[c_514,c_19]) ).
cnf(c_528,plain,
( f(sK3(sK1))
| f(sK4) ),
inference(copy,[status(thm)],[c_840]) ).
cnf(c_529,plain,
( sK1 = A
| ~ f(A)
| f(sK4) ),
inference(resolve,[status(thm)],[c_514,c_16]) ).
cnf(c_530,plain,
( sK2 = sK1
| sK4 = sK2 ),
inference(resolve,[status(thm)],[c_515,c_443]) ).
cnf(c_841,plain,
( f(sK1)
| sK3(sK0) != sK0
| f(sK1) ),
inference(resolve,[status(thm)],[c_515,c_35]) ).
cnf(c_533,plain,
( sK3(sK0) != sK0
| f(sK1) ),
inference(copy,[status(thm)],[c_841]) ).
cnf(c_842,plain,
( f(sK1)
| f(sK3(sK0))
| f(sK1) ),
inference(resolve,[status(thm)],[c_515,c_33]) ).
cnf(c_534,plain,
( f(sK3(sK0))
| f(sK1) ),
inference(copy,[status(thm)],[c_842]) ).
cnf(c_843,plain,
( f(sK0)
| f(sK0)
| f(sK3(sK1)) ),
inference(resolve,[status(thm)],[c_132,c_372]) ).
cnf(c_541,plain,
( f(sK0)
| f(sK3(sK1)) ),
inference(copy,[status(thm)],[c_843]) ).
cnf(c_844,plain,
( sK2 = sK1
| f(sK3(sK0))
| sK2 = sK1 ),
inference(resolve,[status(thm)],[c_168,c_530]) ).
cnf(c_578,plain,
( f(sK3(sK0))
| sK2 = sK1 ),
inference(copy,[status(thm)],[c_844]) ).
cnf(c_845,plain,
( f(sK4)
| sK1 = sK3(sK1)
| f(sK4) ),
inference(resolve,[status(thm)],[c_529,c_528]) ).
cnf(c_846,plain,
( f(sK4)
| sK3(sK1) = sK1
| f(sK4) ),
inference(copy,[status(thm)],[c_845]) ).
cnf(c_593,plain,
( sK3(sK1) = sK1
| f(sK4) ),
inference(copy,[status(thm)],[c_846]) ).
cnf(c_847,plain,
( sK4 = sK3(sK0)
| f(sK1)
| f(sK1) ),
inference(resolve,[status(thm)],[c_534,c_522]) ).
cnf(c_848,plain,
( sK3(sK0) = sK4
| f(sK1)
| f(sK1) ),
inference(copy,[status(thm)],[c_847]) ).
cnf(c_599,plain,
( sK3(sK0) = sK4
| f(sK1) ),
inference(copy,[status(thm)],[c_848]) ).
cnf(c_849,negated_conjecture,
( sK1 = sK3(sK1)
| f(sK0)
| f(sK0) ),
inference(resolve,[status(thm)],[c_541,c_4]) ).
cnf(c_850,negated_conjecture,
( sK3(sK1) = sK1
| f(sK0)
| f(sK0) ),
inference(copy,[status(thm)],[c_849]) ).
cnf(c_615,negated_conjecture,
( sK3(sK1) = sK1
| f(sK0) ),
inference(copy,[status(thm)],[c_850]) ).
cnf(c_688,plain,
( f(sK3(A))
| sK4 != sK1
| ~ f(A)
| f(sK3(sK0)) ),
inference(paramod,[status(thm)],[c_578,c_21]) ).
cnf(c_851,plain,
( f(sK4)
| f(sK4) ),
inference(resolve,[status(thm)],[c_593,c_527]) ).
cnf(c_704,plain,
f(sK4),
inference(copy,[status(thm)],[c_851]) ).
cnf(c_707,plain,
( sK3(sK4) != sK4
| sK4 != sK2 ),
inference(resolve,[status(thm)],[c_704,c_22]) ).
cnf(c_852,plain,
( sK1 = sK4
| ~ f(sK1) ),
inference(resolve,[status(thm)],[c_704,c_16]) ).
cnf(c_709,plain,
( sK4 = sK1
| ~ f(sK1) ),
inference(copy,[status(thm)],[c_852]) ).
cnf(c_853,plain,
( sK4 != sK0
| f(sK1)
| f(sK1) ),
inference(paramod,[status(thm)],[c_599,c_533]) ).
cnf(c_772,plain,
( sK4 != sK0
| f(sK1) ),
inference(copy,[status(thm)],[c_853]) ).
cnf(c_854,plain,
( f(sK1)
| f(sK1) ),
inference(resolve,[status(thm)],[c_772,c_516]) ).
cnf(c_775,plain,
f(sK1),
inference(copy,[status(thm)],[c_854]) ).
cnf(c_776,plain,
sK4 = sK1,
inference(resolve,[status(thm)],[c_775,c_709]) ).
cnf(c_778,plain,
sK2 = sK1,
inference(resolve,[status(thm)],[c_775,c_443]) ).
cnf(c_779,plain,
( sK1 = A
| ~ f(A) ),
inference(resolve,[status(thm)],[c_775,c_16]) ).
cnf(c_855,plain,
( sK3(sK4) != sK4
| sK1 != sK2 ),
inference(paramod,[status(thm)],[c_776,c_707]) ).
cnf(c_856,plain,
( sK3(sK4) != sK4
| sK1 != sK1 ),
inference(paramod,[status(thm)],[c_778,c_855]) ).
cnf(c_857,plain,
( sK3(sK1) != sK4
| sK1 != sK1 ),
inference(paramod,[status(thm)],[c_776,c_856]) ).
cnf(c_858,plain,
( sK3(sK1) != sK1
| sK1 != sK1 ),
inference(paramod,[status(thm)],[c_776,c_857]) ).
cnf(c_787,plain,
sK3(sK1) != sK1,
inference(copy,[status(thm)],[c_858]) ).
cnf(c_859,plain,
( f(sK3(A))
| sK1 != sK1
| ~ f(A)
| f(sK3(sK0)) ),
inference(paramod,[status(thm)],[c_776,c_688]) ).
cnf(c_790,plain,
( f(sK3(A))
| ~ f(A)
| f(sK3(sK0)) ),
inference(copy,[status(thm)],[c_859]) ).
cnf(c_795,negated_conjecture,
f(sK0),
inference(resolve,[status(thm)],[c_787,c_615]) ).
cnf(c_860,plain,
( ~ f(sK0)
| f(sK3(sK0)) ),
inference(factor,[status(thm)],[c_790]) ).
cnf(c_796,plain,
f(sK3(sK0)),
inference(resolve,[status(thm)],[c_795,c_860]) ).
cnf(c_798,plain,
sK1 = sK0,
inference(resolve,[status(thm)],[c_779,c_795]) ).
cnf(c_861,plain,
sK1 != sK3(sK1),
inference(copy,[status(thm)],[c_787]) ).
cnf(c_862,plain,
~ f(sK3(sK1)),
inference(resolve,[status(thm)],[c_779,c_861]) ).
cnf(c_863,plain,
~ f(sK3(sK0)),
inference(paramod,[status(thm)],[c_798,c_862]) ).
cnf(c_799,plain,
$false,
inference(resolve,[status(thm)],[c_796,c_863]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN415+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.10/0.36 % Computer : n013.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 17:40:51 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.36 % Process 3263175 was started by sandbox on n013,
% 0.10/0.36 % Sat Sep 26 17:40:51 2026
% 0.10/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.37
% 0.10/0.37 % From the command line: assign(max_seconds, 300).
% 0.86/0.58
% 0.86/0.58 % SZS status Theorem for theBenchmark
% 0.86/0.58
% 0.86/0.58 % Proof 1 at 0.08 (+ 0.06) seconds.
% 0.86/0.58 % Length of proof is 81.
% 0.86/0.58 % Level of proof is 18.
% 0.86/0.58 % Maximum clause weight is 15.000.
% 0.86/0.58 % Given clauses 120.
% 0.86/0.58
% 0.86/0.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------