%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU451+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n017.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 02:52:10 PM UTC 2026
% Result : Theorem 154.48s 20.05s
% Output : Proof 154.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 15
% Syntax : Number of formulae : 128 ( 85 unt; 0 def)
% Number of atoms : 190 ( 97 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 124 ( 62 ~; 36 |; 18 &)
% ( 1 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-6 aty)
% Number of variables : 181 ( 5 sgn 96 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f0,conjecture,
! [A,B,C] :
( m2_relset_1(C,A,B)
=> k9_relset_2(A,A,B,k6_partfun1(A),C) = k9_relset_2(A,B,B,C,k6_partfun1(B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t65_relset_2) ).
fof(f0_neg,negated_conjecture,
~ ! [A,B,C] :
( m2_relset_1(C,A,B)
=> k9_relset_2(A,A,B,k6_partfun1(A),C) = k9_relset_2(A,B,B,C,k6_partfun1(B)) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
? [A,B,C] :
( k9_relset_2(A,A,B,k6_partfun1(A),C) != k9_relset_2(A,B,B,C,k6_partfun1(B))
& m2_relset_1(C,A,B) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
( k9_relset_2(sk0,sk0,sk1,k6_partfun1(sk0),sk2) != k9_relset_2(sk0,sk1,sk1,sk2,k6_partfun1(sk1))
& m2_relset_1(sk2,sk0,sk1) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f0_nnf]) ).
cnf(c1,plain,
k9_relset_2(sk0,sk0,sk1,k6_partfun1(sk0),sk2) != k9_relset_2(sk0,sk1,sk1,sk2,k6_partfun1(sk1)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t231,plain,
eq(k9_relset_2(sk0,sk0,sk1,k6_partfun1(sk0),sk2),k9_relset_2(sk0,sk1,sk1,sk2,k6_partfun1(sk1))) = false,
inference(equality_encoding,[status(esa)],[c1]) ).
fof(f34,axiom,
! [A] : k6_partfun1(A) = k6_relat_1(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k6_partfun1) ).
fof(f34_nnf,plain,
! [A] : k6_partfun1(A) = k6_relat_1(A),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [A] : k6_partfun1(A) = k6_relat_1(A),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c60,plain,
k6_partfun1(X0) = k6_relat_1(X0),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(t43,plain,
k6_relat_1(X1) = k6_partfun1(X1),
inference(equality_encoding,[status(esa)],[c60]) ).
cnf(t1482,plain,
k6_partfun1(X1) = k6_relat_1(X1),
inference(orient,[status(thm)],[t43]) ).
cnf(t37460,plain,
eq(k9_relset_2(sk0,sk0,sk1,k6_relat_1(sk0),sk2),k9_relset_2(sk0,sk1,sk1,sk2,k6_partfun1(sk1))) = false,
inference(step,[status(thm)],[t231,t1482]) ).
cnf(t37461,plain,
eq(k9_relset_2(sk0,sk0,sk1,k6_relat_1(sk0),sk2),k9_relset_2(sk0,sk1,sk1,sk2,k6_relat_1(sk1))) = false,
inference(step,[status(thm)],[t37460,t1482]) ).
cnf(t1503,plain,
eq(k9_relset_2(sk0,sk0,sk1,k6_relat_1(sk0),sk2),k9_relset_2(sk0,sk1,sk1,sk2,k6_relat_1(sk1))) = false,
inference(orient,[status(thm)],[t37461]) ).
fof(f15,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
=> m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f15_nnf,plain,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
| ~ m2_relset_1(C,A,B) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [C,A,B] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
| ~ m2_relset_1(C,A,B) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c18,plain,
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(hi11,axiom,
ifeq(m2_relset_1(X0,X1,X2),true,m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))),true) = true,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(c0,plain,
m2_relset_1(sk2,sk0,sk1),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi0,negated_conjecture,
m2_relset_1(sk2,sk0,sk1) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(h3,plain,
m1_subset_1(sk2,k1_zfmisc_1(k2_zfmisc_1(sk0,sk1))) = true,
inference(hyper_resolution,[status(thm)],[hi11,hi0]) ).
fof(f9,axiom,
! [A] :
( m2_relset_1(k6_partfun1(A),A,A)
& v1_partfun1(k6_partfun1(A),A,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_partfun1) ).
fof(f9_nnf,plain,
! [A] :
( m2_relset_1(k6_partfun1(A),A,A)
& v1_partfun1(k6_partfun1(A),A,A) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [A] :
( m2_relset_1(k6_partfun1(A),A,A)
& v1_partfun1(k6_partfun1(A),A,A) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c12,plain,
m2_relset_1(k6_partfun1(X0),X0,X0),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(hi7,axiom,
m2_relset_1(k6_partfun1(X0),X0,X0) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(hi6,axiom,
k6_partfun1(X0) = k6_relat_1(X0),
inference(equality_encoding,[status(esa)],[c60]) ).
cnf(h6,plain,
m1_subset_1(k6_partfun1(V0),k1_zfmisc_1(k2_zfmisc_1(V0,V0))) = true,
inference(hyper_resolution,[status(thm)],[hi11,hi7,hi6]) ).
fof(f36,axiom,
! [A,B,C,D,E] :
( ( m1_subset_1(E,k1_zfmisc_1(k2_zfmisc_1(B,C)))
& m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(A,B))) )
=> k9_relset_2(A,B,C,D,E) = k5_relat_1(D,E) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k9_relset_2) ).
fof(f36_nnf,plain,
! [A,B,C,D,E] :
( k9_relset_2(A,B,C,D,E) = k5_relat_1(D,E)
| ~ m1_subset_1(E,k1_zfmisc_1(k2_zfmisc_1(B,C)))
| ~ m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [D,A,B,E,C] :
( k9_relset_2(A,B,C,D,E) = k5_relat_1(D,E)
| ~ m1_subset_1(E,k1_zfmisc_1(k2_zfmisc_1(B,C)))
| ~ m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c62,plain,
( k9_relset_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(hi52,axiom,
ifeq(m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))),true,ifeq(m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X2,X4))),true,k9_relset_2(X1,X2,X4,X0,X3),k5_relat_1(X0,X3)),k5_relat_1(X0,X3)) = k5_relat_1(X0,X3),
inference(equality_encoding,[status(esa)],[c62]) ).
cnf(t168,plain,
k9_relset_2(sk0,sk0,sk1,k6_partfun1(sk0),sk2) = k5_relat_1(k6_partfun1(sk0),sk2),
inference(hyper_resolution,[status(thm)],[hi52,h6,h3]) ).
cnf(t1406,plain,
k9_relset_2(sk0,sk0,sk1,k6_partfun1(sk0),sk2) = k5_relat_1(k6_partfun1(sk0),sk2),
inference(orient,[status(thm)],[t168]) ).
cnf(t37447,plain,
k9_relset_2(sk0,sk0,sk1,k6_relat_1(sk0),sk2) = k5_relat_1(k6_partfun1(sk0),sk2),
inference(step,[status(thm)],[t1406,t1482]) ).
cnf(t37448,plain,
k9_relset_2(sk0,sk0,sk1,k6_relat_1(sk0),sk2) = k5_relat_1(k6_relat_1(sk0),sk2),
inference(step,[status(thm)],[t37447,t1482]) ).
cnf(t1493,plain,
k9_relset_2(sk0,sk0,sk1,k6_relat_1(sk0),sk2) = k5_relat_1(k6_relat_1(sk0),sk2),
inference(rw,[status(thm)],[t37448]) ).
fof(f35,axiom,
! [A,B,C,D,E,F] :
( ( m1_relset_1(F,C,D)
& m1_relset_1(E,A,B) )
=> k7_relset_1(A,B,C,D,E,F) = k5_relat_1(E,F) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k7_relset_1) ).
fof(f35_nnf,plain,
! [A,B,C,D,E,F] :
( k7_relset_1(A,B,C,D,E,F) = k5_relat_1(E,F)
| ~ m1_relset_1(F,C,D)
| ~ m1_relset_1(E,A,B) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
! [E,A,B,F,C,D] :
( k7_relset_1(A,B,C,D,E,F) = k5_relat_1(E,F)
| ~ m1_relset_1(F,C,D)
| ~ m1_relset_1(E,A,B) ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c61,plain,
( k7_relset_1(X0,X1,X2,X3,X4,X5) = k5_relat_1(X4,X5)
| ~ m1_relset_1(X5,X2,X3)
| ~ m1_relset_1(X4,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(t252,plain,
ifeq(m1_relset_1(X1,X2,X3),true,ifeq(m1_relset_1(X4,X5,X6),true,k7_relset_1(X2,X3,X5,X6,X1,X4),k5_relat_1(X1,X4)),k5_relat_1(X1,X4)) = k5_relat_1(X1,X4),
inference(equality_encoding,[status(esa)],[c61]) ).
cnf(t1257,plain,
ifeq(m1_relset_1(X1,X2,X3),true,ifeq(m1_relset_1(X4,X5,X6),true,k7_relset_1(X2,X3,X5,X6,X1,X4),k5_relat_1(X1,X4)),k5_relat_1(X1,X4)) = k5_relat_1(X1,X4),
inference(orient,[status(thm)],[t252]) ).
fof(f40,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
=> ( k7_relset_1(A,B,B,B,C,k6_partfun1(B)) = C
& k7_relset_1(A,A,A,B,k6_partfun1(A),C) = C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t23_funct_2) ).
fof(f40_nnf,plain,
! [A,B,C] :
( ( k7_relset_1(A,B,B,B,C,k6_partfun1(B)) = C
& k7_relset_1(A,A,A,B,k6_partfun1(A),C) = C )
| ~ m2_relset_1(C,A,B) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [C,A,B] :
( ( k7_relset_1(A,B,B,B,C,k6_partfun1(B)) = C
& k7_relset_1(A,A,A,B,k6_partfun1(A),C) = C )
| ~ m2_relset_1(C,A,B) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c67,plain,
( k7_relset_1(X0,X0,X0,X1,k6_partfun1(X0),X2) = X2
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(hi57,axiom,
ifeq(m2_relset_1(X0,X1,X2),true,k7_relset_1(X1,X1,X1,X2,k6_partfun1(X1),X0),X0) = X0,
inference(equality_encoding,[status(esa)],[c67]) ).
cnf(t155,plain,
k7_relset_1(sk0,sk0,sk0,sk1,k6_partfun1(sk0),sk2) = sk2,
inference(hyper_resolution,[status(thm)],[hi57,hi0,hi6]) ).
cnf(t1417,plain,
k7_relset_1(sk0,sk0,sk0,sk1,k6_partfun1(sk0),sk2) = sk2,
inference(orient,[status(thm)],[t155]) ).
cnf(t37446,plain,
k7_relset_1(sk0,sk0,sk0,sk1,k6_relat_1(sk0),sk2) = sk2,
inference(step,[status(thm)],[t1417,t1482]) ).
cnf(t1492,plain,
k7_relset_1(sk0,sk0,sk0,sk1,k6_relat_1(sk0),sk2) = sk2,
inference(rw,[status(thm)],[t37446]) ).
cnf(t1724,plain,
k7_relset_1(sk0,sk0,sk0,sk1,k6_relat_1(sk0),sk2) = sk2,
inference(orient,[status(thm)],[t1492]) ).
cnf(t1725,plain,
k5_relat_1(k6_relat_1(sk0),sk2) = ifeq(m1_relset_1(k6_relat_1(sk0),sk0,sk0),true,ifeq(m1_relset_1(sk2,sk0,sk1),true,sk2,k5_relat_1(k6_relat_1(sk0),sk2)),k5_relat_1(k6_relat_1(sk0),sk2)),
inference(cp,[status(thm)],[t1257,t1724]) ).
fof(f37,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f37_nnf,plain,
! [A,B,C] :
( ( ~ m1_relset_1(C,A,B)
| m2_relset_1(C,A,B) )
& ( m1_relset_1(C,A,B)
| ~ m2_relset_1(C,A,B) ) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [C,A,B] :
( ( ~ m1_relset_1(C,A,B)
| m2_relset_1(C,A,B) )
& ( m1_relset_1(C,A,B)
| ~ m2_relset_1(C,A,B) ) ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c63,plain,
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(hi53,axiom,
ifeq(m2_relset_1(X0,X1,X2),true,m1_relset_1(X0,X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c63]) ).
cnf(t126,plain,
m1_relset_1(k6_partfun1(X1),X1,X1) = true,
inference(hyper_resolution,[status(thm)],[hi53,hi7,hi6]) ).
cnf(t1116,plain,
m1_relset_1(k6_partfun1(X1),X1,X1) = true,
inference(orient,[status(thm)],[t126]) ).
cnf(t37455,plain,
m1_relset_1(k6_relat_1(X1),X1,X1) = true,
inference(step,[status(thm)],[t1116,t1482]) ).
cnf(t1498,plain,
m1_relset_1(k6_relat_1(X1),X1,X1) = true,
inference(rw,[status(thm)],[t37455]) ).
cnf(t1547,plain,
m1_relset_1(k6_relat_1(X1),X1,X1) = true,
inference(orient,[status(thm)],[t1498]) ).
cnf(t37526,plain,
k5_relat_1(k6_relat_1(sk0),sk2) = ifeq(true,true,ifeq(m1_relset_1(sk2,sk0,sk1),true,sk2,k5_relat_1(k6_relat_1(sk0),sk2)),k5_relat_1(k6_relat_1(sk0),sk2)),
inference(step,[status(thm)],[t1725,t1547]) ).
cnf(t111,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t111]) ).
cnf(t37527,plain,
k5_relat_1(k6_relat_1(sk0),sk2) = ifeq(m1_relset_1(sk2,sk0,sk1),true,sk2,k5_relat_1(k6_relat_1(sk0),sk2)),
inference(step,[status(thm)],[t37526,t256]) ).
cnf(t76,plain,
m1_relset_1(sk2,sk0,sk1) = true,
inference(hyper_resolution,[status(thm)],[hi53,hi0]) ).
cnf(t1076,plain,
m1_relset_1(sk2,sk0,sk1) = true,
inference(orient,[status(thm)],[t76]) ).
cnf(t37528,plain,
k5_relat_1(k6_relat_1(sk0),sk2) = ifeq(true,true,sk2,k5_relat_1(k6_relat_1(sk0),sk2)),
inference(step,[status(thm)],[t37527,t1076]) ).
cnf(t37529,plain,
k5_relat_1(k6_relat_1(sk0),sk2) = sk2,
inference(step,[status(thm)],[t37528,t256]) ).
cnf(t1726,plain,
k5_relat_1(k6_relat_1(sk0),sk2) = sk2,
inference(orient,[status(thm)],[t37529]) ).
cnf(t37538,plain,
k9_relset_2(sk0,sk0,sk1,k6_relat_1(sk0),sk2) = sk2,
inference(step,[status(thm)],[t1493,t1726]) ).
cnf(t1758,plain,
k9_relset_2(sk0,sk0,sk1,k6_relat_1(sk0),sk2) = sk2,
inference(orient,[status(thm)],[t37538]) ).
cnf(t37539,plain,
eq(sk2,k9_relset_2(sk0,sk1,sk1,sk2,k6_relat_1(sk1))) = false,
inference(step,[status(thm)],[t1503,t1758]) ).
cnf(t1759,plain,
eq(sk2,k9_relset_2(sk0,sk1,sk1,sk2,k6_relat_1(sk1))) = false,
inference(rw,[status(thm)],[t37539]) ).
cnf(t169,plain,
k9_relset_2(sk0,sk1,sk1,sk2,k6_partfun1(sk1)) = k5_relat_1(sk2,k6_partfun1(sk1)),
inference(hyper_resolution,[status(thm)],[hi52,h3,h6]) ).
cnf(t1371,plain,
k9_relset_2(sk0,sk1,sk1,sk2,k6_partfun1(sk1)) = k5_relat_1(sk2,k6_partfun1(sk1)),
inference(orient,[status(thm)],[t169]) ).
cnf(t37451,plain,
k9_relset_2(sk0,sk1,sk1,sk2,k6_relat_1(sk1)) = k5_relat_1(sk2,k6_partfun1(sk1)),
inference(step,[status(thm)],[t1371,t1482]) ).
cnf(t37452,plain,
k9_relset_2(sk0,sk1,sk1,sk2,k6_relat_1(sk1)) = k5_relat_1(sk2,k6_relat_1(sk1)),
inference(step,[status(thm)],[t37451,t1482]) ).
cnf(t1495,plain,
k9_relset_2(sk0,sk1,sk1,sk2,k6_relat_1(sk1)) = k5_relat_1(sk2,k6_relat_1(sk1)),
inference(rw,[status(thm)],[t37452]) ).
cnf(c68,plain,
( k7_relset_1(X0,X1,X1,X1,X2,k6_partfun1(X1)) = X2
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(hi58,axiom,
ifeq(m2_relset_1(X0,X1,X2),true,k7_relset_1(X1,X2,X2,X2,X0,k6_partfun1(X2)),X0) = X0,
inference(equality_encoding,[status(esa)],[c68]) ).
cnf(t156,plain,
k7_relset_1(sk0,sk1,sk1,sk1,sk2,k6_partfun1(sk1)) = sk2,
inference(hyper_resolution,[status(thm)],[hi58,hi0,hi6]) ).
cnf(t1419,plain,
k7_relset_1(sk0,sk1,sk1,sk1,sk2,k6_partfun1(sk1)) = sk2,
inference(orient,[status(thm)],[t156]) ).
cnf(t37445,plain,
k7_relset_1(sk0,sk1,sk1,sk1,sk2,k6_relat_1(sk1)) = sk2,
inference(step,[status(thm)],[t1419,t1482]) ).
cnf(t1491,plain,
k7_relset_1(sk0,sk1,sk1,sk1,sk2,k6_relat_1(sk1)) = sk2,
inference(rw,[status(thm)],[t37445]) ).
cnf(t1714,plain,
k7_relset_1(sk0,sk1,sk1,sk1,sk2,k6_relat_1(sk1)) = sk2,
inference(orient,[status(thm)],[t1491]) ).
cnf(t1715,plain,
k5_relat_1(sk2,k6_relat_1(sk1)) = ifeq(m1_relset_1(sk2,sk0,sk1),true,ifeq(m1_relset_1(k6_relat_1(sk1),sk1,sk1),true,sk2,k5_relat_1(sk2,k6_relat_1(sk1))),k5_relat_1(sk2,k6_relat_1(sk1))),
inference(cp,[status(thm)],[t1257,t1714]) ).
cnf(t37520,plain,
k5_relat_1(sk2,k6_relat_1(sk1)) = ifeq(true,true,ifeq(m1_relset_1(k6_relat_1(sk1),sk1,sk1),true,sk2,k5_relat_1(sk2,k6_relat_1(sk1))),k5_relat_1(sk2,k6_relat_1(sk1))),
inference(step,[status(thm)],[t1715,t1076]) ).
cnf(t37521,plain,
k5_relat_1(sk2,k6_relat_1(sk1)) = ifeq(m1_relset_1(k6_relat_1(sk1),sk1,sk1),true,sk2,k5_relat_1(sk2,k6_relat_1(sk1))),
inference(step,[status(thm)],[t37520,t256]) ).
cnf(t37522,plain,
k5_relat_1(sk2,k6_relat_1(sk1)) = ifeq(true,true,sk2,k5_relat_1(sk2,k6_relat_1(sk1))),
inference(step,[status(thm)],[t37521,t1547]) ).
cnf(t37523,plain,
k5_relat_1(sk2,k6_relat_1(sk1)) = sk2,
inference(step,[status(thm)],[t37522,t256]) ).
cnf(t1716,plain,
k5_relat_1(sk2,k6_relat_1(sk1)) = sk2,
inference(orient,[status(thm)],[t37523]) ).
cnf(t37540,plain,
k9_relset_2(sk0,sk1,sk1,sk2,k6_relat_1(sk1)) = sk2,
inference(step,[status(thm)],[t1495,t1716]) ).
cnf(t1760,plain,
k9_relset_2(sk0,sk1,sk1,sk2,k6_relat_1(sk1)) = sk2,
inference(orient,[status(thm)],[t37540]) ).
cnf(t38920,plain,
eq(sk2,sk2) = false,
inference(step,[status(thm)],[t1759,t1760]) ).
cnf(t15,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t977,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t15]) ).
cnf(t38921,plain,
true = false,
inference(step,[status(thm)],[t38920,t977]) ).
cnf(t37346,plain,
false = true,
inference(orient,[status(thm)],[t38921]) ).
fof(f1,axiom,
! [A,B] :
( r2_hidden(A,B)
=> ~ r2_hidden(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(f1_nnf,plain,
! [A,B] :
( ~ r2_hidden(B,A)
| ~ r2_hidden(A,B) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B] :
( ~ r2_hidden(B,A)
| ~ r2_hidden(A,B) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c2,plain,
( ~ r2_hidden(X1,X0)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(f21,axiom,
! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f21_nnf,plain,
! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c27,plain,
~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
fof(f30,axiom,
? [A] :
( v1_relat_1(A)
& ~ v1_xboole_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f30_nnf,plain,
? [A] :
( v1_relat_1(A)
& ~ v1_xboole_0(A) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
( v1_relat_1(sk9)
& ~ v1_xboole_0(sk9) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk9])],[f30_nnf]) ).
cnf(c47,plain,
~ v1_xboole_0(sk9),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
fof(f44,axiom,
! [A,B,C] :
~ ( v1_xboole_0(C)
& m1_subset_1(B,k1_zfmisc_1(C))
& r2_hidden(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
fof(f44_nnf,plain,
! [A,B,C] :
( ~ v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [A,B,C] :
( ~ v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c73,plain,
( ~ v1_xboole_0(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
fof(f46,axiom,
! [A,B] :
~ ( v1_xboole_0(B)
& r2_hidden(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f46_nnf,plain,
! [A,B] :
( ~ v1_xboole_0(B)
| ~ r2_hidden(A,B) ),
inference(nnf_transformation,[status(thm)],[f46]) ).
fof(f46_sk,plain,
! [A,B] :
( ~ v1_xboole_0(B)
| ~ r2_hidden(A,B) ),
inference(skolemisation,[status(esa)],[f46_nnf]) ).
cnf(c75,plain,
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c1,c2,c27,c47,c73,c75]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t37346]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU451+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.20/0.44 % Computer : n017.cluster.edu
% 0.20/0.44 % Model : x86_64 x86_64
% 0.20/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.44 % Memory : 8046.5625MB
% 0.20/0.44 % OS : Linux 6.8.0-71-generic
% 0.20/0.44 % CPULimit : 300
% 0.20/0.44 % WCLimit : 300
% 0.20/0.44 % DateTime : Thu Sep 24 14:16:02 UTC 2026
% 0.20/0.44 % CPUTime :
% 0.20/0.44 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 154.48/20.05 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 154.48/20.05 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------