%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU175+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 : n003.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:47:35 PM UTC 2026
% Result : Theorem 17.92s 6.16s
% Output : Refutation 38.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 47
% Syntax : Number of formulae : 317 ( 61 unt; 15 def)
% Number of atoms : 831 ( 172 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 939 ( 425 ~; 438 |; 14 &)
% ( 27 <=>; 34 =>; 0 <=; 1 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 9 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 10 con; 0-3 aty)
% Number of variables : 381 ( 0 sgn 374 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7,axiom,
! [X0,X1] :
( ( X0 != empty_set
=> ( X1 = set_meet(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ! [X3] :
( in(X3,X0)
=> in(X2,X3) ) ) ) )
& ( X0 = empty_set
=> ( X1 = set_meet(X0)
<=> X1 = empty_set ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_setfam_1) ).
fof(f9,axiom,
! [X0] :
( X0 = empty_set
<=> ! [X1] : ~ in(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f15,axiom,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X0)
=> in(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
fof(f17,axiom,
! [X0] : cast_to_subset(X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_subset_1) ).
fof(f18,axiom,
! [X0,X1] :
( X1 = union(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] :
( in(X2,X3)
& in(X3,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_tarski) ).
fof(f19,axiom,
! [X0,X1,X2] :
( X2 = set_difference(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,X0)
& ~ in(X3,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_xboole_0) ).
fof(f20,axiom,
! [X0,X1] :
( element(X1,powerset(X0))
=> subset_complement(X0,X1) = set_difference(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_subset_1) ).
fof(f23,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> ! [X2] :
( element(X2,powerset(powerset(X0)))
=> ( X2 = complements_of_subsets(X0,X1)
<=> ! [X3] :
( element(X3,powerset(X0))
=> ( in(X3,X2)
<=> in(subset_complement(X0,X3),X1) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_setfam_1) ).
fof(f29,axiom,
! [X0] : element(cast_to_subset(X0),powerset(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_subset_1) ).
fof(f38,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> element(union_of_subsets(X0,X1),powerset(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_setfam_1) ).
fof(f39,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> element(meet_of_subsets(X0,X1),powerset(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_setfam_1) ).
fof(f40,axiom,
! [X0,X1,X2] :
( ( element(X1,powerset(X0))
& element(X2,powerset(X0)) )
=> element(subset_difference(X0,X1,X2),powerset(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_subset_1) ).
fof(f41,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> element(complements_of_subsets(X0,X1),powerset(powerset(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_setfam_1) ).
fof(f51,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(f52,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> complements_of_subsets(X0,complements_of_subsets(X0,X1)) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',involutiveness_k7_setfam_1) ).
fof(f60,axiom,
! [X0,X1] :
( element(X1,powerset(X0))
=> ! [X2] :
( in(X2,X1)
=> in(X2,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l3_subset_1) ).
fof(f65,axiom,
! [X0,X1] :
( ! [X2] :
( in(X2,X0)
=> in(X2,X1) )
=> element(X0,powerset(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l71_subset_1) ).
fof(f70,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> union_of_subsets(X0,X1) = union(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k5_setfam_1) ).
fof(f71,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> meet_of_subsets(X0,X1) = set_meet(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k6_setfam_1) ).
fof(f72,axiom,
! [X0,X1,X2] :
( ( element(X1,powerset(X0))
& element(X2,powerset(X0)) )
=> subset_difference(X0,X1,X2) = set_difference(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k6_subset_1) ).
fof(f89,axiom,
! [X0] : set_intersection2(X0,empty_set) = empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_boole) ).
fof(f91,axiom,
! [X0,X1] :
( ! [X2] :
( in(X2,X0)
<=> in(X2,X1) )
=> X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_tarski) ).
fof(f101,axiom,
! [X0] : set_difference(X0,empty_set) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_boole) ).
fof(f102,axiom,
! [X0,X1] :
( element(X0,powerset(X1))
<=> subset(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
fof(f108,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> ~ ( X1 != empty_set
& complements_of_subsets(X0,X1) = empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t46_setfam_1) ).
fof(f110,conjecture,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> ( X1 != empty_set
=> subset_difference(X0,cast_to_subset(X0),union_of_subsets(X0,X1)) = meet_of_subsets(X0,complements_of_subsets(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t47_setfam_1) ).
fof(f111,negated_conjecture,
~ ! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> ( X1 != empty_set
=> subset_difference(X0,cast_to_subset(X0),union_of_subsets(X0,X1)) = meet_of_subsets(X0,complements_of_subsets(X0,X1)) ) ),
inference(negated_conjecture,[status(cth)],[f110]) ).
fof(f112,axiom,
! [X0,X1] : set_difference(X0,set_difference(X0,X1)) = set_intersection2(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f113,axiom,
! [X0] : set_difference(empty_set,X0) = empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_boole) ).
fof(f114,axiom,
! [X0,X1,X2] :
( ( in(X0,X1)
& element(X1,powerset(X2)) )
=> element(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(f116,axiom,
! [X0] :
( X0 != empty_set
=> ! [X1] :
( element(X1,powerset(X0))
=> ! [X2] :
( element(X2,X0)
=> ( ~ in(X2,X1)
=> in(X2,subset_complement(X0,X1)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t50_subset_1) ).
fof(f117,axiom,
! [X0,X1,X2] :
( element(X2,powerset(X0))
=> ~ ( in(X1,subset_complement(X0,X2))
& in(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t54_subset_1) ).
fof(f131,axiom,
! [X0,X1] :
( in(X0,X1)
=> subset(X0,union(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t92_zfmisc_1) ).
fof(f148,plain,
! [X0,X1] :
( ( ( X1 = set_meet(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ! [X3] :
( in(X2,X3)
| ~ in(X3,X0) ) ) )
| empty_set = X0 )
& ( ( X1 = set_meet(X0)
<=> X1 = empty_set )
| empty_set != X0 ) ),
inference(ennf_transformation,[],[f7]) ).
fof(f150,plain,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) ) ),
inference(ennf_transformation,[],[f15]) ).
fof(f151,plain,
! [X0,X1] :
( subset_complement(X0,X1) = set_difference(X0,X1)
| ~ element(X1,powerset(X0)) ),
inference(ennf_transformation,[],[f20]) ).
fof(f152,plain,
! [X0,X1] :
( ! [X2] :
( ( X2 = complements_of_subsets(X0,X1)
<=> ! [X3] :
( ( in(X3,X2)
<=> in(subset_complement(X0,X3),X1) )
| ~ element(X3,powerset(X0)) ) )
| ~ element(X2,powerset(powerset(X0))) )
| ~ element(X1,powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f23]) ).
fof(f156,plain,
! [X0,X1] :
( element(union_of_subsets(X0,X1),powerset(X0))
| ~ element(X1,powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f38]) ).
fof(f157,plain,
! [X0,X1] :
( element(meet_of_subsets(X0,X1),powerset(X0))
| ~ element(X1,powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f39]) ).
fof(f158,plain,
! [X0,X1,X2] :
( element(subset_difference(X0,X1,X2),powerset(X0))
| ~ element(X1,powerset(X0))
| ~ element(X2,powerset(X0)) ),
inference(ennf_transformation,[],[f40]) ).
fof(f159,plain,
! [X0,X1,X2] :
( element(subset_difference(X0,X1,X2),powerset(X0))
| ~ element(X1,powerset(X0))
| ~ element(X2,powerset(X0)) ),
inference(flattening,[],[f158]) ).
fof(f160,plain,
! [X0,X1] :
( element(complements_of_subsets(X0,X1),powerset(powerset(X0)))
| ~ element(X1,powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f41]) ).
fof(f163,plain,
! [X0,X1] :
( subset_complement(X0,subset_complement(X0,X1)) = X1
| ~ element(X1,powerset(X0)) ),
inference(ennf_transformation,[],[f51]) ).
fof(f164,plain,
! [X0,X1] :
( complements_of_subsets(X0,complements_of_subsets(X0,X1)) = X1
| ~ element(X1,powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f52]) ).
fof(f168,plain,
! [X0,X1] :
( ! [X2] :
( in(X2,X0)
| ~ in(X2,X1) )
| ~ element(X1,powerset(X0)) ),
inference(ennf_transformation,[],[f60]) ).
fof(f172,plain,
! [X0,X1] :
( element(X0,powerset(X1))
| ? [X2] :
( ~ in(X2,X1)
& in(X2,X0) ) ),
inference(ennf_transformation,[],[f65]) ).
fof(f174,plain,
! [X0,X1] :
( union_of_subsets(X0,X1) = union(X1)
| ~ element(X1,powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f70]) ).
fof(f175,plain,
! [X0,X1] :
( meet_of_subsets(X0,X1) = set_meet(X1)
| ~ element(X1,powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f71]) ).
fof(f176,plain,
! [X0,X1,X2] :
( subset_difference(X0,X1,X2) = set_difference(X1,X2)
| ~ element(X1,powerset(X0))
| ~ element(X2,powerset(X0)) ),
inference(ennf_transformation,[],[f72]) ).
fof(f177,plain,
! [X0,X1,X2] :
( subset_difference(X0,X1,X2) = set_difference(X1,X2)
| ~ element(X1,powerset(X0))
| ~ element(X2,powerset(X0)) ),
inference(flattening,[],[f176]) ).
fof(f195,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( in(X2,X0)
<~> in(X2,X1) ) ),
inference(ennf_transformation,[],[f91]) ).
fof(f202,plain,
! [X0,X1] :
( empty_set = X1
| empty_set != complements_of_subsets(X0,X1)
| ~ element(X1,powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f108]) ).
fof(f203,plain,
! [X0,X1] :
( empty_set = X1
| empty_set != complements_of_subsets(X0,X1)
| ~ element(X1,powerset(powerset(X0))) ),
inference(flattening,[],[f202]) ).
fof(f205,plain,
? [X0,X1] :
( subset_difference(X0,cast_to_subset(X0),union_of_subsets(X0,X1)) != meet_of_subsets(X0,complements_of_subsets(X0,X1))
& X1 != empty_set
& element(X1,powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f111]) ).
fof(f206,plain,
? [X0,X1] :
( subset_difference(X0,cast_to_subset(X0),union_of_subsets(X0,X1)) != meet_of_subsets(X0,complements_of_subsets(X0,X1))
& X1 != empty_set
& element(X1,powerset(powerset(X0))) ),
inference(flattening,[],[f205]) ).
fof(f207,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ in(X0,X1)
| ~ element(X1,powerset(X2)) ),
inference(ennf_transformation,[],[f114]) ).
fof(f208,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ in(X0,X1)
| ~ element(X1,powerset(X2)) ),
inference(flattening,[],[f207]) ).
fof(f210,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( in(X2,subset_complement(X0,X1))
| in(X2,X1)
| ~ element(X2,X0) )
| ~ element(X1,powerset(X0)) )
| empty_set = X0 ),
inference(ennf_transformation,[],[f116]) ).
fof(f211,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( in(X2,subset_complement(X0,X1))
| in(X2,X1)
| ~ element(X2,X0) )
| ~ element(X1,powerset(X0)) )
| empty_set = X0 ),
inference(flattening,[],[f210]) ).
fof(f212,plain,
! [X0,X1,X2] :
( ~ in(X1,subset_complement(X0,X2))
| ~ in(X1,X2)
| ~ element(X2,powerset(X0)) ),
inference(ennf_transformation,[],[f117]) ).
fof(f213,plain,
! [X0,X1,X2] :
( ~ in(X1,subset_complement(X0,X2))
| ~ in(X1,X2)
| ~ element(X2,powerset(X0)) ),
inference(flattening,[],[f212]) ).
fof(f225,plain,
! [X0,X1] :
( subset(X0,union(X1))
| ~ in(X0,X1) ),
inference(ennf_transformation,[],[f131]) ).
fof(f240,plain,
! [X2,X3,X0,X1] :
( empty_set = X0
| ~ in(X3,X0)
| in(X2,X3)
| ~ in(X2,X1)
| set_meet(X0) != X1 ),
inference(cnf_transformation,[],[f148]) ).
fof(f241,plain,
! [X2,X0,X1] :
( empty_set = X0
| in(sK1(X0,X2),X0)
| in(X2,X1)
| set_meet(X0) != X1 ),
inference(cnf_transformation,[],[f148]) ).
fof(f242,plain,
! [X2,X0,X1] :
( empty_set = X0
| ~ in(X2,sK1(X0,X2))
| in(X2,X1)
| set_meet(X0) != X1 ),
inference(cnf_transformation,[],[f148]) ).
fof(f249,plain,
! [X0] :
( in(sK4(X0),X0)
| empty_set = X0 ),
inference(cnf_transformation,[],[f9]) ).
fof(f250,plain,
! [X0,X1] :
( ~ in(X1,X0)
| empty_set != X0 ),
inference(cnf_transformation,[],[f9]) ).
fof(f279,plain,
! [X2,X0,X1] :
( ~ subset(X0,X1)
| in(X2,X1)
| ~ in(X2,X0) ),
inference(cnf_transformation,[],[f150]) ).
fof(f288,plain,
! [X0] : cast_to_subset(X0) = X0,
inference(cnf_transformation,[],[f17]) ).
fof(f292,plain,
! [X2,X0,X1] :
( in(sK16(X0,X2),X0)
| ~ in(X2,X1)
| union(X0) != X1 ),
inference(cnf_transformation,[],[f18]) ).
fof(f293,plain,
! [X2,X0,X1] :
( in(X2,sK16(X0,X2))
| ~ in(X2,X1)
| union(X0) != X1 ),
inference(cnf_transformation,[],[f18]) ).
fof(f300,plain,
! [X2,X3,X0,X1] :
( in(X3,X1)
| ~ in(X3,X0)
| in(X3,X2)
| set_difference(X0,X1) != X2 ),
inference(cnf_transformation,[],[f19]) ).
fof(f301,plain,
! [X0,X1] :
( set_difference(X0,X1) = subset_complement(X0,X1)
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[],[f151]) ).
fof(f305,plain,
! [X2,X0,X1] :
( in(subset_complement(X0,sK19(X0,X1,X2)),X1)
| ~ element(X2,powerset(powerset(X0)))
| ~ element(X1,powerset(powerset(X0)))
| in(sK19(X0,X1,X2),X2)
| complements_of_subsets(X0,X1) = X2 ),
inference(cnf_transformation,[],[f152]) ).
fof(f308,plain,
! [X2,X3,X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| ~ element(X2,powerset(powerset(X0)))
| ~ element(X3,powerset(X0))
| in(subset_complement(X0,X3),X1)
| ~ in(X3,X2)
| complements_of_subsets(X0,X1) != X2 ),
inference(cnf_transformation,[],[f152]) ).
fof(f311,plain,
! [X0] : element(cast_to_subset(X0),powerset(X0)),
inference(cnf_transformation,[],[f29]) ).
fof(f313,plain,
! [X0,X1] :
( element(union_of_subsets(X0,X1),powerset(X0))
| ~ element(X1,powerset(powerset(X0))) ),
inference(cnf_transformation,[],[f156]) ).
fof(f314,plain,
! [X0,X1] :
( element(meet_of_subsets(X0,X1),powerset(X0))
| ~ element(X1,powerset(powerset(X0))) ),
inference(cnf_transformation,[],[f157]) ).
fof(f315,plain,
! [X2,X0,X1] :
( element(subset_difference(X0,X1,X2),powerset(X0))
| ~ element(X1,powerset(X0))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[],[f159]) ).
fof(f316,plain,
! [X0,X1] :
( element(complements_of_subsets(X0,X1),powerset(powerset(X0)))
| ~ element(X1,powerset(powerset(X0))) ),
inference(cnf_transformation,[],[f160]) ).
fof(f325,plain,
! [X0,X1] :
( subset_complement(X0,subset_complement(X0,X1)) = X1
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[],[f163]) ).
fof(f326,plain,
! [X0,X1] :
( complements_of_subsets(X0,complements_of_subsets(X0,X1)) = X1
| ~ element(X1,powerset(powerset(X0))) ),
inference(cnf_transformation,[],[f164]) ).
fof(f336,plain,
! [X2,X0,X1] :
( ~ element(X1,powerset(X0))
| ~ in(X2,X1)
| in(X2,X0) ),
inference(cnf_transformation,[],[f168]) ).
fof(f345,plain,
! [X0,X1] :
( in(sK21(X0,X1),X0)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f172]) ).
fof(f346,plain,
! [X0,X1] :
( ~ in(sK21(X0,X1),X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f172]) ).
fof(f353,plain,
! [X0,X1] :
( union_of_subsets(X0,X1) = union(X1)
| ~ element(X1,powerset(powerset(X0))) ),
inference(cnf_transformation,[],[f174]) ).
fof(f354,plain,
! [X0,X1] :
( meet_of_subsets(X0,X1) = set_meet(X1)
| ~ element(X1,powerset(powerset(X0))) ),
inference(cnf_transformation,[],[f175]) ).
fof(f355,plain,
! [X2,X0,X1] :
( subset_difference(X0,X1,X2) = set_difference(X1,X2)
| ~ element(X1,powerset(X0))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[],[f177]) ).
fof(f377,plain,
! [X0] : empty_set = set_intersection2(X0,empty_set),
inference(cnf_transformation,[],[f89]) ).
fof(f379,plain,
! [X0,X1] :
( in(sK27(X0,X1),X1)
| in(sK27(X0,X1),X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f195]) ).
fof(f380,plain,
! [X0,X1] :
( ~ in(sK27(X0,X1),X1)
| ~ in(sK27(X0,X1),X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f195]) ).
fof(f397,plain,
! [X0] : set_difference(X0,empty_set) = X0,
inference(cnf_transformation,[],[f101]) ).
fof(f399,plain,
! [X0,X1] :
( ~ element(X0,powerset(X1))
| subset(X0,X1) ),
inference(cnf_transformation,[],[f102]) ).
fof(f408,plain,
! [X0,X1] :
( empty_set != complements_of_subsets(X0,X1)
| ~ element(X1,powerset(powerset(X0)))
| empty_set = X1 ),
inference(cnf_transformation,[],[f203]) ).
fof(f410,plain,
element(sK30,powerset(powerset(sK29))),
inference(cnf_transformation,[],[f206]) ).
fof(f411,plain,
empty_set != sK30,
inference(cnf_transformation,[],[f206]) ).
fof(f412,plain,
subset_difference(sK29,cast_to_subset(sK29),union_of_subsets(sK29,sK30)) != meet_of_subsets(sK29,complements_of_subsets(sK29,sK30)),
inference(cnf_transformation,[],[f206]) ).
fof(f413,plain,
! [X0,X1] : set_intersection2(X0,X1) = set_difference(X0,set_difference(X0,X1)),
inference(cnf_transformation,[],[f112]) ).
fof(f414,plain,
! [X0] : empty_set = set_difference(empty_set,X0),
inference(cnf_transformation,[],[f113]) ).
fof(f415,plain,
! [X2,X0,X1] :
( ~ element(X1,powerset(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(cnf_transformation,[],[f208]) ).
fof(f418,plain,
! [X2,X0,X1] :
( in(X2,subset_complement(X0,X1))
| ~ element(X1,powerset(X0))
| ~ element(X2,X0)
| in(X2,X1)
| empty_set = X0 ),
inference(cnf_transformation,[],[f211]) ).
fof(f419,plain,
! [X2,X0,X1] :
( ~ in(X1,subset_complement(X0,X2))
| ~ in(X1,X2)
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[],[f213]) ).
fof(f435,plain,
! [X0,X1] :
( subset(X0,union(X1))
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f225]) ).
fof(f483,plain,
! [X0] : empty_set = set_difference(X0,set_difference(X0,empty_set)),
inference(definition_unfolding,[],[f377,f413]) ).
fof(f505,plain,
! [X2,X0] :
( ~ in(X2,sK1(X0,X2))
| empty_set = X0
| in(X2,set_meet(X0)) ),
inference(equality_resolution,[],[f242]) ).
fof(f506,plain,
! [X2,X0] :
( in(sK1(X0,X2),X0)
| empty_set = X0
| in(X2,set_meet(X0)) ),
inference(equality_resolution,[],[f241]) ).
fof(f507,plain,
! [X2,X3,X0] :
( ~ in(X2,set_meet(X0))
| ~ in(X3,X0)
| in(X2,X3)
| empty_set = X0 ),
inference(equality_resolution,[],[f240]) ).
fof(f511,plain,
! [X1] : ~ in(X1,empty_set),
inference(equality_resolution,[],[f250]) ).
fof(f531,plain,
! [X2,X0] :
( in(X2,sK16(X0,X2))
| ~ in(X2,union(X0)) ),
inference(equality_resolution,[],[f293]) ).
fof(f532,plain,
! [X2,X0] :
( in(sK16(X0,X2),X0)
| ~ in(X2,union(X0)) ),
inference(equality_resolution,[],[f292]) ).
fof(f533,plain,
! [X3,X0,X1] :
( in(X3,set_difference(X0,X1))
| ~ in(X3,X0)
| in(X3,X1) ),
inference(equality_resolution,[],[f300]) ).
fof(f536,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| ~ element(complements_of_subsets(X0,X1),powerset(powerset(X0)))
| ~ element(X3,powerset(X0))
| in(subset_complement(X0,X3),X1)
| ~ in(X3,complements_of_subsets(X0,X1)) ),
inference(equality_resolution,[],[f308]) ).
fof(f542,definition,
sF34 = cast_to_subset(sK29),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
fof(f543,plain,
cast_to_subset(sK29) = sF34,
inference(reorient_equations,[],[f542]) ).
fof(f544,definition,
sF35 = union_of_subsets(sK29,sK30),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
fof(f545,plain,
union_of_subsets(sK29,sK30) = sF35,
inference(reorient_equations,[],[f544]) ).
fof(f546,definition,
sF36 = subset_difference(sK29,sF34,sF35),
introduced(definition,[new_symbols(definition,[sF36])],[function_definition]) ).
fof(f547,plain,
subset_difference(sK29,sF34,sF35) = sF36,
inference(reorient_equations,[],[f546]) ).
fof(f548,definition,
sF37 = complements_of_subsets(sK29,sK30),
introduced(definition,[new_symbols(definition,[sF37])],[function_definition]) ).
fof(f549,plain,
complements_of_subsets(sK29,sK30) = sF37,
inference(reorient_equations,[],[f548]) ).
fof(f550,definition,
sF38 = meet_of_subsets(sK29,sF37),
introduced(definition,[new_symbols(definition,[sF38])],[function_definition]) ).
fof(f551,plain,
meet_of_subsets(sK29,sF37) = sF38,
inference(reorient_equations,[],[f550]) ).
fof(f552,plain,
sF36 != sF38,
inference(definition_folding,[],[f412,f551,f549,f547,f545,f543]) ).
fof(f553,definition,
sF39 = powerset(sK29),
introduced(definition,[new_symbols(definition,[sF39])],[function_definition]) ).
fof(f554,plain,
powerset(sK29) = sF39,
inference(reorient_equations,[],[f553]) ).
fof(f555,definition,
sF40 = powerset(sF39),
introduced(definition,[new_symbols(definition,[sF40])],[function_definition]) ).
fof(f556,plain,
powerset(sF39) = sF40,
inference(reorient_equations,[],[f555]) ).
fof(f557,plain,
element(sK30,sF40),
inference(definition_folding,[],[f410,f556,f554]) ).
fof(f558,plain,
! [X0] : empty_set = set_difference(X0,X0),
inference(forward_demodulation,[],[f483,f397]) ).
fof(f560,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| ~ element(complements_of_subsets(X0,X1),powerset(powerset(X0)))
| in(subset_complement(X0,X3),X1)
| ~ in(X3,complements_of_subsets(X0,X1)) ),
inference(forward_subsumption_resolution,[],[f536,f415]) ).
fof(f561,plain,
sK29 = sF34,
inference(forward_demodulation,[],[f543,f288]) ).
fof(f562,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| in(subset_complement(X0,X3),X1)
| ~ in(X3,complements_of_subsets(X0,X1)) ),
inference(forward_subsumption_resolution,[],[f560,f316]) ).
fof(f564,plain,
sF36 = subset_difference(sK29,sK29,sF35),
inference(superposition,[],[f547,f561]) ).
fof(f565,plain,
! [X0] :
( ~ element(X0,sF39)
| subset(X0,sK29) ),
inference(superposition,[],[f399,f554]) ).
fof(f566,plain,
! [X0] :
( element(complements_of_subsets(sK29,X0),powerset(sF39))
| ~ element(X0,powerset(sF39)) ),
inference(superposition,[],[f316,f554]) ).
fof(f567,plain,
! [X0] :
( element(complements_of_subsets(sK29,X0),sF40)
| ~ element(X0,powerset(sF39)) ),
inference(forward_demodulation,[],[f566,f556]) ).
fof(f568,plain,
! [X0] :
( element(complements_of_subsets(sK29,X0),sF40)
| ~ element(X0,sF40) ),
inference(forward_demodulation,[],[f567,f556]) ).
fof(f570,plain,
! [X0] :
( element(meet_of_subsets(sK29,X0),sF39)
| ~ element(X0,powerset(sF39)) ),
inference(superposition,[],[f314,f554]) ).
fof(f571,plain,
! [X0] :
( element(meet_of_subsets(sK29,X0),sF39)
| ~ element(X0,sF40) ),
inference(forward_demodulation,[],[f570,f556]) ).
fof(f581,plain,
! [X0] :
( element(union_of_subsets(sK29,X0),sF39)
| ~ element(X0,powerset(sF39)) ),
inference(superposition,[],[f313,f554]) ).
fof(f582,plain,
! [X0] :
( element(union_of_subsets(sK29,X0),sF39)
| ~ element(X0,sF40) ),
inference(forward_demodulation,[],[f581,f556]) ).
fof(f584,plain,
( empty_set != sF37
| ~ element(sK30,powerset(powerset(sK29)))
| empty_set = sK30 ),
inference(superposition,[],[f408,f549]) ).
fof(f585,plain,
( empty_set != sF37
| ~ element(sK30,powerset(powerset(sK29))) ),
inference(forward_subsumption_resolution,[],[f584,f411]) ).
fof(f587,plain,
( ~ element(sK30,powerset(sF39))
| empty_set != sF37 ),
inference(forward_demodulation,[],[f585,f554]) ).
fof(f589,plain,
( ~ element(sK30,sF40)
| empty_set != sF37 ),
inference(forward_demodulation,[],[f587,f556]) ).
fof(f591,plain,
empty_set != sF37,
inference(forward_subsumption_resolution,[],[f589,f557]) ).
fof(f595,plain,
( sF35 = union(sK30)
| ~ element(sK30,powerset(powerset(sK29))) ),
inference(superposition,[],[f353,f545]) ).
fof(f598,plain,
( ~ element(sK30,powerset(sF39))
| sF35 = union(sK30) ),
inference(forward_demodulation,[],[f595,f554]) ).
fof(f599,plain,
( ~ element(sK30,sF40)
| sF35 = union(sK30) ),
inference(forward_demodulation,[],[f598,f556]) ).
fof(f600,plain,
sF35 = union(sK30),
inference(forward_subsumption_resolution,[],[f599,f557]) ).
fof(f604,plain,
! [X0,X1] :
( ~ element(X0,sF39)
| ~ in(X1,X0)
| in(X1,sK29) ),
inference(superposition,[],[f336,f554]) ).
fof(f613,plain,
( sF38 = set_meet(sF37)
| ~ element(sF37,powerset(powerset(sK29))) ),
inference(superposition,[],[f354,f551]) ).
fof(f616,plain,
( ~ element(sF37,powerset(sF39))
| sF38 = set_meet(sF37) ),
inference(forward_demodulation,[],[f613,f554]) ).
fof(f617,plain,
( ~ element(sF37,sF40)
| sF38 = set_meet(sF37) ),
inference(forward_demodulation,[],[f616,f556]) ).
fof(f624,plain,
! [X0,X1] :
( ~ element(X0,powerset(sF39))
| in(subset_complement(sK29,X1),X0)
| ~ in(X1,complements_of_subsets(sK29,X0)) ),
inference(superposition,[],[f562,f554]) ).
fof(f626,plain,
! [X0,X1] :
( ~ in(X1,complements_of_subsets(sK29,X0))
| in(subset_complement(sK29,X1),X0)
| ~ element(X0,sF40) ),
inference(forward_demodulation,[],[f624,f556]) ).
fof(f629,plain,
! [X0] :
( ~ in(X0,sF37)
| in(subset_complement(sK29,X0),sK30)
| ~ element(sK30,sF40) ),
inference(superposition,[],[f626,f549]) ).
fof(f631,plain,
! [X0,X1] :
( ~ in(X1,X0)
| in(subset_complement(sK29,X1),complements_of_subsets(sK29,X0))
| ~ element(complements_of_subsets(sK29,X0),sF40)
| ~ element(X0,powerset(powerset(sK29))) ),
inference(superposition,[],[f626,f326]) ).
fof(f632,plain,
! [X0,X1] :
( ~ element(X0,powerset(sF39))
| ~ in(X1,X0)
| in(subset_complement(sK29,X1),complements_of_subsets(sK29,X0))
| ~ element(complements_of_subsets(sK29,X0),sF40) ),
inference(forward_demodulation,[],[f631,f554]) ).
fof(f633,plain,
! [X0] :
( in(subset_complement(sK29,X0),sK30)
| ~ in(X0,sF37) ),
inference(forward_subsumption_resolution,[],[f629,f557]) ).
fof(f634,plain,
! [X0,X1] :
( ~ element(X0,sF40)
| ~ in(X1,X0)
| in(subset_complement(sK29,X1),complements_of_subsets(sK29,X0))
| ~ element(complements_of_subsets(sK29,X0),sF40) ),
inference(forward_demodulation,[],[f632,f556]) ).
fof(f635,plain,
! [X0,X1] :
( in(subset_complement(sK29,X1),complements_of_subsets(sK29,X0))
| ~ in(X1,X0)
| ~ element(X0,sF40) ),
inference(forward_subsumption_resolution,[],[f634,f568]) ).
fof(f643,plain,
( sF36 = set_difference(sK29,sF35)
| ~ element(sK29,powerset(sK29))
| ~ element(sF35,powerset(sK29)) ),
inference(superposition,[],[f355,f564]) ).
fof(f644,plain,
( ~ element(sK29,sF39)
| sF36 = set_difference(sK29,sF35)
| ~ element(sF35,powerset(sK29)) ),
inference(forward_demodulation,[],[f643,f554]) ).
fof(f646,plain,
( ~ element(sF35,sF39)
| ~ element(sK29,sF39)
| sF36 = set_difference(sK29,sF35) ),
inference(forward_demodulation,[],[f644,f554]) ).
fof(f656,plain,
! [X0] :
( element(X0,powerset(X0))
| element(X0,powerset(X0)) ),
inference(resolution,[],[f345,f346]) ).
fof(f657,plain,
! [X0] : element(empty_set,powerset(X0)),
inference(resolution,[],[f345,f511]) ).
fof(f661,plain,
! [X0] : element(X0,powerset(X0)),
inference(duplicate_literal_removal,[],[f656]) ).
fof(f670,plain,
! [X0,X1] :
( subset_complement(X0,set_difference(X0,X1)) = X1
| ~ element(X1,powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(superposition,[],[f325,f301]) ).
fof(f673,plain,
! [X0,X1] :
( subset_complement(X0,set_difference(X0,X1)) = X1
| ~ element(X1,powerset(X0)) ),
inference(duplicate_literal_removal,[],[f670]) ).
fof(f692,plain,
element(cast_to_subset(sK29),sF39),
inference(superposition,[],[f311,f554]) ).
fof(f695,plain,
element(sK29,sF39),
inference(forward_demodulation,[],[f692,f288]) ).
fof(f700,plain,
( ~ element(sF35,sF39)
| sF36 = set_difference(sK29,sF35) ),
inference(backward_subsumption_resolution,[],[f646,f695]) ).
fof(f721,plain,
( element(sF36,powerset(sK29))
| ~ element(sK29,powerset(sK29))
| ~ element(sF35,powerset(sK29)) ),
inference(superposition,[],[f315,f564]) ).
fof(f726,plain,
( element(sF36,powerset(sK29))
| ~ element(sF35,powerset(sK29)) ),
inference(forward_subsumption_resolution,[],[f721,f661]) ).
fof(f728,plain,
( element(sF36,sF39)
| ~ element(sF35,powerset(sK29)) ),
inference(forward_demodulation,[],[f726,f554]) ).
fof(f730,plain,
( ~ element(sF35,sF39)
| element(sF36,sF39) ),
inference(forward_demodulation,[],[f728,f554]) ).
fof(f739,plain,
! [X0,X1] :
( in(subset_complement(X0,X1),empty_set)
| ~ in(X1,complements_of_subsets(X0,empty_set)) ),
inference(resolution,[],[f657,f562]) ).
fof(f743,plain,
! [X0,X1] : ~ in(X1,complements_of_subsets(X0,empty_set)),
inference(forward_subsumption_resolution,[],[f739,f511]) ).
fof(f745,plain,
! [X0] : empty_set = complements_of_subsets(X0,empty_set),
inference(resolution,[],[f743,f249]) ).
fof(f794,plain,
! [X0,X1] :
( ~ element(X0,powerset(powerset(X1)))
| ~ element(empty_set,powerset(powerset(X1)))
| in(sK19(X1,empty_set,X0),X0)
| complements_of_subsets(X1,empty_set) = X0 ),
inference(resolution,[],[f305,f511]) ).
fof(f802,plain,
! [X0,X1] :
( ~ element(X0,powerset(powerset(X1)))
| in(sK19(X1,empty_set,X0),X0)
| complements_of_subsets(X1,empty_set) = X0 ),
inference(forward_subsumption_resolution,[],[f794,f657]) ).
fof(f807,plain,
! [X0,X1] :
( in(sK19(X1,empty_set,X0),X0)
| ~ element(X0,powerset(powerset(X1)))
| empty_set = X0 ),
inference(forward_demodulation,[],[f802,f745]) ).
fof(f865,plain,
! [X0,X1] :
( ~ element(X1,sF39)
| ~ in(X0,X1)
| element(X0,sK29) ),
inference(superposition,[],[f415,f554]) ).
fof(f866,plain,
! [X0,X1] :
( ~ element(X1,sF40)
| ~ in(X0,X1)
| element(X0,sF39) ),
inference(superposition,[],[f415,f556]) ).
fof(f921,plain,
! [X0] :
( subset_complement(X0,empty_set) = X0
| ~ element(X0,powerset(X0)) ),
inference(superposition,[],[f673,f558]) ).
fof(f939,plain,
! [X0] : subset_complement(X0,empty_set) = X0,
inference(forward_subsumption_resolution,[],[f921,f661]) ).
fof(f958,plain,
! [X0] :
( in(subset_complement(sK29,X0),sF37)
| ~ in(X0,sK30)
| ~ element(sK30,sF40) ),
inference(superposition,[],[f635,f549]) ).
fof(f962,plain,
! [X0] :
( in(subset_complement(sK29,X0),sF37)
| ~ in(X0,sK30) ),
inference(forward_subsumption_resolution,[],[f958,f557]) ).
fof(f990,plain,
! [X0,X1] :
( ~ in(X1,meet_of_subsets(sK29,X0))
| ~ element(X0,sF40)
| in(X1,sK29) ),
inference(resolution,[],[f571,f604]) ).
fof(f1005,plain,
! [X0] :
( ~ in(X0,sF38)
| ~ element(sF37,sF40)
| in(X0,sK29) ),
inference(superposition,[],[f990,f551]) ).
fof(f1032,definition,
( spl41_3
<=> sF36 = set_difference(sK29,sF35) ),
introduced(definition,[new_symbols(definition,[spl41_3])],[avatar_definition]) ).
fof(f1033,plain,
( sF36 = set_difference(sK29,sF35)
| ~ spl41_3 ),
inference(avatar_component_clause,[],[f1032]) ).
fof(f1035,definition,
( spl41_4
<=> element(sF35,sF39) ),
introduced(definition,[new_symbols(definition,[spl41_4])],[avatar_definition]) ).
fof(f1036,plain,
( ~ element(sF35,sF39)
| spl41_4 ),
inference(avatar_component_clause,[],[f1035]) ).
fof(f1037,plain,
( spl41_3
| ~ spl41_4 ),
inference(avatar_split_clause,[],[f700,f1035,f1032]) ).
fof(f1052,definition,
( spl41_5
<=> sF38 = set_meet(sF37) ),
introduced(definition,[new_symbols(definition,[spl41_5])],[avatar_definition]) ).
fof(f1053,plain,
( sF38 = set_meet(sF37)
| ~ spl41_5 ),
inference(avatar_component_clause,[],[f1052]) ).
fof(f1055,definition,
( spl41_6
<=> element(sF37,sF40) ),
introduced(definition,[new_symbols(definition,[spl41_6])],[avatar_definition]) ).
fof(f1056,plain,
( ~ element(sF37,sF40)
| spl41_6 ),
inference(avatar_component_clause,[],[f1055]) ).
fof(f1057,plain,
( spl41_5
| ~ spl41_6 ),
inference(avatar_split_clause,[],[f617,f1055,f1052]) ).
fof(f1098,plain,
( element(sF35,sF39)
| ~ element(sK30,sF40) ),
inference(superposition,[],[f582,f545]) ).
fof(f1101,plain,
( ~ element(sK30,sF40)
| spl41_4 ),
inference(forward_subsumption_resolution,[],[f1098,f1036]) ).
fof(f1104,plain,
( $false
| spl41_4 ),
inference(forward_subsumption_resolution,[],[f1101,f557]) ).
fof(f1105,plain,
spl41_4,
inference(avatar_contradiction_clause,[],[f1104]) ).
fof(f1106,plain,
element(sF35,sF39),
inference(forward_subsumption_resolution,[],[f1098,f557]) ).
fof(f1107,plain,
element(sF36,sF39),
inference(backward_subsumption_resolution,[],[f730,f1106]) ).
fof(f1119,plain,
( sF35 = subset_complement(sK29,sF36)
| ~ element(sF35,powerset(sK29))
| ~ spl41_3 ),
inference(superposition,[],[f673,f1033]) ).
fof(f1123,plain,
( ~ element(sF35,sF39)
| sF35 = subset_complement(sK29,sF36)
| ~ spl41_3 ),
inference(forward_demodulation,[],[f1119,f554]) ).
fof(f1125,plain,
( sF35 = subset_complement(sK29,sF36)
| ~ spl41_3 ),
inference(forward_subsumption_resolution,[],[f1123,f1106]) ).
fof(f1127,plain,
subset(sF36,sK29),
inference(resolution,[],[f1107,f565]) ).
fof(f1157,plain,
( sF35 = set_difference(sK29,sF36)
| ~ element(sF36,powerset(sK29))
| ~ spl41_3 ),
inference(superposition,[],[f301,f1125]) ).
fof(f1158,plain,
( ! [X0] :
( ~ in(X0,sF35)
| ~ in(X0,sF36)
| ~ element(sF36,powerset(sK29)) )
| ~ spl41_3 ),
inference(superposition,[],[f419,f1125]) ).
fof(f1160,plain,
( sF36 = subset_complement(sK29,sF35)
| ~ element(sF36,powerset(sK29))
| ~ spl41_3 ),
inference(superposition,[],[f325,f1125]) ).
fof(f1161,plain,
( ~ element(sF36,sF39)
| sF36 = subset_complement(sK29,sF35)
| ~ spl41_3 ),
inference(forward_demodulation,[],[f1160,f554]) ).
fof(f1162,plain,
( ! [X0] :
( ~ element(sF36,sF39)
| ~ in(X0,sF35)
| ~ in(X0,sF36) )
| ~ spl41_3 ),
inference(forward_demodulation,[],[f1158,f554]) ).
fof(f1163,plain,
( ~ element(sF36,sF39)
| sF35 = set_difference(sK29,sF36)
| ~ spl41_3 ),
inference(forward_demodulation,[],[f1157,f554]) ).
fof(f1168,plain,
( sF36 = subset_complement(sK29,sF35)
| ~ spl41_3 ),
inference(forward_subsumption_resolution,[],[f1161,f1107]) ).
fof(f1169,plain,
( ! [X0] :
( ~ in(X0,sF36)
| ~ in(X0,sF35) )
| ~ spl41_3 ),
inference(forward_subsumption_resolution,[],[f1162,f1107]) ).
fof(f1170,plain,
( sF35 = set_difference(sK29,sF36)
| ~ spl41_3 ),
inference(forward_subsumption_resolution,[],[f1163,f1107]) ).
fof(f1192,definition,
( spl41_7
<=> empty_set = sK29 ),
introduced(definition,[new_symbols(definition,[spl41_7])],[avatar_definition]) ).
fof(f1193,plain,
( empty_set = sK29
| ~ spl41_7 ),
inference(avatar_component_clause,[],[f1192]) ).
fof(f1219,plain,
( sF36 = set_difference(empty_set,sF35)
| ~ spl41_3
| ~ spl41_7 ),
inference(superposition,[],[f1033,f1193]) ).
fof(f1222,plain,
( subset(sF36,empty_set)
| ~ spl41_7 ),
inference(superposition,[],[f1127,f1193]) ).
fof(f1226,plain,
( sF36 = subset_complement(empty_set,sF35)
| ~ spl41_3
| ~ spl41_7 ),
inference(superposition,[],[f1168,f1193]) ).
fof(f1230,plain,
( empty_set = sF36
| ~ spl41_3
| ~ spl41_7 ),
inference(forward_demodulation,[],[f1219,f414]) ).
fof(f1246,plain,
( sF35 = subset_complement(sK29,empty_set)
| ~ spl41_3
| ~ spl41_7 ),
inference(superposition,[],[f1125,f1230]) ).
fof(f1255,plain,
( sK29 = sF35
| ~ spl41_3
| ~ spl41_7 ),
inference(forward_demodulation,[],[f1246,f939]) ).
fof(f1256,plain,
( empty_set = sF35
| ~ spl41_3
| ~ spl41_7 ),
inference(forward_demodulation,[],[f1255,f1193]) ).
fof(f1366,plain,
( ! [X0] :
( in(X0,empty_set)
| ~ in(X0,sF36) )
| ~ spl41_7 ),
inference(resolution,[],[f1222,f279]) ).
fof(f1369,plain,
( ! [X0] : ~ in(X0,sF36)
| ~ spl41_7 ),
inference(forward_subsumption_resolution,[],[f1366,f511]) ).
fof(f1639,plain,
! [X0] :
( ~ in(X0,sK30)
| element(X0,sF39) ),
inference(resolution,[],[f866,f557]) ).
fof(f1972,plain,
( element(sF37,sF40)
| ~ element(sK30,sF40) ),
inference(superposition,[],[f568,f549]) ).
fof(f1977,plain,
( ~ element(sK30,sF40)
| spl41_6 ),
inference(forward_subsumption_resolution,[],[f1972,f1056]) ).
fof(f1979,plain,
( $false
| spl41_6 ),
inference(forward_subsumption_resolution,[],[f1977,f557]) ).
fof(f1980,plain,
spl41_6,
inference(avatar_contradiction_clause,[],[f1979]) ).
fof(f1981,plain,
element(sF37,sF40),
inference(forward_subsumption_resolution,[],[f1972,f557]) ).
fof(f1983,plain,
! [X0] :
( ~ in(X0,sF38)
| in(X0,sK29) ),
inference(backward_subsumption_resolution,[],[f1005,f1981]) ).
fof(f1989,plain,
! [X0] :
( in(sK21(sF38,X0),sK29)
| element(sF38,powerset(X0)) ),
inference(resolution,[],[f1983,f345]) ).
fof(f1993,plain,
! [X0] :
( in(sK27(X0,sF38),sK29)
| in(sK27(X0,sF38),X0)
| sF38 = X0 ),
inference(resolution,[],[f1983,f379]) ).
fof(f1994,plain,
! [X0] :
( in(sK19(X0,empty_set,sF38),sK29)
| ~ element(sF38,powerset(powerset(X0)))
| empty_set = sF38 ),
inference(resolution,[],[f1983,f807]) ).
fof(f2002,plain,
! [X0] :
( ~ in(X0,sF37)
| element(X0,sF39) ),
inference(resolution,[],[f1981,f866]) ).
fof(f2046,plain,
( ! [X0,X1] :
( ~ in(X0,sF38)
| ~ in(X1,sF37)
| in(X0,X1)
| empty_set = sF37 )
| ~ spl41_5 ),
inference(superposition,[],[f507,f1053]) ).
fof(f2047,plain,
( ! [X0,X1] :
( ~ in(X1,sF37)
| ~ in(X0,sF38)
| in(X0,X1) )
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f2046,f591]) ).
fof(f2048,plain,
( ! [X0,X1] :
( in(X0,subset_complement(sK29,X1))
| ~ in(X0,sF38)
| ~ in(X1,sK30) )
| ~ spl41_5 ),
inference(resolution,[],[f2047,f962]) ).
fof(f2062,plain,
( ! [X0,X1] :
( ~ in(X0,sF38)
| ~ in(X1,sK30)
| ~ in(X0,X1)
| ~ element(X1,powerset(sK29)) )
| ~ spl41_5 ),
inference(resolution,[],[f2048,f419]) ).
fof(f2082,plain,
( ! [X0,X1] :
( ~ element(X1,sF39)
| ~ in(X0,sF38)
| ~ in(X1,sK30)
| ~ in(X0,X1) )
| ~ spl41_5 ),
inference(forward_demodulation,[],[f2062,f554]) ).
fof(f2085,plain,
( ! [X0,X1] :
( ~ in(X1,sK30)
| ~ in(X0,sF38)
| ~ in(X0,X1) )
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f2082,f1639]) ).
fof(f2276,definition,
( spl41_14
<=> empty_set = sF38 ),
introduced(definition,[new_symbols(definition,[spl41_14])],[avatar_definition]) ).
fof(f2277,plain,
( empty_set = sF38
| ~ spl41_14 ),
inference(avatar_component_clause,[],[f2276]) ).
fof(f2282,plain,
( empty_set != sF36
| ~ spl41_14 ),
inference(superposition,[],[f552,f2277]) ).
fof(f2918,plain,
! [X0] :
( ~ in(X0,sK30)
| subset(X0,sF35) ),
inference(superposition,[],[f435,f600]) ).
fof(f2921,plain,
! [X0] :
( subset(subset_complement(sK29,X0),sF35)
| ~ in(X0,sF37) ),
inference(resolution,[],[f2918,f633]) ).
fof(f2943,plain,
! [X0,X1] :
( ~ in(X1,subset_complement(sK29,X0))
| in(X1,sF35)
| ~ in(X0,sF37) ),
inference(resolution,[],[f2921,f279]) ).
fof(f3154,plain,
( ! [X0] :
( ~ in(X0,sK29)
| in(X0,sF35)
| in(X0,sF36) )
| ~ spl41_3 ),
inference(superposition,[],[f533,f1170]) ).
fof(f3165,plain,
( ! [X0] :
( in(sK21(sF38,X0),sF35)
| in(sK21(sF38,X0),sF36)
| element(sF38,powerset(X0)) )
| ~ spl41_3 ),
inference(resolution,[],[f3154,f1989]) ).
fof(f3168,plain,
( ! [X0] :
( in(sK27(X0,sF38),sF35)
| in(sK27(X0,sF38),sF36)
| in(sK27(X0,sF38),X0)
| sF38 = X0 )
| ~ spl41_3 ),
inference(resolution,[],[f3154,f1993]) ).
fof(f3630,plain,
( ! [X0,X1] :
( ~ in(X0,union(sK30))
| ~ in(X1,sF38)
| ~ in(X1,sK16(sK30,X0)) )
| ~ spl41_5 ),
inference(resolution,[],[f532,f2085]) ).
fof(f3950,plain,
! [X0] :
( ~ in(X0,sF36)
| element(X0,sK29) ),
inference(resolution,[],[f865,f1107]) ).
fof(f4035,plain,
! [X0,X1] :
( in(X0,sF35)
| ~ in(X1,sF37)
| ~ element(X1,powerset(sK29))
| ~ element(X0,sK29)
| in(X0,X1)
| empty_set = sK29 ),
inference(resolution,[],[f2943,f418]) ).
fof(f4056,plain,
! [X0,X1] :
( ~ element(X1,sF39)
| in(X0,sF35)
| ~ in(X1,sF37)
| ~ element(X0,sK29)
| in(X0,X1)
| empty_set = sK29 ),
inference(forward_demodulation,[],[f4035,f554]) ).
fof(f4059,plain,
! [X0,X1] :
( in(X0,sF35)
| ~ in(X1,sF37)
| ~ element(X0,sK29)
| in(X0,X1)
| empty_set = sK29 ),
inference(forward_subsumption_resolution,[],[f4056,f2002]) ).
fof(f5632,definition,
( spl41_26
<=> ! [X0] :
( in(sK19(X0,empty_set,sF38),sK29)
| ~ element(sF38,powerset(powerset(X0))) ) ),
introduced(definition,[new_symbols(definition,[spl41_26])],[avatar_definition]) ).
fof(f5633,plain,
( ! [X0] :
( in(sK19(X0,empty_set,sF38),sK29)
| ~ element(sF38,powerset(powerset(X0))) )
| ~ spl41_26 ),
inference(avatar_component_clause,[],[f5632]) ).
fof(f5634,plain,
( spl41_14
| spl41_26 ),
inference(avatar_split_clause,[],[f1994,f5632,f2276]) ).
fof(f5908,plain,
( sF36 = subset_complement(empty_set,empty_set)
| ~ spl41_3
| ~ spl41_7 ),
inference(forward_demodulation,[],[f1226,f1256]) ).
fof(f5937,plain,
( empty_set = sF36
| ~ spl41_3
| ~ spl41_7 ),
inference(forward_demodulation,[],[f5908,f939]) ).
fof(f5954,plain,
( $false
| ~ spl41_3
| ~ spl41_7
| ~ spl41_14 ),
inference(forward_subsumption_resolution,[],[f5937,f2282]) ).
fof(f5955,plain,
( ~ spl41_3
| ~ spl41_7
| ~ spl41_14 ),
inference(avatar_contradiction_clause,[],[f5954]) ).
fof(f5996,plain,
( ! [X0] :
( in(sK19(X0,empty_set,sF38),empty_set)
| ~ element(sF38,powerset(powerset(X0))) )
| ~ spl41_7
| ~ spl41_26 ),
inference(forward_demodulation,[],[f5633,f1193]) ).
fof(f6007,plain,
( ! [X0] :
( in(sK21(sF38,X0),sF35)
| element(sF38,powerset(X0)) )
| ~ spl41_3
| ~ spl41_7 ),
inference(forward_subsumption_resolution,[],[f3165,f1369]) ).
fof(f6097,plain,
( ! [X0,X1] :
( ~ in(X1,sK16(sK30,X0))
| ~ in(X1,sF38)
| ~ in(X0,sF35) )
| ~ spl41_5 ),
inference(forward_demodulation,[],[f3630,f600]) ).
fof(f6174,plain,
( ! [X0] : ~ element(sF38,powerset(powerset(X0)))
| ~ spl41_7
| ~ spl41_26 ),
inference(forward_subsumption_resolution,[],[f5996,f511]) ).
fof(f6178,plain,
( ! [X0] :
( in(sK21(sF38,X0),empty_set)
| element(sF38,powerset(X0)) )
| ~ spl41_3
| ~ spl41_7 ),
inference(forward_demodulation,[],[f6007,f1256]) ).
fof(f6349,plain,
( ! [X0] : element(sF38,powerset(X0))
| ~ spl41_3
| ~ spl41_7 ),
inference(forward_subsumption_resolution,[],[f6178,f511]) ).
fof(f6410,plain,
( $false
| ~ spl41_3
| ~ spl41_7
| ~ spl41_26 ),
inference(backward_subsumption_resolution,[],[f6174,f6349]) ).
fof(f6412,plain,
( ~ spl41_3
| ~ spl41_7
| ~ spl41_26 ),
inference(avatar_contradiction_clause,[],[f6410]) ).
fof(f6602,plain,
( ! [X0] :
( ~ in(X0,sF38)
| ~ in(X0,sF35)
| ~ in(X0,union(sK30)) )
| ~ spl41_5 ),
inference(resolution,[],[f6097,f531]) ).
fof(f6633,plain,
( ! [X0] :
( ~ in(X0,sF35)
| ~ in(X0,sF38)
| ~ in(X0,sF35) )
| ~ spl41_5 ),
inference(forward_demodulation,[],[f6602,f600]) ).
fof(f6634,plain,
( ! [X0] :
( ~ in(X0,sF38)
| ~ in(X0,sF35) )
| ~ spl41_5 ),
inference(duplicate_literal_removal,[],[f6633]) ).
fof(f6646,plain,
( ! [X0] :
( ~ in(sK27(X0,sF38),sF35)
| in(sK27(X0,sF38),X0)
| sF38 = X0 )
| ~ spl41_5 ),
inference(resolution,[],[f6634,f379]) ).
fof(f6647,plain,
( ! [X0] :
( in(sK27(X0,sF38),sF36)
| in(sK27(X0,sF38),X0)
| sF38 = X0 )
| ~ spl41_3
| ~ spl41_5 ),
inference(backward_subsumption_resolution,[],[f3168,f6646]) ).
fof(f6728,plain,
( in(sK27(sF36,sF38),sF36)
| sF36 = sF38
| ~ spl41_3
| ~ spl41_5 ),
inference(factoring,[],[f6647]) ).
fof(f6729,plain,
( in(sK27(sF36,sF38),sF36)
| ~ spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f6728,f552]) ).
fof(f6730,plain,
( element(sK27(sF36,sF38),sK29)
| ~ spl41_3
| ~ spl41_5 ),
inference(resolution,[],[f6729,f3950]) ).
fof(f6731,plain,
( ~ in(sK27(sF36,sF38),sF35)
| ~ spl41_3
| ~ spl41_5 ),
inference(resolution,[],[f6729,f1169]) ).
fof(f9488,definition,
( spl41_54
<=> ! [X0,X1] :
( in(X0,sF35)
| in(X0,X1)
| ~ element(X0,sK29)
| ~ in(X1,sF37) ) ),
introduced(definition,[new_symbols(definition,[spl41_54])],[avatar_definition]) ).
fof(f9489,plain,
( ! [X0,X1] :
( ~ element(X0,sK29)
| in(X0,X1)
| in(X0,sF35)
| ~ in(X1,sF37) )
| ~ spl41_54 ),
inference(avatar_component_clause,[],[f9488]) ).
fof(f9490,plain,
( spl41_7
| spl41_54 ),
inference(avatar_split_clause,[],[f4059,f9488,f1192]) ).
fof(f9498,plain,
( ! [X0] :
( in(sK27(sF36,sF38),X0)
| in(sK27(sF36,sF38),sF35)
| ~ in(X0,sF37) )
| ~ spl41_3
| ~ spl41_5
| ~ spl41_54 ),
inference(resolution,[],[f9489,f6730]) ).
fof(f9499,plain,
( ! [X0] :
( in(sK27(sF36,sF38),X0)
| ~ in(X0,sF37) )
| ~ spl41_3
| ~ spl41_5
| ~ spl41_54 ),
inference(forward_subsumption_resolution,[],[f9498,f6731]) ).
fof(f9678,plain,
( ! [X0] :
( ~ in(sK1(X0,sK27(sF36,sF38)),sF37)
| empty_set = X0
| in(sK27(sF36,sF38),set_meet(X0)) )
| ~ spl41_3
| ~ spl41_5
| ~ spl41_54 ),
inference(resolution,[],[f9499,f505]) ).
fof(f10540,plain,
( empty_set = sF37
| in(sK27(sF36,sF38),set_meet(sF37))
| empty_set = sF37
| in(sK27(sF36,sF38),set_meet(sF37))
| ~ spl41_3
| ~ spl41_5
| ~ spl41_54 ),
inference(resolution,[],[f506,f9678]) ).
fof(f10633,plain,
( empty_set = sF37
| in(sK27(sF36,sF38),set_meet(sF37))
| ~ spl41_3
| ~ spl41_5
| ~ spl41_54 ),
inference(duplicate_literal_removal,[],[f10540]) ).
fof(f10650,plain,
( in(sK27(sF36,sF38),set_meet(sF37))
| ~ spl41_3
| ~ spl41_5
| ~ spl41_54 ),
inference(forward_subsumption_resolution,[],[f10633,f591]) ).
fof(f10659,plain,
( in(sK27(sF36,sF38),sF38)
| ~ spl41_3
| ~ spl41_5
| ~ spl41_54 ),
inference(forward_demodulation,[],[f10650,f1053]) ).
fof(f10669,plain,
( ~ in(sK27(sF36,sF38),sF36)
| sF36 = sF38
| ~ spl41_3
| ~ spl41_5
| ~ spl41_54 ),
inference(resolution,[],[f10659,f380]) ).
fof(f10680,plain,
( sF36 = sF38
| ~ spl41_3
| ~ spl41_5
| ~ spl41_54 ),
inference(forward_subsumption_resolution,[],[f10669,f6729]) ).
fof(f10681,plain,
( $false
| ~ spl41_3
| ~ spl41_5
| ~ spl41_54 ),
inference(forward_subsumption_resolution,[],[f10680,f552]) ).
fof(f10682,plain,
( ~ spl41_3
| ~ spl41_5
| ~ spl41_54 ),
inference(avatar_contradiction_clause,[],[f10681]) ).
cnf(s427,plain,
( spl41_3
| ~ spl41_4 ),
inference(sat_conversion,[],[f1037]) ).
cnf(s437,plain,
( spl41_5
| ~ spl41_6 ),
inference(sat_conversion,[],[f1057]) ).
cnf(s471,plain,
spl41_4,
inference(sat_conversion,[],[f1105]) ).
cnf(s792,plain,
spl41_6,
inference(sat_conversion,[],[f1980]) ).
cnf(s2226,plain,
( spl41_14
| spl41_26 ),
inference(sat_conversion,[],[f5634]) ).
cnf(s2372,plain,
( ~ spl41_3
| ~ spl41_7
| ~ spl41_14 ),
inference(sat_conversion,[],[f5955]) ).
cnf(s2513,plain,
( ~ spl41_3
| ~ spl41_7
| ~ spl41_26 ),
inference(sat_conversion,[],[f6412]) ).
cnf(s4253,plain,
( spl41_7
| spl41_54 ),
inference(sat_conversion,[],[f9490]) ).
cnf(s4860,plain,
( ~ spl41_3
| ~ spl41_5
| ~ spl41_54 ),
inference(sat_conversion,[],[f10682]) ).
cnf(s4867,plain,
spl41_5,
inference(rat,[],[s437,s792]) ).
cnf(s4868,plain,
spl41_3,
inference(rat,[],[s427,s471]) ).
cnf(s4869,plain,
~ spl41_54,
inference(rat,[],[s4860,s4867,s4868]) ).
cnf(s4871,plain,
spl41_7,
inference(rat,[],[s4253,s4869]) ).
cnf(s4872,plain,
~ spl41_26,
inference(rat,[],[s2513,s4868,s4871]) ).
cnf(s4875,plain,
~ spl41_14,
inference(rat,[],[s2372,s4868,s4871]) ).
cnf(s4876,plain,
$false,
inference(rat,[],[s2226,s4872,s4875]) ).
fof(f10683,plain,
$false,
inference(avatar_sat_refutation,[],[s4876]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU175+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n003.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 28 03:55:11 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/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
% 12.95/2.78 % (1169657)Detected formulas, will run a generic FOF schedule.
% 12.95/2.78 % (1169666)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1017217235:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.95/2.78 % (1169664)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=3930069604:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.95/2.78 % (1169663)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=2999129263:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.95/2.78 % (1169665)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4042535786:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.95/2.78 % (1169668)dis-21_1_sil=8000:lcm=predicate:random_seed=1612890435: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)
% 12.95/2.78 % (1169662)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=3902427058:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.95/2.78 % (1169667)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2246429997:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.95/2.78 % (1169666)Instruction limit reached!
% 12.95/2.78 % (1169666)------------------------------
% 12.95/2.78 % (1169666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.95/2.78 % (1169666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.95/2.78 % (1169666)CaDiCaL version: 2.1.3
% 12.95/2.78 % (1169666)Termination reason: Instruction limit
% 12.95/2.78 % (1169666)Termination phase: Saturation
% 12.95/2.78 % (1169666)Time elapsed: 0.041 s
% 12.95/2.78 % (1169666)Peak memory usage: 89 MB
% 12.95/2.78 % (1169666)Instructions burned: 119 (million)
% 12.95/2.78 % (1169665)Instruction limit reached!
% 12.95/2.78 % (1169665)------------------------------
% 12.95/2.78 % (1169665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.95/2.78 % (1169665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.95/2.78 % (1169665)CaDiCaL version: 2.1.3
% 12.95/2.78 % (1169665)Termination reason: Instruction limit
% 12.95/2.78 % (1169665)Termination phase: Saturation
% 12.95/2.78 % (1169665)Time elapsed: 0.072 s
% 12.95/2.78 % (1169665)Peak memory usage: 89 MB
% 12.95/2.78 % (1169665)Instructions burned: 110 (million)
% 12.95/2.78 % (1169668)Instruction limit reached!
% 12.95/2.78 % (1169668)------------------------------
% 12.95/2.78 % (1169668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.95/2.78 % (1169668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.95/2.78 % (1169668)CaDiCaL version: 2.1.3
% 12.95/2.78 % (1169668)Termination reason: Instruction limit
% 12.95/2.78 % (1169668)Termination phase: Saturation
% 12.95/2.78 % (1169668)Time elapsed: 0.082 s
% 12.95/2.78 % (1169668)Peak memory usage: 89 MB
% 12.95/2.78 % (1169668)Instructions burned: 130 (million)
% 12.95/2.78 % (1169667)Instruction limit reached!
% 12.95/2.78 % (1169667)------------------------------
% 12.95/2.78 % (1169667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.95/2.78 % (1169667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.95/2.78 % (1169667)CaDiCaL version: 2.1.3
% 12.95/2.78 % (1169667)Termination reason: Instruction limit
% 12.95/2.78 % (1169667)Termination phase: Saturation
% 12.95/2.78 % (1169667)Time elapsed: 0.101 s
% 12.95/2.78 % (1169667)Peak memory usage: 90 MB
% 12.95/2.78 % (1169667)Instructions burned: 140 (million)
% 12.95/2.78 % (1169676)lrs+10_1_sil=8000:sp=occurrence:random_seed=3660744954:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 12.95/2.78 % (1169677)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3974466494:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 12.95/2.78 % (1169676)Instruction limit reached!
% 12.95/2.78 % (1169676)------------------------------
% 12.95/2.78 % (1169676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.95/2.78 % (1169676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.95/2.78 % (1169676)CaDiCaL version: 2.1.3
% 12.95/2.78 % (1169676)Termination reason: Instruction limit
% 12.95/2.78 % (1169676)Termination phase: Saturation
% 20.00/3.78 % (1169676)Time elapsed: 0.102 s
% 20.00/3.78 % (1169676)Peak memory usage: 92 MB
% 20.00/3.78 % (1169676)Instructions burned: 287 (million)
% 20.00/3.78 % (1169678)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3481763160:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 20.00/3.78 % (1169679)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=4191948731:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 20.00/3.78 % (1169677)Instruction limit reached!
% 20.00/3.78 % (1169677)------------------------------
% 20.00/3.78 % (1169677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.00/3.78 % (1169677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.00/3.78 % (1169677)CaDiCaL version: 2.1.3
% 20.00/3.78 % (1169677)Termination reason: Instruction limit
% 20.00/3.78 % (1169677)Termination phase: Saturation
% 20.00/3.78 % (1169677)Time elapsed: 0.086 s
% 20.00/3.78 % (1169677)Peak memory usage: 91 MB
% 20.00/3.78 % (1169677)Instructions burned: 158 (million)
% 20.00/3.78 % (1169682)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=364516137:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 20.00/3.78 % (1169679)Instruction limit reached!
% 20.00/3.78 % (1169679)------------------------------
% 20.00/3.78 % (1169679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.00/3.78 % (1169679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.00/3.78 % (1169679)CaDiCaL version: 2.1.3
% 20.00/3.78 % (1169679)Termination reason: Instruction limit
% 20.00/3.78 % (1169679)Termination phase: Saturation
% 20.00/3.78 % (1169679)Time elapsed: 0.151 s
% 20.00/3.78 % (1169679)Peak memory usage: 92 MB
% 20.00/3.78 % (1169679)Instructions burned: 249 (million)
% 20.00/3.78 % (1169682)Instruction limit reached!
% 20.00/3.78 % (1169682)------------------------------
% 20.00/3.78 % (1169682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.00/3.78 % (1169682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.00/3.78 % (1169682)CaDiCaL version: 2.1.3
% 20.00/3.78 % (1169682)Termination reason: Instruction limit
% 20.00/3.78 % (1169682)Termination phase: Saturation
% 20.00/3.78 % (1169682)Time elapsed: 0.099 s
% 20.00/3.78 % (1169682)Peak memory usage: 90 MB
% 20.00/3.78 % (1169682)Instructions burned: 294 (million)
% 20.00/3.78 % (1169685)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2186765002:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 20.00/3.78 % (1169678)Instruction limit reached!
% 20.00/3.78 % (1169678)------------------------------
% 20.00/3.78 % (1169678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.00/3.78 % (1169678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.00/3.78 % (1169678)CaDiCaL version: 2.1.3
% 20.00/3.78 % (1169678)Termination reason: Instruction limit
% 20.00/3.78 % (1169678)Termination phase: Saturation
% 20.00/3.78 % (1169678)Time elapsed: 0.234 s
% 20.00/3.78 % (1169678)Peak memory usage: 92 MB
% 20.00/3.78 % (1169678)Instructions burned: 326 (million)
% 20.00/3.78 % (1169688)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3290930326:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 20.00/3.78 % (1169687)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2441246832:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 20.00/3.78 % (1169688)Instruction limit reached!
% 20.00/3.78 % (1169688)------------------------------
% 20.00/3.78 % (1169688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.00/3.78 % (1169688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.00/3.78 % (1169688)CaDiCaL version: 2.1.3
% 20.00/3.78 % (1169688)Termination reason: Instruction limit
% 20.00/3.78 % (1169688)Termination phase: Saturation
% 20.00/3.78 % (1169688)Time elapsed: 0.037 s
% 20.00/3.78 % (1169688)Peak memory usage: 89 MB
% 20.00/3.78 % (1169688)Instructions burned: 128 (million)
% 20.00/3.78 % (1169690)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=536556760:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 20.00/3.78 % (1169687)Instruction limit reached!
% 20.00/3.78 % (1169687)------------------------------
% 20.00/3.78 % (1169687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.00/3.78 % (1169687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/6.16 % (1169687)CaDiCaL version: 2.1.3
% 17.92/6.16 % (1169687)Termination reason: Instruction limit
% 17.92/6.16 % (1169687)Termination phase: Saturation
% 17.92/6.16 % (1169687)Time elapsed: 0.067 s
% 17.92/6.16 % (1169687)Peak memory usage: 89 MB
% 17.92/6.16 % (1169687)Instructions burned: 114 (million)
% 17.92/6.16 % (1169690)Instruction limit reached!
% 17.92/6.16 % (1169690)------------------------------
% 17.92/6.16 % (1169690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/6.16 % (1169690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/6.16 % (1169690)CaDiCaL version: 2.1.3
% 17.92/6.16 % (1169690)Termination reason: Instruction limit
% 17.92/6.16 % (1169690)Termination phase: Saturation
% 17.92/6.16 % (1169690)Time elapsed: 0.069 s
% 17.92/6.16 % (1169690)Peak memory usage: 89 MB
% 17.92/6.16 % (1169690)Instructions burned: 115 (million)
% 17.92/6.16 % (1169693)lrs+10_1_sil=8000:sp=occurrence:random_seed=2018607427:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 17.92/6.16 % (1169695)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4085610404:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 17.92/6.16 % (1169696)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2808172171:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 17.92/6.16 % (1169693)Instruction limit reached!
% 17.92/6.16 % (1169693)------------------------------
% 17.92/6.16 % (1169693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/6.16 % (1169693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/6.16 % (1169693)CaDiCaL version: 2.1.3
% 17.92/6.16 % (1169693)Termination reason: Instruction limit
% 17.92/6.16 % (1169693)Termination phase: Saturation
% 17.92/6.16 % (1169693)Time elapsed: 0.314 s
% 17.92/6.16 % (1169693)Peak memory usage: 99 MB
% 17.92/6.16 % (1169693)Instructions burned: 908 (million)
% 17.92/6.16 % (1169695)Instruction limit reached!
% 17.92/6.16 % (1169695)------------------------------
% 17.92/6.16 % (1169695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/6.16 % (1169695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/6.16 % (1169695)CaDiCaL version: 2.1.3
% 17.92/6.16 % (1169695)Termination reason: Instruction limit
% 17.92/6.16 % (1169695)Termination phase: Saturation
% 17.92/6.16 % (1169695)Time elapsed: 0.284 s
% 17.92/6.16 % (1169695)Peak memory usage: 92 MB
% 17.92/6.16 % (1169695)Instructions burned: 438 (million)
% 17.92/6.16 % (1169700)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=577555924:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 17.92/6.16 % (1169700)Instruction limit reached!
% 17.92/6.16 % (1169700)------------------------------
% 17.92/6.16 % (1169700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/6.16 % (1169700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/6.16 % (1169700)CaDiCaL version: 2.1.3
% 17.92/6.16 % (1169700)Termination reason: Instruction limit
% 17.92/6.16 % (1169700)Termination phase: Saturation
% 17.92/6.16 % (1169700)Time elapsed: 0.044 s
% 17.92/6.16 % (1169700)Peak memory usage: 91 MB
% 17.92/6.16 % (1169700)Instructions burned: 135 (million)
% 17.92/6.16 % (1169701)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2764218731:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 17.92/6.16 % (1169703)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3469611409:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 17.92/6.16 % (1169701)Instruction limit reached!
% 17.92/6.16 % (1169701)------------------------------
% 17.92/6.16 % (1169701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/6.16 % (1169701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/6.16 % (1169701)CaDiCaL version: 2.1.3
% 17.92/6.16 % (1169701)Termination reason: Instruction limit
% 17.92/6.16 % (1169701)Termination phase: Saturation
% 17.92/6.16 % (1169701)Time elapsed: 0.382 s
% 17.92/6.16 % (1169701)Peak memory usage: 99 MB
% 17.92/6.16 % (1169701)Instructions burned: 592 (million)
% 17.92/6.16 % (1169706)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1608499226:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/125Mi)
% 17.92/6.16 % (1169706)Instruction limit reached!
% 17.92/6.16 % (1169706)------------------------------
% 17.92/6.16 % (1169706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/6.16 % (1169706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/6.16 % (1169706)CaDiCaL version: 2.1.3
% 17.92/6.16 % (1169706)Termination reason: Instruction limit
% 17.92/6.16 % (1169706)Termination phase: Saturation
% 17.92/6.16 % (1169706)Time elapsed: 0.087 s
% 17.92/6.16 % (1169706)Peak memory usage: 90 MB
% 17.92/6.16 % (1169706)Instructions burned: 125 (million)
% 17.92/6.16 % (1169685)Instruction limit reached!
% 17.92/6.16 % (1169685)------------------------------
% 17.92/6.16 % (1169685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/6.16 % (1169685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/6.16 % (1169685)CaDiCaL version: 2.1.3
% 17.92/6.16 % (1169685)Termination reason: Instruction limit
% 17.92/6.16 % (1169685)Termination phase: Saturation
% 17.92/6.16 % (1169685)Time elapsed: 1.532 s
% 17.92/6.16 % (1169685)Peak memory usage: 142 MB
% 17.92/6.16 % (1169685)Instructions burned: 2351 (million)
% 17.92/6.16 % (1169708)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3080202785:i=134:gtgl=5:slsql=off:gtg=exists_sym_2979 on theBenchmark for (2979ds/134Mi)
% 17.92/6.16 % (1169708)Instruction limit reached!
% 17.92/6.16 % (1169708)------------------------------
% 17.92/6.16 % (1169708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/6.16 % (1169708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/6.16 % (1169708)CaDiCaL version: 2.1.3
% 17.92/6.16 % (1169708)Termination reason: Instruction limit
% 17.92/6.16 % (1169708)Termination phase: Saturation
% 17.92/6.16 % (1169708)Time elapsed: 0.092 s
% 17.92/6.16 % (1169708)Peak memory usage: 90 MB
% 17.92/6.16 % (1169708)Instructions burned: 134 (million)
% 17.92/6.16 % (1169710)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3005469461:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 17.92/6.16 % (1169711)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1502147128:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi)
% 17.92/6.16 % (1169710)Instruction limit reached!
% 17.92/6.16 % (1169710)------------------------------
% 17.92/6.16 % (1169710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/6.16 % (1169710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/6.16 % (1169710)CaDiCaL version: 2.1.3
% 17.92/6.16 % (1169710)Termination reason: Instruction limit
% 17.92/6.16 % (1169710)Termination phase: Saturation
% 17.92/6.16 % (1169710)Time elapsed: 0.090 s
% 17.92/6.16 % (1169710)Peak memory usage: 91 MB
% 17.92/6.16 % (1169710)Instructions burned: 142 (million)
% 17.92/6.16 % (1169714)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3102702683:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi)
% 17.92/6.16 % (1169711)Instruction limit reached!
% 17.92/6.16 % (1169711)------------------------------
% 17.92/6.16 % (1169711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/6.16 % (1169711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/6.16 % (1169711)CaDiCaL version: 2.1.3
% 17.92/6.16 % (1169711)Termination reason: Instruction limit
% 17.92/6.16 % (1169711)Termination phase: Saturation
% 17.92/6.16 % (1169711)Time elapsed: 0.247 s
% 17.92/6.16 % (1169711)Peak memory usage: 93 MB
% 17.92/6.16 % (1169711)Instructions burned: 431 (million)
% 17.92/6.16 % (1169716)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3201749095:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2973 on theBenchmark for (2973ds/150Mi)
% 17.92/6.16 % (1169716)Instruction limit reached!
% 17.92/6.16 % (1169716)------------------------------
% 17.92/6.16 % (1169716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/6.16 % (1169716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/6.16 % (1169716)CaDiCaL version: 2.1.3
% 17.92/6.16 % (1169716)Termination reason: Instruction limit
% 17.92/6.16 % (1169716)Termination phase: Saturation
% 17.92/6.16 % (1169716)Time elapsed: 0.101 s
% 17.92/6.16 % (1169716)Peak memory usage: 91 MB
% 17.92/6.16 % (1169716)Instructions burned: 151 (million)
% 17.92/6.16 % (1169718)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1812807558:i=14155:bd=all_2970 on theBenchmark for (2970ds/14155Mi)
% 17.92/6.16 % (1169696)Instruction limit reached!
% 17.92/6.16 % (1169696)------------------------------
% 17.92/6.16 % (1169696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/6.16 % (1169696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/6.16 % (1169696)CaDiCaL version: 2.1.3
% 17.92/6.16 % (1169696)Termination reason: Instruction limit
% 17.92/6.16 % (1169696)Termination phase: Saturation
% 17.92/6.16 % (1169696)Time elapsed: 3.338 s
% 17.92/6.16 % (1169696)Peak memory usage: 161 MB
% 17.92/6.16 % (1169696)Instructions burned: 5202 (million)
% 17.92/6.16 % (1169720)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=743234966:i=667:av=off:fsr=off_2956 on theBenchmark for (2956ds/667Mi)
% 17.92/6.16 % (1169720)Instruction limit reached!
% 17.92/6.16 % (1169720)------------------------------
% 17.92/6.16 % (1169720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/6.16 % (1169720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/6.16 % (1169720)CaDiCaL version: 2.1.3
% 17.92/6.16 % (1169720)Termination reason: Instruction limit
% 17.92/6.16 % (1169720)Termination phase: Saturation
% 17.92/6.16 % (1169720)Time elapsed: 0.348 s
% 17.92/6.16 % (1169720)Peak memory usage: 112 MB
% 17.92/6.16 % (1169720)Instructions burned: 667 (million)
% 17.92/6.16 % (1169714)First to succeed.
% 17.92/6.16 % (1169714)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1169657"
% 17.92/6.16 % (1169722)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3414356367:s2a=on:i=185:s2at=1.8:fdi=4_2951 on theBenchmark for (2951ds/185Mi)
% 17.92/6.16 % (1169722)Instruction limit reached!
% 17.92/6.16 % (1169722)------------------------------
% 17.92/6.16 % (1169722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/6.16 % (1169722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/6.16 % (1169722)CaDiCaL version: 2.1.3
% 17.92/6.16 % (1169722)Termination reason: Instruction limit
% 17.92/6.16 % (1169722)Termination phase: Saturation
% 17.92/6.16 % (1169722)Time elapsed: 0.115 s
% 17.92/6.16 % (1169722)Peak memory usage: 91 MB
% 17.92/6.16 % (1169722)Instructions burned: 186 (million)
% 17.92/6.16 % (1169714)Refutation found. Thanks to Tanya!
% 17.92/6.16 % SZS status Theorem for theBenchmark
% 17.92/6.16 % SZS output start Proof for theBenchmark
% See solution above
% 38.15/6.36 % (1169714)------------------------------
% 38.15/6.36 % (1169714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.15/6.36 % (1169714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.15/6.36 % (1169714)CaDiCaL version: 2.1.3
% 38.15/6.36 % (1169714)Termination reason: Refutation
% 38.15/6.36 % (1169714)Time elapsed: 2.440 s
% 38.15/6.36 % (1169714)Peak memory usage: 152 MB
% 38.15/6.36 % (1169714)Instructions burned: 3623 (million)
% 38.15/6.36 % (1169714)------------------------------
% 38.15/6.36 % (1169714)------------------------------
% 38.15/6.36 % (1169657)Success in time 5.306 s
% 38.15/6.36 % Vampire exiting
%------------------------------------------------------------------------------