%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : TOP024+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 : n009.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 29.76s 4.81s
% Output : Proof 29.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 7
% Syntax : Number of formulae : 57 ( 11 unt; 0 def)
% Number of atoms : 210 ( 38 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 247 ( 94 ~; 101 |; 32 &)
% ( 2 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 2 con; 0-2 aty)
% Number of variables : 63 ( 0 sgn 40 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f24,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v1_tsp_2(B,A)
<=> ( k3_tex_4(A,B) = u1_struct_0(A)
& v1_tsp_1(B,A) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_tsp_2) ).
fof(f24_nnf,plain,
! [A] :
( ! [B] :
( ( ( k3_tex_4(A,B) != u1_struct_0(A)
| ~ v1_tsp_1(B,A)
| v1_tsp_2(B,A) )
& ( ( k3_tex_4(A,B) = 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)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [A,B] :
( ( ( k3_tex_4(A,B) != u1_struct_0(A)
| ~ v1_tsp_1(B,A)
| v1_tsp_2(B,A) )
& ( ( k3_tex_4(A,B) = 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)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c66,plain,
( k3_tex_4(X0,X1) = u1_struct_0(X0)
| ~ v1_tsp_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
fof(f0,conjecture,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v1_tsp_2(B,A)
=> v1_tops_1(B,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_tsp_2) ).
fof(f0_neg,negated_conjecture,
~ ! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v1_tsp_2(B,A)
=> v1_tops_1(B,A) ) ) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
? [A] :
( ? [B] :
( ~ v1_tops_1(B,A)
& v1_tsp_2(B,A)
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
& l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
( ~ v1_tops_1(sk1,sk0)
& v1_tsp_2(sk1,sk0)
& m1_subset_1(sk1,k1_zfmisc_1(u1_struct_0(sk0)))
& l1_pre_topc(sk0)
& v2_pre_topc(sk0)
& ~ v3_struct_0(sk0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f0_nnf]) ).
cnf(c1,plain,
v2_pre_topc(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p383,plain,
( k3_tex_4(sk0,X0) = u1_struct_0(sk0)
| ~ v1_tsp_2(X0,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ l1_pre_topc(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c66,c1]) ).
cnf(c2,plain,
l1_pre_topc(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1252,plain,
( k3_tex_4(sk0,X0) = u1_struct_0(sk0)
| ~ v1_tsp_2(X0,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p383,c2]) ).
cnf(c3,plain,
m1_subset_1(sk1,k1_zfmisc_1(u1_struct_0(sk0))),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p3832,plain,
( k3_tex_4(sk0,sk1) = u1_struct_0(sk0)
| ~ v1_tsp_2(sk1,sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1252,c3]) ).
cnf(c4,plain,
v1_tsp_2(sk1,sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p3929,plain,
( k3_tex_4(sk0,sk1) = u1_struct_0(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p3832,c4]) ).
fof(f65,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> k6_pre_topc(A,k3_tex_4(A,B)) = k6_pre_topc(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t64_tex_4) ).
fof(f65_nnf,plain,
! [A] :
( ! [B] :
( k6_pre_topc(A,k3_tex_4(A,B)) = k6_pre_topc(A,B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f65]) ).
fof(f65_sk,plain,
! [A,B] :
( k6_pre_topc(A,k3_tex_4(A,B)) = k6_pre_topc(A,B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f65_nnf]) ).
cnf(c151,plain,
( k6_pre_topc(X0,k3_tex_4(X0,X1)) = k6_pre_topc(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f65_sk]) ).
cnf(p953,plain,
( k6_pre_topc(sk0,k3_tex_4(sk0,X0)) = k6_pre_topc(sk0,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ l1_pre_topc(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c151,c1]) ).
cnf(p2477,plain,
( k6_pre_topc(sk0,k3_tex_4(sk0,X0)) = k6_pre_topc(sk0,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p953,c2]) ).
cnf(p5727,plain,
( k6_pre_topc(sk0,k3_tex_4(sk0,sk1)) = k6_pre_topc(sk0,sk1)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p2477,c3]) ).
cnf(p5883,plain,
( u1_struct_0(sk0) = k6_pre_topc(sk0,sk1)
| v3_struct_0(sk0)
| v3_struct_0(sk0) ),
inference(superposition,[status(thm)],[p3929,p5727]) ).
cnf(p5896,plain,
( u1_struct_0(sk0) = k6_pre_topc(sk0,sk1)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p5883]) ).
fof(f63,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( ( ( k6_pre_topc(A,B) = B
& v2_pre_topc(A) )
=> v4_pre_topc(B,A) )
& ( v4_pre_topc(B,A)
=> k6_pre_topc(A,B) = B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t52_pre_topc) ).
fof(f63_nnf,plain,
! [A] :
( ! [B] :
( ( ( v4_pre_topc(B,A)
| k6_pre_topc(A,B) != B
| ~ v2_pre_topc(A) )
& ( k6_pre_topc(A,B) = B
| ~ v4_pre_topc(B,A) ) )
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A) ),
inference(nnf_transformation,[status(thm)],[f63]) ).
fof(f63_sk,plain,
! [A,B] :
( ( ( v4_pre_topc(B,A)
| k6_pre_topc(A,B) != B
| ~ v2_pre_topc(A) )
& ( k6_pre_topc(A,B) = B
| ~ v4_pre_topc(B,A) ) )
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_pre_topc(A) ),
inference(skolemisation,[status(esa)],[f63_nnf]) ).
cnf(c148,plain,
( k6_pre_topc(X0,X1) = X1
| ~ v4_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(esa)],[f63_sk]) ).
cnf(p937,plain,
( k6_pre_topc(sk0,X0) = X0
| ~ v4_pre_topc(X0,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0))) ),
inference(resolution,[status(thm)],[c148,c2]) ).
fof(f29,axiom,
! [A,B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& l1_pre_topc(A) )
=> m1_subset_1(k6_pre_topc(A,B),k1_zfmisc_1(u1_struct_0(A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_pre_topc) ).
fof(f29_nnf,plain,
! [A,B] :
( m1_subset_1(k6_pre_topc(A,B),k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_pre_topc(A) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [A,B] :
( m1_subset_1(k6_pre_topc(A,B),k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_pre_topc(A) ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c72,plain,
( m1_subset_1(k6_pre_topc(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(p409,plain,
( m1_subset_1(k6_pre_topc(sk0,X0),k1_zfmisc_1(u1_struct_0(sk0)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0))) ),
inference(resolution,[status(thm)],[c72,c2]) ).
cnf(p411,plain,
m1_subset_1(k6_pre_topc(sk0,sk1),k1_zfmisc_1(u1_struct_0(sk0))),
inference(resolution,[status(thm)],[p409,c3]) ).
cnf(p1903,plain,
( k6_pre_topc(sk0,k6_pre_topc(sk0,sk1)) = k6_pre_topc(sk0,sk1)
| ~ v4_pre_topc(k6_pre_topc(sk0,sk1),sk0) ),
inference(resolution,[status(thm)],[p937,p411]) ).
fof(f40,axiom,
! [A,B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& l1_pre_topc(A)
& v2_pre_topc(A) )
=> v4_pre_topc(k6_pre_topc(A,B),A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_tops_1) ).
fof(f40_nnf,plain,
! [A,B] :
( v4_pre_topc(k6_pre_topc(A,B),A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [A,B] :
( v4_pre_topc(k6_pre_topc(A,B),A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c83,plain,
( v4_pre_topc(k6_pre_topc(X0,X1),X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(p468,plain,
( v4_pre_topc(k6_pre_topc(sk0,X0),sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ l1_pre_topc(sk0) ),
inference(resolution,[status(thm)],[c83,c1]) ).
cnf(p1615,plain,
( v4_pre_topc(k6_pre_topc(sk0,X0),sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0))) ),
inference(resolution,[status(thm)],[p468,c2]) ).
cnf(p1616,plain,
v4_pre_topc(k6_pre_topc(sk0,sk1),sk0),
inference(resolution,[status(thm)],[p1615,c3]) ).
cnf(p2374,plain,
k6_pre_topc(sk0,k6_pre_topc(sk0,sk1)) = k6_pre_topc(sk0,sk1),
inference(resolution,[status(thm)],[p1903,p1616]) ).
cnf(p5900,plain,
( k6_pre_topc(sk0,sk1) = u1_struct_0(sk0)
| v3_struct_0(sk0) ),
inference(superposition,[status(thm)],[p5896,p2374]) ).
fof(f23,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v1_tops_1(B,A)
<=> k6_pre_topc(A,B) = u1_struct_0(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_tops_3) ).
fof(f23_nnf,plain,
! [A] :
( ! [B] :
( ( ( k6_pre_topc(A,B) != u1_struct_0(A)
| v1_tops_1(B,A) )
& ( k6_pre_topc(A,B) = u1_struct_0(A)
| ~ v1_tops_1(B,A) ) )
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [A,B] :
( ( ( k6_pre_topc(A,B) != u1_struct_0(A)
| v1_tops_1(B,A) )
& ( k6_pre_topc(A,B) = u1_struct_0(A)
| ~ v1_tops_1(B,A) ) )
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_pre_topc(A) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c64,plain,
( k6_pre_topc(X0,X1) != u1_struct_0(X0)
| v1_tops_1(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p371,plain,
( k6_pre_topc(sk0,X0) != u1_struct_0(sk0)
| v1_tops_1(X0,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0))) ),
inference(resolution,[status(thm)],[c64,c2]) ).
cnf(p373,plain,
( k6_pre_topc(sk0,sk1) != u1_struct_0(sk0)
| v1_tops_1(sk1,sk0) ),
inference(resolution,[status(thm)],[p371,c3]) ).
cnf(p5920,plain,
( v1_tops_1(sk1,sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p5900,p373]) ).
cnf(c5,plain,
~ v1_tops_1(sk1,sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p5922,plain,
v3_struct_0(sk0),
inference(resolution,[status(thm)],[p5920,c5]) ).
cnf(c0,plain,
~ v3_struct_0(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p5923,plain,
$false,
inference(resolution,[status(thm)],[p5922,c0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP024+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n009.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 04:09:58 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 29.76/4.81 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.76/4.81 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------