%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU353+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n018.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 : Fri Sep 25 02:51:48 PM UTC 2026
% Result : Theorem 5.24s 1.28s
% Output : Proof 5.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 12
% Syntax : Number of formulae : 72 ( 21 unt; 0 def)
% Number of atoms : 171 ( 34 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 159 ( 60 ~; 63 |; 24 &)
% ( 1 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-4 aty)
% Number of variables : 80 ( 0 sgn 55 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f43,axiom,
! [A] : identity_as_relation_of(A) = identity_relation(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k6_partfun1) ).
fof(f43_nnf,plain,
! [A] : identity_as_relation_of(A) = identity_relation(A),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
! [A] : identity_as_relation_of(A) = identity_relation(A),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c91,plain,
identity_as_relation_of(X0) = identity_relation(X0),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
fof(f49,axiom,
! [A,B] :
( in(B,A)
=> apply(identity_relation(A),B) = B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t35_funct_1) ).
fof(f49_nnf,plain,
! [A,B] :
( apply(identity_relation(A),B) = B
| ~ in(B,A) ),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
! [B,A] :
( apply(identity_relation(A),B) = B
| ~ in(B,A) ),
inference(skolemisation,[status(esa)],[f49_nnf]) ).
cnf(c98,plain,
( apply(identity_relation(X0),X1) = X1
| ~ in(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
fof(f48,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f48_nnf,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(nnf_transformation,[status(thm)],[f48]) ).
fof(f48_sk,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(skolemisation,[status(esa)],[f48_nnf]) ).
cnf(c97,plain,
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
fof(f56,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/sandbox2/benchmark/theBenchmark.p',t91_tmap_1) ).
fof(f56_neg,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)],[f56]) ).
fof(f56_nnf,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(nnf_transformation,[status(thm)],[f56_neg]) ).
fof(f56_sk,plain,
( apply_as_element(the_carrier(sk15),the_carrier(sk15),identity_on_carrier(sk15),sk16) != sk16
& element(sk16,the_carrier(sk15))
& one_sorted_str(sk15)
& ~ empty_carrier(sk15) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk15,sk16])],[f56_nnf]) ).
cnf(c108,plain,
element(sk16,the_carrier(sk15)),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(p279,plain,
( in(sk16,the_carrier(sk15))
| empty(the_carrier(sk15)) ),
inference(resolution,[status(thm)],[c97,c108]) ).
cnf(p293,plain,
( empty(the_carrier(sk15))
| apply(identity_relation(the_carrier(sk15)),sk16) = sk16 ),
inference(resolution,[status(thm)],[c98,p279]) ).
cnf(p295,plain,
( empty(the_carrier(sk15))
| apply(identity_on_carrier(sk15),sk16) = sk16 ),
inference(superposition,[status(thm)],[c91,p293]) ).
fof(f45,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
<=> relation_of2(C,A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f45_nnf,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)],[f45]) ).
fof(f45_sk,plain,
! [C,A,B] :
( ( ~ 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(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c93,plain,
( relation_of2(X2,X0,X1)
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
fof(f9,axiom,
! [A] :
( one_sorted_str(A)
=> identity_on_carrier(A) = identity_as_relation_of(the_carrier(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d11_grcat_1) ).
fof(f9_nnf,plain,
! [A] :
( identity_on_carrier(A) = identity_as_relation_of(the_carrier(A))
| ~ one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [A] :
( identity_on_carrier(A) = identity_as_relation_of(the_carrier(A))
| ~ one_sorted_str(A) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c25,plain,
( identity_on_carrier(X0) = identity_as_relation_of(the_carrier(X0))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(c107,plain,
one_sorted_str(sk15),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(p181,plain,
identity_on_carrier(sk15) = identity_as_relation_of(the_carrier(sk15)),
inference(resolution,[status(thm)],[c25,c107]) ).
fof(f14,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/sandbox2/benchmark/theBenchmark.p',dt_k6_partfun1) ).
fof(f14_nnf,plain,
! [A] :
( relation_of2_as_subset(identity_as_relation_of(A),A,A)
& v1_partfun1(identity_as_relation_of(A),A,A) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [A] :
( relation_of2_as_subset(identity_as_relation_of(A),A,A)
& v1_partfun1(identity_as_relation_of(A),A,A) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c31,plain,
relation_of2_as_subset(identity_as_relation_of(X0),X0,X0),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p184,plain,
relation_of2_as_subset(identity_on_carrier(sk15),the_carrier(sk15),the_carrier(sk15)),
inference(superposition,[status(thm)],[p181,c31]) ).
cnf(p253,plain,
relation_of2(identity_on_carrier(sk15),the_carrier(sk15),the_carrier(sk15)),
inference(resolution,[status(thm)],[c93,p184]) ).
fof(f44,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/sandbox2/benchmark/theBenchmark.p',redefinition_k8_funct_2) ).
fof(f44_nnf,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(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [A,C,B,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(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c92,plain,
( apply_as_element(X0,X1,X2,X3) = apply(X2,X3)
| ~ element(X3,X0)
| ~ relation_of2(X2,X0,X1)
| ~ quasi_total(X2,X0,X1)
| ~ function(X2)
| empty(X0) ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
fof(f16,axiom,
! [A] :
( one_sorted_str(A)
=> ( relation_of2_as_subset(identity_on_carrier(A),the_carrier(A),the_carrier(A))
& quasi_total(identity_on_carrier(A),the_carrier(A),the_carrier(A))
& function(identity_on_carrier(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_grcat_1) ).
fof(f16_nnf,plain,
! [A] :
( ( relation_of2_as_subset(identity_on_carrier(A),the_carrier(A),the_carrier(A))
& quasi_total(identity_on_carrier(A),the_carrier(A),the_carrier(A))
& function(identity_on_carrier(A)) )
| ~ one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [A] :
( ( relation_of2_as_subset(identity_on_carrier(A),the_carrier(A),the_carrier(A))
& quasi_total(identity_on_carrier(A),the_carrier(A),the_carrier(A))
& function(identity_on_carrier(A)) )
| ~ one_sorted_str(A) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c33,plain,
( function(identity_on_carrier(X0))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p130,plain,
function(identity_on_carrier(sk15)),
inference(resolution,[status(thm)],[c33,c107]) ).
cnf(p246,plain,
( apply_as_element(X0,X1,identity_on_carrier(sk15),X2) = apply(identity_on_carrier(sk15),X2)
| ~ element(X2,X0)
| ~ relation_of2(identity_on_carrier(sk15),X0,X1)
| ~ quasi_total(identity_on_carrier(sk15),X0,X1)
| empty(X0) ),
inference(resolution,[status(thm)],[c92,p130]) ).
cnf(c34,plain,
( quasi_total(identity_on_carrier(X0),the_carrier(X0),the_carrier(X0))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p194,plain,
quasi_total(identity_on_carrier(sk15),the_carrier(sk15),the_carrier(sk15)),
inference(resolution,[status(thm)],[c34,c107]) ).
cnf(p250,plain,
( apply_as_element(the_carrier(sk15),the_carrier(sk15),identity_on_carrier(sk15),X0) = apply(identity_on_carrier(sk15),X0)
| ~ element(X0,the_carrier(sk15))
| ~ relation_of2(identity_on_carrier(sk15),the_carrier(sk15),the_carrier(sk15))
| empty(the_carrier(sk15)) ),
inference(resolution,[status(thm)],[p246,p194]) ).
cnf(p262,plain,
( apply_as_element(the_carrier(sk15),the_carrier(sk15),identity_on_carrier(sk15),X0) = apply(identity_on_carrier(sk15),X0)
| ~ element(X0,the_carrier(sk15))
| empty(the_carrier(sk15)) ),
inference(resolution,[status(thm)],[p253,p250]) ).
cnf(p272,plain,
( apply_as_element(the_carrier(sk15),the_carrier(sk15),identity_on_carrier(sk15),sk16) = apply(identity_on_carrier(sk15),sk16)
| empty(the_carrier(sk15)) ),
inference(resolution,[status(thm)],[p262,c108]) ).
cnf(c109,plain,
apply_as_element(the_carrier(sk15),the_carrier(sk15),identity_on_carrier(sk15),sk16) != sk16,
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(p276,plain,
( apply(identity_on_carrier(sk15),sk16) != sk16
| empty(the_carrier(sk15)) ),
inference(superposition,[status(thm)],[p272,c109]) ).
cnf(p297,plain,
( empty(the_carrier(sk15))
| empty(the_carrier(sk15)) ),
inference(resolution,[status(thm)],[p295,p276]) ).
cnf(p298,plain,
empty(the_carrier(sk15)),
inference(factoring,[status(thm)],[p297]) ).
fof(f53,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
fof(f53_nnf,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f53]) ).
fof(f53_sk,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(skolemisation,[status(esa)],[f53_nnf]) ).
cnf(c103,plain,
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(esa)],[f53_sk]) ).
cnf(p299,plain,
the_carrier(sk15) = empty_set,
inference(resolution,[status(thm)],[p298,c103]) ).
fof(f27,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ~ empty(the_carrier(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f27_nnf,plain,
! [A] :
( ~ empty(the_carrier(A))
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [A] :
( ~ empty(the_carrier(A))
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c46,plain,
( ~ empty(the_carrier(X0))
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p227,plain,
( ~ empty(the_carrier(sk15))
| empty_carrier(sk15) ),
inference(resolution,[status(thm)],[c46,c107]) ).
cnf(p310,plain,
( ~ empty(empty_set)
| empty_carrier(sk15) ),
inference(demodulation,[status(thm)],[p299,p227]) ).
fof(f29,axiom,
empty(empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_xboole_0) ).
fof(f29_nnf,plain,
empty(empty_set),
inference(nnf_transformation,[status(thm)],[f29]) ).
cnf(c48,plain,
empty(empty_set),
inference(cnf_transformation,[status(esa)],[f29_nnf]) ).
cnf(p325,plain,
empty_carrier(sk15),
inference(resolution,[status(thm)],[p310,c48]) ).
cnf(c106,plain,
~ empty_carrier(sk15),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(p326,plain,
$false,
inference(resolution,[status(thm)],[p325,c106]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU353+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n018.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 : Thu Sep 24 13:51:03 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 5.24/1.28 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.24/1.28 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------