%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : TOP023+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 03:54:40 PM UTC 2026
% Result : Theorem 30.78s 4.38s
% Output : Proof 30.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 5
% Syntax : Number of formulae : 81 ( 16 unt; 0 def)
% Number of atoms : 311 ( 60 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 382 ( 152 ~; 172 |; 35 &)
% ( 1 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 101 ( 3 sgn 44 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f45,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( l1_pre_topc(B)
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))
=> ( ( v1_tsp_1(C,A)
& C = D
& g1_pre_topc(u1_struct_0(A),u1_pre_topc(A)) = g1_pre_topc(u1_struct_0(B),u1_pre_topc(B)) )
=> v1_tsp_1(D,B) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_tsp_1) ).
fof(f45_nnf,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( v1_tsp_1(D,B)
| ~ v1_tsp_1(C,A)
| C != D
| g1_pre_topc(u1_struct_0(A),u1_pre_topc(A)) != g1_pre_topc(u1_struct_0(B),u1_pre_topc(B))
| ~ m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) )
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(B) )
| ~ l1_pre_topc(A) ),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
! [A,B,C,D] :
( v1_tsp_1(D,B)
| ~ v1_tsp_1(C,A)
| C != D
| g1_pre_topc(u1_struct_0(A),u1_pre_topc(A)) != g1_pre_topc(u1_struct_0(B),u1_pre_topc(B))
| ~ m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_pre_topc(B)
| ~ l1_pre_topc(A) ),
inference(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c104,plain,
( v1_tsp_1(X3,X1)
| ~ v1_tsp_1(X2,X0)
| X2 != X3
| g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1))
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
fof(f0,conjecture,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( l1_pre_topc(B)
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))
=> ( ( v1_tsp_2(C,A)
& C = D
& g1_pre_topc(u1_struct_0(A),u1_pre_topc(A)) = g1_pre_topc(u1_struct_0(B),u1_pre_topc(B)) )
=> v1_tsp_2(D,B) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_tsp_2) ).
fof(f0_neg,negated_conjecture,
~ ! [A] :
( l1_pre_topc(A)
=> ! [B] :
( l1_pre_topc(B)
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))
=> ( ( v1_tsp_2(C,A)
& C = D
& g1_pre_topc(u1_struct_0(A),u1_pre_topc(A)) = g1_pre_topc(u1_struct_0(B),u1_pre_topc(B)) )
=> v1_tsp_2(D,B) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ~ v1_tsp_2(D,B)
& v1_tsp_2(C,A)
& C = D
& g1_pre_topc(u1_struct_0(A),u1_pre_topc(A)) = g1_pre_topc(u1_struct_0(B),u1_pre_topc(B))
& m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) )
& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) )
& l1_pre_topc(B) )
& l1_pre_topc(A) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
( ~ v1_tsp_2(sk3,sk1)
& v1_tsp_2(sk2,sk0)
& sk2 = sk3
& g1_pre_topc(u1_struct_0(sk0),u1_pre_topc(sk0)) = g1_pre_topc(u1_struct_0(sk1),u1_pre_topc(sk1))
& m1_subset_1(sk3,k1_zfmisc_1(u1_struct_0(sk1)))
& m1_subset_1(sk2,k1_zfmisc_1(u1_struct_0(sk0)))
& l1_pre_topc(sk1)
& l1_pre_topc(sk0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3])],[f0_nnf]) ).
cnf(c0,plain,
l1_pre_topc(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p487,plain,
( v1_tsp_1(X2,X0)
| ~ v1_tsp_1(X1,sk0)
| X1 != X2
| g1_pre_topc(u1_struct_0(sk0),u1_pre_topc(sk0)) != g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ l1_pre_topc(X0) ),
inference(resolution,[status(thm)],[c104,c0]) ).
cnf(c1,plain,
l1_pre_topc(sk1),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1151,plain,
( v1_tsp_1(X1,sk1)
| ~ v1_tsp_1(X0,sk0)
| X0 != X1
| g1_pre_topc(u1_struct_0(sk0),u1_pre_topc(sk0)) != g1_pre_topc(u1_struct_0(sk0),u1_pre_topc(sk0))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0))) ),
inference(resolution,[status(thm)],[p487,c1]) ).
cnf(p2514,plain,
( v1_tsp_1(X1,sk1)
| ~ v1_tsp_1(X0,sk0)
| X0 != X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0))) ),
inference(equality_resolution,[status(thm)],[p1151]) ).
cnf(p2515,plain,
( v1_tsp_1(X0,sk1)
| ~ v1_tsp_1(X0,sk0)
| X0 != X0
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0))) ),
inference(factoring,[status(thm)],[p2514]) ).
cnf(p2523,plain,
( v1_tsp_1(X0,sk1)
| ~ v1_tsp_1(X0,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0))) ),
inference(equality_resolution,[status(thm)],[p2515]) ).
cnf(c2,plain,
m1_subset_1(sk2,k1_zfmisc_1(u1_struct_0(sk0))),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2524,plain,
( v1_tsp_1(sk2,sk1)
| ~ v1_tsp_1(sk2,sk0) ),
inference(resolution,[status(thm)],[p2523,c2]) ).
fof(f19,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v1_tsp_2(B,A)
<=> ( ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
=> ( ( r1_tarski(B,C)
& v1_tsp_1(C,A) )
=> B = C ) )
& v1_tsp_1(B,A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_tsp_2) ).
fof(f19_nnf,plain,
! [A] :
( ! [B] :
( ( ( ? [C] :
( B != C
& r1_tarski(B,C)
& v1_tsp_1(C,A)
& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) )
| ~ v1_tsp_1(B,A)
| v1_tsp_2(B,A) )
& ( ( ! [C] :
( B = C
| ~ r1_tarski(B,C)
| ~ v1_tsp_1(C,A)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) )
& v1_tsp_1(B,A) )
| ~ v1_tsp_2(B,A) ) )
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [A,B,C] :
( ( ( ( B != sk4(A,B)
& r1_tarski(B,sk4(A,B))
& v1_tsp_1(sk4(A,B),A)
& m1_subset_1(sk4(A,B),k1_zfmisc_1(u1_struct_0(A))) )
| ~ v1_tsp_1(B,A)
| v1_tsp_2(B,A) )
& ( ( ( B = C
| ~ r1_tarski(B,C)
| ~ v1_tsp_1(C,A)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) )
& v1_tsp_1(B,A) )
| ~ v1_tsp_2(B,A) ) )
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_pre_topc(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk4])],[f19_nnf]) ).
cnf(c50,plain,
( v1_tsp_1(X1,X0)
| ~ v1_tsp_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p263,plain,
( v1_tsp_1(X0,sk0)
| ~ v1_tsp_2(X0,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0))) ),
inference(resolution,[status(thm)],[c50,c0]) ).
cnf(p623,plain,
( v1_tsp_1(sk2,sk0)
| ~ v1_tsp_2(sk2,sk0) ),
inference(resolution,[status(thm)],[p263,c2]) ).
cnf(c6,plain,
v1_tsp_2(sk2,sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p626,plain,
v1_tsp_1(sk2,sk0),
inference(resolution,[status(thm)],[p623,c6]) ).
cnf(p2530,plain,
v1_tsp_1(sk2,sk1),
inference(resolution,[status(thm)],[p2524,p626]) ).
cnf(c4,plain,
g1_pre_topc(u1_struct_0(sk0),u1_pre_topc(sk0)) = g1_pre_topc(u1_struct_0(sk1),u1_pre_topc(sk1)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
fof(f26,axiom,
! [A] :
( l1_pre_topc(A)
=> m1_subset_1(u1_pre_topc(A),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u1_pre_topc) ).
fof(f26_nnf,plain,
! [A] :
( m1_subset_1(u1_pre_topc(A),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A))))
| ~ l1_pre_topc(A) ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [A] :
( m1_subset_1(u1_pre_topc(A),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A))))
| ~ l1_pre_topc(A) ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c63,plain,
( m1_subset_1(u1_pre_topc(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0))))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(p320,plain,
m1_subset_1(u1_pre_topc(sk1),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sk1)))),
inference(resolution,[status(thm)],[c63,c1]) ).
fof(f33,axiom,
! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
=> ! [C,D] :
( g1_pre_topc(A,B) = g1_pre_topc(C,D)
=> ( B = D
& A = C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',free_g1_pre_topc) ).
fof(f33_nnf,plain,
! [A,B] :
( ! [C,D] :
( ( B = D
& A = C )
| g1_pre_topc(A,B) != g1_pre_topc(C,D) )
| ~ m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [B,A,C,D] :
( ( B = D
& A = C )
| g1_pre_topc(A,B) != g1_pre_topc(C,D)
| ~ m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c75,plain,
( X0 = X2
| g1_pre_topc(X0,X1) != g1_pre_topc(X2,X3)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(p341,plain,
( u1_struct_0(sk1) = X0
| g1_pre_topc(u1_struct_0(sk1),u1_pre_topc(sk1)) != g1_pre_topc(X0,X1) ),
inference(resolution,[status(thm)],[p320,c75]) ).
cnf(p762,plain,
( u1_struct_0(sk1) = X0
| g1_pre_topc(u1_struct_0(sk0),u1_pre_topc(sk0)) != g1_pre_topc(X0,X1) ),
inference(superposition,[status(thm)],[c4,p341]) ).
cnf(p936,plain,
u1_struct_0(sk1) = u1_struct_0(sk0),
inference(equality_resolution,[status(thm)],[p762]) ).
cnf(c52,plain,
( m1_subset_1(sk4(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_tsp_1(X1,X0)
| v1_tsp_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p282,plain,
( m1_subset_1(sk4(sk1,X0),k1_zfmisc_1(u1_struct_0(sk1)))
| ~ v1_tsp_1(X0,sk1)
| v1_tsp_2(X0,sk1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk1))) ),
inference(resolution,[status(thm)],[c52,c1]) ).
cnf(c5,plain,
sk2 = sk3,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(c3,plain,
m1_subset_1(sk3,k1_zfmisc_1(u1_struct_0(sk1))),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p109,plain,
m1_subset_1(sk2,k1_zfmisc_1(u1_struct_0(sk1))),
inference(superposition,[status(thm)],[c5,c3]) ).
cnf(p748,plain,
( m1_subset_1(sk4(sk1,sk2),k1_zfmisc_1(u1_struct_0(sk1)))
| ~ v1_tsp_1(sk2,sk1)
| v1_tsp_2(sk2,sk1) ),
inference(resolution,[status(thm)],[p282,p109]) ).
cnf(p944,plain,
( m1_subset_1(sk4(sk1,sk2),k1_zfmisc_1(u1_struct_0(sk0)))
| ~ v1_tsp_1(sk2,sk1)
| v1_tsp_2(sk2,sk1) ),
inference(demodulation,[status(thm)],[p936,p748]) ).
cnf(p2540,plain,
( m1_subset_1(sk4(sk1,sk2),k1_zfmisc_1(u1_struct_0(sk0)))
| v1_tsp_2(sk2,sk1) ),
inference(resolution,[status(thm)],[p2530,p944]) ).
cnf(c51,plain,
( X1 = X2
| ~ r1_tarski(X1,X2)
| ~ v1_tsp_1(X2,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_tsp_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p273,plain,
( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ v1_tsp_1(X1,sk0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ v1_tsp_2(X0,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0))) ),
inference(resolution,[status(thm)],[c51,c0]) ).
cnf(p729,plain,
( sk2 = X0
| ~ r1_tarski(sk2,X0)
| ~ v1_tsp_1(X0,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ v1_tsp_2(sk2,sk0) ),
inference(resolution,[status(thm)],[p273,c2]) ).
cnf(p1481,plain,
( sk2 = X0
| ~ r1_tarski(sk2,X0)
| ~ v1_tsp_1(X0,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0))) ),
inference(resolution,[status(thm)],[p729,c6]) ).
cnf(p2565,plain,
( sk2 = sk4(sk1,sk2)
| ~ r1_tarski(sk2,sk4(sk1,sk2))
| ~ v1_tsp_1(sk4(sk1,sk2),sk0)
| v1_tsp_2(sk2,sk1) ),
inference(resolution,[status(thm)],[p2540,p1481]) ).
cnf(p486,plain,
( v1_tsp_1(X2,X1)
| ~ v1_tsp_1(X2,X0)
| g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(equality_resolution,[status(thm)],[c104]) ).
cnf(p1141,plain,
( v1_tsp_1(X1,X0)
| ~ v1_tsp_1(X1,sk1)
| g1_pre_topc(u1_struct_0(sk0),u1_pre_topc(sk0)) != g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ l1_pre_topc(X0) ),
inference(resolution,[status(thm)],[p486,c1]) ).
cnf(p2444,plain,
( v1_tsp_1(X0,sk0)
| ~ v1_tsp_1(X0,sk1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ l1_pre_topc(sk0) ),
inference(equality_resolution,[status(thm)],[p1141]) ).
cnf(p2465,plain,
( v1_tsp_1(X0,sk0)
| ~ v1_tsp_1(X0,sk1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ l1_pre_topc(sk0) ),
inference(factoring,[status(thm)],[p2444]) ).
cnf(p2466,plain,
( v1_tsp_1(X0,sk0)
| ~ v1_tsp_1(X0,sk1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0))) ),
inference(resolution,[status(thm)],[p2465,c0]) ).
cnf(p2575,plain,
( v1_tsp_1(sk4(sk1,sk2),sk0)
| ~ v1_tsp_1(sk4(sk1,sk2),sk1)
| v1_tsp_2(sk2,sk1) ),
inference(resolution,[status(thm)],[p2540,p2466]) ).
cnf(c53,plain,
( v1_tsp_1(sk4(X0,X1),X0)
| ~ v1_tsp_1(X1,X0)
| v1_tsp_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p288,plain,
( v1_tsp_1(sk4(sk1,X0),sk1)
| ~ v1_tsp_1(X0,sk1)
| v1_tsp_2(X0,sk1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk1))) ),
inference(resolution,[status(thm)],[c53,c1]) ).
cnf(p800,plain,
( v1_tsp_1(sk4(sk1,sk2),sk1)
| ~ v1_tsp_1(sk2,sk1)
| v1_tsp_2(sk2,sk1) ),
inference(resolution,[status(thm)],[p288,p109]) ).
cnf(p2537,plain,
( v1_tsp_1(sk4(sk1,sk2),sk1)
| v1_tsp_2(sk2,sk1) ),
inference(resolution,[status(thm)],[p2530,p800]) ).
cnf(p2599,plain,
( v1_tsp_2(sk2,sk1)
| v1_tsp_1(sk4(sk1,sk2),sk0)
| v1_tsp_2(sk2,sk1) ),
inference(resolution,[status(thm)],[p2575,p2537]) ).
cnf(p2600,plain,
( v1_tsp_1(sk4(sk1,sk2),sk0)
| v1_tsp_2(sk2,sk1) ),
inference(factoring,[status(thm)],[p2599]) ).
cnf(p2651,plain,
( v1_tsp_2(sk2,sk1)
| sk2 = sk4(sk1,sk2)
| ~ r1_tarski(sk2,sk4(sk1,sk2))
| v1_tsp_2(sk2,sk1) ),
inference(resolution,[status(thm)],[p2565,p2600]) ).
cnf(p2652,plain,
( sk2 = sk4(sk1,sk2)
| ~ r1_tarski(sk2,sk4(sk1,sk2))
| v1_tsp_2(sk2,sk1) ),
inference(factoring,[status(thm)],[p2651]) ).
cnf(c54,plain,
( r1_tarski(X1,sk4(X0,X1))
| ~ v1_tsp_1(X1,X0)
| v1_tsp_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p294,plain,
( r1_tarski(X0,sk4(sk1,X0))
| ~ v1_tsp_1(X0,sk1)
| v1_tsp_2(X0,sk1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk1))) ),
inference(resolution,[status(thm)],[c54,c1]) ).
cnf(p825,plain,
( r1_tarski(sk2,sk4(sk1,sk2))
| ~ v1_tsp_1(sk2,sk1)
| v1_tsp_2(sk2,sk1) ),
inference(resolution,[status(thm)],[p294,p109]) ).
cnf(p2538,plain,
( r1_tarski(sk2,sk4(sk1,sk2))
| v1_tsp_2(sk2,sk1) ),
inference(resolution,[status(thm)],[p2530,p825]) ).
cnf(p2653,plain,
( v1_tsp_2(sk2,sk1)
| sk2 = sk4(sk1,sk2)
| v1_tsp_2(sk2,sk1) ),
inference(resolution,[status(thm)],[p2652,p2538]) ).
cnf(p2658,plain,
( sk2 = sk4(sk1,sk2)
| v1_tsp_2(sk2,sk1) ),
inference(factoring,[status(thm)],[p2653]) ).
cnf(c55,plain,
( X1 != sk4(X0,X1)
| ~ v1_tsp_1(X1,X0)
| v1_tsp_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p300,plain,
( X0 != sk4(sk1,X0)
| ~ v1_tsp_1(X0,sk1)
| v1_tsp_2(X0,sk1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk1))) ),
inference(resolution,[status(thm)],[c55,c1]) ).
cnf(p843,plain,
( sk2 != sk4(sk1,sk2)
| ~ v1_tsp_1(sk2,sk1)
| v1_tsp_2(sk2,sk1) ),
inference(resolution,[status(thm)],[p300,p109]) ).
cnf(p2539,plain,
( sk2 != sk4(sk1,sk2)
| v1_tsp_2(sk2,sk1) ),
inference(resolution,[status(thm)],[p2530,p843]) ).
cnf(p2659,plain,
( v1_tsp_2(sk2,sk1)
| v1_tsp_2(sk2,sk1) ),
inference(resolution,[status(thm)],[p2658,p2539]) ).
cnf(p2660,plain,
v1_tsp_2(sk2,sk1),
inference(factoring,[status(thm)],[p2659]) ).
cnf(c7,plain,
~ v1_tsp_2(sk3,sk1),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p108,plain,
~ v1_tsp_2(sk2,sk1),
inference(superposition,[status(thm)],[c5,c7]) ).
cnf(p2661,plain,
$false,
inference(resolution,[status(thm)],[p2660,p108]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP023+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 04:06:53 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 30.78/4.38 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 30.78/4.38 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------