%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU320+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.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 : Tue Sep 29 12:48:20 PM UTC 2026
% Result : Theorem 3.96s 1.53s
% Output : Refutation 3.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 8
% Syntax : Number of formulae : 62 ( 9 unt; 4 def)
% Number of atoms : 160 ( 3 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 166 ( 68 ~; 69 |; 12 &)
% ( 8 <=>; 8 =>; 0 <=; 1 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 5 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 35 ( 0 sgn 29 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f145,axiom,
! [X0,X1] :
( element(X1,powerset(X0))
=> element(subset_complement(X0,X1),powerset(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_subset_1) ).
fof(f247,axiom,
! [X0,X1] :
( element(X1,powerset(X0))
=> subset_complement(X0,subset_complement(X0,X1)) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',involutiveness_k3_subset_1) ).
fof(f418,axiom,
! [X0] :
( top_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> ( closed_subset(X1,X0)
<=> open_subset(subset_complement(the_carrier(X0),X1),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t29_tops_1) ).
fof(f425,conjecture,
! [X0] :
( top_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> ( open_subset(X1,X0)
<=> closed_subset(subset_complement(the_carrier(X0),X1),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t30_tops_1) ).
fof(f426,negated_conjecture,
~ ! [X0] :
( top_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> ( open_subset(X1,X0)
<=> closed_subset(subset_complement(the_carrier(X0),X1),X0) ) ) ),
inference(negated_conjecture,[status(cth)],[f425]) ).
fof(f705,plain,
! [X0,X1] :
( element(subset_complement(X0,X1),powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(ennf_transformation,[],[f145]) ).
fof(f794,plain,
! [X0,X1] :
( subset_complement(X0,subset_complement(X0,X1)) = X1
| ~ element(X1,powerset(X0)) ),
inference(ennf_transformation,[],[f247]) ).
fof(f993,plain,
! [X0] :
( ! [X1] :
( ( closed_subset(X1,X0)
<=> open_subset(subset_complement(the_carrier(X0),X1),X0) )
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f418]) ).
fof(f999,plain,
? [X0] :
( ? [X1] :
( ( open_subset(X1,X0)
<~> closed_subset(subset_complement(the_carrier(X0),X1),X0) )
& element(X1,powerset(the_carrier(X0))) )
& top_str(X0) ),
inference(ennf_transformation,[],[f426]) ).
fof(f1645,plain,
! [X0] :
( ! [X1] :
( ( ( closed_subset(X1,X0)
| ~ open_subset(subset_complement(the_carrier(X0),X1),X0) )
& ( open_subset(subset_complement(the_carrier(X0),X1),X0)
| ~ closed_subset(X1,X0) ) )
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ top_str(X0) ),
inference(nnf_transformation,[],[f993]) ).
fof(f1648,plain,
? [X0] :
( ? [X1] :
( ( ~ closed_subset(subset_complement(the_carrier(X0),X1),X0)
| ~ open_subset(X1,X0) )
& ( closed_subset(subset_complement(the_carrier(X0),X1),X0)
| open_subset(X1,X0) )
& element(X1,powerset(the_carrier(X0))) )
& top_str(X0) ),
inference(nnf_transformation,[],[f999]) ).
fof(f1649,plain,
? [X0] :
( ? [X1] :
( ( ~ closed_subset(subset_complement(the_carrier(X0),X1),X0)
| ~ open_subset(X1,X0) )
& ( closed_subset(subset_complement(the_carrier(X0),X1),X0)
| open_subset(X1,X0) )
& element(X1,powerset(the_carrier(X0))) )
& top_str(X0) ),
inference(flattening,[],[f1648]) ).
fof(f1650,plain,
( ( ~ closed_subset(subset_complement(the_carrier(sK374),sK375),sK374)
| ~ open_subset(sK375,sK374) )
& ( closed_subset(subset_complement(the_carrier(sK374),sK375),sK374)
| open_subset(sK375,sK374) )
& element(sK375,powerset(the_carrier(sK374)))
& top_str(sK374) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK374,sK375]),skolemize(X0,sK374),skolemize(X1,sK375)],[f1649]) ).
fof(f2122,plain,
! [X0,X1] :
( element(subset_complement(X0,X1),powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[],[f705]) ).
fof(f2295,plain,
! [X0,X1] :
( subset_complement(X0,subset_complement(X0,X1)) = X1
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[],[f794]) ).
fof(f2908,plain,
! [X0,X1] :
( ~ top_str(X0)
| ~ closed_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| open_subset(subset_complement(the_carrier(X0),X1),X0) ),
inference(cnf_transformation,[],[f1645]) ).
fof(f2909,plain,
! [X0,X1] :
( closed_subset(X1,X0)
| ~ open_subset(subset_complement(the_carrier(X0),X1),X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f1645]) ).
fof(f2918,plain,
top_str(sK374),
inference(cnf_transformation,[],[f1650]) ).
fof(f2919,plain,
element(sK375,powerset(the_carrier(sK374))),
inference(cnf_transformation,[],[f1650]) ).
fof(f2920,plain,
( closed_subset(subset_complement(the_carrier(sK374),sK375),sK374)
| open_subset(sK375,sK374) ),
inference(cnf_transformation,[],[f1650]) ).
fof(f2921,plain,
( ~ closed_subset(subset_complement(the_carrier(sK374),sK375),sK374)
| ~ open_subset(sK375,sK374) ),
inference(cnf_transformation,[],[f1650]) ).
fof(f3317,definition,
( spl394_1
<=> open_subset(sK375,sK374) ),
introduced(definition,[new_symbols(definition,[spl394_1])],[avatar_definition]) ).
fof(f3318,plain,
( ~ open_subset(sK375,sK374)
| spl394_1 ),
inference(avatar_component_clause,[],[f3317]) ).
fof(f3319,plain,
( open_subset(sK375,sK374)
| ~ spl394_1 ),
inference(avatar_component_clause,[],[f3317]) ).
fof(f3321,definition,
( spl394_2
<=> closed_subset(subset_complement(the_carrier(sK374),sK375),sK374) ),
introduced(definition,[new_symbols(definition,[spl394_2])],[avatar_definition]) ).
fof(f3322,plain,
( ~ closed_subset(subset_complement(the_carrier(sK374),sK375),sK374)
| spl394_2 ),
inference(avatar_component_clause,[],[f3321]) ).
fof(f3323,plain,
( closed_subset(subset_complement(the_carrier(sK374),sK375),sK374)
| ~ spl394_2 ),
inference(avatar_component_clause,[],[f3321]) ).
fof(f3324,plain,
( spl394_1
| spl394_2 ),
inference(avatar_split_clause,[],[f2920,f3321,f3317]) ).
fof(f3325,plain,
( ~ spl394_1
| ~ spl394_2 ),
inference(avatar_split_clause,[],[f2921,f3321,f3317]) ).
fof(f3601,plain,
! [X0] :
( open_subset(subset_complement(the_carrier(sK374),X0),sK374)
| ~ element(X0,powerset(the_carrier(sK374)))
| ~ closed_subset(X0,sK374) ),
inference(resolution,[],[f2908,f2918]) ).
fof(f3751,definition,
( spl394_66
<=> element(subset_complement(the_carrier(sK374),sK375),powerset(the_carrier(sK374))) ),
introduced(definition,[new_symbols(definition,[spl394_66])],[avatar_definition]) ).
fof(f3753,plain,
( ~ element(subset_complement(the_carrier(sK374),sK375),powerset(the_carrier(sK374)))
| spl394_66 ),
inference(avatar_component_clause,[],[f3751]) ).
fof(f3943,plain,
! [X0] :
( open_subset(X0,sK374)
| ~ element(subset_complement(the_carrier(sK374),X0),powerset(the_carrier(sK374)))
| ~ closed_subset(subset_complement(the_carrier(sK374),X0),sK374)
| ~ element(X0,powerset(the_carrier(sK374))) ),
inference(superposition,[],[f3601,f2295]) ).
fof(f3945,plain,
! [X0] :
( ~ closed_subset(subset_complement(the_carrier(sK374),X0),sK374)
| open_subset(X0,sK374)
| ~ element(X0,powerset(the_carrier(sK374))) ),
inference(forward_subsumption_resolution,[],[f3943,f2122]) ).
fof(f4061,plain,
( open_subset(sK375,sK374)
| ~ element(sK375,powerset(the_carrier(sK374)))
| ~ spl394_2 ),
inference(resolution,[],[f3945,f3323]) ).
fof(f4070,plain,
( ~ element(sK375,powerset(the_carrier(sK374)))
| spl394_1
| ~ spl394_2 ),
inference(forward_subsumption_resolution,[],[f4061,f3318]) ).
fof(f4073,plain,
( $false
| spl394_1
| ~ spl394_2 ),
inference(forward_subsumption_resolution,[],[f4070,f2919]) ).
fof(f4074,plain,
( spl394_1
| ~ spl394_2 ),
inference(avatar_contradiction_clause,[],[f4073]) ).
fof(f4079,plain,
( ~ open_subset(subset_complement(the_carrier(sK374),subset_complement(the_carrier(sK374),sK375)),sK374)
| ~ element(subset_complement(the_carrier(sK374),sK375),powerset(the_carrier(sK374)))
| ~ top_str(sK374)
| spl394_2 ),
inference(resolution,[],[f3322,f2909]) ).
fof(f4082,plain,
( ~ open_subset(subset_complement(the_carrier(sK374),subset_complement(the_carrier(sK374),sK375)),sK374)
| ~ element(subset_complement(the_carrier(sK374),sK375),powerset(the_carrier(sK374)))
| spl394_2 ),
inference(forward_subsumption_resolution,[],[f4079,f2918]) ).
fof(f4085,definition,
( spl394_88
<=> open_subset(subset_complement(the_carrier(sK374),subset_complement(the_carrier(sK374),sK375)),sK374) ),
introduced(definition,[new_symbols(definition,[spl394_88])],[avatar_definition]) ).
fof(f4087,plain,
( ~ open_subset(subset_complement(the_carrier(sK374),subset_complement(the_carrier(sK374),sK375)),sK374)
| spl394_88 ),
inference(avatar_component_clause,[],[f4085]) ).
fof(f4088,plain,
( ~ spl394_66
| ~ spl394_88
| spl394_2 ),
inference(avatar_split_clause,[],[f4082,f3321,f4085,f3751]) ).
fof(f4096,plain,
( ~ element(sK375,powerset(the_carrier(sK374)))
| spl394_66 ),
inference(resolution,[],[f3753,f2122]) ).
fof(f4103,plain,
( $false
| spl394_66 ),
inference(forward_subsumption_resolution,[],[f4096,f2919]) ).
fof(f4104,plain,
spl394_66,
inference(avatar_contradiction_clause,[],[f4103]) ).
fof(f4108,plain,
( ~ open_subset(sK375,sK374)
| ~ element(sK375,powerset(the_carrier(sK374)))
| spl394_88 ),
inference(superposition,[],[f4087,f2295]) ).
fof(f4115,plain,
( ~ element(sK375,powerset(the_carrier(sK374)))
| ~ spl394_1
| spl394_88 ),
inference(forward_subsumption_resolution,[],[f4108,f3319]) ).
fof(f4126,plain,
( $false
| ~ spl394_1
| spl394_88 ),
inference(forward_subsumption_resolution,[],[f4115,f2919]) ).
fof(f4127,plain,
( ~ spl394_1
| spl394_88 ),
inference(avatar_contradiction_clause,[],[f4126]) ).
cnf(s1,plain,
( spl394_1
| spl394_2 ),
inference(sat_conversion,[],[f3324]) ).
cnf(s2,plain,
( ~ spl394_1
| ~ spl394_2 ),
inference(sat_conversion,[],[f3325]) ).
cnf(s73,plain,
( spl394_1
| ~ spl394_2 ),
inference(sat_conversion,[],[f4074]) ).
cnf(s74,plain,
( spl394_2
| ~ spl394_66
| ~ spl394_88 ),
inference(sat_conversion,[],[f4088]) ).
cnf(s76,plain,
spl394_66,
inference(sat_conversion,[],[f4104]) ).
cnf(s79,plain,
( ~ spl394_1
| spl394_88 ),
inference(sat_conversion,[],[f4127]) ).
cnf(s81,plain,
( spl394_2
| ~ spl394_88 ),
inference(rat,[],[s74,s76]) ).
cnf(s87,plain,
spl394_1,
inference(rat,[],[s1,s73]) ).
cnf(s88,plain,
spl394_88,
inference(rat,[],[s79,s87]) ).
cnf(s89,plain,
~ spl394_2,
inference(rat,[],[s2,s87]) ).
cnf(s90,plain,
$false,
inference(rat,[],[s81,s88,s89]) ).
fof(f4128,plain,
$false,
inference(avatar_sat_refutation,[],[s90]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU320+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.38 % Computer : n008.cluster.edu
% 0.14/0.38 % Model : x86_64 x86_64
% 0.14/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.38 % Memory : 8046.5625MB
% 0.14/0.38 % OS : Linux 6.8.0-71-generic
% 0.14/0.38 % CPULimit : 300
% 0.14/0.38 % WCLimit : 300
% 0.14/0.38 % DateTime : Mon Sep 28 04:41:25 UTC 2026
% 0.14/0.38 % CPUTime :
% 0.14/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.41 Running first-order theorem proving
% 0.14/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.98/1.34 % (1879882)Detected formulas, will run a generic FOF schedule.
% 2.98/1.34 % (1879890)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1091275998:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.98/1.34 % (1879890)Instruction limit reached!
% 2.98/1.34 % (1879890)------------------------------
% 2.98/1.34 % (1879890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.98/1.34 % (1879890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.98/1.34 % (1879890)CaDiCaL version: 2.1.3
% 2.98/1.34 % (1879890)Termination reason: Instruction limit
% 2.98/1.34 % (1879890)Termination phase: Saturation
% 2.98/1.34 % (1879890)Time elapsed: 0.034 s
% 2.98/1.34 % (1879890)Peak memory usage: 91 MB
% 2.98/1.34 % (1879890)Instructions burned: 110 (million)
% 2.98/1.34 % (1879893)dis-21_1_sil=8000:lcm=predicate:random_seed=1651573978:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.98/1.34 % (1879891)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1720884041:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.98/1.34 % (1879892)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3407041206:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.98/1.34 % (1879888)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1748291034:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.98/1.34 % (1879887)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1471737560:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.98/1.34 % (1879889)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1952093492:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.98/1.34 % (1879892)First to succeed.
% 2.98/1.34 % (1879892)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1879882"
% 2.98/1.34 % (1879893)Instruction limit reached!
% 2.98/1.34 % (1879893)------------------------------
% 2.98/1.34 % (1879893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.98/1.34 % (1879893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.98/1.34 % (1879893)CaDiCaL version: 2.1.3
% 2.98/1.34 % (1879893)Termination reason: Instruction limit
% 2.98/1.34 % (1879893)Termination phase: Saturation
% 2.98/1.34 % (1879893)Time elapsed: 0.065 s
% 2.98/1.34 % (1879893)Peak memory usage: 91 MB
% 2.98/1.34 % (1879893)Instructions burned: 130 (million)
% 2.98/1.34 % (1879891)Instruction limit reached!
% 2.98/1.34 % (1879891)------------------------------
% 2.98/1.34 % (1879891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.98/1.34 % (1879891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.98/1.34 % (1879891)CaDiCaL version: 2.1.3
% 2.98/1.34 % (1879891)Termination reason: Instruction limit
% 2.98/1.34 % (1879891)Termination phase: Saturation
% 2.98/1.34 % (1879891)Time elapsed: 0.078 s
% 2.98/1.34 % (1879891)Peak memory usage: 91 MB
% 2.98/1.34 % (1879891)Instructions burned: 119 (million)
% 2.98/1.34 % (1879895)lrs+10_1_sil=8000:sp=occurrence:random_seed=788382663:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 2.98/1.34 % (1879895)Instruction limit reached!
% 2.98/1.34 % (1879895)------------------------------
% 2.98/1.34 % (1879895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.98/1.34 % (1879895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.98/1.34 % (1879895)CaDiCaL version: 2.1.3
% 2.98/1.34 % (1879895)Termination reason: Instruction limit
% 2.98/1.34 % (1879895)Termination phase: Saturation
% 2.98/1.34 % (1879895)Time elapsed: 0.102 s
% 2.98/1.34 % (1879895)Peak memory usage: 95 MB
% 2.98/1.34 % (1879895)Instructions burned: 286 (million)
% 2.98/1.34 % (1879902)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2103392995:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 2.98/1.34 % (1879902)Also succeeded, but the first one will report.
% 2.98/1.34 % (1879904)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4023054675:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 2.98/1.34 % (1879905)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=353557774:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 3.96/1.53 % (1879905)Also succeeded, but the first one will report.
% 3.96/1.53 % (1879892)Refutation found. Thanks to Tanya!
% 3.96/1.53 % SZS status Theorem for theBenchmark
% 3.96/1.53 % SZS output start Proof for theBenchmark
% See solution above
% 3.96/1.53 % (1879892)------------------------------
% 3.96/1.53 % (1879892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.53 % (1879892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.53 % (1879892)CaDiCaL version: 2.1.3
% 3.96/1.53 % (1879892)Termination reason: Refutation
% 3.96/1.53 % (1879892)Time elapsed: 0.061 s
% 3.96/1.53 % (1879892)Peak memory usage: 92 MB
% 3.96/1.53 % (1879892)Instructions burned: 94 (million)
% 3.96/1.53 % (1879892)------------------------------
% 3.96/1.53 % (1879892)------------------------------
% 3.96/1.53 % (1879882)Success in time 0.485 s
% 3.96/1.53 % Vampire exiting
%------------------------------------------------------------------------------