%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU195+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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 02:19:37 PM UTC 2026
% Result : Theorem 0.13s 0.68s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 78
% Syntax : Number of formulae : 344 ( 46 unt; 53 def)
% Number of atoms : 1333 ( 303 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 1618 ( 629 ~; 700 |; 162 &)
% ( 100 <=>; 27 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 60 ( 58 usr; 54 prp; 0-2 aty)
% Number of functors : 41 ( 41 usr; 3 con; 0-5 aty)
% Number of variables : 640 ( 578 !; 62 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B] :
( relation(B)
=> ( B = identity_relation(A)
<=> ! [C,D] :
( in(ordered_pair(C,D),B)
<=> ( C = D
& in(C,A) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A] :
( relation(A)
=> ! [B,C] :
( relation(C)
=> ( C = relation_dom_restriction(A,B)
<=> ! [D,E] :
( in(ordered_pair(D,E),C)
<=> ( in(ordered_pair(D,E),A)
& in(D,B) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A,B] :
( ( A = empty_set
=> ( B = set_meet(A)
<=> B = empty_set ) )
& ( A != empty_set
=> ( B = set_meet(A)
<=> ! [C] :
( in(C,B)
<=> ! [D] :
( in(D,A)
=> in(C,D) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A,B] :
( B = singleton(A)
<=> ! [C] :
( in(C,B)
<=> C = A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ( A = B
<=> ! [C,D] :
( in(ordered_pair(C,D),A)
<=> in(ordered_pair(C,D),B) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A,B] :
( ( empty(A)
=> ( element(B,A)
<=> empty(B) ) )
& ( ~ empty(A)
=> ( element(B,A)
<=> in(B,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A,B,C] :
( C = unordered_pair(A,B)
<=> ! [D] :
( in(D,C)
<=> ( D = B
| D = A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ( subset(A,B)
<=> ! [C,D] :
( in(ordered_pair(C,D),A)
=> in(ordered_pair(C,D),B) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [A] :
( relation(A)
=> ! [B] :
( B = relation_dom(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(C,D),A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [A] :
( relation(A)
=> ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(D,C),A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ( B = relation_inverse(A)
<=> ! [C,D] :
( in(ordered_pair(C,D),B)
<=> in(ordered_pair(D,C),A) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ! [C] :
( relation(C)
=> ( C = relation_composition(A,B)
<=> ! [D,E] :
( in(ordered_pair(D,E),C)
<=> ? [F] :
( in(ordered_pair(F,E),B)
& in(ordered_pair(D,F),A) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [A,B] :
( ( relation(B)
& relation(A) )
=> relation(relation_composition(A,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [A] : relation(identity_relation(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [A,B] : ~ empty(ordered_pair(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [A] : ~ empty(singleton(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,axiom,
( relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f109,lemma,
! [A,B,C,D] :
~ ( A != D
& A != C
& unordered_pair(A,B) = unordered_pair(C,D) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f160,lemma,
! [A] :
( relation(A)
=> ( ! [B,C] : ~ in(ordered_pair(B,C),A)
=> A = empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f168,lemma,
! [A] : unordered_pair(A,A) = singleton(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f172,lemma,
! [A,B,C,D] :
( relation(D)
=> ( in(ordered_pair(A,B),relation_composition(identity_relation(C),D))
<=> ( in(ordered_pair(A,B),D)
& in(A,C) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f183,conjecture,
! [A,B] :
( relation(B)
=> relation_dom_restriction(B,A) = relation_composition(identity_relation(A),B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f184,negated_conjecture,
~ ! [A,B] :
( relation(B)
=> relation_dom_restriction(B,A) = relation_composition(identity_relation(A),B) ),
inference(negated_conjecture,[status(cth)],[f183]) ).
fof(f188,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f189,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f194,plain,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f197,plain,
! [A,B] :
( ( B = identity_relation(A)
<=> ! [C,D] :
( in(ordered_pair(C,D),B)
<=> ( C = D
& in(C,A) ) ) )
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f198,plain,
! [A,B] :
( ( ( ? [C,D] :
( ( ( C = D
& in(C,A) )
| in(ordered_pair(C,D),B) )
& ( C != D
| ~ in(C,A)
| ~ in(ordered_pair(C,D),B) ) )
| B = identity_relation(A) )
& ( ! [C,D] :
( ( C != D
| ~ in(C,A)
| in(ordered_pair(C,D),B) )
& ( ( C = D
& in(C,A) )
| ~ in(ordered_pair(C,D),B) ) )
| B != identity_relation(A) ) )
| ~ relation(B) ),
inference(NNF_transformation,[status(thm)],[f197]) ).
fof(f199,plain,
! [B] :
( ( ! [A] :
( ? [C,D] :
( ( ( C = D
& in(C,A) )
| in(ordered_pair(C,D),B) )
& ( C != D
| ~ in(C,A)
| ~ in(ordered_pair(C,D),B) ) )
| B = identity_relation(A) )
& ! [A] :
( ( ! [C,D] :
( C != D
| ~ in(C,A)
| in(ordered_pair(C,D),B) )
& ! [C,D] :
( ( C = D
& in(C,A) )
| ~ in(ordered_pair(C,D),B) ) )
| B != identity_relation(A) ) )
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f198]) ).
fof(f200,plain,
! [B] :
( ( ! [A] :
( ( ( ( sK0_skl(A,B) = sK1_skl(A,B)
& in(sK0_skl(A,B),A) )
| in(ordered_pair(sK0_skl(A,B),sK1_skl(A,B)),B) )
& ( sK0_skl(A,B) != sK1_skl(A,B)
| ~ in(sK0_skl(A,B),A)
| ~ in(ordered_pair(sK0_skl(A,B),sK1_skl(A,B)),B) ) )
| B = identity_relation(A) )
& ! [A] :
( ( ! [C,D] :
( C != D
| ~ in(C,A)
| in(ordered_pair(C,D),B) )
& ! [C,D] :
( ( C = D
& in(C,A) )
| ~ in(ordered_pair(C,D),B) ) )
| B != identity_relation(A) ) )
| ~ relation(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(C,sK0_skl(A,B)),skolemize(D,sK1_skl(A,B))],[f199]) ).
fof(f201,plain,
! [X0,X1,X2,X3] :
( in(X2,X1)
| ~ in(ordered_pair(X2,X3),X0)
| X0 != identity_relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f205,plain,
! [X0,X1] :
( in(sK0_skl(X1,X0),X1)
| in(ordered_pair(sK0_skl(X1,X0),sK1_skl(X1,X0)),X0)
| X0 = identity_relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f206,plain,
! [X0,X1] :
( sK0_skl(X1,X0) = sK1_skl(X1,X0)
| in(ordered_pair(sK0_skl(X1,X0),sK1_skl(X1,X0)),X0)
| X0 = identity_relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f212,plain,
! [A] :
( ! [B,C] :
( ( C = relation_dom_restriction(A,B)
<=> ! [D,E] :
( in(ordered_pair(D,E),C)
<=> ( in(ordered_pair(D,E),A)
& in(D,B) ) ) )
| ~ relation(C) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f213,plain,
! [A] :
( ! [B,C] :
( ( ( ? [D,E] :
( ( ( in(ordered_pair(D,E),A)
& in(D,B) )
| in(ordered_pair(D,E),C) )
& ( ~ in(ordered_pair(D,E),A)
| ~ in(D,B)
| ~ in(ordered_pair(D,E),C) ) )
| C = relation_dom_restriction(A,B) )
& ( ! [D,E] :
( ( ~ in(ordered_pair(D,E),A)
| ~ in(D,B)
| in(ordered_pair(D,E),C) )
& ( ( in(ordered_pair(D,E),A)
& in(D,B) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_dom_restriction(A,B) ) )
| ~ relation(C) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f212]) ).
fof(f214,plain,
! [A] :
( ! [C] :
( ( ! [B] :
( ? [D,E] :
( ( ( in(ordered_pair(D,E),A)
& in(D,B) )
| in(ordered_pair(D,E),C) )
& ( ~ in(ordered_pair(D,E),A)
| ~ in(D,B)
| ~ in(ordered_pair(D,E),C) ) )
| C = relation_dom_restriction(A,B) )
& ! [B] :
( ( ! [D,E] :
( ~ in(ordered_pair(D,E),A)
| ~ in(D,B)
| in(ordered_pair(D,E),C) )
& ! [D,E] :
( ( in(ordered_pair(D,E),A)
& in(D,B) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_dom_restriction(A,B) ) )
| ~ relation(C) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f213]) ).
fof(f215,plain,
! [A] :
( ! [C] :
( ( ! [B] :
( ( ( ( in(ordered_pair(sK2_skl(B,C,A),sK3_skl(B,C,A)),A)
& in(sK2_skl(B,C,A),B) )
| in(ordered_pair(sK2_skl(B,C,A),sK3_skl(B,C,A)),C) )
& ( ~ in(ordered_pair(sK2_skl(B,C,A),sK3_skl(B,C,A)),A)
| ~ in(sK2_skl(B,C,A),B)
| ~ in(ordered_pair(sK2_skl(B,C,A),sK3_skl(B,C,A)),C) ) )
| C = relation_dom_restriction(A,B) )
& ! [B] :
( ( ! [D,E] :
( ~ in(ordered_pair(D,E),A)
| ~ in(D,B)
| in(ordered_pair(D,E),C) )
& ! [D,E] :
( ( in(ordered_pair(D,E),A)
& in(D,B) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_dom_restriction(A,B) ) )
| ~ relation(C) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(D,sK2_skl(B,C,A)),skolemize(E,sK3_skl(B,C,A))],[f214]) ).
fof(f219,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(sK2_skl(X2,X1,X0),sK3_skl(X2,X1,X0)),X0)
| ~ in(sK2_skl(X2,X1,X0),X2)
| ~ in(ordered_pair(sK2_skl(X2,X1,X0),sK3_skl(X2,X1,X0)),X1)
| X1 = relation_dom_restriction(X0,X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f220,plain,
! [X0,X1,X2] :
( in(sK2_skl(X2,X1,X0),X2)
| in(ordered_pair(sK2_skl(X2,X1,X0),sK3_skl(X2,X1,X0)),X1)
| X1 = relation_dom_restriction(X0,X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f221,plain,
! [X0,X1,X2] :
( in(ordered_pair(sK2_skl(X2,X1,X0),sK3_skl(X2,X1,X0)),X0)
| in(ordered_pair(sK2_skl(X2,X1,X0),sK3_skl(X2,X1,X0)),X1)
| X1 = relation_dom_restriction(X0,X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f229,plain,
! [A,B] :
( ( ( B = set_meet(A)
<=> B = empty_set )
| A != empty_set )
& ( ( B = set_meet(A)
<=> ! [C] :
( in(C,B)
<=> ! [D] :
( in(C,D)
| ~ in(D,A) ) ) )
| A = empty_set ) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f230,plain,
! [A,B] :
( ( ( ( B != empty_set
| B = set_meet(A) )
& ( B = empty_set
| B != set_meet(A) ) )
| A != empty_set )
& ( ( ( ? [C] :
( ( ! [D] :
( in(C,D)
| ~ in(D,A) )
| in(C,B) )
& ( ? [D] :
( ~ in(C,D)
& in(D,A) )
| ~ in(C,B) ) )
| B = set_meet(A) )
& ( ! [C] :
( ( ? [D] :
( ~ in(C,D)
& in(D,A) )
| in(C,B) )
& ( ! [D] :
( in(C,D)
| ~ in(D,A) )
| ~ in(C,B) ) )
| B != set_meet(A) ) )
| A = empty_set ) ),
inference(NNF_transformation,[status(thm)],[f229]) ).
fof(f231,plain,
( ! [A] :
( ( ! [B] :
( B != empty_set
| B = set_meet(A) )
& ! [B] :
( B = empty_set
| B != set_meet(A) ) )
| A != empty_set )
& ! [A] :
( ( ! [B] :
( ? [C] :
( ( ! [D] :
( in(C,D)
| ~ in(D,A) )
| in(C,B) )
& ( ? [D] :
( ~ in(C,D)
& in(D,A) )
| ~ in(C,B) ) )
| B = set_meet(A) )
& ! [B] :
( ( ! [C] :
( ? [D] :
( ~ in(C,D)
& in(D,A) )
| in(C,B) )
& ! [C] :
( ! [D] :
( in(C,D)
| ~ in(D,A) )
| ~ in(C,B) ) )
| B != set_meet(A) ) )
| A = empty_set ) ),
inference(miniscoping,[status(thm)],[f230]) ).
fof(f232,plain,
( ! [A] :
( ( ! [B] :
( B != empty_set
| B = set_meet(A) )
& ! [B] :
( B = empty_set
| B != set_meet(A) ) )
| A != empty_set )
& ! [A] :
( ( ! [B] :
( ( ( ! [D] :
( in(sK8_skl(B,A),D)
| ~ in(D,A) )
| in(sK8_skl(B,A),B) )
& ( ( ~ in(sK8_skl(B,A),sK9_skl(B,A))
& in(sK9_skl(B,A),A) )
| ~ in(sK8_skl(B,A),B) ) )
| B = set_meet(A) )
& ! [B] :
( ( ! [C] :
( ( ~ in(C,sK7_skl(C,B,A))
& in(sK7_skl(C,B,A),A) )
| in(C,B) )
& ! [C] :
( ! [D] :
( in(C,D)
| ~ in(D,A) )
| ~ in(C,B) ) )
| B != set_meet(A) ) )
| A = empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl,sK9_skl]),skolemize(D,sK7_skl(C,B,A)),skolemize(C,sK8_skl(B,A)),skolemize(D,sK9_skl(B,A))],[f231]) ).
fof(f239,plain,
! [X0,X1] :
( X1 = empty_set
| X1 != set_meet(X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(thm)],[f232]) ).
fof(f241,plain,
! [A,B] :
( ( ? [C] :
( ( C = A
| in(C,B) )
& ( C != A
| ~ in(C,B) ) )
| B = singleton(A) )
& ( ! [C] :
( ( C != A
| in(C,B) )
& ( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(NNF_transformation,[status(thm)],[f12]) ).
fof(f242,plain,
( ! [A,B] :
( ? [C] :
( ( C = A
| in(C,B) )
& ( C != A
| ~ in(C,B) ) )
| B = singleton(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| in(C,B) )
& ! [C] :
( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(miniscoping,[status(thm)],[f241]) ).
fof(f243,plain,
( ! [A,B] :
( ( ( sK10_skl(B,A) = A
| in(sK10_skl(B,A),B) )
& ( sK10_skl(B,A) != A
| ~ in(sK10_skl(B,A),B) ) )
| B = singleton(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| in(C,B) )
& ! [C] :
( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(C,sK10_skl(B,A))],[f242]) ).
fof(f244,plain,
! [X0,X1,X2] :
( X2 = X1
| ~ in(X2,X0)
| X0 != singleton(X1) ),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f248,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(NNF_transformation,[status(thm)],[f13]) ).
fof(f249,plain,
( ! [A] :
( ? [B] : in(B,A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(miniscoping,[status(thm)],[f248]) ).
fof(f250,plain,
( ! [A] :
( in(sK11_skl(A),A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(B,sK11_skl(A))],[f249]) ).
fof(f251,plain,
! [X0,X1] :
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f260,plain,
! [A] :
( ! [B] :
( ( A = B
<=> ! [C,D] :
( in(ordered_pair(C,D),A)
<=> in(ordered_pair(C,D),B) ) )
| ~ relation(B) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f261,plain,
! [A] :
( ! [B] :
( ( ( ? [C,D] :
( ( in(ordered_pair(C,D),B)
| in(ordered_pair(C,D),A) )
& ( ~ in(ordered_pair(C,D),B)
| ~ in(ordered_pair(C,D),A) ) )
| A = B )
& ( ! [C,D] :
( ( ~ in(ordered_pair(C,D),B)
| in(ordered_pair(C,D),A) )
& ( in(ordered_pair(C,D),B)
| ~ in(ordered_pair(C,D),A) ) )
| A != B ) )
| ~ relation(B) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f260]) ).
fof(f262,plain,
! [A] :
( ! [B] :
( ( ( ? [C,D] :
( ( in(ordered_pair(C,D),B)
| in(ordered_pair(C,D),A) )
& ( ~ in(ordered_pair(C,D),B)
| ~ in(ordered_pair(C,D),A) ) )
| A = B )
& ( ( ! [C,D] :
( ~ in(ordered_pair(C,D),B)
| in(ordered_pair(C,D),A) )
& ! [C,D] :
( in(ordered_pair(C,D),B)
| ~ in(ordered_pair(C,D),A) ) )
| A != B ) )
| ~ relation(B) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f261]) ).
fof(f263,plain,
! [A] :
( ! [B] :
( ( ( ( ( in(ordered_pair(sK13_skl(B,A),sK14_skl(B,A)),B)
| in(ordered_pair(sK13_skl(B,A),sK14_skl(B,A)),A) )
& ( ~ in(ordered_pair(sK13_skl(B,A),sK14_skl(B,A)),B)
| ~ in(ordered_pair(sK13_skl(B,A),sK14_skl(B,A)),A) ) )
| A = B )
& ( ( ! [C,D] :
( ~ in(ordered_pair(C,D),B)
| in(ordered_pair(C,D),A) )
& ! [C,D] :
( in(ordered_pair(C,D),B)
| ~ in(ordered_pair(C,D),A) ) )
| A != B ) )
| ~ relation(B) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl]),skolemize(C,sK13_skl(B,A)),skolemize(D,sK14_skl(B,A))],[f262]) ).
fof(f267,plain,
! [X0,X1] :
( in(ordered_pair(sK13_skl(X1,X0),sK14_skl(X1,X0)),X1)
| in(ordered_pair(sK13_skl(X1,X0),sK14_skl(X1,X0)),X0)
| X0 = X1
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f263]) ).
fof(f268,plain,
! [A,B] :
( ( ( element(B,A)
<=> empty(B) )
| ~ empty(A) )
& ( ( element(B,A)
<=> in(B,A) )
| empty(A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f269,plain,
! [A,B] :
( ( ( ( ~ empty(B)
| element(B,A) )
& ( empty(B)
| ~ element(B,A) ) )
| ~ empty(A) )
& ( ( ( ~ in(B,A)
| element(B,A) )
& ( in(B,A)
| ~ element(B,A) ) )
| empty(A) ) ),
inference(NNF_transformation,[status(thm)],[f268]) ).
fof(f270,plain,
( ! [A] :
( ( ! [B] :
( ~ empty(B)
| element(B,A) )
& ! [B] :
( empty(B)
| ~ element(B,A) ) )
| ~ empty(A) )
& ! [A] :
( ( ! [B] :
( ~ in(B,A)
| element(B,A) )
& ! [B] :
( in(B,A)
| ~ element(B,A) ) )
| empty(A) ) ),
inference(miniscoping,[status(thm)],[f269]) ).
fof(f271,plain,
! [X0,X1] :
( in(X1,X0)
| ~ element(X1,X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f275,plain,
! [A,B,C] :
( ( ? [D] :
( ( D = B
| D = A
| in(D,C) )
& ( ( D != B
& D != A )
| ~ in(D,C) ) )
| C = unordered_pair(A,B) )
& ( ! [D] :
( ( ( D != B
& D != A )
| in(D,C) )
& ( D = B
| D = A
| ~ in(D,C) ) )
| C != unordered_pair(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f17]) ).
fof(f276,plain,
( ! [A,B,C] :
( ? [D] :
( ( D = B
| D = A
| in(D,C) )
& ( ( D != B
& D != A )
| ~ in(D,C) ) )
| C = unordered_pair(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ( D != B
& D != A )
| in(D,C) )
& ! [D] :
( D = B
| D = A
| ~ in(D,C) ) )
| C != unordered_pair(A,B) ) ),
inference(miniscoping,[status(thm)],[f275]) ).
fof(f277,plain,
( ! [A,B,C] :
( ( ( sK15_skl(C,B,A) = B
| sK15_skl(C,B,A) = A
| in(sK15_skl(C,B,A),C) )
& ( ( sK15_skl(C,B,A) != B
& sK15_skl(C,B,A) != A )
| ~ in(sK15_skl(C,B,A),C) ) )
| C = unordered_pair(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ( D != B
& D != A )
| in(D,C) )
& ! [D] :
( D = B
| D = A
| ~ in(D,C) ) )
| C != unordered_pair(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(D,sK15_skl(C,B,A))],[f276]) ).
fof(f278,plain,
! [X0,X1,X2,X3] :
( X3 = X2
| X3 = X1
| ~ in(X3,X0)
| X0 != unordered_pair(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f302,plain,
! [A] :
( ! [B] :
( ( subset(A,B)
<=> ! [C,D] :
( in(ordered_pair(C,D),B)
| ~ in(ordered_pair(C,D),A) ) )
| ~ relation(B) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f303,plain,
! [A] :
( ! [B] :
( ( ( ? [C,D] :
( ~ in(ordered_pair(C,D),B)
& in(ordered_pair(C,D),A) )
| subset(A,B) )
& ( ! [C,D] :
( in(ordered_pair(C,D),B)
| ~ in(ordered_pair(C,D),A) )
| ~ subset(A,B) ) )
| ~ relation(B) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f302]) ).
fof(f304,plain,
! [A] :
( ! [B] :
( ( ( ( ~ in(ordered_pair(sK22_skl(B,A),sK23_skl(B,A)),B)
& in(ordered_pair(sK22_skl(B,A),sK23_skl(B,A)),A) )
| subset(A,B) )
& ( ! [C,D] :
( in(ordered_pair(C,D),B)
| ~ in(ordered_pair(C,D),A) )
| ~ subset(A,B) ) )
| ~ relation(B) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl,sK23_skl]),skolemize(C,sK22_skl(B,A)),skolemize(D,sK23_skl(B,A))],[f303]) ).
fof(f306,plain,
! [X0,X1] :
( in(ordered_pair(sK22_skl(X1,X0),sK23_skl(X1,X0)),X0)
| subset(X0,X1)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f304]) ).
fof(f324,plain,
! [A] :
( ! [B] :
( B = relation_dom(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(C,D),A) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f325,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ( ? [D] : in(ordered_pair(C,D),A)
| in(C,B) )
& ( ! [D] : ~ in(ordered_pair(C,D),A)
| ~ in(C,B) ) )
| B = relation_dom(A) )
& ( ! [C] :
( ( ! [D] : ~ in(ordered_pair(C,D),A)
| in(C,B) )
& ( ? [D] : in(ordered_pair(C,D),A)
| ~ in(C,B) ) )
| B != relation_dom(A) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f324]) ).
fof(f326,plain,
! [A] :
( ( ! [B] :
( ? [C] :
( ( ? [D] : in(ordered_pair(C,D),A)
| in(C,B) )
& ( ! [D] : ~ in(ordered_pair(C,D),A)
| ~ in(C,B) ) )
| B = relation_dom(A) )
& ! [B] :
( ( ! [C] :
( ! [D] : ~ in(ordered_pair(C,D),A)
| in(C,B) )
& ! [C] :
( ? [D] : in(ordered_pair(C,D),A)
| ~ in(C,B) ) )
| B != relation_dom(A) ) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f325]) ).
fof(f327,plain,
! [A] :
( ( ! [B] :
( ( ( in(ordered_pair(sK27_skl(B,A),sK28_skl(B,A)),A)
| in(sK27_skl(B,A),B) )
& ( ! [D] : ~ in(ordered_pair(sK27_skl(B,A),D),A)
| ~ in(sK27_skl(B,A),B) ) )
| B = relation_dom(A) )
& ! [B] :
( ( ! [C] :
( ! [D] : ~ in(ordered_pair(C,D),A)
| in(C,B) )
& ! [C] :
( in(ordered_pair(C,sK26_skl(C,B,A)),A)
| ~ in(C,B) ) )
| B != relation_dom(A) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl,sK27_skl,sK28_skl]),skolemize(D,sK26_skl(C,B,A)),skolemize(C,sK27_skl(B,A)),skolemize(D,sK28_skl(B,A))],[f326]) ).
fof(f331,plain,
! [X0,X1] :
( in(ordered_pair(sK27_skl(X1,X0),sK28_skl(X1,X0)),X0)
| in(sK27_skl(X1,X0),X1)
| X1 = relation_dom(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f327]) ).
fof(f351,plain,
! [A] :
( ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(D,C),A) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f352,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ( ? [D] : in(ordered_pair(D,C),A)
| in(C,B) )
& ( ! [D] : ~ in(ordered_pair(D,C),A)
| ~ in(C,B) ) )
| B = relation_rng(A) )
& ( ! [C] :
( ( ! [D] : ~ in(ordered_pair(D,C),A)
| in(C,B) )
& ( ? [D] : in(ordered_pair(D,C),A)
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f351]) ).
fof(f353,plain,
! [A] :
( ( ! [B] :
( ? [C] :
( ( ? [D] : in(ordered_pair(D,C),A)
| in(C,B) )
& ( ! [D] : ~ in(ordered_pair(D,C),A)
| ~ in(C,B) ) )
| B = relation_rng(A) )
& ! [B] :
( ( ! [C] :
( ! [D] : ~ in(ordered_pair(D,C),A)
| in(C,B) )
& ! [C] :
( ? [D] : in(ordered_pair(D,C),A)
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f352]) ).
fof(f354,plain,
! [A] :
( ( ! [B] :
( ( ( in(ordered_pair(sK35_skl(B,A),sK34_skl(B,A)),A)
| in(sK34_skl(B,A),B) )
& ( ! [D] : ~ in(ordered_pair(D,sK34_skl(B,A)),A)
| ~ in(sK34_skl(B,A),B) ) )
| B = relation_rng(A) )
& ! [B] :
( ( ! [C] :
( ! [D] : ~ in(ordered_pair(D,C),A)
| in(C,B) )
& ! [C] :
( in(ordered_pair(sK33_skl(C,B,A),C),A)
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33_skl,sK34_skl,sK35_skl]),skolemize(D,sK33_skl(C,B,A)),skolemize(C,sK34_skl(B,A)),skolemize(D,sK35_skl(B,A))],[f353]) ).
fof(f358,plain,
! [X0,X1] :
( in(ordered_pair(sK35_skl(X1,X0),sK34_skl(X1,X0)),X0)
| in(sK34_skl(X1,X0),X1)
| X1 = relation_rng(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f354]) ).
fof(f364,plain,
! [A] :
( ! [B] :
( ( B = relation_inverse(A)
<=> ! [C,D] :
( in(ordered_pair(C,D),B)
<=> in(ordered_pair(D,C),A) ) )
| ~ relation(B) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f365,plain,
! [A] :
( ! [B] :
( ( ( ? [C,D] :
( ( in(ordered_pair(D,C),A)
| in(ordered_pair(C,D),B) )
& ( ~ in(ordered_pair(D,C),A)
| ~ in(ordered_pair(C,D),B) ) )
| B = relation_inverse(A) )
& ( ! [C,D] :
( ( ~ in(ordered_pair(D,C),A)
| in(ordered_pair(C,D),B) )
& ( in(ordered_pair(D,C),A)
| ~ in(ordered_pair(C,D),B) ) )
| B != relation_inverse(A) ) )
| ~ relation(B) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f364]) ).
fof(f366,plain,
! [A] :
( ! [B] :
( ( ( ? [C,D] :
( ( in(ordered_pair(D,C),A)
| in(ordered_pair(C,D),B) )
& ( ~ in(ordered_pair(D,C),A)
| ~ in(ordered_pair(C,D),B) ) )
| B = relation_inverse(A) )
& ( ( ! [C,D] :
( ~ in(ordered_pair(D,C),A)
| in(ordered_pair(C,D),B) )
& ! [C,D] :
( in(ordered_pair(D,C),A)
| ~ in(ordered_pair(C,D),B) ) )
| B != relation_inverse(A) ) )
| ~ relation(B) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f365]) ).
fof(f367,plain,
! [A] :
( ! [B] :
( ( ( ( ( in(ordered_pair(sK37_skl(B,A),sK36_skl(B,A)),A)
| in(ordered_pair(sK36_skl(B,A),sK37_skl(B,A)),B) )
& ( ~ in(ordered_pair(sK37_skl(B,A),sK36_skl(B,A)),A)
| ~ in(ordered_pair(sK36_skl(B,A),sK37_skl(B,A)),B) ) )
| B = relation_inverse(A) )
& ( ( ! [C,D] :
( ~ in(ordered_pair(D,C),A)
| in(ordered_pair(C,D),B) )
& ! [C,D] :
( in(ordered_pair(D,C),A)
| ~ in(ordered_pair(C,D),B) ) )
| B != relation_inverse(A) ) )
| ~ relation(B) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl,sK37_skl]),skolemize(C,sK36_skl(B,A)),skolemize(D,sK37_skl(B,A))],[f366]) ).
fof(f371,plain,
! [X0,X1] :
( in(ordered_pair(sK37_skl(X1,X0),sK36_skl(X1,X0)),X0)
| in(ordered_pair(sK36_skl(X1,X0),sK37_skl(X1,X0)),X1)
| X1 = relation_inverse(X0)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f367]) ).
fof(f376,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( C = relation_composition(A,B)
<=> ! [D,E] :
( in(ordered_pair(D,E),C)
<=> ? [F] :
( in(ordered_pair(F,E),B)
& in(ordered_pair(D,F),A) ) ) )
| ~ relation(C) )
| ~ relation(B) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f377,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ? [D,E] :
( ( ? [F] :
( in(ordered_pair(F,E),B)
& in(ordered_pair(D,F),A) )
| in(ordered_pair(D,E),C) )
& ( ! [F] :
( ~ in(ordered_pair(F,E),B)
| ~ in(ordered_pair(D,F),A) )
| ~ in(ordered_pair(D,E),C) ) )
| C = relation_composition(A,B) )
& ( ! [D,E] :
( ( ! [F] :
( ~ in(ordered_pair(F,E),B)
| ~ in(ordered_pair(D,F),A) )
| in(ordered_pair(D,E),C) )
& ( ? [F] :
( in(ordered_pair(F,E),B)
& in(ordered_pair(D,F),A) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_composition(A,B) ) )
| ~ relation(C) )
| ~ relation(B) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f376]) ).
fof(f378,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ? [D,E] :
( ( ? [F] :
( in(ordered_pair(F,E),B)
& in(ordered_pair(D,F),A) )
| in(ordered_pair(D,E),C) )
& ( ! [F] :
( ~ in(ordered_pair(F,E),B)
| ~ in(ordered_pair(D,F),A) )
| ~ in(ordered_pair(D,E),C) ) )
| C = relation_composition(A,B) )
& ( ( ! [D,E] :
( ! [F] :
( ~ in(ordered_pair(F,E),B)
| ~ in(ordered_pair(D,F),A) )
| in(ordered_pair(D,E),C) )
& ! [D,E] :
( ? [F] :
( in(ordered_pair(F,E),B)
& in(ordered_pair(D,F),A) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_composition(A,B) ) )
| ~ relation(C) )
| ~ relation(B) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f377]) ).
fof(f379,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ( ( ( in(ordered_pair(sK41_skl(C,B,A),sK40_skl(C,B,A)),B)
& in(ordered_pair(sK39_skl(C,B,A),sK41_skl(C,B,A)),A) )
| in(ordered_pair(sK39_skl(C,B,A),sK40_skl(C,B,A)),C) )
& ( ! [F] :
( ~ in(ordered_pair(F,sK40_skl(C,B,A)),B)
| ~ in(ordered_pair(sK39_skl(C,B,A),F),A) )
| ~ in(ordered_pair(sK39_skl(C,B,A),sK40_skl(C,B,A)),C) ) )
| C = relation_composition(A,B) )
& ( ( ! [D,E] :
( ! [F] :
( ~ in(ordered_pair(F,E),B)
| ~ in(ordered_pair(D,F),A) )
| in(ordered_pair(D,E),C) )
& ! [D,E] :
( ( in(ordered_pair(sK38_skl(E,D,C,B,A),E),B)
& in(ordered_pair(D,sK38_skl(E,D,C,B,A)),A) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_composition(A,B) ) )
| ~ relation(C) )
| ~ relation(B) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38_skl,sK39_skl,sK40_skl,sK41_skl]),skolemize(F,sK38_skl(E,D,C,B,A)),skolemize(D,sK39_skl(C,B,A)),skolemize(E,sK40_skl(C,B,A)),skolemize(F,sK41_skl(C,B,A))],[f378]) ).
fof(f384,plain,
! [X0,X1,X2] :
( in(ordered_pair(sK39_skl(X2,X1,X0),sK41_skl(X2,X1,X0)),X0)
| in(ordered_pair(sK39_skl(X2,X1,X0),sK40_skl(X2,X1,X0)),X2)
| X2 = relation_composition(X0,X1)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f379]) ).
fof(f385,plain,
! [X0,X1,X2] :
( in(ordered_pair(sK41_skl(X2,X1,X0),sK40_skl(X2,X1,X0)),X1)
| in(ordered_pair(sK39_skl(X2,X1,X0),sK40_skl(X2,X1,X0)),X2)
| X2 = relation_composition(X0,X1)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f379]) ).
fof(f404,plain,
! [A,B] :
( relation(relation_composition(A,B))
| ~ relation(B)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f53]) ).
fof(f405,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f408,plain,
! [X0] : relation(identity_relation(X0)),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f427,plain,
! [X0,X1] : ~ empty(ordered_pair(X0,X1)),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f430,plain,
! [X0] : ~ empty(singleton(X0)),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f439,plain,
relation(empty_set),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f535,plain,
! [A,B,C,D] :
( A = D
| A = C
| unordered_pair(A,B) != unordered_pair(C,D) ),
inference(pre_NNF_transformation,[status(thm)],[f109]) ).
fof(f536,plain,
! [A,D] :
( A = D
| ! [C] :
( A = C
| ! [B] : unordered_pair(A,B) != unordered_pair(C,D) ) ),
inference(miniscoping,[status(thm)],[f535]) ).
fof(f537,plain,
! [X0,X1,X2,X3] :
( X0 = X3
| X0 = X2
| unordered_pair(X0,X1) != unordered_pair(X2,X3) ),
inference(cnf_transformation,[status(thm)],[f536]) ).
fof(f670,plain,
! [A] :
( A = empty_set
| ? [B,C] : in(ordered_pair(B,C),A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f160]) ).
fof(f671,plain,
! [A] :
( A = empty_set
| in(ordered_pair(sK55_skl(A),sK56_skl(A)),A)
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55_skl,sK56_skl]),skolemize(B,sK55_skl(A)),skolemize(C,sK56_skl(A))],[f670]) ).
fof(f672,plain,
! [X0] :
( X0 = empty_set
| in(ordered_pair(sK55_skl(X0),sK56_skl(X0)),X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f671]) ).
fof(f694,plain,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f702,plain,
! [A,B,C,D] :
( ( in(ordered_pair(A,B),relation_composition(identity_relation(C),D))
<=> ( in(ordered_pair(A,B),D)
& in(A,C) ) )
| ~ relation(D) ),
inference(pre_NNF_transformation,[status(thm)],[f172]) ).
fof(f703,plain,
! [A,B,C,D] :
( ( ( ~ in(ordered_pair(A,B),D)
| ~ in(A,C)
| in(ordered_pair(A,B),relation_composition(identity_relation(C),D)) )
& ( ( in(ordered_pair(A,B),D)
& in(A,C) )
| ~ in(ordered_pair(A,B),relation_composition(identity_relation(C),D)) ) )
| ~ relation(D) ),
inference(NNF_transformation,[status(thm)],[f702]) ).
fof(f704,plain,
! [D] :
( ( ! [A,B,C] :
( ~ in(ordered_pair(A,B),D)
| ~ in(A,C)
| in(ordered_pair(A,B),relation_composition(identity_relation(C),D)) )
& ! [A,B,C] :
( ( in(ordered_pair(A,B),D)
& in(A,C) )
| ~ in(ordered_pair(A,B),relation_composition(identity_relation(C),D)) ) )
| ~ relation(D) ),
inference(miniscoping,[status(thm)],[f703]) ).
fof(f705,plain,
! [X0,X1,X2,X3] :
( in(X1,X3)
| ~ in(ordered_pair(X1,X2),relation_composition(identity_relation(X3),X0))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f704]) ).
fof(f706,plain,
! [X0,X1,X2,X3] :
( in(ordered_pair(X1,X2),X0)
| ~ in(ordered_pair(X1,X2),relation_composition(identity_relation(X3),X0))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f704]) ).
fof(f707,plain,
! [X0,X1,X2,X3] :
( ~ in(ordered_pair(X1,X2),X0)
| ~ in(X1,X3)
| in(ordered_pair(X1,X2),relation_composition(identity_relation(X3),X0))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f704]) ).
fof(f738,plain,
? [A,B] :
( relation_dom_restriction(B,A) != relation_composition(identity_relation(A),B)
& relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f184]) ).
fof(f739,plain,
? [B] :
( ? [A] : relation_dom_restriction(B,A) != relation_composition(identity_relation(A),B)
& relation(B) ),
inference(miniscoping,[status(thm)],[f738]) ).
fof(f740,plain,
( relation_dom_restriction(sK57_skl,sK58_skl) != relation_composition(identity_relation(sK58_skl),sK57_skl)
& relation(sK57_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK57_skl,sK58_skl]),skolemize(B,sK57_skl),skolemize(A,sK58_skl)],[f739]) ).
fof(f741,plain,
relation(sK57_skl),
inference(cnf_transformation,[status(thm)],[f740]) ).
fof(f742,plain,
relation_dom_restriction(sK57_skl,sK58_skl) != relation_composition(identity_relation(sK58_skl),sK57_skl),
inference(cnf_transformation,[status(thm)],[f740]) ).
fof(f761,plain,
! [X0,X1,X2] :
( in(X1,X0)
| ~ in(ordered_pair(X1,X2),identity_relation(X0))
| ~ relation(identity_relation(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f201]) ).
fof(f772,plain,
set_meet(empty_set) = empty_set,
inference(destructive_equality_resolution,[status(thm)],[f239]) ).
fof(f774,plain,
! [X0,X1] :
( X0 = X1
| ~ in(X0,singleton(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f244]) ).
fof(f776,plain,
! [X0] : ~ in(X0,empty_set),
inference(destructive_equality_resolution,[status(thm)],[f251]) ).
fof(f779,plain,
! [X0,X1,X2] :
( X0 = X2
| X0 = X1
| ~ in(X0,unordered_pair(X1,X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f278]) ).
fof(f816,plain,
! [X0,X1,X2] :
( in(X0,X2)
| ~ in(ordered_pair(X0,X1),identity_relation(X2)) ),
inference(backward_subsumption_resolution,[status(thm)],[f761,f408]) ).
fof(f841,plain,
! [X0,X1] :
( ~ in(X0,ordered_pair(sK0_skl(X1,X0),sK1_skl(X1,X0)))
| sK0_skl(X1,X0) = sK1_skl(X1,X0)
| X0 = identity_relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f206,f189]) ).
fof(f845,plain,
! [X0,X1,X2] :
( ~ in(X1,ordered_pair(sK2_skl(X2,X1,X0),sK3_skl(X2,X1,X0)))
| in(ordered_pair(sK2_skl(X2,X1,X0),sK3_skl(X2,X1,X0)),X0)
| X1 = relation_dom_restriction(X0,X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f221,f189]) ).
fof(f851,plain,
! [X0] :
( relation_dom_restriction(sK57_skl,sK58_skl) = X0
| ~ in(relation_dom_restriction(sK57_skl,sK58_skl),unordered_pair(relation_composition(identity_relation(sK58_skl),sK57_skl),X0)) ),
inference(resolution,[status(thm)],[f779,f742]) ).
fof(f852,plain,
! [X0] :
( relation_composition(identity_relation(sK58_skl),sK57_skl) = X0
| ~ in(relation_composition(identity_relation(sK58_skl),sK57_skl),unordered_pair(relation_dom_restriction(sK57_skl,sK58_skl),X0)) ),
inference(resolution,[status(thm)],[f779,f742]) ).
fof(f887,plain,
! [X0,X1] :
( relation_dom_restriction(sK57_skl,sK58_skl) = X1
| unordered_pair(relation_dom_restriction(sK57_skl,sK58_skl),X0) != unordered_pair(relation_composition(identity_relation(sK58_skl),sK57_skl),X1) ),
inference(resolution,[status(thm)],[f537,f742]) ).
fof(f888,plain,
! [X0,X1] :
( relation_composition(identity_relation(sK58_skl),sK57_skl) = X1
| unordered_pair(relation_composition(identity_relation(sK58_skl),sK57_skl),X0) != unordered_pair(relation_dom_restriction(sK57_skl,sK58_skl),X1) ),
inference(resolution,[status(thm)],[f537,f742]) ).
fof(f916,plain,
! [X0,X1] :
( ~ in(X0,ordered_pair(sK13_skl(X1,X0),sK14_skl(X1,X0)))
| in(ordered_pair(sK13_skl(X1,X0),sK14_skl(X1,X0)),X1)
| X0 = X1
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f267,f189]) ).
fof(f938,plain,
~ in(relation_dom_restriction(sK57_skl,sK58_skl),unordered_pair(relation_composition(identity_relation(sK58_skl),sK57_skl),relation_composition(identity_relation(sK58_skl),sK57_skl))),
inference(resolution,[status(thm)],[f851,f742]) ).
fof(f939,plain,
~ in(relation_dom_restriction(sK57_skl,sK58_skl),singleton(relation_composition(identity_relation(sK58_skl),sK57_skl))),
inference(forward_demodulation,[status(thm)],[f694,f938]) ).
fof(f940,plain,
~ in(relation_composition(identity_relation(sK58_skl),sK57_skl),unordered_pair(relation_dom_restriction(sK57_skl,sK58_skl),relation_dom_restriction(sK57_skl,sK58_skl))),
inference(resolution,[status(thm)],[f852,f742]) ).
fof(f941,plain,
~ in(relation_composition(identity_relation(sK58_skl),sK57_skl),singleton(relation_dom_restriction(sK57_skl,sK58_skl))),
inference(forward_demodulation,[status(thm)],[f694,f940]) ).
fof(f962,plain,
! [X0,X1] :
( ~ in(X1,ordered_pair(sK36_skl(X1,X0),sK37_skl(X1,X0)))
| in(ordered_pair(sK37_skl(X1,X0),sK36_skl(X1,X0)),X0)
| X1 = relation_inverse(X0)
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f371,f189]) ).
fof(f964,plain,
! [X0,X1,X2] :
( ~ in(X2,ordered_pair(sK39_skl(X2,X1,X0),sK40_skl(X2,X1,X0)))
| in(ordered_pair(sK39_skl(X2,X1,X0),sK41_skl(X2,X1,X0)),X0)
| X2 = relation_composition(X0,X1)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f384,f189]) ).
fof(f966,plain,
! [X0,X1,X2] :
( ~ in(X2,ordered_pair(sK39_skl(X2,X1,X0),sK40_skl(X2,X1,X0)))
| in(ordered_pair(sK41_skl(X2,X1,X0),sK40_skl(X2,X1,X0)),X1)
| X2 = relation_composition(X0,X1)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f385,f189]) ).
fof(f1024,plain,
! [X0] : unordered_pair(relation_dom_restriction(sK57_skl,sK58_skl),X0) != unordered_pair(relation_composition(identity_relation(sK58_skl),sK57_skl),relation_composition(identity_relation(sK58_skl),sK57_skl)),
inference(resolution,[status(thm)],[f887,f742]) ).
fof(f1025,plain,
! [X0] : unordered_pair(relation_dom_restriction(sK57_skl,sK58_skl),X0) != singleton(relation_composition(identity_relation(sK58_skl),sK57_skl)),
inference(forward_demodulation,[status(thm)],[f694,f1024]) ).
fof(f1026,plain,
! [X0] : unordered_pair(relation_composition(identity_relation(sK58_skl),sK57_skl),X0) != unordered_pair(relation_dom_restriction(sK57_skl,sK58_skl),relation_dom_restriction(sK57_skl,sK58_skl)),
inference(resolution,[status(thm)],[f888,f742]) ).
fof(f1027,plain,
! [X0] : unordered_pair(relation_composition(identity_relation(sK58_skl),sK57_skl),X0) != singleton(relation_dom_restriction(sK57_skl,sK58_skl)),
inference(forward_demodulation,[status(thm)],[f694,f1026]) ).
fof(f1032,plain,
( ~ element(relation_dom_restriction(sK57_skl,sK58_skl),singleton(relation_composition(identity_relation(sK58_skl),sK57_skl)))
| empty(singleton(relation_composition(identity_relation(sK58_skl),sK57_skl))) ),
inference(resolution,[status(thm)],[f939,f271]) ).
fof(f1033,definition,
( sQ0_spl
<=> empty(singleton(relation_composition(identity_relation(sK58_skl),sK57_skl))) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f1034,plain,
( ~ sQ0_spl
| empty(singleton(relation_composition(identity_relation(sK58_skl),sK57_skl))) ),
inference(component_clause,[status(thm)],[f1033]) ).
fof(f1036,definition,
( sQ1_spl
<=> element(relation_dom_restriction(sK57_skl,sK58_skl),singleton(relation_composition(identity_relation(sK58_skl),sK57_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f1039,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1032,f1033,f1036]) ).
fof(f1040,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1034,f430]) ).
fof(f1041,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f1040]) ).
fof(f1046,plain,
( ~ element(relation_composition(identity_relation(sK58_skl),sK57_skl),singleton(relation_dom_restriction(sK57_skl,sK58_skl)))
| empty(singleton(relation_dom_restriction(sK57_skl,sK58_skl))) ),
inference(resolution,[status(thm)],[f941,f271]) ).
fof(f1047,definition,
( sQ2_spl
<=> empty(singleton(relation_dom_restriction(sK57_skl,sK58_skl))) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f1048,plain,
( ~ sQ2_spl
| empty(singleton(relation_dom_restriction(sK57_skl,sK58_skl))) ),
inference(component_clause,[status(thm)],[f1047]) ).
fof(f1050,definition,
( sQ3_spl
<=> element(relation_composition(identity_relation(sK58_skl),sK57_skl),singleton(relation_dom_restriction(sK57_skl,sK58_skl))) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f1053,plain,
( ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1046,f1047,f1050]) ).
fof(f1054,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1048,f430]) ).
fof(f1055,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f1054]) ).
fof(f1061,plain,
! [X0] : unordered_pair(X0,relation_dom_restriction(sK57_skl,sK58_skl)) != singleton(relation_composition(identity_relation(sK58_skl),sK57_skl)),
inference(paramodulation,[status(thm)],[f194,f1025]) ).
fof(f1068,plain,
! [X0] : unordered_pair(X0,relation_composition(identity_relation(sK58_skl),sK57_skl)) != singleton(relation_dom_restriction(sK57_skl,sK58_skl)),
inference(paramodulation,[status(thm)],[f194,f1027]) ).
fof(f1099,plain,
( ~ in(ordered_pair(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK3_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl)),sK57_skl)
| ~ in(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK58_skl)
| ~ in(ordered_pair(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK3_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl)),relation_composition(identity_relation(sK58_skl),sK57_skl))
| ~ relation(relation_composition(identity_relation(sK58_skl),sK57_skl))
| ~ relation(sK57_skl) ),
inference(resolution,[status(thm)],[f219,f742]) ).
fof(f1100,definition,
( sQ6_spl
<=> relation(sK57_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1102,plain,
( sQ6_spl
| ~ relation(sK57_skl) ),
inference(component_clause,[status(thm)],[f1100]) ).
fof(f1103,definition,
( sQ7_spl
<=> relation(relation_composition(identity_relation(sK58_skl),sK57_skl)) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f1105,plain,
( sQ7_spl
| ~ relation(relation_composition(identity_relation(sK58_skl),sK57_skl)) ),
inference(component_clause,[status(thm)],[f1103]) ).
fof(f1106,definition,
( sQ8_spl
<=> in(ordered_pair(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK3_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl)),relation_composition(identity_relation(sK58_skl),sK57_skl)) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f1107,plain,
( ~ sQ8_spl
| in(ordered_pair(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK3_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl)),relation_composition(identity_relation(sK58_skl),sK57_skl)) ),
inference(component_clause,[status(thm)],[f1106]) ).
fof(f1108,plain,
( sQ8_spl
| ~ in(ordered_pair(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK3_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl)),relation_composition(identity_relation(sK58_skl),sK57_skl)) ),
inference(component_clause,[status(thm)],[f1106]) ).
fof(f1109,definition,
( sQ9_spl
<=> in(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK58_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f1110,plain,
( ~ sQ9_spl
| in(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK58_skl) ),
inference(component_clause,[status(thm)],[f1109]) ).
fof(f1111,plain,
( sQ9_spl
| ~ in(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK58_skl) ),
inference(component_clause,[status(thm)],[f1109]) ).
fof(f1112,definition,
( sQ10_spl
<=> in(ordered_pair(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK3_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl)),sK57_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f1114,plain,
( sQ10_spl
| ~ in(ordered_pair(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK3_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl)),sK57_skl) ),
inference(component_clause,[status(thm)],[f1112]) ).
fof(f1115,plain,
( ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1099,f1100,f1103,f1106,f1109,f1112]) ).
fof(f1154,definition,
( sQ11_spl
<=> relation_composition(identity_relation(sK58_skl),sK57_skl) = relation_dom_restriction(sK57_skl,sK58_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f1155,plain,
( ~ sQ11_spl
| relation_composition(identity_relation(sK58_skl),sK57_skl) = relation_dom_restriction(sK57_skl,sK58_skl) ),
inference(component_clause,[status(thm)],[f1154]) ).
fof(f1168,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1102,f741]) ).
fof(f1169,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f1168]) ).
fof(f1172,plain,
( sQ7_spl
| ~ relation(sK57_skl)
| ~ relation(identity_relation(sK58_skl)) ),
inference(resolution,[status(thm)],[f1105,f405]) ).
fof(f1178,definition,
( sQ16_spl
<=> relation(identity_relation(sK58_skl)) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f1180,plain,
( sQ16_spl
| ~ relation(identity_relation(sK58_skl)) ),
inference(component_clause,[status(thm)],[f1178]) ).
fof(f1182,plain,
( sQ7_spl
| ~ sQ6_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f1172,f1178,f1100,f1103]) ).
fof(f1183,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1180,f408]) ).
fof(f1184,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f1183]) ).
fof(f1185,plain,
( ~ sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1155,f742]) ).
fof(f1186,plain,
~ sQ11_spl,
inference(contradiction_clause,[status(thm)],[f1185]) ).
fof(f1218,plain,
( sQ8_spl
| in(ordered_pair(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK3_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl)),sK57_skl)
| relation_composition(identity_relation(sK58_skl),sK57_skl) = relation_dom_restriction(sK57_skl,sK58_skl)
| ~ relation(relation_composition(identity_relation(sK58_skl),sK57_skl))
| ~ relation(sK57_skl) ),
inference(resolution,[status(thm)],[f1108,f221]) ).
fof(f1225,plain,
( sQ8_spl
| sQ10_spl
| sQ11_spl
| ~ sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1218,f1100,f1103,f1154,f1112,f1106]) ).
fof(f1236,plain,
( ~ sQ9_spl
| ~ in(sK58_skl,sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl)) ),
inference(resolution,[status(thm)],[f1110,f189]) ).
fof(f1328,definition,
( sQ25_spl
<=> empty(ordered_pair(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK3_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl))) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f1329,plain,
( ~ sQ25_spl
| empty(ordered_pair(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK3_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl))) ),
inference(component_clause,[status(thm)],[f1328]) ).
fof(f1352,plain,
( ~ sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1329,f427]) ).
fof(f1353,plain,
~ sQ25_spl,
inference(contradiction_clause,[status(thm)],[f1352]) ).
fof(f1400,plain,
! [X0,X1] :
( ~ in(X1,ordered_pair(sK39_skl(X1,empty_set,X0),sK40_skl(X1,empty_set,X0)))
| X1 = relation_composition(X0,empty_set)
| ~ relation(X1)
| ~ relation(empty_set)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f776,f966]) ).
fof(f1401,plain,
! [X0] :
( ~ in(X0,ordered_pair(sK36_skl(X0,empty_set),sK37_skl(X0,empty_set)))
| X0 = relation_inverse(empty_set)
| ~ relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f776,f962]) ).
fof(f1402,plain,
! [X0,X1] :
( ~ in(X1,ordered_pair(sK39_skl(X1,X0,empty_set),sK40_skl(X1,X0,empty_set)))
| X1 = relation_composition(empty_set,X0)
| ~ relation(X1)
| ~ relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f776,f964]) ).
fof(f1403,plain,
! [X0,X1] :
( in(ordered_pair(sK41_skl(empty_set,X1,X0),sK40_skl(empty_set,X1,X0)),X1)
| empty_set = relation_composition(X0,X1)
| ~ relation(empty_set)
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f776,f385]) ).
fof(f1404,plain,
! [X0,X1] :
( in(ordered_pair(sK39_skl(empty_set,X1,X0),sK41_skl(empty_set,X1,X0)),X0)
| empty_set = relation_composition(X0,X1)
| ~ relation(empty_set)
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f776,f384]) ).
fof(f1405,plain,
! [X0] :
( in(ordered_pair(sK37_skl(empty_set,X0),sK36_skl(empty_set,X0)),X0)
| empty_set = relation_inverse(X0)
| ~ relation(empty_set)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f776,f371]) ).
fof(f1406,plain,
! [X0] :
( in(sK34_skl(X0,empty_set),X0)
| X0 = relation_rng(empty_set)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f776,f358]) ).
fof(f1407,plain,
! [X0] :
( in(sK27_skl(X0,empty_set),X0)
| X0 = relation_dom(empty_set)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f776,f331]) ).
fof(f1408,plain,
! [X0] :
( subset(empty_set,X0)
| ~ relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f776,f306]) ).
fof(f1409,plain,
! [X0] :
( ~ in(X0,ordered_pair(sK13_skl(empty_set,X0),sK14_skl(empty_set,X0)))
| X0 = empty_set
| ~ relation(empty_set)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f776,f916]) ).
fof(f1410,plain,
! [X0] :
( in(ordered_pair(sK13_skl(X0,empty_set),sK14_skl(X0,empty_set)),X0)
| empty_set = X0
| ~ relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f776,f267]) ).
fof(f1411,plain,
( empty_set = empty_set
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f776,f672]) ).
fof(f1412,plain,
! [X0,X1] :
( ~ in(X0,ordered_pair(sK2_skl(X1,X0,empty_set),sK3_skl(X1,X0,empty_set)))
| X0 = relation_dom_restriction(empty_set,X1)
| ~ relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f776,f845]) ).
fof(f1413,plain,
! [X0,X1] :
( in(ordered_pair(sK2_skl(X1,empty_set,X0),sK3_skl(X1,empty_set,X0)),X0)
| empty_set = relation_dom_restriction(X0,X1)
| ~ relation(empty_set)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f776,f221]) ).
fof(f1414,plain,
! [X0,X1] :
( in(sK2_skl(X1,empty_set,X0),X1)
| empty_set = relation_dom_restriction(X0,X1)
| ~ relation(empty_set)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f776,f220]) ).
fof(f1415,plain,
! [X0] :
( sK0_skl(X0,empty_set) = sK1_skl(X0,empty_set)
| empty_set = identity_relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f776,f206]) ).
fof(f1416,plain,
! [X0] :
( in(sK0_skl(X0,empty_set),X0)
| empty_set = identity_relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f776,f205]) ).
fof(f1433,definition,
( sQ28_spl
<=> empty_set = empty_set ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f1440,definition,
! [X0] :
( sQ30_spl
<=> in(X0,set_meet(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f1441,plain,
! [X0] :
( ~ sQ30_spl
| in(X0,set_meet(empty_set)) ),
inference(component_clause,[status(thm)],[f1440]) ).
fof(f1446,definition,
! [X0,X1] :
( sQ31_spl
<=> ( ~ in(X1,ordered_pair(sK39_skl(X1,empty_set,X0),sK40_skl(X1,empty_set,X0)))
| X1 = relation_composition(X0,empty_set)
| ~ relation(X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f1449,definition,
( sQ32_spl
<=> relation(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f1451,plain,
( sQ32_spl
| ~ relation(empty_set) ),
inference(component_clause,[status(thm)],[f1449]) ).
fof(f1452,plain,
( ~ sQ32_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f1400,f1446,f1449]) ).
fof(f1453,definition,
! [X0] :
( sQ33_spl
<=> ( ~ in(X0,ordered_pair(sK36_skl(X0,empty_set),sK37_skl(X0,empty_set)))
| X0 = relation_inverse(empty_set)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f1456,plain,
( sQ33_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1401,f1449,f1453]) ).
fof(f1457,definition,
! [X0,X1] :
( sQ34_spl
<=> ( ~ in(X1,ordered_pair(sK39_skl(X1,X0,empty_set),sK40_skl(X1,X0,empty_set)))
| X1 = relation_composition(empty_set,X0)
| ~ relation(X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f1460,plain,
( sQ34_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1402,f1449,f1457]) ).
fof(f1461,definition,
! [X0,X1] :
( sQ35_spl
<=> ( in(ordered_pair(sK41_skl(empty_set,X1,X0),sK40_skl(empty_set,X1,X0)),X1)
| empty_set = relation_composition(X0,X1)
| ~ relation(X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f1462,plain,
! [X0,X1] :
( ~ sQ35_spl
| in(ordered_pair(sK41_skl(empty_set,X1,X0),sK40_skl(empty_set,X1,X0)),X1)
| empty_set = relation_composition(X0,X1)
| ~ relation(X1)
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f1461]) ).
fof(f1464,plain,
( ~ sQ32_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f1403,f1461,f1449]) ).
fof(f1465,definition,
! [X0,X1] :
( sQ36_spl
<=> ( in(ordered_pair(sK39_skl(empty_set,X1,X0),sK41_skl(empty_set,X1,X0)),X0)
| empty_set = relation_composition(X0,X1)
| ~ relation(X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f1466,plain,
! [X0,X1] :
( ~ sQ36_spl
| in(ordered_pair(sK39_skl(empty_set,X1,X0),sK41_skl(empty_set,X1,X0)),X0)
| empty_set = relation_composition(X0,X1)
| ~ relation(X1)
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f1465]) ).
fof(f1468,plain,
( ~ sQ32_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f1404,f1465,f1449]) ).
fof(f1469,definition,
! [X0] :
( sQ37_spl
<=> ( in(ordered_pair(sK37_skl(empty_set,X0),sK36_skl(empty_set,X0)),X0)
| empty_set = relation_inverse(X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f1470,plain,
! [X0] :
( ~ sQ37_spl
| in(ordered_pair(sK37_skl(empty_set,X0),sK36_skl(empty_set,X0)),X0)
| empty_set = relation_inverse(X0)
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f1469]) ).
fof(f1472,plain,
( ~ sQ32_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f1405,f1469,f1449]) ).
fof(f1473,definition,
! [X0] :
( sQ38_spl
<=> ( in(sK34_skl(X0,empty_set),X0)
| X0 = relation_rng(empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f1476,plain,
( sQ38_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1406,f1449,f1473]) ).
fof(f1477,definition,
! [X0] :
( sQ39_spl
<=> ( in(sK27_skl(X0,empty_set),X0)
| X0 = relation_dom(empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f1480,plain,
( sQ39_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1407,f1449,f1477]) ).
fof(f1481,definition,
! [X0] :
( sQ40_spl
<=> ( subset(empty_set,X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f1484,plain,
( sQ40_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1408,f1449,f1481]) ).
fof(f1485,definition,
! [X0] :
( sQ41_spl
<=> ( ~ in(X0,ordered_pair(sK13_skl(empty_set,X0),sK14_skl(empty_set,X0)))
| X0 = empty_set
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f1488,plain,
( ~ sQ32_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f1409,f1485,f1449]) ).
fof(f1489,definition,
! [X0] :
( sQ42_spl
<=> ( in(ordered_pair(sK13_skl(X0,empty_set),sK14_skl(X0,empty_set)),X0)
| empty_set = X0
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f1492,plain,
( sQ42_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1410,f1449,f1489]) ).
fof(f1493,plain,
( sQ28_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1411,f1449,f1433]) ).
fof(f1494,definition,
! [X0,X1] :
( sQ43_spl
<=> ( ~ in(X0,ordered_pair(sK2_skl(X1,X0,empty_set),sK3_skl(X1,X0,empty_set)))
| X0 = relation_dom_restriction(empty_set,X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1497,plain,
( sQ43_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1412,f1449,f1494]) ).
fof(f1498,definition,
! [X0,X1] :
( sQ44_spl
<=> ( in(ordered_pair(sK2_skl(X1,empty_set,X0),sK3_skl(X1,empty_set,X0)),X0)
| empty_set = relation_dom_restriction(X0,X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1499,plain,
! [X0,X1] :
( ~ sQ44_spl
| in(ordered_pair(sK2_skl(X1,empty_set,X0),sK3_skl(X1,empty_set,X0)),X0)
| empty_set = relation_dom_restriction(X0,X1)
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f1498]) ).
fof(f1501,plain,
( ~ sQ32_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f1413,f1498,f1449]) ).
fof(f1502,definition,
! [X0,X1] :
( sQ45_spl
<=> ( in(sK2_skl(X1,empty_set,X0),X1)
| empty_set = relation_dom_restriction(X0,X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f1505,plain,
( ~ sQ32_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f1414,f1502,f1449]) ).
fof(f1506,definition,
! [X0] :
( sQ46_spl
<=> ( sK0_skl(X0,empty_set) = sK1_skl(X0,empty_set)
| empty_set = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f1507,plain,
! [X0] :
( ~ sQ46_spl
| sK0_skl(X0,empty_set) = sK1_skl(X0,empty_set)
| empty_set = identity_relation(X0) ),
inference(component_clause,[status(thm)],[f1506]) ).
fof(f1509,plain,
( sQ46_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1415,f1449,f1506]) ).
fof(f1510,definition,
! [X0] :
( sQ47_spl
<=> ( in(sK0_skl(X0,empty_set),X0)
| empty_set = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f1513,plain,
( sQ47_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1416,f1449,f1510]) ).
fof(f1522,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1451,f439]) ).
fof(f1523,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f1522]) ).
fof(f1526,plain,
! [X0] :
( ~ sQ30_spl
| in(X0,empty_set) ),
inference(forward_demodulation,[status(thm)],[f772,f1441]) ).
fof(f1527,plain,
( ~ sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1526,f776]) ).
fof(f1528,plain,
~ sQ30_spl,
inference(contradiction_clause,[status(thm)],[f1527]) ).
fof(f1601,plain,
! [X0] :
( ~ sQ46_spl
| empty_set = identity_relation(X0)
| ~ in(empty_set,ordered_pair(sK0_skl(X0,empty_set),sK1_skl(X0,empty_set)))
| sK0_skl(X0,empty_set) = sK0_skl(X0,empty_set)
| empty_set = identity_relation(X0)
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f1507,f841]) ).
fof(f1602,plain,
! [X0] :
( ~ sQ46_spl
| empty_set = identity_relation(X0)
| sK0_skl(X0,empty_set) = sK1_skl(X0,empty_set)
| in(ordered_pair(sK0_skl(X0,empty_set),sK0_skl(X0,empty_set)),empty_set)
| empty_set = identity_relation(X0)
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f1507,f206]) ).
fof(f1603,plain,
! [X0] :
( ~ sQ46_spl
| empty_set = identity_relation(X0)
| in(sK0_skl(X0,empty_set),X0)
| in(ordered_pair(sK0_skl(X0,empty_set),sK0_skl(X0,empty_set)),empty_set)
| empty_set = identity_relation(X0)
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f1507,f205]) ).
fof(f1604,definition,
! [X0] :
( sQ57_spl
<=> ( empty_set = identity_relation(X0)
| ~ in(empty_set,ordered_pair(sK0_skl(X0,empty_set),sK1_skl(X0,empty_set)))
| sK0_skl(X0,empty_set) = sK0_skl(X0,empty_set)
| empty_set = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1607,plain,
( ~ sQ46_spl
| sQ57_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1601,f1449,f1604,f1506]) ).
fof(f1608,definition,
! [X0] :
( sQ58_spl
<=> ( empty_set = identity_relation(X0)
| sK0_skl(X0,empty_set) = sK1_skl(X0,empty_set)
| in(ordered_pair(sK0_skl(X0,empty_set),sK0_skl(X0,empty_set)),empty_set)
| empty_set = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1611,plain,
( ~ sQ46_spl
| sQ58_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1602,f1449,f1608,f1506]) ).
fof(f1612,definition,
! [X0] :
( sQ59_spl
<=> ( empty_set = identity_relation(X0)
| in(sK0_skl(X0,empty_set),X0)
| in(ordered_pair(sK0_skl(X0,empty_set),sK0_skl(X0,empty_set)),empty_set)
| empty_set = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1615,plain,
( ~ sQ46_spl
| sQ59_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1603,f1449,f1612,f1506]) ).
fof(f1657,plain,
! [X0] :
( ~ sQ44_spl
| empty_set = relation_dom_restriction(empty_set,X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f1499,f776]) ).
fof(f1660,definition,
! [X0] :
( sQ62_spl
<=> empty_set = relation_dom_restriction(empty_set,X0) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1663,plain,
( ~ sQ44_spl
| sQ62_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1657,f1449,f1660,f1498]) ).
fof(f1669,plain,
( ~ sQ37_spl
| empty_set = relation_inverse(empty_set)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f1470,f776]) ).
fof(f1672,definition,
( sQ63_spl
<=> empty_set = relation_inverse(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1675,plain,
( ~ sQ37_spl
| sQ63_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1669,f1449,f1672,f1469]) ).
fof(f1677,plain,
! [X0] :
( ~ sQ36_spl
| empty_set = relation_composition(empty_set,X0)
| ~ relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f1466,f776]) ).
fof(f1680,definition,
! [X0] :
( sQ64_spl
<=> ( empty_set = relation_composition(empty_set,X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1683,plain,
( ~ sQ36_spl
| sQ64_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1677,f1449,f1680,f1465]) ).
fof(f1684,plain,
! [X0] :
( ~ sQ35_spl
| empty_set = relation_composition(X0,empty_set)
| ~ relation(empty_set)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f1462,f776]) ).
fof(f1687,definition,
! [X0] :
( sQ65_spl
<=> ( empty_set = relation_composition(X0,empty_set)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1690,plain,
( ~ sQ35_spl
| ~ sQ32_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f1684,f1687,f1449,f1461]) ).
fof(f1791,plain,
! [X0] : ~ in(ordered_pair(relation_composition(identity_relation(sK58_skl),sK57_skl),X0),identity_relation(singleton(relation_dom_restriction(sK57_skl,sK58_skl)))),
inference(resolution,[status(thm)],[f816,f941]) ).
fof(f1793,plain,
! [X0] : ~ in(ordered_pair(relation_dom_restriction(sK57_skl,sK58_skl),X0),identity_relation(singleton(relation_composition(identity_relation(sK58_skl),sK57_skl)))),
inference(resolution,[status(thm)],[f816,f939]) ).
fof(f1800,plain,
! [X0,X1] :
( sQ9_spl
| ~ in(ordered_pair(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),X1),relation_composition(identity_relation(sK58_skl),X0))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f705,f1111]) ).
fof(f1825,plain,
! [X0] : ~ in(unordered_pair(relation_composition(identity_relation(sK58_skl),sK57_skl),X0),singleton(singleton(relation_dom_restriction(sK57_skl,sK58_skl)))),
inference(resolution,[status(thm)],[f774,f1027]) ).
fof(f1826,plain,
! [X0] : ~ in(unordered_pair(relation_dom_restriction(sK57_skl,sK58_skl),X0),singleton(singleton(relation_composition(identity_relation(sK58_skl),sK57_skl)))),
inference(resolution,[status(thm)],[f774,f1025]) ).
fof(f1827,plain,
! [X0] : ~ in(unordered_pair(X0,relation_composition(identity_relation(sK58_skl),sK57_skl)),singleton(singleton(relation_dom_restriction(sK57_skl,sK58_skl)))),
inference(resolution,[status(thm)],[f774,f1068]) ).
fof(f1828,plain,
! [X0] : ~ in(unordered_pair(X0,relation_dom_restriction(sK57_skl,sK58_skl)),singleton(singleton(relation_composition(identity_relation(sK58_skl),sK57_skl)))),
inference(resolution,[status(thm)],[f774,f1061]) ).
fof(f1883,plain,
( sQ9_spl
| in(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK58_skl)
| relation_composition(identity_relation(sK58_skl),sK57_skl) = relation_dom_restriction(sK57_skl,sK58_skl)
| ~ relation(relation_composition(identity_relation(sK58_skl),sK57_skl))
| ~ relation(sK57_skl)
| ~ relation(sK57_skl) ),
inference(resolution,[status(thm)],[f1800,f220]) ).
fof(f1893,plain,
( sQ9_spl
| sQ11_spl
| ~ sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1883,f1100,f1103,f1154,f1109]) ).
fof(f1897,plain,
! [X0] :
( ~ sQ9_spl
| ~ in(ordered_pair(sK58_skl,X0),identity_relation(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl))) ),
inference(resolution,[status(thm)],[f1236,f816]) ).
fof(f1942,plain,
! [X0] :
( ~ element(unordered_pair(relation_composition(identity_relation(sK58_skl),sK57_skl),X0),singleton(singleton(relation_dom_restriction(sK57_skl,sK58_skl))))
| empty(singleton(singleton(relation_dom_restriction(sK57_skl,sK58_skl)))) ),
inference(resolution,[status(thm)],[f1825,f271]) ).
fof(f1945,definition,
( sQ73_spl
<=> empty(singleton(singleton(relation_dom_restriction(sK57_skl,sK58_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1946,plain,
( ~ sQ73_spl
| empty(singleton(singleton(relation_dom_restriction(sK57_skl,sK58_skl)))) ),
inference(component_clause,[status(thm)],[f1945]) ).
fof(f1948,definition,
! [X0] :
( sQ74_spl
<=> ~ element(unordered_pair(relation_composition(identity_relation(sK58_skl),sK57_skl),X0),singleton(singleton(relation_dom_restriction(sK57_skl,sK58_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1951,plain,
( sQ74_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f1942,f1945,f1948]) ).
fof(f1952,plain,
( ~ sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1946,f430]) ).
fof(f1953,plain,
~ sQ73_spl,
inference(contradiction_clause,[status(thm)],[f1952]) ).
fof(f1960,plain,
! [X0] :
( ~ element(unordered_pair(relation_dom_restriction(sK57_skl,sK58_skl),X0),singleton(singleton(relation_composition(identity_relation(sK58_skl),sK57_skl))))
| empty(singleton(singleton(relation_composition(identity_relation(sK58_skl),sK57_skl)))) ),
inference(resolution,[status(thm)],[f1826,f271]) ).
fof(f1963,definition,
( sQ75_spl
<=> empty(singleton(singleton(relation_composition(identity_relation(sK58_skl),sK57_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1964,plain,
( ~ sQ75_spl
| empty(singleton(singleton(relation_composition(identity_relation(sK58_skl),sK57_skl)))) ),
inference(component_clause,[status(thm)],[f1963]) ).
fof(f1966,definition,
! [X0] :
( sQ76_spl
<=> ~ element(unordered_pair(relation_dom_restriction(sK57_skl,sK58_skl),X0),singleton(singleton(relation_composition(identity_relation(sK58_skl),sK57_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1969,plain,
( sQ76_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f1960,f1963,f1966]) ).
fof(f1970,plain,
( ~ sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1964,f430]) ).
fof(f1971,plain,
~ sQ75_spl,
inference(contradiction_clause,[status(thm)],[f1970]) ).
fof(f2019,plain,
! [X0] :
( ~ element(unordered_pair(X0,relation_composition(identity_relation(sK58_skl),sK57_skl)),singleton(singleton(relation_dom_restriction(sK57_skl,sK58_skl))))
| empty(singleton(singleton(relation_dom_restriction(sK57_skl,sK58_skl)))) ),
inference(resolution,[status(thm)],[f1827,f271]) ).
fof(f2022,definition,
! [X0] :
( sQ77_spl
<=> ~ element(unordered_pair(X0,relation_composition(identity_relation(sK58_skl),sK57_skl)),singleton(singleton(relation_dom_restriction(sK57_skl,sK58_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f2025,plain,
( sQ77_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f2019,f1945,f2022]) ).
fof(f2032,plain,
! [X0] :
( ~ element(unordered_pair(X0,relation_dom_restriction(sK57_skl,sK58_skl)),singleton(singleton(relation_composition(identity_relation(sK58_skl),sK57_skl))))
| empty(singleton(singleton(relation_composition(identity_relation(sK58_skl),sK57_skl)))) ),
inference(resolution,[status(thm)],[f1828,f271]) ).
fof(f2035,definition,
! [X0] :
( sQ78_spl
<=> ~ element(unordered_pair(X0,relation_dom_restriction(sK57_skl,sK58_skl)),singleton(singleton(relation_composition(identity_relation(sK58_skl),sK57_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f2038,plain,
( sQ78_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f2032,f1963,f2035]) ).
fof(f2194,plain,
! [X0,X1] :
( ~ sQ9_spl
| ~ in(ordered_pair(sK58_skl,X0),relation_composition(identity_relation(X1),identity_relation(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl))))
| ~ relation(identity_relation(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl))) ),
inference(resolution,[status(thm)],[f706,f1897]) ).
fof(f2195,plain,
! [X0] :
( sQ10_spl
| ~ in(ordered_pair(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK3_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl)),relation_composition(identity_relation(X0),sK57_skl))
| ~ relation(sK57_skl) ),
inference(resolution,[status(thm)],[f706,f1114]) ).
fof(f2209,plain,
! [X0,X1] :
( ~ in(ordered_pair(relation_composition(identity_relation(sK58_skl),sK57_skl),X0),relation_composition(identity_relation(X1),identity_relation(singleton(relation_dom_restriction(sK57_skl,sK58_skl)))))
| ~ relation(identity_relation(singleton(relation_dom_restriction(sK57_skl,sK58_skl)))) ),
inference(resolution,[status(thm)],[f706,f1791]) ).
fof(f2211,plain,
! [X0,X1] :
( ~ in(ordered_pair(relation_dom_restriction(sK57_skl,sK58_skl),X0),relation_composition(identity_relation(X1),identity_relation(singleton(relation_composition(identity_relation(sK58_skl),sK57_skl)))))
| ~ relation(identity_relation(singleton(relation_composition(identity_relation(sK58_skl),sK57_skl)))) ),
inference(resolution,[status(thm)],[f706,f1793]) ).
fof(f2213,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X0,X1),relation_composition(identity_relation(X2),empty_set))
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f706,f776]) ).
fof(f2219,definition,
( sQ83_spl
<=> relation(identity_relation(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl))) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f2221,plain,
( sQ83_spl
| ~ relation(identity_relation(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl))) ),
inference(component_clause,[status(thm)],[f2219]) ).
fof(f2222,definition,
! [X0,X1] :
( sQ84_spl
<=> ~ in(ordered_pair(sK58_skl,X0),relation_composition(identity_relation(X1),identity_relation(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f2225,plain,
( ~ sQ9_spl
| sQ84_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f2194,f2219,f2222,f1109]) ).
fof(f2226,definition,
! [X0] :
( sQ85_spl
<=> ~ in(ordered_pair(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK3_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl)),relation_composition(identity_relation(X0),sK57_skl)) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f2227,plain,
! [X0] :
( ~ sQ85_spl
| ~ in(ordered_pair(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK3_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl)),relation_composition(identity_relation(X0),sK57_skl)) ),
inference(component_clause,[status(thm)],[f2226]) ).
fof(f2229,plain,
( sQ10_spl
| sQ85_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2195,f1100,f2226,f1112]) ).
fof(f2230,definition,
( sQ86_spl
<=> relation(identity_relation(sK57_skl)) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f2232,plain,
( sQ86_spl
| ~ relation(identity_relation(sK57_skl)) ),
inference(component_clause,[status(thm)],[f2230]) ).
fof(f2246,definition,
( sQ88_spl
<=> relation(identity_relation(singleton(relation_dom_restriction(sK57_skl,sK58_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f2248,plain,
( sQ88_spl
| ~ relation(identity_relation(singleton(relation_dom_restriction(sK57_skl,sK58_skl)))) ),
inference(component_clause,[status(thm)],[f2246]) ).
fof(f2249,definition,
! [X0,X1] :
( sQ89_spl
<=> ~ in(ordered_pair(relation_composition(identity_relation(sK58_skl),sK57_skl),X0),relation_composition(identity_relation(X1),identity_relation(singleton(relation_dom_restriction(sK57_skl,sK58_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f2252,plain,
( sQ89_spl
| ~ sQ88_spl ),
inference(split_clause,[status(thm)],[f2209,f2246,f2249]) ).
fof(f2254,definition,
( sQ90_spl
<=> relation(identity_relation(singleton(relation_composition(identity_relation(sK58_skl),sK57_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f2256,plain,
( sQ90_spl
| ~ relation(identity_relation(singleton(relation_composition(identity_relation(sK58_skl),sK57_skl)))) ),
inference(component_clause,[status(thm)],[f2254]) ).
fof(f2257,definition,
! [X0,X1] :
( sQ91_spl
<=> ~ in(ordered_pair(relation_dom_restriction(sK57_skl,sK58_skl),X0),relation_composition(identity_relation(X1),identity_relation(singleton(relation_composition(identity_relation(sK58_skl),sK57_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f2260,plain,
( sQ91_spl
| ~ sQ90_spl ),
inference(split_clause,[status(thm)],[f2211,f2254,f2257]) ).
fof(f2262,definition,
! [X0,X1,X2] :
( sQ92_spl
<=> ~ in(ordered_pair(X0,X1),relation_composition(identity_relation(X2),empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f2265,plain,
( sQ92_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f2213,f1449,f2262]) ).
fof(f2266,plain,
( ~ sQ8_spl
| ~ sQ85_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1107,f2227]) ).
fof(f2267,plain,
( sQ86_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2232,f408]) ).
fof(f2268,plain,
sQ86_spl,
inference(contradiction_clause,[status(thm)],[f2267]) ).
fof(f2269,plain,
( sQ83_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2221,f408]) ).
fof(f2270,plain,
sQ83_spl,
inference(contradiction_clause,[status(thm)],[f2269]) ).
fof(f2271,plain,
( sQ90_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2256,f408]) ).
fof(f2272,plain,
sQ90_spl,
inference(contradiction_clause,[status(thm)],[f2271]) ).
fof(f2273,plain,
( sQ88_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2248,f408]) ).
fof(f2274,plain,
sQ88_spl,
inference(contradiction_clause,[status(thm)],[f2273]) ).
fof(f2275,plain,
( ~ sQ8_spl
| ~ sQ85_spl ),
inference(contradiction_clause,[status(thm)],[f2266]) ).
fof(f2362,plain,
( sQ8_spl
| ~ in(ordered_pair(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK3_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl)),sK57_skl)
| ~ in(sK2_skl(sK58_skl,relation_composition(identity_relation(sK58_skl),sK57_skl),sK57_skl),sK58_skl)
| ~ relation(sK57_skl) ),
inference(resolution,[status(thm)],[f1108,f707]) ).
fof(f2373,plain,
( sQ8_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2362,f1100,f1109,f1112,f1106]) ).
fof(f2379,plain,
$false,
inference(sat_refutation,[status(thm)],[f1039,f1041,f1053,f1055,f1115,f1169,f1182,f1184,f1186,f1225,f1353,f1452,f1456,f1460,f1464,f1468,f1472,f1476,f1480,f1484,f1488,f1492,f1493,f1497,f1501,f1505,f1509,f1513,f1523,f1528,f1607,f1611,f1615,f1663,f1675,f1683,f1690,f1893,f1951,f1953,f1969,f1971,f2025,f2038,f2225,f2229,f2252,f2260,f2265,f2268,f2270,f2272,f2274,f2275,f2373]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU195+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n005.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 05:56:19 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.40 % Drodi V4.1.1
% 0.13/0.68 % Refutation found
% 0.13/0.68 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.74 % Elapsed time: 0.353367 seconds
% 0.13/0.74 % CPU time: 2.327648 seconds
% 0.13/0.74 % Total memory used: 136.434 MB
% 0.13/0.74 % Net memory used: 133.182 MB
%------------------------------------------------------------------------------