%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU210+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 : n017.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:41 PM UTC 2026
% Result : Theorem 45.36s 6.24s
% Output : CNFRefutation 41.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 5
% Syntax : Number of formulae : 56 ( 8 unt; 0 def)
% Number of atoms : 254 ( 54 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 315 ( 117 ~; 134 |; 48 &)
% ( 11 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 3 con; 0-4 aty)
% Number of variables : 170 ( 146 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f12,axiom,
! [A] :
( relation(A)
=> ! [B,C] :
( C = relation_inverse_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,A)
=> in(C,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,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(f133,conjecture,
! [A,B] :
( relation(B)
=> ~ ( relation_inverse_image(B,A) = empty_set
& subset(A,relation_rng(B))
& A != empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f134,negated_conjecture,
~ ! [A,B] :
( relation(B)
=> ~ ( relation_inverse_image(B,A) = empty_set
& subset(A,relation_rng(B))
& A != empty_set ) ),
inference(negated_conjecture,[status(cth)],[f133]) ).
fof(f263,plain,
! [A] :
( ! [B,C] :
( C = relation_inverse_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) ) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f264,plain,
! [A] :
( ! [B,C] :
( ( ? [D] :
( ( ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) )
| in(D,C) )
& ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(D,E),A) )
| ~ in(D,C) ) )
| C = relation_inverse_image(A,B) )
& ( ! [D] :
( ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(D,E),A) )
| in(D,C) )
& ( ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) )
| ~ in(D,C) ) )
| C != relation_inverse_image(A,B) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f263]) ).
fof(f265,plain,
! [A] :
( ( ! [B,C] :
( ? [D] :
( ( ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) )
| in(D,C) )
& ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(D,E),A) )
| ~ in(D,C) ) )
| C = relation_inverse_image(A,B) )
& ! [B,C] :
( ( ! [D] :
( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(D,E),A) )
| in(D,C) )
& ! [D] :
( ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) )
| ~ in(D,C) ) )
| C != relation_inverse_image(A,B) ) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f264]) ).
fof(f266,plain,
! [A] :
( ( ! [B,C] :
( ( ( ( in(sK11_skl(C,B,A),B)
& in(ordered_pair(sK10_skl(C,B,A),sK11_skl(C,B,A)),A) )
| in(sK10_skl(C,B,A),C) )
& ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(sK10_skl(C,B,A),E),A) )
| ~ in(sK10_skl(C,B,A),C) ) )
| C = relation_inverse_image(A,B) )
& ! [B,C] :
( ( ! [D] :
( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(D,E),A) )
| in(D,C) )
& ! [D] :
( ( in(sK9_skl(D,C,B,A),B)
& in(ordered_pair(D,sK9_skl(D,C,B,A)),A) )
| ~ in(D,C) ) )
| C != relation_inverse_image(A,B) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl]),skolemize(E,sK9_skl(D,C,B,A)),skolemize(D,sK10_skl(C,B,A)),skolemize(E,sK11_skl(C,B,A))],[f265]) ).
fof(f269,plain,
! [X0,X1,X2,X3,X4] :
( ~ in(X4,X2)
| ~ in(ordered_pair(X3,X4),X0)
| in(X3,X1)
| X1 != relation_inverse_image(X0,X2)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f271,plain,
! [X0,X1,X2] :
( in(ordered_pair(sK10_skl(X1,X2,X0),sK11_skl(X1,X2,X0)),X0)
| in(sK10_skl(X1,X2,X0),X1)
| X1 = relation_inverse_image(X0,X2)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f272,plain,
! [X0,X1,X2] :
( in(sK11_skl(X1,X2,X0),X2)
| in(sK10_skl(X1,X2,X0),X1)
| X1 = relation_inverse_image(X0,X2)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f299,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(NNF_transformation,[status(thm)],[f16]) ).
fof(f300,plain,
( ! [A] :
( ? [B] : in(B,A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(miniscoping,[status(thm)],[f299]) ).
fof(f301,plain,
( ! [A] :
( in(sK19_skl(A),A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl]),skolemize(B,sK19_skl(A))],[f300]) ).
fof(f302,plain,
! [X0,X1] :
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(thm)],[f301]) ).
fof(f359,plain,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,B)
| ~ in(C,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f360,plain,
! [A,B] :
( ( ? [C] :
( ~ in(C,B)
& in(C,A) )
| subset(A,B) )
& ( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f359]) ).
fof(f361,plain,
( ! [A,B] :
( ? [C] :
( ~ in(C,B)
& in(C,A) )
| subset(A,B) )
& ! [A,B] :
( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(miniscoping,[status(thm)],[f360]) ).
fof(f362,plain,
( ! [A,B] :
( ( ~ in(sK32_skl(B,A),B)
& in(sK32_skl(B,A),A) )
| subset(A,B) )
& ! [A,B] :
( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32_skl]),skolemize(C,sK32_skl(B,A))],[f361]) ).
fof(f363,plain,
! [X0,X1,X2] :
( in(X2,X1)
| ~ in(X2,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f402,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)],[f30]) ).
fof(f403,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)],[f402]) ).
fof(f404,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)],[f403]) ).
fof(f405,plain,
! [A] :
( ( ! [B] :
( ( ( in(ordered_pair(sK43_skl(B,A),sK42_skl(B,A)),A)
| in(sK42_skl(B,A),B) )
& ( ! [D] : ~ in(ordered_pair(D,sK42_skl(B,A)),A)
| ~ in(sK42_skl(B,A),B) ) )
| B = relation_rng(A) )
& ! [B] :
( ( ! [C] :
( ! [D] : ~ in(ordered_pair(D,C),A)
| in(C,B) )
& ! [C] :
( in(ordered_pair(sK41_skl(C,B,A),C),A)
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41_skl,sK42_skl,sK43_skl]),skolemize(D,sK41_skl(C,B,A)),skolemize(C,sK42_skl(B,A)),skolemize(D,sK43_skl(B,A))],[f404]) ).
fof(f406,plain,
! [X0,X1,X2] :
( in(ordered_pair(sK41_skl(X2,X1,X0),X2),X0)
| ~ in(X2,X1)
| X1 != relation_rng(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f405]) ).
fof(f657,plain,
? [A,B] :
( relation_inverse_image(B,A) = empty_set
& subset(A,relation_rng(B))
& A != empty_set
& relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f134]) ).
fof(f658,plain,
? [B] :
( ? [A] :
( relation_inverse_image(B,A) = empty_set
& subset(A,relation_rng(B))
& A != empty_set )
& relation(B) ),
inference(miniscoping,[status(thm)],[f657]) ).
fof(f659,plain,
( relation_inverse_image(sK62_skl,sK63_skl) = empty_set
& subset(sK63_skl,relation_rng(sK62_skl))
& sK63_skl != empty_set
& relation(sK62_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK62_skl,sK63_skl]),skolemize(B,sK62_skl),skolemize(A,sK63_skl)],[f658]) ).
fof(f660,plain,
relation(sK62_skl),
inference(cnf_transformation,[status(thm)],[f659]) ).
fof(f661,plain,
sK63_skl != empty_set,
inference(cnf_transformation,[status(thm)],[f659]) ).
fof(f662,plain,
subset(sK63_skl,relation_rng(sK62_skl)),
inference(cnf_transformation,[status(thm)],[f659]) ).
fof(f663,plain,
relation_inverse_image(sK62_skl,sK63_skl) = empty_set,
inference(cnf_transformation,[status(thm)],[f659]) ).
fof(f889,plain,
! [X0,X1,X2,X3] :
( ~ in(X3,X2)
| ~ in(ordered_pair(X1,X3),X0)
| in(X1,relation_inverse_image(X0,X2))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f269]) ).
fof(f897,plain,
! [X0] : ~ in(X0,empty_set),
inference(destructive_equality_resolution,[status(thm)],[f302]) ).
fof(f919,plain,
! [X0,X1] :
( in(ordered_pair(sK41_skl(X1,relation_rng(X0),X0),X1),X0)
| ~ in(X1,relation_rng(X0))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f406]) ).
fof(f946,plain,
! [X0] :
( in(X0,relation_rng(sK62_skl))
| ~ in(X0,sK63_skl) ),
inference(resolution,[status(thm)],[f363,f662]) ).
fof(f3432,plain,
! [X0,X1,X2,X3] :
( ~ in(sK11_skl(X1,X2,X0),X3)
| in(sK10_skl(X1,X2,X0),relation_inverse_image(X0,X3))
| ~ relation(X0)
| in(sK10_skl(X1,X2,X0),X1)
| X1 = relation_inverse_image(X0,X2)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f271,f889]) ).
fof(f3450,plain,
! [X0,X1,X2,X3] :
( ~ in(sK11_skl(X1,X2,X0),X3)
| in(sK10_skl(X1,X2,X0),relation_inverse_image(X0,X3))
| in(sK10_skl(X1,X2,X0),X1)
| X1 = relation_inverse_image(X0,X2)
| ~ relation(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3432]) ).
fof(f9436,plain,
! [X0,X1,X2] :
( ~ in(X1,X2)
| in(sK41_skl(X1,relation_rng(X0),X0),relation_inverse_image(X0,X2))
| ~ relation(X0)
| ~ in(X1,relation_rng(X0))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f919,f889]) ).
fof(f9478,plain,
! [X0,X1,X2] :
( ~ in(X1,X2)
| in(sK41_skl(X1,relation_rng(X0),X0),relation_inverse_image(X0,X2))
| ~ in(X1,relation_rng(X0))
| ~ relation(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f9436]) ).
fof(f14828,plain,
! [X0,X1] :
( ~ in(sK11_skl(X0,X1,sK62_skl),sK63_skl)
| in(sK10_skl(X0,X1,sK62_skl),empty_set)
| in(sK10_skl(X0,X1,sK62_skl),X0)
| X0 = relation_inverse_image(sK62_skl,X1)
| ~ relation(sK62_skl) ),
inference(paramodulation,[status(thm)],[f663,f3450]) ).
fof(f14834,plain,
! [X0,X1] :
( ~ in(sK11_skl(X0,X1,sK62_skl),sK63_skl)
| in(sK10_skl(X0,X1,sK62_skl),empty_set)
| in(sK10_skl(X0,X1,sK62_skl),X0)
| X0 = relation_inverse_image(sK62_skl,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f14828,f660]) ).
fof(f19711,plain,
! [X0,X1] :
( ~ in(sK11_skl(X0,X1,sK62_skl),sK63_skl)
| in(sK10_skl(X0,X1,sK62_skl),X0)
| X0 = relation_inverse_image(sK62_skl,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f14834,f897]) ).
fof(f19712,plain,
! [X0] :
( in(sK10_skl(X0,sK63_skl,sK62_skl),X0)
| X0 = relation_inverse_image(sK62_skl,sK63_skl)
| ~ relation(sK62_skl)
| in(sK10_skl(X0,sK63_skl,sK62_skl),X0)
| X0 = relation_inverse_image(sK62_skl,sK63_skl) ),
inference(resolution,[status(thm)],[f19711,f272]) ).
fof(f19713,plain,
! [X0] :
( in(sK10_skl(X0,sK63_skl,sK62_skl),X0)
| X0 = relation_inverse_image(sK62_skl,sK63_skl)
| ~ relation(sK62_skl)
| in(sK10_skl(X0,sK63_skl,sK62_skl),X0)
| X0 = empty_set ),
inference(forward_demodulation,[status(thm)],[f663,f19712]) ).
fof(f19714,plain,
! [X0] :
( in(sK10_skl(X0,sK63_skl,sK62_skl),X0)
| X0 = empty_set
| ~ relation(sK62_skl)
| in(sK10_skl(X0,sK63_skl,sK62_skl),X0)
| X0 = empty_set ),
inference(forward_demodulation,[status(thm)],[f663,f19713]) ).
fof(f19715,plain,
! [X0] :
( ~ relation(sK62_skl)
| in(sK10_skl(X0,sK63_skl,sK62_skl),X0)
| X0 = empty_set ),
inference(duplicate_literals_removal,[status(thm)],[f19714]) ).
fof(f19716,plain,
! [X0] :
( in(sK10_skl(X0,sK63_skl,sK62_skl),X0)
| X0 = empty_set ),
inference(forward_subsumption_resolution,[status(thm)],[f19715,f660]) ).
fof(f23988,plain,
! [X0] :
( ~ in(X0,sK63_skl)
| in(sK41_skl(X0,relation_rng(sK62_skl),sK62_skl),empty_set)
| ~ in(X0,relation_rng(sK62_skl))
| ~ relation(sK62_skl) ),
inference(paramodulation,[status(thm)],[f663,f9478]) ).
fof(f23997,plain,
! [X0] :
( ~ in(X0,sK63_skl)
| in(sK41_skl(X0,relation_rng(sK62_skl),sK62_skl),empty_set)
| ~ in(X0,relation_rng(sK62_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f23988,f660]) ).
fof(f24516,plain,
! [X0] :
( ~ in(X0,sK63_skl)
| in(sK41_skl(X0,relation_rng(sK62_skl),sK62_skl),empty_set) ),
inference(forward_subsumption_resolution,[status(thm)],[f23997,f946]) ).
fof(f24517,plain,
! [X0] : ~ in(X0,sK63_skl),
inference(resolution,[status(thm)],[f24516,f897]) ).
fof(f24527,plain,
sK63_skl = empty_set,
inference(resolution,[status(thm)],[f24517,f19716]) ).
fof(f24600,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f24527,f661]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU210+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 : n017.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:53:42 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.39 % Drodi V4.1.1
% 45.36/6.24 % Refutation found
% 45.36/6.24 % SZS status Theorem for theBenchmark: Theorem is valid
% 45.36/6.24 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.88/6.34 % Elapsed time: 5.957267 seconds
% 2.88/6.34 % CPU time: 46.584318 seconds
% 2.88/6.34 % Total memory used: 371.499 MB
% 2.88/6.34 % Net memory used: 322.835 MB
%------------------------------------------------------------------------------