%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU353+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:15 PM UTC 2026
% Result : Theorem 0.15s 0.43s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 11
% Syntax : Number of formulae : 65 ( 22 unt; 0 def)
% Number of atoms : 163 ( 29 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 155 ( 57 ~; 56 |; 30 &)
% ( 1 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-4 aty)
% Number of variables : 87 ( 85 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [A,B,C] :
( relation_of2(C,A,B)
=> ( ( v1_partfun1(C,A,B)
& function(C) )
=> ( quasi_total(C,A,B)
& function(C) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A] :
( one_sorted_str(A)
=> identity_on_carrier(A) = identity_as_relation_of(the_carrier(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A] :
( relation_of2_as_subset(identity_as_relation_of(A),A,A)
& v1_partfun1(identity_as_relation_of(A),A,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ~ empty(the_carrier(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [A] :
( transitive(identity_relation(A))
& antisymmetric(identity_relation(A))
& symmetric(identity_relation(A))
& reflexive(identity_relation(A))
& function(identity_relation(A))
& relation(identity_relation(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [A] : identity_as_relation_of(A) = identity_relation(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [A,B,C,D] :
( ( element(D,A)
& relation_of2(C,A,B)
& quasi_total(C,A,B)
& function(C)
& ~ empty(A) )
=> apply_as_element(A,B,C,D) = apply(C,D) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
<=> relation_of2(C,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [A,B] :
( in(B,A)
=> apply(identity_relation(A),B) = B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,conjecture,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> apply_as_element(the_carrier(A),the_carrier(A),identity_on_carrier(A),B) = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,negated_conjecture,
~ ! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> apply_as_element(the_carrier(A),the_carrier(A),identity_on_carrier(A),B) = B ) ),
inference(negated_conjecture,[status(cth)],[f57]) ).
fof(f61,plain,
! [A,B,C] :
( ( quasi_total(C,A,B)
& function(C) )
| ~ v1_partfun1(C,A,B)
| ~ function(C)
| ~ relation_of2(C,A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f63,plain,
! [X0,X1,X2] :
( quasi_total(X0,X1,X2)
| ~ v1_partfun1(X0,X1,X2)
| ~ function(X0)
| ~ relation_of2(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f95,plain,
! [A] :
( identity_on_carrier(A) = identity_as_relation_of(the_carrier(A))
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f96,plain,
! [X0] :
( identity_on_carrier(X0) = identity_as_relation_of(the_carrier(X0))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f97,plain,
( ! [A] : relation_of2_as_subset(identity_as_relation_of(A),A,A)
& ! [A] : v1_partfun1(identity_as_relation_of(A),A,A) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f98,plain,
! [X0] : v1_partfun1(identity_as_relation_of(X0),X0,X0),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f99,plain,
! [X0] : relation_of2_as_subset(identity_as_relation_of(X0),X0,X0),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f117,plain,
! [A] :
( ~ empty(the_carrier(A))
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f118,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f121,plain,
( ! [A] : transitive(identity_relation(A))
& ! [A] : antisymmetric(identity_relation(A))
& ! [A] : symmetric(identity_relation(A))
& ! [A] : reflexive(identity_relation(A))
& ! [A] : function(identity_relation(A))
& ! [A] : relation(identity_relation(A)) ),
inference(miniscoping,[status(thm)],[f31]) ).
fof(f123,plain,
! [X0] : function(identity_relation(X0)),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f178,plain,
! [X0] : identity_as_relation_of(X0) = identity_relation(X0),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f179,plain,
! [A,B,C,D] :
( apply_as_element(A,B,C,D) = apply(C,D)
| ~ element(D,A)
| ~ relation_of2(C,A,B)
| ~ quasi_total(C,A,B)
| ~ function(C)
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f180,plain,
! [X0,X1,X2,X3] :
( apply_as_element(X0,X2,X1,X3) = apply(X1,X3)
| ~ element(X3,X0)
| ~ relation_of2(X1,X0,X2)
| ~ quasi_total(X1,X0,X2)
| ~ function(X1)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f181,plain,
! [A,B,C] :
( ( ~ relation_of2(C,A,B)
| relation_of2_as_subset(C,A,B) )
& ( relation_of2(C,A,B)
| ~ relation_of2_as_subset(C,A,B) ) ),
inference(NNF_transformation,[status(thm)],[f46]) ).
fof(f182,plain,
( ! [A,B,C] :
( ~ relation_of2(C,A,B)
| relation_of2_as_subset(C,A,B) )
& ! [A,B,C] :
( relation_of2(C,A,B)
| ~ relation_of2_as_subset(C,A,B) ) ),
inference(miniscoping,[status(thm)],[f181]) ).
fof(f183,plain,
! [X0,X1,X2] :
( relation_of2(X0,X1,X2)
| ~ relation_of2_as_subset(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f189,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f190,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f191,plain,
! [A,B] :
( apply(identity_relation(A),B) = B
| ~ in(B,A) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f192,plain,
! [X0,X1] :
( apply(identity_relation(X1),X0) = X0
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f211,plain,
? [A] :
( ? [B] :
( apply_as_element(the_carrier(A),the_carrier(A),identity_on_carrier(A),B) != B
& element(B,the_carrier(A)) )
& one_sorted_str(A)
& ~ empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f58]) ).
fof(f212,plain,
( apply_as_element(the_carrier(sK15_skl),the_carrier(sK15_skl),identity_on_carrier(sK15_skl),sK16_skl) != sK16_skl
& element(sK16_skl,the_carrier(sK15_skl))
& one_sorted_str(sK15_skl)
& ~ empty_carrier(sK15_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl]),skolemize(A,sK15_skl),skolemize(B,sK16_skl)],[f211]) ).
fof(f213,plain,
~ empty_carrier(sK15_skl),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f214,plain,
one_sorted_str(sK15_skl),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f215,plain,
element(sK16_skl,the_carrier(sK15_skl)),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f216,plain,
apply_as_element(the_carrier(sK15_skl),the_carrier(sK15_skl),identity_on_carrier(sK15_skl),sK16_skl) != sK16_skl,
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f220,plain,
! [X0] :
( identity_on_carrier(X0) = identity_relation(the_carrier(X0))
| ~ one_sorted_str(X0) ),
inference(backward_demodulation,[status(thm)],[f178,f96]) ).
fof(f221,plain,
! [X0] : relation_of2_as_subset(identity_relation(X0),X0,X0),
inference(backward_demodulation,[status(thm)],[f178,f99]) ).
fof(f222,plain,
! [X0] : v1_partfun1(identity_relation(X0),X0,X0),
inference(backward_demodulation,[status(thm)],[f178,f98]) ).
fof(f252,plain,
! [X0] :
( quasi_total(identity_relation(X0),X0,X0)
| ~ function(identity_relation(X0))
| ~ relation_of2(identity_relation(X0),X0,X0) ),
inference(resolution,[status(thm)],[f222,f63]) ).
fof(f253,plain,
! [X0] :
( quasi_total(identity_relation(X0),X0,X0)
| ~ relation_of2(identity_relation(X0),X0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f252,f123]) ).
fof(f264,plain,
! [X0] : relation_of2(identity_relation(X0),X0,X0),
inference(resolution,[status(thm)],[f183,f221]) ).
fof(f266,plain,
! [X0] : quasi_total(identity_relation(X0),X0,X0),
inference(backward_subsumption_resolution,[status(thm)],[f253,f264]) ).
fof(f289,plain,
! [X0,X1] :
( empty(X0)
| ~ element(X1,X0)
| apply(identity_relation(X0),X1) = X1 ),
inference(resolution,[status(thm)],[f192,f190]) ).
fof(f292,plain,
identity_on_carrier(sK15_skl) = identity_relation(the_carrier(sK15_skl)),
inference(resolution,[status(thm)],[f220,f214]) ).
fof(f293,plain,
quasi_total(identity_on_carrier(sK15_skl),the_carrier(sK15_skl),the_carrier(sK15_skl)),
inference(paramodulation,[status(thm)],[f292,f266]) ).
fof(f294,plain,
relation_of2(identity_on_carrier(sK15_skl),the_carrier(sK15_skl),the_carrier(sK15_skl)),
inference(paramodulation,[status(thm)],[f292,f264]) ).
fof(f301,plain,
function(identity_on_carrier(sK15_skl)),
inference(paramodulation,[status(thm)],[f292,f123]) ).
fof(f346,plain,
! [X0] :
( apply_as_element(the_carrier(sK15_skl),the_carrier(sK15_skl),identity_on_carrier(sK15_skl),X0) = apply(identity_on_carrier(sK15_skl),X0)
| ~ element(X0,the_carrier(sK15_skl))
| ~ relation_of2(identity_on_carrier(sK15_skl),the_carrier(sK15_skl),the_carrier(sK15_skl))
| ~ function(identity_on_carrier(sK15_skl))
| empty(the_carrier(sK15_skl)) ),
inference(resolution,[status(thm)],[f180,f293]) ).
fof(f351,plain,
! [X0] :
( apply_as_element(the_carrier(sK15_skl),the_carrier(sK15_skl),identity_on_carrier(sK15_skl),X0) = apply(identity_on_carrier(sK15_skl),X0)
| ~ element(X0,the_carrier(sK15_skl))
| ~ relation_of2(identity_on_carrier(sK15_skl),the_carrier(sK15_skl),the_carrier(sK15_skl))
| empty(the_carrier(sK15_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f346,f301]) ).
fof(f374,plain,
! [X0] :
( apply_as_element(the_carrier(sK15_skl),the_carrier(sK15_skl),identity_on_carrier(sK15_skl),X0) = apply(identity_on_carrier(sK15_skl),X0)
| ~ element(X0,the_carrier(sK15_skl))
| empty(the_carrier(sK15_skl)) ),
inference(resolution,[status(thm)],[f351,f294]) ).
fof(f387,plain,
( apply_as_element(the_carrier(sK15_skl),the_carrier(sK15_skl),identity_on_carrier(sK15_skl),sK16_skl) = apply(identity_on_carrier(sK15_skl),sK16_skl)
| empty(the_carrier(sK15_skl)) ),
inference(resolution,[status(thm)],[f374,f215]) ).
fof(f388,plain,
( ~ one_sorted_str(sK15_skl)
| empty_carrier(sK15_skl)
| apply_as_element(the_carrier(sK15_skl),the_carrier(sK15_skl),identity_on_carrier(sK15_skl),sK16_skl) = apply(identity_on_carrier(sK15_skl),sK16_skl) ),
inference(resolution,[status(thm)],[f387,f118]) ).
fof(f393,plain,
( ~ one_sorted_str(sK15_skl)
| apply_as_element(the_carrier(sK15_skl),the_carrier(sK15_skl),identity_on_carrier(sK15_skl),sK16_skl) = apply(identity_on_carrier(sK15_skl),sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f388,f213]) ).
fof(f394,plain,
apply_as_element(the_carrier(sK15_skl),the_carrier(sK15_skl),identity_on_carrier(sK15_skl),sK16_skl) = apply(identity_on_carrier(sK15_skl),sK16_skl),
inference(resolution,[status(thm)],[f393,f214]) ).
fof(f397,plain,
apply(identity_on_carrier(sK15_skl),sK16_skl) != sK16_skl,
inference(backward_demodulation,[status(thm)],[f394,f216]) ).
fof(f445,plain,
( empty(the_carrier(sK15_skl))
| apply(identity_relation(the_carrier(sK15_skl)),sK16_skl) = sK16_skl ),
inference(resolution,[status(thm)],[f289,f215]) ).
fof(f451,plain,
( empty(the_carrier(sK15_skl))
| apply(identity_on_carrier(sK15_skl),sK16_skl) = sK16_skl ),
inference(forward_demodulation,[status(thm)],[f292,f445]) ).
fof(f452,plain,
empty(the_carrier(sK15_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f451,f397]) ).
fof(f455,plain,
( ~ one_sorted_str(sK15_skl)
| empty_carrier(sK15_skl) ),
inference(resolution,[status(thm)],[f452,f118]) ).
fof(f461,plain,
~ one_sorted_str(sK15_skl),
inference(forward_subsumption_resolution,[status(thm)],[f455,f213]) ).
fof(f462,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f214,f461]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU353+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n017.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 06:10:11 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.15/0.38 % Drodi V4.1.1
% 0.15/0.43 % Refutation found
% 0.15/0.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.43 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/0.46 % Elapsed time: 0.080126 seconds
% 0.15/0.46 % CPU time: 0.394279 seconds
% 0.15/0.46 % Total memory used: 112.667 MB
% 0.15/0.46 % Net memory used: 112.202 MB
%------------------------------------------------------------------------------