%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN551+3 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:49 AM UTC 2026
% Result : Theorem 0.13s 0.45s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 89
% Number of leaves : 1
% Syntax : Number of formulae : 149 ( 12 unt; 0 def)
% Number of atoms : 477 ( 476 equ)
% Maximal formula atoms : 28 ( 3 avg)
% Number of connectives : 484 ( 156 ~; 301 |; 21 &)
% ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 2 con; 0-1 aty)
% Number of variables : 72 ( 0 sgn 24 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(prove_this_cute_thing,conjecture,
( ? [X] :
( ! [Y] :
( Y = f(g(Y))
=> Y = X )
& X = f(g(X)) )
<=> ? [X] :
( ! [Y] :
( Y = g(f(Y))
=> Y = X )
& X = g(f(X)) ) ),
file('theBenchmark.p',prove_this_cute_thing) ).
fof(prove_this_cute_thing_neg,negated_conjecture,
~ ( ? [X] :
( ! [Y] :
( Y = f(g(Y))
=> Y = X )
& X = f(g(X)) )
<=> ? [X] :
( ! [Y] :
( Y = g(f(Y))
=> Y = X )
& X = g(f(X)) ) ),
inference(assume_negation,[status(cth)],[prove_this_cute_thing]) ).
fof(nnf_1,plain,
( ( ! [X] :
( ? [Y] :
( Y != X
& g(f(Y)) = Y )
| g(f(X)) != X )
| ! [X4] :
( ? [X5] :
( X5 != X4
& f(g(X5)) = X5 )
| f(g(X4)) != X4 ) )
& ( ? [X2] :
( ! [X3] :
( X3 = X2
| g(f(X3)) != X3 )
& g(f(X2)) = X2 )
| ? [X0] :
( ! [X1] :
( X1 = X0
| f(g(X1)) != X1 )
& f(g(X0)) = X0 ) ) ),
inference(fof_nnf,[status(thm)],[prove_this_cute_thing_neg]) ).
fof(sk_prove_this_cute_thing_neg_sk,plain,
( ( ! [X] :
( ( sK3(X) != X
& g(f(sK3(X))) = sK3(X) )
| g(f(X)) != X )
| ! [X4] :
( ( sK2(X4) != X4
& f(g(sK2(X4))) = sK2(X4) )
| f(g(X4)) != X4 ) )
& ( ( ! [X3] :
( X3 = sK1
| g(f(X3)) != X3 )
& g(f(sK1)) = sK1 )
| ( ! [X1] :
( X1 = sK0
| f(g(X1)) != X1 )
& f(g(sK0)) = sK0 ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X0,sK0),skolemize(X2,sK1),skolemize(X5,sK2(X4)),skolemize(Y,sK3(X))],[nnf_1]) ).
fof(sk_prove_this_cute_thing_neg,plain,
( ! [VAR_0,VAR_1] :
( sK3(VAR_1) != VAR_1
| g(f(VAR_1)) != VAR_1
| sK2(VAR_0) != VAR_0
| f(g(VAR_0)) != VAR_0 )
& ! [VAR_0,VAR_1] :
( g(f(sK3(VAR_1))) = sK3(VAR_1)
| g(f(VAR_1)) != VAR_1
| sK2(VAR_0) != VAR_0
| f(g(VAR_0)) != VAR_0 )
& ! [VAR_0,VAR_1] :
( sK3(VAR_1) != VAR_1
| g(f(VAR_1)) != VAR_1
| f(g(sK2(VAR_0))) = sK2(VAR_0)
| f(g(VAR_0)) != VAR_0 )
& ! [VAR_0,VAR_1] :
( g(f(sK3(VAR_1))) = sK3(VAR_1)
| g(f(VAR_1)) != VAR_1
| f(g(sK2(VAR_0))) = sK2(VAR_0)
| f(g(VAR_0)) != VAR_0 )
& ! [VAR_0,VAR_1] :
( VAR_1 = sK1
| g(f(VAR_1)) != VAR_1
| VAR_0 = sK0
| f(g(VAR_0)) != VAR_0 )
& ! [VAR_0] :
( g(f(sK1)) = sK1
| VAR_0 = sK0
| f(g(VAR_0)) != VAR_0 )
& ! [VAR_0] :
( VAR_0 = sK1
| g(f(VAR_0)) != VAR_0
| f(g(sK0)) = sK0 )
& ( g(f(sK1)) = sK1
| f(g(sK0)) = sK0 ) ),
inference(cnf_transformation,[status(thm)],[sk_prove_this_cute_thing_neg_sk]) ).
cnf(c_2,negated_conjecture,
( g(f(sK1)) = sK1
| f(g(sK0)) = sK0 ),
inference(split_conjunct,[status(thm)],[sk_prove_this_cute_thing_neg]) ).
cnf(c_3,negated_conjecture,
( A = sK1
| g(f(A)) != A
| f(g(sK0)) = sK0 ),
inference(split_conjunct,[status(thm)],[sk_prove_this_cute_thing_neg]) ).
cnf(c_4,negated_conjecture,
( sK1 = A
| g(f(A)) != A
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_3]) ).
cnf(c_7,negated_conjecture,
( B = sK1
| g(f(B)) != B
| A = sK0
| f(g(A)) != A ),
inference(split_conjunct,[status(thm)],[sk_prove_this_cute_thing_neg]) ).
cnf(c_180,negated_conjecture,
( B = sK1
| g(f(B)) != B
| sK0 = A
| f(g(A)) != A ),
inference(copy,[status(thm)],[c_7]) ).
cnf(c_8,negated_conjecture,
( sK1 = B
| g(f(B)) != B
| sK0 = A
| f(g(A)) != A ),
inference(copy,[status(thm)],[c_180]) ).
cnf(c_9,negated_conjecture,
( g(f(sK3(B))) = sK3(B)
| g(f(B)) != B
| f(g(sK2(A))) = sK2(A)
| f(g(A)) != A ),
inference(split_conjunct,[status(thm)],[sk_prove_this_cute_thing_neg]) ).
cnf(c_10,negated_conjecture,
( sK3(B) != B
| g(f(B)) != B
| f(g(sK2(A))) = sK2(A)
| f(g(A)) != A ),
inference(split_conjunct,[status(thm)],[sk_prove_this_cute_thing_neg]) ).
cnf(c_11,negated_conjecture,
( g(f(sK3(B))) = sK3(B)
| g(f(B)) != B
| sK2(A) != A
| f(g(A)) != A ),
inference(split_conjunct,[status(thm)],[sk_prove_this_cute_thing_neg]) ).
cnf(c_12,negated_conjecture,
( sK3(B) != B
| g(f(B)) != B
| sK2(A) != A
| f(g(A)) != A ),
inference(split_conjunct,[status(thm)],[sk_prove_this_cute_thing_neg]) ).
cnf(c_13,plain,
( f(g(sK0)) = sK0
| g(f(sK3(sK1))) = sK3(sK1)
| f(g(sK2(A))) = sK2(A)
| f(g(A)) != A ),
inference(resolve,[status(thm)],[c_9,c_2]) ).
cnf(c_15,plain,
( f(g(sK0)) = sK0
| sK3(sK1) != sK1
| f(g(sK2(A))) = sK2(A)
| f(g(A)) != A ),
inference(resolve,[status(thm)],[c_10,c_2]) ).
cnf(c_17,plain,
( f(g(sK0)) = sK0
| g(f(sK3(sK1))) = sK3(sK1)
| sK2(A) != A
| f(g(A)) != A ),
inference(resolve,[status(thm)],[c_11,c_2]) ).
cnf(c_19,plain,
( f(g(sK0)) = sK0
| sK3(sK1) != sK1
| sK2(A) != A
| f(g(A)) != A ),
inference(resolve,[status(thm)],[c_12,c_2]) ).
cnf(c_181,plain,
( f(g(sK0)) = sK0
| g(f(sK3(sK1))) = sK3(sK1)
| f(g(sK2(f(sK1)))) = sK2(f(sK1))
| f(sK1) != f(sK1)
| f(g(sK0)) = sK0 ),
inference(paramod,[status(thm)],[c_2,c_13]) ).
cnf(c_182,plain,
( f(g(sK0)) = sK0
| g(f(sK3(sK1))) = sK3(sK1)
| f(g(sK2(f(sK1)))) = sK2(f(sK1))
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_181]) ).
cnf(c_21,plain,
( g(f(sK3(sK1))) = sK3(sK1)
| f(g(sK2(f(sK1)))) = sK2(f(sK1))
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_182]) ).
cnf(c_183,plain,
( f(g(sK0)) = sK0
| sK3(sK1) != sK1
| f(g(sK2(f(sK1)))) = sK2(f(sK1))
| f(sK1) != f(sK1)
| f(g(sK0)) = sK0 ),
inference(paramod,[status(thm)],[c_2,c_15]) ).
cnf(c_184,plain,
( f(g(sK0)) = sK0
| sK3(sK1) != sK1
| f(g(sK2(f(sK1)))) = sK2(f(sK1))
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_183]) ).
cnf(c_22,plain,
( sK3(sK1) != sK1
| f(g(sK2(f(sK1)))) = sK2(f(sK1))
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_184]) ).
cnf(c_185,plain,
( f(g(sK0)) = sK0
| sK3(sK1) != sK1
| sK2(f(sK1)) != f(sK1)
| f(sK1) != f(sK1)
| f(g(sK0)) = sK0 ),
inference(paramod,[status(thm)],[c_2,c_19]) ).
cnf(c_186,plain,
( f(g(sK0)) = sK0
| sK3(sK1) != sK1
| sK2(f(sK1)) != f(sK1)
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_185]) ).
cnf(c_23,plain,
( sK3(sK1) != sK1
| sK2(f(sK1)) != f(sK1)
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_186]) ).
cnf(c_187,plain,
( f(g(sK0)) = sK0
| g(f(sK3(sK1))) = sK3(sK1)
| sK2(f(sK1)) != f(sK1)
| f(sK1) != f(sK1)
| f(g(sK0)) = sK0 ),
inference(paramod,[status(thm)],[c_2,c_17]) ).
cnf(c_188,plain,
( f(g(sK0)) = sK0
| g(f(sK3(sK1))) = sK3(sK1)
| sK2(f(sK1)) != f(sK1)
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_187]) ).
cnf(c_24,plain,
( g(f(sK3(sK1))) = sK3(sK1)
| sK2(f(sK1)) != f(sK1)
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_188]) ).
cnf(c_189,negated_conjecture,
( sK1 = sK3(sK1)
| f(g(sK0)) = sK0
| f(g(sK2(f(sK1)))) = sK2(f(sK1))
| f(g(sK0)) = sK0 ),
inference(resolve,[status(thm)],[c_21,c_4]) ).
cnf(c_190,negated_conjecture,
( sK3(sK1) = sK1
| f(g(sK0)) = sK0
| f(g(sK2(f(sK1)))) = sK2(f(sK1))
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_30,negated_conjecture,
( sK3(sK1) = sK1
| f(g(sK2(f(sK1)))) = sK2(f(sK1))
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_190]) ).
cnf(c_191,plain,
( f(g(sK2(f(sK1)))) = sK2(f(sK1))
| f(g(sK0)) = sK0
| f(g(sK2(f(sK1)))) = sK2(f(sK1))
| f(g(sK0)) = sK0 ),
inference(resolve,[status(thm)],[c_30,c_22]) ).
cnf(c_192,plain,
( f(g(sK2(f(sK1)))) = sK2(f(sK1))
| f(g(sK2(f(sK1)))) = sK2(f(sK1))
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_191]) ).
cnf(c_32,plain,
( f(g(sK2(f(sK1)))) = sK2(f(sK1))
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_192]) ).
cnf(c_193,plain,
( sK1 = g(sK2(f(sK1)))
| g(sK2(f(sK1))) != g(sK2(f(sK1)))
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(paramod,[status(thm)],[c_32,c_4]) ).
cnf(c_194,plain,
( g(sK2(f(sK1))) = sK1
| g(sK2(f(sK1))) != g(sK2(f(sK1)))
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_193]) ).
cnf(c_195,plain,
( g(sK2(f(sK1))) = sK1
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_41,plain,
( g(sK2(f(sK1))) = sK1
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_195]) ).
cnf(c_196,plain,
( f(sK1) = sK2(f(sK1))
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(paramod,[status(thm)],[c_41,c_32]) ).
cnf(c_197,plain,
( sK2(f(sK1)) = f(sK1)
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_196]) ).
cnf(c_48,plain,
( sK2(f(sK1)) = f(sK1)
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_197]) ).
cnf(c_198,plain,
( g(f(sK3(sK1))) = sK3(sK1)
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(resolve,[status(thm)],[c_48,c_24]) ).
cnf(c_49,plain,
( g(f(sK3(sK1))) = sK3(sK1)
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_198]) ).
cnf(c_199,plain,
( sK3(sK1) != sK1
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(resolve,[status(thm)],[c_48,c_23]) ).
cnf(c_50,plain,
( sK3(sK1) != sK1
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_199]) ).
cnf(c_200,negated_conjecture,
( sK1 = sK3(sK1)
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(resolve,[status(thm)],[c_49,c_4]) ).
cnf(c_201,negated_conjecture,
( sK3(sK1) = sK1
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_200]) ).
cnf(c_64,negated_conjecture,
( sK3(sK1) = sK1
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_201]) ).
cnf(c_202,plain,
( f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(resolve,[status(thm)],[c_64,c_50]) ).
cnf(c_66,plain,
f(g(sK0)) = sK0,
inference(copy,[status(thm)],[c_202]) ).
cnf(c_67,plain,
( sK3(A) != A
| g(f(A)) != A
| sK2(sK0) != sK0 ),
inference(resolve,[status(thm)],[c_66,c_12]) ).
cnf(c_68,plain,
( g(f(sK3(A))) = sK3(A)
| g(f(A)) != A
| sK2(sK0) != sK0 ),
inference(resolve,[status(thm)],[c_66,c_11]) ).
cnf(c_69,plain,
( sK3(A) != A
| g(f(A)) != A
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(resolve,[status(thm)],[c_66,c_10]) ).
cnf(c_70,plain,
( g(f(sK3(A))) = sK3(A)
| g(f(A)) != A
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(resolve,[status(thm)],[c_66,c_9]) ).
cnf(c_203,plain,
( sK1 = g(sK0)
| g(sK0) != g(sK0)
| sK0 = A
| f(g(A)) != A ),
inference(paramod,[status(thm)],[c_66,c_8]) ).
cnf(c_204,plain,
( g(sK0) = sK1
| g(sK0) != g(sK0)
| sK0 = A
| f(g(A)) != A ),
inference(copy,[status(thm)],[c_203]) ).
cnf(c_71,plain,
( g(sK0) = sK1
| sK0 = A
| f(g(A)) != A ),
inference(copy,[status(thm)],[c_204]) ).
cnf(c_205,plain,
( g(f(sK3(g(sK0)))) = sK3(g(sK0))
| g(sK0) != g(sK0)
| sK2(A) != A
| f(g(A)) != A ),
inference(paramod,[status(thm)],[c_66,c_11]) ).
cnf(c_74,plain,
( g(f(sK3(g(sK0)))) = sK3(g(sK0))
| sK2(A) != A
| f(g(A)) != A ),
inference(copy,[status(thm)],[c_205]) ).
cnf(c_206,plain,
( g(f(sK3(g(sK0)))) = sK3(g(sK0))
| g(sK0) != g(sK0)
| sK2(sK0) != sK0 ),
inference(paramod,[status(thm)],[c_66,c_68]) ).
cnf(c_77,plain,
( g(f(sK3(g(sK0)))) = sK3(g(sK0))
| sK2(sK0) != sK0 ),
inference(copy,[status(thm)],[c_206]) ).
cnf(c_207,plain,
( sK3(g(sK0)) != g(sK0)
| g(sK0) != g(sK0)
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(paramod,[status(thm)],[c_66,c_69]) ).
cnf(c_78,plain,
( sK3(g(sK0)) != g(sK0)
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(copy,[status(thm)],[c_207]) ).
cnf(c_208,plain,
( g(f(sK3(g(sK0)))) = sK3(g(sK0))
| g(sK0) != g(sK0)
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(paramod,[status(thm)],[c_66,c_70]) ).
cnf(c_79,plain,
( g(f(sK3(g(sK0)))) = sK3(g(sK0))
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(copy,[status(thm)],[c_208]) ).
cnf(c_209,negated_conjecture,
( sK1 = sK3(g(sK0))
| sK0 = A
| f(g(A)) != A
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(resolve,[status(thm)],[c_79,c_8]) ).
cnf(c_82,negated_conjecture,
( sK3(g(sK0)) = sK1
| sK0 = A
| f(g(A)) != A
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(copy,[status(thm)],[c_209]) ).
cnf(c_210,plain,
( g(sK0) = sK1
| sK0 = f(sK3(g(sK0)))
| f(sK3(g(sK0))) != f(sK3(g(sK0)))
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(paramod,[status(thm)],[c_79,c_71]) ).
cnf(c_211,plain,
( g(sK0) = sK1
| f(sK3(g(sK0))) = sK0
| f(sK3(g(sK0))) != f(sK3(g(sK0)))
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(copy,[status(thm)],[c_210]) ).
cnf(c_85,plain,
( g(sK0) = sK1
| f(sK3(g(sK0))) = sK0
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(copy,[status(thm)],[c_211]) ).
cnf(c_212,plain,
( g(sK0) = sK3(g(sK0))
| f(g(sK2(sK0))) = sK2(sK0)
| g(sK0) = sK1
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(paramod,[status(thm)],[c_85,c_79]) ).
cnf(c_213,plain,
( sK3(g(sK0)) = g(sK0)
| f(g(sK2(sK0))) = sK2(sK0)
| g(sK0) = sK1
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(copy,[status(thm)],[c_212]) ).
cnf(c_86,plain,
( sK3(g(sK0)) = g(sK0)
| g(sK0) = sK1
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(copy,[status(thm)],[c_213]) ).
cnf(c_214,plain,
( f(g(sK2(sK0))) = sK2(sK0)
| g(sK0) = sK1
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(resolve,[status(thm)],[c_86,c_78]) ).
cnf(c_87,plain,
( g(sK0) = sK1
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(copy,[status(thm)],[c_214]) ).
cnf(c_215,plain,
( g(sK0) = sK1
| sK0 = sK2(sK0)
| g(sK0) = sK1 ),
inference(resolve,[status(thm)],[c_87,c_71]) ).
cnf(c_216,plain,
( g(sK0) = sK1
| sK2(sK0) = sK0
| g(sK0) = sK1 ),
inference(copy,[status(thm)],[c_215]) ).
cnf(c_97,plain,
( sK2(sK0) = sK0
| g(sK0) = sK1 ),
inference(copy,[status(thm)],[c_216]) ).
cnf(c_108,plain,
( g(f(sK3(g(sK0)))) = sK3(g(sK0))
| g(sK0) = sK1 ),
inference(resolve,[status(thm)],[c_97,c_77]) ).
cnf(c_111,plain,
( sK3(A) != A
| g(f(A)) != A
| g(sK0) = sK1 ),
inference(resolve,[status(thm)],[c_97,c_67]) ).
cnf(c_217,plain,
( sK3(g(sK0)) = sK1
| sK0 = f(sK3(g(sK0)))
| f(sK3(g(sK0))) != f(sK3(g(sK0)))
| f(g(sK2(sK0))) = sK2(sK0)
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(paramod,[status(thm)],[c_79,c_82]) ).
cnf(c_218,plain,
( sK3(g(sK0)) = sK1
| f(sK3(g(sK0))) = sK0
| f(sK3(g(sK0))) != f(sK3(g(sK0)))
| f(g(sK2(sK0))) = sK2(sK0)
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(copy,[status(thm)],[c_217]) ).
cnf(c_219,plain,
( sK3(g(sK0)) = sK1
| f(sK3(g(sK0))) = sK0
| f(g(sK2(sK0))) = sK2(sK0)
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(copy,[status(thm)],[c_218]) ).
cnf(c_116,plain,
( sK3(g(sK0)) = sK1
| f(sK3(g(sK0))) = sK0
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(copy,[status(thm)],[c_219]) ).
cnf(c_220,plain,
( g(sK0) = sK1
| sK0 = f(sK3(g(sK0)))
| f(sK3(g(sK0))) != f(sK3(g(sK0)))
| g(sK0) = sK1 ),
inference(paramod,[status(thm)],[c_108,c_71]) ).
cnf(c_221,plain,
( g(sK0) = sK1
| f(sK3(g(sK0))) = sK0
| f(sK3(g(sK0))) != f(sK3(g(sK0)))
| g(sK0) = sK1 ),
inference(copy,[status(thm)],[c_220]) ).
cnf(c_222,plain,
( g(sK0) = sK1
| f(sK3(g(sK0))) = sK0
| g(sK0) = sK1 ),
inference(copy,[status(thm)],[c_221]) ).
cnf(c_124,plain,
( f(sK3(g(sK0))) = sK0
| g(sK0) = sK1 ),
inference(copy,[status(thm)],[c_222]) ).
cnf(c_223,plain,
( g(sK0) = sK3(g(sK0))
| g(sK0) = sK1
| g(sK0) = sK1 ),
inference(paramod,[status(thm)],[c_124,c_108]) ).
cnf(c_224,plain,
( sK3(g(sK0)) = g(sK0)
| g(sK0) = sK1
| g(sK0) = sK1 ),
inference(copy,[status(thm)],[c_223]) ).
cnf(c_125,plain,
( sK3(g(sK0)) = g(sK0)
| g(sK0) = sK1 ),
inference(copy,[status(thm)],[c_224]) ).
cnf(c_225,plain,
( g(f(g(sK0))) != g(sK0)
| g(sK0) = sK1
| g(sK0) = sK1 ),
inference(resolve,[status(thm)],[c_125,c_111]) ).
cnf(c_226,plain,
( g(sK0) != g(sK0)
| g(sK0) = sK1
| g(sK0) = sK1 ),
inference(paramod,[status(thm)],[c_66,c_225]) ).
cnf(c_227,plain,
( g(sK0) = sK1
| g(sK0) = sK1 ),
inference(copy,[status(thm)],[c_226]) ).
cnf(c_126,plain,
g(sK0) = sK1,
inference(copy,[status(thm)],[c_227]) ).
cnf(c_228,plain,
( sK3(g(sK0)) = sK1
| f(sK3(sK1)) = sK0
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(paramod,[status(thm)],[c_126,c_116]) ).
cnf(c_129,plain,
( sK3(sK1) = sK1
| f(sK3(sK1)) = sK0
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(paramod,[status(thm)],[c_126,c_228]) ).
cnf(c_229,plain,
( g(f(sK3(sK1))) = sK3(g(sK0))
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(paramod,[status(thm)],[c_126,c_79]) ).
cnf(c_140,plain,
( g(f(sK3(sK1))) = sK3(sK1)
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(paramod,[status(thm)],[c_126,c_229]) ).
cnf(c_230,plain,
( sK3(sK1) != g(sK0)
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(paramod,[status(thm)],[c_126,c_78]) ).
cnf(c_141,plain,
( sK3(sK1) != sK1
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(paramod,[status(thm)],[c_126,c_230]) ).
cnf(c_231,plain,
( g(f(sK3(sK1))) = sK3(g(sK0))
| sK2(A) != A
| f(g(A)) != A ),
inference(paramod,[status(thm)],[c_126,c_74]) ).
cnf(c_145,plain,
( g(f(sK3(sK1))) = sK3(sK1)
| sK2(A) != A
| f(g(A)) != A ),
inference(paramod,[status(thm)],[c_126,c_231]) ).
cnf(c_148,plain,
f(sK1) = sK0,
inference(paramod,[status(thm)],[c_126,c_66]) ).
cnf(c_232,plain,
( g(sK0) = sK3(sK1)
| f(g(sK2(sK0))) = sK2(sK0)
| sK3(sK1) = sK1
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(paramod,[status(thm)],[c_129,c_140]) ).
cnf(c_233,plain,
( sK1 = sK3(sK1)
| f(g(sK2(sK0))) = sK2(sK0)
| sK3(sK1) = sK1
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(paramod,[status(thm)],[c_126,c_232]) ).
cnf(c_234,plain,
( sK3(sK1) = sK1
| f(g(sK2(sK0))) = sK2(sK0)
| sK3(sK1) = sK1
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(copy,[status(thm)],[c_233]) ).
cnf(c_235,plain,
( sK3(sK1) = sK1
| sK3(sK1) = sK1
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(copy,[status(thm)],[c_234]) ).
cnf(c_149,plain,
( sK3(sK1) = sK1
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(copy,[status(thm)],[c_235]) ).
cnf(c_236,plain,
( f(g(sK2(sK0))) = sK2(sK0)
| f(g(sK2(sK0))) = sK2(sK0) ),
inference(resolve,[status(thm)],[c_149,c_141]) ).
cnf(c_152,plain,
f(g(sK2(sK0))) = sK2(sK0),
inference(copy,[status(thm)],[c_236]) ).
cnf(c_154,plain,
( sK3(A) != A
| g(f(A)) != A
| sK2(sK2(sK0)) != sK2(sK0) ),
inference(resolve,[status(thm)],[c_152,c_12]) ).
cnf(c_237,negated_conjecture,
( sK1 = A
| g(f(A)) != A
| sK0 = sK2(sK0) ),
inference(resolve,[status(thm)],[c_152,c_8]) ).
cnf(c_158,negated_conjecture,
( sK1 = A
| g(f(A)) != A
| sK2(sK0) = sK0 ),
inference(copy,[status(thm)],[c_237]) ).
cnf(c_166,plain,
( g(f(sK3(sK1))) = sK3(sK1)
| sK2(sK2(sK0)) != sK2(sK0) ),
inference(resolve,[status(thm)],[c_145,c_152]) ).
cnf(c_238,plain,
( sK3(g(sK2(sK0))) != g(sK2(sK0))
| g(sK2(sK0)) != g(sK2(sK0))
| sK2(sK2(sK0)) != sK2(sK0) ),
inference(paramod,[status(thm)],[c_152,c_154]) ).
cnf(c_169,plain,
( sK3(g(sK2(sK0))) != g(sK2(sK0))
| sK2(sK2(sK0)) != sK2(sK0) ),
inference(copy,[status(thm)],[c_238]) ).
cnf(c_239,plain,
( sK1 = g(sK2(sK0))
| g(sK2(sK0)) != g(sK2(sK0))
| sK2(sK0) = sK0 ),
inference(paramod,[status(thm)],[c_152,c_158]) ).
cnf(c_240,plain,
( g(sK2(sK0)) = sK1
| g(sK2(sK0)) != g(sK2(sK0))
| sK2(sK0) = sK0 ),
inference(copy,[status(thm)],[c_239]) ).
cnf(c_170,plain,
( g(sK2(sK0)) = sK1
| sK2(sK0) = sK0 ),
inference(copy,[status(thm)],[c_240]) ).
cnf(c_241,plain,
( f(sK1) = sK2(sK0)
| sK2(sK0) = sK0 ),
inference(paramod,[status(thm)],[c_170,c_152]) ).
cnf(c_242,plain,
( sK0 = sK2(sK0)
| sK2(sK0) = sK0 ),
inference(paramod,[status(thm)],[c_148,c_241]) ).
cnf(c_243,plain,
( sK2(sK0) = sK0
| sK2(sK0) = sK0 ),
inference(copy,[status(thm)],[c_242]) ).
cnf(c_171,plain,
sK2(sK0) = sK0,
inference(copy,[status(thm)],[c_243]) ).
cnf(c_244,plain,
( sK3(g(sK2(sK0))) != g(sK2(sK0))
| sK2(sK0) != sK2(sK0) ),
inference(paramod,[status(thm)],[c_171,c_169]) ).
cnf(c_245,plain,
( sK3(g(sK2(sK0))) != g(sK2(sK0))
| sK0 != sK2(sK0) ),
inference(paramod,[status(thm)],[c_171,c_244]) ).
cnf(c_246,plain,
( sK3(g(sK2(sK0))) != g(sK2(sK0))
| sK0 != sK0 ),
inference(paramod,[status(thm)],[c_171,c_245]) ).
cnf(c_247,plain,
( sK3(g(sK0)) != g(sK2(sK0))
| sK0 != sK0 ),
inference(paramod,[status(thm)],[c_171,c_246]) ).
cnf(c_248,plain,
( sK3(sK1) != g(sK2(sK0))
| sK0 != sK0 ),
inference(paramod,[status(thm)],[c_126,c_247]) ).
cnf(c_249,plain,
( sK3(sK1) != g(sK0)
| sK0 != sK0 ),
inference(paramod,[status(thm)],[c_171,c_248]) ).
cnf(c_250,plain,
( sK3(sK1) != sK1
| sK0 != sK0 ),
inference(paramod,[status(thm)],[c_126,c_249]) ).
cnf(c_172,plain,
sK3(sK1) != sK1,
inference(copy,[status(thm)],[c_250]) ).
cnf(c_251,plain,
( g(f(sK3(sK1))) = sK3(sK1)
| sK2(sK0) != sK2(sK0) ),
inference(paramod,[status(thm)],[c_171,c_166]) ).
cnf(c_252,plain,
( g(f(sK3(sK1))) = sK3(sK1)
| sK0 != sK2(sK0) ),
inference(paramod,[status(thm)],[c_171,c_251]) ).
cnf(c_253,plain,
( g(f(sK3(sK1))) = sK3(sK1)
| sK0 != sK0 ),
inference(paramod,[status(thm)],[c_171,c_252]) ).
cnf(c_173,plain,
g(f(sK3(sK1))) = sK3(sK1),
inference(copy,[status(thm)],[c_253]) ).
cnf(c_254,negated_conjecture,
( sK1 = sK3(sK1)
| sK0 = A
| f(g(A)) != A ),
inference(resolve,[status(thm)],[c_173,c_8]) ).
cnf(c_255,negated_conjecture,
( sK3(sK1) = sK1
| sK0 = A
| f(g(A)) != A ),
inference(copy,[status(thm)],[c_254]) ).
cnf(c_176,negated_conjecture,
( sK0 = A
| f(g(A)) != A ),
inference(resolve,[status(thm)],[c_172,c_255]) ).
cnf(c_256,plain,
( sK0 = f(sK3(sK1))
| f(sK3(sK1)) != f(sK3(sK1)) ),
inference(paramod,[status(thm)],[c_173,c_176]) ).
cnf(c_257,plain,
( f(sK3(sK1)) = sK0
| f(sK3(sK1)) != f(sK3(sK1)) ),
inference(copy,[status(thm)],[c_256]) ).
cnf(c_178,plain,
f(sK3(sK1)) = sK0,
inference(copy,[status(thm)],[c_257]) ).
cnf(c_258,plain,
g(sK0) = sK3(sK1),
inference(paramod,[status(thm)],[c_178,c_173]) ).
cnf(c_259,plain,
sK1 = sK3(sK1),
inference(paramod,[status(thm)],[c_126,c_258]) ).
cnf(c_260,plain,
sK3(sK1) = sK1,
inference(copy,[status(thm)],[c_259]) ).
cnf(c_179,plain,
$false,
inference(resolve,[status(thm)],[c_172,c_260]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN551+3 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 18:13:14 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 1237586 was started by sandbox on n011,
% 0.09/0.37 % Sat Sep 26 18:13:14 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.13/0.37
% 0.13/0.37 % From the command line: assign(max_seconds, 300).
% 0.13/0.45
% 0.13/0.45 % SZS status Theorem for theBenchmark
% 0.13/0.45
% 0.13/0.45 % Proof 1 at 0.04 (+ 0.02) seconds.
% 0.13/0.45 % Length of proof is 64.
% 0.13/0.45 % Level of proof is 30.
% 0.13/0.45 % Maximum clause weight is 46.000.
% 0.13/0.45 % Given clauses 87.
% 0.13/0.45
% 0.13/0.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------