%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT294+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 : Thu Sep 24 01:02:35 PM UTC 2026
% Result : Theorem 0.12s 0.40s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 36
% Syntax : Number of formulae : 183 ( 40 unt; 30 def)
% Number of atoms : 822 ( 18 equ)
% Maximal formula atoms : 23 ( 4 avg)
% Number of connectives : 1102 ( 463 ~; 497 |; 82 &)
% ( 32 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 41 ( 39 usr; 31 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 144 ( 138 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ~ v1_xboole_0(A)
=> ! [B] :
( ( m1_subset_1(B,k1_zfmisc_1(A))
& ~ v1_xboole_0(B) )
=> ! [C] :
( ( m2_relset_1(C,k2_zfmisc_1(A,A),A)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& v1_funct_1(C) )
=> ! [D] :
( ( m2_relset_1(D,k2_zfmisc_1(A,A),A)
& v1_funct_2(D,k2_zfmisc_1(A,A),A)
& v1_funct_1(D) )
=> ! [E] :
( ( m2_relset_1(E,k2_zfmisc_1(B,B),B)
& v1_funct_2(E,k2_zfmisc_1(B,B),B)
& v1_funct_1(E) )
=> ! [F] :
( ( m2_relset_1(F,k2_zfmisc_1(B,B),B)
& v1_funct_2(F,k2_zfmisc_1(B,B),B)
& v1_funct_1(F) )
=> ( ( r6_binop_1(A,C,D)
& F = k1_realset1(D,B)
& E = k1_realset1(C,B) )
=> r6_binop_1(B,E,F) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ~ v1_xboole_0(A)
=> ! [B] :
( ( m1_subset_1(B,k1_zfmisc_1(A))
& ~ v1_xboole_0(B) )
=> ! [C] :
( ( m2_relset_1(C,k2_zfmisc_1(A,A),A)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& v1_funct_1(C) )
=> ! [D] :
( ( m2_relset_1(D,k2_zfmisc_1(A,A),A)
& v1_funct_2(D,k2_zfmisc_1(A,A),A)
& v1_funct_1(D) )
=> ! [E] :
( ( m2_relset_1(E,k2_zfmisc_1(B,B),B)
& v1_funct_2(E,k2_zfmisc_1(B,B),B)
& v1_funct_1(E) )
=> ! [F] :
( ( m2_relset_1(F,k2_zfmisc_1(B,B),B)
& v1_funct_2(F,k2_zfmisc_1(B,B),B)
& v1_funct_1(F) )
=> ( ( r6_binop_1(A,C,D)
& F = k1_realset1(D,B)
& E = k1_realset1(C,B) )
=> r6_binop_1(B,E,F) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f5,axiom,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> v1_relat_1(C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B] :
( ( m2_relset_1(B,k2_zfmisc_1(A,A),A)
& v1_funct_2(B,k2_zfmisc_1(A,A),A)
& v1_funct_1(B) )
=> ! [C] :
( ( m2_relset_1(C,k2_zfmisc_1(A,A),A)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& v1_funct_1(C) )
=> ( r6_binop_1(A,B,C)
<=> ( r5_binop_1(A,B,C)
& r4_binop_1(A,B,C) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,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/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [A,B] :
( ( v1_funct_1(A)
& v1_relat_1(A) )
=> ( v1_funct_1(k1_realset1(A,B))
& v1_relat_1(k1_realset1(A,B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [A] :
( ~ v1_xboole_0(A)
=> ! [B] :
( ( m1_subset_1(B,k1_zfmisc_1(A))
& ~ v1_xboole_0(B) )
=> ! [C] :
( ( m2_relset_1(C,k2_zfmisc_1(A,A),A)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& v1_funct_1(C) )
=> ! [D] :
( ( m2_relset_1(D,k2_zfmisc_1(A,A),A)
& v1_funct_2(D,k2_zfmisc_1(A,A),A)
& v1_funct_1(D) )
=> ! [E] :
( ( m2_relset_1(E,k2_zfmisc_1(B,B),B)
& v1_funct_2(E,k2_zfmisc_1(B,B),B)
& v1_funct_1(E) )
=> ! [F] :
( ( m2_relset_1(F,k2_zfmisc_1(B,B),B)
& v1_funct_2(F,k2_zfmisc_1(B,B),B)
& v1_funct_1(F) )
=> ( ( F = k1_realset1(D,B)
& E = k1_realset1(C,B) )
=> ( ( r5_binop_1(A,C,D)
=> r5_binop_1(B,E,F) )
& ( r4_binop_1(A,C,D)
=> r4_binop_1(B,E,F) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ? [E] :
( ? [F] :
( ~ r6_binop_1(B,E,F)
& r6_binop_1(A,C,D)
& F = k1_realset1(D,B)
& E = k1_realset1(C,B)
& m2_relset_1(F,k2_zfmisc_1(B,B),B)
& v1_funct_2(F,k2_zfmisc_1(B,B),B)
& v1_funct_1(F) )
& m2_relset_1(E,k2_zfmisc_1(B,B),B)
& v1_funct_2(E,k2_zfmisc_1(B,B),B)
& v1_funct_1(E) )
& m2_relset_1(D,k2_zfmisc_1(A,A),A)
& v1_funct_2(D,k2_zfmisc_1(A,A),A)
& v1_funct_1(D) )
& m2_relset_1(C,k2_zfmisc_1(A,A),A)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& v1_funct_1(C) )
& m1_subset_1(B,k1_zfmisc_1(A))
& ~ v1_xboole_0(B) )
& ~ v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f45,plain,
( ~ r6_binop_1(sK1_skl,sK4_skl,sK5_skl)
& r6_binop_1(sK0_skl,sK2_skl,sK3_skl)
& sK5_skl = k1_realset1(sK3_skl,sK1_skl)
& sK4_skl = k1_realset1(sK2_skl,sK1_skl)
& m2_relset_1(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
& v1_funct_2(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
& v1_funct_1(sK5_skl)
& m2_relset_1(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
& v1_funct_2(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
& v1_funct_1(sK4_skl)
& m2_relset_1(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
& v1_funct_2(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
& v1_funct_1(sK3_skl)
& m2_relset_1(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
& v1_funct_2(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
& v1_funct_1(sK2_skl)
& m1_subset_1(sK1_skl,k1_zfmisc_1(sK0_skl))
& ~ v1_xboole_0(sK1_skl)
& ~ v1_xboole_0(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl),skolemize(D,sK3_skl),skolemize(E,sK4_skl),skolemize(F,sK5_skl)],[f44]) ).
fof(f46,plain,
~ v1_xboole_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f47,plain,
~ v1_xboole_0(sK1_skl),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f48,plain,
m1_subset_1(sK1_skl,k1_zfmisc_1(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f49,plain,
v1_funct_1(sK2_skl),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f50,plain,
v1_funct_2(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f51,plain,
m2_relset_1(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f52,plain,
v1_funct_1(sK3_skl),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f53,plain,
v1_funct_2(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f54,plain,
m2_relset_1(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f55,plain,
v1_funct_1(sK4_skl),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f56,plain,
v1_funct_2(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f57,plain,
m2_relset_1(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f58,plain,
v1_funct_1(sK5_skl),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f59,plain,
v1_funct_2(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f60,plain,
m2_relset_1(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f61,plain,
sK4_skl = k1_realset1(sK2_skl,sK1_skl),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f62,plain,
sK5_skl = k1_realset1(sK3_skl,sK1_skl),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f63,plain,
r6_binop_1(sK0_skl,sK2_skl,sK3_skl),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f64,plain,
~ r6_binop_1(sK1_skl,sK4_skl,sK5_skl),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f69,plain,
! [A,B,C] :
( v1_relat_1(C)
| ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f70,plain,
! [C] :
( v1_relat_1(C)
| ! [A,B] : ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(miniscoping,[status(thm)],[f69]) ).
fof(f71,plain,
! [X0,X1,X2] :
( v1_relat_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f76,plain,
! [A,B] :
( ! [C] :
( ( r6_binop_1(A,B,C)
<=> ( r5_binop_1(A,B,C)
& r4_binop_1(A,B,C) ) )
| ~ m2_relset_1(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(C) )
| ~ m2_relset_1(B,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(B,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(B) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f77,plain,
! [A,B] :
( ! [C] :
( ( ( ~ r5_binop_1(A,B,C)
| ~ r4_binop_1(A,B,C)
| r6_binop_1(A,B,C) )
& ( ( r5_binop_1(A,B,C)
& r4_binop_1(A,B,C) )
| ~ r6_binop_1(A,B,C) ) )
| ~ m2_relset_1(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(C) )
| ~ m2_relset_1(B,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(B,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(B) ),
inference(NNF_transformation,[status(thm)],[f76]) ).
fof(f78,plain,
! [X0,X1,X2] :
( r4_binop_1(X1,X0,X2)
| ~ r6_binop_1(X1,X0,X2)
| ~ m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X0) ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f79,plain,
! [X0,X1,X2] :
( r5_binop_1(X1,X0,X2)
| ~ r6_binop_1(X1,X0,X2)
| ~ m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X0) ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f80,plain,
! [X0,X1,X2] :
( ~ r5_binop_1(X1,X0,X2)
| ~ r4_binop_1(X1,X0,X2)
| r6_binop_1(X1,X0,X2)
| ~ m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X0) ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f86,plain,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
| ~ m2_relset_1(C,A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f87,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f99,plain,
! [A,B] :
( ( v1_funct_1(k1_realset1(A,B))
& v1_relat_1(k1_realset1(A,B)) )
| ~ v1_funct_1(A)
| ~ v1_relat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f100,plain,
! [A] :
( ( ! [B] : v1_funct_1(k1_realset1(A,B))
& ! [B] : v1_relat_1(k1_realset1(A,B)) )
| ~ v1_funct_1(A)
| ~ v1_relat_1(A) ),
inference(miniscoping,[status(thm)],[f99]) ).
fof(f102,plain,
! [X0,X1] :
( v1_funct_1(k1_realset1(X0,X1))
| ~ v1_funct_1(X0)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f141,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ! [F] :
( ( ( r5_binop_1(B,E,F)
| ~ r5_binop_1(A,C,D) )
& ( r4_binop_1(B,E,F)
| ~ r4_binop_1(A,C,D) ) )
| F != k1_realset1(D,B)
| E != k1_realset1(C,B)
| ~ m2_relset_1(F,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(F,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(F) )
| ~ m2_relset_1(E,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(E,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(E) )
| ~ m2_relset_1(D,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(D,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(D) )
| ~ m2_relset_1(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(C) )
| ~ m1_subset_1(B,k1_zfmisc_1(A))
| v1_xboole_0(B) )
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f142,plain,
! [X0,X1,X2,X3,X4,X5] :
( r4_binop_1(X1,X4,X5)
| ~ r4_binop_1(X0,X2,X3)
| X5 != k1_realset1(X3,X1)
| X4 != k1_realset1(X2,X1)
| ~ m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X5)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f143,plain,
! [X0,X1,X2,X3,X4,X5] :
( r5_binop_1(X1,X4,X5)
| ~ r5_binop_1(X0,X2,X3)
| X5 != k1_realset1(X3,X1)
| X4 != k1_realset1(X2,X1)
| ~ m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X5)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f162,plain,
! [X0,X1,X2,X3] :
( r4_binop_1(X1,k1_realset1(X2,X1),k1_realset1(X3,X1))
| ~ r4_binop_1(X0,X2,X3)
| ~ m2_relset_1(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X3,X1))
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f142]) ).
fof(f163,plain,
! [X0,X1,X2,X3] :
( r5_binop_1(X1,k1_realset1(X2,X1),k1_realset1(X3,X1))
| ~ r5_binop_1(X0,X2,X3)
| ~ m2_relset_1(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X3,X1))
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f143]) ).
fof(f182,definition,
( sQ0_spl
<=> v1_relat_1(sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f184,plain,
( sQ0_spl
| ~ v1_relat_1(sK3_skl) ),
inference(component_clause,[status(thm)],[f182]) ).
fof(f189,definition,
( sQ2_spl
<=> v1_relat_1(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f191,plain,
( sQ2_spl
| ~ v1_relat_1(sK2_skl) ),
inference(component_clause,[status(thm)],[f189]) ).
fof(f196,plain,
! [X0,X1] :
( sQ2_spl
| ~ m1_subset_1(sK2_skl,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(resolution,[status(thm)],[f191,f71]) ).
fof(f197,plain,
! [X0,X1] :
( sQ0_spl
| ~ m1_subset_1(sK3_skl,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(resolution,[status(thm)],[f184,f71]) ).
fof(f207,plain,
! [X0,X1] :
( sQ2_spl
| ~ m2_relset_1(sK2_skl,X0,X1) ),
inference(resolution,[status(thm)],[f196,f87]) ).
fof(f208,plain,
( sQ2_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f51,f207]) ).
fof(f209,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f208]) ).
fof(f210,plain,
! [X0,X1] :
( sQ0_spl
| ~ m2_relset_1(sK3_skl,X0,X1) ),
inference(resolution,[status(thm)],[f197,f87]) ).
fof(f211,plain,
( sQ0_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f54,f210]) ).
fof(f212,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f211]) ).
fof(f213,plain,
( v1_funct_1(sK5_skl)
| ~ v1_funct_1(sK3_skl)
| ~ v1_relat_1(sK3_skl) ),
inference(paramodulation,[status(thm)],[f62,f102]) ).
fof(f214,plain,
( v1_funct_1(sK4_skl)
| ~ v1_funct_1(sK2_skl)
| ~ v1_relat_1(sK2_skl) ),
inference(paramodulation,[status(thm)],[f61,f102]) ).
fof(f215,definition,
( sQ4_spl
<=> v1_funct_1(sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f217,plain,
( sQ4_spl
| ~ v1_funct_1(sK3_skl) ),
inference(component_clause,[status(thm)],[f215]) ).
fof(f218,definition,
( sQ5_spl
<=> v1_funct_1(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f221,plain,
( sQ5_spl
| ~ sQ4_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f213,f182,f215,f218]) ).
fof(f222,definition,
( sQ6_spl
<=> v1_funct_1(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f224,plain,
( sQ6_spl
| ~ v1_funct_1(sK2_skl) ),
inference(component_clause,[status(thm)],[f222]) ).
fof(f225,definition,
( sQ7_spl
<=> v1_funct_1(sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f228,plain,
( sQ7_spl
| ~ sQ6_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f214,f189,f222,f225]) ).
fof(f229,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f224,f49]) ).
fof(f230,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f229]) ).
fof(f231,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f217,f52]) ).
fof(f232,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f231]) ).
fof(f233,plain,
( ~ r5_binop_1(sK1_skl,sK4_skl,sK5_skl)
| ~ r4_binop_1(sK1_skl,sK4_skl,sK5_skl)
| ~ m2_relset_1(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(sK5_skl)
| ~ m2_relset_1(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(sK4_skl) ),
inference(resolution,[status(thm)],[f80,f64]) ).
fof(f234,definition,
( sQ8_spl
<=> v1_funct_2(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f236,plain,
( sQ8_spl
| ~ v1_funct_2(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f234]) ).
fof(f237,definition,
( sQ9_spl
<=> m2_relset_1(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f239,plain,
( sQ9_spl
| ~ m2_relset_1(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f237]) ).
fof(f240,definition,
( sQ10_spl
<=> v1_funct_2(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f242,plain,
( sQ10_spl
| ~ v1_funct_2(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f240]) ).
fof(f243,definition,
( sQ11_spl
<=> m2_relset_1(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f245,plain,
( sQ11_spl
| ~ m2_relset_1(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f243]) ).
fof(f246,definition,
( sQ12_spl
<=> r4_binop_1(sK1_skl,sK4_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f248,plain,
( sQ12_spl
| ~ r4_binop_1(sK1_skl,sK4_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f246]) ).
fof(f249,definition,
( sQ13_spl
<=> r5_binop_1(sK1_skl,sK4_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f251,plain,
( sQ13_spl
| ~ r5_binop_1(sK1_skl,sK4_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f249]) ).
fof(f252,plain,
( ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ5_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f233,f225,f234,f237,f218,f240,f243,f246,f249]) ).
fof(f259,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f245,f60]) ).
fof(f260,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f259]) ).
fof(f261,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f242,f59]) ).
fof(f262,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f261]) ).
fof(f263,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f239,f57]) ).
fof(f264,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f263]) ).
fof(f265,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f236,f56]) ).
fof(f266,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f265]) ).
fof(f273,plain,
! [X0,X1,X2,X3] :
( ~ r6_binop_1(X0,X2,X3)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| r4_binop_1(X1,k1_realset1(X2,X1),k1_realset1(X3,X1))
| ~ m2_relset_1(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X3,X1))
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(resolution,[status(thm)],[f162,f78]) ).
fof(f274,plain,
! [X0,X1,X2,X3] :
( ~ r6_binop_1(X0,X2,X3)
| r4_binop_1(X1,k1_realset1(X2,X1),k1_realset1(X3,X1))
| ~ m2_relset_1(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X3,X1))
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f273]) ).
fof(f295,definition,
( sQ18_spl
<=> v1_xboole_0(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f296,plain,
( ~ sQ18_spl
| v1_xboole_0(sK1_skl) ),
inference(component_clause,[status(thm)],[f295]) ).
fof(f381,plain,
! [X0,X1,X2,X3] :
( ~ r6_binop_1(X0,X2,X3)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| r5_binop_1(X1,k1_realset1(X2,X1),k1_realset1(X3,X1))
| ~ m2_relset_1(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X3,X1))
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(resolution,[status(thm)],[f163,f79]) ).
fof(f382,plain,
! [X0,X1,X2,X3] :
( ~ r6_binop_1(X0,X2,X3)
| r5_binop_1(X1,k1_realset1(X2,X1),k1_realset1(X3,X1))
| ~ m2_relset_1(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X3,X1))
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f381]) ).
fof(f383,plain,
! [X0,X1] :
( ~ r6_binop_1(X0,X1,sK3_skl)
| r4_binop_1(sK1_skl,k1_realset1(X1,sK1_skl),k1_realset1(sK3_skl,sK1_skl))
| ~ m2_relset_1(k1_realset1(sK3_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(sK3_skl,sK1_skl))
| ~ m2_relset_1(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X1,sK1_skl))
| ~ m2_relset_1(sK3_skl,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(sK3_skl,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(sK3_skl)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(sK1_skl)
| v1_xboole_0(X0) ),
inference(paramodulation,[status(thm)],[f62,f274]) ).
fof(f385,definition,
! [X0,X1] :
( sQ26_spl
<=> ( ~ r6_binop_1(X0,X1,sK3_skl)
| r4_binop_1(sK1_skl,k1_realset1(X1,sK1_skl),k1_realset1(sK3_skl,sK1_skl))
| ~ m2_relset_1(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X1,sK1_skl))
| ~ m2_relset_1(sK3_skl,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(sK3_skl,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f386,plain,
! [X0,X1] :
( ~ sQ26_spl
| ~ r6_binop_1(X0,X1,sK3_skl)
| r4_binop_1(sK1_skl,k1_realset1(X1,sK1_skl),k1_realset1(sK3_skl,sK1_skl))
| ~ m2_relset_1(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X1,sK1_skl))
| ~ m2_relset_1(sK3_skl,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(sK3_skl,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(component_clause,[status(thm)],[f385]) ).
fof(f388,definition,
( sQ27_spl
<=> v1_funct_1(k1_realset1(sK3_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f390,plain,
( sQ27_spl
| ~ v1_funct_1(k1_realset1(sK3_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f388]) ).
fof(f391,definition,
( sQ28_spl
<=> m2_relset_1(k1_realset1(sK3_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f393,plain,
( sQ28_spl
| ~ m2_relset_1(k1_realset1(sK3_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f391]) ).
fof(f394,plain,
( ~ sQ28_spl
| ~ sQ10_spl
| ~ sQ27_spl
| ~ sQ4_spl
| sQ18_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f383,f385,f295,f215,f388,f240,f391]) ).
fof(f398,definition,
( sQ30_spl
<=> v1_funct_1(k1_realset1(sK2_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f400,plain,
( sQ30_spl
| ~ v1_funct_1(k1_realset1(sK2_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f398]) ).
fof(f401,definition,
( sQ31_spl
<=> m2_relset_1(k1_realset1(sK2_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f403,plain,
( sQ31_spl
| ~ m2_relset_1(k1_realset1(sK2_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f401]) ).
fof(f405,plain,
( ~ sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f296,f47]) ).
fof(f406,plain,
~ sQ18_spl,
inference(contradiction_clause,[status(thm)],[f405]) ).
fof(f407,plain,
( sQ31_spl
| ~ m2_relset_1(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
inference(forward_demodulation,[status(thm)],[f61,f403]) ).
fof(f408,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f407,f57]) ).
fof(f409,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f408]) ).
fof(f410,plain,
( sQ30_spl
| ~ v1_funct_1(sK4_skl) ),
inference(forward_demodulation,[status(thm)],[f61,f400]) ).
fof(f411,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f410,f55]) ).
fof(f412,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f411]) ).
fof(f414,plain,
( sQ28_spl
| ~ m2_relset_1(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
inference(forward_demodulation,[status(thm)],[f62,f393]) ).
fof(f415,plain,
( sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f414,f60]) ).
fof(f416,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f415]) ).
fof(f419,plain,
! [X0,X1] :
( ~ sQ26_spl
| ~ r6_binop_1(X0,X1,sK3_skl)
| r4_binop_1(sK1_skl,k1_realset1(X1,sK1_skl),sK5_skl)
| ~ m2_relset_1(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X1,sK1_skl))
| ~ m2_relset_1(sK3_skl,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(sK3_skl,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(forward_demodulation,[status(thm)],[f62,f386]) ).
fof(f421,plain,
! [X0,X1] :
( ~ r6_binop_1(X0,X1,sK3_skl)
| r5_binop_1(sK1_skl,k1_realset1(X1,sK1_skl),k1_realset1(sK3_skl,sK1_skl))
| ~ m2_relset_1(k1_realset1(sK3_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(sK3_skl,sK1_skl))
| ~ m2_relset_1(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X1,sK1_skl))
| ~ m2_relset_1(sK3_skl,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(sK3_skl,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(sK3_skl)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(sK1_skl)
| v1_xboole_0(X0) ),
inference(paramodulation,[status(thm)],[f62,f382]) ).
fof(f423,definition,
! [X0,X1] :
( sQ32_spl
<=> ( ~ r6_binop_1(X0,X1,sK3_skl)
| r5_binop_1(sK1_skl,k1_realset1(X1,sK1_skl),k1_realset1(sK3_skl,sK1_skl))
| ~ m2_relset_1(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X1,sK1_skl))
| ~ m2_relset_1(sK3_skl,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(sK3_skl,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f424,plain,
! [X0,X1] :
( ~ sQ32_spl
| ~ r6_binop_1(X0,X1,sK3_skl)
| r5_binop_1(sK1_skl,k1_realset1(X1,sK1_skl),k1_realset1(sK3_skl,sK1_skl))
| ~ m2_relset_1(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X1,sK1_skl))
| ~ m2_relset_1(sK3_skl,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(sK3_skl,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(component_clause,[status(thm)],[f423]) ).
fof(f426,plain,
( ~ sQ28_spl
| ~ sQ10_spl
| ~ sQ27_spl
| ~ sQ4_spl
| sQ18_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f421,f423,f295,f215,f388,f240,f391]) ).
fof(f431,plain,
( sQ27_spl
| ~ v1_funct_1(sK5_skl) ),
inference(forward_demodulation,[status(thm)],[f62,f390]) ).
fof(f432,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f431,f58]) ).
fof(f433,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f432]) ).
fof(f435,plain,
! [X0,X1] :
( ~ sQ32_spl
| ~ r6_binop_1(X0,X1,sK3_skl)
| r5_binop_1(sK1_skl,k1_realset1(X1,sK1_skl),sK5_skl)
| ~ m2_relset_1(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X1,sK1_skl))
| ~ m2_relset_1(sK3_skl,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(sK3_skl,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(forward_demodulation,[status(thm)],[f62,f424]) ).
fof(f443,definition,
( sQ34_spl
<=> v1_xboole_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f444,plain,
( ~ sQ34_spl
| v1_xboole_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f443]) ).
fof(f446,definition,
( sQ35_spl
<=> m1_subset_1(sK1_skl,k1_zfmisc_1(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f448,plain,
( sQ35_spl
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f446]) ).
fof(f452,definition,
( sQ37_spl
<=> m2_relset_1(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f454,plain,
( sQ37_spl
| ~ m2_relset_1(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f452]) ).
fof(f456,plain,
( sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f454,f51]) ).
fof(f457,plain,
sQ37_spl,
inference(contradiction_clause,[status(thm)],[f456]) ).
fof(f476,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f448,f48]) ).
fof(f477,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f476]) ).
fof(f478,plain,
( ~ sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f444,f46]) ).
fof(f479,plain,
~ sQ34_spl,
inference(contradiction_clause,[status(thm)],[f478]) ).
fof(f480,plain,
! [X0] :
( ~ sQ26_spl
| ~ r6_binop_1(sK0_skl,X0,sK3_skl)
| r4_binop_1(sK1_skl,k1_realset1(X0,sK1_skl),sK5_skl)
| ~ m2_relset_1(k1_realset1(X0,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X0,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X0,sK1_skl))
| ~ m2_relset_1(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
| ~ m2_relset_1(X0,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
| ~ v1_funct_2(X0,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
| ~ v1_funct_1(X0)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(sK0_skl))
| v1_xboole_0(sK0_skl) ),
inference(resolution,[status(thm)],[f419,f53]) ).
fof(f481,definition,
! [X0] :
( sQ39_spl
<=> ( ~ r6_binop_1(sK0_skl,X0,sK3_skl)
| r4_binop_1(sK1_skl,k1_realset1(X0,sK1_skl),sK5_skl)
| ~ m2_relset_1(k1_realset1(X0,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X0,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X0,sK1_skl))
| ~ m2_relset_1(X0,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
| ~ v1_funct_2(X0,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
| ~ v1_funct_1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f482,plain,
! [X0] :
( ~ sQ39_spl
| ~ r6_binop_1(sK0_skl,X0,sK3_skl)
| r4_binop_1(sK1_skl,k1_realset1(X0,sK1_skl),sK5_skl)
| ~ m2_relset_1(k1_realset1(X0,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X0,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X0,sK1_skl))
| ~ m2_relset_1(X0,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
| ~ v1_funct_2(X0,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
| ~ v1_funct_1(X0) ),
inference(component_clause,[status(thm)],[f481]) ).
fof(f484,definition,
( sQ40_spl
<=> m2_relset_1(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f486,plain,
( sQ40_spl
| ~ m2_relset_1(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f484]) ).
fof(f487,plain,
( ~ sQ26_spl
| ~ sQ40_spl
| sQ39_spl
| ~ sQ35_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f480,f443,f446,f481,f484,f385]) ).
fof(f528,plain,
! [X0] :
( ~ sQ32_spl
| ~ r6_binop_1(sK0_skl,X0,sK3_skl)
| r5_binop_1(sK1_skl,k1_realset1(X0,sK1_skl),sK5_skl)
| ~ m2_relset_1(k1_realset1(X0,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X0,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X0,sK1_skl))
| ~ m2_relset_1(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
| ~ m2_relset_1(X0,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
| ~ v1_funct_2(X0,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
| ~ v1_funct_1(X0)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(sK0_skl))
| v1_xboole_0(sK0_skl) ),
inference(resolution,[status(thm)],[f435,f53]) ).
fof(f529,definition,
! [X0] :
( sQ45_spl
<=> ( ~ r6_binop_1(sK0_skl,X0,sK3_skl)
| r5_binop_1(sK1_skl,k1_realset1(X0,sK1_skl),sK5_skl)
| ~ m2_relset_1(k1_realset1(X0,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X0,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X0,sK1_skl))
| ~ m2_relset_1(X0,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
| ~ v1_funct_2(X0,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
| ~ v1_funct_1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f530,plain,
! [X0] :
( ~ sQ45_spl
| ~ r6_binop_1(sK0_skl,X0,sK3_skl)
| r5_binop_1(sK1_skl,k1_realset1(X0,sK1_skl),sK5_skl)
| ~ m2_relset_1(k1_realset1(X0,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X0,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X0,sK1_skl))
| ~ m2_relset_1(X0,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
| ~ v1_funct_2(X0,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
| ~ v1_funct_1(X0) ),
inference(component_clause,[status(thm)],[f529]) ).
fof(f532,plain,
( ~ sQ32_spl
| ~ sQ40_spl
| sQ45_spl
| ~ sQ35_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f528,f443,f446,f529,f484,f423]) ).
fof(f533,plain,
( sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f486,f54]) ).
fof(f534,plain,
sQ40_spl,
inference(contradiction_clause,[status(thm)],[f533]) ).
fof(f540,definition,
( sQ47_spl
<=> v1_funct_2(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f542,plain,
( sQ47_spl
| ~ v1_funct_2(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f540]) ).
fof(f563,plain,
( sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f542,f50]) ).
fof(f564,plain,
sQ47_spl,
inference(contradiction_clause,[status(thm)],[f563]) ).
fof(f582,plain,
( ~ sQ39_spl
| ~ r6_binop_1(sK0_skl,sK2_skl,sK3_skl)
| r4_binop_1(sK1_skl,k1_realset1(sK2_skl,sK1_skl),sK5_skl)
| ~ m2_relset_1(k1_realset1(sK2_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(sK2_skl,sK1_skl))
| ~ m2_relset_1(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
| ~ v1_funct_2(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
| ~ v1_funct_1(sK2_skl) ),
inference(paramodulation,[status(thm)],[f61,f482]) ).
fof(f583,definition,
( sQ51_spl
<=> v1_funct_2(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f585,plain,
( sQ51_spl
| ~ v1_funct_2(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f583]) ).
fof(f593,definition,
( sQ54_spl
<=> r4_binop_1(sK1_skl,k1_realset1(sK2_skl,sK1_skl),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f594,plain,
( ~ sQ54_spl
| r4_binop_1(sK1_skl,k1_realset1(sK2_skl,sK1_skl),sK5_skl) ),
inference(component_clause,[status(thm)],[f593]) ).
fof(f596,definition,
( sQ55_spl
<=> r6_binop_1(sK0_skl,sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f598,plain,
( sQ55_spl
| ~ r6_binop_1(sK0_skl,sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f596]) ).
fof(f599,plain,
( ~ sQ39_spl
| ~ sQ55_spl
| sQ54_spl
| ~ sQ31_spl
| ~ sQ8_spl
| ~ sQ30_spl
| ~ sQ37_spl
| ~ sQ47_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f582,f222,f540,f452,f398,f234,f401,f593,f596,f481]) ).
fof(f600,plain,
( ~ sQ54_spl
| r4_binop_1(sK1_skl,sK4_skl,sK5_skl) ),
inference(forward_demodulation,[status(thm)],[f61,f594]) ).
fof(f601,plain,
( ~ sQ54_spl
| sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f600,f248]) ).
fof(f602,plain,
( ~ sQ54_spl
| sQ12_spl ),
inference(contradiction_clause,[status(thm)],[f601]) ).
fof(f603,plain,
( sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f598,f63]) ).
fof(f604,plain,
sQ55_spl,
inference(contradiction_clause,[status(thm)],[f603]) ).
fof(f618,plain,
( sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f585,f53]) ).
fof(f619,plain,
sQ51_spl,
inference(contradiction_clause,[status(thm)],[f618]) ).
fof(f673,plain,
( ~ sQ45_spl
| ~ r6_binop_1(sK0_skl,sK2_skl,sK3_skl)
| r5_binop_1(sK1_skl,k1_realset1(sK2_skl,sK1_skl),sK5_skl)
| ~ m2_relset_1(k1_realset1(sK2_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(sK2_skl,sK1_skl))
| ~ m2_relset_1(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
| ~ v1_funct_2(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)
| ~ v1_funct_1(sK2_skl) ),
inference(paramodulation,[status(thm)],[f61,f530]) ).
fof(f678,definition,
( sQ66_spl
<=> r5_binop_1(sK1_skl,k1_realset1(sK2_skl,sK1_skl),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f679,plain,
( ~ sQ66_spl
| r5_binop_1(sK1_skl,k1_realset1(sK2_skl,sK1_skl),sK5_skl) ),
inference(component_clause,[status(thm)],[f678]) ).
fof(f681,plain,
( ~ sQ45_spl
| ~ sQ55_spl
| sQ66_spl
| ~ sQ31_spl
| ~ sQ8_spl
| ~ sQ30_spl
| ~ sQ37_spl
| ~ sQ47_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f673,f222,f540,f452,f398,f234,f401,f678,f596,f529]) ).
fof(f682,plain,
( ~ sQ66_spl
| r5_binop_1(sK1_skl,sK4_skl,sK5_skl) ),
inference(forward_demodulation,[status(thm)],[f61,f679]) ).
fof(f683,plain,
( ~ sQ66_spl
| sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f682,f251]) ).
fof(f684,plain,
( ~ sQ66_spl
| sQ13_spl ),
inference(contradiction_clause,[status(thm)],[f683]) ).
fof(f685,plain,
$false,
inference(sat_refutation,[status(thm)],[f209,f212,f221,f228,f230,f232,f252,f260,f262,f264,f266,f394,f406,f409,f412,f416,f426,f433,f457,f477,f479,f487,f532,f534,f564,f599,f602,f604,f619,f681,f684]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT294+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n001.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.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 23:34:13 UTC 2026
% 0.12/0.35 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 0.12/0.40 % Refutation found
% 0.12/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.44 % Elapsed time: 0.067846 seconds
% 0.12/0.44 % CPU time: 0.243447 seconds
% 0.12/0.44 % Total memory used: 107.564 MB
% 0.12/0.44 % Net memory used: 107.373 MB
%------------------------------------------------------------------------------