%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU305+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 : n007.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:40 PM UTC 2026
% Result : Theorem 18.74s 2.99s
% Output : Proof 18.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 12
% Syntax : Number of formulae : 137 ( 103 unt; 0 def)
% Number of atoms : 257 ( 111 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 204 ( 84 ~; 59 |; 46 &)
% ( 1 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-4 aty)
% Number of variables : 106 ( 5 sgn 57 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [A,B,C] :
( ( element(C,the_carrier(A))
& element(B,the_carrier(A))
& join_semilatt_str(A)
& join_commutative(A)
& ~ empty_carrier(A) )
=> join_commut(A,B,C) = join_commut(A,C,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k3_lattices) ).
fof(f3_nnf,plain,
! [A,B,C] :
( join_commut(A,B,C) = join_commut(A,C,B)
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ join_semilatt_str(A)
| ~ join_commutative(A)
| empty_carrier(A) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,B,C] :
( join_commut(A,B,C) = join_commut(A,C,B)
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ join_semilatt_str(A)
| ~ join_commutative(A)
| empty_carrier(A) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c4,plain,
( join_commut(X0,X1,X2) = join_commut(X0,X2,X1)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ join_semilatt_str(X0)
| ~ join_commutative(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t168,plain,
ifeq(join_commutative(X1),true,ifeq(join_semilatt_str(X1),true,ifeq(element(X2,the_carrier(X1)),true,ifeq(element(X3,the_carrier(X1)),true,or(empty_carrier(X1),eq(join_commut(X1,X2,X3),join_commut(X1,X3,X2))),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t358,plain,
ifeq(join_commutative(X1),true,ifeq(join_semilatt_str(X1),true,ifeq(element(X2,the_carrier(X1)),true,ifeq(element(X3,the_carrier(X1)),true,or(empty_carrier(X1),eq(join_commut(X1,X2,X3),join_commut(X1,X3,X2))),true),true),true),true) = true,
inference(orient,[status(thm)],[t168]) ).
cnf(t42,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t177,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t42]) ).
fof(f30,axiom,
! [A,B,C] :
( ( element(C,the_carrier(A))
& element(B,the_carrier(A))
& join_semilatt_str(A)
& join_commutative(A)
& ~ empty_carrier(A) )
=> join_commut(A,B,C) = join(A,B,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k3_lattices) ).
fof(f30_nnf,plain,
! [A,B,C] :
( join_commut(A,B,C) = join(A,B,C)
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ join_semilatt_str(A)
| ~ join_commutative(A)
| empty_carrier(A) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [A,B,C] :
( join_commut(A,B,C) = join(A,B,C)
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ join_semilatt_str(A)
| ~ join_commutative(A)
| empty_carrier(A) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c39,plain,
( join_commut(X0,X1,X2) = join(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ join_semilatt_str(X0)
| ~ join_commutative(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(t167,plain,
ifeq(join_commutative(X1),true,ifeq(join_semilatt_str(X1),true,ifeq(element(X2,the_carrier(X1)),true,ifeq(element(X3,the_carrier(X1)),true,or(empty_carrier(X1),eq(join_commut(X1,X2,X3),join(X1,X2,X3))),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c39]) ).
cnf(t368,plain,
ifeq(join_commutative(X1),true,ifeq(join_semilatt_str(X1),true,ifeq(element(X2,the_carrier(X1)),true,ifeq(element(X3,the_carrier(X1)),true,or(empty_carrier(X1),eq(join_commut(X1,X2,X3),join(X1,X2,X3))),true),true),true),true) = true,
inference(orient,[status(thm)],[t167]) ).
fof(f5,axiom,
! [A] :
( ( join_semilatt_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> ( below(A,B,C)
<=> join(A,B,C) = C ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_lattices) ).
fof(f5_nnf,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( join(A,B,C) != C
| below(A,B,C) )
& ( join(A,B,C) = C
| ~ below(A,B,C) ) )
| ~ element(C,the_carrier(A)) )
| ~ element(B,the_carrier(A)) )
| ~ join_semilatt_str(A)
| empty_carrier(A) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A,B,C] :
( ( ( join(A,B,C) != C
| below(A,B,C) )
& ( join(A,B,C) = C
| ~ below(A,B,C) ) )
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ join_semilatt_str(A)
| empty_carrier(A) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c6,plain,
( join(X0,X1,X2) = X2
| ~ below(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ join_semilatt_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(hi5,axiom,
ifeq(join_semilatt_str(X0),true,ifeq(element(X1,the_carrier(X0)),true,ifeq(element(X2,the_carrier(X0)),true,ifeq(below(X0,X1,X2),true,or(empty_carrier(X0),eq(join(X0,X1,X2),X2)),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
fof(f34,conjecture,
! [A] :
( ( join_semilatt_str(A)
& join_commutative(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> ( ( below(A,C,B)
& below(A,B,C) )
=> B = C ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t26_lattices) ).
fof(f34_neg,negated_conjecture,
~ ! [A] :
( ( join_semilatt_str(A)
& join_commutative(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> ( ( below(A,C,B)
& below(A,B,C) )
=> B = C ) ) ) ),
inference(negated_conjecture,[status(cth)],[f34]) ).
fof(f34_nnf,plain,
? [A] :
( ? [B] :
( ? [C] :
( B != C
& below(A,C,B)
& below(A,B,C)
& element(C,the_carrier(A)) )
& element(B,the_carrier(A)) )
& join_semilatt_str(A)
& join_commutative(A)
& ~ empty_carrier(A) ),
inference(nnf_transformation,[status(thm)],[f34_neg]) ).
fof(f34_sk,plain,
( sk8 != sk9
& below(sk7,sk9,sk8)
& below(sk7,sk8,sk9)
& element(sk9,the_carrier(sk7))
& element(sk8,the_carrier(sk7))
& join_semilatt_str(sk7)
& join_commutative(sk7)
& ~ empty_carrier(sk7) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk7,sk8,sk9])],[f34_nnf]) ).
cnf(c46,plain,
join_semilatt_str(sk7),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(hi34,negated_conjecture,
join_semilatt_str(sk7) = true,
inference(equality_encoding,[status(esa)],[c46]) ).
cnf(c47,plain,
element(sk8,the_carrier(sk7)),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(hi35,negated_conjecture,
element(sk8,the_carrier(sk7)) = true,
inference(equality_encoding,[status(esa)],[c47]) ).
cnf(c48,plain,
element(sk9,the_carrier(sk7)),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(hi36,negated_conjecture,
element(sk9,the_carrier(sk7)) = true,
inference(equality_encoding,[status(esa)],[c48]) ).
cnf(c49,plain,
below(sk7,sk8,sk9),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(hi37,negated_conjecture,
below(sk7,sk8,sk9) = true,
inference(equality_encoding,[status(esa)],[c49]) ).
cnf(t61,plain,
or(empty_carrier(sk7),eq(join(sk7,sk8,sk9),sk9)) = true,
inference(hyper_resolution,[status(thm)],[hi5,hi34,hi35,hi36,hi37]) ).
cnf(t222,plain,
or(empty_carrier(sk7),eq(join(sk7,sk8,sk9),sk9)) = true,
inference(orient,[status(thm)],[t61]) ).
cnf(c44,plain,
~ empty_carrier(sk7),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(t1,plain,
empty_carrier(sk7) = false,
inference(equality_encoding,[status(esa)],[c44]) ).
cnf(t613,plain,
empty_carrier(sk7) = false,
inference(orient,[status(thm)],[t1]) ).
cnf(t817,plain,
or(false,eq(join(sk7,sk8,sk9),sk9)) = true,
inference(step,[status(thm)],[t222,t613]) ).
cnf(t20,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t173,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t20]) ).
cnf(t818,plain,
eq(join(sk7,sk8,sk9),sk9) = true,
inference(step,[status(thm)],[t817,t173]) ).
cnf(t626,plain,
eq(join(sk7,sk8,sk9),sk9) = true,
inference(rw,[status(thm)],[t818]) ).
cnf(t746,plain,
eq(join(sk7,sk8,sk9),sk9) = true,
inference(orient,[status(thm)],[t626]) ).
cnf(t747,plain,
sk9 = ifeq(true,true,join(sk7,sk8,sk9),sk9),
inference(cp,[status(thm)],[t177,t746]) ).
cnf(t30,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t174,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t30]) ).
cnf(t927,plain,
sk9 = join(sk7,sk8,sk9),
inference(step,[status(thm)],[t747,t174]) ).
cnf(t748,plain,
join(sk7,sk8,sk9) = sk9,
inference(orient,[status(thm)],[t927]) ).
cnf(t750,plain,
true = ifeq(join_commutative(sk7),true,ifeq(join_semilatt_str(sk7),true,ifeq(element(sk8,the_carrier(sk7)),true,ifeq(element(sk9,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk8,sk9),sk9)),true),true),true),true),
inference(cp,[status(thm)],[t368,t748]) ).
cnf(c45,plain,
join_commutative(sk7),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(t2,plain,
join_commutative(sk7) = true,
inference(equality_encoding,[status(esa)],[c45]) ).
cnf(t596,plain,
join_commutative(sk7) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t947,plain,
true = ifeq(true,true,ifeq(join_semilatt_str(sk7),true,ifeq(element(sk8,the_carrier(sk7)),true,ifeq(element(sk9,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk8,sk9),sk9)),true),true),true),true),
inference(step,[status(thm)],[t750,t596]) ).
cnf(t948,plain,
true = ifeq(join_semilatt_str(sk7),true,ifeq(element(sk8,the_carrier(sk7)),true,ifeq(element(sk9,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk8,sk9),sk9)),true),true),true),
inference(step,[status(thm)],[t947,t174]) ).
cnf(t4,plain,
join_semilatt_str(sk7) = true,
inference(equality_encoding,[status(esa)],[c46]) ).
cnf(t515,plain,
join_semilatt_str(sk7) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t949,plain,
true = ifeq(true,true,ifeq(element(sk8,the_carrier(sk7)),true,ifeq(element(sk9,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk8,sk9),sk9)),true),true),true),
inference(step,[status(thm)],[t948,t515]) ).
cnf(t950,plain,
true = ifeq(element(sk8,the_carrier(sk7)),true,ifeq(element(sk9,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk8,sk9),sk9)),true),true),
inference(step,[status(thm)],[t949,t174]) ).
cnf(t28,plain,
element(sk8,the_carrier(sk7)) = true,
inference(equality_encoding,[status(esa)],[c47]) ).
cnf(t419,plain,
element(sk8,the_carrier(sk7)) = true,
inference(orient,[status(thm)],[t28]) ).
cnf(t951,plain,
true = ifeq(true,true,ifeq(element(sk9,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk8,sk9),sk9)),true),true),
inference(step,[status(thm)],[t950,t419]) ).
cnf(t952,plain,
true = ifeq(element(sk9,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk8,sk9),sk9)),true),
inference(step,[status(thm)],[t951,t174]) ).
cnf(t29,plain,
element(sk9,the_carrier(sk7)) = true,
inference(equality_encoding,[status(esa)],[c48]) ).
cnf(t440,plain,
element(sk9,the_carrier(sk7)) = true,
inference(orient,[status(thm)],[t29]) ).
cnf(t953,plain,
true = ifeq(true,true,or(empty_carrier(sk7),eq(join_commut(sk7,sk8,sk9),sk9)),true),
inference(step,[status(thm)],[t952,t440]) ).
cnf(t954,plain,
true = or(empty_carrier(sk7),eq(join_commut(sk7,sk8,sk9),sk9)),
inference(step,[status(thm)],[t953,t174]) ).
cnf(t955,plain,
true = or(false,eq(join_commut(sk7,sk8,sk9),sk9)),
inference(step,[status(thm)],[t954,t613]) ).
cnf(t956,plain,
true = eq(join_commut(sk7,sk8,sk9),sk9),
inference(step,[status(thm)],[t955,t173]) ).
cnf(t787,plain,
eq(join_commut(sk7,sk8,sk9),sk9) = true,
inference(orient,[status(thm)],[t956]) ).
cnf(t788,plain,
sk9 = ifeq(true,true,join_commut(sk7,sk8,sk9),sk9),
inference(cp,[status(thm)],[t177,t787]) ).
cnf(t957,plain,
sk9 = join_commut(sk7,sk8,sk9),
inference(step,[status(thm)],[t788,t174]) ).
cnf(t789,plain,
join_commut(sk7,sk8,sk9) = sk9,
inference(orient,[status(thm)],[t957]) ).
cnf(t791,plain,
true = ifeq(join_commutative(sk7),true,ifeq(join_semilatt_str(sk7),true,ifeq(element(sk9,the_carrier(sk7)),true,ifeq(element(sk8,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk9,sk8),sk9)),true),true),true),true),
inference(cp,[status(thm)],[t358,t789]) ).
cnf(t958,plain,
true = ifeq(true,true,ifeq(join_semilatt_str(sk7),true,ifeq(element(sk9,the_carrier(sk7)),true,ifeq(element(sk8,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk9,sk8),sk9)),true),true),true),true),
inference(step,[status(thm)],[t791,t596]) ).
cnf(t959,plain,
true = ifeq(join_semilatt_str(sk7),true,ifeq(element(sk9,the_carrier(sk7)),true,ifeq(element(sk8,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk9,sk8),sk9)),true),true),true),
inference(step,[status(thm)],[t958,t174]) ).
cnf(t960,plain,
true = ifeq(true,true,ifeq(element(sk9,the_carrier(sk7)),true,ifeq(element(sk8,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk9,sk8),sk9)),true),true),true),
inference(step,[status(thm)],[t959,t515]) ).
cnf(t961,plain,
true = ifeq(element(sk9,the_carrier(sk7)),true,ifeq(element(sk8,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk9,sk8),sk9)),true),true),
inference(step,[status(thm)],[t960,t174]) ).
cnf(t962,plain,
true = ifeq(true,true,ifeq(element(sk8,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk9,sk8),sk9)),true),true),
inference(step,[status(thm)],[t961,t440]) ).
cnf(t963,plain,
true = ifeq(element(sk8,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk9,sk8),sk9)),true),
inference(step,[status(thm)],[t962,t174]) ).
cnf(t964,plain,
true = ifeq(true,true,or(empty_carrier(sk7),eq(join_commut(sk7,sk9,sk8),sk9)),true),
inference(step,[status(thm)],[t963,t419]) ).
cnf(t965,plain,
true = or(empty_carrier(sk7),eq(join_commut(sk7,sk9,sk8),sk9)),
inference(step,[status(thm)],[t964,t174]) ).
cnf(t966,plain,
true = or(false,eq(join_commut(sk7,sk9,sk8),sk9)),
inference(step,[status(thm)],[t965,t613]) ).
cnf(t967,plain,
true = eq(join_commut(sk7,sk9,sk8),sk9),
inference(step,[status(thm)],[t966,t173]) ).
cnf(c50,plain,
below(sk7,sk9,sk8),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(hi38,negated_conjecture,
below(sk7,sk9,sk8) = true,
inference(equality_encoding,[status(esa)],[c50]) ).
cnf(t62,plain,
or(empty_carrier(sk7),eq(join(sk7,sk9,sk8),sk8)) = true,
inference(hyper_resolution,[status(thm)],[hi5,hi34,hi36,hi35,hi38]) ).
cnf(t225,plain,
or(empty_carrier(sk7),eq(join(sk7,sk9,sk8),sk8)) = true,
inference(orient,[status(thm)],[t62]) ).
cnf(t815,plain,
or(false,eq(join(sk7,sk9,sk8),sk8)) = true,
inference(step,[status(thm)],[t225,t613]) ).
cnf(t816,plain,
eq(join(sk7,sk9,sk8),sk8) = true,
inference(step,[status(thm)],[t815,t173]) ).
cnf(t625,plain,
eq(join(sk7,sk9,sk8),sk8) = true,
inference(rw,[status(thm)],[t816]) ).
cnf(t741,plain,
eq(join(sk7,sk9,sk8),sk8) = true,
inference(orient,[status(thm)],[t625]) ).
cnf(t742,plain,
sk8 = ifeq(true,true,join(sk7,sk9,sk8),sk8),
inference(cp,[status(thm)],[t177,t741]) ).
cnf(t926,plain,
sk8 = join(sk7,sk9,sk8),
inference(step,[status(thm)],[t742,t174]) ).
cnf(t743,plain,
join(sk7,sk9,sk8) = sk8,
inference(orient,[status(thm)],[t926]) ).
cnf(t745,plain,
true = ifeq(join_commutative(sk7),true,ifeq(join_semilatt_str(sk7),true,ifeq(element(sk9,the_carrier(sk7)),true,ifeq(element(sk8,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk9,sk8),sk8)),true),true),true),true),
inference(cp,[status(thm)],[t368,t743]) ).
cnf(t936,plain,
true = ifeq(true,true,ifeq(join_semilatt_str(sk7),true,ifeq(element(sk9,the_carrier(sk7)),true,ifeq(element(sk8,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk9,sk8),sk8)),true),true),true),true),
inference(step,[status(thm)],[t745,t596]) ).
cnf(t937,plain,
true = ifeq(join_semilatt_str(sk7),true,ifeq(element(sk9,the_carrier(sk7)),true,ifeq(element(sk8,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk9,sk8),sk8)),true),true),true),
inference(step,[status(thm)],[t936,t174]) ).
cnf(t938,plain,
true = ifeq(true,true,ifeq(element(sk9,the_carrier(sk7)),true,ifeq(element(sk8,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk9,sk8),sk8)),true),true),true),
inference(step,[status(thm)],[t937,t515]) ).
cnf(t939,plain,
true = ifeq(element(sk9,the_carrier(sk7)),true,ifeq(element(sk8,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk9,sk8),sk8)),true),true),
inference(step,[status(thm)],[t938,t174]) ).
cnf(t940,plain,
true = ifeq(true,true,ifeq(element(sk8,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk9,sk8),sk8)),true),true),
inference(step,[status(thm)],[t939,t440]) ).
cnf(t941,plain,
true = ifeq(element(sk8,the_carrier(sk7)),true,or(empty_carrier(sk7),eq(join_commut(sk7,sk9,sk8),sk8)),true),
inference(step,[status(thm)],[t940,t174]) ).
cnf(t942,plain,
true = ifeq(true,true,or(empty_carrier(sk7),eq(join_commut(sk7,sk9,sk8),sk8)),true),
inference(step,[status(thm)],[t941,t419]) ).
cnf(t943,plain,
true = or(empty_carrier(sk7),eq(join_commut(sk7,sk9,sk8),sk8)),
inference(step,[status(thm)],[t942,t174]) ).
cnf(t944,plain,
true = or(false,eq(join_commut(sk7,sk9,sk8),sk8)),
inference(step,[status(thm)],[t943,t613]) ).
cnf(t945,plain,
true = eq(join_commut(sk7,sk9,sk8),sk8),
inference(step,[status(thm)],[t944,t173]) ).
cnf(t782,plain,
eq(join_commut(sk7,sk9,sk8),sk8) = true,
inference(orient,[status(thm)],[t945]) ).
cnf(t783,plain,
sk8 = ifeq(true,true,join_commut(sk7,sk9,sk8),sk8),
inference(cp,[status(thm)],[t177,t782]) ).
cnf(t946,plain,
sk8 = join_commut(sk7,sk9,sk8),
inference(step,[status(thm)],[t783,t174]) ).
cnf(t784,plain,
join_commut(sk7,sk9,sk8) = sk8,
inference(orient,[status(thm)],[t946]) ).
cnf(t968,plain,
true = eq(sk8,sk9),
inference(step,[status(thm)],[t967,t784]) ).
cnf(c51,plain,
sk8 != sk9,
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(t15,plain,
eq(sk8,sk9) = false,
inference(equality_encoding,[status(esa)],[c51]) ).
cnf(t701,plain,
eq(sk8,sk9) = false,
inference(orient,[status(thm)],[t15]) ).
cnf(t969,plain,
true = false,
inference(step,[status(thm)],[t968,t701]) ).
cnf(t792,plain,
false = true,
inference(orient,[status(thm)],[t969]) ).
fof(f0,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(f0_nnf,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
fof(f25,axiom,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_finsub_1) ).
fof(f25_nnf,plain,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c29,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
fof(f27,axiom,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc3_struct_0) ).
fof(f27_nnf,plain,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
( ~ empty_carrier(sk5)
& one_sorted_str(sk5) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk5])],[f27_nnf]) ).
cnf(c35,plain,
~ empty_carrier(sk5),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
fof(f38,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
fof(f38_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c56,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
fof(f40,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f40_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c58,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c29,c35,c44,c51,c56,c58]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t792]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU305+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 : n007.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:35:53 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 18.74/2.99 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.74/2.99 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------