%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ALG223+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 : n010.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 12:53:52 PM UTC 2026
% Result : Theorem 8.56s 1.64s
% Output : CNFRefutation 8.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 4
% Syntax : Number of formulae : 103 ( 17 unt; 0 def)
% Number of atoms : 400 ( 34 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 559 ( 262 ~; 245 |; 35 &)
% ( 2 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 7 usr; 3 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 226 ( 0 sgn 211 !; 15 ?; 125 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k1_closure2(X0,X1)))
=> ( ( r1_closure3(X0,X1,X4,X3)
& r1_closure3(X0,X1,X3,X2) )
=> r1_closure3(X0,X1,X4,X2) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_closure3) ).
fof(f2,negated_conjecture,
~ ! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k1_closure2(X0,X1)))
=> ( ( r1_closure3(X0,X1,X4,X3)
& r1_closure3(X0,X1,X3,X2) )
=> r1_closure3(X0,X1,X4,X2) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f9,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
=> ( r1_closure3(X0,X1,X2,X3)
<=> ! [X4] :
~ ( ! [X5] :
~ ( r1_tarski(X4,X5)
& r2_hidden(X5,X2) )
& r2_hidden(X4,X3) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_closure3) ).
fof(f33,axiom,
! [X0,X1,X2,X3] :
( ( m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
& m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
& m1_pboole(X1,X0) )
=> r1_closure3(X0,X1,X3,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_closure3) ).
fof(f36,axiom,
! [X0,X1,X2] :
( ( r1_tarski(X1,X2)
& r1_tarski(X0,X1) )
=> r1_tarski(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_xboole_1) ).
fof(f56,plain,
? [X0,X1] :
( m1_pboole(X1,X0)
& ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
& ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k1_closure2(X0,X1)))
& r1_closure3(X0,X1,X4,X3)
& r1_closure3(X0,X1,X3,X2)
& ~ r1_closure3(X0,X1,X4,X2) ) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f57,plain,
? [X0,X1] :
( m1_pboole(X1,X0)
& ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
& ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k1_closure2(X0,X1)))
& r1_closure3(X0,X1,X4,X3)
& r1_closure3(X0,X1,X3,X2)
& ~ r1_closure3(X0,X1,X4,X2) ) ) ) ),
inference(flattening,[],[f56]) ).
fof(f64,plain,
! [X0,X1] :
( ~ m1_pboole(X1,X0)
| ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| ( r1_closure3(X0,X1,X2,X3)
<=> ! [X4] :
( ? [X5] :
( r1_tarski(X4,X5)
& r2_hidden(X5,X2) )
| ~ r2_hidden(X4,X3) ) ) ) ) ),
inference(ennf_transformation,[],[f9]) ).
fof(f72,plain,
! [X0,X1,X2,X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_pboole(X1,X0)
| r1_closure3(X0,X1,X3,X3) ),
inference(ennf_transformation,[],[f33]) ).
fof(f73,plain,
! [X0,X1,X2,X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_pboole(X1,X0)
| r1_closure3(X0,X1,X3,X3) ),
inference(flattening,[],[f72]) ).
fof(f75,plain,
! [X0,X1,X2] :
( ~ r1_tarski(X1,X2)
| ~ r1_tarski(X0,X1)
| r1_tarski(X0,X2) ),
inference(ennf_transformation,[],[f36]) ).
fof(f76,plain,
! [X0,X1,X2] :
( ~ r1_tarski(X1,X2)
| ~ r1_tarski(X0,X1)
| r1_tarski(X0,X2) ),
inference(flattening,[],[f75]) ).
fof(f85,plain,
( m1_pboole(sK1,sK0)
& m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
& m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1)))
& m1_subset_1(sK4,k1_zfmisc_1(k1_closure2(sK0,sK1)))
& r1_closure3(sK0,sK1,sK4,sK3)
& r1_closure3(sK0,sK1,sK3,sK2)
& ~ r1_closure3(sK0,sK1,sK4,sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4)],[f57]) ).
fof(f86,plain,
! [X0,X1] :
( ~ m1_pboole(X1,X0)
| ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| ( ( ~ r1_closure3(X0,X1,X2,X3)
| ! [X4] :
( ? [X5] :
( r1_tarski(X4,X5)
& r2_hidden(X5,X2) )
| ~ r2_hidden(X4,X3) ) )
& ( ? [X4] :
( ! [X5] :
( ~ r1_tarski(X4,X5)
| ~ r2_hidden(X5,X2) )
& r2_hidden(X4,X3) )
| r1_closure3(X0,X1,X2,X3) ) ) ) ) ),
inference(nnf_transformation,[],[f64]) ).
fof(f87,plain,
! [X0,X1] :
( ~ m1_pboole(X1,X0)
| ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| ( ( ~ r1_closure3(X0,X1,X2,X3)
| ! [X6] :
( ? [X7] :
( r1_tarski(X6,X7)
& r2_hidden(X7,X2) )
| ~ r2_hidden(X6,X3) ) )
& ( ? [X4] :
( ! [X5] :
( ~ r1_tarski(X4,X5)
| ~ r2_hidden(X5,X2) )
& r2_hidden(X4,X3) )
| r1_closure3(X0,X1,X2,X3) ) ) ) ) ),
inference(rectify,[],[f86]) ).
fof(f88,plain,
! [X0,X1] :
( ~ m1_pboole(X1,X0)
| ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| ( ( ~ r1_closure3(X0,X1,X2,X3)
| ! [X6] :
( ( r1_tarski(X6,sK6(X2,X6))
& r2_hidden(sK6(X2,X6),X2) )
| ~ r2_hidden(X6,X3) ) )
& ( ( ! [X5] :
( ~ r1_tarski(sK5(X2,X3),X5)
| ~ r2_hidden(X5,X2) )
& r2_hidden(sK5(X2,X3),X3) )
| r1_closure3(X0,X1,X2,X3) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6]),skolemize(X4,sK5(X2,X3)),skolemize(X7,sK6(X2,X6))],[f87]) ).
fof(f105,plain,
m1_pboole(sK1,sK0),
inference(cnf_transformation,[],[f85]) ).
fof(f106,plain,
m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1))),
inference(cnf_transformation,[],[f85]) ).
fof(f107,plain,
m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))),
inference(cnf_transformation,[],[f85]) ).
fof(f108,plain,
m1_subset_1(sK4,k1_zfmisc_1(k1_closure2(sK0,sK1))),
inference(cnf_transformation,[],[f85]) ).
fof(f109,plain,
r1_closure3(sK0,sK1,sK4,sK3),
inference(cnf_transformation,[],[f85]) ).
fof(f110,plain,
r1_closure3(sK0,sK1,sK3,sK2),
inference(cnf_transformation,[],[f85]) ).
fof(f111,plain,
~ r1_closure3(sK0,sK1,sK4,sK2),
inference(cnf_transformation,[],[f85]) ).
fof(f118,plain,
! [X2,X3,X0,X1,X6] :
( ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ r1_closure3(X0,X1,X2,X3)
| r1_tarski(X6,sK6(X2,X6))
| ~ r2_hidden(X6,X3) ),
inference(cnf_transformation,[],[f88]) ).
fof(f119,plain,
! [X2,X3,X0,X1,X6] :
( ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ r1_closure3(X0,X1,X2,X3)
| r2_hidden(sK6(X2,X6),X2)
| ~ r2_hidden(X6,X3) ),
inference(cnf_transformation,[],[f88]) ).
fof(f120,plain,
! [X2,X3,X0,X1,X5] :
( ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ r1_tarski(sK5(X2,X3),X5)
| ~ r2_hidden(X5,X2)
| r1_closure3(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f88]) ).
fof(f121,plain,
! [X2,X3,X0,X1] :
( ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| r2_hidden(sK5(X2,X3),X3)
| r1_closure3(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f88]) ).
fof(f161,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_pboole(X1,X0)
| r1_closure3(X0,X1,X3,X3) ),
inference(cnf_transformation,[],[f73]) ).
fof(f164,plain,
! [X2,X0,X1] :
( ~ r1_tarski(X1,X2)
| ~ r1_tarski(X0,X1)
| r1_tarski(X0,X2) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_49,negated_conjecture,
~ r1_closure3(sK0,sK1,sK4,sK2),
inference(cnf_transformation,[],[f111]) ).
tcf(c_50,negated_conjecture,
r1_closure3(sK0,sK1,sK3,sK2),
inference(cnf_transformation,[],[f110]) ).
tcf(c_51,negated_conjecture,
r1_closure3(sK0,sK1,sK4,sK3),
inference(cnf_transformation,[],[f109]) ).
tcf(c_52,negated_conjecture,
m1_subset_1(sK4,k1_zfmisc_1(k1_closure2(sK0,sK1))),
inference(cnf_transformation,[],[f108]) ).
tcf(c_53,negated_conjecture,
m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))),
inference(cnf_transformation,[],[f107]) ).
tcf(c_54,negated_conjecture,
m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1))),
inference(cnf_transformation,[],[f106]) ).
tcf(c_55,negated_conjecture,
m1_pboole(sK1,sK0),
inference(cnf_transformation,[],[f105]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r2_hidden(sK5(X0,X3),X3)
| r1_closure3(X1,X2,X0,X3)
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(cnf_transformation,[],[f121]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( r1_closure3(X1,X2,X0,X3)
| ~ r2_hidden(X4,X0)
| ~ m1_pboole(X2,X1)
| ~ r1_tarski(sK5(X0,X3),X4)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(cnf_transformation,[],[f120]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( r2_hidden(sK6(X0,X4),X0)
| ~ r2_hidden(X4,X3)
| ~ m1_pboole(X2,X1)
| ~ r1_closure3(X1,X2,X0,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( r1_tarski(X4,sK6(X0,X4))
| ~ r2_hidden(X4,X3)
| ~ m1_pboole(X2,X1)
| ~ r1_closure3(X1,X2,X0,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r1_closure3(X1,X2,X3,X3)
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(cnf_transformation,[],[f161]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1_tarski(X2,X1)
| ~ r1_tarski(X2,X0)
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f164]) ).
tcf(c_617,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r1_closure3(X0,X1,X3,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ( X1 != sK1 )
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_103]) ).
tcf(c_618,plain,
! [X0: $i,X1: $i] :
( r1_closure3(sK0,sK1,X1,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(unflattening,[status(thm)],[c_617]) ).
tcf(c_629,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( r1_tarski(X4,sK6(X2,X4))
| ~ r2_hidden(X4,X3)
| ~ r1_closure3(X0,X1,X2,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ( X1 != sK1 )
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_63]) ).
tcf(c_630,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1_tarski(X2,sK6(X0,X2))
| ~ r2_hidden(X2,X1)
| ~ r1_closure3(sK0,sK1,X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(unflattening,[status(thm)],[c_629]) ).
tcf(c_646,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( r2_hidden(sK6(X2,X4),X2)
| ~ r2_hidden(X4,X3)
| ~ r1_closure3(X0,X1,X2,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ( X1 != sK1 )
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_62]) ).
tcf(c_647,plain,
! [X0: $i,X1: $i,X2: $i] :
( r2_hidden(sK6(X0,X2),X0)
| ~ r2_hidden(X2,X1)
| ~ r1_closure3(sK0,sK1,X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(unflattening,[status(thm)],[c_646]) ).
tcf(c_663,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( r1_closure3(X0,X1,X2,X3)
| ~ r2_hidden(X4,X2)
| ~ r1_tarski(sK5(X2,X3),X4)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ( X1 != sK1 )
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_61]) ).
tcf(c_664,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1_closure3(sK0,sK1,X0,X1)
| ~ r2_hidden(X2,X0)
| ~ r1_tarski(sK5(X0,X1),X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(unflattening,[status(thm)],[c_663]) ).
tcf(c_680,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r2_hidden(sK5(X2,X3),X3)
| r1_closure3(X0,X1,X2,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ( X1 != sK1 )
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_60]) ).
tcf(c_681,plain,
! [X0: $i,X1: $i] :
( r1_closure3(sK0,sK1,X0,X1)
| r2_hidden(sK5(X0,X1),X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(unflattening,[status(thm)],[c_680]) ).
tcf(c_1051,plain,
! [X0: $i,X1: $i] :
( r2_hidden(sK5(X0,X1),X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ( sK1 != sK1 )
| ( sK0 != sK0 )
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_681]) ).
tcf(c_1052,plain,
( r2_hidden(sK5(sK4,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK4,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(unflattening,[status(thm)],[c_1051]) ).
tcf(c_1058,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r2_hidden(X2,X0)
| ~ r1_tarski(sK5(X0,X1),X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ( sK1 != sK1 )
| ( sK0 != sK0 )
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_664]) ).
tcf(c_1059,plain,
! [X0: $i] :
( ~ r2_hidden(X0,sK4)
| ~ r1_tarski(sK5(sK4,sK2),X0)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK4,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(unflattening,[status(thm)],[c_1058]) ).
tcf(c_1061,plain,
! [X0: $i] :
( ~ r2_hidden(X0,sK4)
| ~ r1_tarski(sK5(sK4,sK2),X0) ),
inference(global_subsumption_just,[status(thm)],[c_1059,c_54,c_52,c_1059]) ).
tcf(c_1089,plain,
! [X0: $i,X1: $i,X2: $i] :
( r2_hidden(sK6(X1,X2),X1)
| ~ r2_hidden(X2,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ( sK1 != sK1 )
| ( sK0 != sK0 )
| ( X1 != sK3 )
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_647]) ).
tcf(c_1090,plain,
! [X0: $i] :
( r2_hidden(sK6(sK3,X0),sK3)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(unflattening,[status(thm)],[c_1089]) ).
tcf(c_1092,plain,
! [X0: $i] :
( r2_hidden(sK6(sK3,X0),sK3)
| ~ r2_hidden(X0,sK2) ),
inference(global_subsumption_just,[status(thm)],[c_1090,c_54,c_53,c_1090]) ).
tcf(c_1101,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1_tarski(X2,sK6(X1,X2))
| ~ r2_hidden(X2,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ( sK1 != sK1 )
| ( sK0 != sK0 )
| ( X1 != sK3 )
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_630]) ).
tcf(c_1102,plain,
! [X0: $i] :
( r1_tarski(X0,sK6(sK3,X0))
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(unflattening,[status(thm)],[c_1101]) ).
tcf(c_1117,plain,
! [X0: $i,X1: $i,X2: $i] :
( r2_hidden(sK6(X0,X2),X0)
| ~ r2_hidden(X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ( sK1 != sK1 )
| ( sK0 != sK0 )
| ( X1 != sK3 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_51,c_647]) ).
tcf(c_1118,plain,
! [X0: $i] :
( r2_hidden(sK6(sK4,X0),sK4)
| ~ r2_hidden(X0,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK4,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(unflattening,[status(thm)],[c_1117]) ).
tcf(c_1120,plain,
! [X0: $i] :
( r2_hidden(sK6(sK4,X0),sK4)
| ~ r2_hidden(X0,sK3) ),
inference(global_subsumption_just,[status(thm)],[c_1118,c_53,c_52,c_1118]) ).
tcf(c_1129,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1_tarski(X2,sK6(X0,X2))
| ~ r2_hidden(X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ( sK1 != sK1 )
| ( sK0 != sK0 )
| ( X1 != sK3 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_51,c_630]) ).
tcf(c_1130,plain,
! [X0: $i] :
( r1_tarski(X0,sK6(sK4,X0))
| ~ r2_hidden(X0,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK4,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(unflattening,[status(thm)],[c_1129]) ).
tcf(c_2167,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| r1_closure3(sK0,sK1,X0,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_618]) ).
tcf(c_2168,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_618]) ).
tcf(c_2169,plain,
( iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_618]) ).
tcf(c_2189,plain,
! [X0: $i] :
( r1_closure3(sK0,sK1,X0,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(global_subsumption_just,[status(thm)],[c_2167,c_2167,c_2168,c_2169]) ).
tcf(c_2696,plain,
! [X0: $i] :
( r1_closure3(sK0,sK1,X0,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(prop_impl_just,[status(thm)],[c_2189]) ).
tcf(c_3238,plain,
( r1_closure3(sK0,sK1,sK3,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(instantiation,[status(thm)],[c_2696]) ).
tcf(c_3836,plain,
! [X0: $i,X1: $i] :
( r1_tarski(X1,sK6(sK3,X1))
| ~ r2_hidden(X1,X0)
| ~ r1_closure3(sK0,sK1,sK3,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(superposition,[status(thm)],[c_53,c_630]) ).
tcf(c_3881,plain,
! [X0: $i] :
( r1_tarski(X0,sK6(sK3,X0))
| ~ r2_hidden(X0,sK3)
| ~ r1_closure3(sK0,sK1,sK3,sK3) ),
inference(superposition,[status(thm)],[c_53,c_3836]) ).
tcf(c_7019,plain,
! [X0: $i,X1: $i] :
( r1_tarski(X1,sK6(sK4,X1))
| ~ r2_hidden(X1,X0)
| ~ r1_closure3(sK0,sK1,sK4,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(superposition,[status(thm)],[c_52,c_630]) ).
tcf(c_7025,plain,
! [X0: $i] :
( r1_tarski(X0,sK6(sK4,X0))
| ~ r2_hidden(X0,sK3)
| ~ r1_closure3(sK0,sK1,sK4,sK3) ),
inference(superposition,[status(thm)],[c_53,c_7019]) ).
tcf(c_7059,plain,
! [X0: $i] :
( r1_tarski(X0,sK6(sK4,X0))
| ~ r2_hidden(X0,sK3) ),
inference(global_subsumption_just,[status(thm)],[c_7025,c_53,c_52,c_1130]) ).
tcf(c_7235,plain,
! [X0: $i,X1: $i] :
( r1_tarski(X0,sK6(sK4,X1))
| ~ r2_hidden(X1,sK3)
| ~ r1_tarski(X0,X1) ),
inference(superposition,[status(thm)],[c_7059,c_106]) ).
tcf(c_7249,plain,
! [X0: $i,X1: $i] :
( r1_closure3(sK0,sK1,sK4,X0)
| ~ r2_hidden(X1,sK4)
| ~ r1_tarski(sK5(sK4,X0),X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(superposition,[status(thm)],[c_52,c_664]) ).
tcf(c_7262,plain,
! [X0: $i] :
( r1_closure3(sK0,sK1,sK4,sK2)
| ~ r2_hidden(X0,sK4)
| ~ r1_tarski(sK5(sK4,sK2),X0) ),
inference(superposition,[status(thm)],[c_54,c_7249]) ).
tcf(c_7271,plain,
! [X0: $i] :
( ~ r1_tarski(sK5(sK4,sK2),X0)
| ~ r2_hidden(X0,sK4) ),
inference(global_subsumption_just,[status(thm)],[c_7262,c_1061]) ).
tcf(c_7272,plain,
! [X0: $i] :
( ~ r2_hidden(X0,sK4)
| ~ r1_tarski(sK5(sK4,sK2),X0) ),
inference(renaming,[status(thm)],[c_7271]) ).
tcf(c_8443,plain,
! [X0: $i] :
( ~ r2_hidden(X0,sK3)
| ~ r1_tarski(sK5(sK4,sK2),X0)
| ~ r2_hidden(sK6(sK4,X0),sK4) ),
inference(superposition,[status(thm)],[c_7235,c_7272]) ).
tcf(c_11868,plain,
! [X0: $i,X1: $i] :
( r1_tarski(X1,sK6(sK3,X1))
| ~ r2_hidden(X1,X0)
| ~ r1_closure3(sK0,sK1,sK3,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(superposition,[status(thm)],[c_53,c_630]) ).
tcf(c_11886,plain,
! [X0: $i] :
( r1_tarski(X0,sK6(sK3,X0))
| ~ r2_hidden(X0,sK3)
| ~ r1_closure3(sK0,sK1,sK3,sK3) ),
inference(superposition,[status(thm)],[c_53,c_11868]) ).
tcf(c_11887,plain,
! [X0: $i] :
( r1_tarski(X0,sK6(sK3,X0))
| ~ r2_hidden(X0,sK2)
| ~ r1_closure3(sK0,sK1,sK3,sK2) ),
inference(superposition,[status(thm)],[c_54,c_11868]) ).
tcf(c_11893,plain,
! [X0: $i] :
( r1_tarski(X0,sK6(sK3,X0))
| ~ r2_hidden(X0,sK3) ),
inference(global_subsumption_just,[status(thm)],[c_11886,c_53,c_3238,c_3881]) ).
tcf(c_11920,plain,
! [X0: $i] :
( r1_tarski(X0,sK6(sK3,X0))
| ~ r2_hidden(X0,sK2) ),
inference(global_subsumption_just,[status(thm)],[c_11887,c_54,c_53,c_1102]) ).
tcf(c_11939,plain,
! [X0: $i,X1: $i] :
( r2_hidden(sK6(sK3,X1),sK3)
| ~ r2_hidden(X1,X0)
| ~ r1_closure3(sK0,sK1,sK3,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(superposition,[status(thm)],[c_53,c_647]) ).
tcf(c_11993,plain,
! [X0: $i] :
( r2_hidden(sK6(sK3,X0),sK3)
| ~ r2_hidden(X0,sK2)
| ~ r1_closure3(sK0,sK1,sK3,sK2) ),
inference(superposition,[status(thm)],[c_54,c_11939]) ).
tcf(c_12008,plain,
! [X0: $i] :
( r2_hidden(sK6(sK3,X0),sK3)
| ~ r2_hidden(X0,sK2) ),
inference(global_subsumption_just,[status(thm)],[c_11993,c_1092]) ).
tcf(c_12061,plain,
! [X0: $i,X1: $i] :
( r1_tarski(X0,sK6(sK3,X1))
| ~ r2_hidden(X1,sK3)
| ~ r1_tarski(X0,X1) ),
inference(superposition,[status(thm)],[c_11893,c_106]) ).
tcf(c_12092,plain,
! [X0: $i,X1: $i] :
( r1_closure3(sK0,sK1,sK4,X0)
| ~ r2_hidden(X1,sK4)
| ~ r1_tarski(sK5(sK4,X0),X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(superposition,[status(thm)],[c_52,c_664]) ).
tcf(c_12105,plain,
! [X0: $i] :
( r1_closure3(sK0,sK1,sK4,sK2)
| ~ r2_hidden(X0,sK4)
| ~ r1_tarski(sK5(sK4,sK2),X0) ),
inference(superposition,[status(thm)],[c_54,c_12092]) ).
tcf(c_12129,plain,
! [X0: $i] :
( ~ r1_tarski(sK5(sK4,sK2),X0)
| ~ r2_hidden(X0,sK4) ),
inference(global_subsumption_just,[status(thm)],[c_12105,c_1061]) ).
tcf(c_12130,plain,
! [X0: $i] :
( ~ r2_hidden(X0,sK4)
| ~ r1_tarski(sK5(sK4,sK2),X0) ),
inference(renaming,[status(thm)],[c_12129]) ).
tcf(c_12413,plain,
! [X0: $i] :
( ~ r2_hidden(X0,sK3)
| ~ r1_tarski(sK5(sK4,sK2),X0)
| ~ r2_hidden(sK6(sK3,X0),sK4) ),
inference(superposition,[status(thm)],[c_12061,c_12130]) ).
tcf(c_13266,plain,
! [X0: $i] :
( ~ r2_hidden(X0,sK3)
| ~ r1_tarski(sK5(sK4,sK2),X0) ),
inference(global_subsumption_just,[status(thm)],[c_12413,c_1120,c_8443]) ).
tcf(c_13273,plain,
( ~ r2_hidden(sK5(sK4,sK2),sK2)
| ~ r2_hidden(sK6(sK3,sK5(sK4,sK2)),sK3) ),
inference(superposition,[status(thm)],[c_11920,c_13266]) ).
tcf(c_13298,plain,
~ r2_hidden(sK6(sK3,sK5(sK4,sK2)),sK3),
inference(global_subsumption_just,[status(thm)],[c_13273,c_54,c_52,c_1052,c_13273]) ).
tcf(c_13303,plain,
~ r2_hidden(sK5(sK4,sK2),sK2),
inference(superposition,[status(thm)],[c_12008,c_13298]) ).
tcf(c_13305,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_13303,c_1052,c_52,c_54]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG223+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.10/0.37 % Computer : n010.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Fri Sep 25 05:10:00 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 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.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 8.56/1.64 % SZS status Started for theBenchmark.p
% 8.56/1.64 % SZS status Theorem for theBenchmark.p
% 8.56/1.64
% 8.56/1.64 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.56/1.64
% 8.56/1.64 % ------ iProver source info
% 8.56/1.64
% 8.56/1.64 % git: date: 2026-07-19 20:42:38 +0200
% 8.56/1.64 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.56/1.64 % git: non_committed_changes: false
% 8.56/1.64
% 8.56/1.64 % ------ Parsing...
% 8.56/1.64 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 8.56/1.64
% 8.56/1.64 % ------ Preprocessing... sup_sim: 0 sf_s rm: 24 0s sf_e pe_s pe:1:0s pe_e sup_sim: 0 sf_s rm: 5 0s sf_e pe_s pe_e %
% 8.56/1.64
% 8.56/1.64 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e %
% 8.56/1.64
% 8.56/1.64 % ------ Preprocessing... sf_s rm: 3 0s sf_e sf_s rm: 0 0s sf_e
% 8.56/1.64 % ------ Proving...
% 8.56/1.64 % ------ Problem Properties
% 8.56/1.64
% 8.56/1.64 %
% 8.56/1.64 % clauses 56
% 8.56/1.64 % conjectures 6
% 8.56/1.64 % EPR 20
% 8.56/1.64 % Horn 49
% 8.56/1.64 % unary 27
% 8.56/1.64 % binary 14
% 8.56/1.64 % lits 114
% 8.56/1.64 % lits eq 2
% 8.56/1.64 % fd_pure 0
% 8.56/1.64 % fd_pseudo 0
% 8.56/1.64 % fd_cond 1
% 8.56/1.64 % fd_pseudo_cond 1
% 8.56/1.64 % AC symbols 0
% 8.56/1.64
% 8.56/1.64 % ------ Input Options Time Limit: Unbounded
% 8.56/1.64
% 8.56/1.64
% 8.56/1.64 % ------
% 8.56/1.64 % Current options:
% 8.56/1.64 % ------
% 8.56/1.64
% 8.56/1.64
% 8.56/1.64 %
% 8.56/1.64
% 8.56/1.64 % ------ Proving...
% 8.56/1.64 %
% 8.56/1.64
% 8.56/1.64 % SZS status Theorem for theBenchmark.p
% 8.56/1.64
% 8.56/1.64 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.56/1.65
% 8.56/1.65
%------------------------------------------------------------------------------