%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET248-6 : TPTP v9.3.1. Bugfixed v2.1.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:40:36 PM UTC 2026
% Result : Unsatisfiable 12.47s 2.65s
% Output : Refutation 13.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 55
% Syntax : Number of formulae : 357 ( 57 unt; 39 def)
% Number of atoms : 804 ( 83 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 768 ( 321 ~; 418 |; 0 &)
% ( 29 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 33 ( 31 usr; 30 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 17 con; 0-3 aty)
% Number of variables : 211 ( 0 sgn 211 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( ~ member(X2,X0)
| ~ subclass(X0,X1)
| member(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_members) ).
fof(f2,axiom,
! [X0,X1] :
( member(not_subclass_element(X0,X1),X0)
| subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_members1) ).
fof(f3,axiom,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),X1)
| subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_members2) ).
fof(f4,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',class_elements_are_sets) ).
fof(f7,axiom,
! [X0,X1] :
( ~ subclass(X1,X0)
| ~ subclass(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_implies_equal) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton_set) ).
fof(f13,axiom,
! [X0,X1] : unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))) = ordered_pair(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ordered_pair) ).
fof(f14,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product1) ).
fof(f15,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product2) ).
fof(f16,axiom,
! [X2,X3,X0,X1] :
( ~ member(X0,X1)
| ~ member(X2,X3)
| member(ordered_pair(X0,X2),cross_product(X1,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product3) ).
fof(f17,axiom,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| ordered_pair(first(X0),second(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product4) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection1) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection2) ).
fof(f23,axiom,
! [X2,X0,X1] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection3) ).
fof(f28,axiom,
! [X2,X0,X1] : intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',restriction1) ).
fof(f122,negated_conjecture,
intersection(restrict(xr1,x1,y1),restrict(xr2,x2,y2)) != restrict(intersection(xr1,xr2),intersection(x1,x2),intersection(y1,y2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_restriction_preserves_intersections_1) ).
fof(f127,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),
inference(definition_unfolding,[],[f13,f12,f12]) ).
fof(f136,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| member(X0,X2) ),
inference(definition_unfolding,[],[f14,f127]) ).
fof(f137,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| member(X1,X3) ),
inference(definition_unfolding,[],[f15,f127]) ).
fof(f138,plain,
! [X2,X3,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2))),cross_product(X1,X3))
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(definition_unfolding,[],[f16,f127]) ).
fof(f139,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 ),
inference(definition_unfolding,[],[f17,f127]) ).
fof(f185,plain,
intersection(intersection(xr1,cross_product(x1,y1)),intersection(xr2,cross_product(x2,y2))) != intersection(intersection(xr1,xr2),cross_product(intersection(x1,x2),intersection(y1,y2))),
inference(definition_unfolding,[],[f122,f28,f28,f28]) ).
fof(f190,definition,
sF0 = cross_product(x1,y1),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f191,plain,
cross_product(x1,y1) = sF0,
inference(reorient_equations,[],[f190]) ).
fof(f192,definition,
sF1 = intersection(xr1,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f193,plain,
intersection(xr1,sF0) = sF1,
inference(reorient_equations,[],[f192]) ).
fof(f194,definition,
sF2 = cross_product(x2,y2),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f195,plain,
cross_product(x2,y2) = sF2,
inference(reorient_equations,[],[f194]) ).
fof(f196,definition,
sF3 = intersection(xr2,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f197,plain,
intersection(xr2,sF2) = sF3,
inference(reorient_equations,[],[f196]) ).
fof(f198,definition,
sF4 = intersection(sF1,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f199,plain,
intersection(sF1,sF3) = sF4,
inference(reorient_equations,[],[f198]) ).
fof(f200,definition,
sF5 = intersection(xr1,xr2),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f201,plain,
intersection(xr1,xr2) = sF5,
inference(reorient_equations,[],[f200]) ).
fof(f202,definition,
sF6 = intersection(x1,x2),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f203,plain,
intersection(x1,x2) = sF6,
inference(reorient_equations,[],[f202]) ).
fof(f204,definition,
sF7 = intersection(y1,y2),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f205,plain,
intersection(y1,y2) = sF7,
inference(reorient_equations,[],[f204]) ).
fof(f206,definition,
sF8 = cross_product(sF6,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f207,plain,
cross_product(sF6,sF7) = sF8,
inference(reorient_equations,[],[f206]) ).
fof(f208,definition,
sF9 = intersection(sF5,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f209,plain,
intersection(sF5,sF8) = sF9,
inference(reorient_equations,[],[f208]) ).
fof(f210,plain,
sF4 != sF9,
inference(definition_folding,[],[f185,f209,f207,f205,f203,f201,f199,f197,f195,f193,f191]) ).
fof(f211,plain,
! [X0] :
( ~ member(X0,sF1)
| member(X0,xr1) ),
inference(superposition,[],[f21,f193]) ).
fof(f212,plain,
! [X0] :
( ~ member(X0,sF5)
| member(X0,xr1) ),
inference(superposition,[],[f21,f201]) ).
fof(f213,plain,
! [X0] :
( ~ member(X0,sF3)
| member(X0,xr2) ),
inference(superposition,[],[f21,f197]) ).
fof(f214,plain,
! [X0] :
( ~ member(X0,sF4)
| member(X0,sF1) ),
inference(superposition,[],[f21,f199]) ).
fof(f215,plain,
! [X0] :
( ~ member(X0,sF9)
| member(X0,sF5) ),
inference(superposition,[],[f21,f209]) ).
fof(f216,plain,
! [X0] :
( ~ member(X0,sF7)
| member(X0,y1) ),
inference(superposition,[],[f21,f205]) ).
fof(f217,plain,
! [X0] :
( ~ member(X0,sF6)
| member(X0,x1) ),
inference(superposition,[],[f21,f203]) ).
fof(f218,plain,
! [X0] :
( ~ member(X0,sF1)
| member(X0,sF0) ),
inference(superposition,[],[f22,f193]) ).
fof(f219,plain,
! [X0] :
( ~ member(X0,sF5)
| member(X0,xr2) ),
inference(superposition,[],[f22,f201]) ).
fof(f220,plain,
! [X0] :
( ~ member(X0,sF6)
| member(X0,x2) ),
inference(superposition,[],[f22,f203]) ).
fof(f221,plain,
! [X0] :
( ~ member(X0,sF7)
| member(X0,y2) ),
inference(superposition,[],[f22,f205]) ).
fof(f222,plain,
! [X0] :
( ~ member(X0,sF3)
| member(X0,sF2) ),
inference(superposition,[],[f22,f197]) ).
fof(f223,plain,
! [X0] :
( ~ member(X0,sF4)
| member(X0,sF3) ),
inference(superposition,[],[f22,f199]) ).
fof(f224,plain,
! [X0] :
( ~ member(X0,sF9)
| member(X0,sF8) ),
inference(superposition,[],[f22,f209]) ).
fof(f227,plain,
! [X0] :
( ~ member(X0,sF0)
| member(X0,sF1)
| ~ member(X0,xr1) ),
inference(superposition,[],[f23,f193]) ).
fof(f228,plain,
! [X0] :
( ~ member(X0,xr2)
| member(X0,sF5)
| ~ member(X0,xr1) ),
inference(superposition,[],[f23,f201]) ).
fof(f229,plain,
! [X0] :
( ~ member(X0,x2)
| member(X0,sF6)
| ~ member(X0,x1) ),
inference(superposition,[],[f23,f203]) ).
fof(f230,plain,
! [X0] :
( ~ member(X0,y2)
| member(X0,sF7)
| ~ member(X0,y1) ),
inference(superposition,[],[f23,f205]) ).
fof(f231,plain,
! [X0] :
( ~ member(X0,sF2)
| member(X0,sF3)
| ~ member(X0,xr2) ),
inference(superposition,[],[f23,f197]) ).
fof(f232,plain,
! [X0] :
( ~ member(X0,sF3)
| member(X0,sF4)
| ~ member(X0,sF1) ),
inference(superposition,[],[f23,f199]) ).
fof(f243,plain,
! [X0] :
( ~ member(X0,sF8)
| unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 ),
inference(superposition,[],[f139,f207]) ).
fof(f245,plain,
! [X0] :
( ~ member(X0,sF0)
| unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 ),
inference(superposition,[],[f139,f191]) ).
fof(f246,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF8)
| member(X0,sF6) ),
inference(superposition,[],[f136,f207]) ).
fof(f247,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| member(X0,x2) ),
inference(superposition,[],[f136,f195]) ).
fof(f248,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| member(X0,x1) ),
inference(superposition,[],[f136,f191]) ).
fof(f249,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF8)
| member(X1,sF7) ),
inference(superposition,[],[f137,f207]) ).
fof(f250,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| member(X1,y2) ),
inference(superposition,[],[f137,f195]) ).
fof(f251,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| member(X1,y1) ),
inference(superposition,[],[f137,f191]) ).
fof(f253,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X1)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f2,f22]) ).
fof(f254,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X0)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f2,f21]) ).
fof(f265,plain,
! [X0] :
( member(not_subclass_element(sF4,X0),sF3)
| subclass(sF4,X0) ),
inference(resolution,[],[f2,f223]) ).
fof(f266,plain,
! [X0] :
( member(not_subclass_element(sF4,X0),sF1)
| subclass(sF4,X0) ),
inference(resolution,[],[f2,f214]) ).
fof(f274,plain,
! [X0] :
( member(not_subclass_element(sF9,X0),sF8)
| subclass(sF9,X0) ),
inference(resolution,[],[f2,f224]) ).
fof(f275,plain,
! [X0] :
( member(not_subclass_element(sF9,X0),sF5)
| subclass(sF9,X0) ),
inference(resolution,[],[f2,f215]) ).
fof(f276,plain,
! [X0] :
( member(not_subclass_element(sF4,X0),xr1)
| subclass(sF4,X0) ),
inference(resolution,[],[f266,f211]) ).
fof(f277,plain,
! [X0] :
( member(not_subclass_element(sF4,X0),sF0)
| subclass(sF4,X0) ),
inference(resolution,[],[f266,f218]) ).
fof(f279,plain,
! [X0] :
( member(not_subclass_element(sF4,X0),xr2)
| subclass(sF4,X0) ),
inference(resolution,[],[f265,f213]) ).
fof(f280,plain,
! [X0] :
( member(not_subclass_element(sF4,X0),sF2)
| subclass(sF4,X0) ),
inference(resolution,[],[f265,f222]) ).
fof(f283,plain,
! [X0] :
( subclass(sF4,X0)
| member(not_subclass_element(sF4,X0),sF5)
| ~ member(not_subclass_element(sF4,X0),xr1) ),
inference(resolution,[],[f279,f228]) ).
fof(f284,plain,
! [X0] :
( member(not_subclass_element(sF4,X0),sF5)
| subclass(sF4,X0) ),
inference(forward_subsumption_resolution,[],[f283,f276]) ).
fof(f288,plain,
! [X0] :
( member(not_subclass_element(sF9,X0),xr1)
| subclass(sF9,X0) ),
inference(resolution,[],[f275,f212]) ).
fof(f297,plain,
( subclass(sF4,sF0)
| subclass(sF4,sF0) ),
inference(resolution,[],[f3,f277]) ).
fof(f301,plain,
( subclass(sF4,sF5)
| subclass(sF4,sF5) ),
inference(resolution,[],[f3,f284]) ).
fof(f302,plain,
( subclass(sF9,sF5)
| subclass(sF9,sF5) ),
inference(resolution,[],[f3,f275]) ).
fof(f303,plain,
( subclass(sF9,sF8)
| subclass(sF9,sF8) ),
inference(resolution,[],[f3,f274]) ).
fof(f304,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,intersection(X1,X2)),X2)
| subclass(X0,intersection(X1,X2))
| ~ member(not_subclass_element(X0,intersection(X1,X2)),X1) ),
inference(resolution,[],[f3,f23]) ).
fof(f305,plain,
subclass(sF9,sF8),
inference(duplicate_literal_removal,[],[f303]) ).
fof(f306,plain,
subclass(sF9,sF5),
inference(duplicate_literal_removal,[],[f302]) ).
fof(f307,plain,
subclass(sF4,sF5),
inference(duplicate_literal_removal,[],[f301]) ).
fof(f311,plain,
subclass(sF4,sF0),
inference(duplicate_literal_removal,[],[f297]) ).
fof(f318,plain,
! [X2,X0,X1] :
( member(not_subclass_element(X0,X2),X1)
| ~ subclass(X0,X1)
| subclass(X0,X2) ),
inference(resolution,[],[f1,f2]) ).
fof(f327,plain,
! [X0,X1] :
( member(not_subclass_element(sF4,X1),X0)
| ~ subclass(sF5,X0)
| subclass(sF4,X1) ),
inference(resolution,[],[f1,f284]) ).
fof(f334,plain,
! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF8)
| ~ member(X1,sF7)
| ~ member(X0,sF6) ),
inference(superposition,[],[f138,f207]) ).
fof(f335,plain,
! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| ~ member(X1,y2)
| ~ member(X0,x2) ),
inference(superposition,[],[f138,f195]) ).
fof(f336,plain,
! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X1,y1)
| ~ member(X0,x1) ),
inference(superposition,[],[f138,f191]) ).
fof(f375,plain,
! [X0] :
( subclass(sF4,X0)
| not_subclass_element(sF4,X0) = unordered_pair(unordered_pair(first(not_subclass_element(sF4,X0)),first(not_subclass_element(sF4,X0))),unordered_pair(first(not_subclass_element(sF4,X0)),unordered_pair(second(not_subclass_element(sF4,X0)),second(not_subclass_element(sF4,X0))))) ),
inference(resolution,[],[f245,f277]) ).
fof(f378,plain,
! [X0,X1] :
( subclass(X0,intersection(X1,X0))
| ~ member(not_subclass_element(X0,intersection(X1,X0)),X1)
| subclass(X0,intersection(X1,X0)) ),
inference(resolution,[],[f304,f2]) ).
fof(f403,plain,
! [X0] :
( ~ member(not_subclass_element(X0,sF4),sF3)
| subclass(X0,sF4)
| ~ member(not_subclass_element(X0,sF4),sF1) ),
inference(superposition,[],[f304,f199]) ).
fof(f406,plain,
! [X0] :
( ~ member(not_subclass_element(X0,sF9),sF8)
| subclass(X0,sF9)
| ~ member(not_subclass_element(X0,sF9),sF5) ),
inference(superposition,[],[f304,f209]) ).
fof(f419,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,intersection(X1,X0)),X1)
| subclass(X0,intersection(X1,X0)) ),
inference(duplicate_literal_removal,[],[f378]) ).
fof(f448,plain,
! [X0] :
( subclass(sF9,X0)
| not_subclass_element(sF9,X0) = unordered_pair(unordered_pair(first(not_subclass_element(sF9,X0)),first(not_subclass_element(sF9,X0))),unordered_pair(first(not_subclass_element(sF9,X0)),unordered_pair(second(not_subclass_element(sF9,X0)),second(not_subclass_element(sF9,X0))))) ),
inference(resolution,[],[f243,f274]) ).
fof(f450,plain,
! [X0] :
( ~ subclass(X0,sF9)
| not_subclass_element(sF9,X0) = unordered_pair(unordered_pair(first(not_subclass_element(sF9,X0)),first(not_subclass_element(sF9,X0))),unordered_pair(first(not_subclass_element(sF9,X0)),unordered_pair(second(not_subclass_element(sF9,X0)),second(not_subclass_element(sF9,X0)))))
| sF9 = X0 ),
inference(resolution,[],[f448,f7]) ).
fof(f451,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X0)
| subclass(intersection(X0,X1),X0) ),
inference(resolution,[],[f254,f3]) ).
fof(f452,plain,
! [X2,X0,X1] :
( subclass(intersection(X0,X1),intersection(X2,X0))
| subclass(intersection(X0,X1),intersection(X2,X0))
| ~ member(not_subclass_element(intersection(X0,X1),intersection(X2,X0)),X2) ),
inference(resolution,[],[f254,f304]) ).
fof(f502,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(intersection(X0,X1),intersection(X2,X0)),X2)
| subclass(intersection(X0,X1),intersection(X2,X0)) ),
inference(duplicate_literal_removal,[],[f452]) ).
fof(f503,plain,
! [X0,X1] : subclass(intersection(X0,X1),X0),
inference(duplicate_literal_removal,[],[f451]) ).
fof(f504,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X1)
| subclass(intersection(X0,X1),X1) ),
inference(resolution,[],[f253,f3]) ).
fof(f510,plain,
! [X2,X3,X0,X1] :
( member(not_subclass_element(intersection(X0,intersection(X1,X2)),X3),X2)
| subclass(intersection(X0,intersection(X1,X2)),X3) ),
inference(resolution,[],[f253,f22]) ).
fof(f556,plain,
! [X0,X1] : subclass(intersection(X0,X1),X1),
inference(duplicate_literal_removal,[],[f504]) ).
fof(f564,plain,
subclass(sF5,xr1),
inference(superposition,[],[f503,f201]) ).
fof(f575,plain,
! [X0,X1] :
( ~ subclass(X0,intersection(X1,X0))
| intersection(X1,X0) = X0 ),
inference(resolution,[],[f556,f7]) ).
fof(f582,plain,
subclass(sF5,xr2),
inference(superposition,[],[f556,f201]) ).
fof(f596,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),xr1)
| ~ member(X1,x1)
| member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF1)
| ~ member(X0,y1) ),
inference(resolution,[],[f336,f227]) ).
fof(f601,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),xr2)
| ~ member(X1,x2)
| member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF3)
| ~ member(X0,y2) ),
inference(resolution,[],[f335,f231]) ).
fof(f604,plain,
! [X2,X0,X1] :
( ~ subclass(X0,X1)
| subclass(X0,intersection(X2,X1))
| subclass(X0,intersection(X2,X1))
| ~ member(not_subclass_element(X0,intersection(X2,X1)),X2) ),
inference(resolution,[],[f318,f304]) ).
fof(f637,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,intersection(X2,X1)),X2)
| subclass(X0,intersection(X2,X1))
| ~ subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f604]) ).
fof(f639,plain,
! [X0,X1] :
( subclass(X0,intersection(X0,X1))
| ~ subclass(X0,X1)
| subclass(X0,intersection(X0,X1)) ),
inference(resolution,[],[f637,f2]) ).
fof(f686,plain,
! [X0,X1] :
( subclass(X0,intersection(X0,X1))
| ~ subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f639]) ).
fof(f687,plain,
! [X0,X1] :
( ~ subclass(X0,X1)
| ~ subclass(intersection(X0,X1),X0)
| intersection(X0,X1) = X0 ),
inference(resolution,[],[f686,f7]) ).
fof(f786,plain,
! [X0,X1] :
( ~ subclass(X0,X1)
| intersection(X0,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f687,f503]) ).
fof(f787,plain,
! [X0] : intersection(X0,universal_class) = X0,
inference(resolution,[],[f786,f4]) ).
fof(f789,plain,
! [X0,X1] : intersection(X0,X1) = intersection(intersection(X0,X1),X0),
inference(resolution,[],[f786,f503]) ).
fof(f790,plain,
! [X0,X1] : intersection(X0,X1) = intersection(intersection(X0,X1),X1),
inference(resolution,[],[f786,f556]) ).
fof(f791,plain,
sF4 = intersection(sF4,sF5),
inference(resolution,[],[f786,f307]) ).
fof(f793,plain,
! [X0] :
( not_subclass_element(sF9,X0) = unordered_pair(unordered_pair(first(not_subclass_element(sF9,X0)),first(not_subclass_element(sF9,X0))),unordered_pair(first(not_subclass_element(sF9,X0)),unordered_pair(second(not_subclass_element(sF9,X0)),second(not_subclass_element(sF9,X0)))))
| sF9 = intersection(sF9,X0) ),
inference(resolution,[],[f786,f448]) ).
fof(f882,plain,
! [X0] : intersection(X0,X0) = X0,
inference(superposition,[],[f789,f787]) ).
fof(f908,plain,
! [X0] :
( ~ member(X0,sF4)
| member(X0,sF5) ),
inference(superposition,[],[f22,f791]) ).
fof(f1852,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),intersection(X1,X0))
| subclass(intersection(X0,X1),intersection(X1,X0)) ),
inference(resolution,[],[f502,f253]) ).
fof(f1934,plain,
! [X0,X1] : subclass(intersection(X0,X1),intersection(X1,X0)),
inference(duplicate_literal_removal,[],[f1852]) ).
fof(f2744,plain,
! [X2,X0,X1] :
( subclass(intersection(X0,intersection(X1,X2)),intersection(X2,X0))
| subclass(intersection(X0,intersection(X1,X2)),intersection(X2,X0)) ),
inference(resolution,[],[f510,f502]) ).
fof(f2836,plain,
! [X2,X0,X1] : subclass(intersection(X0,intersection(X1,X2)),intersection(X2,X0)),
inference(duplicate_literal_removal,[],[f2744]) ).
fof(f2925,plain,
! [X2,X0,X1] : intersection(X0,intersection(X1,X2)) = intersection(intersection(X0,intersection(X1,X2)),intersection(X2,X0)),
inference(resolution,[],[f2836,f786]) ).
fof(f3278,plain,
! [X0,X1] : intersection(X1,X0) = intersection(intersection(X1,X0),intersection(X0,X1)),
inference(superposition,[],[f2925,f882]) ).
fof(f4754,plain,
( not_subclass_element(sF9,sF4) = unordered_pair(unordered_pair(first(not_subclass_element(sF9,sF4)),first(not_subclass_element(sF9,sF4))),unordered_pair(first(not_subclass_element(sF9,sF4)),unordered_pair(second(not_subclass_element(sF9,sF4)),second(not_subclass_element(sF9,sF4)))))
| sF4 = sF9
| not_subclass_element(sF4,sF9) = unordered_pair(unordered_pair(first(not_subclass_element(sF4,sF9)),first(not_subclass_element(sF4,sF9))),unordered_pair(first(not_subclass_element(sF4,sF9)),unordered_pair(second(not_subclass_element(sF4,sF9)),second(not_subclass_element(sF4,sF9))))) ),
inference(resolution,[],[f450,f375]) ).
fof(f4758,plain,
( not_subclass_element(sF9,sF4) = unordered_pair(unordered_pair(first(not_subclass_element(sF9,sF4)),first(not_subclass_element(sF9,sF4))),unordered_pair(first(not_subclass_element(sF9,sF4)),unordered_pair(second(not_subclass_element(sF9,sF4)),second(not_subclass_element(sF9,sF4)))))
| not_subclass_element(sF4,sF9) = unordered_pair(unordered_pair(first(not_subclass_element(sF4,sF9)),first(not_subclass_element(sF4,sF9))),unordered_pair(first(not_subclass_element(sF4,sF9)),unordered_pair(second(not_subclass_element(sF4,sF9)),second(not_subclass_element(sF4,sF9))))) ),
inference(forward_subsumption_resolution,[],[f4754,f210]) ).
fof(f5928,plain,
! [X0,X1] :
( ~ subclass(intersection(X1,X0),intersection(X0,X1))
| intersection(X0,X1) = intersection(X1,X0) ),
inference(superposition,[],[f575,f3278]) ).
fof(f5975,plain,
! [X0,X1] : intersection(X0,X1) = intersection(X1,X0),
inference(forward_subsumption_resolution,[],[f5928,f1934]) ).
fof(f6166,plain,
! [X0,X1] : intersection(X1,X0) = intersection(X0,intersection(X1,X0)),
inference(superposition,[],[f790,f5975]) ).
fof(f8194,plain,
! [X0] :
( member(first(not_subclass_element(sF9,X0)),sF6)
| ~ member(not_subclass_element(sF9,X0),sF8)
| sF9 = intersection(sF9,X0) ),
inference(superposition,[],[f246,f793]) ).
fof(f8197,plain,
! [X0] :
( member(second(not_subclass_element(sF9,X0)),sF7)
| ~ member(not_subclass_element(sF9,X0),sF8)
| sF9 = intersection(sF9,X0) ),
inference(superposition,[],[f249,f793]) ).
fof(f8203,plain,
! [X0] :
( ~ member(second(not_subclass_element(sF9,X0)),y1)
| ~ member(first(not_subclass_element(sF9,X0)),x1)
| member(not_subclass_element(sF9,X0),sF1)
| ~ member(not_subclass_element(sF9,X0),xr1)
| sF9 = intersection(sF9,X0) ),
inference(superposition,[],[f596,f793]) ).
fof(f9893,plain,
! [X0] :
( member(first(not_subclass_element(sF9,X0)),x1)
| sF9 = intersection(sF9,X0)
| ~ member(not_subclass_element(sF9,X0),sF8) ),
inference(resolution,[],[f8194,f217]) ).
fof(f10581,plain,
! [X0] :
( member(second(not_subclass_element(sF9,X0)),y1)
| sF9 = intersection(sF9,X0)
| ~ member(not_subclass_element(sF9,X0),sF8) ),
inference(resolution,[],[f8197,f216]) ).
fof(f11137,plain,
! [X0] :
( ~ member(first(not_subclass_element(sF9,X0)),x1)
| member(not_subclass_element(sF9,X0),sF1)
| ~ member(not_subclass_element(sF9,X0),xr1)
| sF9 = intersection(sF9,X0)
| sF9 = intersection(sF9,X0)
| ~ member(not_subclass_element(sF9,X0),sF8) ),
inference(resolution,[],[f8203,f10581]) ).
fof(f11140,plain,
! [X0] :
( ~ member(first(not_subclass_element(sF9,X0)),x1)
| member(not_subclass_element(sF9,X0),sF1)
| ~ member(not_subclass_element(sF9,X0),xr1)
| sF9 = intersection(sF9,X0)
| ~ member(not_subclass_element(sF9,X0),sF8) ),
inference(duplicate_literal_removal,[],[f11137]) ).
fof(f11141,plain,
! [X0] :
( ~ member(not_subclass_element(sF9,X0),sF8)
| ~ member(not_subclass_element(sF9,X0),xr1)
| sF9 = intersection(sF9,X0)
| member(not_subclass_element(sF9,X0),sF1) ),
inference(forward_subsumption_resolution,[],[f11140,f9893]) ).
fof(f11142,plain,
! [X0] :
( ~ member(not_subclass_element(sF9,X0),xr1)
| sF9 = intersection(sF9,X0)
| member(not_subclass_element(sF9,X0),sF1)
| subclass(sF9,X0) ),
inference(resolution,[],[f11141,f274]) ).
fof(f11145,plain,
! [X0] :
( ~ member(not_subclass_element(sF9,X0),xr1)
| sF9 = intersection(sF9,X0)
| member(not_subclass_element(sF9,X0),sF1) ),
inference(forward_subsumption_resolution,[],[f11142,f786]) ).
fof(f11147,plain,
! [X0] :
( sF9 = intersection(sF9,X0)
| member(not_subclass_element(sF9,X0),sF1)
| subclass(sF9,X0) ),
inference(resolution,[],[f11145,f288]) ).
fof(f11150,plain,
! [X0] :
( member(not_subclass_element(sF9,X0),sF1)
| sF9 = intersection(sF9,X0) ),
inference(forward_subsumption_resolution,[],[f11147,f786]) ).
fof(f11158,plain,
! [X0] :
( member(not_subclass_element(sF9,X0),sF0)
| sF9 = intersection(sF9,X0) ),
inference(resolution,[],[f11150,f218]) ).
fof(f11289,plain,
( sF9 = intersection(sF9,intersection(sF0,sF9))
| subclass(sF9,intersection(sF0,sF9)) ),
inference(resolution,[],[f11158,f419]) ).
fof(f11296,plain,
sF9 = intersection(sF9,intersection(sF0,sF9)),
inference(forward_subsumption_resolution,[],[f11289,f786]) ).
fof(f11299,plain,
sF9 = intersection(sF0,sF9),
inference(forward_demodulation,[],[f11296,f6166]) ).
fof(f11324,plain,
subclass(sF9,sF0),
inference(superposition,[],[f503,f11299]) ).
fof(f13204,definition,
( spl10_213
<=> not_subclass_element(sF4,sF9) = unordered_pair(unordered_pair(first(not_subclass_element(sF4,sF9)),first(not_subclass_element(sF4,sF9))),unordered_pair(first(not_subclass_element(sF4,sF9)),unordered_pair(second(not_subclass_element(sF4,sF9)),second(not_subclass_element(sF4,sF9))))) ),
introduced(definition,[new_symbols(definition,[spl10_213])],[avatar_definition]) ).
fof(f13205,plain,
( not_subclass_element(sF4,sF9) != unordered_pair(unordered_pair(first(not_subclass_element(sF4,sF9)),first(not_subclass_element(sF4,sF9))),unordered_pair(first(not_subclass_element(sF4,sF9)),unordered_pair(second(not_subclass_element(sF4,sF9)),second(not_subclass_element(sF4,sF9)))))
| spl10_213 ),
inference(avatar_component_clause,[],[f13204]) ).
fof(f13206,plain,
( not_subclass_element(sF4,sF9) = unordered_pair(unordered_pair(first(not_subclass_element(sF4,sF9)),first(not_subclass_element(sF4,sF9))),unordered_pair(first(not_subclass_element(sF4,sF9)),unordered_pair(second(not_subclass_element(sF4,sF9)),second(not_subclass_element(sF4,sF9)))))
| ~ spl10_213 ),
inference(avatar_component_clause,[],[f13204]) ).
fof(f13208,definition,
( spl10_214
<=> not_subclass_element(sF9,sF4) = unordered_pair(unordered_pair(first(not_subclass_element(sF9,sF4)),first(not_subclass_element(sF9,sF4))),unordered_pair(first(not_subclass_element(sF9,sF4)),unordered_pair(second(not_subclass_element(sF9,sF4)),second(not_subclass_element(sF9,sF4))))) ),
introduced(definition,[new_symbols(definition,[spl10_214])],[avatar_definition]) ).
fof(f13209,plain,
( not_subclass_element(sF9,sF4) != unordered_pair(unordered_pair(first(not_subclass_element(sF9,sF4)),first(not_subclass_element(sF9,sF4))),unordered_pair(first(not_subclass_element(sF9,sF4)),unordered_pair(second(not_subclass_element(sF9,sF4)),second(not_subclass_element(sF9,sF4)))))
| spl10_214 ),
inference(avatar_component_clause,[],[f13208]) ).
fof(f13210,plain,
( not_subclass_element(sF9,sF4) = unordered_pair(unordered_pair(first(not_subclass_element(sF9,sF4)),first(not_subclass_element(sF9,sF4))),unordered_pair(first(not_subclass_element(sF9,sF4)),unordered_pair(second(not_subclass_element(sF9,sF4)),second(not_subclass_element(sF9,sF4)))))
| ~ spl10_214 ),
inference(avatar_component_clause,[],[f13208]) ).
fof(f13211,plain,
( spl10_213
| spl10_214 ),
inference(avatar_split_clause,[],[f4758,f13208,f13204]) ).
fof(f13237,definition,
( spl10_217
<=> subclass(sF9,sF4) ),
introduced(definition,[new_symbols(definition,[spl10_217])],[avatar_definition]) ).
fof(f13238,plain,
( ~ subclass(sF9,sF4)
| spl10_217 ),
inference(avatar_component_clause,[],[f13237]) ).
fof(f13239,plain,
( subclass(sF9,sF4)
| ~ spl10_217 ),
inference(avatar_component_clause,[],[f13237]) ).
fof(f13347,definition,
( spl10_241
<=> member(not_subclass_element(sF4,sF9),sF5) ),
introduced(definition,[new_symbols(definition,[spl10_241])],[avatar_definition]) ).
fof(f13348,plain,
( member(not_subclass_element(sF4,sF9),sF5)
| ~ spl10_241 ),
inference(avatar_component_clause,[],[f13347]) ).
fof(f13349,plain,
( ~ member(not_subclass_element(sF4,sF9),sF5)
| spl10_241 ),
inference(avatar_component_clause,[],[f13347]) ).
fof(f13396,plain,
( ~ member(not_subclass_element(sF4,sF9),sF2)
| member(first(not_subclass_element(sF4,sF9)),x2)
| ~ spl10_213 ),
inference(superposition,[],[f247,f13206]) ).
fof(f13397,plain,
( ~ member(not_subclass_element(sF4,sF9),sF0)
| member(first(not_subclass_element(sF4,sF9)),x1)
| ~ spl10_213 ),
inference(superposition,[],[f248,f13206]) ).
fof(f13399,plain,
( ~ member(not_subclass_element(sF4,sF9),sF2)
| member(second(not_subclass_element(sF4,sF9)),y2)
| ~ spl10_213 ),
inference(superposition,[],[f250,f13206]) ).
fof(f13400,plain,
( ~ member(not_subclass_element(sF4,sF9),sF0)
| member(second(not_subclass_element(sF4,sF9)),y1)
| ~ spl10_213 ),
inference(superposition,[],[f251,f13206]) ).
fof(f13401,plain,
( member(not_subclass_element(sF4,sF9),sF8)
| ~ member(second(not_subclass_element(sF4,sF9)),sF7)
| ~ member(first(not_subclass_element(sF4,sF9)),sF6)
| ~ spl10_213 ),
inference(superposition,[],[f334,f13206]) ).
fof(f13411,definition,
( spl10_250
<=> member(second(not_subclass_element(sF4,sF9)),y2) ),
introduced(definition,[new_symbols(definition,[spl10_250])],[avatar_definition]) ).
fof(f13412,plain,
( member(second(not_subclass_element(sF4,sF9)),y2)
| ~ spl10_250 ),
inference(avatar_component_clause,[],[f13411]) ).
fof(f13415,definition,
( spl10_251
<=> member(not_subclass_element(sF4,sF9),sF3) ),
introduced(definition,[new_symbols(definition,[spl10_251])],[avatar_definition]) ).
fof(f13417,plain,
( member(not_subclass_element(sF4,sF9),sF3)
| ~ spl10_251 ),
inference(avatar_component_clause,[],[f13415]) ).
fof(f13419,definition,
( spl10_252
<=> member(first(not_subclass_element(sF4,sF9)),x2) ),
introduced(definition,[new_symbols(definition,[spl10_252])],[avatar_definition]) ).
fof(f13420,plain,
( member(first(not_subclass_element(sF4,sF9)),x2)
| ~ spl10_252 ),
inference(avatar_component_clause,[],[f13419]) ).
fof(f13423,definition,
( spl10_253
<=> member(not_subclass_element(sF4,sF9),xr2) ),
introduced(definition,[new_symbols(definition,[spl10_253])],[avatar_definition]) ).
fof(f13425,plain,
( ~ member(not_subclass_element(sF4,sF9),xr2)
| spl10_253 ),
inference(avatar_component_clause,[],[f13423]) ).
fof(f13428,definition,
( spl10_254
<=> member(second(not_subclass_element(sF4,sF9)),y1) ),
introduced(definition,[new_symbols(definition,[spl10_254])],[avatar_definition]) ).
fof(f13429,plain,
( member(second(not_subclass_element(sF4,sF9)),y1)
| ~ spl10_254 ),
inference(avatar_component_clause,[],[f13428]) ).
fof(f13432,definition,
( spl10_255
<=> member(not_subclass_element(sF4,sF9),sF1) ),
introduced(definition,[new_symbols(definition,[spl10_255])],[avatar_definition]) ).
fof(f13434,plain,
( member(not_subclass_element(sF4,sF9),sF1)
| ~ spl10_255 ),
inference(avatar_component_clause,[],[f13432]) ).
fof(f13436,definition,
( spl10_256
<=> member(first(not_subclass_element(sF4,sF9)),x1) ),
introduced(definition,[new_symbols(definition,[spl10_256])],[avatar_definition]) ).
fof(f13437,plain,
( member(first(not_subclass_element(sF4,sF9)),x1)
| ~ spl10_256 ),
inference(avatar_component_clause,[],[f13436]) ).
fof(f13440,definition,
( spl10_257
<=> member(not_subclass_element(sF4,sF9),xr1) ),
introduced(definition,[new_symbols(definition,[spl10_257])],[avatar_definition]) ).
fof(f13442,plain,
( ~ member(not_subclass_element(sF4,sF9),xr1)
| spl10_257 ),
inference(avatar_component_clause,[],[f13440]) ).
fof(f13445,definition,
( spl10_258
<=> member(not_subclass_element(sF4,sF9),sF0) ),
introduced(definition,[new_symbols(definition,[spl10_258])],[avatar_definition]) ).
fof(f13446,plain,
( ~ member(not_subclass_element(sF4,sF9),sF0)
| spl10_258 ),
inference(avatar_component_clause,[],[f13445]) ).
fof(f13447,plain,
( member(not_subclass_element(sF4,sF9),sF0)
| ~ spl10_258 ),
inference(avatar_component_clause,[],[f13445]) ).
fof(f13450,definition,
( spl10_259
<=> member(not_subclass_element(sF4,sF9),sF2) ),
introduced(definition,[new_symbols(definition,[spl10_259])],[avatar_definition]) ).
fof(f13451,plain,
( ~ member(not_subclass_element(sF4,sF9),sF2)
| spl10_259 ),
inference(avatar_component_clause,[],[f13450]) ).
fof(f13452,plain,
( member(not_subclass_element(sF4,sF9),sF2)
| ~ spl10_259 ),
inference(avatar_component_clause,[],[f13450]) ).
fof(f13455,definition,
( spl10_260
<=> member(first(not_subclass_element(sF4,sF9)),sF6) ),
introduced(definition,[new_symbols(definition,[spl10_260])],[avatar_definition]) ).
fof(f13459,definition,
( spl10_261
<=> member(second(not_subclass_element(sF4,sF9)),sF7) ),
introduced(definition,[new_symbols(definition,[spl10_261])],[avatar_definition]) ).
fof(f13461,plain,
( ~ member(second(not_subclass_element(sF4,sF9)),sF7)
| spl10_261 ),
inference(avatar_component_clause,[],[f13459]) ).
fof(f13463,definition,
( spl10_262
<=> member(not_subclass_element(sF4,sF9),sF8) ),
introduced(definition,[new_symbols(definition,[spl10_262])],[avatar_definition]) ).
fof(f13465,plain,
( member(not_subclass_element(sF4,sF9),sF8)
| ~ spl10_262 ),
inference(avatar_component_clause,[],[f13463]) ).
fof(f13466,plain,
( ~ spl10_260
| ~ spl10_261
| spl10_262
| ~ spl10_213 ),
inference(avatar_split_clause,[],[f13401,f13204,f13463,f13459,f13455]) ).
fof(f13467,plain,
( spl10_254
| ~ spl10_258
| ~ spl10_213 ),
inference(avatar_split_clause,[],[f13400,f13204,f13445,f13428]) ).
fof(f13468,plain,
( spl10_250
| ~ spl10_259
| ~ spl10_213 ),
inference(avatar_split_clause,[],[f13399,f13204,f13450,f13411]) ).
fof(f13470,plain,
( spl10_256
| ~ spl10_258
| ~ spl10_213 ),
inference(avatar_split_clause,[],[f13397,f13204,f13445,f13436]) ).
fof(f13471,plain,
( spl10_252
| ~ spl10_259
| ~ spl10_213 ),
inference(avatar_split_clause,[],[f13396,f13204,f13450,f13419]) ).
fof(f13481,definition,
( spl10_263
<=> subclass(sF4,sF9) ),
introduced(definition,[new_symbols(definition,[spl10_263])],[avatar_definition]) ).
fof(f13482,plain,
( ~ subclass(sF4,sF9)
| spl10_263 ),
inference(avatar_component_clause,[],[f13481]) ).
fof(f13483,plain,
( subclass(sF4,sF9)
| ~ spl10_263 ),
inference(avatar_component_clause,[],[f13481]) ).
fof(f13495,plain,
( ~ member(not_subclass_element(sF9,sF4),sF8)
| member(first(not_subclass_element(sF9,sF4)),sF6)
| ~ spl10_214 ),
inference(superposition,[],[f246,f13210]) ).
fof(f13498,plain,
( ~ member(not_subclass_element(sF9,sF4),sF8)
| member(second(not_subclass_element(sF9,sF4)),sF7)
| ~ spl10_214 ),
inference(superposition,[],[f249,f13210]) ).
fof(f13505,plain,
( ~ member(not_subclass_element(sF9,sF4),xr2)
| ~ member(first(not_subclass_element(sF9,sF4)),x2)
| member(not_subclass_element(sF9,sF4),sF3)
| ~ member(second(not_subclass_element(sF9,sF4)),y2)
| ~ spl10_214 ),
inference(superposition,[],[f601,f13210]) ).
fof(f13511,definition,
( spl10_266
<=> member(second(not_subclass_element(sF9,sF4)),sF7) ),
introduced(definition,[new_symbols(definition,[spl10_266])],[avatar_definition]) ).
fof(f13512,plain,
( member(second(not_subclass_element(sF9,sF4)),sF7)
| ~ spl10_266 ),
inference(avatar_component_clause,[],[f13511]) ).
fof(f13519,definition,
( spl10_268
<=> member(first(not_subclass_element(sF9,sF4)),sF6) ),
introduced(definition,[new_symbols(definition,[spl10_268])],[avatar_definition]) ).
fof(f13520,plain,
( member(first(not_subclass_element(sF9,sF4)),sF6)
| ~ spl10_268 ),
inference(avatar_component_clause,[],[f13519]) ).
fof(f13523,definition,
( spl10_269
<=> member(not_subclass_element(sF9,sF4),sF5) ),
introduced(definition,[new_symbols(definition,[spl10_269])],[avatar_definition]) ).
fof(f13524,plain,
( member(not_subclass_element(sF9,sF4),sF5)
| ~ spl10_269 ),
inference(avatar_component_clause,[],[f13523]) ).
fof(f13525,plain,
( ~ member(not_subclass_element(sF9,sF4),sF5)
| spl10_269 ),
inference(avatar_component_clause,[],[f13523]) ).
fof(f13528,definition,
( spl10_270
<=> member(second(not_subclass_element(sF9,sF4)),y2) ),
introduced(definition,[new_symbols(definition,[spl10_270])],[avatar_definition]) ).
fof(f13530,plain,
( ~ member(second(not_subclass_element(sF9,sF4)),y2)
| spl10_270 ),
inference(avatar_component_clause,[],[f13528]) ).
fof(f13532,definition,
( spl10_271
<=> member(not_subclass_element(sF9,sF4),sF3) ),
introduced(definition,[new_symbols(definition,[spl10_271])],[avatar_definition]) ).
fof(f13534,plain,
( member(not_subclass_element(sF9,sF4),sF3)
| ~ spl10_271 ),
inference(avatar_component_clause,[],[f13532]) ).
fof(f13536,definition,
( spl10_272
<=> member(first(not_subclass_element(sF9,sF4)),x2) ),
introduced(definition,[new_symbols(definition,[spl10_272])],[avatar_definition]) ).
fof(f13540,definition,
( spl10_273
<=> member(not_subclass_element(sF9,sF4),xr2) ),
introduced(definition,[new_symbols(definition,[spl10_273])],[avatar_definition]) ).
fof(f13542,plain,
( ~ member(not_subclass_element(sF9,sF4),xr2)
| spl10_273 ),
inference(avatar_component_clause,[],[f13540]) ).
fof(f13543,plain,
( ~ spl10_270
| spl10_271
| ~ spl10_272
| ~ spl10_273
| ~ spl10_214 ),
inference(avatar_split_clause,[],[f13505,f13208,f13540,f13536,f13532,f13528]) ).
fof(f13549,definition,
( spl10_275
<=> member(not_subclass_element(sF9,sF4),sF1) ),
introduced(definition,[new_symbols(definition,[spl10_275])],[avatar_definition]) ).
fof(f13550,plain,
( ~ member(not_subclass_element(sF9,sF4),sF1)
| spl10_275 ),
inference(avatar_component_clause,[],[f13549]) ).
fof(f13551,plain,
( member(not_subclass_element(sF9,sF4),sF1)
| ~ spl10_275 ),
inference(avatar_component_clause,[],[f13549]) ).
fof(f13557,definition,
( spl10_277
<=> member(not_subclass_element(sF9,sF4),xr1) ),
introduced(definition,[new_symbols(definition,[spl10_277])],[avatar_definition]) ).
fof(f13558,plain,
( member(not_subclass_element(sF9,sF4),xr1)
| ~ spl10_277 ),
inference(avatar_component_clause,[],[f13557]) ).
fof(f13559,plain,
( ~ member(not_subclass_element(sF9,sF4),xr1)
| spl10_277 ),
inference(avatar_component_clause,[],[f13557]) ).
fof(f13562,definition,
( spl10_278
<=> member(not_subclass_element(sF9,sF4),sF0) ),
introduced(definition,[new_symbols(definition,[spl10_278])],[avatar_definition]) ).
fof(f13563,plain,
( ~ member(not_subclass_element(sF9,sF4),sF0)
| spl10_278 ),
inference(avatar_component_clause,[],[f13562]) ).
fof(f13564,plain,
( member(not_subclass_element(sF9,sF4),sF0)
| ~ spl10_278 ),
inference(avatar_component_clause,[],[f13562]) ).
fof(f13572,definition,
( spl10_280
<=> member(not_subclass_element(sF9,sF4),sF8) ),
introduced(definition,[new_symbols(definition,[spl10_280])],[avatar_definition]) ).
fof(f13573,plain,
( ~ member(not_subclass_element(sF9,sF4),sF8)
| spl10_280 ),
inference(avatar_component_clause,[],[f13572]) ).
fof(f13574,plain,
( member(not_subclass_element(sF9,sF4),sF8)
| ~ spl10_280 ),
inference(avatar_component_clause,[],[f13572]) ).
fof(f13578,plain,
( spl10_266
| ~ spl10_280
| ~ spl10_214 ),
inference(avatar_split_clause,[],[f13498,f13208,f13572,f13511]) ).
fof(f13581,plain,
( spl10_268
| ~ spl10_280
| ~ spl10_214 ),
inference(avatar_split_clause,[],[f13495,f13208,f13572,f13519]) ).
fof(f13724,plain,
( ~ subclass(sF9,sF0)
| subclass(sF9,sF4)
| spl10_278 ),
inference(resolution,[],[f13563,f318]) ).
fof(f13727,plain,
( ~ subclass(sF4,sF0)
| subclass(sF4,sF9)
| spl10_258 ),
inference(resolution,[],[f13446,f318]) ).
fof(f13730,plain,
( ~ subclass(sF9,sF8)
| subclass(sF9,sF4)
| spl10_280 ),
inference(resolution,[],[f13573,f318]) ).
fof(f13737,plain,
( subclass(sF4,sF9)
| spl10_259 ),
inference(resolution,[],[f13451,f280]) ).
fof(f13747,plain,
( ~ subclass(sF4,sF9)
| sF4 = sF9
| ~ spl10_217 ),
inference(resolution,[],[f13239,f7]) ).
fof(f13748,plain,
( sF4 = sF9
| ~ spl10_217
| ~ spl10_263 ),
inference(forward_subsumption_resolution,[],[f13747,f13483]) ).
fof(f13751,plain,
( $false
| ~ spl10_217
| ~ spl10_263 ),
inference(forward_subsumption_resolution,[],[f13748,f210]) ).
fof(f13752,plain,
( ~ spl10_217
| ~ spl10_263 ),
inference(avatar_contradiction_clause,[],[f13751]) ).
fof(f13753,plain,
( subclass(sF4,sF9)
| spl10_258 ),
inference(forward_subsumption_resolution,[],[f13727,f311]) ).
fof(f13761,plain,
( $false
| spl10_258
| spl10_263 ),
inference(forward_subsumption_resolution,[],[f13753,f13482]) ).
fof(f13762,plain,
( spl10_258
| spl10_263 ),
inference(avatar_contradiction_clause,[],[f13761]) ).
fof(f13769,plain,
( member(not_subclass_element(sF4,sF9),sF3)
| ~ member(not_subclass_element(sF4,sF9),xr2)
| ~ spl10_259 ),
inference(resolution,[],[f13452,f231]) ).
fof(f13773,plain,
( ~ spl10_253
| spl10_251
| ~ spl10_259 ),
inference(avatar_split_clause,[],[f13769,f13450,f13415,f13423]) ).
fof(f13776,plain,
( spl10_263
| spl10_259 ),
inference(avatar_split_clause,[],[f13737,f13450,f13481]) ).
fof(f13778,plain,
( subclass(sF9,sF4)
| spl10_278 ),
inference(forward_subsumption_resolution,[],[f13724,f11324]) ).
fof(f13781,plain,
( subclass(sF9,sF4)
| spl10_280 ),
inference(forward_subsumption_resolution,[],[f13730,f305]) ).
fof(f13784,plain,
( $false
| spl10_217
| spl10_278 ),
inference(forward_subsumption_resolution,[],[f13778,f13238]) ).
fof(f13785,plain,
( spl10_217
| spl10_278 ),
inference(avatar_contradiction_clause,[],[f13784]) ).
fof(f13786,plain,
( $false
| spl10_217
| spl10_280 ),
inference(forward_subsumption_resolution,[],[f13781,f13238]) ).
fof(f13787,plain,
( spl10_217
| spl10_280 ),
inference(avatar_contradiction_clause,[],[f13786]) ).
fof(f13788,plain,
( member(first(not_subclass_element(sF9,sF4)),x2)
| ~ spl10_268 ),
inference(resolution,[],[f13520,f220]) ).
fof(f13792,plain,
( spl10_272
| ~ spl10_268 ),
inference(avatar_split_clause,[],[f13788,f13519,f13536]) ).
fof(f13795,plain,
( member(second(not_subclass_element(sF9,sF4)),y2)
| ~ spl10_266 ),
inference(resolution,[],[f13512,f221]) ).
fof(f13798,plain,
( $false
| ~ spl10_266
| spl10_270 ),
inference(forward_subsumption_resolution,[],[f13795,f13530]) ).
fof(f13799,plain,
( ~ spl10_266
| spl10_270 ),
inference(avatar_contradiction_clause,[],[f13798]) ).
fof(f13812,plain,
( not_subclass_element(sF4,sF9) = unordered_pair(unordered_pair(first(not_subclass_element(sF4,sF9)),first(not_subclass_element(sF4,sF9))),unordered_pair(first(not_subclass_element(sF4,sF9)),unordered_pair(second(not_subclass_element(sF4,sF9)),second(not_subclass_element(sF4,sF9)))))
| ~ spl10_258 ),
inference(resolution,[],[f13447,f245]) ).
fof(f13813,plain,
( member(not_subclass_element(sF4,sF9),sF1)
| ~ member(not_subclass_element(sF4,sF9),xr1)
| ~ spl10_258 ),
inference(resolution,[],[f13447,f227]) ).
fof(f13817,plain,
( ~ spl10_257
| spl10_255
| ~ spl10_258 ),
inference(avatar_split_clause,[],[f13813,f13445,f13432,f13440]) ).
fof(f13818,plain,
( $false
| spl10_213
| ~ spl10_258 ),
inference(forward_subsumption_resolution,[],[f13812,f13205]) ).
fof(f13819,plain,
( spl10_213
| ~ spl10_258 ),
inference(avatar_contradiction_clause,[],[f13818]) ).
fof(f13821,plain,
( member(not_subclass_element(sF9,sF4),sF1)
| ~ member(not_subclass_element(sF9,sF4),xr1)
| ~ spl10_278 ),
inference(resolution,[],[f13564,f227]) ).
fof(f13825,plain,
( not_subclass_element(sF9,sF4) = unordered_pair(unordered_pair(first(not_subclass_element(sF9,sF4)),first(not_subclass_element(sF9,sF4))),unordered_pair(first(not_subclass_element(sF9,sF4)),unordered_pair(second(not_subclass_element(sF9,sF4)),second(not_subclass_element(sF9,sF4)))))
| ~ spl10_280 ),
inference(resolution,[],[f13574,f243]) ).
fof(f13839,plain,
( ~ subclass(sF9,sF5)
| subclass(sF9,sF4)
| spl10_269 ),
inference(resolution,[],[f13525,f318]) ).
fof(f13840,plain,
( subclass(sF9,sF4)
| spl10_269 ),
inference(forward_subsumption_resolution,[],[f13839,f306]) ).
fof(f13843,plain,
( $false
| spl10_217
| spl10_269 ),
inference(forward_subsumption_resolution,[],[f13840,f13238]) ).
fof(f13844,plain,
( spl10_217
| spl10_269 ),
inference(avatar_contradiction_clause,[],[f13843]) ).
fof(f13846,plain,
( member(not_subclass_element(sF9,sF4),xr2)
| ~ spl10_269 ),
inference(resolution,[],[f13524,f219]) ).
fof(f13847,plain,
( member(not_subclass_element(sF9,sF4),xr1)
| ~ spl10_269 ),
inference(resolution,[],[f13524,f212]) ).
fof(f13850,plain,
( $false
| ~ spl10_269
| spl10_277 ),
inference(forward_subsumption_resolution,[],[f13847,f13559]) ).
fof(f13851,plain,
( ~ spl10_269
| spl10_277 ),
inference(avatar_contradiction_clause,[],[f13850]) ).
fof(f13852,plain,
( $false
| ~ spl10_269
| spl10_273 ),
inference(forward_subsumption_resolution,[],[f13846,f13542]) ).
fof(f13853,plain,
( ~ spl10_269
| spl10_273 ),
inference(avatar_contradiction_clause,[],[f13852]) ).
fof(f13854,plain,
( subclass(sF9,sF4)
| ~ member(not_subclass_element(sF9,sF4),sF1)
| ~ spl10_271 ),
inference(resolution,[],[f13534,f403]) ).
fof(f13861,plain,
( ~ member(not_subclass_element(sF9,sF4),sF1)
| spl10_217
| ~ spl10_271 ),
inference(forward_subsumption_resolution,[],[f13854,f13238]) ).
fof(f13862,plain,
( $false
| spl10_217
| ~ spl10_271
| ~ spl10_275 ),
inference(forward_subsumption_resolution,[],[f13861,f13551]) ).
fof(f13863,plain,
( spl10_217
| ~ spl10_271
| ~ spl10_275 ),
inference(avatar_contradiction_clause,[],[f13862]) ).
fof(f13866,plain,
( ~ member(not_subclass_element(sF9,sF4),xr1)
| spl10_275
| ~ spl10_278 ),
inference(forward_subsumption_resolution,[],[f13821,f13550]) ).
fof(f13871,plain,
( $false
| spl10_214
| ~ spl10_280 ),
inference(forward_subsumption_resolution,[],[f13825,f13209]) ).
fof(f13872,plain,
( spl10_214
| ~ spl10_280 ),
inference(avatar_contradiction_clause,[],[f13871]) ).
fof(f13873,plain,
( $false
| spl10_275
| ~ spl10_277
| ~ spl10_278 ),
inference(forward_subsumption_resolution,[],[f13866,f13558]) ).
fof(f13874,plain,
( spl10_275
| ~ spl10_277
| ~ spl10_278 ),
inference(avatar_contradiction_clause,[],[f13873]) ).
fof(f13905,plain,
( member(first(not_subclass_element(sF4,sF9)),sF6)
| ~ member(first(not_subclass_element(sF4,sF9)),x1)
| ~ spl10_252 ),
inference(resolution,[],[f13420,f229]) ).
fof(f13908,plain,
( member(first(not_subclass_element(sF4,sF9)),sF6)
| ~ spl10_252
| ~ spl10_256 ),
inference(forward_subsumption_resolution,[],[f13905,f13437]) ).
fof(f13909,plain,
( spl10_260
| ~ spl10_252
| ~ spl10_256 ),
inference(avatar_split_clause,[],[f13908,f13436,f13419,f13455]) ).
fof(f13945,plain,
( member(second(not_subclass_element(sF4,sF9)),sF7)
| ~ member(second(not_subclass_element(sF4,sF9)),y1)
| ~ spl10_250 ),
inference(resolution,[],[f13412,f230]) ).
fof(f13948,plain,
( ~ member(second(not_subclass_element(sF4,sF9)),y1)
| ~ spl10_250
| spl10_261 ),
inference(forward_subsumption_resolution,[],[f13945,f13461]) ).
fof(f13949,plain,
( $false
| ~ spl10_250
| ~ spl10_254
| spl10_261 ),
inference(forward_subsumption_resolution,[],[f13948,f13429]) ).
fof(f13950,plain,
( ~ spl10_250
| ~ spl10_254
| spl10_261 ),
inference(avatar_contradiction_clause,[],[f13949]) ).
fof(f13953,plain,
( subclass(sF4,sF9)
| ~ member(not_subclass_element(sF4,sF9),sF5)
| ~ spl10_262 ),
inference(resolution,[],[f13465,f406]) ).
fof(f13995,plain,
( ~ subclass(sF5,xr1)
| subclass(sF4,sF9)
| spl10_257 ),
inference(resolution,[],[f13442,f327]) ).
fof(f13998,plain,
( subclass(sF4,sF9)
| spl10_257 ),
inference(forward_subsumption_resolution,[],[f13995,f564]) ).
fof(f14003,plain,
( $false
| spl10_257
| spl10_263 ),
inference(forward_subsumption_resolution,[],[f13998,f13482]) ).
fof(f14004,plain,
( spl10_257
| spl10_263 ),
inference(avatar_contradiction_clause,[],[f14003]) ).
fof(f14014,plain,
( ~ subclass(sF5,xr2)
| subclass(sF4,sF9)
| spl10_253 ),
inference(resolution,[],[f13425,f327]) ).
fof(f14017,plain,
( subclass(sF4,sF9)
| spl10_253 ),
inference(forward_subsumption_resolution,[],[f14014,f582]) ).
fof(f14022,plain,
( $false
| spl10_253
| spl10_263 ),
inference(forward_subsumption_resolution,[],[f14017,f13482]) ).
fof(f14023,plain,
( spl10_253
| spl10_263 ),
inference(avatar_contradiction_clause,[],[f14022]) ).
fof(f14026,plain,
( member(not_subclass_element(sF4,sF9),sF4)
| ~ member(not_subclass_element(sF4,sF9),sF1)
| ~ spl10_251 ),
inference(resolution,[],[f13417,f232]) ).
fof(f14029,plain,
( member(not_subclass_element(sF4,sF9),sF4)
| ~ spl10_251
| ~ spl10_255 ),
inference(forward_subsumption_resolution,[],[f14026,f13434]) ).
fof(f14032,plain,
( member(not_subclass_element(sF4,sF9),sF5)
| ~ spl10_251
| ~ spl10_255 ),
inference(resolution,[],[f14029,f908]) ).
fof(f14039,plain,
( $false
| spl10_241
| ~ spl10_251
| ~ spl10_255 ),
inference(forward_subsumption_resolution,[],[f14032,f13349]) ).
fof(f14040,plain,
( spl10_241
| ~ spl10_251
| ~ spl10_255 ),
inference(avatar_contradiction_clause,[],[f14039]) ).
fof(f14045,plain,
( ~ member(not_subclass_element(sF4,sF9),sF5)
| ~ spl10_262
| spl10_263 ),
inference(forward_subsumption_resolution,[],[f13953,f13482]) ).
fof(f14049,plain,
( $false
| ~ spl10_241
| ~ spl10_262
| spl10_263 ),
inference(forward_subsumption_resolution,[],[f14045,f13348]) ).
fof(f14050,plain,
( ~ spl10_241
| ~ spl10_262
| spl10_263 ),
inference(avatar_contradiction_clause,[],[f14049]) ).
cnf(s264,plain,
( spl10_213
| spl10_214 ),
inference(sat_conversion,[],[f13211]) ).
cnf(s295,plain,
( ~ spl10_213
| ~ spl10_260
| ~ spl10_261
| spl10_262 ),
inference(sat_conversion,[],[f13466]) ).
cnf(s296,plain,
( ~ spl10_213
| spl10_254
| ~ spl10_258 ),
inference(sat_conversion,[],[f13467]) ).
cnf(s297,plain,
( ~ spl10_213
| spl10_250
| ~ spl10_259 ),
inference(sat_conversion,[],[f13468]) ).
cnf(s299,plain,
( ~ spl10_213
| spl10_256
| ~ spl10_258 ),
inference(sat_conversion,[],[f13470]) ).
cnf(s300,plain,
( ~ spl10_213
| spl10_252
| ~ spl10_259 ),
inference(sat_conversion,[],[f13471]) ).
cnf(s305,plain,
( ~ spl10_214
| ~ spl10_270
| spl10_271
| ~ spl10_272
| ~ spl10_273 ),
inference(sat_conversion,[],[f13543]) ).
cnf(s312,plain,
( ~ spl10_214
| spl10_266
| ~ spl10_280 ),
inference(sat_conversion,[],[f13578]) ).
cnf(s315,plain,
( ~ spl10_214
| spl10_268
| ~ spl10_280 ),
inference(sat_conversion,[],[f13581]) ).
cnf(s324,plain,
( ~ spl10_217
| ~ spl10_263 ),
inference(sat_conversion,[],[f13752]) ).
cnf(s327,plain,
( spl10_258
| spl10_263 ),
inference(sat_conversion,[],[f13762]) ).
cnf(s332,plain,
( spl10_251
| ~ spl10_253
| ~ spl10_259 ),
inference(sat_conversion,[],[f13773]) ).
cnf(s334,plain,
( spl10_259
| spl10_263 ),
inference(sat_conversion,[],[f13776]) ).
cnf(s338,plain,
( spl10_217
| spl10_278 ),
inference(sat_conversion,[],[f13785]) ).
cnf(s339,plain,
( spl10_217
| spl10_280 ),
inference(sat_conversion,[],[f13787]) ).
cnf(s340,plain,
( ~ spl10_268
| spl10_272 ),
inference(sat_conversion,[],[f13792]) ).
cnf(s341,plain,
( ~ spl10_266
| spl10_270 ),
inference(sat_conversion,[],[f13799]) ).
cnf(s343,plain,
( spl10_255
| ~ spl10_257
| ~ spl10_258 ),
inference(sat_conversion,[],[f13817]) ).
cnf(s344,plain,
( spl10_213
| ~ spl10_258 ),
inference(sat_conversion,[],[f13819]) ).
cnf(s346,plain,
( spl10_217
| spl10_269 ),
inference(sat_conversion,[],[f13844]) ).
cnf(s347,plain,
( ~ spl10_269
| spl10_277 ),
inference(sat_conversion,[],[f13851]) ).
cnf(s348,plain,
( ~ spl10_269
| spl10_273 ),
inference(sat_conversion,[],[f13853]) ).
cnf(s349,plain,
( spl10_217
| ~ spl10_271
| ~ spl10_275 ),
inference(sat_conversion,[],[f13863]) ).
cnf(s353,plain,
( spl10_214
| ~ spl10_280 ),
inference(sat_conversion,[],[f13872]) ).
cnf(s354,plain,
( spl10_275
| ~ spl10_277
| ~ spl10_278 ),
inference(sat_conversion,[],[f13874]) ).
cnf(s356,plain,
( ~ spl10_252
| ~ spl10_256
| spl10_260 ),
inference(sat_conversion,[],[f13909]) ).
cnf(s360,plain,
( ~ spl10_250
| ~ spl10_254
| spl10_261 ),
inference(sat_conversion,[],[f13950]) ).
cnf(s363,plain,
( spl10_257
| spl10_263 ),
inference(sat_conversion,[],[f14004]) ).
cnf(s366,plain,
( spl10_253
| spl10_263 ),
inference(sat_conversion,[],[f14023]) ).
cnf(s367,plain,
( spl10_241
| ~ spl10_251
| ~ spl10_255 ),
inference(sat_conversion,[],[f14040]) ).
cnf(s368,plain,
( ~ spl10_241
| ~ spl10_262
| spl10_263 ),
inference(sat_conversion,[],[f14050]) ).
cnf(s387,plain,
spl10_213,
inference(rat,[],[s305,s349,s341,s340,s354,s312,s315,s347,s348,s338,s339,s346,s324,s327,s264,s344]) ).
cnf(s388,plain,
( spl10_217
| ~ spl10_214 ),
inference(rat,[],[s305,s349,s341,s340,s354,s312,s315,s347,s348,s338,s339,s346]) ).
cnf(s389,plain,
spl10_263,
inference(rat,[],[s295,s368,s360,s356,s367,s296,s299,s297,s300,s332,s343,s327,s334,s363,s366,s387]) ).
cnf(s390,plain,
~ spl10_217,
inference(rat,[],[s324,s389]) ).
cnf(s392,plain,
spl10_280,
inference(rat,[],[s339,s390]) ).
cnf(s395,plain,
~ spl10_214,
inference(rat,[],[s388,s390]) ).
cnf(s398,plain,
$false,
inference(rat,[],[s353,s392,s395]) ).
fof(f14051,plain,
$false,
inference(avatar_sat_refutation,[],[s398]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET248-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.37 % Computer : n008.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 28 01:13:24 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/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
% 10.82/2.46 % (1780851)Input is clausal, will run a generic CNF schedule.
% 10.82/2.46 % (1780857)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1074923848:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.82/2.46 % (1780858)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4275040644:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.82/2.46 % (1780860)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3786858933:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.82/2.46 % (1780859)lrs+10_1_sil=8000:sp=occurrence:random_seed=711469354:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.82/2.46 % (1780856)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=2614381993:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.82/2.46 % (1780861)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2673322728:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.82/2.46 % (1780859)Refutation not found, incomplete strategy
% 10.82/2.46 % (1780859)------------------------------
% 10.82/2.46 % (1780859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.82/2.46 % (1780859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.82/2.46 % (1780859)CaDiCaL version: 2.1.3
% 10.82/2.46 % (1780859)Termination reason: Refutation not found, incomplete strategy
% 10.82/2.46 % (1780859)Time elapsed: 0.002 s
% 10.82/2.46 % (1780859)Peak memory usage: 88 MB
% 10.82/2.46 % (1780859)Instructions burned: 1 (million)
% 10.82/2.46 % (1780862)dis-21_1_sil=8000:lcm=predicate:random_seed=3802785406:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 10.82/2.46 % (1780860)Instruction limit reached!
% 10.82/2.46 % (1780860)------------------------------
% 10.82/2.46 % (1780860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.82/2.46 % (1780860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.82/2.46 % (1780860)CaDiCaL version: 2.1.3
% 10.82/2.46 % (1780860)Termination reason: Instruction limit
% 10.82/2.46 % (1780860)Termination phase: Saturation
% 10.82/2.46 % (1780860)Time elapsed: 0.065 s
% 10.82/2.46 % (1780860)Peak memory usage: 89 MB
% 10.82/2.46 % (1780860)Instructions burned: 115 (million)
% 10.82/2.46 % (1780862)Instruction limit reached!
% 10.82/2.46 % (1780862)------------------------------
% 10.82/2.46 % (1780862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.82/2.46 % (1780862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.82/2.46 % (1780862)CaDiCaL version: 2.1.3
% 10.82/2.46 % (1780862)Termination reason: Instruction limit
% 10.82/2.46 % (1780862)Termination phase: Saturation
% 10.82/2.46 % (1780862)Time elapsed: 0.065 s
% 10.82/2.46 % (1780862)Peak memory usage: 90 MB
% 10.82/2.46 % (1780862)Instructions burned: 117 (million)
% 10.82/2.46 % (1780861)Instruction limit reached!
% 10.82/2.46 % (1780861)------------------------------
% 10.82/2.46 % (1780861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.82/2.46 % (1780861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.82/2.46 % (1780861)CaDiCaL version: 2.1.3
% 10.82/2.46 % (1780861)Termination reason: Instruction limit
% 10.82/2.46 % (1780861)Termination phase: Saturation
% 10.82/2.46 % (1780861)Time elapsed: 0.141 s
% 10.82/2.46 % (1780861)Peak memory usage: 90 MB
% 10.82/2.46 % (1780861)Instructions burned: 181 (million)
% 10.82/2.46 % (1780870)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1101256541:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 10.82/2.46 % (1780871)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3876262595:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 10.82/2.46 % (1780870)Refutation not found, incomplete strategy
% 10.82/2.46 % (1780870)------------------------------
% 10.82/2.46 % (1780870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.82/2.46 % (1780870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.82/2.46 % (1780870)CaDiCaL version: 2.1.3
% 12.47/2.65 % (1780870)Termination reason: Refutation not found, incomplete strategy
% 12.47/2.65 % (1780870)Time elapsed: 0.003 s
% 12.47/2.65 % (1780870)Peak memory usage: 88 MB
% 12.47/2.65 % (1780870)Instructions burned: 3 (million)
% 12.47/2.65 % (1780871)Refutation not found, incomplete strategy
% 12.47/2.65 % (1780871)------------------------------
% 12.47/2.65 % (1780871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.47/2.65 % (1780871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.47/2.65 % (1780871)CaDiCaL version: 2.1.3
% 12.47/2.65 % (1780871)Termination reason: Refutation not found, incomplete strategy
% 12.47/2.65 % (1780871)Time elapsed: 0.008 s
% 12.47/2.65 % (1780871)Peak memory usage: 88 MB
% 12.47/2.65 % (1780871)Instructions burned: 14 (million)
% 12.47/2.65 % (1780859)------------------------------
% 12.47/2.65 % (1780859)------------------------------
% 12.47/2.65 % (1780872)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1524916229:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 12.47/2.65 % (1780872)Refutation not found, incomplete strategy
% 12.47/2.65 % (1780872)------------------------------
% 12.47/2.65 % (1780872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.47/2.65 % (1780872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.47/2.65 % (1780872)CaDiCaL version: 2.1.3
% 12.47/2.65 % (1780872)Termination reason: Refutation not found, incomplete strategy
% 12.47/2.65 % (1780872)Time elapsed: 0.003 s
% 12.47/2.65 % (1780872)Peak memory usage: 88 MB
% 12.47/2.65 % (1780872)Instructions burned: 3 (million)
% 12.47/2.65 % (1780875)lrs+10_64_to=lpo:sil=8000:random_seed=3980443400:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 12.47/2.65 % (1780870)------------------------------
% 12.47/2.65 % (1780870)------------------------------
% 12.47/2.65 % (1780871)------------------------------
% 12.47/2.65 % (1780871)------------------------------
% 12.47/2.65 % (1780875)Instruction limit reached!
% 12.47/2.65 % (1780875)------------------------------
% 12.47/2.65 % (1780875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.47/2.65 % (1780875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.47/2.65 % (1780875)CaDiCaL version: 2.1.3
% 12.47/2.65 % (1780875)Termination reason: Instruction limit
% 12.47/2.65 % (1780875)Termination phase: Saturation
% 12.47/2.65 % (1780875)Time elapsed: 0.080 s
% 12.47/2.65 % (1780875)Peak memory usage: 89 MB
% 12.47/2.65 % (1780875)Instructions burned: 127 (million)
% 12.47/2.65 % (1780872)------------------------------
% 12.47/2.65 % (1780872)------------------------------
% 12.47/2.65 % (1780879)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1747596017:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 12.47/2.65 % (1780878)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2232853287:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 12.47/2.65 % (1780880)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3763598531:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 12.47/2.65 % (1780881)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=560831214:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 12.47/2.65 % (1780879)Instruction limit reached!
% 12.47/2.65 % (1780879)------------------------------
% 12.47/2.65 % (1780879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.47/2.65 % (1780879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.47/2.65 % (1780879)CaDiCaL version: 2.1.3
% 12.47/2.65 % (1780879)Termination reason: Instruction limit
% 12.47/2.65 % (1780879)Termination phase: Saturation
% 12.47/2.65 % (1780879)Time elapsed: 0.103 s
% 12.47/2.65 % (1780879)Peak memory usage: 91 MB
% 12.47/2.65 % (1780879)Instructions burned: 158 (million)
% 12.47/2.65 % (1780878)Instruction limit reached!
% 12.47/2.65 % (1780878)------------------------------
% 12.47/2.65 % (1780878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.47/2.65 % (1780878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.47/2.65 % (1780878)CaDiCaL version: 2.1.3
% 12.47/2.65 % (1780878)Termination reason: Instruction limit
% 12.47/2.65 % (1780878)Termination phase: Saturation
% 12.47/2.65 % (1780878)Time elapsed: 0.117 s
% 12.47/2.65 % (1780878)Peak memory usage: 89 MB
% 12.47/2.65 % (1780878)Instructions burned: 194 (million)
% 12.47/2.65 % (1780881)Instruction limit reached!
% 12.47/2.65 % (1780881)------------------------------
% 12.47/2.65 % (1780881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.47/2.65 % (1780881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.47/2.65 % (1780881)CaDiCaL version: 2.1.3
% 12.47/2.65 % (1780881)Termination reason: Instruction limit
% 12.47/2.65 % (1780881)Termination phase: Saturation
% 12.47/2.65 % (1780881)Time elapsed: 0.064 s
% 12.47/2.65 % (1780881)Peak memory usage: 90 MB
% 12.47/2.65 % (1780881)Instructions burned: 107 (million)
% 12.47/2.65 % (1780886)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3832524596:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 12.47/2.65 % (1780886)Refutation not found, incomplete strategy
% 12.47/2.65 % (1780886)------------------------------
% 12.47/2.65 % (1780886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.47/2.65 % (1780886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.47/2.65 % (1780886)CaDiCaL version: 2.1.3
% 12.47/2.65 % (1780886)Termination reason: Refutation not found, incomplete strategy
% 12.47/2.65 % (1780886)Time elapsed: 0.005 s
% 12.47/2.65 % (1780886)Peak memory usage: 88 MB
% 12.47/2.65 % (1780886)Instructions burned: 8 (million)
% 12.47/2.65 % (1780887)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1735427845:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 12.47/2.65 % (1780888)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4067805020:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 12.47/2.65 % (1780887)Instruction limit reached!
% 12.47/2.65 % (1780887)------------------------------
% 12.47/2.65 % (1780887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.47/2.65 % (1780887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.47/2.65 % (1780887)CaDiCaL version: 2.1.3
% 12.47/2.65 % (1780887)Termination reason: Instruction limit
% 12.47/2.65 % (1780887)Termination phase: Saturation
% 12.47/2.65 % (1780887)Time elapsed: 0.166 s
% 12.47/2.65 % (1780887)Peak memory usage: 90 MB
% 12.47/2.65 % (1780887)Instructions burned: 243 (million)
% 12.47/2.65 % (1780886)------------------------------
% 12.47/2.65 % (1780886)------------------------------
% 12.47/2.65 % (1780892)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1879990881:i=134:sd=2:doe=on:ss=axioms:sgt=14_2988 on theBenchmark for (2988ds/134Mi)
% 12.47/2.65 % (1780893)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=788372426:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 12.47/2.65 % (1780892)Instruction limit reached!
% 12.47/2.65 % (1780892)------------------------------
% 12.47/2.65 % (1780892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.47/2.65 % (1780892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.47/2.65 % (1780892)CaDiCaL version: 2.1.3
% 12.47/2.65 % (1780892)Termination reason: Instruction limit
% 12.47/2.65 % (1780892)Termination phase: Saturation
% 12.47/2.65 % (1780892)Time elapsed: 0.090 s
% 12.47/2.65 % (1780892)Peak memory usage: 90 MB
% 12.47/2.65 % (1780892)Instructions burned: 134 (million)
% 12.47/2.65 % (1780896)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2083412955:i=191:fgj=on:bd=all_2986 on theBenchmark for (2986ds/191Mi)
% 12.47/2.65 % (1780856)First to succeed.
% 12.47/2.65 % (1780856)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1780851"
% 12.47/2.65 % (1780896)Instruction limit reached!
% 12.47/2.65 % (1780896)------------------------------
% 12.47/2.65 % (1780896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.47/2.65 % (1780896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.47/2.65 % (1780896)CaDiCaL version: 2.1.3
% 12.47/2.65 % (1780896)Termination reason: Instruction limit
% 12.47/2.65 % (1780896)Termination phase: Saturation
% 12.47/2.65 % (1780896)Time elapsed: 0.114 s
% 12.47/2.65 % (1780896)Peak memory usage: 90 MB
% 12.47/2.65 % (1780896)Instructions burned: 192 (million)
% 12.47/2.65 % (1780893)Instruction limit reached!
% 12.47/2.65 % (1780893)------------------------------
% 12.47/2.65 % (1780893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.47/2.65 % (1780893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.47/2.65 % (1780893)CaDiCaL version: 2.1.3
% 12.47/2.65 % (1780893)Termination reason: Instruction limit
% 12.47/2.65 % (1780893)Termination phase: Saturation
% 12.47/2.65 % (1780893)Time elapsed: 0.292 s
% 12.47/2.65 % (1780893)Peak memory usage: 93 MB
% 12.47/2.65 % (1780893)Instructions burned: 500 (million)
% 12.47/2.65 % (1780898)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1280871809:i=264:kws=precedence:fsr=off_2983 on theBenchmark for (2983ds/264Mi)
% 12.47/2.65 % (1780888)Also succeeded, but the first one will report.
% 12.47/2.65 % (1780899)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3970006507:cond=on:i=156:bs=on:gtg=exists_all:er=known_2983 on theBenchmark for (2983ds/156Mi)
% 12.47/2.65 % (1780856)Refutation found. Thanks to Tanya!
% 12.47/2.65 % SZS status Unsatisfiable for theBenchmark
% 12.47/2.65 % SZS output start Proof for theBenchmark
% See solution above
% 13.29/2.85 % (1780856)------------------------------
% 13.29/2.85 % (1780856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.29/2.85 % (1780856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.29/2.85 % (1780856)CaDiCaL version: 2.1.3
% 13.29/2.85 % (1780856)Termination reason: Refutation
% 13.29/2.85 % (1780856)Time elapsed: 1.395 s
% 13.29/2.85 % (1780856)Peak memory usage: 142 MB
% 13.29/2.85 % (1780856)Instructions burned: 2172 (million)
% 13.29/2.85 % (1780856)------------------------------
% 13.29/2.85 % (1780856)------------------------------
% 13.29/2.85 % (1780851)Success in time 1.805 s
% 13.29/2.85 % Vampire exiting
%------------------------------------------------------------------------------