%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO090-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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 09:51:30 AM UTC 2026
% Result : Unsatisfiable 6.66s 2.00s
% Output : Refutation 8.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 28
% Syntax : Number of formulae : 145 ( 18 unt; 8 def)
% Number of atoms : 481 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 586 ( 250 ~; 328 |; 0 &)
% ( 8 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 13 ( 12 usr; 9 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-3 aty)
% Number of variables : 119 ( 0 sgn 119 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( ~ incident_c(X2,X0)
| ~ part_of(X0,X1)
| incident_c(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',part_of_defn_1) ).
fof(f2,axiom,
! [X0,X1] :
( incident_c(ax0_sk1(X0,X1),X0)
| part_of(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',part_of_defn_2) ).
fof(f3,axiom,
! [X0,X1] :
( ~ incident_c(ax0_sk1(X0,X1),X1)
| part_of(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',part_of_defn_3) ).
fof(f23,axiom,
! [X2,X3,X0,X1] :
( ~ end_point(X0,X1)
| ~ part_of(X2,X1)
| ~ part_of(X3,X1)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,X3)
| part_of(X2,X3)
| part_of(X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',end_point_defn_14) ).
fof(f24,axiom,
! [X0,X1] :
( part_of(ax0_sk3(X1,X0),X1)
| ~ incident_c(X0,X1)
| end_point(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',end_point_defn_15) ).
fof(f25,axiom,
! [X0,X1] :
( part_of(ax0_sk4(X1,X0),X1)
| ~ incident_c(X0,X1)
| end_point(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',end_point_defn_16) ).
fof(f26,axiom,
! [X0,X1] :
( incident_c(X0,ax0_sk3(X1,X0))
| ~ incident_c(X0,X1)
| end_point(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',end_point_defn_17) ).
fof(f27,axiom,
! [X0,X1] :
( incident_c(X0,ax0_sk4(X1,X0))
| ~ incident_c(X0,X1)
| end_point(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',end_point_defn_18) ).
fof(f28,axiom,
! [X0,X1] :
( ~ part_of(ax0_sk3(X1,X0),ax0_sk4(X1,X0))
| ~ incident_c(X0,X1)
| end_point(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',end_point_defn_19) ).
fof(f29,axiom,
! [X0,X1] :
( ~ part_of(ax0_sk4(X1,X0),ax0_sk3(X1,X0))
| ~ incident_c(X0,X1)
| end_point(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',end_point_defn_20) ).
fof(f34,axiom,
! [X2,X0,X1] :
( ~ meet(X0,X1,X2)
| incident_c(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_defn_25) ).
fof(f35,axiom,
! [X2,X3,X0,X1] :
( ~ meet(X0,X1,X2)
| ~ incident_c(X3,X1)
| ~ incident_c(X3,X2)
| end_point(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_defn_26) ).
fof(f36,axiom,
! [X2,X3,X0,X1] :
( ~ meet(X0,X1,X2)
| ~ incident_c(X3,X1)
| ~ incident_c(X3,X2)
| end_point(X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_defn_27) ).
fof(f37,axiom,
! [X2,X0,X1] :
( incident_c(ax0_sk5(X2,X1,X0),X1)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,X1)
| meet(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_defn_28) ).
fof(f38,axiom,
! [X2,X0,X1] :
( incident_c(ax0_sk5(X2,X1,X0),X2)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,X1)
| meet(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_defn_29) ).
fof(f39,axiom,
! [X2,X0,X1] :
( ~ end_point(ax0_sk5(X2,X1,X0),X2)
| ~ incident_c(X0,X2)
| ~ end_point(ax0_sk5(X2,X1,X0),X1)
| ~ incident_c(X0,X1)
| meet(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_defn_30) ).
fof(f66,negated_conjecture,
part_of(sk15,sk14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',corollary_2_12_67) ).
fof(f67,negated_conjecture,
incident_c(sk17,sk15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',corollary_2_12_68) ).
fof(f68,negated_conjecture,
meet(sk17,sk14,sk16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',corollary_2_12_69) ).
fof(f69,negated_conjecture,
~ meet(sk17,sk15,sk16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',corollary_2_12_70) ).
fof(f74,plain,
! [X0] :
( ~ incident_c(X0,sk16)
| ~ incident_c(X0,sk14)
| end_point(X0,sk14) ),
inference(resolution,[],[f35,f68]) ).
fof(f75,plain,
! [X0] :
( ~ incident_c(X0,sk16)
| ~ incident_c(X0,sk14)
| end_point(X0,sk16) ),
inference(resolution,[],[f36,f68]) ).
fof(f76,plain,
! [X0,X1] :
( ~ incident_c(ax0_sk5(sk16,X0,X1),sk14)
| end_point(ax0_sk5(sk16,X0,X1),sk16)
| ~ incident_c(X1,sk16)
| ~ incident_c(X1,X0)
| meet(X1,X0,sk16) ),
inference(resolution,[],[f75,f38]) ).
fof(f77,plain,
! [X0,X1] :
( ~ incident_c(ax0_sk5(X0,sk16,X1),sk14)
| end_point(ax0_sk5(X0,sk16,X1),sk16)
| ~ incident_c(X1,X0)
| ~ incident_c(X1,sk16)
| meet(X1,sk16,X0) ),
inference(resolution,[],[f75,f37]) ).
fof(f79,plain,
! [X2,X3,X0,X1] :
( incident_c(ax0_sk5(X0,X2,X3),X1)
| ~ part_of(X0,X1)
| ~ incident_c(X3,X0)
| ~ incident_c(X3,X2)
| meet(X3,X2,X0) ),
inference(resolution,[],[f1,f38]) ).
fof(f80,plain,
! [X2,X3,X0,X1] :
( incident_c(ax0_sk5(X2,X0,X3),X1)
| ~ part_of(X0,X1)
| ~ incident_c(X3,X2)
| ~ incident_c(X3,X0)
| meet(X3,X0,X2) ),
inference(resolution,[],[f1,f37]) ).
fof(f82,plain,
! [X2,X3,X0,X1,X4] :
( ~ incident_c(X2,X3)
| ~ incident_c(X2,X0)
| ~ part_of(X0,X1)
| meet(X2,X3,X0)
| ~ part_of(X1,X4)
| incident_c(ax0_sk5(X0,X3,X2),X4) ),
inference(resolution,[],[f79,f1]) ).
fof(f84,plain,
! [X2,X3,X0,X1,X4] :
( ~ incident_c(X2,X3)
| ~ part_of(X0,X1)
| ~ incident_c(X2,X0)
| meet(X2,X0,X3)
| ~ part_of(X1,X4)
| incident_c(ax0_sk5(X3,X0,X2),X4) ),
inference(resolution,[],[f80,f1]) ).
fof(f86,plain,
! [X0,X1] :
( ~ incident_c(ax0_sk5(X0,sk16,X1),sk14)
| end_point(ax0_sk5(X0,sk16,X1),sk14)
| ~ incident_c(X1,X0)
| ~ incident_c(X1,sk16)
| meet(X1,sk16,X0) ),
inference(resolution,[],[f74,f37]) ).
fof(f89,plain,
incident_c(sk17,sk16),
inference(resolution,[],[f34,f68]) ).
fof(f152,plain,
! [X2,X0,X1] :
( ~ incident_c(sk17,X0)
| ~ part_of(X0,X1)
| meet(sk17,sk15,X0)
| ~ part_of(X1,X2)
| incident_c(ax0_sk5(X0,sk15,sk17),X2) ),
inference(resolution,[],[f82,f67]) ).
fof(f153,plain,
! [X2,X0,X1] :
( ~ incident_c(sk17,X0)
| ~ part_of(X0,X1)
| meet(sk17,sk16,X0)
| ~ part_of(X1,X2)
| incident_c(ax0_sk5(X0,sk16,sk17),X2) ),
inference(resolution,[],[f82,f89]) ).
fof(f160,plain,
! [X0,X1] :
( ~ part_of(sk16,X0)
| meet(sk17,sk15,sk16)
| ~ part_of(X0,X1)
| incident_c(ax0_sk5(sk16,sk15,sk17),X1) ),
inference(resolution,[],[f152,f89]) ).
fof(f170,plain,
! [X0,X1] :
( ~ part_of(sk16,X0)
| ~ part_of(X0,X1)
| incident_c(ax0_sk5(sk16,sk15,sk17),X1) ),
inference(forward_subsumption_resolution,[],[f160,f69]) ).
fof(f186,plain,
! [X0,X1] :
( ~ part_of(sk15,X0)
| meet(sk17,sk16,sk15)
| ~ part_of(X0,X1)
| incident_c(ax0_sk5(sk15,sk16,sk17),X1) ),
inference(resolution,[],[f153,f67]) ).
fof(f206,definition,
( spl0_14
<=> meet(sk17,sk16,sk15) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f207,plain,
( ~ meet(sk17,sk16,sk15)
| spl0_14 ),
inference(avatar_component_clause,[],[f206]) ).
fof(f208,plain,
( meet(sk17,sk16,sk15)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f206]) ).
fof(f210,definition,
( spl0_15
<=> ! [X0,X1] :
( ~ part_of(sk15,X0)
| incident_c(ax0_sk5(sk15,sk16,sk17),X1)
| ~ part_of(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f211,plain,
( ! [X0,X1] :
( ~ part_of(sk15,X0)
| incident_c(ax0_sk5(sk15,sk16,sk17),X1)
| ~ part_of(X0,X1) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f210]) ).
fof(f212,plain,
( spl0_14
| spl0_15 ),
inference(avatar_split_clause,[],[f186,f210,f206]) ).
fof(f216,plain,
( ! [X0] :
( ~ incident_c(X0,sk16)
| ~ incident_c(X0,sk15)
| end_point(X0,sk15) )
| ~ spl0_14 ),
inference(resolution,[],[f208,f36]) ).
fof(f231,plain,
! [X0] :
( part_of(X0,X0)
| part_of(X0,X0) ),
inference(resolution,[],[f2,f3]) ).
fof(f235,plain,
! [X2,X0,X1] :
( incident_c(ax0_sk1(X0,X1),X2)
| ~ part_of(X0,X2)
| part_of(X0,X1) ),
inference(resolution,[],[f2,f1]) ).
fof(f237,plain,
! [X0] : part_of(X0,X0),
inference(duplicate_literal_removal,[],[f231]) ).
fof(f242,plain,
! [X2,X3,X0,X1] :
( ~ part_of(X1,X3)
| part_of(X0,X2)
| ~ part_of(X0,X1)
| incident_c(ax0_sk1(X0,X2),X3) ),
inference(resolution,[],[f235,f1]) ).
fof(f246,plain,
! [X2,X0,X1] :
( ~ incident_c(sk17,X0)
| ~ part_of(X0,X1)
| meet(sk17,X0,sk16)
| ~ part_of(X1,X2)
| incident_c(ax0_sk5(sk16,X0,sk17),X2) ),
inference(resolution,[],[f84,f89]) ).
fof(f265,plain,
! [X0,X1] :
( ~ part_of(sk15,X0)
| meet(sk17,sk15,sk16)
| ~ part_of(X0,X1)
| incident_c(ax0_sk5(sk16,sk15,sk17),X1) ),
inference(resolution,[],[f246,f67]) ).
fof(f268,plain,
! [X0,X1] :
( ~ part_of(sk15,X0)
| ~ part_of(X0,X1)
| incident_c(ax0_sk5(sk16,sk15,sk17),X1) ),
inference(forward_subsumption_resolution,[],[f265,f69]) ).
fof(f269,plain,
! [X0] :
( incident_c(ax0_sk5(sk16,sk15,sk17),X0)
| ~ part_of(sk14,X0) ),
inference(resolution,[],[f268,f66]) ).
fof(f270,plain,
( ~ part_of(sk14,sk14)
| end_point(ax0_sk5(sk16,sk15,sk17),sk16)
| ~ incident_c(sk17,sk16)
| ~ incident_c(sk17,sk15)
| meet(sk17,sk15,sk16) ),
inference(resolution,[],[f269,f76]) ).
fof(f279,definition,
( spl0_18
<=> end_point(ax0_sk5(sk16,sk15,sk17),sk15) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f280,plain,
( ~ end_point(ax0_sk5(sk16,sk15,sk17),sk15)
| spl0_18 ),
inference(avatar_component_clause,[],[f279]) ).
fof(f288,definition,
( spl0_20
<=> end_point(ax0_sk5(sk16,sk15,sk17),sk16) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f290,plain,
( end_point(ax0_sk5(sk16,sk15,sk17),sk16)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f306,plain,
( end_point(ax0_sk5(sk16,sk15,sk17),sk16)
| ~ incident_c(sk17,sk16)
| ~ incident_c(sk17,sk15)
| meet(sk17,sk15,sk16) ),
inference(forward_subsumption_resolution,[],[f270,f237]) ).
fof(f308,plain,
( end_point(ax0_sk5(sk16,sk15,sk17),sk16)
| ~ incident_c(sk17,sk15)
| meet(sk17,sk15,sk16) ),
inference(forward_subsumption_resolution,[],[f306,f89]) ).
fof(f310,plain,
( end_point(ax0_sk5(sk16,sk15,sk17),sk16)
| meet(sk17,sk15,sk16) ),
inference(forward_subsumption_resolution,[],[f308,f67]) ).
fof(f312,plain,
end_point(ax0_sk5(sk16,sk15,sk17),sk16),
inference(forward_subsumption_resolution,[],[f310,f69]) ).
fof(f314,plain,
spl0_20,
inference(avatar_split_clause,[],[f312,f288]) ).
fof(f369,plain,
( ~ incident_c(sk17,sk16)
| ~ end_point(ax0_sk5(sk16,sk15,sk17),sk15)
| ~ incident_c(sk17,sk15)
| meet(sk17,sk15,sk16)
| ~ spl0_20 ),
inference(resolution,[],[f39,f290]) ).
fof(f375,plain,
( ~ end_point(ax0_sk5(sk16,sk15,sk17),sk15)
| ~ incident_c(sk17,sk15)
| meet(sk17,sk15,sk16)
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f369,f89]) ).
fof(f376,plain,
( ~ end_point(ax0_sk5(sk16,sk15,sk17),sk15)
| meet(sk17,sk15,sk16)
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f375,f67]) ).
fof(f377,plain,
( ~ end_point(ax0_sk5(sk16,sk15,sk17),sk15)
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f376,f69]) ).
fof(f378,plain,
( ~ spl0_18
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f377,f288,f279]) ).
fof(f461,plain,
! [X0] :
( incident_c(ax0_sk5(sk16,sk15,sk17),X0)
| ~ part_of(sk16,X0) ),
inference(resolution,[],[f237,f170]) ).
fof(f504,plain,
( ~ part_of(sk16,sk16)
| ~ incident_c(ax0_sk5(sk16,sk15,sk17),sk15)
| end_point(ax0_sk5(sk16,sk15,sk17),sk15)
| ~ spl0_14 ),
inference(resolution,[],[f461,f216]) ).
fof(f511,plain,
( ~ incident_c(ax0_sk5(sk16,sk15,sk17),sk15)
| end_point(ax0_sk5(sk16,sk15,sk17),sk15)
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f504,f237]) ).
fof(f512,plain,
( ~ incident_c(ax0_sk5(sk16,sk15,sk17),sk15)
| ~ spl0_14
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f511,f280]) ).
fof(f517,plain,
( ~ part_of(sk15,sk15)
| ~ incident_c(sk17,sk16)
| ~ incident_c(sk17,sk15)
| meet(sk17,sk15,sk16)
| ~ spl0_14
| spl0_18 ),
inference(resolution,[],[f512,f80]) ).
fof(f520,plain,
( ~ incident_c(sk17,sk16)
| ~ incident_c(sk17,sk15)
| meet(sk17,sk15,sk16)
| ~ spl0_14
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f517,f237]) ).
fof(f524,plain,
( ~ incident_c(sk17,sk15)
| meet(sk17,sk15,sk16)
| ~ spl0_14
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f520,f89]) ).
fof(f526,plain,
( meet(sk17,sk15,sk16)
| ~ spl0_14
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f524,f67]) ).
fof(f529,plain,
( $false
| ~ spl0_14
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f526,f69]) ).
fof(f530,plain,
( ~ spl0_14
| spl0_18 ),
inference(avatar_contradiction_clause,[],[f529]) ).
fof(f532,plain,
( ! [X0] :
( incident_c(ax0_sk5(sk15,sk16,sk17),X0)
| ~ part_of(sk14,X0) )
| ~ spl0_15 ),
inference(resolution,[],[f211,f66]) ).
fof(f534,plain,
( ~ part_of(sk14,sk14)
| end_point(ax0_sk5(sk15,sk16,sk17),sk16)
| ~ incident_c(sk17,sk15)
| ~ incident_c(sk17,sk16)
| meet(sk17,sk16,sk15)
| ~ spl0_15 ),
inference(resolution,[],[f532,f77]) ).
fof(f535,plain,
( ~ part_of(sk14,sk14)
| end_point(ax0_sk5(sk15,sk16,sk17),sk14)
| ~ incident_c(sk17,sk15)
| ~ incident_c(sk17,sk16)
| meet(sk17,sk16,sk15)
| ~ spl0_15 ),
inference(resolution,[],[f532,f86]) ).
fof(f541,plain,
( end_point(ax0_sk5(sk15,sk16,sk17),sk14)
| ~ incident_c(sk17,sk15)
| ~ incident_c(sk17,sk16)
| meet(sk17,sk16,sk15)
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f535,f237]) ).
fof(f542,plain,
( end_point(ax0_sk5(sk15,sk16,sk17),sk16)
| ~ incident_c(sk17,sk15)
| ~ incident_c(sk17,sk16)
| meet(sk17,sk16,sk15)
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f534,f237]) ).
fof(f543,plain,
( end_point(ax0_sk5(sk15,sk16,sk17),sk14)
| ~ incident_c(sk17,sk16)
| meet(sk17,sk16,sk15)
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f541,f67]) ).
fof(f544,plain,
( end_point(ax0_sk5(sk15,sk16,sk17),sk16)
| ~ incident_c(sk17,sk16)
| meet(sk17,sk16,sk15)
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f542,f67]) ).
fof(f545,plain,
( end_point(ax0_sk5(sk15,sk16,sk17),sk14)
| meet(sk17,sk16,sk15)
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f543,f89]) ).
fof(f546,plain,
( end_point(ax0_sk5(sk15,sk16,sk17),sk16)
| meet(sk17,sk16,sk15)
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f544,f89]) ).
fof(f547,plain,
( end_point(ax0_sk5(sk15,sk16,sk17),sk14)
| spl0_14
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f545,f207]) ).
fof(f548,plain,
( end_point(ax0_sk5(sk15,sk16,sk17),sk16)
| spl0_14
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f546,f207]) ).
fof(f552,plain,
( ! [X0,X1] :
( ~ incident_c(ax0_sk5(sk15,sk16,sk17),X1)
| ~ part_of(X1,sk14)
| ~ incident_c(ax0_sk5(sk15,sk16,sk17),X0)
| ~ part_of(X0,sk14)
| part_of(X0,X1)
| part_of(X1,X0) )
| spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f547,f23]) ).
fof(f568,plain,
( ! [X0,X1] :
( ~ part_of(ax0_sk4(X0,ax0_sk5(sk15,sk16,sk17)),sk14)
| ~ incident_c(ax0_sk5(sk15,sk16,sk17),X1)
| ~ part_of(X1,sk14)
| part_of(X1,ax0_sk4(X0,ax0_sk5(sk15,sk16,sk17)))
| part_of(ax0_sk4(X0,ax0_sk5(sk15,sk16,sk17)),X1)
| ~ incident_c(ax0_sk5(sk15,sk16,sk17),X0)
| end_point(ax0_sk5(sk15,sk16,sk17),X0) )
| spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f552,f27]) ).
fof(f653,plain,
! [X0,X1] :
( incident_c(ax0_sk1(X0,X1),sk14)
| ~ part_of(X0,sk15)
| part_of(X0,X1) ),
inference(resolution,[],[f242,f66]) ).
fof(f655,plain,
! [X0] :
( ~ part_of(X0,sk15)
| part_of(X0,sk14)
| part_of(X0,sk14) ),
inference(resolution,[],[f653,f3]) ).
fof(f659,plain,
! [X0] :
( ~ part_of(X0,sk15)
| part_of(X0,sk14) ),
inference(duplicate_literal_removal,[],[f655]) ).
fof(f678,plain,
! [X0] :
( part_of(ax0_sk4(sk15,X0),sk14)
| end_point(X0,sk15)
| ~ incident_c(X0,sk15) ),
inference(resolution,[],[f25,f659]) ).
fof(f692,plain,
( ! [X0] :
( end_point(ax0_sk5(sk15,sk16,sk17),sk15)
| ~ incident_c(ax0_sk5(sk15,sk16,sk17),sk15)
| ~ incident_c(ax0_sk5(sk15,sk16,sk17),X0)
| ~ part_of(X0,sk14)
| part_of(X0,ax0_sk4(sk15,ax0_sk5(sk15,sk16,sk17)))
| part_of(ax0_sk4(sk15,ax0_sk5(sk15,sk16,sk17)),X0)
| ~ incident_c(ax0_sk5(sk15,sk16,sk17),sk15)
| end_point(ax0_sk5(sk15,sk16,sk17),sk15) )
| spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f678,f568]) ).
fof(f696,plain,
( ! [X0] :
( end_point(ax0_sk5(sk15,sk16,sk17),sk15)
| ~ incident_c(ax0_sk5(sk15,sk16,sk17),sk15)
| ~ incident_c(ax0_sk5(sk15,sk16,sk17),X0)
| ~ part_of(X0,sk14)
| part_of(X0,ax0_sk4(sk15,ax0_sk5(sk15,sk16,sk17)))
| part_of(ax0_sk4(sk15,ax0_sk5(sk15,sk16,sk17)),X0) )
| spl0_14
| ~ spl0_15 ),
inference(duplicate_literal_removal,[],[f692]) ).
fof(f701,definition,
( spl0_30
<=> ! [X0] :
( ~ incident_c(ax0_sk5(sk15,sk16,sk17),X0)
| part_of(ax0_sk4(sk15,ax0_sk5(sk15,sk16,sk17)),X0)
| part_of(X0,ax0_sk4(sk15,ax0_sk5(sk15,sk16,sk17)))
| ~ part_of(X0,sk14) ) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f702,plain,
( ! [X0] :
( part_of(ax0_sk4(sk15,ax0_sk5(sk15,sk16,sk17)),X0)
| part_of(X0,ax0_sk4(sk15,ax0_sk5(sk15,sk16,sk17)))
| ~ incident_c(ax0_sk5(sk15,sk16,sk17),X0)
| ~ part_of(X0,sk14) )
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f701]) ).
fof(f704,definition,
( spl0_31
<=> incident_c(ax0_sk5(sk15,sk16,sk17),sk15) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f705,plain,
( incident_c(ax0_sk5(sk15,sk16,sk17),sk15)
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f704]) ).
fof(f706,plain,
( ~ incident_c(ax0_sk5(sk15,sk16,sk17),sk15)
| spl0_31 ),
inference(avatar_component_clause,[],[f704]) ).
fof(f708,definition,
( spl0_32
<=> end_point(ax0_sk5(sk15,sk16,sk17),sk15) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f709,plain,
( ~ end_point(ax0_sk5(sk15,sk16,sk17),sk15)
| spl0_32 ),
inference(avatar_component_clause,[],[f708]) ).
fof(f710,plain,
( end_point(ax0_sk5(sk15,sk16,sk17),sk15)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f708]) ).
fof(f711,plain,
( spl0_30
| ~ spl0_31
| spl0_32
| spl0_14
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f696,f210,f206,f708,f704,f701]) ).
fof(f807,plain,
( ~ part_of(sk15,sk15)
| ~ incident_c(sk17,sk15)
| ~ incident_c(sk17,sk16)
| meet(sk17,sk16,sk15)
| spl0_31 ),
inference(resolution,[],[f706,f79]) ).
fof(f808,plain,
( ~ incident_c(sk17,sk15)
| ~ incident_c(sk17,sk16)
| meet(sk17,sk16,sk15)
| spl0_31 ),
inference(forward_subsumption_resolution,[],[f807,f237]) ).
fof(f813,plain,
( ~ incident_c(sk17,sk16)
| meet(sk17,sk16,sk15)
| spl0_31 ),
inference(forward_subsumption_resolution,[],[f808,f67]) ).
fof(f816,plain,
( meet(sk17,sk16,sk15)
| spl0_31 ),
inference(forward_subsumption_resolution,[],[f813,f89]) ).
fof(f820,plain,
( $false
| spl0_14
| spl0_31 ),
inference(forward_subsumption_resolution,[],[f816,f207]) ).
fof(f821,plain,
( spl0_14
| spl0_31 ),
inference(avatar_contradiction_clause,[],[f820]) ).
fof(f831,plain,
( part_of(ax0_sk3(sk15,ax0_sk5(sk15,sk16,sk17)),ax0_sk4(sk15,ax0_sk5(sk15,sk16,sk17)))
| ~ incident_c(ax0_sk5(sk15,sk16,sk17),ax0_sk3(sk15,ax0_sk5(sk15,sk16,sk17)))
| ~ part_of(ax0_sk3(sk15,ax0_sk5(sk15,sk16,sk17)),sk14)
| ~ incident_c(ax0_sk5(sk15,sk16,sk17),sk15)
| end_point(ax0_sk5(sk15,sk16,sk17),sk15)
| ~ spl0_30 ),
inference(resolution,[],[f702,f29]) ).
fof(f838,plain,
( ~ incident_c(ax0_sk5(sk15,sk16,sk17),ax0_sk3(sk15,ax0_sk5(sk15,sk16,sk17)))
| ~ part_of(ax0_sk3(sk15,ax0_sk5(sk15,sk16,sk17)),sk14)
| ~ incident_c(ax0_sk5(sk15,sk16,sk17),sk15)
| end_point(ax0_sk5(sk15,sk16,sk17),sk15)
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f831,f28]) ).
fof(f840,plain,
( ~ part_of(ax0_sk3(sk15,ax0_sk5(sk15,sk16,sk17)),sk14)
| ~ incident_c(ax0_sk5(sk15,sk16,sk17),sk15)
| end_point(ax0_sk5(sk15,sk16,sk17),sk15)
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f838,f26]) ).
fof(f850,plain,
( ~ part_of(ax0_sk3(sk15,ax0_sk5(sk15,sk16,sk17)),sk14)
| end_point(ax0_sk5(sk15,sk16,sk17),sk15)
| ~ spl0_30
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f840,f705]) ).
fof(f852,definition,
( spl0_43
<=> part_of(ax0_sk3(sk15,ax0_sk5(sk15,sk16,sk17)),sk14) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f854,plain,
( ~ part_of(ax0_sk3(sk15,ax0_sk5(sk15,sk16,sk17)),sk14)
| spl0_43 ),
inference(avatar_component_clause,[],[f852]) ).
fof(f856,plain,
( ~ incident_c(sk17,sk15)
| ~ end_point(ax0_sk5(sk15,sk16,sk17),sk16)
| ~ incident_c(sk17,sk16)
| meet(sk17,sk16,sk15)
| ~ spl0_32 ),
inference(resolution,[],[f710,f39]) ).
fof(f860,plain,
( ~ end_point(ax0_sk5(sk15,sk16,sk17),sk16)
| ~ incident_c(sk17,sk16)
| meet(sk17,sk16,sk15)
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f856,f67]) ).
fof(f861,plain,
( ~ incident_c(sk17,sk16)
| meet(sk17,sk16,sk15)
| spl0_14
| ~ spl0_15
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f860,f548]) ).
fof(f862,plain,
( meet(sk17,sk16,sk15)
| spl0_14
| ~ spl0_15
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f861,f89]) ).
fof(f863,plain,
( $false
| spl0_14
| ~ spl0_15
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f862,f207]) ).
fof(f864,plain,
( spl0_14
| ~ spl0_15
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f863]) ).
fof(f866,plain,
( spl0_32
| ~ spl0_43
| ~ spl0_30
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f850,f704,f701,f852,f708]) ).
fof(f880,plain,
! [X0] :
( part_of(ax0_sk3(sk15,X0),sk14)
| end_point(X0,sk15)
| ~ incident_c(X0,sk15) ),
inference(resolution,[],[f24,f659]) ).
fof(f892,plain,
( end_point(ax0_sk5(sk15,sk16,sk17),sk15)
| ~ incident_c(ax0_sk5(sk15,sk16,sk17),sk15)
| spl0_43 ),
inference(resolution,[],[f880,f854]) ).
fof(f907,plain,
( ~ incident_c(ax0_sk5(sk15,sk16,sk17),sk15)
| spl0_32
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f892,f709]) ).
fof(f912,plain,
( $false
| ~ spl0_31
| spl0_32
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f907,f705]) ).
fof(f913,plain,
( ~ spl0_31
| spl0_32
| spl0_43 ),
inference(avatar_contradiction_clause,[],[f912]) ).
cnf(s9,plain,
( spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f212]) ).
cnf(s15,plain,
spl0_20,
inference(sat_conversion,[],[f314]) ).
cnf(s17,plain,
( ~ spl0_18
| ~ spl0_20 ),
inference(sat_conversion,[],[f378]) ).
cnf(s27,plain,
( ~ spl0_14
| spl0_18 ),
inference(sat_conversion,[],[f530]) ).
cnf(s29,plain,
( spl0_14
| ~ spl0_15
| spl0_30
| ~ spl0_31
| spl0_32 ),
inference(sat_conversion,[],[f711]) ).
cnf(s40,plain,
( spl0_14
| spl0_31 ),
inference(sat_conversion,[],[f821]) ).
cnf(s43,plain,
( spl0_14
| ~ spl0_15
| ~ spl0_32 ),
inference(sat_conversion,[],[f864]) ).
cnf(s44,plain,
( ~ spl0_30
| ~ spl0_31
| spl0_32
| ~ spl0_43 ),
inference(sat_conversion,[],[f866]) ).
cnf(s46,plain,
( ~ spl0_31
| spl0_32
| spl0_43 ),
inference(sat_conversion,[],[f913]) ).
cnf(s50,plain,
~ spl0_18,
inference(rat,[],[s17,s15]) ).
cnf(s53,plain,
~ spl0_14,
inference(rat,[],[s27,s50]) ).
cnf(s54,plain,
spl0_31,
inference(rat,[],[s40,s53]) ).
cnf(s60,plain,
spl0_15,
inference(rat,[],[s9,s53]) ).
cnf(s61,plain,
~ spl0_32,
inference(rat,[],[s43,s53,s60]) ).
cnf(s62,plain,
spl0_30,
inference(rat,[],[s29,s61,s54,s53,s60]) ).
cnf(s63,plain,
spl0_43,
inference(rat,[],[s46,s54,s61]) ).
cnf(s64,plain,
$false,
inference(rat,[],[s44,s63,s54,s61,s62]) ).
fof(f916,plain,
$false,
inference(avatar_sat_refutation,[],[s64]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO090-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n009.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 06:56:15 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.66/2.00 % (1683826)Input is clausal, will run a generic CNF schedule.
% 6.66/2.00 % (1683835)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1228359066:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.66/2.00 % (1683835)Instruction limit reached!
% 6.66/2.00 % (1683835)------------------------------
% 6.66/2.00 % (1683835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.66/2.00 % (1683835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/2.00 % (1683835)CaDiCaL version: 2.1.3
% 6.66/2.00 % (1683835)Termination reason: Instruction limit
% 6.66/2.00 % (1683835)Termination phase: Saturation
% 6.66/2.00 % (1683835)Time elapsed: 0.035 s
% 6.66/2.00 % (1683835)Peak memory usage: 88 MB
% 6.66/2.00 % (1683835)Instructions burned: 118 (million)
% 6.66/2.00 % (1683834)lrs+10_1_sil=8000:sp=occurrence:random_seed=3036710615:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.66/2.00 % (1683831)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=1690281925:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.66/2.00 % (1683832)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=842099956:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.66/2.00 % (1683833)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4029508692:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.66/2.00 % (1683837)dis-21_1_sil=8000:lcm=predicate:random_seed=2658844002: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)
% 6.66/2.00 % (1683836)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1578375856:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.66/2.00 % (1683834)Refutation not found, incomplete strategy
% 6.66/2.00 % (1683834)------------------------------
% 6.66/2.00 % (1683834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.66/2.00 % (1683834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/2.00 % (1683834)CaDiCaL version: 2.1.3
% 6.66/2.00 % (1683834)Termination reason: Refutation not found, incomplete strategy
% 6.66/2.00 % (1683834)Time elapsed: 0.003 s
% 6.66/2.00 % (1683834)Peak memory usage: 88 MB
% 6.66/2.00 % (1683834)Instructions burned: 2 (million)
% 6.66/2.00 % (1683837)Instruction limit reached!
% 6.66/2.00 % (1683837)------------------------------
% 6.66/2.00 % (1683837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.66/2.00 % (1683837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/2.00 % (1683837)CaDiCaL version: 2.1.3
% 6.66/2.00 % (1683837)Termination reason: Instruction limit
% 6.66/2.00 % (1683837)Termination phase: Saturation
% 6.66/2.00 % (1683837)Time elapsed: 0.065 s
% 6.66/2.00 % (1683837)Peak memory usage: 88 MB
% 6.66/2.00 % (1683837)Instructions burned: 117 (million)
% 6.66/2.00 % (1683839)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=611029792:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 6.66/2.00 % (1683839)Refutation not found, incomplete strategy
% 6.66/2.00 % (1683839)------------------------------
% 6.66/2.00 % (1683839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.66/2.00 % (1683839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/2.00 % (1683839)CaDiCaL version: 2.1.3
% 6.66/2.00 % (1683839)Termination reason: Refutation not found, incomplete strategy
% 6.66/2.00 % (1683839)Time elapsed: 0.006 s
% 6.66/2.00 % (1683839)Peak memory usage: 88 MB
% 6.66/2.00 % (1683839)Instructions burned: 16 (million)
% 6.66/2.00 % (1683836)Instruction limit reached!
% 6.66/2.00 % (1683836)------------------------------
% 6.66/2.00 % (1683836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.66/2.00 % (1683836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/2.00 % (1683836)CaDiCaL version: 2.1.3
% 6.66/2.00 % (1683836)Termination reason: Instruction limit
% 6.66/2.00 % (1683836)Termination phase: Saturation
% 6.66/2.00 % (1683836)Time elapsed: 0.123 s
% 6.66/2.00 % (1683836)Peak memory usage: 89 MB
% 6.66/2.00 % (1683836)Instructions burned: 181 (million)
% 6.66/2.00 % (1683846)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3186333478: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)
% 6.66/2.00 % (1683839)------------------------------
% 6.66/2.00 % (1683839)------------------------------
% 6.66/2.00 % (1683834)------------------------------
% 6.66/2.00 % (1683834)------------------------------
% 6.66/2.00 % (1683848)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3934119854:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 6.66/2.00 % (1683846)Instruction limit reached!
% 6.66/2.00 % (1683846)------------------------------
% 6.66/2.00 % (1683846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.66/2.00 % (1683846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/2.00 % (1683846)CaDiCaL version: 2.1.3
% 6.66/2.00 % (1683846)Termination reason: Instruction limit
% 6.66/2.00 % (1683846)Termination phase: Saturation
% 6.66/2.00 % (1683846)Time elapsed: 0.107 s
% 6.66/2.00 % (1683846)Peak memory usage: 89 MB
% 6.66/2.00 % (1683846)Instructions burned: 190 (million)
% 6.66/2.00 % (1683850)lrs+10_64_to=lpo:sil=8000:random_seed=2943712197:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 6.66/2.00 % (1683850)Instruction limit reached!
% 6.66/2.00 % (1683850)------------------------------
% 6.66/2.00 % (1683850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.66/2.00 % (1683850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/2.00 % (1683850)CaDiCaL version: 2.1.3
% 6.66/2.00 % (1683850)Termination reason: Instruction limit
% 6.66/2.00 % (1683850)Termination phase: Saturation
% 6.66/2.00 % (1683850)Time elapsed: 0.043 s
% 6.66/2.00 % (1683850)Peak memory usage: 89 MB
% 6.66/2.00 % (1683850)Instructions burned: 126 (million)
% 6.66/2.00 % (1683848)Instruction limit reached!
% 6.66/2.00 % (1683848)------------------------------
% 6.66/2.00 % (1683848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.66/2.00 % (1683848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/2.00 % (1683848)CaDiCaL version: 2.1.3
% 6.66/2.00 % (1683848)Termination reason: Instruction limit
% 6.66/2.00 % (1683848)Termination phase: Saturation
% 6.66/2.00 % (1683848)Time elapsed: 0.128 s
% 6.66/2.00 % (1683848)Peak memory usage: 89 MB
% 6.66/2.00 % (1683848)Instructions burned: 219 (million)
% 6.66/2.00 % (1683851)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2961921734:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 6.66/2.00 % (1683853)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3275985795:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 6.66/2.00 % (1683855)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1915294752:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 6.66/2.00 % (1683851)Instruction limit reached!
% 6.66/2.00 % (1683851)------------------------------
% 6.66/2.00 % (1683851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.66/2.00 % (1683851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/2.00 % (1683851)CaDiCaL version: 2.1.3
% 6.66/2.00 % (1683851)Termination reason: Instruction limit
% 6.66/2.00 % (1683851)Termination phase: Saturation
% 6.66/2.00 % (1683851)Time elapsed: 0.123 s
% 6.66/2.00 % (1683851)Peak memory usage: 90 MB
% 6.66/2.00 % (1683851)Instructions burned: 195 (million)
% 6.66/2.00 % (1683857)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=4283610326:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 6.66/2.00 % (1683853)Instruction limit reached!
% 6.66/2.00 % (1683853)------------------------------
% 6.66/2.00 % (1683853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.66/2.00 % (1683853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/2.00 % (1683853)CaDiCaL version: 2.1.3
% 6.66/2.00 % (1683853)Termination reason: Instruction limit
% 6.66/2.00 % (1683853)Termination phase: Saturation
% 6.66/2.00 % (1683853)Time elapsed: 0.097 s
% 6.66/2.00 % (1683853)Peak memory usage: 90 MB
% 6.66/2.00 % (1683853)Instructions burned: 158 (million)
% 6.66/2.00 % (1683857)Instruction limit reached!
% 6.66/2.00 % (1683857)------------------------------
% 6.66/2.00 % (1683857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.66/2.00 % (1683857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/2.00 % (1683857)CaDiCaL version: 2.1.3
% 6.66/2.00 % (1683857)Termination reason: Instruction limit
% 6.66/2.00 % (1683857)Termination phase: Saturation
% 6.66/2.00 % (1683857)Time elapsed: 0.056 s
% 6.66/2.00 % (1683857)Peak memory usage: 89 MB
% 6.66/2.00 % (1683857)Instructions burned: 107 (million)
% 6.66/2.00 % (1683861)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2283852116:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 6.66/2.00 % (1683862)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3673140086:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 6.66/2.00 % (1683863)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3159183754:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 6.66/2.00 % (1683861)Instruction limit reached!
% 6.66/2.00 % (1683861)------------------------------
% 6.66/2.00 % (1683861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.66/2.00 % (1683861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/2.00 % (1683861)CaDiCaL version: 2.1.3
% 6.66/2.00 % (1683861)Termination reason: Instruction limit
% 6.66/2.00 % (1683861)Termination phase: Saturation
% 6.66/2.00 % (1683861)Time elapsed: 0.070 s
% 6.66/2.00 % (1683861)Peak memory usage: 89 MB
% 6.66/2.00 % (1683861)Instructions burned: 107 (million)
% 6.66/2.00 % (1683831)First to succeed.
% 6.66/2.00 % (1683831)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1683826"
% 6.66/2.00 % (1683862)Instruction limit reached!
% 6.66/2.00 % (1683862)------------------------------
% 6.66/2.00 % (1683862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.66/2.00 % (1683862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/2.00 % (1683862)CaDiCaL version: 2.1.3
% 6.66/2.00 % (1683862)Termination reason: Instruction limit
% 6.66/2.00 % (1683862)Termination phase: Saturation
% 6.66/2.00 % (1683862)Time elapsed: 0.154 s
% 6.66/2.00 % (1683862)Peak memory usage: 90 MB
% 6.66/2.00 % (1683862)Instructions burned: 242 (million)
% 6.66/2.00 % (1683867)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4182193526:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 6.66/2.00 % (1683855)Also succeeded, but the first one will report.
% 6.66/2.00 % (1683868)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2653576468:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 6.66/2.00 % (1683867)Instruction limit reached!
% 6.66/2.00 % (1683867)------------------------------
% 6.66/2.00 % (1683867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.66/2.00 % (1683867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/2.00 % (1683867)CaDiCaL version: 2.1.3
% 6.66/2.00 % (1683867)Termination reason: Instruction limit
% 6.66/2.00 % (1683867)Termination phase: Saturation
% 6.66/2.00 % (1683867)Time elapsed: 0.093 s
% 6.66/2.00 % (1683867)Peak memory usage: 89 MB
% 6.66/2.00 % (1683867)Instructions burned: 135 (million)
% 6.66/2.00 % (1683831)Refutation found. Thanks to Tanya!
% 6.66/2.00 % SZS status Unsatisfiable for theBenchmark
% 6.66/2.00 % SZS output start Proof for theBenchmark
% See solution above
% 8.66/2.20 % (1683831)------------------------------
% 8.66/2.20 % (1683831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.66/2.20 % (1683831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.66/2.20 % (1683831)CaDiCaL version: 2.1.3
% 8.66/2.20 % (1683831)Termination reason: Refutation
% 8.66/2.20 % (1683831)Time elapsed: 0.735 s
% 8.66/2.20 % (1683831)Peak memory usage: 129 MB
% 8.66/2.20 % (1683831)Instructions burned: 1080 (million)
% 8.66/2.20 % (1683831)------------------------------
% 8.66/2.20 % (1683831)------------------------------
% 8.66/2.20 % (1683826)Success in time 1.145 s
% 8.66/2.20 % Vampire exiting
%------------------------------------------------------------------------------