%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYN015-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n005.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 : Fri Sep 25 03:33:20 PM UTC 2026
% Result : Unsatisfiable 18.64s 5.91s
% Output : Proof 18.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 141
% Number of leaves : 16
% Syntax : Number of formulae : 261 ( 6 unt; 0 def)
% Number of atoms : 1261 (1041 equ)
% Maximal formula atoms : 11 ( 4 avg)
% Number of connectives : 1174 ( 174 ~;1000 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 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 : 78 ( 0 sgn 34 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f15,negated_conjecture,
( ~ element(Y,k)
| Y = n
| Y = m
| Y = k ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_16) ).
fof(f15_nnf,plain,
! [Y] :
( ~ element(Y,k)
| Y = n
| Y = m
| Y = k ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [Y] :
( ~ element(Y,k)
| Y = n
| Y = m
| Y = k ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( ~ element(X0,k)
| X0 = n
| X0 = m
| X0 = k ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(f11,negated_conjecture,
( element(g(Y),Y)
| element(Y,n)
| Y = n ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_12) ).
fof(f11_nnf,plain,
! [Y] :
( element(g(Y),Y)
| element(Y,n)
| Y = n ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [Y] :
( element(g(Y),Y)
| element(Y,n)
| Y = n ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( element(g(X0),X0)
| element(X0,n)
| X0 = n ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p41,plain,
( element(k,n)
| k = n
| g(k) = n
| g(k) = m
| g(k) = k ),
inference(resolution,[status(thm)],[c15,c11]) ).
cnf(f9,negated_conjecture,
( g(Y) != Y
| element(Y,n)
| Y = n ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_10) ).
fof(f9_nnf,plain,
! [Y] :
( g(Y) != Y
| element(Y,n)
| Y = n ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [Y] :
( g(Y) != Y
| element(Y,n)
| Y = n ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( g(X0) != X0
| element(X0,n)
| X0 = n ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p98,plain,
( element(k,n)
| k = n
| element(k,n)
| k = n
| g(k) = n
| g(k) = m ),
inference(resolution,[status(thm)],[p41,c9]) ).
cnf(p196,plain,
( element(k,n)
| element(k,n)
| k = n
| g(k) = n
| g(k) = m ),
inference(factoring,[status(thm)],[p98]) ).
cnf(p198,plain,
( element(k,n)
| k = n
| g(k) = n
| g(k) = m ),
inference(factoring,[status(thm)],[p196]) ).
cnf(f8,negated_conjecture,
( g(Y) != n
| element(Y,n)
| Y = n ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_9) ).
fof(f8_nnf,plain,
! [Y] :
( g(Y) != n
| element(Y,n)
| Y = n ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [Y] :
( g(Y) != n
| element(Y,n)
| Y = n ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( g(X0) != n
| element(X0,n)
| X0 = n ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p201,plain,
( element(k,n)
| k = n
| element(k,n)
| k = n
| g(k) = m ),
inference(resolution,[status(thm)],[p198,c8]) ).
cnf(p202,plain,
( element(k,n)
| element(k,n)
| k = n
| g(k) = m ),
inference(factoring,[status(thm)],[p201]) ).
cnf(p204,plain,
( element(k,n)
| k = n
| g(k) = m ),
inference(factoring,[status(thm)],[p202]) ).
cnf(f10,negated_conjecture,
( element(Y,g(Y))
| element(Y,n)
| Y = n ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_11) ).
fof(f10_nnf,plain,
! [Y] :
( element(Y,g(Y))
| element(Y,n)
| Y = n ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [Y] :
( element(Y,g(Y))
| element(Y,n)
| Y = n ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( element(X0,g(X0))
| element(X0,n)
| X0 = n ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p208,plain,
( element(k,m)
| element(k,n)
| k = n
| element(k,n)
| k = n ),
inference(superposition,[status(thm)],[p204,c10]) ).
cnf(p214,plain,
( element(k,m)
| element(k,n)
| element(k,n)
| k = n ),
inference(factoring,[status(thm)],[p208]) ).
cnf(p216,plain,
( element(k,m)
| element(k,n)
| k = n ),
inference(factoring,[status(thm)],[p214]) ).
cnf(f7,negated_conjecture,
( ~ element(V1,Y)
| ~ element(Y,V1)
| V1 = Y
| V1 = m
| element(Y,m)
| Y = m ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_8) ).
fof(f7_nnf,plain,
! [Y,V1] :
( ~ element(V1,Y)
| ~ element(Y,V1)
| V1 = Y
| V1 = m
| element(Y,m)
| Y = m ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [Y,V1] :
( ~ element(V1,Y)
| ~ element(Y,V1)
| V1 = Y
| V1 = m
| element(Y,m)
| Y = m ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( ~ element(X1,X0)
| ~ element(X0,X1)
| X1 = X0
| X1 = m
| element(X0,m)
| X0 = m ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p217,plain,
( ~ element(n,k)
| n = k
| n = m
| element(k,m)
| k = m
| element(k,m)
| k = n ),
inference(resolution,[status(thm)],[p216,c7]) ).
cnf(p248,plain,
( ~ element(n,k)
| n = k
| n = m
| k = m
| element(k,m)
| k = n ),
inference(factoring,[status(thm)],[p217]) ).
cnf(f14,negated_conjecture,
( element(Y,k)
| Y != n
| Y = k ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_15) ).
fof(f14_nnf,plain,
! [Y] :
( element(Y,k)
| Y != n
| Y = k ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [Y] :
( element(Y,k)
| Y != n
| Y = k ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( element(X0,k)
| X0 != n
| X0 = k ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p20,plain,
( element(n,k)
| n = k ),
inference(equality_resolution,[status(thm)],[c14]) ).
cnf(p252,plain,
( n = k
| n = k
| n = m
| k = m
| element(k,m)
| k = n ),
inference(resolution,[status(thm)],[p248,p20]) ).
cnf(p254,plain,
( n = k
| n = m
| k = m
| element(k,m)
| k = n ),
inference(factoring,[status(thm)],[p252]) ).
cnf(f6,negated_conjecture,
( element(f(Y),Y)
| ~ element(Y,m)
| Y = m ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_7) ).
fof(f6_nnf,plain,
! [Y] :
( element(f(Y),Y)
| ~ element(Y,m)
| Y = m ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [Y] :
( element(f(Y),Y)
| ~ element(Y,m)
| Y = m ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( element(f(X0),X0)
| ~ element(X0,m)
| X0 = m ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p259,plain,
( element(f(k),k)
| k = m
| n = k
| n = m
| k = m
| k = n ),
inference(resolution,[status(thm)],[p254,c6]) ).
cnf(p269,plain,
( element(f(k),k)
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p259]) ).
cnf(p272,plain,
( f(k) = n
| f(k) = m
| f(k) = k
| n = k
| n = m
| k = m
| k = n ),
inference(resolution,[status(thm)],[p269,c15]) ).
cnf(f4,negated_conjecture,
( f(Y) != Y
| ~ element(Y,m)
| Y = m ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_5) ).
fof(f4_nnf,plain,
! [Y] :
( f(Y) != Y
| ~ element(Y,m)
| Y = m ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [Y] :
( f(Y) != Y
| ~ element(Y,m)
| Y = m ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( f(X0) != X0
| ~ element(X0,m)
| X0 = m ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p257,plain,
( f(k) != k
| k = m
| n = k
| n = m
| k = m
| k = n ),
inference(resolution,[status(thm)],[p254,c4]) ).
cnf(p264,plain,
( f(k) != k
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p257]) ).
cnf(p394,plain,
( n = k
| n = m
| k = m
| k = n
| f(k) = n
| f(k) = m
| n = k
| n = m
| k = m
| k = n ),
inference(resolution,[status(thm)],[p272,p264]) ).
cnf(p598,plain,
( n = k
| n = m
| k = m
| f(k) = n
| f(k) = m
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p394]) ).
cnf(p869,plain,
( n = k
| n = m
| f(k) = n
| f(k) = m
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p598]) ).
cnf(p931,plain,
( n = k
| f(k) = n
| f(k) = m
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p869]) ).
cnf(p933,plain,
( f(k) = n
| f(k) = m
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p931]) ).
cnf(f5,negated_conjecture,
( element(Y,f(Y))
| ~ element(Y,m)
| Y = m ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_6) ).
fof(f5_nnf,plain,
! [Y] :
( element(Y,f(Y))
| ~ element(Y,m)
| Y = m ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [Y] :
( element(Y,f(Y))
| ~ element(Y,m)
| Y = m ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( element(X0,f(X0))
| ~ element(X0,m)
| X0 = m ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p258,plain,
( element(k,f(k))
| k = m
| n = k
| n = m
| k = m
| k = n ),
inference(resolution,[status(thm)],[p254,c5]) ).
cnf(p266,plain,
( element(k,f(k))
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p258]) ).
cnf(p934,plain,
( element(k,n)
| n = k
| n = m
| k = m
| k = n
| f(k) = m
| n = k
| n = m
| k = m
| k = n ),
inference(superposition,[status(thm)],[p933,p266]) ).
cnf(p1541,plain,
( element(k,n)
| n = k
| n = m
| k = m
| f(k) = m
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p934]) ).
cnf(p2057,plain,
( element(k,n)
| n = k
| n = m
| f(k) = m
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p1541]) ).
cnf(p2060,plain,
( element(k,n)
| n = k
| f(k) = m
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p2057]) ).
cnf(p2063,plain,
( element(k,n)
| f(k) = m
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p2060]) ).
cnf(f3,negated_conjecture,
( f(Y) != m
| ~ element(Y,m)
| Y = m ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_4) ).
fof(f3_nnf,plain,
! [Y] :
( f(Y) != m
| ~ element(Y,m)
| Y = m ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [Y] :
( f(Y) != m
| ~ element(Y,m)
| Y = m ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( f(X0) != m
| ~ element(X0,m)
| X0 = m ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p256,plain,
( f(k) != m
| k = m
| n = k
| n = m
| k = m
| k = n ),
inference(resolution,[status(thm)],[p254,c3]) ).
cnf(p261,plain,
( f(k) != m
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p256]) ).
cnf(p2064,plain,
( n = k
| n = m
| k = m
| k = n
| element(k,n)
| n = k
| n = m
| k = m
| k = n ),
inference(resolution,[status(thm)],[p2063,p261]) ).
cnf(p2065,plain,
( n = k
| n = m
| k = m
| element(k,n)
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p2064]) ).
cnf(p2069,plain,
( n = k
| n = m
| element(k,n)
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p2065]) ).
cnf(p2073,plain,
( n = k
| element(k,n)
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p2069]) ).
cnf(p2075,plain,
( element(k,n)
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p2073]) ).
cnf(f12,negated_conjecture,
( ~ element(V,Y)
| ~ element(Y,V)
| V = Y
| V = n
| ~ element(Y,n)
| Y = n ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_13) ).
fof(f12_nnf,plain,
! [Y,V] :
( ~ element(V,Y)
| ~ element(Y,V)
| V = Y
| V = n
| ~ element(Y,n)
| Y = n ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [Y,V] :
( ~ element(V,Y)
| ~ element(Y,V)
| V = Y
| V = n
| ~ element(Y,n)
| Y = n ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( ~ element(X1,X0)
| ~ element(X0,X1)
| X1 = X0
| X1 = n
| ~ element(X0,n)
| X0 = n ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p2076,plain,
( ~ element(X0,k)
| ~ element(k,X0)
| X0 = k
| X0 = n
| k = n
| n = k
| n = m
| k = m
| k = n ),
inference(resolution,[status(thm)],[p2075,c12]) ).
cnf(p2079,plain,
( ~ element(X0,k)
| ~ element(k,X0)
| X0 = k
| X0 = n
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p2076]) ).
cnf(p2084,plain,
( n = k
| n = m
| k = m
| k = n
| ~ element(m,k)
| m = k
| m = n
| n = k
| n = m
| k = m
| k = n ),
inference(resolution,[status(thm)],[p2079,p254]) ).
cnf(p3754,plain,
( n = k
| n = m
| k = m
| ~ element(m,k)
| m = k
| m = n
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p2084]) ).
cnf(p3866,plain,
( n = k
| n = m
| ~ element(m,k)
| m = k
| m = n
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p3754]) ).
cnf(p3869,plain,
( n = k
| ~ element(m,k)
| m = k
| m = n
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p3866]) ).
cnf(p3871,plain,
( ~ element(m,k)
| m = k
| m = n
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p3869]) ).
cnf(f13,negated_conjecture,
( element(Y,k)
| Y != m
| Y = k ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_14) ).
fof(f13_nnf,plain,
! [Y] :
( element(Y,k)
| Y != m
| Y = k ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [Y] :
( element(Y,k)
| Y != m
| Y = k ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( element(X0,k)
| X0 != m
| X0 = k ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p19,plain,
( element(m,k)
| m = k ),
inference(equality_resolution,[status(thm)],[c13]) ).
cnf(p3876,plain,
( m = k
| m = k
| m = n
| n = k
| n = m
| k = m
| k = n ),
inference(resolution,[status(thm)],[p3871,p19]) ).
cnf(p3877,plain,
( m = k
| m = n
| n = k
| n = m
| k = m
| k = n ),
inference(factoring,[status(thm)],[p3876]) ).
cnf(p37,plain,
( k != n
| ~ element(X0,k)
| X0 = m
| X0 = k ),
inference(equality_factoring,[status(thm)],[c15]) ).
cnf(p47,plain,
( n = k
| k != n
| n = m
| n = k ),
inference(resolution,[status(thm)],[p37,p20]) ).
cnf(p71,plain,
( k != n
| n = m
| n = k ),
inference(factoring,[status(thm)],[p47]) ).
cnf(p3885,plain,
( n = m
| n = k
| m = k
| m = n
| n = k
| n = m
| k = m ),
inference(resolution,[status(thm)],[p3877,p71]) ).
cnf(p3971,plain,
( n = k
| m = k
| m = n
| n = k
| n = m
| k = m ),
inference(factoring,[status(thm)],[p3885]) ).
cnf(p3973,plain,
( m = k
| m = n
| n = k
| n = m
| k = m ),
inference(factoring,[status(thm)],[p3971]) ).
cnf(p36,plain,
( k != m
| ~ element(X0,k)
| X0 = n
| X0 = k ),
inference(equality_factoring,[status(thm)],[c15]) ).
cnf(p44,plain,
( m = k
| k != m
| m = n
| m = k ),
inference(resolution,[status(thm)],[p36,p19]) ).
cnf(p66,plain,
( k != m
| m = n
| m = k ),
inference(factoring,[status(thm)],[p44]) ).
cnf(p3980,plain,
( m = n
| m = k
| m = k
| m = n
| n = k
| n = m ),
inference(resolution,[status(thm)],[p3973,p66]) ).
cnf(p4050,plain,
( m = k
| m = k
| m = n
| n = k
| n = m ),
inference(factoring,[status(thm)],[p3980]) ).
cnf(p4052,plain,
( m = k
| m = n
| n = k
| n = m ),
inference(factoring,[status(thm)],[p4050]) ).
cnf(p39,plain,
( n != k
| ~ element(X0,k)
| X0 = n
| X0 = m ),
inference(equality_factoring,[status(thm)],[c15]) ).
cnf(p4062,plain,
( n != k
| ~ element(X0,n)
| X0 = n
| X0 = m
| m = k
| m = n
| n = m ),
inference(superposition,[status(thm)],[p4052,p39]) ).
cnf(p4252,plain,
( n != k
| n != k
| ~ element(X0,n)
| X0 = n
| X0 = m
| m = n
| n = m ),
inference(equality_factoring,[status(thm)],[p4062]) ).
cnf(p4310,plain,
( n != k
| ~ element(X0,n)
| X0 = n
| X0 = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p4252]) ).
cnf(f2,negated_conjecture,
( ~ element(Y,j)
| Y = k
| Y = j ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_3) ).
fof(f2_nnf,plain,
! [Y] :
( ~ element(Y,j)
| Y = k
| Y = j ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [Y] :
( ~ element(Y,j)
| Y = k
| Y = j ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( ~ element(X0,j)
| X0 = k
| X0 = j ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p28,plain,
( g(j) = k
| g(j) = j
| element(j,n)
| j = n ),
inference(resolution,[status(thm)],[c11,c2]) ).
cnf(p87,plain,
( element(j,k)
| element(j,n)
| j = n
| g(j) = j
| element(j,n)
| j = n ),
inference(superposition,[status(thm)],[p28,c10]) ).
cnf(p116,plain,
( element(j,k)
| element(j,n)
| g(j) = j
| element(j,n)
| j = n ),
inference(factoring,[status(thm)],[p87]) ).
cnf(p118,plain,
( element(j,k)
| g(j) = j
| element(j,n)
| j = n ),
inference(factoring,[status(thm)],[p116]) ).
cnf(p119,plain,
( element(j,n)
| j = n
| element(j,k)
| element(j,n)
| j = n ),
inference(resolution,[status(thm)],[p118,c9]) ).
cnf(p122,plain,
( element(j,n)
| element(j,k)
| element(j,n)
| j = n ),
inference(factoring,[status(thm)],[p119]) ).
cnf(p124,plain,
( element(j,k)
| element(j,n)
| j = n ),
inference(factoring,[status(thm)],[p122]) ).
cnf(p126,plain,
( j = n
| j = m
| j = k
| element(j,n)
| j = n ),
inference(resolution,[status(thm)],[p124,c15]) ).
cnf(p143,plain,
( j = m
| j = k
| element(j,n)
| j = n ),
inference(factoring,[status(thm)],[p126]) ).
cnf(p4311,plain,
( j = m
| j = k
| j = n
| n != k
| j = n
| j = m
| m = n
| n = m ),
inference(resolution,[status(thm)],[p4310,p143]) ).
cnf(p4445,plain,
( j = k
| j = n
| n != k
| j = n
| j = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p4311]) ).
cnf(p4447,plain,
( j = k
| n != k
| j = n
| j = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p4445]) ).
cnf(p4451,plain,
( n != k
| n != k
| j = n
| j = m
| m = n
| n = m ),
inference(equality_factoring,[status(thm)],[p4447]) ).
cnf(p4454,plain,
( n != k
| j = n
| j = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p4451]) ).
cnf(p4455,plain,
( m = k
| m = n
| n = m
| j = n
| j = m
| m = n
| n = m ),
inference(resolution,[status(thm)],[p4454,p4052]) ).
cnf(p4459,plain,
( m = k
| m = n
| j = n
| j = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p4455]) ).
cnf(p4461,plain,
( m = k
| j = n
| j = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p4459]) ).
cnf(p17,plain,
( j != k
| ~ element(X0,j)
| X0 = j ),
inference(equality_factoring,[status(thm)],[c2]) ).
cnf(f1,negated_conjecture,
( element(Y,j)
| Y != k
| Y = j ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_2) ).
fof(f1_nnf,plain,
! [Y] :
( element(Y,j)
| Y != k
| Y = j ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [Y] :
( element(Y,j)
| Y != k
| Y = j ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( element(X0,j)
| X0 != k
| X0 = j ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p16,plain,
( element(k,j)
| k = j ),
inference(equality_resolution,[status(thm)],[c1]) ).
cnf(p21,plain,
( k = j
| j != k
| k = j ),
inference(resolution,[status(thm)],[p17,p16]) ).
cnf(p22,plain,
( j != k
| k = j ),
inference(factoring,[status(thm)],[p21]) ).
cnf(p4468,plain,
( n != k
| k = j
| m = k
| j = m
| m = n
| n = m ),
inference(superposition,[status(thm)],[p4461,p22]) ).
cnf(p4500,plain,
( n != k
| n != k
| k = j
| j = m
| m = n
| n = m ),
inference(equality_factoring,[status(thm)],[p4468]) ).
cnf(p4505,plain,
( n != k
| k = j
| j = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p4500]) ).
cnf(p4508,plain,
( m = k
| m = n
| n = m
| k = j
| j = m
| m = n
| n = m ),
inference(resolution,[status(thm)],[p4505,p4052]) ).
cnf(p4566,plain,
( m = k
| m = n
| k = j
| j = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p4508]) ).
cnf(p4568,plain,
( m = k
| k = j
| j = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p4566]) ).
cnf(p4572,plain,
( element(m,j)
| m = k
| m = k
| j = m
| m = n
| n = m ),
inference(superposition,[status(thm)],[p4568,p19]) ).
cnf(p4615,plain,
( element(m,j)
| m = k
| j = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p4572]) ).
cnf(p4618,plain,
( m = k
| m = j
| m = k
| j = m
| m = n
| n = m ),
inference(resolution,[status(thm)],[p4615,c2]) ).
cnf(p4626,plain,
( m = j
| m = k
| j = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p4618]) ).
cnf(p4630,plain,
( k != j
| m = k
| j = m
| m = n
| n = m ),
inference(equality_factoring,[status(thm)],[p4626]) ).
cnf(p4688,plain,
( m = k
| j = m
| m = n
| n = m
| m = k
| j = m
| m = n
| n = m ),
inference(resolution,[status(thm)],[p4630,p4568]) ).
cnf(p5955,plain,
( m = k
| j = m
| m = n
| m = k
| j = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p4688]) ).
cnf(p5959,plain,
( m = k
| j = m
| m = k
| j = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p5955]) ).
cnf(p5966,plain,
( m = k
| m = k
| j = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p5959]) ).
cnf(p5968,plain,
( m = k
| j = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p5966]) ).
cnf(p4055,plain,
( element(n,j)
| n = j
| m = k
| m = n
| n = m ),
inference(resolution,[status(thm)],[p4052,c1]) ).
cnf(p4152,plain,
( m != j
| element(n,j)
| m = k
| m = n
| n = m ),
inference(equality_factoring,[status(thm)],[p4055]) ).
cnf(p6014,plain,
( m != m
| element(n,j)
| m = k
| m = n
| n = m
| m = k
| m = n
| n = m ),
inference(superposition,[status(thm)],[p5968,p4152]) ).
cnf(p6417,plain,
( m != m
| element(n,j)
| m = k
| m = n
| m = k
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6014]) ).
cnf(p6420,plain,
( m != m
| element(n,j)
| m = k
| m = k
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6417]) ).
cnf(p6423,plain,
( m != m
| element(n,j)
| m = k
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6420]) ).
cnf(p6424,plain,
( element(n,j)
| m = k
| m = n
| n = m ),
inference(equality_resolution,[status(thm)],[p6423]) ).
cnf(p6427,plain,
( element(n,m)
| m = k
| m = n
| n = m
| m = k
| m = n
| n = m ),
inference(superposition,[status(thm)],[p5968,p6424]) ).
cnf(p6429,plain,
( element(n,m)
| m = k
| m = n
| m = k
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6427]) ).
cnf(p6432,plain,
( element(n,m)
| m = k
| m = k
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6429]) ).
cnf(p6434,plain,
( element(n,m)
| m = k
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6432]) ).
cnf(p6440,plain,
( element(f(n),n)
| n = m
| m = k
| m = n
| n = m ),
inference(resolution,[status(thm)],[p6434,c6]) ).
cnf(p6459,plain,
( element(f(n),n)
| m = k
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6440]) ).
cnf(p6472,plain,
( n != k
| f(n) = n
| f(n) = m
| m = n
| n = m
| m = k
| m = n
| n = m ),
inference(resolution,[status(thm)],[p6459,p4310]) ).
cnf(p6711,plain,
( n != k
| f(n) = n
| f(n) = m
| m = n
| m = k
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6472]) ).
cnf(p6713,plain,
( n != k
| f(n) = n
| f(n) = m
| m = k
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6711]) ).
cnf(p6718,plain,
( n != k
| n != k
| f(n) = n
| f(n) = m
| m = n
| n = m ),
inference(equality_factoring,[status(thm)],[p6713]) ).
cnf(p6721,plain,
( n != k
| f(n) = n
| f(n) = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6718]) ).
cnf(p6722,plain,
( m = k
| m = n
| n = m
| f(n) = n
| f(n) = m
| m = n
| n = m ),
inference(resolution,[status(thm)],[p6721,p4052]) ).
cnf(p6726,plain,
( m = k
| m = n
| f(n) = n
| f(n) = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6722]) ).
cnf(p6728,plain,
( m = k
| f(n) = n
| f(n) = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6726]) ).
cnf(p6438,plain,
( f(n) != n
| n = m
| m = k
| m = n
| n = m ),
inference(resolution,[status(thm)],[p6434,c4]) ).
cnf(p6446,plain,
( f(n) != n
| m = k
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6438]) ).
cnf(p6737,plain,
( m = k
| m = n
| n = m
| m = k
| f(n) = m
| m = n
| n = m ),
inference(resolution,[status(thm)],[p6728,p6446]) ).
cnf(p6746,plain,
( m = k
| m = n
| m = k
| f(n) = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6737]) ).
cnf(p6753,plain,
( m = k
| m = k
| f(n) = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6746]) ).
cnf(p6755,plain,
( m = k
| f(n) = m
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6753]) ).
cnf(p6437,plain,
( f(n) != m
| n = m
| m = k
| m = n
| n = m ),
inference(resolution,[status(thm)],[p6434,c3]) ).
cnf(p6441,plain,
( f(n) != m
| m = k
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6437]) ).
cnf(p6762,plain,
( m = k
| m = n
| n = m
| m = k
| m = n
| n = m ),
inference(resolution,[status(thm)],[p6755,p6441]) ).
cnf(p6775,plain,
( m = k
| m = n
| m = k
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6762]) ).
cnf(p6778,plain,
( m = k
| m = k
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6775]) ).
cnf(p6780,plain,
( m = k
| m = n
| n = m ),
inference(factoring,[status(thm)],[p6778]) ).
cnf(f0,negated_conjecture,
m != n,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_1) ).
fof(f0_nnf,plain,
m != n,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
m != n,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
m != n,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p6783,plain,
( m != m
| m = k
| m = n ),
inference(superposition,[status(thm)],[p6780,c0]) ).
cnf(p6861,plain,
( m = k
| m = n ),
inference(equality_resolution,[status(thm)],[p6783]) ).
cnf(p6867,plain,
( element(n,m)
| n = k
| m = n ),
inference(superposition,[status(thm)],[p6861,p20]) ).
cnf(p7089,plain,
( element(f(n),n)
| n = m
| n = k
| m = n ),
inference(resolution,[status(thm)],[p6867,c6]) ).
cnf(p7185,plain,
( m != k
| element(f(n),n)
| n = m
| m = n ),
inference(equality_factoring,[status(thm)],[p7089]) ).
cnf(p7200,plain,
( m = n
| element(f(n),n)
| n = m
| m = n ),
inference(resolution,[status(thm)],[p7185,p6861]) ).
cnf(p7216,plain,
( element(f(n),n)
| n = m
| m = n ),
inference(factoring,[status(thm)],[p7200]) ).
cnf(p7217,plain,
( ~ element(n,f(n))
| n = f(n)
| n = m
| element(f(n),m)
| f(n) = m
| n = m
| m = n ),
inference(resolution,[status(thm)],[p7216,c7]) ).
cnf(p7879,plain,
( ~ element(n,f(n))
| n = f(n)
| element(f(n),m)
| f(n) = m
| n = m
| m = n ),
inference(factoring,[status(thm)],[p7217]) ).
cnf(p7088,plain,
( element(n,f(n))
| n = m
| n = k
| m = n ),
inference(resolution,[status(thm)],[p6867,c5]) ).
cnf(p7173,plain,
( m != k
| element(n,f(n))
| n = m
| m = n ),
inference(equality_factoring,[status(thm)],[p7088]) ).
cnf(p7198,plain,
( m = n
| element(n,f(n))
| n = m
| m = n ),
inference(resolution,[status(thm)],[p7173,p6861]) ).
cnf(p7201,plain,
( element(n,f(n))
| n = m
| m = n ),
inference(factoring,[status(thm)],[p7198]) ).
cnf(p7881,plain,
( n = m
| m = n
| n = f(n)
| element(f(n),m)
| f(n) = m
| n = m
| m = n ),
inference(resolution,[status(thm)],[p7879,p7201]) ).
cnf(p7888,plain,
( n = m
| n = f(n)
| element(f(n),m)
| f(n) = m
| n = m
| m = n ),
inference(factoring,[status(thm)],[p7881]) ).
cnf(p7890,plain,
( n = f(n)
| element(f(n),m)
| f(n) = m
| n = m
| m = n ),
inference(factoring,[status(thm)],[p7888]) ).
cnf(p6870,plain,
( k != m
| ~ element(X0,m)
| X0 = n
| X0 = k
| m = n ),
inference(superposition,[status(thm)],[p6861,p36]) ).
cnf(p7899,plain,
( k != m
| f(n) = n
| f(n) = k
| m = n
| n = f(n)
| f(n) = m
| n = m
| m = n ),
inference(resolution,[status(thm)],[p7890,p6870]) ).
cnf(p8852,plain,
( k != m
| f(n) = n
| f(n) = k
| n = f(n)
| f(n) = m
| n = m
| m = n ),
inference(factoring,[status(thm)],[p7899]) ).
cnf(p8856,plain,
( k != m
| k != m
| f(n) = n
| f(n) = k
| n = f(n)
| n = m
| m = n ),
inference(equality_factoring,[status(thm)],[p8852]) ).
cnf(p8862,plain,
( k != m
| f(n) = n
| f(n) = k
| n = f(n)
| n = m
| m = n ),
inference(factoring,[status(thm)],[p8856]) ).
cnf(p8865,plain,
( m != m
| f(n) = n
| f(n) = k
| n = f(n)
| n = m
| m = n
| m = n ),
inference(superposition,[status(thm)],[p6861,p8862]) ).
cnf(p8873,plain,
( m != m
| f(n) = n
| f(n) = k
| n = f(n)
| n = m
| m = n ),
inference(factoring,[status(thm)],[p8865]) ).
cnf(p8875,plain,
( f(n) = n
| f(n) = k
| n = f(n)
| n = m
| m = n ),
inference(equality_resolution,[status(thm)],[p8873]) ).
cnf(p8879,plain,
( f(n) = n
| f(n) = m
| n = f(n)
| n = m
| m = n
| m = n ),
inference(superposition,[status(thm)],[p6861,p8875]) ).
cnf(p8891,plain,
( f(n) = n
| f(n) = m
| n = f(n)
| n = m
| m = n ),
inference(factoring,[status(thm)],[p8879]) ).
cnf(p7205,plain,
( ~ element(f(n),n)
| f(n) = n
| f(n) = m
| element(n,m)
| n = m
| n = m
| m = n ),
inference(resolution,[status(thm)],[p7201,c7]) ).
cnf(p7746,plain,
( ~ element(f(n),n)
| f(n) = n
| f(n) = m
| element(n,m)
| n = m
| m = n ),
inference(factoring,[status(thm)],[p7205]) ).
cnf(p7748,plain,
( n = m
| m = n
| f(n) = n
| f(n) = m
| element(n,m)
| n = m
| m = n ),
inference(resolution,[status(thm)],[p7746,p7216]) ).
cnf(p7751,plain,
( n = m
| f(n) = n
| f(n) = m
| element(n,m)
| n = m
| m = n ),
inference(factoring,[status(thm)],[p7748]) ).
cnf(p7753,plain,
( f(n) = n
| f(n) = m
| element(n,m)
| n = m
| m = n ),
inference(factoring,[status(thm)],[p7751]) ).
cnf(p7087,plain,
( f(n) != n
| n = m
| n = k
| m = n ),
inference(resolution,[status(thm)],[p6867,c4]) ).
cnf(p7171,plain,
( m != k
| f(n) != n
| n = m
| m = n ),
inference(equality_factoring,[status(thm)],[p7087]) ).
cnf(p7755,plain,
( m != k
| n = m
| m = n
| f(n) = m
| element(n,m)
| n = m
| m = n ),
inference(resolution,[status(thm)],[p7753,p7171]) ).
cnf(p7786,plain,
( m != k
| n = m
| f(n) = m
| element(n,m)
| n = m
| m = n ),
inference(factoring,[status(thm)],[p7755]) ).
cnf(p7788,plain,
( m != k
| f(n) = m
| element(n,m)
| n = m
| m = n ),
inference(factoring,[status(thm)],[p7786]) ).
cnf(p7789,plain,
( m = n
| f(n) = m
| element(n,m)
| n = m
| m = n ),
inference(resolution,[status(thm)],[p7788,p6861]) ).
cnf(p7790,plain,
( f(n) = m
| element(n,m)
| n = m
| m = n ),
inference(factoring,[status(thm)],[p7789]) ).
cnf(p7086,plain,
( f(n) != m
| n = m
| n = k
| m = n ),
inference(resolution,[status(thm)],[p6867,c3]) ).
cnf(p7156,plain,
( m != k
| f(n) != m
| n = m
| m = n ),
inference(equality_factoring,[status(thm)],[p7086]) ).
cnf(p7807,plain,
( m != k
| n = m
| m = n
| element(n,m)
| n = m
| m = n ),
inference(resolution,[status(thm)],[p7790,p7156]) ).
cnf(p7814,plain,
( m != k
| n = m
| element(n,m)
| n = m
| m = n ),
inference(factoring,[status(thm)],[p7807]) ).
cnf(p7816,plain,
( m != k
| element(n,m)
| n = m
| m = n ),
inference(factoring,[status(thm)],[p7814]) ).
cnf(p7823,plain,
( m = n
| element(n,m)
| n = m
| m = n ),
inference(resolution,[status(thm)],[p7816,p6861]) ).
cnf(p7824,plain,
( element(n,m)
| n = m
| m = n ),
inference(factoring,[status(thm)],[p7823]) ).
cnf(p7826,plain,
( f(n) != n
| n = m
| n = m
| m = n ),
inference(resolution,[status(thm)],[p7824,c4]) ).
cnf(p7829,plain,
( f(n) != n
| n = m
| m = n ),
inference(factoring,[status(thm)],[p7826]) ).
cnf(p8897,plain,
( n = m
| m = n
| f(n) = m
| n = f(n)
| n = m
| m = n ),
inference(resolution,[status(thm)],[p8891,p7829]) ).
cnf(p8898,plain,
( n = m
| f(n) = m
| n = f(n)
| n = m
| m = n ),
inference(factoring,[status(thm)],[p8897]) ).
cnf(p8901,plain,
( f(n) = m
| n = f(n)
| n = m
| m = n ),
inference(factoring,[status(thm)],[p8898]) ).
cnf(p7825,plain,
( f(n) != m
| n = m
| n = m
| m = n ),
inference(resolution,[status(thm)],[p7824,c3]) ).
cnf(p7827,plain,
( f(n) != m
| n = m
| m = n ),
inference(factoring,[status(thm)],[p7825]) ).
cnf(p8906,plain,
( n = m
| m = n
| n = f(n)
| n = m
| m = n ),
inference(resolution,[status(thm)],[p8901,p7827]) ).
cnf(p8909,plain,
( n = m
| n = f(n)
| n = m
| m = n ),
inference(factoring,[status(thm)],[p8906]) ).
cnf(p8912,plain,
( n = f(n)
| n = m
| m = n ),
inference(factoring,[status(thm)],[p8909]) ).
cnf(p8922,plain,
( n != n
| n = m
| m = n
| n = m
| m = n ),
inference(superposition,[status(thm)],[p8912,p7829]) ).
cnf(p8936,plain,
( n != n
| n = m
| n = m
| m = n ),
inference(factoring,[status(thm)],[p8922]) ).
cnf(p8942,plain,
( n != n
| n = m
| m = n ),
inference(factoring,[status(thm)],[p8936]) ).
cnf(p8943,plain,
( n = m
| m = n ),
inference(equality_resolution,[status(thm)],[p8942]) ).
cnf(p8944,plain,
( m != m
| m = n ),
inference(superposition,[status(thm)],[p8943,c0]) ).
cnf(p8987,plain,
m = n,
inference(equality_resolution,[status(thm)],[p8944]) ).
cnf(p8992,plain,
$false,
inference(resolution,[status(thm)],[p8987,c0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN015-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n005.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Thu Sep 24 23:51:17 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 18.64/5.91 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.64/5.91 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------