%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU383+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n002.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:54 PM UTC 2026
% Result : Theorem 35.56s 10.20s
% Output : Proof 35.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 12
% Syntax : Number of formulae : 99 ( 12 unt; 0 def)
% Number of atoms : 360 ( 40 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 396 ( 135 ~; 174 |; 62 &)
% ( 5 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-2 aty)
% Number of variables : 119 ( 2 sgn 71 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f38,axiom,
! [A,B,C] :
( ( element(B,powerset(C))
& in(A,B) )
=> element(A,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(f38_nnf,plain,
! [A,B,C] :
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [A,B,C] :
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c60,plain,
( element(X0,X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
fof(f35,axiom,
! [A,B] :
( ! [C] :
( in(C,A)
<=> in(C,B) )
=> A = B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_tarski) ).
fof(f35_nnf,plain,
! [A,B] :
( A = B
| ? [C] :
( ( in(C,B)
& ~ in(C,A) )
| ( ~ in(C,B)
& in(C,A) ) ) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
! [A,B] :
( A = B
| ( in(sk15(A,B),B)
& ~ in(sk15(A,B),A) )
| ( ~ in(sk15(A,B),B)
& in(sk15(A,B),A) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk15])],[f35_nnf]) ).
cnf(c54,plain,
( X0 = X1
| in(sk15(X0,X1),X1)
| in(sk15(X0,X1),X0) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p371,plain,
( X0 = X2
| in(sk15(X0,X2),X2)
| element(sk15(X0,X2),X1)
| ~ element(X0,powerset(X1)) ),
inference(resolution,[status(thm)],[c60,c54]) ).
fof(f44,conjecture,
! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( element(B,powerset(the_carrier(A)))
& upper_relstr_subset(B,A)
& filtered_subset(B,A)
& ~ empty(B) )
=> ( proper_element(B,powerset(the_carrier(A)))
<=> ~ in(bottom_of_relstr(A),B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_waybel_7) ).
fof(f44_neg,negated_conjecture,
~ ! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( element(B,powerset(the_carrier(A)))
& upper_relstr_subset(B,A)
& filtered_subset(B,A)
& ~ empty(B) )
=> ( proper_element(B,powerset(the_carrier(A)))
<=> ~ in(bottom_of_relstr(A),B) ) ) ),
inference(negated_conjecture,[status(cth)],[f44]) ).
fof(f44_nnf,plain,
? [A] :
( ? [B] :
( ( ( ~ in(bottom_of_relstr(A),B)
& ~ proper_element(B,powerset(the_carrier(A))) )
| ( in(bottom_of_relstr(A),B)
& proper_element(B,powerset(the_carrier(A))) ) )
& element(B,powerset(the_carrier(A)))
& upper_relstr_subset(B,A)
& filtered_subset(B,A)
& ~ empty(B) )
& rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ),
inference(nnf_transformation,[status(thm)],[f44_neg]) ).
fof(f44_sk,plain,
( ( ( ~ in(bottom_of_relstr(sk16),sk17)
& ~ proper_element(sk17,powerset(the_carrier(sk16))) )
| ( in(bottom_of_relstr(sk16),sk17)
& proper_element(sk17,powerset(the_carrier(sk16))) ) )
& element(sk17,powerset(the_carrier(sk16)))
& upper_relstr_subset(sk17,sk16)
& filtered_subset(sk17,sk16)
& ~ empty(sk17)
& rel_str(sk16)
& lower_bounded_relstr(sk16)
& antisymmetric_relstr(sk16)
& transitive_relstr(sk16)
& reflexive_relstr(sk16)
& ~ empty_carrier(sk16) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk16,sk17])],[f44_nnf]) ).
cnf(c76,plain,
element(sk17,powerset(the_carrier(sk16))),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p1292,plain,
( sk17 = X0
| in(sk15(sk17,X0),X0)
| element(sk15(sk17,X0),the_carrier(sk16)) ),
inference(resolution,[status(thm)],[p371,c76]) ).
fof(f33,axiom,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
fof(f33_nnf,plain,
! [A,B] :
( element(A,B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [A,B] :
( element(A,B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c51,plain,
( element(X0,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(p1330,plain,
( element(sk15(sk17,X0),X0)
| sk17 = X0
| element(sk15(sk17,X0),the_carrier(sk16)) ),
inference(resolution,[status(thm)],[p1292,c51]) ).
cnf(p1462,plain,
( sk17 = the_carrier(sk16)
| element(sk15(sk17,the_carrier(sk16)),the_carrier(sk16)) ),
inference(factoring,[status(thm)],[p1330]) ).
fof(f6,axiom,
! [A] :
( rel_str(A)
=> bottom_of_relstr(A) = join_on_relstr(A,empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d11_yellow_0) ).
fof(f6_nnf,plain,
! [A] :
( bottom_of_relstr(A) = join_on_relstr(A,empty_set)
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A] :
( bottom_of_relstr(A) = join_on_relstr(A,empty_set)
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c7,plain,
( bottom_of_relstr(X0) = join_on_relstr(X0,empty_set)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(c72,plain,
rel_str(sk16),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p92,plain,
bottom_of_relstr(sk16) = join_on_relstr(sk16,empty_set),
inference(resolution,[status(thm)],[c7,c72]) ).
fof(f9,axiom,
! [A,B] :
( rel_str(A)
=> element(join_on_relstr(A,B),the_carrier(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_yellow_0) ).
fof(f9_nnf,plain,
! [A,B] :
( element(join_on_relstr(A,B),the_carrier(A))
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [A,B] :
( element(join_on_relstr(A,B),the_carrier(A))
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c15,plain,
( element(join_on_relstr(X0,X1),the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p126,plain,
element(join_on_relstr(sk16,X0),the_carrier(sk16)),
inference(resolution,[status(thm)],[c15,c72]) ).
cnf(p127,plain,
element(bottom_of_relstr(sk16),the_carrier(sk16)),
inference(superposition,[status(thm)],[p92,p126]) ).
fof(f7,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ( upper_relstr_subset(B,A)
<=> ! [C] :
( element(C,the_carrier(A))
=> ! [D] :
( element(D,the_carrier(A))
=> ( ( related(A,C,D)
& in(C,B) )
=> in(D,B) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d20_waybel_0) ).
fof(f7_nnf,plain,
! [A] :
( ! [B] :
( ( ( ? [C] :
( ? [D] :
( ~ in(D,B)
& related(A,C,D)
& in(C,B)
& element(D,the_carrier(A)) )
& element(C,the_carrier(A)) )
| upper_relstr_subset(B,A) )
& ( ! [C] :
( ! [D] :
( in(D,B)
| ~ related(A,C,D)
| ~ in(C,B)
| ~ element(D,the_carrier(A)) )
| ~ element(C,the_carrier(A)) )
| ~ upper_relstr_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A,B,C,D] :
( ( ( ( ~ in(sk1(A,B),B)
& related(A,sk0(A,B),sk1(A,B))
& in(sk0(A,B),B)
& element(sk1(A,B),the_carrier(A))
& element(sk0(A,B),the_carrier(A)) )
| upper_relstr_subset(B,A) )
& ( in(D,B)
| ~ related(A,C,D)
| ~ in(C,B)
| ~ element(D,the_carrier(A))
| ~ element(C,the_carrier(A))
| ~ upper_relstr_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A)))
| ~ rel_str(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f7_nnf]) ).
cnf(c8,plain,
( in(X3,X1)
| ~ related(X0,X2,X3)
| ~ in(X2,X1)
| ~ element(X3,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p95,plain,
( in(X2,X0)
| ~ related(sk16,X1,X2)
| ~ in(X1,X0)
| ~ element(X2,the_carrier(sk16))
| ~ element(X1,the_carrier(sk16))
| ~ upper_relstr_subset(X0,sk16)
| ~ element(X0,powerset(the_carrier(sk16))) ),
inference(resolution,[status(thm)],[c8,c72]) ).
cnf(p96,plain,
( in(X1,sk17)
| ~ related(sk16,X0,X1)
| ~ in(X0,sk17)
| ~ element(X1,the_carrier(sk16))
| ~ element(X0,the_carrier(sk16))
| ~ upper_relstr_subset(sk17,sk16) ),
inference(resolution,[status(thm)],[p95,c76]) ).
cnf(c75,plain,
upper_relstr_subset(sk17,sk16),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p97,plain,
( in(X1,sk17)
| ~ related(sk16,X0,X1)
| ~ in(X0,sk17)
| ~ element(X1,the_carrier(sk16))
| ~ element(X0,the_carrier(sk16)) ),
inference(resolution,[status(thm)],[p96,c75]) ).
cnf(p132,plain,
( in(X0,sk17)
| ~ related(sk16,bottom_of_relstr(sk16),X0)
| ~ in(bottom_of_relstr(sk16),sk17)
| ~ element(X0,the_carrier(sk16)) ),
inference(resolution,[status(thm)],[p127,p97]) ).
cnf(p1514,plain,
( in(sk15(sk17,the_carrier(sk16)),sk17)
| ~ related(sk16,bottom_of_relstr(sk16),sk15(sk17,the_carrier(sk16)))
| ~ in(bottom_of_relstr(sk16),sk17)
| sk17 = the_carrier(sk16) ),
inference(resolution,[status(thm)],[p1462,p132]) ).
fof(f40,axiom,
! [A,B] :
( element(B,powerset(A))
=> ( proper_element(B,powerset(A))
<=> B != A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_tex_2) ).
fof(f40_nnf,plain,
! [A,B] :
( ( ( B = A
| proper_element(B,powerset(A)) )
& ( B != A
| ~ proper_element(B,powerset(A)) ) )
| ~ element(B,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [B,A] :
( ( ( B = A
| proper_element(B,powerset(A)) )
& ( B != A
| ~ proper_element(B,powerset(A)) ) )
| ~ element(B,powerset(A)) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c63,plain,
( X1 = X0
| proper_element(X1,powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(p415,plain,
( sk17 = the_carrier(sk16)
| proper_element(sk17,powerset(the_carrier(sk16))) ),
inference(resolution,[status(thm)],[c63,c76]) ).
cnf(c79,plain,
( ~ proper_element(sk17,powerset(the_carrier(sk16)))
| in(bottom_of_relstr(sk16),sk17) ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p423,plain,
( in(bottom_of_relstr(sk16),sk17)
| sk17 = the_carrier(sk16) ),
inference(resolution,[status(thm)],[p415,c79]) ).
cnf(p5644,plain,
( sk17 = the_carrier(sk16)
| in(sk15(sk17,the_carrier(sk16)),sk17)
| ~ related(sk16,bottom_of_relstr(sk16),sk15(sk17,the_carrier(sk16)))
| sk17 = the_carrier(sk16) ),
inference(resolution,[status(thm)],[p1514,p423]) ).
cnf(p6966,plain,
( in(sk15(sk17,the_carrier(sk16)),sk17)
| ~ related(sk16,bottom_of_relstr(sk16),sk15(sk17,the_carrier(sk16)))
| sk17 = the_carrier(sk16) ),
inference(factoring,[status(thm)],[p5644]) ).
fof(f37,axiom,
! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> related(A,bottom_of_relstr(A),B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t44_yellow_0) ).
fof(f37_nnf,plain,
! [A] :
( ! [B] :
( related(A,bottom_of_relstr(A),B)
| ~ element(B,the_carrier(A)) )
| ~ rel_str(A)
| ~ lower_bounded_relstr(A)
| ~ antisymmetric_relstr(A)
| empty_carrier(A) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [A,B] :
( related(A,bottom_of_relstr(A),B)
| ~ element(B,the_carrier(A))
| ~ rel_str(A)
| ~ lower_bounded_relstr(A)
| ~ antisymmetric_relstr(A)
| empty_carrier(A) ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c59,plain,
( related(X0,bottom_of_relstr(X0),X1)
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0)
| ~ lower_bounded_relstr(X0)
| ~ antisymmetric_relstr(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(c70,plain,
antisymmetric_relstr(sk16),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p356,plain,
( related(sk16,bottom_of_relstr(sk16),X0)
| ~ element(X0,the_carrier(sk16))
| ~ rel_str(sk16)
| ~ lower_bounded_relstr(sk16)
| empty_carrier(sk16) ),
inference(resolution,[status(thm)],[c59,c70]) ).
cnf(c71,plain,
lower_bounded_relstr(sk16),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p358,plain,
( related(sk16,bottom_of_relstr(sk16),X0)
| ~ element(X0,the_carrier(sk16))
| ~ rel_str(sk16)
| empty_carrier(sk16) ),
inference(resolution,[status(thm)],[p356,c71]) ).
cnf(p359,plain,
( related(sk16,bottom_of_relstr(sk16),X0)
| ~ element(X0,the_carrier(sk16))
| empty_carrier(sk16) ),
inference(resolution,[status(thm)],[p358,c72]) ).
cnf(p1517,plain,
( related(sk16,bottom_of_relstr(sk16),sk15(sk17,the_carrier(sk16)))
| empty_carrier(sk16)
| sk17 = the_carrier(sk16) ),
inference(resolution,[status(thm)],[p1462,p359]) ).
cnf(p6969,plain,
( empty_carrier(sk16)
| sk17 = the_carrier(sk16)
| in(sk15(sk17,the_carrier(sk16)),sk17)
| sk17 = the_carrier(sk16) ),
inference(resolution,[status(thm)],[p6966,p1517]) ).
cnf(p6970,plain,
( empty_carrier(sk16)
| in(sk15(sk17,the_carrier(sk16)),sk17)
| sk17 = the_carrier(sk16) ),
inference(factoring,[status(thm)],[p6969]) ).
fof(f34,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
fof(f34_nnf,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c52,plain,
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(p1516,plain,
( in(sk15(sk17,the_carrier(sk16)),the_carrier(sk16))
| empty(the_carrier(sk16))
| sk17 = the_carrier(sk16) ),
inference(resolution,[status(thm)],[p1462,c52]) ).
cnf(c55,plain,
( X0 = X1
| ~ in(sk15(X0,X1),X0)
| ~ in(sk15(X0,X1),X1) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p1627,plain,
( sk17 = the_carrier(sk16)
| ~ in(sk15(sk17,the_carrier(sk16)),sk17)
| empty(the_carrier(sk16))
| sk17 = the_carrier(sk16) ),
inference(resolution,[status(thm)],[p1516,c55]) ).
cnf(p1984,plain,
( ~ in(sk15(sk17,the_carrier(sk16)),sk17)
| empty(the_carrier(sk16))
| sk17 = the_carrier(sk16) ),
inference(factoring,[status(thm)],[p1627]) ).
cnf(p6974,plain,
( empty(the_carrier(sk16))
| sk17 = the_carrier(sk16)
| empty_carrier(sk16)
| sk17 = the_carrier(sk16) ),
inference(resolution,[status(thm)],[p6970,p1984]) ).
cnf(p6975,plain,
( empty(the_carrier(sk16))
| empty_carrier(sk16)
| sk17 = the_carrier(sk16) ),
inference(factoring,[status(thm)],[p6974]) ).
cnf(p314,plain,
( in(bottom_of_relstr(sk16),the_carrier(sk16))
| empty(the_carrier(sk16)) ),
inference(resolution,[status(thm)],[c52,p127]) ).
cnf(p7054,plain,
( in(bottom_of_relstr(sk16),sk17)
| empty(the_carrier(sk16))
| empty(the_carrier(sk16))
| empty_carrier(sk16) ),
inference(superposition,[status(thm)],[p6975,p314]) ).
cnf(p7546,plain,
( in(bottom_of_relstr(sk16),sk17)
| empty(the_carrier(sk16))
| empty_carrier(sk16) ),
inference(factoring,[status(thm)],[p7054]) ).
cnf(c78,plain,
( ~ in(bottom_of_relstr(sk16),sk17)
| proper_element(sk17,powerset(the_carrier(sk16))) ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p7547,plain,
( proper_element(sk17,powerset(the_carrier(sk16)))
| empty(the_carrier(sk16))
| empty_carrier(sk16) ),
inference(resolution,[status(thm)],[p7546,c78]) ).
cnf(c62,plain,
( X1 != X0
| ~ proper_element(X1,powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(p406,plain,
( sk17 != the_carrier(sk16)
| ~ proper_element(sk17,powerset(the_carrier(sk16))) ),
inference(resolution,[status(thm)],[c62,c76]) ).
cnf(p7564,plain,
( sk17 != the_carrier(sk16)
| empty(the_carrier(sk16))
| empty_carrier(sk16) ),
inference(resolution,[status(thm)],[p7547,p406]) ).
cnf(p7567,plain,
( empty(the_carrier(sk16))
| empty_carrier(sk16)
| empty(the_carrier(sk16))
| empty_carrier(sk16) ),
inference(resolution,[status(thm)],[p7564,p6975]) ).
cnf(p7569,plain,
( empty_carrier(sk16)
| empty(the_carrier(sk16))
| empty_carrier(sk16) ),
inference(factoring,[status(thm)],[p7567]) ).
cnf(p7570,plain,
( empty(the_carrier(sk16))
| empty_carrier(sk16) ),
inference(factoring,[status(thm)],[p7569]) ).
fof(f19,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ~ empty(the_carrier(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f19_nnf,plain,
! [A] :
( ~ empty(the_carrier(A))
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [A] :
( ~ empty(the_carrier(A))
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c25,plain,
( ~ empty(the_carrier(X0))
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
fof(f12,axiom,
! [A] :
( rel_str(A)
=> one_sorted_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f12_nnf,plain,
! [A] :
( one_sorted_str(A)
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [A] :
( one_sorted_str(A)
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c18,plain,
( one_sorted_str(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p147,plain,
one_sorted_str(sk16),
inference(resolution,[status(thm)],[c18,c72]) ).
cnf(p151,plain,
( ~ empty(the_carrier(sk16))
| empty_carrier(sk16) ),
inference(resolution,[status(thm)],[c25,p147]) ).
cnf(p7572,plain,
( empty_carrier(sk16)
| empty_carrier(sk16) ),
inference(resolution,[status(thm)],[p7570,p151]) ).
cnf(p7584,plain,
empty_carrier(sk16),
inference(factoring,[status(thm)],[p7572]) ).
cnf(c67,plain,
~ empty_carrier(sk16),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p7585,plain,
$false,
inference(resolution,[status(thm)],[p7584,c67]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU383+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 13:58:04 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 35.56/10.20 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 35.56/10.20 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------