%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU374+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/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:20:20 PM UTC 2026
% Result : Theorem 0.18s 0.47s
% Output : CNFRefutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 5
% Syntax : Number of formulae : 45 ( 17 unt; 0 def)
% Number of atoms : 204 ( 20 equ)
% Maximal formula atoms : 11 ( 4 avg)
% Number of connectives : 262 ( 103 ~; 96 |; 31 &)
% ( 2 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-4 aty)
% Number of variables : 92 ( 85 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> ! [C] :
( net_str(C,A)
=> ( subnetstr(C,A,B)
<=> ( the_mapping(A,C) = relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
& subrelstr(C,B) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> rel_str(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A,B] :
( ( net_str(B,A)
& one_sorted_str(A) )
=> ! [C] :
( subnetstr(C,A,B)
=> net_str(C,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,conjecture,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> ! [C] :
( subnetstr(C,A,B)
=> ! [D] :
( element(D,the_carrier(B))
=> ! [E] :
( element(E,the_carrier(B))
=> ! [F] :
( element(F,the_carrier(C))
=> ! [G] :
( element(G,the_carrier(C))
=> ( ( related(C,F,G)
& E = G
& D = F )
=> related(B,D,E) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,negated_conjecture,
~ ! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> ! [C] :
( subnetstr(C,A,B)
=> ! [D] :
( element(D,the_carrier(B))
=> ! [E] :
( element(E,the_carrier(B))
=> ! [F] :
( element(F,the_carrier(C))
=> ! [G] :
( element(G,the_carrier(C))
=> ( ( related(C,F,G)
& E = G
& D = F )
=> related(B,D,E) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f50]) ).
fof(f56,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( subrelstr(B,A)
=> ! [C] :
( element(C,the_carrier(A))
=> ! [D] :
( element(D,the_carrier(A))
=> ! [E] :
( element(E,the_carrier(B))
=> ! [F] :
( element(F,the_carrier(B))
=> ( ( related(B,E,F)
& F = D
& E = C )
=> related(A,C,D) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( subnetstr(C,A,B)
<=> ( the_mapping(A,C) = relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
& subrelstr(C,B) ) )
| ~ net_str(C,A) )
| ~ net_str(B,A) )
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f74,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( the_mapping(A,C) != relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
| ~ subrelstr(C,B)
| subnetstr(C,A,B) )
& ( ( the_mapping(A,C) = relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
& subrelstr(C,B) )
| ~ subnetstr(C,A,B) ) )
| ~ net_str(C,A) )
| ~ net_str(B,A) )
| ~ one_sorted_str(A) ),
inference(NNF_transformation,[status(thm)],[f73]) ).
fof(f75,plain,
! [X0,X1,X2] :
( subrelstr(X2,X1)
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X2,X0)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f86,plain,
! [A] :
( ! [B] :
( rel_str(B)
| ~ net_str(B,A) )
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f87,plain,
! [X0,X1] :
( rel_str(X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f90,plain,
! [A,B] :
( ! [C] :
( net_str(C,A)
| ~ subnetstr(C,A,B) )
| ~ net_str(B,A)
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f91,plain,
! [X0,X1,X2] :
( net_str(X2,X0)
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f179,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ? [E] :
( ? [F] :
( ? [G] :
( ~ related(B,D,E)
& related(C,F,G)
& E = G
& D = F
& element(G,the_carrier(C)) )
& element(F,the_carrier(C)) )
& element(E,the_carrier(B)) )
& element(D,the_carrier(B)) )
& subnetstr(C,A,B) )
& net_str(B,A) )
& one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f51]) ).
fof(f180,plain,
( ~ related(sK19_skl,sK21_skl,sK22_skl)
& related(sK20_skl,sK23_skl,sK24_skl)
& sK22_skl = sK24_skl
& sK21_skl = sK23_skl
& element(sK24_skl,the_carrier(sK20_skl))
& element(sK23_skl,the_carrier(sK20_skl))
& element(sK22_skl,the_carrier(sK19_skl))
& element(sK21_skl,the_carrier(sK19_skl))
& subnetstr(sK20_skl,sK18_skl,sK19_skl)
& net_str(sK19_skl,sK18_skl)
& one_sorted_str(sK18_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl,sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl]),skolemize(A,sK18_skl),skolemize(B,sK19_skl),skolemize(C,sK20_skl),skolemize(D,sK21_skl),skolemize(E,sK22_skl),skolemize(F,sK23_skl),skolemize(G,sK24_skl)],[f179]) ).
fof(f181,plain,
one_sorted_str(sK18_skl),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f182,plain,
net_str(sK19_skl,sK18_skl),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f183,plain,
subnetstr(sK20_skl,sK18_skl,sK19_skl),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f184,plain,
element(sK21_skl,the_carrier(sK19_skl)),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f185,plain,
element(sK22_skl,the_carrier(sK19_skl)),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f186,plain,
element(sK23_skl,the_carrier(sK20_skl)),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f187,plain,
element(sK24_skl,the_carrier(sK20_skl)),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f188,plain,
sK21_skl = sK23_skl,
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f189,plain,
sK22_skl = sK24_skl,
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f190,plain,
related(sK20_skl,sK23_skl,sK24_skl),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f191,plain,
~ related(sK19_skl,sK21_skl,sK22_skl),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f204,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ! [F] :
( related(A,C,D)
| ~ related(B,E,F)
| F != D
| E != C
| ~ element(F,the_carrier(B)) )
| ~ element(E,the_carrier(B)) )
| ~ element(D,the_carrier(A)) )
| ~ element(C,the_carrier(A)) )
| ~ subrelstr(B,A) )
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f205,plain,
! [X0,X1,X2,X3,X4,X5] :
( related(X0,X2,X3)
| ~ related(X1,X4,X5)
| X5 != X3
| X4 != X2
| ~ element(X5,the_carrier(X1))
| ~ element(X4,the_carrier(X1))
| ~ element(X3,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ subrelstr(X1,X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f214,plain,
! [X0,X1,X2,X3] :
( related(X0,X2,X3)
| ~ related(X1,X2,X3)
| ~ element(X3,the_carrier(X1))
| ~ element(X2,the_carrier(X1))
| ~ element(X3,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ subrelstr(X1,X0)
| ~ rel_str(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f205]) ).
fof(f215,plain,
element(sK21_skl,the_carrier(sK20_skl)),
inference(forward_demodulation,[status(thm)],[f188,f186]) ).
fof(f216,plain,
element(sK22_skl,the_carrier(sK20_skl)),
inference(forward_demodulation,[status(thm)],[f189,f187]) ).
fof(f217,plain,
related(sK20_skl,sK21_skl,sK24_skl),
inference(forward_demodulation,[status(thm)],[f188,f190]) ).
fof(f218,plain,
related(sK20_skl,sK21_skl,sK22_skl),
inference(forward_demodulation,[status(thm)],[f189,f217]) ).
fof(f220,plain,
! [X0,X1,X2] :
( subrelstr(X2,X1)
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f75,f91]) ).
fof(f221,plain,
! [X0,X1,X2,X3,X4] :
( related(X1,X3,X4)
| ~ related(X2,X3,X4)
| ~ element(X4,the_carrier(X2))
| ~ element(X3,the_carrier(X2))
| ~ element(X4,the_carrier(X1))
| ~ element(X3,the_carrier(X1))
| ~ rel_str(X1)
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(resolution,[status(thm)],[f220,f214]) ).
fof(f224,plain,
! [X0,X1,X2,X3,X4] :
( related(X1,X3,X4)
| ~ related(X2,X3,X4)
| ~ element(X4,the_carrier(X2))
| ~ element(X3,the_carrier(X2))
| ~ element(X4,the_carrier(X1))
| ~ element(X3,the_carrier(X1))
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f221,f87]) ).
fof(f225,plain,
! [X0,X1] :
( related(X1,sK21_skl,sK22_skl)
| ~ element(sK22_skl,the_carrier(sK20_skl))
| ~ element(sK21_skl,the_carrier(sK20_skl))
| ~ element(sK22_skl,the_carrier(X1))
| ~ element(sK21_skl,the_carrier(X1))
| ~ subnetstr(sK20_skl,X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(resolution,[status(thm)],[f224,f218]) ).
fof(f226,plain,
! [X0,X1] :
( related(X1,sK21_skl,sK22_skl)
| ~ element(sK22_skl,the_carrier(sK20_skl))
| ~ element(sK22_skl,the_carrier(X1))
| ~ element(sK21_skl,the_carrier(X1))
| ~ subnetstr(sK20_skl,X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f225,f215]) ).
fof(f227,plain,
! [X0,X1] :
( related(X1,sK21_skl,sK22_skl)
| ~ element(sK22_skl,the_carrier(X1))
| ~ element(sK21_skl,the_carrier(X1))
| ~ subnetstr(sK20_skl,X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f226,f216]) ).
fof(f229,plain,
! [X0] :
( related(sK19_skl,sK21_skl,sK22_skl)
| ~ element(sK21_skl,the_carrier(sK19_skl))
| ~ subnetstr(sK20_skl,X0,sK19_skl)
| ~ net_str(sK19_skl,X0)
| ~ one_sorted_str(X0) ),
inference(resolution,[status(thm)],[f227,f185]) ).
fof(f230,plain,
! [X0] :
( related(sK19_skl,sK21_skl,sK22_skl)
| ~ subnetstr(sK20_skl,X0,sK19_skl)
| ~ net_str(sK19_skl,X0)
| ~ one_sorted_str(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f229,f184]) ).
fof(f231,plain,
! [X0] :
( ~ subnetstr(sK20_skl,X0,sK19_skl)
| ~ net_str(sK19_skl,X0)
| ~ one_sorted_str(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f230,f191]) ).
fof(f232,plain,
( ~ subnetstr(sK20_skl,sK18_skl,sK19_skl)
| ~ one_sorted_str(sK18_skl) ),
inference(resolution,[status(thm)],[f231,f182]) ).
fof(f234,plain,
~ subnetstr(sK20_skl,sK18_skl,sK19_skl),
inference(forward_subsumption_resolution,[status(thm)],[f232,f181]) ).
fof(f236,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f234,f183]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU374+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n017.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Mon Sep 21 06:12:26 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.45 % Drodi V4.1.1
% 0.18/0.47 % Refutation found
% 0.18/0.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.18/0.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.18/0.55 % Elapsed time: 0.101243 seconds
% 0.18/0.55 % CPU time: 0.125842 seconds
% 0.18/0.55 % Total memory used: 13.291 MB
% 0.18/0.55 % Net memory used: 13.284 MB
%------------------------------------------------------------------------------