%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU271+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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:58 PM UTC 2026
% Result : Theorem 0.15s 0.46s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 6
% Syntax : Number of formulae : 53 ( 11 unt; 0 def)
% Number of atoms : 249 ( 38 equ)
% Maximal formula atoms : 17 ( 4 avg)
% Number of connectives : 322 ( 126 ~; 137 |; 45 &)
% ( 9 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 1 con; 0-2 aty)
% Number of variables : 120 ( 111 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
! [A,B] :
( A = B
<=> ( subset(B,A)
& subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A] :
( relation(A)
=> ( antisymmetric(A)
<=> is_antisymmetric_in(A,relation_field(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A,B] :
( relation(B)
=> ( B = inclusion_relation(A)
<=> ( ! [C,D] :
( ( in(D,A)
& in(C,A) )
=> ( in(ordered_pair(C,D),B)
<=> subset(C,D) ) )
& relation_field(B) = A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A] :
( relation(A)
=> ! [B] :
( is_antisymmetric_in(A,B)
<=> ! [C,D] :
( ( in(ordered_pair(D,C),A)
& in(ordered_pair(C,D),A)
& in(D,B)
& in(C,B) )
=> C = D ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A] : relation(inclusion_relation(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,conjecture,
! [A] : antisymmetric(inclusion_relation(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,negated_conjecture,
~ ! [A] : antisymmetric(inclusion_relation(A)),
inference(negated_conjecture,[status(cth)],[f49]) ).
fof(f73,plain,
! [A,B] :
( ( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(NNF_transformation,[status(thm)],[f9]) ).
fof(f74,plain,
( ! [A,B] :
( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ! [A,B] :
( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(miniscoping,[status(thm)],[f73]) ).
fof(f77,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f78,plain,
! [A] :
( ( antisymmetric(A)
<=> is_antisymmetric_in(A,relation_field(A)) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f79,plain,
! [A] :
( ( ( ~ is_antisymmetric_in(A,relation_field(A))
| antisymmetric(A) )
& ( is_antisymmetric_in(A,relation_field(A))
| ~ antisymmetric(A) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f78]) ).
fof(f81,plain,
! [X0] :
( ~ is_antisymmetric_in(X0,relation_field(X0))
| antisymmetric(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f82,plain,
! [A,B] :
( ( B = inclusion_relation(A)
<=> ( ! [C,D] :
( ( in(ordered_pair(C,D),B)
<=> subset(C,D) )
| ~ in(D,A)
| ~ in(C,A) )
& relation_field(B) = A ) )
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f83,plain,
! [A,B] :
( ( ( ? [C,D] :
( ( subset(C,D)
| in(ordered_pair(C,D),B) )
& ( ~ subset(C,D)
| ~ in(ordered_pair(C,D),B) )
& in(D,A)
& in(C,A) )
| relation_field(B) != A
| B = inclusion_relation(A) )
& ( ( ! [C,D] :
( ( ( ~ subset(C,D)
| in(ordered_pair(C,D),B) )
& ( subset(C,D)
| ~ in(ordered_pair(C,D),B) ) )
| ~ in(D,A)
| ~ in(C,A) )
& relation_field(B) = A )
| B != inclusion_relation(A) ) )
| ~ relation(B) ),
inference(NNF_transformation,[status(thm)],[f82]) ).
fof(f84,plain,
! [B] :
( ( ! [A] :
( ? [C,D] :
( ( subset(C,D)
| in(ordered_pair(C,D),B) )
& ( ~ subset(C,D)
| ~ in(ordered_pair(C,D),B) )
& in(D,A)
& in(C,A) )
| relation_field(B) != A
| B = inclusion_relation(A) )
& ! [A] :
( ( ! [C,D] :
( ( ( ~ subset(C,D)
| in(ordered_pair(C,D),B) )
& ( subset(C,D)
| ~ in(ordered_pair(C,D),B) ) )
| ~ in(D,A)
| ~ in(C,A) )
& relation_field(B) = A )
| B != inclusion_relation(A) ) )
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f83]) ).
fof(f85,plain,
! [B] :
( ( ! [A] :
( ( ( subset(sK0_skl(A,B),sK1_skl(A,B))
| in(ordered_pair(sK0_skl(A,B),sK1_skl(A,B)),B) )
& ( ~ subset(sK0_skl(A,B),sK1_skl(A,B))
| ~ in(ordered_pair(sK0_skl(A,B),sK1_skl(A,B)),B) )
& in(sK1_skl(A,B),A)
& in(sK0_skl(A,B),A) )
| relation_field(B) != A
| B = inclusion_relation(A) )
& ! [A] :
( ( ! [C,D] :
( ( ( ~ subset(C,D)
| in(ordered_pair(C,D),B) )
& ( subset(C,D)
| ~ in(ordered_pair(C,D),B) ) )
| ~ in(D,A)
| ~ in(C,A) )
& relation_field(B) = A )
| B != inclusion_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))],[f84]) ).
fof(f86,plain,
! [X0,X1] :
( relation_field(X0) = X1
| X0 != inclusion_relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f87,plain,
! [X0,X1,X2,X3] :
( subset(X2,X3)
| ~ in(ordered_pair(X2,X3),X0)
| ~ in(X3,X1)
| ~ in(X2,X1)
| X0 != inclusion_relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f93,plain,
! [A] :
( ! [B] :
( is_antisymmetric_in(A,B)
<=> ! [C,D] :
( C = D
| ~ in(ordered_pair(D,C),A)
| ~ in(ordered_pair(C,D),A)
| ~ in(D,B)
| ~ in(C,B) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f94,plain,
! [A] :
( ! [B] :
( ( ? [C,D] :
( C != D
& in(ordered_pair(D,C),A)
& in(ordered_pair(C,D),A)
& in(D,B)
& in(C,B) )
| is_antisymmetric_in(A,B) )
& ( ! [C,D] :
( C = D
| ~ in(ordered_pair(D,C),A)
| ~ in(ordered_pair(C,D),A)
| ~ in(D,B)
| ~ in(C,B) )
| ~ is_antisymmetric_in(A,B) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f93]) ).
fof(f95,plain,
! [A] :
( ( ! [B] :
( ? [C,D] :
( C != D
& in(ordered_pair(D,C),A)
& in(ordered_pair(C,D),A)
& in(D,B)
& in(C,B) )
| is_antisymmetric_in(A,B) )
& ! [B] :
( ! [C,D] :
( C = D
| ~ in(ordered_pair(D,C),A)
| ~ in(ordered_pair(C,D),A)
| ~ in(D,B)
| ~ in(C,B) )
| ~ is_antisymmetric_in(A,B) ) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f94]) ).
fof(f96,plain,
! [A] :
( ( ! [B] :
( ( sK2_skl(B,A) != sK3_skl(B,A)
& in(ordered_pair(sK3_skl(B,A),sK2_skl(B,A)),A)
& in(ordered_pair(sK2_skl(B,A),sK3_skl(B,A)),A)
& in(sK3_skl(B,A),B)
& in(sK2_skl(B,A),B) )
| is_antisymmetric_in(A,B) )
& ! [B] :
( ! [C,D] :
( C = D
| ~ in(ordered_pair(D,C),A)
| ~ in(ordered_pair(C,D),A)
| ~ in(D,B)
| ~ in(C,B) )
| ~ is_antisymmetric_in(A,B) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(C,sK2_skl(B,A)),skolemize(D,sK3_skl(B,A))],[f95]) ).
fof(f98,plain,
! [X0,X1] :
( in(sK2_skl(X1,X0),X1)
| is_antisymmetric_in(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f99,plain,
! [X0,X1] :
( in(sK3_skl(X1,X0),X1)
| is_antisymmetric_in(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f100,plain,
! [X0,X1] :
( in(ordered_pair(sK2_skl(X1,X0),sK3_skl(X1,X0)),X0)
| is_antisymmetric_in(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f101,plain,
! [X0,X1] :
( in(ordered_pair(sK3_skl(X1,X0),sK2_skl(X1,X0)),X0)
| is_antisymmetric_in(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f102,plain,
! [X0,X1] :
( sK2_skl(X1,X0) != sK3_skl(X1,X0)
| is_antisymmetric_in(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f106,plain,
! [X0] : relation(inclusion_relation(X0)),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f180,plain,
? [A] : ~ antisymmetric(inclusion_relation(A)),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f181,plain,
~ antisymmetric(inclusion_relation(sK14_skl)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(A,sK14_skl)],[f180]) ).
fof(f182,plain,
~ antisymmetric(inclusion_relation(sK14_skl)),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f193,plain,
! [X0] :
( relation_field(inclusion_relation(X0)) = X0
| ~ relation(inclusion_relation(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f86]) ).
fof(f194,plain,
! [X0,X1,X2] :
( subset(X1,X2)
| ~ in(ordered_pair(X1,X2),inclusion_relation(X0))
| ~ in(X2,X0)
| ~ in(X1,X0)
| ~ relation(inclusion_relation(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f87]) ).
fof(f201,plain,
! [X0,X1,X2] :
( subset(X0,X2)
| ~ in(ordered_pair(X0,X2),inclusion_relation(X1))
| ~ in(X2,X1)
| ~ in(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f194,f106]) ).
fof(f398,plain,
! [X0] : relation_field(inclusion_relation(X0)) = X0,
inference(forward_subsumption_resolution,[status(thm)],[f193,f106]) ).
fof(f399,plain,
! [X0] :
( ~ is_antisymmetric_in(inclusion_relation(X0),X0)
| antisymmetric(inclusion_relation(X0))
| ~ relation(inclusion_relation(X0)) ),
inference(paramodulation,[status(thm)],[f398,f81]) ).
fof(f401,plain,
! [X0] :
( ~ is_antisymmetric_in(inclusion_relation(X0),X0)
| antisymmetric(inclusion_relation(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f399,f106]) ).
fof(f534,plain,
! [X0,X1] :
( subset(sK2_skl(X1,inclusion_relation(X0)),sK3_skl(X1,inclusion_relation(X0)))
| ~ in(sK3_skl(X1,inclusion_relation(X0)),X0)
| ~ in(sK2_skl(X1,inclusion_relation(X0)),X0)
| is_antisymmetric_in(inclusion_relation(X0),X1)
| ~ relation(inclusion_relation(X0)) ),
inference(resolution,[status(thm)],[f100,f201]) ).
fof(f543,plain,
! [X0,X1] :
( subset(sK2_skl(X1,inclusion_relation(X0)),sK3_skl(X1,inclusion_relation(X0)))
| ~ in(sK3_skl(X1,inclusion_relation(X0)),X0)
| ~ in(sK2_skl(X1,inclusion_relation(X0)),X0)
| is_antisymmetric_in(inclusion_relation(X0),X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f534,f106]) ).
fof(f545,plain,
! [X0,X1] :
( ~ subset(sK3_skl(X1,inclusion_relation(X0)),sK2_skl(X1,inclusion_relation(X0)))
| sK3_skl(X1,inclusion_relation(X0)) = sK2_skl(X1,inclusion_relation(X0))
| ~ in(sK3_skl(X1,inclusion_relation(X0)),X0)
| ~ in(sK2_skl(X1,inclusion_relation(X0)),X0)
| is_antisymmetric_in(inclusion_relation(X0),X1) ),
inference(resolution,[status(thm)],[f543,f77]) ).
fof(f602,plain,
! [X0,X1] :
( subset(sK3_skl(X1,inclusion_relation(X0)),sK2_skl(X1,inclusion_relation(X0)))
| ~ in(sK2_skl(X1,inclusion_relation(X0)),X0)
| ~ in(sK3_skl(X1,inclusion_relation(X0)),X0)
| is_antisymmetric_in(inclusion_relation(X0),X1)
| ~ relation(inclusion_relation(X0)) ),
inference(resolution,[status(thm)],[f101,f201]) ).
fof(f611,plain,
! [X0,X1] :
( subset(sK3_skl(X1,inclusion_relation(X0)),sK2_skl(X1,inclusion_relation(X0)))
| ~ in(sK2_skl(X1,inclusion_relation(X0)),X0)
| ~ in(sK3_skl(X1,inclusion_relation(X0)),X0)
| is_antisymmetric_in(inclusion_relation(X0),X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f602,f106]) ).
fof(f616,plain,
! [X0,X1] :
( sK3_skl(X1,inclusion_relation(X0)) = sK2_skl(X1,inclusion_relation(X0))
| ~ in(sK3_skl(X1,inclusion_relation(X0)),X0)
| ~ in(sK2_skl(X1,inclusion_relation(X0)),X0)
| is_antisymmetric_in(inclusion_relation(X0),X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f545,f611]) ).
fof(f620,plain,
! [X0,X1] :
( is_antisymmetric_in(inclusion_relation(X0),X1)
| ~ relation(inclusion_relation(X0))
| ~ in(sK3_skl(X1,inclusion_relation(X0)),X0)
| ~ in(sK2_skl(X1,inclusion_relation(X0)),X0)
| is_antisymmetric_in(inclusion_relation(X0),X1) ),
inference(resolution,[status(thm)],[f616,f102]) ).
fof(f621,plain,
! [X0,X1] :
( ~ relation(inclusion_relation(X0))
| ~ in(sK3_skl(X1,inclusion_relation(X0)),X0)
| ~ in(sK2_skl(X1,inclusion_relation(X0)),X0)
| is_antisymmetric_in(inclusion_relation(X0),X1) ),
inference(duplicate_literals_removal,[status(thm)],[f620]) ).
fof(f622,plain,
! [X0,X1] :
( ~ in(sK3_skl(X1,inclusion_relation(X0)),X0)
| ~ in(sK2_skl(X1,inclusion_relation(X0)),X0)
| is_antisymmetric_in(inclusion_relation(X0),X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f621,f106]) ).
fof(f623,plain,
! [X0] :
( is_antisymmetric_in(inclusion_relation(X0),X0)
| ~ relation(inclusion_relation(X0))
| ~ in(sK3_skl(X0,inclusion_relation(X0)),X0)
| is_antisymmetric_in(inclusion_relation(X0),X0) ),
inference(resolution,[status(thm)],[f622,f98]) ).
fof(f624,plain,
! [X0] :
( ~ relation(inclusion_relation(X0))
| ~ in(sK3_skl(X0,inclusion_relation(X0)),X0)
| is_antisymmetric_in(inclusion_relation(X0),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f623]) ).
fof(f625,plain,
! [X0] :
( ~ relation(inclusion_relation(X0))
| is_antisymmetric_in(inclusion_relation(X0),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f624,f99]) ).
fof(f626,plain,
! [X0] : antisymmetric(inclusion_relation(X0)),
inference(backward_subsumption_resolution,[status(thm)],[f401,f627]) ).
fof(f627,plain,
! [X0] : is_antisymmetric_in(inclusion_relation(X0),X0),
inference(forward_subsumption_resolution,[status(thm)],[f625,f106]) ).
fof(f629,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f182,f626]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU271+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n006.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 06:04:57 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.44 % Drodi V4.1.1
% 0.15/0.46 % Refutation found
% 0.15/0.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.46 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/0.50 % Elapsed time: 0.069559 seconds
% 0.15/0.50 % CPU time: 0.198612 seconds
% 0.15/0.50 % Total memory used: 63.199 MB
% 0.15/0.50 % Net memory used: 63.124 MB
%------------------------------------------------------------------------------