%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : TOP029+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n011.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:55:03 PM UTC 2026
% Result : Theorem 121.82s 29.31s
% Output : CNFRefutation 121.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 12
% Syntax : Number of formulae : 114 ( 15 unt; 0 def)
% Number of atoms : 591 ( 32 equ)
% Maximal formula atoms : 11 ( 5 avg)
% Number of connectives : 821 ( 344 ~; 374 |; 71 &)
% ( 8 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 7 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 2 con; 0-2 aty)
% Number of variables : 181 ( 0 sgn 171 !; 10 ?; 67 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( m2_tsp_1(X1,X0)
& v2_t_0topsp(X1)
& ~ v3_struct_0(X1) )
=> ? [X2] :
( v2_tsp_2(X2,X0)
& m2_tsp_1(X1,X2)
& m2_tsp_1(X2,X0)
& v1_pre_topc(X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t13_tsp_2) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( m2_tsp_1(X1,X0)
& v2_t_0topsp(X1)
& ~ v3_struct_0(X1) )
=> ? [X2] :
( v2_tsp_2(X2,X0)
& m2_tsp_1(X1,X2)
& m2_tsp_1(X2,X0)
& v1_pre_topc(X2) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f57,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
=> l1_pre_topc(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_tsp_1) ).
fof(f69,axiom,
! [X0] :
( ( l1_pre_topc(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( m2_tsp_1(X1,X0)
=> m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l19_tsp_2) ).
fof(f96,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_tsp_1) ).
fof(f98,axiom,
! [X0] :
( ( l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
& ~ v1_xboole_0(X1) )
=> ~ ( ! [X2] :
( ( m2_tsp_1(X2,X0)
& v1_pre_topc(X2)
& ~ v3_struct_0(X2) )
=> ~ ( X1 = u1_struct_0(X2)
& v2_tsp_2(X2,X0) ) )
& v1_tsp_2(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_tsp_2) ).
fof(f99,axiom,
! [X0] :
( ( l1_pre_topc(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( m2_tsp_1(X1,X0)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ( X2 = u1_struct_0(X1)
=> ( v1_tsp_1(X2,X0)
<=> v2_t_0topsp(X1) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_tsp_1) ).
fof(f104,axiom,
! [X0] :
( ( l1_pre_topc(X0)
& v2_pre_topc(X0) )
=> ! [X1] :
( m1_pre_topc(X1,X0)
=> ! [X2] :
( m1_pre_topc(X2,X0)
=> ( r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
<=> m1_pre_topc(X1,X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_tsep_1) ).
fof(f105,axiom,
! [X0] :
( ( l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
& v1_xboole_0(X1) )
=> ~ v1_tsp_2(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_tsp_2) ).
fof(f110,axiom,
! [X0] :
( ( l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ~ ( ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ~ ( v1_tsp_2(X2,X0)
& r1_tarski(X1,X2) ) )
& v1_tsp_1(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t9_tsp_2) ).
fof(f136,plain,
? [X0] :
( l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0)
& ? [X1] :
( m2_tsp_1(X1,X0)
& v2_t_0topsp(X1)
& ~ v3_struct_0(X1)
& ! [X2] :
( ~ v2_tsp_2(X2,X0)
| ~ m2_tsp_1(X1,X2)
| ~ m2_tsp_1(X2,X0)
| ~ v1_pre_topc(X2) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f137,plain,
? [X0] :
( l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0)
& ? [X1] :
( m2_tsp_1(X1,X0)
& v2_t_0topsp(X1)
& ~ v3_struct_0(X1)
& ! [X2] :
( ~ v2_tsp_2(X2,X0)
| ~ m2_tsp_1(X1,X2)
| ~ m2_tsp_1(X2,X0)
| ~ v1_pre_topc(X2) ) ) ),
inference(flattening,[],[f136]) ).
fof(f208,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ! [X1] :
( ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1) ) ),
inference(ennf_transformation,[],[f57]) ).
fof(f215,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m2_tsp_1(X1,X0)
| m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0))) ) ),
inference(ennf_transformation,[],[f69]) ).
fof(f216,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m2_tsp_1(X1,X0)
| m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0))) ) ),
inference(flattening,[],[f215]) ).
fof(f248,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) ) ),
inference(ennf_transformation,[],[f96]) ).
fof(f249,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v1_xboole_0(X1)
| ? [X2] :
( m2_tsp_1(X2,X0)
& v1_pre_topc(X2)
& ~ v3_struct_0(X2)
& X1 = u1_struct_0(X2)
& v2_tsp_2(X2,X0) )
| ~ v1_tsp_2(X1,X0) ) ),
inference(ennf_transformation,[],[f98]) ).
fof(f250,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v1_xboole_0(X1)
| ? [X2] :
( m2_tsp_1(X2,X0)
& v1_pre_topc(X2)
& ~ v3_struct_0(X2)
& X1 = u1_struct_0(X2)
& v2_tsp_2(X2,X0) )
| ~ v1_tsp_2(X1,X0) ) ),
inference(flattening,[],[f249]) ).
fof(f251,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m2_tsp_1(X1,X0)
| v3_struct_0(X1)
| ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| u1_struct_0(X1) != X2
| ( v1_tsp_1(X2,X0)
<=> v2_t_0topsp(X1) ) ) ) ),
inference(ennf_transformation,[],[f99]) ).
fof(f252,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m2_tsp_1(X1,X0)
| v3_struct_0(X1)
| ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| u1_struct_0(X1) != X2
| ( v1_tsp_1(X2,X0)
<=> v2_t_0topsp(X1) ) ) ) ),
inference(flattening,[],[f251]) ).
fof(f258,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ! [X1] :
( ~ m1_pre_topc(X1,X0)
| ! [X2] :
( ~ m1_pre_topc(X2,X0)
| ( r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
<=> m1_pre_topc(X1,X2) ) ) ) ),
inference(ennf_transformation,[],[f104]) ).
fof(f259,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ! [X1] :
( ~ m1_pre_topc(X1,X0)
| ! [X2] :
( ~ m1_pre_topc(X2,X0)
| ( r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
<=> m1_pre_topc(X1,X2) ) ) ) ),
inference(flattening,[],[f258]) ).
fof(f260,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_xboole_0(X1)
| ~ v1_tsp_2(X1,X0) ) ),
inference(ennf_transformation,[],[f105]) ).
fof(f261,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_xboole_0(X1)
| ~ v1_tsp_2(X1,X0) ) ),
inference(flattening,[],[f260]) ).
fof(f266,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
& v1_tsp_2(X2,X0)
& r1_tarski(X1,X2) )
| ~ v1_tsp_1(X1,X0) ) ),
inference(ennf_transformation,[],[f110]) ).
fof(f267,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
& v1_tsp_2(X2,X0)
& r1_tarski(X1,X2) )
| ~ v1_tsp_1(X1,X0) ) ),
inference(flattening,[],[f266]) ).
fof(f272,plain,
( l1_pre_topc(sK2)
& v2_pre_topc(sK2)
& ~ v3_struct_0(sK2)
& m2_tsp_1(sK3,sK2)
& v2_t_0topsp(sK3)
& ~ v3_struct_0(sK3)
& ! [X2] :
( ~ v2_tsp_2(X2,sK2)
| ~ m2_tsp_1(sK3,X2)
| ~ m2_tsp_1(X2,sK2)
| ~ v1_pre_topc(X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X0,sK2),skolemize(X1,sK3)],[f137]) ).
fof(f307,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ! [X1] :
( ( ~ m2_tsp_1(X1,X0)
| m1_pre_topc(X1,X0) )
& ( ~ m1_pre_topc(X1,X0)
| m2_tsp_1(X1,X0) ) ) ),
inference(nnf_transformation,[],[f248]) ).
fof(f308,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v1_xboole_0(X1)
| ( m2_tsp_1(sK35(X0,X1),X0)
& v1_pre_topc(sK35(X0,X1))
& ~ v3_struct_0(sK35(X0,X1))
& u1_struct_0(sK35(X0,X1)) = X1
& v2_tsp_2(sK35(X0,X1),X0) )
| ~ v1_tsp_2(X1,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35]),skolemize(X2,sK35(X0,X1))],[f250]) ).
fof(f309,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m2_tsp_1(X1,X0)
| v3_struct_0(X1)
| ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| u1_struct_0(X1) != X2
| ( ( ~ v1_tsp_1(X2,X0)
| v2_t_0topsp(X1) )
& ( ~ v2_t_0topsp(X1)
| v1_tsp_1(X2,X0) ) ) ) ) ),
inference(nnf_transformation,[],[f252]) ).
fof(f311,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ! [X1] :
( ~ m1_pre_topc(X1,X0)
| ! [X2] :
( ~ m1_pre_topc(X2,X0)
| ( ( ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| m1_pre_topc(X1,X2) )
& ( ~ m1_pre_topc(X1,X2)
| r1_tarski(u1_struct_0(X1),u1_struct_0(X2)) ) ) ) ) ),
inference(nnf_transformation,[],[f259]) ).
fof(f312,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ( m1_subset_1(sK36(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
& v1_tsp_2(sK36(X0,X1),X0)
& r1_tarski(X1,sK36(X0,X1)) )
| ~ v1_tsp_1(X1,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36]),skolemize(X2,sK36(X0,X1))],[f267]) ).
fof(f313,plain,
l1_pre_topc(sK2),
inference(cnf_transformation,[],[f272]) ).
fof(f314,plain,
v2_pre_topc(sK2),
inference(cnf_transformation,[],[f272]) ).
fof(f315,plain,
~ v3_struct_0(sK2),
inference(cnf_transformation,[],[f272]) ).
fof(f316,plain,
m2_tsp_1(sK3,sK2),
inference(cnf_transformation,[],[f272]) ).
fof(f317,plain,
v2_t_0topsp(sK3),
inference(cnf_transformation,[],[f272]) ).
fof(f318,plain,
~ v3_struct_0(sK3),
inference(cnf_transformation,[],[f272]) ).
fof(f319,plain,
! [X2] :
( ~ v2_tsp_2(X2,sK2)
| ~ m2_tsp_1(sK3,X2)
| ~ m2_tsp_1(X2,sK2)
| ~ v1_pre_topc(X2) ),
inference(cnf_transformation,[],[f272]) ).
fof(f430,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1) ),
inference(cnf_transformation,[],[f208]) ).
fof(f447,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| v3_struct_0(X0)
| ~ m2_tsp_1(X1,X0)
| m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f216]) ).
fof(f556,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m2_tsp_1(X1,X0)
| m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f307]) ).
fof(f557,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m1_pre_topc(X1,X0)
| m2_tsp_1(X1,X0) ),
inference(cnf_transformation,[],[f307]) ).
fof(f559,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v1_xboole_0(X1)
| m2_tsp_1(sK35(X0,X1),X0)
| ~ v1_tsp_2(X1,X0) ),
inference(cnf_transformation,[],[f308]) ).
fof(f560,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v1_xboole_0(X1)
| v1_pre_topc(sK35(X0,X1))
| ~ v1_tsp_2(X1,X0) ),
inference(cnf_transformation,[],[f308]) ).
fof(f562,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v1_xboole_0(X1)
| u1_struct_0(sK35(X0,X1)) = X1
| ~ v1_tsp_2(X1,X0) ),
inference(cnf_transformation,[],[f308]) ).
fof(f563,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v1_xboole_0(X1)
| v2_tsp_2(sK35(X0,X1),X0)
| ~ v1_tsp_2(X1,X0) ),
inference(cnf_transformation,[],[f308]) ).
fof(f565,plain,
! [X2,X0,X1] :
( ~ l1_pre_topc(X0)
| v3_struct_0(X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| u1_struct_0(X1) != X2
| ~ v2_t_0topsp(X1)
| v1_tsp_1(X2,X0) ),
inference(cnf_transformation,[],[f309]) ).
fof(f571,plain,
! [X2,X0,X1] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ~ m1_pre_topc(X1,X0)
| ~ m1_pre_topc(X2,X0)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| m1_pre_topc(X1,X2) ),
inference(cnf_transformation,[],[f311]) ).
fof(f573,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_xboole_0(X1)
| ~ v1_tsp_2(X1,X0) ),
inference(cnf_transformation,[],[f261]) ).
fof(f578,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| m1_subset_1(sK36(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_tsp_1(X1,X0) ),
inference(cnf_transformation,[],[f312]) ).
fof(f579,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v1_tsp_2(sK36(X0,X1),X0)
| ~ v1_tsp_1(X1,X0) ),
inference(cnf_transformation,[],[f312]) ).
fof(f580,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| r1_tarski(X1,sK36(X0,X1))
| ~ v1_tsp_1(X1,X0) ),
inference(cnf_transformation,[],[f312]) ).
fof(f581,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| v3_struct_0(X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X1)
| ~ m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v2_t_0topsp(X1)
| v1_tsp_1(u1_struct_0(X1),X0) ),
inference(equality_resolution,[],[f565]) ).
tcf(c_49,negated_conjecture,
! [X0: $i] :
( ~ v1_pre_topc(X0)
| ~ v2_tsp_2(X0,sK2)
| ~ m2_tsp_1(sK3,X0)
| ~ m2_tsp_1(X0,sK2) ),
inference(cnf_transformation,[],[f319]) ).
tcf(c_50,negated_conjecture,
~ v3_struct_0(sK3),
inference(cnf_transformation,[],[f318]) ).
tcf(c_51,negated_conjecture,
v2_t_0topsp(sK3),
inference(cnf_transformation,[],[f317]) ).
tcf(c_52,negated_conjecture,
m2_tsp_1(sK3,sK2),
inference(cnf_transformation,[],[f316]) ).
tcf(c_53,negated_conjecture,
~ v3_struct_0(sK2),
inference(cnf_transformation,[],[f315]) ).
tcf(c_54,negated_conjecture,
v2_pre_topc(sK2),
inference(cnf_transformation,[],[f314]) ).
tcf(c_55,negated_conjecture,
l1_pre_topc(sK2),
inference(cnf_transformation,[],[f313]) ).
tcf(c_134,plain,
! [X0: $i,X1: $i] :
( l1_pre_topc(X0)
| ~ l1_pre_topc(X1)
| ~ m2_tsp_1(X0,X1) ),
inference(cnf_transformation,[],[f430]) ).
tcf(c_151,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_pre_topc(X1)
| ~ m2_tsp_1(X0,X1) ),
inference(cnf_transformation,[],[f447]) ).
tcf(c_260,plain,
! [X0: $i,X1: $i] :
( m2_tsp_1(X0,X1)
| ~ l1_pre_topc(X1)
| ~ m1_pre_topc(X0,X1) ),
inference(cnf_transformation,[],[f557]) ).
tcf(c_261,plain,
! [X0: $i,X1: $i] :
( m1_pre_topc(X0,X1)
| ~ l1_pre_topc(X1)
| ~ m2_tsp_1(X0,X1) ),
inference(cnf_transformation,[],[f556]) ).
tcf(c_263,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(X0)
| v3_struct_0(X1)
| v2_tsp_2(sK35(X1,X0),X1)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ v1_tsp_2(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(cnf_transformation,[],[f563]) ).
tcf(c_264,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(X0)
| v3_struct_0(X1)
| ( u1_struct_0(sK35(X1,X0)) = X0 )
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ v1_tsp_2(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(cnf_transformation,[],[f562]) ).
tcf(c_266,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(X0)
| v3_struct_0(X1)
| v1_pre_topc(sK35(X1,X0))
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ v1_tsp_2(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(cnf_transformation,[],[f560]) ).
tcf(c_267,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(X0)
| v3_struct_0(X1)
| m2_tsp_1(sK35(X1,X0),X1)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ v1_tsp_2(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(cnf_transformation,[],[f559]) ).
tcf(c_268,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| v1_tsp_1(u1_struct_0(X0),X1)
| ~ l1_pre_topc(X1)
| ~ v2_t_0topsp(X0)
| ~ m2_tsp_1(X0,X1)
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X1))) ),
inference(cnf_transformation,[],[f581]) ).
tcf(c_276,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_pre_topc(X0,X1)
| ~ l1_pre_topc(X2)
| ~ v2_pre_topc(X2)
| ~ m1_pre_topc(X1,X2)
| ~ m1_pre_topc(X0,X2)
| ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f571]) ).
tcf(c_277,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| ~ v1_xboole_0(X0)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ v1_tsp_2(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(cnf_transformation,[],[f573]) ).
tcf(c_282,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| r1_tarski(X0,sK36(X1,X0))
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ v1_tsp_1(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(cnf_transformation,[],[f580]) ).
tcf(c_283,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v1_tsp_2(sK36(X1,X0),X1)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ v1_tsp_1(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(cnf_transformation,[],[f579]) ).
tcf(c_284,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| m1_subset_1(sK36(X1,X0),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ v1_tsp_1(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(cnf_transformation,[],[f578]) ).
tcf(c_420,plain,
! [X0: $i,X1: $i] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v1_tsp_2(X0,X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1)
| v1_pre_topc(sK35(X1,X0))
| v3_struct_0(X1) ),
inference(global_subsumption_just,[status(thm)],[c_266,c_277,c_266]) ).
tcf(c_421,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v1_pre_topc(sK35(X1,X0))
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ v1_tsp_2(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(renaming,[status(thm)],[c_420]) ).
tcf(c_426,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| v1_tsp_1(u1_struct_0(X0),X1)
| ~ l1_pre_topc(X1)
| ~ v2_t_0topsp(X0)
| ~ m2_tsp_1(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_268,c_151,c_268]) ).
tcf(c_429,plain,
! [X0: $i,X1: $i] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v1_tsp_2(X0,X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1)
| m2_tsp_1(sK35(X1,X0),X1)
| v3_struct_0(X1) ),
inference(global_subsumption_just,[status(thm)],[c_267,c_277,c_267]) ).
tcf(c_430,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| m2_tsp_1(sK35(X1,X0),X1)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ v1_tsp_2(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(renaming,[status(thm)],[c_429]) ).
tcf(c_435,plain,
! [X0: $i,X1: $i] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v1_tsp_2(X0,X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1)
| v2_tsp_2(sK35(X1,X0),X1)
| v3_struct_0(X1) ),
inference(global_subsumption_just,[status(thm)],[c_263,c_277,c_263]) ).
tcf(c_436,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v2_tsp_2(sK35(X1,X0),X1)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ v1_tsp_2(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(renaming,[status(thm)],[c_435]) ).
tcf(c_438,plain,
! [X0: $i,X1: $i] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v1_tsp_2(X0,X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1)
| ( u1_struct_0(sK35(X1,X0)) = X0 )
| v3_struct_0(X1) ),
inference(global_subsumption_just,[status(thm)],[c_264,c_277,c_264]) ).
tcf(c_439,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| ( u1_struct_0(sK35(X1,X0)) = X0 )
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ v1_tsp_2(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(renaming,[status(thm)],[c_438]) ).
tcf(c_503,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_513,plain,
! [X0: $i,X1: $i] :
( ( u1_struct_0(X0) = u1_struct_0(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_528,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_662,plain,
( m1_pre_topc(sK3,sK2)
| ~ l1_pre_topc(sK2) ),
inference(superposition,[status(thm)],[c_52,c_261]) ).
tcf(c_1133,plain,
( v3_struct_0(sK2)
| m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l1_pre_topc(sK2)
| ~ m2_tsp_1(sK3,sK2) ),
inference(instantiation,[status(thm)],[c_151]) ).
tcf(c_1156,plain,
( v3_struct_0(sK3)
| v3_struct_0(sK2)
| v1_tsp_1(u1_struct_0(sK3),sK2)
| ~ l1_pre_topc(sK2)
| ~ v2_t_0topsp(sK3)
| ~ m2_tsp_1(sK3,sK2) ),
inference(instantiation,[status(thm)],[c_426]) ).
tcf(c_2070,plain,
( v3_struct_0(sK2)
| m1_subset_1(sK36(sK2,u1_struct_0(sK3)),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l1_pre_topc(sK2)
| ~ v2_pre_topc(sK2)
| ~ v1_tsp_1(u1_struct_0(sK3),sK2)
| ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2))) ),
inference(instantiation,[status(thm)],[c_284]) ).
tcf(c_2071,plain,
( v3_struct_0(sK2)
| v1_tsp_2(sK36(sK2,u1_struct_0(sK3)),sK2)
| ~ l1_pre_topc(sK2)
| ~ v2_pre_topc(sK2)
| ~ v1_tsp_1(u1_struct_0(sK3),sK2)
| ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2))) ),
inference(instantiation,[status(thm)],[c_283]) ).
tcf(c_2072,plain,
( v3_struct_0(sK2)
| r1_tarski(u1_struct_0(sK3),sK36(sK2,u1_struct_0(sK3)))
| ~ l1_pre_topc(sK2)
| ~ v2_pre_topc(sK2)
| ~ v1_tsp_1(u1_struct_0(sK3),sK2)
| ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2))) ),
inference(instantiation,[status(thm)],[c_282]) ).
tcf(c_6298,plain,
( v3_struct_0(sK2)
| ( u1_struct_0(sK35(sK2,sK36(sK2,u1_struct_0(sK3)))) = sK36(sK2,u1_struct_0(sK3)) )
| ~ l1_pre_topc(sK2)
| ~ v2_pre_topc(sK2)
| ~ v1_tsp_2(sK36(sK2,u1_struct_0(sK3)),sK2)
| ~ m1_subset_1(sK36(sK2,u1_struct_0(sK3)),k1_zfmisc_1(u1_struct_0(sK2))) ),
inference(instantiation,[status(thm)],[c_439]) ).
tcf(c_6299,plain,
( v3_struct_0(sK2)
| v2_tsp_2(sK35(sK2,sK36(sK2,u1_struct_0(sK3))),sK2)
| ~ l1_pre_topc(sK2)
| ~ v2_pre_topc(sK2)
| ~ v1_tsp_2(sK36(sK2,u1_struct_0(sK3)),sK2)
| ~ m1_subset_1(sK36(sK2,u1_struct_0(sK3)),k1_zfmisc_1(u1_struct_0(sK2))) ),
inference(instantiation,[status(thm)],[c_436]) ).
tcf(c_6300,plain,
( v3_struct_0(sK2)
| m2_tsp_1(sK35(sK2,sK36(sK2,u1_struct_0(sK3))),sK2)
| ~ l1_pre_topc(sK2)
| ~ v2_pre_topc(sK2)
| ~ v1_tsp_2(sK36(sK2,u1_struct_0(sK3)),sK2)
| ~ m1_subset_1(sK36(sK2,u1_struct_0(sK3)),k1_zfmisc_1(u1_struct_0(sK2))) ),
inference(instantiation,[status(thm)],[c_430]) ).
tcf(c_6302,plain,
( v3_struct_0(sK2)
| v1_pre_topc(sK35(sK2,sK36(sK2,u1_struct_0(sK3))))
| ~ l1_pre_topc(sK2)
| ~ v2_pre_topc(sK2)
| ~ v1_tsp_2(sK36(sK2,u1_struct_0(sK3)),sK2)
| ~ m1_subset_1(sK36(sK2,u1_struct_0(sK3)),k1_zfmisc_1(u1_struct_0(sK2))) ),
inference(instantiation,[status(thm)],[c_421]) ).
tcf(c_6903,plain,
! [X0: $i] :
( ( u1_struct_0(X0) = u1_struct_0(sK3) )
| ( X0 != sK3 ) ),
inference(instantiation,[status(thm)],[c_513]) ).
tcf(c_9991,plain,
! [X0: $i] :
( l1_pre_topc(X0)
| ~ l1_pre_topc(sK2)
| ~ m2_tsp_1(X0,sK2) ),
inference(instantiation,[status(thm)],[c_134]) ).
tcf(c_10646,plain,
! [X0: $i] :
( m1_pre_topc(X0,sK2)
| ~ l1_pre_topc(sK2)
| ~ m2_tsp_1(X0,sK2) ),
inference(instantiation,[status(thm)],[c_261]) ).
tcf(c_10955,plain,
( ~ v1_pre_topc(sK35(sK2,sK36(sK2,u1_struct_0(sK3))))
| ~ v2_tsp_2(sK35(sK2,sK36(sK2,u1_struct_0(sK3))),sK2)
| ~ m2_tsp_1(sK3,sK35(sK2,sK36(sK2,u1_struct_0(sK3))))
| ~ m2_tsp_1(sK35(sK2,sK36(sK2,u1_struct_0(sK3))),sK2) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_11487,plain,
( m2_tsp_1(sK3,sK35(sK2,sK36(sK2,u1_struct_0(sK3))))
| ~ l1_pre_topc(sK35(sK2,sK36(sK2,u1_struct_0(sK3))))
| ~ m1_pre_topc(sK3,sK35(sK2,sK36(sK2,u1_struct_0(sK3)))) ),
inference(instantiation,[status(thm)],[c_260]) ).
tcf(c_11566,plain,
( l1_pre_topc(sK35(sK2,sK36(sK2,u1_struct_0(sK3))))
| ~ l1_pre_topc(sK2)
| ~ m2_tsp_1(sK35(sK2,sK36(sK2,u1_struct_0(sK3))),sK2) ),
inference(instantiation,[status(thm)],[c_9991]) ).
tcf(c_11578,plain,
( m1_pre_topc(sK35(sK2,sK36(sK2,u1_struct_0(sK3))),sK2)
| ~ l1_pre_topc(sK2)
| ~ m2_tsp_1(sK35(sK2,sK36(sK2,u1_struct_0(sK3))),sK2) ),
inference(instantiation,[status(thm)],[c_10646]) ).
tcf(c_14092,plain,
( ( u1_struct_0(sK3) = u1_struct_0(sK3) )
| ( sK3 != sK3 ) ),
inference(instantiation,[status(thm)],[c_6903]) ).
tcf(c_14093,plain,
sK3 = sK3,
inference(instantiation,[status(thm)],[c_503]) ).
tcf(c_55012,plain,
! [X0: $i,X1: $i] :
( m1_pre_topc(sK3,X0)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ m1_pre_topc(sK3,X1)
| ~ m1_pre_topc(X0,X1)
| ~ r1_tarski(u1_struct_0(sK3),u1_struct_0(X0)) ),
inference(instantiation,[status(thm)],[c_276]) ).
tcf(c_60527,plain,
! [X0: $i] :
( m1_pre_topc(sK3,X0)
| ~ l1_pre_topc(sK2)
| ~ v2_pre_topc(sK2)
| ~ m1_pre_topc(sK3,sK2)
| ~ m1_pre_topc(X0,sK2)
| ~ r1_tarski(u1_struct_0(sK3),u1_struct_0(X0)) ),
inference(instantiation,[status(thm)],[c_55012]) ).
tcf(c_65550,plain,
( m1_pre_topc(sK3,sK35(sK2,sK36(sK2,u1_struct_0(sK3))))
| ~ l1_pre_topc(sK2)
| ~ v2_pre_topc(sK2)
| ~ m1_pre_topc(sK3,sK2)
| ~ m1_pre_topc(sK35(sK2,sK36(sK2,u1_struct_0(sK3))),sK2)
| ~ r1_tarski(u1_struct_0(sK3),u1_struct_0(sK35(sK2,sK36(sK2,u1_struct_0(sK3))))) ),
inference(instantiation,[status(thm)],[c_60527]) ).
tcf(c_118620,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1_tarski(u1_struct_0(sK3),u1_struct_0(X0))
| ~ r1_tarski(X2,X1)
| ( u1_struct_0(sK3) != X2 )
| ( u1_struct_0(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_528]) ).
tcf(c_127175,plain,
! [X0: $i,X1: $i] :
( r1_tarski(u1_struct_0(sK3),u1_struct_0(X0))
| ~ r1_tarski(u1_struct_0(sK3),X1)
| ( u1_struct_0(sK3) != u1_struct_0(sK3) )
| ( u1_struct_0(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_118620]) ).
tcf(c_140638,plain,
! [X0: $i] :
( r1_tarski(u1_struct_0(sK3),u1_struct_0(X0))
| ~ r1_tarski(u1_struct_0(sK3),sK36(sK2,u1_struct_0(sK3)))
| ( u1_struct_0(sK3) != u1_struct_0(sK3) )
| ( u1_struct_0(X0) != sK36(sK2,u1_struct_0(sK3)) ) ),
inference(instantiation,[status(thm)],[c_127175]) ).
tcf(c_154225,plain,
( r1_tarski(u1_struct_0(sK3),u1_struct_0(sK35(sK2,sK36(sK2,u1_struct_0(sK3)))))
| ~ r1_tarski(u1_struct_0(sK3),sK36(sK2,u1_struct_0(sK3)))
| ( u1_struct_0(sK3) != u1_struct_0(sK3) )
| ( u1_struct_0(sK35(sK2,sK36(sK2,u1_struct_0(sK3)))) != sK36(sK2,u1_struct_0(sK3)) ) ),
inference(instantiation,[status(thm)],[c_140638]) ).
tcf(c_154226,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_154225,c_65550,c_14093,c_14092,c_11578,c_11566,c_11487,c_10955,c_6298,c_6299,c_6300,c_6302,c_2070,c_2071,c_2072,c_1156,c_1133,c_662,c_50,c_52,c_53,c_51,c_54,c_55]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP029+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/5.41 % Computer : n011.cluster.edu
% 0.14/5.41 % Model : x86_64 x86_64
% 0.14/5.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/5.41 % Memory : 8046.5625MB
% 0.14/5.41 % OS : Linux 6.8.0-71-generic
% 0.14/5.41 % CPULimit : 300
% 0.14/5.41 % WCLimit : 300
% 0.14/5.41 % DateTime : Fri Sep 25 04:12:33 UTC 2026
% 0.14/5.41 % CPUTime :
% 0.14/5.41 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/5.46 Running first-order theorem proving
% 0.14/5.46 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/5.48
% 0.14/5.48 % ======== iProver multi-core TPTP/SMT =========
% 0.14/5.48
% 0.14/5.48 % Detected problem language: tptp
% 0.14/5.49 % Proving...
% 121.82/29.31 % SZS status Started for theBenchmark.p
% 121.82/29.31 % SZS status Theorem for theBenchmark.p
% 121.82/29.31
% 121.82/29.31 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 121.82/29.31
% 121.82/29.31 % ------ iProver source info
% 121.82/29.31
% 121.82/29.31 % git: date: 2026-07-19 20:42:38 +0200
% 121.82/29.31 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 121.82/29.31 % git: non_committed_changes: false
% 121.82/29.31
% 121.82/29.31 % ------ Parsing...
% 121.82/29.31 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 121.82/29.31
% 121.82/29.31 % ------ Preprocessing... sf_s rm: 61 0s sf_e sf_s rm: 7 0s sf_e %
% 121.82/29.31
% 121.82/29.31 % ------ Preprocessing...%
% 121.82/29.31
% 121.82/29.31 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 121.82/29.31 % ------ Proving...
% 121.82/29.31 % ------ Problem Properties
% 121.82/29.31
% 121.82/29.31 %
% 121.82/29.31 % clauses 164
% 121.82/29.31 % conjectures 7
% 121.82/29.31 % EPR 70
% 121.82/29.31 % Horn 122
% 121.82/29.31 % unary 47
% 121.82/29.31 % binary 30
% 121.82/29.31 % lits 479
% 121.82/29.31 % lits eq 8
% 121.82/29.31 % fd_pure 0
% 121.82/29.31 % fd_pseudo 0
% 121.82/29.31 % fd_cond 1
% 121.82/29.31 % fd_pseudo_cond 3
% 121.82/29.31 % AC symbols 0
% 121.82/29.31
% 121.82/29.31 % ------ Input Options Time Limit: Unbounded
% 121.82/29.31
% 121.82/29.31
% 121.82/29.31 % ------
% 121.82/29.31 % Current options:
% 121.82/29.31 % ------
% 121.82/29.31
% 121.82/29.31
% 121.82/29.31 %
% 121.82/29.31
% 121.82/29.31 % ------ Proving...
% 121.82/29.31 %
% 121.82/29.31
% 121.82/29.31 % SZS status Theorem for theBenchmark.p
% 121.82/29.31
% 121.82/29.31 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 121.82/29.31
% 121.82/29.31
%------------------------------------------------------------------------------