%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN551+1 : 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 : n007.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 8.91s 1.52s
% Output : CNFRefutation 8.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 112
% Number of leaves : 1
% Syntax : Number of formulae : 381 ( 19 unt; 0 def)
% Number of atoms : 1350 (1349 equ)
% Maximal formula atoms : 52 ( 3 avg)
% Number of connectives : 1320 ( 351 ~; 929 |; 34 &)
% ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-1 aty)
% Number of variables : 176 ( 0 sgn 46 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(prove_this_cute_thing,conjecture,
( ( ! [Y,Z] :
( ( Z = f(g(Z))
& Y = f(g(Y)) )
=> Y = Z )
& ? [X] : X = f(g(X)) )
<=> ( ! [Y,Z] :
( ( Z = g(f(Z))
& Y = g(f(Y)) )
=> Y = Z )
& ? [X] : X = g(f(X)) ) ),
file('theBenchmark.p',prove_this_cute_thing) ).
fof(prove_this_cute_thing_neg,negated_conjecture,
~ ( ( ! [Y,Z] :
( ( Z = f(g(Z))
& Y = f(g(Y)) )
=> Y = Z )
& ? [X] : X = f(g(X)) )
<=> ( ! [Y,Z] :
( ( Z = g(f(Z))
& Y = g(f(Y)) )
=> Y = Z )
& ? [X] : X = g(f(X)) ) ),
inference(assume_negation,[status(cth)],[prove_this_cute_thing]) ).
fof(nnf_1,plain,
( ( ? [Y,Z] :
( Z != Y
& g(f(Z)) = Z
& g(f(Y)) = Y )
| ! [X] : g(f(X)) != X
| ? [X7,X8] :
( X8 != X7
& f(g(X8)) = X8
& f(g(X7)) = X7 )
| ! [X6] : f(g(X6)) != X6 )
& ( ( ! [X4,X5] :
( X5 = X4
| g(f(X5)) != X5
| g(f(X4)) != X4 )
& ? [X3] : g(f(X3)) = X3 )
| ( ! [X1,X2] :
( X2 = X1
| f(g(X2)) != X2
| f(g(X1)) != X1 )
& ? [X0] : f(g(X0)) = X0 ) ) ),
inference(fof_nnf,[status(thm)],[prove_this_cute_thing_neg]) ).
fof(sk_prove_this_cute_thing_neg_sk,plain,
( ( ( sK4 != sK3
& g(f(sK4)) = sK4
& g(f(sK3)) = sK3 )
| ! [X] : g(f(X)) != X
| ( sK5 != sK2
& f(g(sK5)) = sK5
& f(g(sK2)) = sK2 )
| ! [X6] : f(g(X6)) != X6 )
& ( ( ! [X4,X5] :
( X5 = X4
| g(f(X5)) != X5
| g(f(X4)) != X4 )
& g(f(sK1)) = sK1 )
| ( ! [X1,X2] :
( X2 = X1
| f(g(X2)) != X2
| f(g(X1)) != X1 )
& f(g(sK0)) = sK0 ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK5,sK3,sK4]),skolemize(X0,sK0),skolemize(X3,sK1),skolemize(X7,sK2),skolemize(X8,sK5),skolemize(Y,sK3),skolemize(Z,sK4)],[nnf_1]) ).
fof(sk_prove_this_cute_thing_neg,plain,
( ! [VAR_0,VAR_1] :
( sK4 != sK3
| g(f(VAR_1)) != VAR_1
| sK5 != sK2
| f(g(VAR_0)) != VAR_0 )
& ! [VAR_0,VAR_1] :
( g(f(sK4)) = sK4
| g(f(VAR_1)) != VAR_1
| sK5 != sK2
| f(g(VAR_0)) != VAR_0 )
& ! [VAR_0,VAR_1] :
( g(f(sK3)) = sK3
| g(f(VAR_1)) != VAR_1
| sK5 != sK2
| f(g(VAR_0)) != VAR_0 )
& ! [VAR_0,VAR_1] :
( sK4 != sK3
| g(f(VAR_1)) != VAR_1
| f(g(sK5)) = sK5
| f(g(VAR_0)) != VAR_0 )
& ! [VAR_0,VAR_1] :
( g(f(sK4)) = sK4
| g(f(VAR_1)) != VAR_1
| f(g(sK5)) = sK5
| f(g(VAR_0)) != VAR_0 )
& ! [VAR_0,VAR_1] :
( g(f(sK3)) = sK3
| g(f(VAR_1)) != VAR_1
| f(g(sK5)) = sK5
| f(g(VAR_0)) != VAR_0 )
& ! [VAR_0,VAR_1] :
( sK4 != sK3
| g(f(VAR_1)) != VAR_1
| f(g(sK2)) = sK2
| f(g(VAR_0)) != VAR_0 )
& ! [VAR_0,VAR_1] :
( g(f(sK4)) = sK4
| g(f(VAR_1)) != VAR_1
| f(g(sK2)) = sK2
| f(g(VAR_0)) != VAR_0 )
& ! [VAR_0,VAR_1] :
( g(f(sK3)) = sK3
| g(f(VAR_1)) != VAR_1
| f(g(sK2)) = sK2
| f(g(VAR_0)) != VAR_0 )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( VAR_3 = VAR_2
| g(f(VAR_3)) != VAR_3
| g(f(VAR_2)) != VAR_2
| VAR_1 = VAR_0
| f(g(VAR_1)) != VAR_1
| f(g(VAR_0)) != VAR_0 )
& ! [VAR_0,VAR_1] :
( g(f(sK1)) = sK1
| VAR_1 = VAR_0
| f(g(VAR_1)) != VAR_1
| f(g(VAR_0)) != VAR_0 )
& ! [VAR_0,VAR_1] :
( VAR_1 = VAR_0
| g(f(VAR_1)) != VAR_1
| 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,
( B = A
| g(f(B)) != B
| g(f(A)) != A
| f(g(sK0)) = sK0 ),
inference(split_conjunct,[status(thm)],[sk_prove_this_cute_thing_neg]) ).
cnf(c_4,negated_conjecture,
( g(f(sK1)) = sK1
| B = A
| f(g(B)) != B
| f(g(A)) != A ),
inference(split_conjunct,[status(thm)],[sk_prove_this_cute_thing_neg]) ).
cnf(c_5,negated_conjecture,
( D = C
| g(f(D)) != D
| g(f(C)) != C
| B = A
| f(g(B)) != B
| f(g(A)) != A ),
inference(split_conjunct,[status(thm)],[sk_prove_this_cute_thing_neg]) ).
cnf(c_6,negated_conjecture,
( g(f(sK3)) = sK3
| g(f(B)) != B
| f(g(sK2)) = sK2
| f(g(A)) != A ),
inference(split_conjunct,[status(thm)],[sk_prove_this_cute_thing_neg]) ).
cnf(c_7,negated_conjecture,
( g(f(sK4)) = sK4
| g(f(B)) != B
| f(g(sK2)) = sK2
| f(g(A)) != A ),
inference(split_conjunct,[status(thm)],[sk_prove_this_cute_thing_neg]) ).
cnf(c_8,negated_conjecture,
( sK4 != sK3
| g(f(B)) != B
| f(g(sK2)) = sK2
| f(g(A)) != A ),
inference(split_conjunct,[status(thm)],[sk_prove_this_cute_thing_neg]) ).
cnf(c_9,negated_conjecture,
( g(f(sK3)) = sK3
| g(f(B)) != B
| f(g(sK5)) = sK5
| f(g(A)) != A ),
inference(split_conjunct,[status(thm)],[sk_prove_this_cute_thing_neg]) ).
cnf(c_10,negated_conjecture,
( g(f(sK4)) = sK4
| g(f(B)) != B
| f(g(sK5)) = sK5
| f(g(A)) != A ),
inference(split_conjunct,[status(thm)],[sk_prove_this_cute_thing_neg]) ).
cnf(c_11,negated_conjecture,
( sK4 != sK3
| g(f(B)) != B
| f(g(sK5)) = sK5
| f(g(A)) != A ),
inference(split_conjunct,[status(thm)],[sk_prove_this_cute_thing_neg]) ).
cnf(c_12,negated_conjecture,
( g(f(sK3)) = sK3
| g(f(B)) != B
| sK5 != sK2
| f(g(A)) != A ),
inference(split_conjunct,[status(thm)],[sk_prove_this_cute_thing_neg]) ).
cnf(c_13,negated_conjecture,
( g(f(sK4)) = sK4
| g(f(B)) != B
| sK5 != sK2
| f(g(A)) != A ),
inference(split_conjunct,[status(thm)],[sk_prove_this_cute_thing_neg]) ).
cnf(c_14,negated_conjecture,
( sK4 != sK3
| g(f(B)) != B
| sK5 != sK2
| f(g(A)) != A ),
inference(split_conjunct,[status(thm)],[sk_prove_this_cute_thing_neg]) ).
cnf(c_1615,negated_conjecture,
( f(g(sK0)) = sK0
| A = sK1
| g(f(A)) != A
| f(g(sK0)) = sK0 ),
inference(resolve,[status(thm)],[c_3,c_2]) ).
cnf(c_1616,negated_conjecture,
( f(g(sK0)) = sK0
| sK1 = A
| g(f(A)) != A
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1615]) ).
cnf(c_18,negated_conjecture,
( sK1 = A
| g(f(A)) != A
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1616]) ).
cnf(c_1617,negated_conjecture,
( g(f(sK1)) = sK1
| g(f(sK1)) = sK1
| A = sK0
| f(g(A)) != A ),
inference(resolve,[status(thm)],[c_4,c_2]) ).
cnf(c_1618,negated_conjecture,
( g(f(sK1)) = sK1
| g(f(sK1)) = sK1
| sK0 = A
| f(g(A)) != A ),
inference(copy,[status(thm)],[c_1617]) ).
cnf(c_19,negated_conjecture,
( g(f(sK1)) = sK1
| sK0 = A
| f(g(A)) != A ),
inference(copy,[status(thm)],[c_1618]) ).
cnf(c_20,plain,
( g(f(sK1)) = sK1
| g(f(sK3)) = sK3
| g(f(A)) != A
| f(g(sK2)) = sK2 ),
inference(resolve,[status(thm)],[c_6,c_2]) ).
cnf(c_21,plain,
( f(g(sK0)) = sK0
| g(f(sK3)) = sK3
| f(g(sK2)) = sK2
| f(g(A)) != A ),
inference(resolve,[status(thm)],[c_6,c_2]) ).
cnf(c_24,plain,
( g(f(sK1)) = sK1
| g(f(sK4)) = sK4
| g(f(A)) != A
| f(g(sK2)) = sK2 ),
inference(resolve,[status(thm)],[c_7,c_2]) ).
cnf(c_25,plain,
( f(g(sK0)) = sK0
| g(f(sK4)) = sK4
| f(g(sK2)) = sK2
| f(g(A)) != A ),
inference(resolve,[status(thm)],[c_7,c_2]) ).
cnf(c_29,plain,
( f(g(sK0)) = sK0
| sK4 != sK3
| f(g(sK2)) = sK2
| f(g(A)) != A ),
inference(resolve,[status(thm)],[c_8,c_2]) ).
cnf(c_32,plain,
( g(f(sK1)) = sK1
| g(f(sK3)) = sK3
| g(f(A)) != A
| f(g(sK5)) = sK5 ),
inference(resolve,[status(thm)],[c_9,c_2]) ).
cnf(c_33,plain,
( f(g(sK0)) = sK0
| g(f(sK3)) = sK3
| f(g(sK5)) = sK5
| f(g(A)) != A ),
inference(resolve,[status(thm)],[c_9,c_2]) ).
cnf(c_36,plain,
( g(f(sK1)) = sK1
| g(f(sK4)) = sK4
| g(f(A)) != A
| f(g(sK5)) = sK5 ),
inference(resolve,[status(thm)],[c_10,c_2]) ).
cnf(c_37,plain,
( f(g(sK0)) = sK0
| g(f(sK4)) = sK4
| f(g(sK5)) = sK5
| f(g(A)) != A ),
inference(resolve,[status(thm)],[c_10,c_2]) ).
cnf(c_40,plain,
( g(f(sK1)) = sK1
| sK4 != sK3
| g(f(A)) != A
| f(g(sK5)) = sK5 ),
inference(resolve,[status(thm)],[c_11,c_2]) ).
cnf(c_41,plain,
( f(g(sK0)) = sK0
| sK4 != sK3
| f(g(sK5)) = sK5
| f(g(A)) != A ),
inference(resolve,[status(thm)],[c_11,c_2]) ).
cnf(c_48,plain,
( g(f(sK1)) = sK1
| g(f(sK4)) = sK4
| g(f(A)) != A
| sK5 != sK2 ),
inference(resolve,[status(thm)],[c_13,c_2]) ).
cnf(c_49,plain,
( f(g(sK0)) = sK0
| g(f(sK4)) = sK4
| sK5 != sK2
| f(g(A)) != A ),
inference(resolve,[status(thm)],[c_13,c_2]) ).
cnf(c_52,plain,
( g(f(sK1)) = sK1
| sK4 != sK3
| g(f(A)) != A
| sK5 != sK2 ),
inference(resolve,[status(thm)],[c_14,c_2]) ).
cnf(c_1619,plain,
( g(f(sK1)) = sK1
| sK4 != sK3
| g(sK0) != g(sK0)
| sK5 != sK2
| g(f(sK1)) = sK1 ),
inference(paramod,[status(thm)],[c_2,c_52]) ).
cnf(c_1620,plain,
( g(f(sK1)) = sK1
| sK4 != sK3
| sK5 != sK2
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1619]) ).
cnf(c_56,plain,
( sK4 != sK3
| sK5 != sK2
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1620]) ).
cnf(c_1621,plain,
( g(f(sK1)) = sK1
| g(f(sK3)) = sK3
| g(sK0) != g(sK0)
| f(g(sK2)) = sK2
| g(f(sK1)) = sK1 ),
inference(paramod,[status(thm)],[c_2,c_20]) ).
cnf(c_1622,plain,
( g(f(sK1)) = sK1
| g(f(sK3)) = sK3
| f(g(sK2)) = sK2
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1621]) ).
cnf(c_59,plain,
( g(f(sK3)) = sK3
| f(g(sK2)) = sK2
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1622]) ).
cnf(c_1623,plain,
( f(g(sK0)) = sK0
| g(f(sK3)) = sK3
| f(g(sK2)) = sK2
| f(sK1) != f(sK1)
| f(g(sK0)) = sK0 ),
inference(paramod,[status(thm)],[c_2,c_21]) ).
cnf(c_1624,plain,
( f(g(sK0)) = sK0
| g(f(sK3)) = sK3
| f(g(sK2)) = sK2
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1623]) ).
cnf(c_60,plain,
( g(f(sK3)) = sK3
| f(g(sK2)) = sK2
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1624]) ).
cnf(c_1625,negated_conjecture,
( g(f(sK3)) = sK3
| f(g(sK2)) = sK2
| f(g(A)) != A
| g(f(sK3)) = sK3
| f(g(sK2)) = sK2 ),
inference(resolve,[status(thm)],[c_59,c_6]) ).
cnf(c_1626,negated_conjecture,
( g(f(sK3)) = sK3
| f(g(A)) != A
| g(f(sK3)) = sK3
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1625]) ).
cnf(c_68,negated_conjecture,
( f(g(A)) != A
| g(f(sK3)) = sK3
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1626]) ).
cnf(c_1627,plain,
( g(f(sK1)) = sK1
| sK0 = f(sK3)
| f(sK3) != f(sK3)
| f(g(sK2)) = sK2
| g(f(sK1)) = sK1 ),
inference(paramod,[status(thm)],[c_59,c_19]) ).
cnf(c_1628,plain,
( g(f(sK1)) = sK1
| f(sK3) = sK0
| f(sK3) != f(sK3)
| f(g(sK2)) = sK2
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1627]) ).
cnf(c_1629,plain,
( g(f(sK1)) = sK1
| f(sK3) = sK0
| f(g(sK2)) = sK2
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1628]) ).
cnf(c_73,plain,
( f(sK3) = sK0
| f(g(sK2)) = sK2
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1629]) ).
cnf(c_1630,plain,
( f(g(sK2)) = sK2
| g(f(sK1)) = sK1
| g(f(sK1)) = sK1
| g(f(sK4)) = sK4
| f(g(sK2)) = sK2 ),
inference(resolve,[status(thm)],[c_24,c_59]) ).
cnf(c_1631,plain,
( f(g(sK2)) = sK2
| g(f(sK1)) = sK1
| g(f(sK4)) = sK4
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1630]) ).
cnf(c_117,plain,
( g(f(sK1)) = sK1
| g(f(sK4)) = sK4
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1631]) ).
cnf(c_1632,plain,
( f(g(sK0)) = sK0
| g(f(sK4)) = sK4
| f(g(sK2)) = sK2
| f(sK1) != f(sK1)
| f(g(sK0)) = sK0 ),
inference(paramod,[status(thm)],[c_2,c_25]) ).
cnf(c_1633,plain,
( f(g(sK0)) = sK0
| g(f(sK4)) = sK4
| f(g(sK2)) = sK2
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1632]) ).
cnf(c_118,plain,
( g(f(sK4)) = sK4
| f(g(sK2)) = sK2
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1633]) ).
cnf(c_1634,plain,
( g(sK0) = sK3
| f(g(sK2)) = sK2
| g(f(sK1)) = sK1
| f(g(sK2)) = sK2
| g(f(sK1)) = sK1 ),
inference(paramod,[status(thm)],[c_73,c_59]) ).
cnf(c_1635,plain,
( g(sK0) = sK3
| f(g(sK2)) = sK2
| f(g(sK2)) = sK2
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1634]) ).
cnf(c_128,plain,
( g(sK0) = sK3
| f(g(sK2)) = sK2
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1635]) ).
cnf(c_1636,plain,
( f(g(sK0)) = sK0
| sK4 != sK3
| f(g(sK2)) = sK2
| f(sK1) != f(sK1)
| f(g(sK0)) = sK0 ),
inference(paramod,[status(thm)],[c_2,c_29]) ).
cnf(c_1637,plain,
( f(g(sK0)) = sK0
| sK4 != sK3
| f(g(sK2)) = sK2
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1636]) ).
cnf(c_178,plain,
( sK4 != sK3
| f(g(sK2)) = sK2
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1637]) ).
cnf(c_1638,plain,
( g(f(sK1)) = sK1
| g(f(sK3)) = sK3
| g(sK0) != g(sK0)
| f(g(sK5)) = sK5
| g(f(sK1)) = sK1 ),
inference(paramod,[status(thm)],[c_2,c_32]) ).
cnf(c_1639,plain,
( g(f(sK1)) = sK1
| g(f(sK3)) = sK3
| f(g(sK5)) = sK5
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1638]) ).
cnf(c_179,plain,
( g(f(sK3)) = sK3
| f(g(sK5)) = sK5
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1639]) ).
cnf(c_1640,plain,
( sK1 = sK3
| f(g(sK0)) = sK0
| f(g(sK2)) = sK2
| f(g(sK0)) = sK0 ),
inference(resolve,[status(thm)],[c_60,c_18]) ).
cnf(c_1641,plain,
( sK3 = sK1
| f(g(sK0)) = sK0
| f(g(sK2)) = sK2
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1640]) ).
cnf(c_192,plain,
( sK3 = sK1
| f(g(sK2)) = sK2
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1641]) ).
cnf(c_1642,plain,
( sK4 != sK1
| f(g(sK2)) = sK2
| f(g(sK0)) = sK0
| f(g(sK2)) = sK2
| f(g(sK0)) = sK0 ),
inference(paramod,[status(thm)],[c_192,c_178]) ).
cnf(c_1643,plain,
( sK4 != sK1
| f(g(sK2)) = sK2
| f(g(sK2)) = sK2
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1642]) ).
cnf(c_208,plain,
( sK4 != sK1
| f(g(sK2)) = sK2
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1643]) ).
cnf(c_1644,plain,
( g(f(sK3)) = sK3
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0
| g(f(sK3)) = sK3
| f(g(sK5)) = sK5 ),
inference(resolve,[status(thm)],[c_33,c_60]) ).
cnf(c_1645,plain,
( g(f(sK3)) = sK3
| f(g(sK0)) = sK0
| g(f(sK3)) = sK3
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1644]) ).
cnf(c_227,plain,
( f(g(sK0)) = sK0
| g(f(sK3)) = sK3
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1645]) ).
cnf(c_1646,plain,
( g(f(sK1)) = sK1
| g(f(sK4)) = sK4
| g(sK0) != g(sK0)
| f(g(sK5)) = sK5
| g(f(sK1)) = sK1 ),
inference(paramod,[status(thm)],[c_2,c_36]) ).
cnf(c_1647,plain,
( g(f(sK1)) = sK1
| g(f(sK4)) = sK4
| f(g(sK5)) = sK5
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1646]) ).
cnf(c_229,plain,
( g(f(sK4)) = sK4
| f(g(sK5)) = sK5
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1647]) ).
cnf(c_1648,plain,
( f(g(sK0)) = sK0
| g(f(sK4)) = sK4
| f(g(sK5)) = sK5
| f(sK1) != f(sK1)
| f(g(sK0)) = sK0 ),
inference(paramod,[status(thm)],[c_2,c_37]) ).
cnf(c_1649,plain,
( f(g(sK0)) = sK0
| g(f(sK4)) = sK4
| f(g(sK5)) = sK5
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1648]) ).
cnf(c_279,plain,
( g(f(sK4)) = sK4
| f(g(sK5)) = sK5
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1649]) ).
cnf(c_1650,plain,
( g(f(sK1)) = sK1
| sK4 != sK3
| g(sK0) != g(sK0)
| f(g(sK5)) = sK5
| g(f(sK1)) = sK1 ),
inference(paramod,[status(thm)],[c_2,c_40]) ).
cnf(c_1651,plain,
( g(f(sK1)) = sK1
| sK4 != sK3
| f(g(sK5)) = sK5
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1650]) ).
cnf(c_281,plain,
( sK4 != sK3
| f(g(sK5)) = sK5
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1651]) ).
cnf(c_1652,plain,
( g(f(sK3)) = sK3
| f(g(sK2)) = sK2
| g(f(sK3)) = sK3
| f(g(sK2)) = sK2 ),
inference(resolve,[status(thm)],[c_68,c_60]) ).
cnf(c_1653,plain,
( g(f(sK3)) = sK3
| g(f(sK3)) = sK3
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1652]) ).
cnf(c_326,plain,
( g(f(sK3)) = sK3
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1653]) ).
cnf(c_1654,plain,
( f(g(sK0)) = sK0
| sK4 != sK3
| f(g(sK5)) = sK5
| f(sK1) != f(sK1)
| f(g(sK0)) = sK0 ),
inference(paramod,[status(thm)],[c_2,c_41]) ).
cnf(c_1655,plain,
( f(g(sK0)) = sK0
| sK4 != sK3
| f(g(sK5)) = sK5
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1654]) ).
cnf(c_328,plain,
( sK4 != sK3
| f(g(sK5)) = sK5
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1655]) ).
cnf(c_1656,negated_conjecture,
( g(f(sK3)) = sK3
| g(f(A)) != A
| sK5 != sK2
| g(f(sK3)) = sK3 ),
inference(resolve,[status(thm)],[c_326,c_12]) ).
cnf(c_336,negated_conjecture,
( g(f(A)) != A
| sK5 != sK2
| g(f(sK3)) = sK3 ),
inference(copy,[status(thm)],[c_1656]) ).
cnf(c_1657,negated_conjecture,
( g(f(sK3)) = sK3
| g(f(A)) != A
| f(g(sK5)) = sK5
| g(f(sK3)) = sK3 ),
inference(resolve,[status(thm)],[c_326,c_9]) ).
cnf(c_339,negated_conjecture,
( g(f(A)) != A
| f(g(sK5)) = sK5
| g(f(sK3)) = sK3 ),
inference(copy,[status(thm)],[c_1657]) ).
cnf(c_1658,negated_conjecture,
( sK4 != sK3
| f(g(sK2)) = sK2
| f(g(A)) != A
| f(g(sK2)) = sK2 ),
inference(resolve,[status(thm)],[c_326,c_8]) ).
cnf(c_345,negated_conjecture,
( sK4 != sK3
| f(g(A)) != A
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1658]) ).
cnf(c_1659,negated_conjecture,
( g(f(sK4)) = sK4
| f(g(sK2)) = sK2
| f(g(A)) != A
| f(g(sK2)) = sK2 ),
inference(resolve,[status(thm)],[c_326,c_7]) ).
cnf(c_346,negated_conjecture,
( g(f(sK4)) = sK4
| f(g(A)) != A
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1659]) ).
cnf(c_1660,plain,
( g(sK2) != g(sK2)
| sK5 != sK2
| g(f(sK3)) = sK3
| g(f(sK3)) = sK3 ),
inference(paramod,[status(thm)],[c_326,c_336]) ).
cnf(c_1661,plain,
( sK5 != sK2
| g(f(sK3)) = sK3
| g(f(sK3)) = sK3 ),
inference(copy,[status(thm)],[c_1660]) ).
cnf(c_366,plain,
( sK5 != sK2
| g(f(sK3)) = sK3 ),
inference(copy,[status(thm)],[c_1661]) ).
cnf(c_1662,plain,
( g(f(sK1)) = sK1
| g(f(sK4)) = sK4
| g(sK0) != g(sK0)
| sK5 != sK2
| g(f(sK1)) = sK1 ),
inference(paramod,[status(thm)],[c_2,c_48]) ).
cnf(c_1663,plain,
( g(f(sK1)) = sK1
| g(f(sK4)) = sK4
| sK5 != sK2
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1662]) ).
cnf(c_368,plain,
( g(f(sK4)) = sK4
| sK5 != sK2
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1663]) ).
cnf(c_1664,plain,
( f(g(sK0)) = sK0
| g(f(sK4)) = sK4
| sK5 != sK2
| f(sK1) != f(sK1)
| f(g(sK0)) = sK0 ),
inference(paramod,[status(thm)],[c_2,c_49]) ).
cnf(c_1665,plain,
( f(g(sK0)) = sK0
| g(f(sK4)) = sK4
| sK5 != sK2
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1664]) ).
cnf(c_372,plain,
( g(f(sK4)) = sK4
| sK5 != sK2
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1665]) ).
cnf(c_1666,plain,
( sK4 != sK3
| f(sK3) != f(sK3)
| f(g(sK2)) = sK2
| f(g(sK2)) = sK2 ),
inference(paramod,[status(thm)],[c_326,c_345]) ).
cnf(c_1667,plain,
( sK4 != sK3
| f(g(sK2)) = sK2
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1666]) ).
cnf(c_384,plain,
( sK4 != sK3
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1667]) ).
cnf(c_1668,plain,
( g(f(sK1)) = sK1
| sK0 = f(sK4)
| f(sK4) != f(sK4)
| g(f(sK1)) = sK1
| f(g(sK2)) = sK2 ),
inference(paramod,[status(thm)],[c_117,c_19]) ).
cnf(c_1669,plain,
( g(f(sK1)) = sK1
| f(sK4) = sK0
| f(sK4) != f(sK4)
| g(f(sK1)) = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1668]) ).
cnf(c_1670,plain,
( g(f(sK1)) = sK1
| f(sK4) = sK0
| g(f(sK1)) = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1669]) ).
cnf(c_392,plain,
( f(sK4) = sK0
| g(f(sK1)) = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1670]) ).
cnf(c_1671,plain,
( g(f(sK1)) = sK1
| g(sK0) = sK4
| f(g(sK2)) = sK2
| g(f(sK1)) = sK1
| f(g(sK2)) = sK2 ),
inference(paramod,[status(thm)],[c_392,c_117]) ).
cnf(c_1672,plain,
( g(f(sK1)) = sK1
| g(sK0) = sK4
| g(f(sK1)) = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1671]) ).
cnf(c_476,plain,
( g(sK0) = sK4
| g(f(sK1)) = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1672]) ).
cnf(c_1673,plain,
( sK1 = sK4
| f(g(sK0)) = sK0
| f(g(sK2)) = sK2
| f(g(sK0)) = sK0 ),
inference(resolve,[status(thm)],[c_118,c_18]) ).
cnf(c_1674,plain,
( sK4 = sK1
| f(g(sK0)) = sK0
| f(g(sK2)) = sK2
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1673]) ).
cnf(c_486,plain,
( sK4 = sK1
| f(g(sK2)) = sK2
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1674]) ).
cnf(c_1675,plain,
( f(g(sK2)) = sK2
| f(g(sK0)) = sK0
| f(g(sK2)) = sK2
| f(g(sK0)) = sK0 ),
inference(resolve,[status(thm)],[c_486,c_208]) ).
cnf(c_1676,plain,
( f(g(sK2)) = sK2
| f(g(sK2)) = sK2
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1675]) ).
cnf(c_490,plain,
( f(g(sK2)) = sK2
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1676]) ).
cnf(c_1677,plain,
( sK1 = g(sK2)
| g(sK2) != g(sK2)
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(paramod,[status(thm)],[c_490,c_18]) ).
cnf(c_1678,plain,
( g(sK2) = sK1
| g(sK2) != g(sK2)
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1677]) ).
cnf(c_1679,plain,
( g(sK2) = sK1
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1678]) ).
cnf(c_495,plain,
( g(sK2) = sK1
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1679]) ).
cnf(c_1680,plain,
( f(sK1) = sK2
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(paramod,[status(thm)],[c_495,c_490]) ).
cnf(c_505,plain,
( f(sK1) = sK2
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1680]) ).
cnf(c_1681,plain,
( sK4 = sK3
| f(g(sK2)) = sK2
| g(f(sK1)) = sK1
| g(f(sK1)) = sK1
| f(g(sK2)) = sK2 ),
inference(paramod,[status(thm)],[c_476,c_128]) ).
cnf(c_1682,plain,
( sK4 = sK3
| f(g(sK2)) = sK2
| g(f(sK1)) = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1681]) ).
cnf(c_516,plain,
( sK4 = sK3
| g(f(sK1)) = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1682]) ).
cnf(c_1683,plain,
( f(g(sK2)) = sK2
| g(f(sK1)) = sK1
| f(g(sK2)) = sK2 ),
inference(resolve,[status(thm)],[c_516,c_384]) ).
cnf(c_524,plain,
( g(f(sK1)) = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1683]) ).
cnf(c_1684,negated_conjecture,
( g(f(sK1)) = sK1
| sK2 = A
| f(g(A)) != A
| g(f(sK1)) = sK1 ),
inference(resolve,[status(thm)],[c_524,c_4]) ).
cnf(c_528,negated_conjecture,
( sK2 = A
| f(g(A)) != A
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1684]) ).
cnf(c_1685,plain,
( sK2 = sK5
| g(f(sK1)) = sK1
| g(f(sK3)) = sK3
| g(f(sK1)) = sK1 ),
inference(resolve,[status(thm)],[c_179,c_528]) ).
cnf(c_1686,plain,
( sK5 = sK2
| g(f(sK1)) = sK1
| g(f(sK3)) = sK3
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1685]) ).
cnf(c_550,plain,
( sK5 = sK2
| g(f(sK3)) = sK3
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1686]) ).
cnf(c_1687,plain,
( sK1 = sK3
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0
| f(g(sK5)) = sK5 ),
inference(resolve,[status(thm)],[c_227,c_18]) ).
cnf(c_1688,plain,
( sK3 = sK1
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1687]) ).
cnf(c_556,plain,
( sK3 = sK1
| f(g(sK0)) = sK0
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1688]) ).
cnf(c_1689,plain,
( g(f(sK3)) = sK3
| g(f(sK3)) = sK3
| g(f(sK1)) = sK1 ),
inference(resolve,[status(thm)],[c_550,c_366]) ).
cnf(c_561,plain,
( g(f(sK3)) = sK3
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1689]) ).
cnf(c_1690,plain,
( g(f(sK1)) = sK1
| sK0 = f(sK3)
| f(sK3) != f(sK3)
| g(f(sK1)) = sK1 ),
inference(paramod,[status(thm)],[c_561,c_19]) ).
cnf(c_1691,plain,
( g(f(sK1)) = sK1
| f(sK3) = sK0
| f(sK3) != f(sK3)
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1690]) ).
cnf(c_1692,plain,
( g(f(sK1)) = sK1
| f(sK3) = sK0
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1691]) ).
cnf(c_567,plain,
( f(sK3) = sK0
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1692]) ).
cnf(c_1693,plain,
( g(sK0) = sK3
| g(f(sK1)) = sK1
| g(f(sK1)) = sK1 ),
inference(paramod,[status(thm)],[c_567,c_561]) ).
cnf(c_578,plain,
( g(sK0) = sK3
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1693]) ).
cnf(c_1694,negated_conjecture,
( g(f(sK4)) = sK4
| f(g(sK5)) = sK5
| f(g(A)) != A
| g(f(sK4)) = sK4
| f(g(sK5)) = sK5 ),
inference(resolve,[status(thm)],[c_229,c_10]) ).
cnf(c_1695,negated_conjecture,
( g(f(sK4)) = sK4
| f(g(A)) != A
| g(f(sK4)) = sK4
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1694]) ).
cnf(c_601,negated_conjecture,
( f(g(A)) != A
| g(f(sK4)) = sK4
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1695]) ).
cnf(c_1696,plain,
( sK2 = sK5
| g(f(sK1)) = sK1
| g(f(sK4)) = sK4
| g(f(sK1)) = sK1 ),
inference(resolve,[status(thm)],[c_229,c_528]) ).
cnf(c_1697,plain,
( sK5 = sK2
| g(f(sK1)) = sK1
| g(f(sK4)) = sK4
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1696]) ).
cnf(c_602,plain,
( sK5 = sK2
| g(f(sK4)) = sK4
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1697]) ).
cnf(c_1698,plain,
( sK1 = sK4
| f(g(sK0)) = sK0
| f(g(sK5)) = sK5
| f(g(sK0)) = sK0 ),
inference(resolve,[status(thm)],[c_279,c_18]) ).
cnf(c_1699,plain,
( sK4 = sK1
| f(g(sK0)) = sK0
| f(g(sK5)) = sK5
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1698]) ).
cnf(c_609,plain,
( sK4 = sK1
| f(g(sK5)) = sK5
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1699]) ).
cnf(c_1700,plain,
( sK4 != sK1
| f(g(sK5)) = sK5
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0
| f(g(sK5)) = sK5 ),
inference(paramod,[status(thm)],[c_556,c_328]) ).
cnf(c_1701,plain,
( sK4 != sK1
| f(g(sK5)) = sK5
| f(g(sK0)) = sK0
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1700]) ).
cnf(c_627,plain,
( sK4 != sK1
| f(g(sK0)) = sK0
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1701]) ).
cnf(c_1702,plain,
( g(f(sK3)) = sK3
| f(g(sK5)) = sK5
| g(f(sK3)) = sK3 ),
inference(resolve,[status(thm)],[c_339,c_561]) ).
cnf(c_663,plain,
( f(g(sK5)) = sK5
| g(f(sK3)) = sK3 ),
inference(copy,[status(thm)],[c_1702]) ).
cnf(c_1703,negated_conjecture,
( sK4 != sK3
| f(g(sK5)) = sK5
| f(g(A)) != A
| f(g(sK5)) = sK5 ),
inference(resolve,[status(thm)],[c_663,c_11]) ).
cnf(c_666,negated_conjecture,
( sK4 != sK3
| f(g(A)) != A
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1703]) ).
cnf(c_1704,plain,
( g(f(sK4)) = sK4
| g(f(sK1)) = sK1
| g(f(sK4)) = sK4
| g(f(sK1)) = sK1 ),
inference(resolve,[status(thm)],[c_602,c_368]) ).
cnf(c_1705,plain,
( g(f(sK4)) = sK4
| g(f(sK4)) = sK4
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1704]) ).
cnf(c_670,plain,
( g(f(sK4)) = sK4
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1705]) ).
cnf(c_1706,negated_conjecture,
( g(f(sK4)) = sK4
| sK5 != sK2
| f(g(A)) != A
| g(f(sK4)) = sK4 ),
inference(resolve,[status(thm)],[c_670,c_13]) ).
cnf(c_676,negated_conjecture,
( sK5 != sK2
| f(g(A)) != A
| g(f(sK4)) = sK4 ),
inference(copy,[status(thm)],[c_1706]) ).
cnf(c_1707,plain,
( g(f(sK1)) = sK1
| sK0 = f(sK4)
| f(sK4) != f(sK4)
| g(f(sK1)) = sK1 ),
inference(paramod,[status(thm)],[c_670,c_19]) ).
cnf(c_1708,plain,
( g(f(sK1)) = sK1
| f(sK4) = sK0
| f(sK4) != f(sK4)
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1707]) ).
cnf(c_1709,plain,
( g(f(sK1)) = sK1
| f(sK4) = sK0
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1708]) ).
cnf(c_679,plain,
( f(sK4) = sK0
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1709]) ).
cnf(c_1710,plain,
( g(sK0) = sK4
| g(f(sK1)) = sK1
| g(f(sK1)) = sK1 ),
inference(paramod,[status(thm)],[c_679,c_670]) ).
cnf(c_684,plain,
( g(sK0) = sK4
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1710]) ).
cnf(c_1711,plain,
( f(g(sK2)) = sK2
| g(f(sK4)) = sK4
| f(g(sK2)) = sK2 ),
inference(resolve,[status(thm)],[c_346,c_490]) ).
cnf(c_703,plain,
( g(f(sK4)) = sK4
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1711]) ).
cnf(c_1712,plain,
( sK4 = sK3
| g(f(sK1)) = sK1
| g(f(sK1)) = sK1 ),
inference(paramod,[status(thm)],[c_684,c_578]) ).
cnf(c_711,plain,
( sK4 = sK3
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1712]) ).
cnf(c_1713,plain,
( f(g(sK5)) = sK5
| g(f(sK1)) = sK1
| g(f(sK1)) = sK1 ),
inference(resolve,[status(thm)],[c_711,c_281]) ).
cnf(c_715,plain,
( f(g(sK5)) = sK5
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1713]) ).
cnf(c_1714,plain,
( sK5 != sK2
| g(f(sK1)) = sK1
| g(f(sK1)) = sK1 ),
inference(resolve,[status(thm)],[c_711,c_56]) ).
cnf(c_716,plain,
( sK5 != sK2
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1714]) ).
cnf(c_1715,plain,
( sK2 = sK5
| g(f(sK1)) = sK1
| g(f(sK1)) = sK1 ),
inference(resolve,[status(thm)],[c_715,c_528]) ).
cnf(c_1716,plain,
( sK5 = sK2
| g(f(sK1)) = sK1
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1715]) ).
cnf(c_727,plain,
( sK5 = sK2
| g(f(sK1)) = sK1 ),
inference(copy,[status(thm)],[c_1716]) ).
cnf(c_1717,plain,
( g(f(sK1)) = sK1
| g(f(sK1)) = sK1 ),
inference(resolve,[status(thm)],[c_727,c_716]) ).
cnf(c_733,plain,
g(f(sK1)) = sK1,
inference(copy,[status(thm)],[c_1717]) ).
cnf(c_736,plain,
( sK4 != sK3
| sK5 != sK2
| f(g(A)) != A ),
inference(resolve,[status(thm)],[c_733,c_14]) ).
cnf(c_737,plain,
( sK1 = C
| g(f(C)) != C
| B = A
| f(g(B)) != B
| f(g(A)) != A ),
inference(resolve,[status(thm)],[c_733,c_5]) ).
cnf(c_1718,plain,
( sK4 != sK3
| sK5 != sK2
| f(sK1) != f(sK1) ),
inference(paramod,[status(thm)],[c_733,c_736]) ).
cnf(c_754,plain,
( sK4 != sK3
| sK5 != sK2 ),
inference(copy,[status(thm)],[c_1718]) ).
cnf(c_1719,plain,
( f(g(sK5)) = sK5
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0
| f(g(sK5)) = sK5 ),
inference(resolve,[status(thm)],[c_627,c_609]) ).
cnf(c_1720,plain,
( f(g(sK5)) = sK5
| f(g(sK0)) = sK0
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1719]) ).
cnf(c_788,plain,
( f(g(sK0)) = sK0
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1720]) ).
cnf(c_1721,plain,
( sK1 = g(sK5)
| g(sK5) != g(sK5)
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(paramod,[status(thm)],[c_788,c_18]) ).
cnf(c_1722,plain,
( g(sK5) = sK1
| g(sK5) != g(sK5)
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1721]) ).
cnf(c_1723,plain,
( g(sK5) = sK1
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1722]) ).
cnf(c_791,plain,
( g(sK5) = sK1
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1723]) ).
cnf(c_1724,plain,
( f(g(sK0)) = sK0
| f(sK1) = sK5
| f(g(sK0)) = sK0 ),
inference(paramod,[status(thm)],[c_791,c_788]) ).
cnf(c_796,plain,
( f(sK1) = sK5
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1724]) ).
cnf(c_1725,plain,
( sK5 = sK2
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(paramod,[status(thm)],[c_796,c_505]) ).
cnf(c_799,plain,
( sK5 = sK2
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1725]) ).
cnf(c_803,plain,
( sK4 != sK3
| f(g(sK0)) = sK0 ),
inference(resolve,[status(thm)],[c_799,c_754]) ).
cnf(c_1726,plain,
( g(f(sK4)) = sK4
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(resolve,[status(thm)],[c_799,c_372]) ).
cnf(c_804,plain,
( g(f(sK4)) = sK4
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1726]) ).
cnf(c_805,plain,
( g(f(sK3)) = sK3
| f(g(sK0)) = sK0 ),
inference(resolve,[status(thm)],[c_799,c_366]) ).
cnf(c_1727,plain,
( f(g(sK5)) = sK5
| g(f(sK4)) = sK4
| f(g(sK5)) = sK5 ),
inference(resolve,[status(thm)],[c_601,c_788]) ).
cnf(c_812,plain,
( g(f(sK4)) = sK4
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1727]) ).
cnf(c_1728,plain,
( sK1 = sK4
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(resolve,[status(thm)],[c_804,c_18]) ).
cnf(c_1729,plain,
( sK4 = sK1
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1728]) ).
cnf(c_818,plain,
( sK4 = sK1
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1729]) ).
cnf(c_823,plain,
( C = B
| g(f(C)) != C
| g(f(B)) != B
| sK0 = A
| f(g(A)) != A
| sK4 = sK1 ),
inference(resolve,[status(thm)],[c_818,c_5]) ).
cnf(c_1730,plain,
( sK1 != sK3
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(paramod,[status(thm)],[c_818,c_803]) ).
cnf(c_1731,plain,
( sK3 != sK1
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1730]) ).
cnf(c_825,plain,
( sK3 != sK1
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1731]) ).
cnf(c_1732,plain,
( g(f(sK4)) != sK4
| g(f(sK1)) != sK1
| sK0 = A
| f(g(A)) != A
| sK4 = sK1 ),
inference(factor,[status(thm)],[c_823]) ).
cnf(c_1733,plain,
( g(f(sK4)) != sK4
| sK1 != sK1
| sK0 = A
| f(g(A)) != A
| sK4 = sK1 ),
inference(paramod,[status(thm)],[c_733,c_1732]) ).
cnf(c_827,plain,
( g(f(sK4)) != sK4
| sK0 = A
| f(g(A)) != A
| sK4 = sK1 ),
inference(copy,[status(thm)],[c_1733]) ).
cnf(c_1734,plain,
( sK1 = sK3
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(resolve,[status(thm)],[c_805,c_18]) ).
cnf(c_1735,plain,
( sK3 = sK1
| f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1734]) ).
cnf(c_842,plain,
( sK3 = sK1
| f(g(sK0)) = sK0 ),
inference(copy,[status(thm)],[c_1735]) ).
cnf(c_1736,plain,
( f(g(sK5)) = sK5
| sK4 != sK3
| f(g(sK5)) = sK5 ),
inference(resolve,[status(thm)],[c_666,c_788]) ).
cnf(c_865,plain,
( sK4 != sK3
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1736]) ).
cnf(c_867,plain,
( C = B
| g(f(C)) != C
| g(f(B)) != B
| sK0 = A
| f(g(A)) != A
| sK3 = sK1 ),
inference(resolve,[status(thm)],[c_842,c_5]) ).
cnf(c_1737,plain,
( f(g(sK0)) = sK0
| f(g(sK0)) = sK0 ),
inference(resolve,[status(thm)],[c_842,c_825]) ).
cnf(c_868,plain,
f(g(sK0)) = sK0,
inference(copy,[status(thm)],[c_1737]) ).
cnf(c_1738,plain,
( g(f(sK3)) != sK3
| g(f(sK1)) != sK1
| sK0 = A
| f(g(A)) != A
| sK3 = sK1 ),
inference(factor,[status(thm)],[c_867]) ).
cnf(c_1739,plain,
( g(f(sK3)) != sK3
| sK1 != sK1
| sK0 = A
| f(g(A)) != A
| sK3 = sK1 ),
inference(paramod,[status(thm)],[c_733,c_1738]) ).
cnf(c_869,plain,
( g(f(sK3)) != sK3
| sK0 = A
| f(g(A)) != A
| sK3 = sK1 ),
inference(copy,[status(thm)],[c_1739]) ).
cnf(c_871,plain,
( C = B
| g(f(C)) != C
| g(f(B)) != B
| sK0 = A
| f(g(A)) != A ),
inference(resolve,[status(thm)],[c_868,c_5]) ).
cnf(c_876,plain,
( sK5 != sK2
| g(f(sK4)) = sK4 ),
inference(resolve,[status(thm)],[c_676,c_868]) ).
cnf(c_881,plain,
( f(g(sK5)) = sK5
| sK0 = A
| f(g(A)) != A
| sK4 = sK1 ),
inference(resolve,[status(thm)],[c_827,c_812]) ).
cnf(c_882,plain,
( f(g(sK2)) = sK2
| sK0 = A
| f(g(A)) != A
| sK4 = sK1 ),
inference(resolve,[status(thm)],[c_827,c_703]) ).
cnf(c_1740,plain,
( g(f(sK4)) != sK4
| sK0 = f(sK1)
| f(sK1) != f(sK1)
| sK4 = sK1 ),
inference(paramod,[status(thm)],[c_733,c_827]) ).
cnf(c_1741,plain,
( g(f(sK4)) != sK4
| f(sK1) = sK0
| f(sK1) != f(sK1)
| sK4 = sK1 ),
inference(copy,[status(thm)],[c_1740]) ).
cnf(c_886,plain,
( g(f(sK4)) != sK4
| f(sK1) = sK0
| sK4 = sK1 ),
inference(copy,[status(thm)],[c_1741]) ).
cnf(c_888,plain,
( f(g(sK5)) = sK5
| f(sK1) = sK0
| sK4 = sK1 ),
inference(resolve,[status(thm)],[c_886,c_812]) ).
cnf(c_1742,plain,
( sK1 != sK3
| f(g(sK5)) = sK5
| f(g(sK5)) = sK5
| f(sK1) = sK0 ),
inference(paramod,[status(thm)],[c_888,c_865]) ).
cnf(c_1743,plain,
( sK3 != sK1
| f(g(sK5)) = sK5
| f(g(sK5)) = sK5
| f(sK1) = sK0 ),
inference(copy,[status(thm)],[c_1742]) ).
cnf(c_894,plain,
( sK3 != sK1
| f(g(sK5)) = sK5
| f(sK1) = sK0 ),
inference(copy,[status(thm)],[c_1743]) ).
cnf(c_939,plain,
( f(g(sK5)) = sK5
| sK0 = A
| f(g(A)) != A
| sK3 = sK1 ),
inference(resolve,[status(thm)],[c_869,c_663]) ).
cnf(c_940,plain,
( f(g(sK2)) = sK2
| sK0 = A
| f(g(A)) != A
| sK3 = sK1 ),
inference(resolve,[status(thm)],[c_869,c_326]) ).
cnf(c_1744,plain,
( g(f(sK3)) != sK3
| sK0 = f(sK1)
| f(sK1) != f(sK1)
| sK3 = sK1 ),
inference(paramod,[status(thm)],[c_733,c_869]) ).
cnf(c_1745,plain,
( g(f(sK3)) != sK3
| f(sK1) = sK0
| f(sK1) != f(sK1)
| sK3 = sK1 ),
inference(copy,[status(thm)],[c_1744]) ).
cnf(c_944,plain,
( g(f(sK3)) != sK3
| f(sK1) = sK0
| sK3 = sK1 ),
inference(copy,[status(thm)],[c_1745]) ).
cnf(c_946,plain,
( f(g(sK5)) = sK5
| f(sK1) = sK0
| sK3 = sK1 ),
inference(resolve,[status(thm)],[c_944,c_663]) ).
cnf(c_1746,plain,
( sK1 = B
| g(f(B)) != B
| A = sK0
| f(g(A)) != A ),
inference(resolve,[status(thm)],[c_737,c_868]) ).
cnf(c_952,plain,
( sK1 = B
| g(f(B)) != B
| sK0 = A
| f(g(A)) != A ),
inference(copy,[status(thm)],[c_1746]) ).
cnf(c_1747,plain,
( f(g(sK5)) = sK5
| f(sK1) = sK0
| f(g(sK5)) = sK5
| f(sK1) = sK0 ),
inference(resolve,[status(thm)],[c_946,c_894]) ).
cnf(c_1748,plain,
( f(g(sK5)) = sK5
| f(g(sK5)) = sK5
| f(sK1) = sK0 ),
inference(copy,[status(thm)],[c_1747]) ).
cnf(c_1043,plain,
( f(g(sK5)) = sK5
| f(sK1) = sK0 ),
inference(copy,[status(thm)],[c_1748]) ).
cnf(c_1054,plain,
( g(sK0) = sK1
| f(g(sK5)) = sK5 ),
inference(paramod,[status(thm)],[c_1043,c_733]) ).
cnf(c_1749,plain,
( sK1 = g(sK5)
| g(sK5) != g(sK5)
| B = A
| f(g(B)) != B
| f(g(A)) != A
| f(sK1) = sK0 ),
inference(paramod,[status(thm)],[c_1043,c_737]) ).
cnf(c_1750,plain,
( g(sK5) = sK1
| g(sK5) != g(sK5)
| B = A
| f(g(B)) != B
| f(g(A)) != A
| f(sK1) = sK0 ),
inference(copy,[status(thm)],[c_1749]) ).
cnf(c_1056,plain,
( g(sK5) = sK1
| B = A
| f(g(B)) != B
| f(g(A)) != A
| f(sK1) = sK0 ),
inference(copy,[status(thm)],[c_1750]) ).
cnf(c_1751,plain,
( g(sK5) = sK1
| f(g(f(sK1))) != f(sK1)
| f(g(sK0)) != sK0
| f(sK1) = sK0 ),
inference(factor,[status(thm)],[c_1056]) ).
cnf(c_1752,plain,
( g(sK5) = sK1
| f(g(f(sK1))) != f(sK1)
| sK0 != sK0
| f(sK1) = sK0 ),
inference(paramod,[status(thm)],[c_868,c_1751]) ).
cnf(c_1753,plain,
( g(sK5) = sK1
| f(sK1) != f(sK1)
| sK0 != sK0
| f(sK1) = sK0 ),
inference(paramod,[status(thm)],[c_733,c_1752]) ).
cnf(c_1754,plain,
( g(sK5) = sK1
| f(sK1) != f(sK1)
| f(sK1) = sK0 ),
inference(copy,[status(thm)],[c_1753]) ).
cnf(c_1058,plain,
( g(sK5) = sK1
| f(sK1) = sK0 ),
inference(copy,[status(thm)],[c_1754]) ).
cnf(c_1061,plain,
( g(sK0) = sK1
| g(sK5) = sK1 ),
inference(paramod,[status(thm)],[c_1058,c_733]) ).
cnf(c_1755,plain,
( g(sK0) = sK1
| B = A
| g(f(B)) != B
| g(f(A)) != A
| sK0 = sK5 ),
inference(resolve,[status(thm)],[c_871,c_1054]) ).
cnf(c_1098,plain,
( g(sK0) = sK1
| B = A
| g(f(B)) != B
| g(f(A)) != A
| sK5 = sK0 ),
inference(copy,[status(thm)],[c_1755]) ).
cnf(c_1756,plain,
( g(sK0) = sK1
| g(f(g(sK0))) != g(sK0)
| g(f(sK1)) != sK1
| sK5 = sK0 ),
inference(factor,[status(thm)],[c_1098]) ).
cnf(c_1757,plain,
( g(sK0) = sK1
| g(f(g(sK0))) != g(sK0)
| sK1 != sK1
| sK5 = sK0 ),
inference(paramod,[status(thm)],[c_733,c_1756]) ).
cnf(c_1758,plain,
( g(sK0) = sK1
| g(sK0) != g(sK0)
| sK1 != sK1
| sK5 = sK0 ),
inference(paramod,[status(thm)],[c_868,c_1757]) ).
cnf(c_1759,plain,
( g(sK0) = sK1
| g(sK0) != g(sK0)
| sK5 = sK0 ),
inference(copy,[status(thm)],[c_1758]) ).
cnf(c_1119,plain,
( g(sK0) = sK1
| sK5 = sK0 ),
inference(copy,[status(thm)],[c_1759]) ).
cnf(c_1760,plain,
( g(sK0) = sK1
| g(sK0) = sK1
| g(sK0) = sK1 ),
inference(paramod,[status(thm)],[c_1119,c_1061]) ).
cnf(c_1761,plain,
( g(sK0) = sK1
| g(sK0) = sK1 ),
inference(copy,[status(thm)],[c_1760]) ).
cnf(c_1131,plain,
g(sK0) = sK1,
inference(copy,[status(thm)],[c_1761]) ).
cnf(c_1132,plain,
f(sK1) = sK0,
inference(paramod,[status(thm)],[c_1131,c_868]) ).
cnf(c_1762,plain,
( f(g(sK5)) = sK5
| sK0 = f(sK4)
| f(sK4) != f(sK4)
| sK4 = sK1
| f(g(sK5)) = sK5 ),
inference(paramod,[status(thm)],[c_812,c_881]) ).
cnf(c_1763,plain,
( f(g(sK5)) = sK5
| f(sK4) = sK0
| f(sK4) != f(sK4)
| sK4 = sK1
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1762]) ).
cnf(c_1764,plain,
( f(g(sK5)) = sK5
| f(sK4) = sK0
| sK4 = sK1
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1763]) ).
cnf(c_1136,plain,
( f(sK4) = sK0
| sK4 = sK1
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1764]) ).
cnf(c_1765,plain,
( g(sK0) = sK4
| f(g(sK5)) = sK5
| sK4 = sK1
| f(g(sK5)) = sK5 ),
inference(paramod,[status(thm)],[c_1136,c_812]) ).
cnf(c_1766,plain,
( sK1 = sK4
| f(g(sK5)) = sK5
| sK4 = sK1
| f(g(sK5)) = sK5 ),
inference(paramod,[status(thm)],[c_1131,c_1765]) ).
cnf(c_1767,plain,
( sK4 = sK1
| f(g(sK5)) = sK5
| sK4 = sK1
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1766]) ).
cnf(c_1768,plain,
( sK4 = sK1
| sK4 = sK1
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1767]) ).
cnf(c_1190,plain,
( sK4 = sK1
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1768]) ).
cnf(c_1769,plain,
( sK1 != sK3
| f(g(sK5)) = sK5
| f(g(sK5)) = sK5 ),
inference(paramod,[status(thm)],[c_1190,c_865]) ).
cnf(c_1770,plain,
( sK3 != sK1
| f(g(sK5)) = sK5
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1769]) ).
cnf(c_1209,plain,
( sK3 != sK1
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1770]) ).
cnf(c_1771,plain,
( f(g(sK2)) = sK2
| sK0 = f(sK4)
| f(sK4) != f(sK4)
| sK4 = sK1
| f(g(sK2)) = sK2 ),
inference(paramod,[status(thm)],[c_703,c_882]) ).
cnf(c_1772,plain,
( f(g(sK2)) = sK2
| f(sK4) = sK0
| f(sK4) != f(sK4)
| sK4 = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1771]) ).
cnf(c_1773,plain,
( f(g(sK2)) = sK2
| f(sK4) = sK0
| sK4 = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1772]) ).
cnf(c_1251,plain,
( f(sK4) = sK0
| sK4 = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1773]) ).
cnf(c_1774,plain,
( g(sK0) = sK4
| f(g(sK2)) = sK2
| sK4 = sK1
| f(g(sK2)) = sK2 ),
inference(paramod,[status(thm)],[c_1251,c_703]) ).
cnf(c_1775,plain,
( sK1 = sK4
| f(g(sK2)) = sK2
| sK4 = sK1
| f(g(sK2)) = sK2 ),
inference(paramod,[status(thm)],[c_1131,c_1774]) ).
cnf(c_1776,plain,
( sK4 = sK1
| f(g(sK2)) = sK2
| sK4 = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1775]) ).
cnf(c_1777,plain,
( sK4 = sK1
| sK4 = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1776]) ).
cnf(c_1297,plain,
( sK4 = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1777]) ).
cnf(c_1312,plain,
( C = B
| g(f(C)) != C
| g(f(B)) != B
| sK2 = A
| f(g(A)) != A
| sK4 = sK1 ),
inference(resolve,[status(thm)],[c_1297,c_5]) ).
cnf(c_1778,plain,
( sK1 != sK3
| f(g(sK2)) = sK2
| f(g(sK2)) = sK2 ),
inference(paramod,[status(thm)],[c_1297,c_384]) ).
cnf(c_1779,plain,
( sK3 != sK1
| f(g(sK2)) = sK2
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1778]) ).
cnf(c_1313,plain,
( sK3 != sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1779]) ).
cnf(c_1780,plain,
( g(f(sK4)) != sK4
| g(f(sK1)) != sK1
| sK2 = A
| f(g(A)) != A
| sK4 = sK1 ),
inference(factor,[status(thm)],[c_1312]) ).
cnf(c_1781,plain,
( g(f(sK4)) != sK4
| g(sK0) != sK1
| sK2 = A
| f(g(A)) != A
| sK4 = sK1 ),
inference(paramod,[status(thm)],[c_1132,c_1780]) ).
cnf(c_1782,plain,
( g(f(sK4)) != sK4
| sK1 != sK1
| sK2 = A
| f(g(A)) != A
| sK4 = sK1 ),
inference(paramod,[status(thm)],[c_1131,c_1781]) ).
cnf(c_1325,plain,
( g(f(sK4)) != sK4
| sK2 = A
| f(g(A)) != A
| sK4 = sK1 ),
inference(copy,[status(thm)],[c_1782]) ).
cnf(c_1783,plain,
( f(g(sK5)) = sK5
| sK0 = f(sK3)
| f(sK3) != f(sK3)
| sK3 = sK1
| f(g(sK5)) = sK5 ),
inference(paramod,[status(thm)],[c_663,c_939]) ).
cnf(c_1784,plain,
( f(g(sK5)) = sK5
| f(sK3) = sK0
| f(sK3) != f(sK3)
| sK3 = sK1
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1783]) ).
cnf(c_1785,plain,
( f(g(sK5)) = sK5
| f(sK3) = sK0
| sK3 = sK1
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1784]) ).
cnf(c_1385,plain,
( f(sK3) = sK0
| sK3 = sK1
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1785]) ).
cnf(c_1786,plain,
( f(g(sK2)) = sK2
| sK0 = f(sK3)
| f(sK3) != f(sK3)
| sK3 = sK1
| f(g(sK2)) = sK2 ),
inference(paramod,[status(thm)],[c_326,c_940]) ).
cnf(c_1787,plain,
( f(g(sK2)) = sK2
| f(sK3) = sK0
| f(sK3) != f(sK3)
| sK3 = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1786]) ).
cnf(c_1788,plain,
( f(g(sK2)) = sK2
| f(sK3) = sK0
| sK3 = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1787]) ).
cnf(c_1388,plain,
( f(sK3) = sK0
| sK3 = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1788]) ).
cnf(c_1789,plain,
( f(g(sK5)) = sK5
| g(sK0) = sK3
| sK3 = sK1
| f(g(sK5)) = sK5 ),
inference(paramod,[status(thm)],[c_1385,c_663]) ).
cnf(c_1790,plain,
( f(g(sK5)) = sK5
| sK1 = sK3
| sK3 = sK1
| f(g(sK5)) = sK5 ),
inference(paramod,[status(thm)],[c_1131,c_1789]) ).
cnf(c_1791,plain,
( f(g(sK5)) = sK5
| sK3 = sK1
| sK3 = sK1
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1790]) ).
cnf(c_1792,plain,
( f(g(sK5)) = sK5
| sK3 = sK1
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1791]) ).
cnf(c_1401,plain,
( sK3 = sK1
| f(g(sK5)) = sK5 ),
inference(copy,[status(thm)],[c_1792]) ).
cnf(c_1793,plain,
( f(g(sK5)) = sK5
| f(g(sK5)) = sK5 ),
inference(resolve,[status(thm)],[c_1401,c_1209]) ).
cnf(c_1420,plain,
f(g(sK5)) = sK5,
inference(copy,[status(thm)],[c_1793]) ).
cnf(c_1794,plain,
( sK1 = A
| g(f(A)) != A
| sK0 = sK5 ),
inference(resolve,[status(thm)],[c_952,c_1420]) ).
cnf(c_1457,plain,
( sK1 = A
| g(f(A)) != A
| sK5 = sK0 ),
inference(copy,[status(thm)],[c_1794]) ).
cnf(c_1795,plain,
( sK1 = g(sK5)
| g(sK5) != g(sK5)
| sK5 = sK0 ),
inference(paramod,[status(thm)],[c_1420,c_1457]) ).
cnf(c_1796,plain,
( g(sK5) = sK1
| g(sK5) != g(sK5)
| sK5 = sK0 ),
inference(copy,[status(thm)],[c_1795]) ).
cnf(c_1513,plain,
( g(sK5) = sK1
| sK5 = sK0 ),
inference(copy,[status(thm)],[c_1796]) ).
cnf(c_1797,plain,
( f(sK1) = sK5
| sK5 = sK0 ),
inference(paramod,[status(thm)],[c_1513,c_1420]) ).
cnf(c_1798,plain,
( sK0 = sK5
| sK5 = sK0 ),
inference(paramod,[status(thm)],[c_1132,c_1797]) ).
cnf(c_1799,plain,
( sK5 = sK0
| sK5 = sK0 ),
inference(copy,[status(thm)],[c_1798]) ).
cnf(c_1521,plain,
sK5 = sK0,
inference(copy,[status(thm)],[c_1799]) ).
cnf(c_1800,plain,
( sK0 != sK2
| g(f(sK4)) = sK4 ),
inference(paramod,[status(thm)],[c_1521,c_876]) ).
cnf(c_1522,plain,
( sK2 != sK0
| g(f(sK4)) = sK4 ),
inference(copy,[status(thm)],[c_1800]) ).
cnf(c_1801,plain,
( sK4 != sK3
| sK0 != sK2 ),
inference(paramod,[status(thm)],[c_1521,c_754]) ).
cnf(c_1523,plain,
( sK4 != sK3
| sK2 != sK0 ),
inference(copy,[status(thm)],[c_1801]) ).
cnf(c_1802,plain,
( sK0 != sK2
| g(f(sK3)) = sK3 ),
inference(paramod,[status(thm)],[c_1521,c_366]) ).
cnf(c_1524,plain,
( sK2 != sK0
| g(f(sK3)) = sK3 ),
inference(copy,[status(thm)],[c_1802]) ).
cnf(c_1803,plain,
( g(sK0) = sK3
| f(g(sK2)) = sK2
| sK3 = sK1
| f(g(sK2)) = sK2 ),
inference(paramod,[status(thm)],[c_1388,c_326]) ).
cnf(c_1804,plain,
( sK1 = sK3
| f(g(sK2)) = sK2
| sK3 = sK1
| f(g(sK2)) = sK2 ),
inference(paramod,[status(thm)],[c_1131,c_1803]) ).
cnf(c_1805,plain,
( sK3 = sK1
| f(g(sK2)) = sK2
| sK3 = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1804]) ).
cnf(c_1806,plain,
( sK3 = sK1
| sK3 = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1805]) ).
cnf(c_1533,plain,
( sK3 = sK1
| f(g(sK2)) = sK2 ),
inference(copy,[status(thm)],[c_1806]) ).
cnf(c_1807,plain,
( f(g(sK2)) = sK2
| f(g(sK2)) = sK2 ),
inference(resolve,[status(thm)],[c_1533,c_1313]) ).
cnf(c_1547,plain,
f(g(sK2)) = sK2,
inference(copy,[status(thm)],[c_1807]) ).
cnf(c_1808,plain,
( sK1 = A
| g(f(A)) != A
| sK0 = sK2 ),
inference(resolve,[status(thm)],[c_1547,c_952]) ).
cnf(c_1555,plain,
( sK1 = A
| g(f(A)) != A
| sK2 = sK0 ),
inference(copy,[status(thm)],[c_1808]) ).
cnf(c_1809,plain,
( sK1 = g(sK2)
| g(sK2) != g(sK2)
| sK2 = sK0 ),
inference(paramod,[status(thm)],[c_1547,c_1555]) ).
cnf(c_1810,plain,
( g(sK2) = sK1
| g(sK2) != g(sK2)
| sK2 = sK0 ),
inference(copy,[status(thm)],[c_1809]) ).
cnf(c_1568,plain,
( g(sK2) = sK1
| sK2 = sK0 ),
inference(copy,[status(thm)],[c_1810]) ).
cnf(c_1811,plain,
( f(sK1) = sK2
| sK2 = sK0 ),
inference(paramod,[status(thm)],[c_1568,c_1547]) ).
cnf(c_1812,plain,
( sK0 = sK2
| sK2 = sK0 ),
inference(paramod,[status(thm)],[c_1132,c_1811]) ).
cnf(c_1813,plain,
( sK2 = sK0
| sK2 = sK0 ),
inference(copy,[status(thm)],[c_1812]) ).
cnf(c_1572,plain,
sK2 = sK0,
inference(copy,[status(thm)],[c_1813]) ).
cnf(c_1814,plain,
( sK0 != sK0
| g(f(sK3)) = sK3 ),
inference(paramod,[status(thm)],[c_1572,c_1524]) ).
cnf(c_1573,plain,
g(f(sK3)) = sK3,
inference(copy,[status(thm)],[c_1814]) ).
cnf(c_1815,plain,
( sK4 != sK3
| sK0 != sK0 ),
inference(paramod,[status(thm)],[c_1572,c_1523]) ).
cnf(c_1574,plain,
sK4 != sK3,
inference(copy,[status(thm)],[c_1815]) ).
cnf(c_1816,plain,
( sK0 != sK0
| g(f(sK4)) = sK4 ),
inference(paramod,[status(thm)],[c_1572,c_1522]) ).
cnf(c_1575,plain,
g(f(sK4)) = sK4,
inference(copy,[status(thm)],[c_1816]) ).
cnf(c_1817,plain,
( g(f(sK4)) != sK4
| sK0 = A
| f(g(A)) != A
| sK4 = sK1 ),
inference(paramod,[status(thm)],[c_1572,c_1325]) ).
cnf(c_1818,plain,
( sK4 != sK4
| sK0 = A
| f(g(A)) != A
| sK4 = sK1 ),
inference(paramod,[status(thm)],[c_1575,c_1817]) ).
cnf(c_1576,plain,
( sK0 = A
| f(g(A)) != A
| sK4 = sK1 ),
inference(copy,[status(thm)],[c_1818]) ).
cnf(c_1819,plain,
( sK3 != sK3
| sK0 = A
| f(g(A)) != A
| sK3 = sK1 ),
inference(paramod,[status(thm)],[c_1573,c_869]) ).
cnf(c_1577,plain,
( sK0 = A
| f(g(A)) != A
| sK3 = sK1 ),
inference(copy,[status(thm)],[c_1819]) ).
cnf(c_1820,plain,
( sK0 = f(sK4)
| f(sK4) != f(sK4)
| sK4 = sK1 ),
inference(paramod,[status(thm)],[c_1575,c_1576]) ).
cnf(c_1821,plain,
( f(sK4) = sK0
| f(sK4) != f(sK4)
| sK4 = sK1 ),
inference(copy,[status(thm)],[c_1820]) ).
cnf(c_1603,plain,
( f(sK4) = sK0
| sK4 = sK1 ),
inference(copy,[status(thm)],[c_1821]) ).
cnf(c_1822,plain,
( g(sK0) = sK4
| sK4 = sK1 ),
inference(paramod,[status(thm)],[c_1603,c_1575]) ).
cnf(c_1823,plain,
( sK1 = sK4
| sK4 = sK1 ),
inference(paramod,[status(thm)],[c_1131,c_1822]) ).
cnf(c_1824,plain,
( sK4 = sK1
| sK4 = sK1 ),
inference(copy,[status(thm)],[c_1823]) ).
cnf(c_1607,plain,
sK4 = sK1,
inference(copy,[status(thm)],[c_1824]) ).
cnf(c_1825,plain,
sK1 != sK3,
inference(paramod,[status(thm)],[c_1607,c_1574]) ).
cnf(c_1608,plain,
sK3 != sK1,
inference(copy,[status(thm)],[c_1825]) ).
cnf(c_1611,plain,
( sK0 = A
| f(g(A)) != A ),
inference(resolve,[status(thm)],[c_1608,c_1577]) ).
cnf(c_1826,plain,
( sK0 = f(sK3)
| f(sK3) != f(sK3) ),
inference(paramod,[status(thm)],[c_1573,c_1611]) ).
cnf(c_1827,plain,
( f(sK3) = sK0
| f(sK3) != f(sK3) ),
inference(copy,[status(thm)],[c_1826]) ).
cnf(c_1613,plain,
f(sK3) = sK0,
inference(copy,[status(thm)],[c_1827]) ).
cnf(c_1828,plain,
g(sK0) = sK3,
inference(paramod,[status(thm)],[c_1613,c_1573]) ).
cnf(c_1829,plain,
sK1 = sK3,
inference(paramod,[status(thm)],[c_1131,c_1828]) ).
cnf(c_1830,plain,
sK3 = sK1,
inference(copy,[status(thm)],[c_1829]) ).
cnf(c_1614,plain,
$false,
inference(resolve,[status(thm)],[c_1608,c_1830]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN551+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n007.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 26 18:11:24 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.35 % Process 180633 was started by sandbox on n007,
% 0.09/0.35 % Sat Sep 26 18:11:24 2026
% 0.09/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.36
% 0.09/0.36 % From the command line: assign(max_seconds, 300).
% 8.91/1.52
% 8.91/1.52 % SZS status Theorem for theBenchmark
% 8.91/1.52
% 8.91/1.52 % Proof 1 at 0.82 (+ 0.30) seconds.
% 8.91/1.52 % Length of proof is 161.
% 8.91/1.52 % Level of proof is 41.
% 8.91/1.52 % Maximum clause weight is 32.000.
% 8.91/1.52 % Given clauses 337.
% 8.91/1.52
% 8.91/1.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------