%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN015-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:36:16 AM UTC 2026
% Result : Unsatisfiable 0.15s 0.45s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 151
% Number of leaves : 16
% Syntax : Number of formulae : 262 ( 14 unt; 0 def)
% Number of atoms : 1142 ( 909 equ)
% Maximal formula atoms : 9 ( 4 avg)
% Number of connectives : 1020 ( 140 ~; 880 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-1 aty)
% Number of variables : 71 ( 0 sgn 17 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(c_1,axiom,
m != n,
file('theBenchmark.p',c_1) ).
cnf(c_1_001,plain,
m != n,
inference(clausify,[status(thm)],[c_1]) ).
cnf(c_2,plain,
n != m,
inference(copy,[status(thm)],[c_1]) ).
fof(c_2_002,axiom,
! [VAR_0] :
( element(VAR_0,j)
| VAR_0 != k
| VAR_0 = j ),
file('theBenchmark.p',c_2) ).
cnf(c_3,plain,
( element(A,j)
| A != k
| A = j ),
inference(clausify,[status(thm)],[c_2]) ).
cnf(c_363,plain,
( element(A,j)
| A != k
| j = A ),
inference(copy,[status(thm)],[c_3]) ).
cnf(c_4,plain,
( element(A,j)
| k != A
| j = A ),
inference(copy,[status(thm)],[c_363]) ).
fof(c_3_003,axiom,
! [VAR_0] :
( ~ element(VAR_0,j)
| VAR_0 = k
| VAR_0 = j ),
file('theBenchmark.p',c_3) ).
cnf(c_5,plain,
( ~ element(A,j)
| A = k
| A = j ),
inference(clausify,[status(thm)],[c_3]) ).
cnf(c_364,plain,
( ~ element(A,j)
| A = k
| j = A ),
inference(copy,[status(thm)],[c_5]) ).
cnf(c_6,plain,
( ~ element(A,j)
| k = A
| j = A ),
inference(copy,[status(thm)],[c_364]) ).
fof(c_4_004,axiom,
! [VAR_0] :
( f(VAR_0) != m
| ~ element(VAR_0,m)
| VAR_0 = m ),
file('theBenchmark.p',c_4) ).
cnf(c_7,plain,
( f(A) != m
| ~ element(A,m)
| A = m ),
inference(clausify,[status(thm)],[c_4]) ).
cnf(c_8,plain,
( f(A) != m
| ~ element(A,m)
| m = A ),
inference(copy,[status(thm)],[c_7]) ).
fof(c_5_005,axiom,
! [VAR_0] :
( f(VAR_0) != VAR_0
| ~ element(VAR_0,m)
| VAR_0 = m ),
file('theBenchmark.p',c_5) ).
cnf(c_9,plain,
( f(A) != A
| ~ element(A,m)
| A = m ),
inference(clausify,[status(thm)],[c_5]) ).
cnf(c_10,plain,
( f(A) != A
| ~ element(A,m)
| m = A ),
inference(copy,[status(thm)],[c_9]) ).
fof(c_6_006,axiom,
! [VAR_0] :
( element(VAR_0,f(VAR_0))
| ~ element(VAR_0,m)
| VAR_0 = m ),
file('theBenchmark.p',c_6) ).
cnf(c_11,plain,
( element(A,f(A))
| ~ element(A,m)
| A = m ),
inference(clausify,[status(thm)],[c_6]) ).
cnf(c_12,plain,
( element(A,f(A))
| ~ element(A,m)
| m = A ),
inference(copy,[status(thm)],[c_11]) ).
fof(c_7_007,axiom,
! [VAR_0] :
( element(f(VAR_0),VAR_0)
| ~ element(VAR_0,m)
| VAR_0 = m ),
file('theBenchmark.p',c_7) ).
cnf(c_13,plain,
( element(f(A),A)
| ~ element(A,m)
| A = m ),
inference(clausify,[status(thm)],[c_7]) ).
cnf(c_14,plain,
( element(f(A),A)
| ~ element(A,m)
| m = A ),
inference(copy,[status(thm)],[c_13]) ).
fof(c_8_008,axiom,
! [VAR_0,VAR_1] :
( ~ element(VAR_1,VAR_0)
| ~ element(VAR_0,VAR_1)
| VAR_1 = VAR_0
| VAR_1 = m
| element(VAR_0,m)
| VAR_0 = m ),
file('theBenchmark.p',c_8) ).
cnf(c_15,plain,
( ~ element(B,A)
| ~ element(A,B)
| B = A
| B = m
| element(A,m)
| A = m ),
inference(clausify,[status(thm)],[c_8]) ).
cnf(c_365,plain,
( ~ element(B,A)
| ~ element(A,B)
| B = A
| B = m
| element(A,m)
| m = A ),
inference(copy,[status(thm)],[c_15]) ).
cnf(c_16,plain,
( ~ element(B,A)
| ~ element(A,B)
| B = A
| m = B
| element(A,m)
| m = A ),
inference(copy,[status(thm)],[c_365]) ).
fof(c_9_009,axiom,
! [VAR_0] :
( g(VAR_0) != n
| element(VAR_0,n)
| VAR_0 = n ),
file('theBenchmark.p',c_9) ).
cnf(c_17,plain,
( g(A) != n
| element(A,n)
| A = n ),
inference(clausify,[status(thm)],[c_9]) ).
cnf(c_18,plain,
( g(A) != n
| element(A,n)
| n = A ),
inference(copy,[status(thm)],[c_17]) ).
fof(c_10_010,axiom,
! [VAR_0] :
( g(VAR_0) != VAR_0
| element(VAR_0,n)
| VAR_0 = n ),
file('theBenchmark.p',c_10) ).
cnf(c_19,plain,
( g(A) != A
| element(A,n)
| A = n ),
inference(clausify,[status(thm)],[c_10]) ).
cnf(c_20,plain,
( g(A) != A
| element(A,n)
| n = A ),
inference(copy,[status(thm)],[c_19]) ).
fof(c_11_011,axiom,
! [VAR_0] :
( element(VAR_0,g(VAR_0))
| element(VAR_0,n)
| VAR_0 = n ),
file('theBenchmark.p',c_11) ).
cnf(c_21,plain,
( element(A,g(A))
| element(A,n)
| A = n ),
inference(clausify,[status(thm)],[c_11]) ).
cnf(c_22,plain,
( element(A,g(A))
| element(A,n)
| n = A ),
inference(copy,[status(thm)],[c_21]) ).
fof(c_12_012,axiom,
! [VAR_0] :
( element(g(VAR_0),VAR_0)
| element(VAR_0,n)
| VAR_0 = n ),
file('theBenchmark.p',c_12) ).
cnf(c_23,plain,
( element(g(A),A)
| element(A,n)
| A = n ),
inference(clausify,[status(thm)],[c_12]) ).
cnf(c_24,plain,
( element(g(A),A)
| element(A,n)
| n = A ),
inference(copy,[status(thm)],[c_23]) ).
fof(c_13_013,axiom,
! [VAR_0,VAR_1] :
( ~ element(VAR_1,VAR_0)
| ~ element(VAR_0,VAR_1)
| VAR_1 = VAR_0
| VAR_1 = n
| ~ element(VAR_0,n)
| VAR_0 = n ),
file('theBenchmark.p',c_13) ).
cnf(c_25,plain,
( ~ element(B,A)
| ~ element(A,B)
| B = A
| B = n
| ~ element(A,n)
| A = n ),
inference(clausify,[status(thm)],[c_13]) ).
cnf(c_366,plain,
( ~ element(B,A)
| ~ element(A,B)
| B = A
| B = n
| ~ element(A,n)
| n = A ),
inference(copy,[status(thm)],[c_25]) ).
cnf(c_26,plain,
( ~ element(B,A)
| ~ element(A,B)
| B = A
| n = B
| ~ element(A,n)
| n = A ),
inference(copy,[status(thm)],[c_366]) ).
fof(c_14_014,axiom,
! [VAR_0] :
( element(VAR_0,k)
| VAR_0 != m
| VAR_0 = k ),
file('theBenchmark.p',c_14) ).
cnf(c_27,plain,
( element(A,k)
| A != m
| A = k ),
inference(clausify,[status(thm)],[c_14]) ).
cnf(c_367,plain,
( element(A,k)
| A != m
| k = A ),
inference(copy,[status(thm)],[c_27]) ).
cnf(c_28,plain,
( element(A,k)
| m != A
| k = A ),
inference(copy,[status(thm)],[c_367]) ).
fof(c_15_015,axiom,
! [VAR_0] :
( element(VAR_0,k)
| VAR_0 != n
| VAR_0 = k ),
file('theBenchmark.p',c_15) ).
cnf(c_29,plain,
( element(A,k)
| A != n
| A = k ),
inference(clausify,[status(thm)],[c_15]) ).
cnf(c_368,plain,
( element(A,k)
| A != n
| k = A ),
inference(copy,[status(thm)],[c_29]) ).
cnf(c_30,plain,
( element(A,k)
| n != A
| k = A ),
inference(copy,[status(thm)],[c_368]) ).
fof(c_16_016,axiom,
! [VAR_0] :
( ~ element(VAR_0,k)
| VAR_0 = n
| VAR_0 = m
| VAR_0 = k ),
file('theBenchmark.p',c_16) ).
cnf(c_31,plain,
( ~ element(A,k)
| A = n
| A = m
| A = k ),
inference(clausify,[status(thm)],[c_16]) ).
cnf(c_369,plain,
( ~ element(A,k)
| A = n
| A = m
| k = A ),
inference(copy,[status(thm)],[c_31]) ).
cnf(c_370,plain,
( ~ element(A,k)
| A = n
| m = A
| k = A ),
inference(copy,[status(thm)],[c_369]) ).
cnf(c_32,plain,
( ~ element(A,k)
| n = A
| m = A
| k = A ),
inference(copy,[status(thm)],[c_370]) ).
cnf(c_33,plain,
( element(k,j)
| j = k ),
inference(xxres,[status(thm)],[c_4]) ).
cnf(c_371,plain,
( ~ element(g(A),A)
| g(A) = A
| m = g(A)
| element(A,m)
| m = A
| element(A,n)
| n = A ),
inference(resolve,[status(thm)],[c_22,c_16]) ).
cnf(c_35,plain,
( ~ element(g(A),A)
| g(A) = A
| g(A) = m
| element(A,m)
| m = A
| element(A,n)
| n = A ),
inference(copy,[status(thm)],[c_371]) ).
cnf(c_372,plain,
( k = g(j)
| j = g(j)
| element(j,n)
| n = j ),
inference(resolve,[status(thm)],[c_24,c_6]) ).
cnf(c_373,plain,
( k = g(j)
| j = g(j)
| element(j,n)
| j = n ),
inference(copy,[status(thm)],[c_372]) ).
cnf(c_374,plain,
( k = g(j)
| g(j) = j
| element(j,n)
| j = n ),
inference(copy,[status(thm)],[c_373]) ).
cnf(c_42,plain,
( g(j) = k
| g(j) = j
| element(j,n)
| j = n ),
inference(copy,[status(thm)],[c_374]) ).
cnf(c_45,plain,
( element(m,k)
| k = m ),
inference(xxres,[status(thm)],[c_28]) ).
cnf(c_46,plain,
( element(n,k)
| k = n ),
inference(xxres,[status(thm)],[c_30]) ).
cnf(c_375,plain,
( element(k,n)
| n = k
| n = g(k)
| m = g(k)
| k = g(k) ),
inference(resolve,[status(thm)],[c_32,c_24]) ).
cnf(c_376,plain,
( element(k,n)
| n = k
| n = g(k)
| m = g(k)
| g(k) = k ),
inference(copy,[status(thm)],[c_375]) ).
cnf(c_377,plain,
( element(k,n)
| n = k
| n = g(k)
| g(k) = m
| g(k) = k ),
inference(copy,[status(thm)],[c_376]) ).
cnf(c_378,plain,
( element(k,n)
| n = k
| g(k) = n
| g(k) = m
| g(k) = k ),
inference(copy,[status(thm)],[c_377]) ).
cnf(c_47,plain,
( element(k,n)
| k = n
| g(k) = n
| g(k) = m
| g(k) = k ),
inference(copy,[status(thm)],[c_378]) ).
cnf(c_379,plain,
( element(A,n)
| n = A
| g(A) = A
| g(A) = m
| element(A,m)
| m = A
| element(A,n)
| n = A ),
inference(resolve,[status(thm)],[c_35,c_24]) ).
cnf(c_380,plain,
( element(A,n)
| g(A) = A
| g(A) = m
| element(A,m)
| m = A
| element(A,n)
| n = A ),
inference(copy,[status(thm)],[c_379]) ).
cnf(c_53,plain,
( g(A) = A
| g(A) = m
| element(A,m)
| m = A
| element(A,n)
| n = A ),
inference(copy,[status(thm)],[c_380]) ).
cnf(c_381,plain,
( ~ element(k,m)
| m = k
| n = m
| ~ element(k,n)
| n = k
| k = m ),
inference(resolve,[status(thm)],[c_45,c_26]) ).
cnf(c_382,plain,
( ~ element(k,m)
| m = k
| n = m
| ~ element(k,n)
| k = n
| k = m ),
inference(copy,[status(thm)],[c_381]) ).
cnf(c_383,plain,
( ~ element(k,m)
| k = m
| n = m
| ~ element(k,n)
| k = n
| k = m ),
inference(copy,[status(thm)],[c_382]) ).
cnf(c_384,plain,
( ~ element(k,m)
| n = m
| ~ element(k,n)
| k = n
| k = m ),
inference(copy,[status(thm)],[c_383]) ).
cnf(c_54,plain,
( ~ element(k,m)
| ~ element(k,n)
| k = n
| k = m ),
inference(resolve,[status(thm)],[c_2,c_384]) ).
cnf(c_385,plain,
( ~ element(k,n)
| n = k
| m = n
| element(k,m)
| m = k
| k = n ),
inference(resolve,[status(thm)],[c_46,c_16]) ).
cnf(c_386,plain,
( ~ element(k,n)
| n = k
| m = n
| element(k,m)
| k = m
| k = n ),
inference(copy,[status(thm)],[c_385]) ).
cnf(c_387,plain,
( ~ element(k,n)
| n = k
| n = m
| element(k,m)
| k = m
| k = n ),
inference(copy,[status(thm)],[c_386]) ).
cnf(c_388,plain,
( ~ element(k,n)
| k = n
| n = m
| element(k,m)
| k = m
| k = n ),
inference(copy,[status(thm)],[c_387]) ).
cnf(c_389,plain,
( ~ element(k,n)
| n = m
| element(k,m)
| k = m
| k = n ),
inference(copy,[status(thm)],[c_388]) ).
cnf(c_56,plain,
( ~ element(k,n)
| element(k,m)
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_2,c_389]) ).
cnf(c_390,plain,
( element(k,m)
| k = m
| k = n
| g(k) = k
| g(k) = m
| element(k,m)
| m = k
| n = k ),
inference(resolve,[status(thm)],[c_53,c_56]) ).
cnf(c_391,plain,
( element(k,m)
| k = m
| k = n
| g(k) = k
| g(k) = m
| element(k,m)
| m = k
| k = n ),
inference(copy,[status(thm)],[c_390]) ).
cnf(c_392,plain,
( element(k,m)
| k = m
| k = n
| g(k) = k
| g(k) = m
| element(k,m)
| k = m
| k = n ),
inference(copy,[status(thm)],[c_391]) ).
cnf(c_393,plain,
( element(k,m)
| k = m
| g(k) = k
| g(k) = m
| element(k,m)
| k = m
| k = n ),
inference(copy,[status(thm)],[c_392]) ).
cnf(c_394,plain,
( element(k,m)
| g(k) = k
| g(k) = m
| element(k,m)
| k = m
| k = n ),
inference(copy,[status(thm)],[c_393]) ).
cnf(c_83,plain,
( g(k) = k
| g(k) = m
| element(k,m)
| k = m
| k = n ),
inference(copy,[status(thm)],[c_394]) ).
cnf(c_395,plain,
( ~ element(k,n)
| k = n
| k = m
| g(k) = k
| g(k) = m
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_83,c_54]) ).
cnf(c_396,plain,
( ~ element(k,n)
| k = n
| g(k) = k
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_395]) ).
cnf(c_91,plain,
( ~ element(k,n)
| g(k) = k
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_396]) ).
cnf(c_397,plain,
( k = n
| g(k) = n
| g(k) = m
| g(k) = k
| g(k) = k
| g(k) = m
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_91,c_47]) ).
cnf(c_398,plain,
( k = n
| g(k) = n
| g(k) = m
| g(k) = k
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_397]) ).
cnf(c_399,plain,
( k = n
| g(k) = n
| g(k) = k
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_398]) ).
cnf(c_96,plain,
( g(k) = n
| g(k) = k
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_399]) ).
cnf(c_400,plain,
( element(k,n)
| n = k
| g(k) = n
| g(k) = m
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_96,c_20]) ).
cnf(c_401,plain,
( element(k,n)
| k = n
| g(k) = n
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_400]) ).
cnf(c_105,plain,
( element(k,n)
| g(k) = n
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_401]) ).
cnf(c_402,plain,
( element(k,m)
| k = m
| k = n
| g(k) = n
| g(k) = m
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_105,c_56]) ).
cnf(c_403,plain,
( element(k,m)
| k = m
| g(k) = n
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_402]) ).
cnf(c_108,plain,
( element(k,m)
| g(k) = n
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_403]) ).
cnf(c_404,plain,
( ~ element(k,m)
| k = n
| k = m
| g(k) = n
| g(k) = m
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_105,c_54]) ).
cnf(c_405,plain,
( ~ element(k,m)
| k = n
| g(k) = n
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_404]) ).
cnf(c_109,plain,
( ~ element(k,m)
| g(k) = n
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_405]) ).
cnf(c_406,plain,
( g(k) = n
| g(k) = m
| k = m
| k = n
| g(k) = n
| g(k) = m
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_109,c_108]) ).
cnf(c_407,plain,
( g(k) = n
| g(k) = m
| k = m
| g(k) = n
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_406]) ).
cnf(c_408,plain,
( g(k) = n
| g(k) = m
| g(k) = n
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_407]) ).
cnf(c_409,plain,
( g(k) = n
| g(k) = n
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_408]) ).
cnf(c_123,plain,
( g(k) = n
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_409]) ).
cnf(c_410,plain,
( element(k,n)
| n = k
| g(k) = m
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_123,c_18]) ).
cnf(c_411,plain,
( element(k,n)
| k = n
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_410]) ).
cnf(c_124,plain,
( element(k,n)
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_411]) ).
cnf(c_412,plain,
( element(k,m)
| k = m
| k = n
| g(k) = m
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_124,c_56]) ).
cnf(c_413,plain,
( element(k,m)
| k = m
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_412]) ).
cnf(c_128,plain,
( element(k,m)
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_413]) ).
cnf(c_414,plain,
( ~ element(k,m)
| k = n
| k = m
| g(k) = m
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_124,c_54]) ).
cnf(c_415,plain,
( ~ element(k,m)
| k = n
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_414]) ).
cnf(c_129,plain,
( ~ element(k,m)
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_415]) ).
cnf(c_416,plain,
( g(k) = m
| k = m
| k = n
| g(k) = m
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_129,c_128]) ).
cnf(c_417,plain,
( g(k) = m
| k = m
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_416]) ).
cnf(c_418,plain,
( g(k) = m
| g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_417]) ).
cnf(c_142,plain,
( g(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_418]) ).
cnf(c_419,plain,
( element(k,m)
| element(k,n)
| n = k
| k = m
| k = n ),
inference(paramod,[status(thm)],[c_142,c_22]) ).
cnf(c_420,plain,
( element(k,m)
| element(k,n)
| k = n
| k = m
| k = n ),
inference(copy,[status(thm)],[c_419]) ).
cnf(c_144,plain,
( element(k,m)
| element(k,n)
| k = m
| k = n ),
inference(copy,[status(thm)],[c_420]) ).
cnf(c_421,plain,
( element(k,m)
| k = m
| k = n
| element(k,m)
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_144,c_56]) ).
cnf(c_422,plain,
( element(k,m)
| k = m
| element(k,m)
| k = m
| k = n ),
inference(copy,[status(thm)],[c_421]) ).
cnf(c_423,plain,
( element(k,m)
| element(k,m)
| k = m
| k = n ),
inference(copy,[status(thm)],[c_422]) ).
cnf(c_147,plain,
( element(k,m)
| k = m
| k = n ),
inference(copy,[status(thm)],[c_423]) ).
cnf(c_424,plain,
( ~ element(k,n)
| k = n
| k = m
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_147,c_54]) ).
cnf(c_425,plain,
( ~ element(k,n)
| k = n
| k = m
| k = n ),
inference(copy,[status(thm)],[c_424]) ).
cnf(c_149,plain,
( ~ element(k,n)
| k = m
| k = n ),
inference(copy,[status(thm)],[c_425]) ).
cnf(c_426,plain,
( element(f(k),k)
| m = k
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_147,c_14]) ).
cnf(c_427,plain,
( element(f(k),k)
| k = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_426]) ).
cnf(c_150,plain,
( element(f(k),k)
| k = m
| k = n ),
inference(copy,[status(thm)],[c_427]) ).
cnf(c_428,plain,
( element(k,f(k))
| m = k
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_147,c_12]) ).
cnf(c_429,plain,
( element(k,f(k))
| k = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_428]) ).
cnf(c_151,plain,
( element(k,f(k))
| k = m
| k = n ),
inference(copy,[status(thm)],[c_429]) ).
cnf(c_430,plain,
( f(k) != k
| m = k
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_147,c_10]) ).
cnf(c_431,plain,
( f(k) != k
| k = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_430]) ).
cnf(c_152,plain,
( f(k) != k
| k = m
| k = n ),
inference(copy,[status(thm)],[c_431]) ).
cnf(c_432,plain,
( f(k) != m
| m = k
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_147,c_8]) ).
cnf(c_433,plain,
( f(k) != m
| k = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_432]) ).
cnf(c_153,plain,
( f(k) != m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_433]) ).
cnf(c_434,plain,
( n = f(k)
| m = f(k)
| k = f(k)
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_150,c_32]) ).
cnf(c_435,plain,
( n = f(k)
| m = f(k)
| f(k) = k
| k = m
| k = n ),
inference(copy,[status(thm)],[c_434]) ).
cnf(c_436,plain,
( n = f(k)
| f(k) = m
| f(k) = k
| k = m
| k = n ),
inference(copy,[status(thm)],[c_435]) ).
cnf(c_156,plain,
( f(k) = n
| f(k) = m
| f(k) = k
| k = m
| k = n ),
inference(copy,[status(thm)],[c_436]) ).
cnf(c_437,plain,
( k = m
| k = n
| f(k) = n
| f(k) = m
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_156,c_152]) ).
cnf(c_438,plain,
( k = m
| f(k) = n
| f(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_437]) ).
cnf(c_162,plain,
( f(k) = n
| f(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_438]) ).
cnf(c_439,plain,
( element(k,n)
| k = m
| k = n
| f(k) = m
| k = m
| k = n ),
inference(paramod,[status(thm)],[c_162,c_151]) ).
cnf(c_440,plain,
( element(k,n)
| k = m
| f(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_439]) ).
cnf(c_165,plain,
( element(k,n)
| f(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_440]) ).
cnf(c_441,plain,
( k = m
| k = n
| f(k) = m
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_165,c_149]) ).
cnf(c_442,plain,
( k = m
| f(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_441]) ).
cnf(c_166,plain,
( f(k) = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_442]) ).
cnf(c_443,plain,
( k = m
| k = n
| k = m
| k = n ),
inference(resolve,[status(thm)],[c_166,c_153]) ).
cnf(c_444,plain,
( k = m
| k = m
| k = n ),
inference(copy,[status(thm)],[c_443]) ).
cnf(c_167,plain,
( k = m
| k = n ),
inference(copy,[status(thm)],[c_444]) ).
cnf(c_170,plain,
( ~ element(A,n)
| n = A
| m = A
| k = A
| k = m ),
inference(paramod,[status(thm)],[c_167,c_32]) ).
cnf(c_445,plain,
( element(m,n)
| k = m
| k = m ),
inference(paramod,[status(thm)],[c_167,c_45]) ).
cnf(c_172,plain,
( element(m,n)
| k = m ),
inference(copy,[status(thm)],[c_445]) ).
cnf(c_446,plain,
( g(j) = k
| g(j) = j
| j = n
| n = j
| m = j
| k = j
| k = m ),
inference(resolve,[status(thm)],[c_170,c_42]) ).
cnf(c_447,plain,
( g(j) = k
| g(j) = j
| j = n
| n = j
| m = j
| j = k
| k = m ),
inference(copy,[status(thm)],[c_446]) ).
cnf(c_448,plain,
( g(j) = k
| g(j) = j
| j = n
| n = j
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_447]) ).
cnf(c_449,plain,
( g(j) = k
| g(j) = j
| j = n
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_448]) ).
cnf(c_187,plain,
( g(j) = k
| g(j) = j
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_449]) ).
cnf(c_450,plain,
( element(j,n)
| n = j
| g(j) = k
| j = n
| j = m
| j = k
| k = m ),
inference(resolve,[status(thm)],[c_187,c_20]) ).
cnf(c_451,plain,
( element(j,n)
| j = n
| g(j) = k
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_450]) ).
cnf(c_200,plain,
( element(j,n)
| g(j) = k
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_451]) ).
cnf(c_452,plain,
( n = j
| m = j
| k = j
| k = m
| g(j) = k
| j = n
| j = m
| j = k
| k = m ),
inference(resolve,[status(thm)],[c_200,c_170]) ).
cnf(c_453,plain,
( n = j
| m = j
| j = k
| k = m
| g(j) = k
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_452]) ).
cnf(c_454,plain,
( n = j
| j = m
| j = k
| k = m
| g(j) = k
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_453]) ).
cnf(c_455,plain,
( j = n
| j = m
| j = k
| k = m
| g(j) = k
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_454]) ).
cnf(c_456,plain,
( j = n
| j = m
| j = k
| g(j) = k
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_455]) ).
cnf(c_457,plain,
( j = n
| j = m
| g(j) = k
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_456]) ).
cnf(c_458,plain,
( j = n
| g(j) = k
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_457]) ).
cnf(c_204,plain,
( g(j) = k
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_458]) ).
cnf(c_459,plain,
( k != n
| element(j,n)
| n = j
| j = n
| j = m
| j = k
| k = m ),
inference(paramod,[status(thm)],[c_204,c_18]) ).
cnf(c_460,plain,
( k != n
| element(j,n)
| j = n
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_459]) ).
cnf(c_207,plain,
( k != n
| element(j,n)
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_460]) ).
cnf(c_461,plain,
( k = m
| element(j,n)
| j = n
| j = m
| j = k
| k = m ),
inference(resolve,[status(thm)],[c_207,c_167]) ).
cnf(c_220,plain,
( element(j,n)
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_461]) ).
cnf(c_462,plain,
( n = j
| m = j
| k = j
| k = m
| j = n
| j = m
| j = k
| k = m ),
inference(resolve,[status(thm)],[c_220,c_170]) ).
cnf(c_463,plain,
( n = j
| m = j
| j = k
| k = m
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_462]) ).
cnf(c_464,plain,
( n = j
| j = m
| j = k
| k = m
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_463]) ).
cnf(c_465,plain,
( j = n
| j = m
| j = k
| k = m
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_464]) ).
cnf(c_466,plain,
( j = n
| j = m
| j = k
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_465]) ).
cnf(c_467,plain,
( j = n
| j = m
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_466]) ).
cnf(c_468,plain,
( j = n
| j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_467]) ).
cnf(c_224,plain,
( j = n
| j = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_468]) ).
cnf(c_469,plain,
( j = n
| j = m
| j = n
| k = m
| k = m ),
inference(paramod,[status(thm)],[c_167,c_224]) ).
cnf(c_470,plain,
( j = n
| j = m
| j = n
| k = m ),
inference(copy,[status(thm)],[c_469]) ).
cnf(c_229,plain,
( j = m
| j = n
| k = m ),
inference(copy,[status(thm)],[c_470]) ).
cnf(c_231,plain,
( ~ element(A,n)
| k = A
| j = A
| j = m
| k = m ),
inference(paramod,[status(thm)],[c_229,c_6]) ).
cnf(c_471,plain,
( ~ element(m,n)
| j = m
| j = m
| k = m ),
inference(factor,[status(thm)],[c_231]) ).
cnf(c_238,plain,
( ~ element(m,n)
| j = m
| k = m ),
inference(copy,[status(thm)],[c_471]) ).
cnf(c_472,plain,
( k = m
| j = m
| k = m ),
inference(resolve,[status(thm)],[c_238,c_172]) ).
cnf(c_239,plain,
( j = m
| k = m ),
inference(copy,[status(thm)],[c_472]) ).
cnf(c_249,plain,
( element(k,m)
| j = k
| k = m ),
inference(paramod,[status(thm)],[c_239,c_33]) ).
cnf(c_473,plain,
( element(f(k),k)
| m = k
| j = k
| k = m ),
inference(resolve,[status(thm)],[c_249,c_14]) ).
cnf(c_474,plain,
( element(f(k),k)
| k = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_473]) ).
cnf(c_255,plain,
( element(f(k),k)
| j = k
| k = m ),
inference(copy,[status(thm)],[c_474]) ).
cnf(c_475,plain,
( f(k) != k
| m = k
| j = k
| k = m ),
inference(resolve,[status(thm)],[c_249,c_10]) ).
cnf(c_476,plain,
( f(k) != k
| k = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_475]) ).
cnf(c_257,plain,
( f(k) != k
| j = k
| k = m ),
inference(copy,[status(thm)],[c_476]) ).
cnf(c_477,plain,
( f(k) != m
| m = k
| j = k
| k = m ),
inference(resolve,[status(thm)],[c_249,c_8]) ).
cnf(c_478,plain,
( f(k) != m
| k = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_477]) ).
cnf(c_258,plain,
( f(k) != m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_478]) ).
cnf(c_479,plain,
( n = f(k)
| m = f(k)
| k = f(k)
| j = k
| k = m ),
inference(resolve,[status(thm)],[c_255,c_32]) ).
cnf(c_480,plain,
( n = f(k)
| m = f(k)
| f(k) = k
| j = k
| k = m ),
inference(copy,[status(thm)],[c_479]) ).
cnf(c_481,plain,
( n = f(k)
| f(k) = m
| f(k) = k
| j = k
| k = m ),
inference(copy,[status(thm)],[c_480]) ).
cnf(c_273,plain,
( f(k) = n
| f(k) = m
| f(k) = k
| j = k
| k = m ),
inference(copy,[status(thm)],[c_481]) ).
cnf(c_482,plain,
( f(k) != n
| j = k
| k = m
| k = m ),
inference(paramod,[status(thm)],[c_167,c_257]) ).
cnf(c_281,plain,
( f(k) != n
| j = k
| k = m ),
inference(copy,[status(thm)],[c_482]) ).
cnf(c_483,plain,
( j = k
| k = m
| f(k) = n
| f(k) = m
| j = k
| k = m ),
inference(resolve,[status(thm)],[c_273,c_257]) ).
cnf(c_484,plain,
( j = k
| f(k) = n
| f(k) = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_483]) ).
cnf(c_317,plain,
( f(k) = n
| f(k) = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_484]) ).
cnf(c_485,plain,
( j = k
| k = m
| f(k) = m
| j = k
| k = m ),
inference(resolve,[status(thm)],[c_317,c_281]) ).
cnf(c_486,plain,
( j = k
| f(k) = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_485]) ).
cnf(c_321,plain,
( f(k) = m
| j = k
| k = m ),
inference(copy,[status(thm)],[c_486]) ).
cnf(c_487,plain,
( j = k
| k = m
| j = k
| k = m ),
inference(resolve,[status(thm)],[c_321,c_258]) ).
cnf(c_488,plain,
( j = k
| j = k
| k = m ),
inference(copy,[status(thm)],[c_487]) ).
cnf(c_322,plain,
( j = k
| k = m ),
inference(copy,[status(thm)],[c_488]) ).
cnf(c_489,plain,
( k = m
| k = m
| k = m ),
inference(paramod,[status(thm)],[c_322,c_239]) ).
cnf(c_490,plain,
( k = m
| k = m ),
inference(copy,[status(thm)],[c_489]) ).
cnf(c_328,plain,
k = m,
inference(copy,[status(thm)],[c_490]) ).
cnf(c_491,plain,
( element(n,k)
| m = n ),
inference(paramod,[status(thm)],[c_328,c_46]) ).
cnf(c_492,plain,
( element(n,m)
| m = n ),
inference(paramod,[status(thm)],[c_328,c_491]) ).
cnf(c_493,plain,
( element(n,m)
| n = m ),
inference(copy,[status(thm)],[c_492]) ).
cnf(c_338,plain,
element(n,m),
inference(resolve,[status(thm)],[c_2,c_493]) ).
cnf(c_494,plain,
( ~ element(A,k)
| n = A
| m = A
| m = A ),
inference(paramod,[status(thm)],[c_328,c_32]) ).
cnf(c_495,plain,
( ~ element(A,m)
| n = A
| m = A
| m = A ),
inference(paramod,[status(thm)],[c_328,c_494]) ).
cnf(c_341,plain,
( ~ element(A,m)
| n = A
| m = A ),
inference(copy,[status(thm)],[c_495]) ).
cnf(c_496,plain,
( element(f(n),n)
| m = n ),
inference(resolve,[status(thm)],[c_338,c_14]) ).
cnf(c_497,plain,
( element(f(n),n)
| n = m ),
inference(copy,[status(thm)],[c_496]) ).
cnf(c_345,plain,
element(f(n),n),
inference(resolve,[status(thm)],[c_2,c_497]) ).
cnf(c_498,plain,
( element(n,f(n))
| m = n ),
inference(resolve,[status(thm)],[c_338,c_12]) ).
cnf(c_499,plain,
( element(n,f(n))
| n = m ),
inference(copy,[status(thm)],[c_498]) ).
cnf(c_346,plain,
element(n,f(n)),
inference(resolve,[status(thm)],[c_2,c_499]) ).
cnf(c_500,plain,
( f(n) != n
| m = n ),
inference(resolve,[status(thm)],[c_338,c_10]) ).
cnf(c_501,plain,
( f(n) != n
| n = m ),
inference(copy,[status(thm)],[c_500]) ).
cnf(c_347,plain,
f(n) != n,
inference(resolve,[status(thm)],[c_2,c_501]) ).
cnf(c_502,plain,
( f(n) != m
| m = n ),
inference(resolve,[status(thm)],[c_338,c_8]) ).
cnf(c_503,plain,
( f(n) != m
| n = m ),
inference(copy,[status(thm)],[c_502]) ).
cnf(c_348,plain,
f(n) != m,
inference(resolve,[status(thm)],[c_2,c_503]) ).
cnf(c_504,plain,
m != f(n),
inference(copy,[status(thm)],[c_348]) ).
cnf(c_505,plain,
( ~ element(f(n),m)
| n = f(n) ),
inference(resolve,[status(thm)],[c_341,c_504]) ).
cnf(c_506,plain,
n != f(n),
inference(copy,[status(thm)],[c_347]) ).
cnf(c_360,plain,
~ element(f(n),m),
inference(resolve,[status(thm)],[c_505,c_506]) ).
cnf(c_507,plain,
( ~ element(n,f(n))
| n = f(n)
| m = n
| element(f(n),m)
| m = f(n) ),
inference(resolve,[status(thm)],[c_345,c_16]) ).
cnf(c_508,plain,
( ~ element(n,f(n))
| n = f(n)
| m = n
| element(f(n),m)
| f(n) = m ),
inference(copy,[status(thm)],[c_507]) ).
cnf(c_509,plain,
( ~ element(n,f(n))
| n = f(n)
| n = m
| element(f(n),m)
| f(n) = m ),
inference(copy,[status(thm)],[c_508]) ).
cnf(c_510,plain,
( ~ element(n,f(n))
| f(n) = n
| n = m
| element(f(n),m)
| f(n) = m ),
inference(copy,[status(thm)],[c_509]) ).
cnf(c_511,plain,
( ~ element(n,f(n))
| f(n) = n
| n = m
| element(f(n),m) ),
inference(resolve,[status(thm)],[c_348,c_510]) ).
cnf(c_512,plain,
( ~ element(n,f(n))
| f(n) = n
| n = m ),
inference(resolve,[status(thm)],[c_360,c_511]) ).
cnf(c_513,plain,
( ~ element(n,f(n))
| f(n) = n ),
inference(resolve,[status(thm)],[c_2,c_512]) ).
cnf(c_514,plain,
~ element(n,f(n)),
inference(resolve,[status(thm)],[c_347,c_513]) ).
cnf(c_362,plain,
$false,
inference(resolve,[status(thm)],[c_346,c_514]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN015-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n010.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 26 17:04:31 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.15/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/0.37 % Process 3770018 was started by sandbox on n010,
% 0.15/0.37 % Sat Sep 26 17:04:31 2026
% 0.15/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.15/0.38
% 0.15/0.38 % From the command line: assign(max_seconds, 300).
% 0.15/0.45
% 0.15/0.45 % SZS status Unsatisfiable for theBenchmark
% 0.15/0.45
% 0.15/0.45 % Proof 1 at 0.03 (+ 0.01) seconds.
% 0.15/0.45 % Length of proof is 94.
% 0.15/0.45 % Level of proof is 42.
% 0.15/0.45 % Maximum clause weight is 34.000.
% 0.15/0.45 % Given clauses 179.
% 0.15/0.45
% 0.15/0.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------