%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO119-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.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:36 AM UTC 2026
% Result : Unsatisfiable 9.34s 2.15s
% Output : Refutation 9.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 38
% Syntax : Number of formulae : 163 ( 27 unt; 12 def)
% Number of atoms : 410 ( 64 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 435 ( 188 ~; 236 |; 0 &)
% ( 11 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 24 ( 22 usr; 12 prp; 0-4 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-5 aty)
% Number of variables : 143 ( 0 sgn 143 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1] :
( incident_c(ax0_sk1(X0,X1),X0)
| part_of(X0,X1) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',part_of_defn_3) ).
fof(f32,axiom,
! [X0,X1] :
( ~ incident_c(X0,X1)
| end_point(X0,X1)
| inner_point(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inner_point_defn_23) ).
fof(f40,axiom,
! [X0,X1] :
( ~ end_point(X1,X0)
| ~ closed(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',closed_defn_31) ).
fof(f41,axiom,
! [X0] :
( end_point(ax0_sk6(X0),X0)
| closed(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',closed_defn_32) ).
fof(f42,axiom,
! [X0] :
( end_point(ax0_sk7(X0),X0)
| ~ open(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',open_defn_33) ).
fof(f43,axiom,
! [X0,X1] :
( ~ end_point(X0,X1)
| open(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',open_defn_34) ).
fof(f44,axiom,
! [X0,X1] :
( ~ part_of(X0,X1)
| X0 = X1
| open(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c1_35) ).
fof(f51,axiom,
! [X0,X1] :
( end_point(ax0_sk11(X0,X1),X1)
| ~ end_point(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c6_41) ).
fof(f52,axiom,
! [X0,X1] :
( ~ end_point(X0,X1)
| X0 != ax0_sk11(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c6_42) ).
fof(f53,plain,
! [X0,X1] :
( ax0_sk11(X0,X1) != X0
| ~ end_point(X0,X1) ),
inference(reorient_equations,[],[f52]) ).
fof(f66,axiom,
! [X2,X3,X0,X1] :
( ~ between_c(X0,X1,X2,X3)
| X1 != X3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',between_c_defn_1) ).
fof(f71,axiom,
! [X2,X3,X0,X1,X4] :
( ~ inner_point(X4,X2)
| ~ part_of(X2,X3)
| ~ end_point(X0,X2)
| ~ end_point(X1,X2)
| X0 = X1
| between_c(X3,X0,X4,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',between_c_defn_6) ).
fof(f72,axiom,
! [X2,X3,X0,X1] :
( ~ between_o(X0,X1,X2,X3)
| ordered_by(X0,X1,X2)
| ordered_by(X0,X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',between_o_defn_1) ).
fof(f76,axiom,
! [X2,X3,X0,X1] :
( between_o(X0,X1,X2,X3)
| ~ ordered_by(X0,X2,X3)
| ~ ordered_by(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',between_o_defn_5) ).
fof(f78,axiom,
! [X0,X1] :
( ~ start_point(X0,X1)
| incident_o(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',start_point_defn_7) ).
fof(f79,axiom,
! [X2,X0,X1] :
( ordered_by(X1,X0,X2)
| X0 = X2
| ~ incident_o(X2,X1)
| ~ start_point(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',start_point_defn_8) ).
fof(f90,axiom,
! [X2,X0,X1] :
( ~ ordered_by(X0,X1,X2)
| incident_o(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',o1_17) ).
fof(f92,axiom,
! [X0] : open(ax2_sk3(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',o2_19) ).
fof(f93,axiom,
! [X0,X1] :
( incident_c(X0,ax2_sk3(X1))
| ~ incident_o(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',o2_20) ).
fof(f97,axiom,
! [X2,X3,X0,X1] :
( between_c(ax2_sk4(X0,X3,X2,X1),X1,X2,X3)
| ~ between_o(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',o3_24) ).
fof(f98,axiom,
! [X2,X3,X0,X1,X4] :
( incident_o(ax2_sk5(X0,X1,X2,X3,X4),X1)
| incident_c(ax2_sk5(X0,X1,X2,X3,X4),X0)
| ~ between_c(X0,X4,X3,X2)
| between_o(X1,X4,X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',o3_25) ).
fof(f101,axiom,
! [X2,X3,X0,X1,X4] :
( ~ incident_o(ax2_sk5(X0,X1,X2,X3,X4),X1)
| ~ incident_c(ax2_sk5(X0,X1,X2,X3,X4),X0)
| ~ between_c(X0,X4,X3,X2)
| between_o(X1,X4,X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',o3_28) ).
fof(f112,axiom,
! [X2,X0,X1] :
( X0 != underlying_curve(X1)
| ~ incident_o(X2,X1)
| incident_c(X2,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',underlying_curve_defn_37) ).
fof(f113,plain,
! [X2,X0,X1] :
( underlying_curve(X1) != X0
| ~ incident_o(X2,X1)
| incident_c(X2,X0) ),
inference(reorient_equations,[],[f112]) ).
fof(f114,axiom,
! [X2,X0,X1] :
( X0 != underlying_curve(X1)
| ~ incident_c(X2,X0)
| incident_o(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',underlying_curve_defn_38) ).
fof(f115,plain,
! [X2,X0,X1] :
( underlying_curve(X1) != X0
| ~ incident_c(X2,X0)
| incident_o(X2,X1) ),
inference(reorient_equations,[],[f114]) ).
fof(f124,negated_conjecture,
start_point(sk26,sk25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_4_6_1_133) ).
fof(f125,negated_conjecture,
~ end_point(sk26,underlying_curve(sk25)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_4_6_1_134) ).
fof(f130,plain,
! [X2,X3,X0] : ~ between_c(X0,X3,X2,X3),
inference(equality_resolution,[],[f66]) ).
fof(f131,plain,
! [X2,X1] :
( incident_c(X2,underlying_curve(X1))
| ~ incident_o(X2,X1) ),
inference(equality_resolution,[],[f113]) ).
fof(f132,plain,
! [X2,X1] :
( ~ incident_c(X2,underlying_curve(X1))
| incident_o(X2,X1) ),
inference(equality_resolution,[],[f115]) ).
fof(f133,definition,
sF0 = underlying_curve(sk25),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f134,plain,
underlying_curve(sk25) = sF0,
inference(reorient_equations,[],[f133]) ).
fof(f135,plain,
~ end_point(sk26,sF0),
inference(definition_folding,[],[f125,f134]) ).
fof(f138,plain,
! [X0] :
( ~ incident_c(X0,sF0)
| incident_o(X0,sk25) ),
inference(superposition,[],[f132,f134]) ).
fof(f139,plain,
incident_o(sk26,sk25),
inference(resolution,[],[f78,f124]) ).
fof(f141,plain,
! [X0] :
( ~ incident_o(X0,sk25)
| incident_c(X0,sF0) ),
inference(superposition,[],[f131,f134]) ).
fof(f142,plain,
incident_c(sk26,sF0),
inference(resolution,[],[f141,f139]) ).
fof(f143,plain,
! [X2,X0,X1] : ~ between_o(X0,X1,X2,X1),
inference(resolution,[],[f97,f130]) ).
fof(f145,plain,
! [X2,X0,X1] :
( ~ ordered_by(X0,X2,X1)
| ~ ordered_by(X0,X1,X2) ),
inference(resolution,[],[f76,f143]) ).
fof(f146,plain,
! [X2,X0,X1] :
( ~ ordered_by(X0,X1,X2)
| X1 = X2
| ~ incident_o(X1,X0)
| ~ start_point(X2,X0) ),
inference(resolution,[],[f145,f79]) ).
fof(f147,plain,
! [X2,X0,X1] :
( ~ ordered_by(X0,X1,X2)
| X1 = X2
| ~ start_point(X2,X0) ),
inference(forward_subsumption_resolution,[],[f146,f90]) ).
fof(f178,definition,
( spl1_2
<=> open(sF0) ),
introduced(definition,[new_symbols(definition,[spl1_2])],[avatar_definition]) ).
fof(f179,plain,
( open(sF0)
| ~ spl1_2 ),
inference(avatar_component_clause,[],[f178]) ).
fof(f180,plain,
( ~ open(sF0)
| spl1_2 ),
inference(avatar_component_clause,[],[f178]) ).
fof(f186,plain,
( end_point(sk26,sF0)
| inner_point(sk26,sF0) ),
inference(resolution,[],[f32,f142]) ).
fof(f187,plain,
inner_point(sk26,sF0),
inference(forward_subsumption_resolution,[],[f186,f135]) ).
fof(f201,plain,
! [X0] :
( ~ open(X0)
| ~ closed(X0) ),
inference(resolution,[],[f40,f42]) ).
fof(f208,plain,
! [X2,X0,X1] :
( between_c(X0,X1,sk26,X2)
| ~ end_point(X1,sF0)
| ~ end_point(X2,sF0)
| X1 = X2
| ~ part_of(sF0,X0) ),
inference(resolution,[],[f71,f187]) ).
fof(f236,plain,
! [X0,X1] :
( ~ incident_o(ax0_sk1(X0,ax2_sk3(X1)),X1)
| part_of(X0,ax2_sk3(X1)) ),
inference(resolution,[],[f3,f93]) ).
fof(f254,plain,
! [X0] :
( part_of(X0,X0)
| part_of(X0,X0) ),
inference(resolution,[],[f2,f3]) ).
fof(f258,plain,
! [X0] :
( incident_o(ax0_sk1(sF0,X0),sk25)
| part_of(sF0,X0) ),
inference(resolution,[],[f2,f138]) ).
fof(f259,plain,
! [X0] : part_of(X0,X0),
inference(duplicate_literal_removal,[],[f254]) ).
fof(f436,definition,
( spl1_8
<=> closed(sF0) ),
introduced(definition,[new_symbols(definition,[spl1_8])],[avatar_definition]) ).
fof(f437,plain,
( ~ closed(sF0)
| spl1_8 ),
inference(avatar_component_clause,[],[f436]) ).
fof(f438,plain,
( closed(sF0)
| ~ spl1_8 ),
inference(avatar_component_clause,[],[f436]) ).
fof(f455,definition,
( spl1_11
<=> end_point(ax0_sk6(sF0),sF0) ),
introduced(definition,[new_symbols(definition,[spl1_11])],[avatar_definition]) ).
fof(f456,plain,
( ~ end_point(ax0_sk6(sF0),sF0)
| spl1_11 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f457,plain,
( end_point(ax0_sk6(sF0),sF0)
| ~ spl1_11 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f781,plain,
( part_of(sF0,ax2_sk3(sk25))
| part_of(sF0,ax2_sk3(sk25)) ),
inference(resolution,[],[f236,f258]) ).
fof(f786,plain,
part_of(sF0,ax2_sk3(sk25)),
inference(duplicate_literal_removal,[],[f781]) ).
fof(f841,plain,
! [X2,X3,X0,X1] :
( incident_c(ax2_sk5(X0,sk25,X1,X2,X3),sF0)
| incident_c(ax2_sk5(X0,sk25,X1,X2,X3),X0)
| between_o(sk25,X3,X2,X1)
| ~ between_c(X0,X3,X2,X1) ),
inference(resolution,[],[f98,f141]) ).
fof(f884,plain,
! [X2,X0,X1] :
( incident_c(ax2_sk5(sF0,sk25,X0,X1,X2),sF0)
| between_o(sk25,X2,X1,X0)
| ~ between_c(sF0,X2,X1,X0) ),
inference(factoring,[],[f841]) ).
fof(f885,plain,
! [X2,X0,X1] :
( incident_o(ax2_sk5(sF0,sk25,X2,X1,X0),sk25)
| ~ between_c(sF0,X0,X1,X2)
| between_o(sk25,X0,X1,X2) ),
inference(resolution,[],[f884,f138]) ).
fof(f888,plain,
! [X2,X0,X1] :
( ~ between_c(sF0,X0,X1,X2)
| between_o(sk25,X0,X1,X2)
| ~ incident_c(ax2_sk5(sF0,sk25,X2,X1,X0),sF0)
| ~ between_c(sF0,X0,X1,X2)
| between_o(sk25,X0,X1,X2) ),
inference(resolution,[],[f885,f101]) ).
fof(f892,plain,
! [X2,X0,X1] :
( ~ between_c(sF0,X0,X1,X2)
| between_o(sk25,X0,X1,X2)
| ~ incident_c(ax2_sk5(sF0,sk25,X2,X1,X0),sF0) ),
inference(duplicate_literal_removal,[],[f888]) ).
fof(f893,plain,
! [X2,X0,X1] :
( ~ between_c(sF0,X0,X1,X2)
| between_o(sk25,X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f892,f884]) ).
fof(f895,plain,
! [X0,X1] :
( between_o(sk25,X0,sk26,X1)
| ~ end_point(X0,sF0)
| ~ end_point(X1,sF0)
| X0 = X1
| ~ part_of(sF0,sF0) ),
inference(resolution,[],[f893,f208]) ).
fof(f897,plain,
! [X0,X1] :
( between_o(sk25,X0,sk26,X1)
| ~ end_point(X0,sF0)
| ~ end_point(X1,sF0)
| X0 = X1 ),
inference(forward_subsumption_resolution,[],[f895,f259]) ).
fof(f902,plain,
! [X0,X1] :
( ordered_by(sk25,X1,sk26)
| ordered_by(sk25,X0,sk26)
| X0 = X1
| ~ end_point(X1,sF0)
| ~ end_point(X0,sF0) ),
inference(resolution,[],[f897,f72]) ).
fof(f920,plain,
! [X0,X1] :
( ordered_by(sk25,X1,sk26)
| X0 = X1
| ~ end_point(X1,sF0)
| ~ end_point(X0,sF0)
| sk26 = X0
| ~ start_point(sk26,sk25) ),
inference(resolution,[],[f902,f147]) ).
fof(f930,plain,
! [X0,X1] :
( ~ end_point(X1,sF0)
| X0 = X1
| ordered_by(sk25,X1,sk26)
| ~ end_point(X0,sF0)
| sk26 = X0 ),
inference(forward_subsumption_resolution,[],[f920,f124]) ).
fof(f943,plain,
! [X0] :
( ax0_sk7(sF0) = X0
| ordered_by(sk25,ax0_sk7(sF0),sk26)
| ~ end_point(X0,sF0)
| sk26 = X0
| ~ open(sF0) ),
inference(resolution,[],[f930,f42]) ).
fof(f944,plain,
! [X0,X1] :
( ~ end_point(X1,sF0)
| ordered_by(sk25,ax0_sk11(X1,sF0),sk26)
| ~ end_point(X0,sF0)
| sk26 = X0
| ax0_sk11(X1,sF0) = X0 ),
inference(resolution,[],[f930,f51]) ).
fof(f1012,plain,
! [X0] :
( ordered_by(sk25,ax0_sk11(ax0_sk6(sF0),sF0),sk26)
| ~ end_point(X0,sF0)
| sk26 = X0
| ax0_sk11(ax0_sk6(sF0),sF0) = X0
| closed(sF0) ),
inference(resolution,[],[f944,f41]) ).
fof(f1592,plain,
( sF0 = ax2_sk3(sk25)
| open(sF0) ),
inference(resolution,[],[f44,f786]) ).
fof(f1596,plain,
( sF0 = ax2_sk3(sk25)
| spl1_2 ),
inference(forward_subsumption_resolution,[],[f1592,f180]) ).
fof(f1615,plain,
( open(sF0)
| spl1_2 ),
inference(superposition,[],[f92,f1596]) ).
fof(f1635,plain,
( $false
| spl1_2 ),
inference(forward_subsumption_resolution,[],[f1615,f180]) ).
fof(f1636,plain,
spl1_2,
inference(avatar_contradiction_clause,[],[f1635]) ).
fof(f1648,plain,
! [X0] :
( ax0_sk7(sF0) = X0
| ordered_by(sk25,ax0_sk7(sF0),sk26)
| ~ end_point(X0,sF0)
| sk26 = X0 ),
inference(forward_subsumption_resolution,[],[f943,f43]) ).
fof(f1662,definition,
( spl1_34
<=> ordered_by(sk25,ax0_sk7(sF0),sk26) ),
introduced(definition,[new_symbols(definition,[spl1_34])],[avatar_definition]) ).
fof(f1664,plain,
( ordered_by(sk25,ax0_sk7(sF0),sk26)
| ~ spl1_34 ),
inference(avatar_component_clause,[],[f1662]) ).
fof(f1666,definition,
( spl1_35
<=> ! [X0] :
( ax0_sk7(sF0) = X0
| sk26 = X0
| ~ end_point(X0,sF0) ) ),
introduced(definition,[new_symbols(definition,[spl1_35])],[avatar_definition]) ).
fof(f1667,plain,
( ! [X0] :
( ~ end_point(X0,sF0)
| sk26 = X0
| ax0_sk7(sF0) = X0 )
| ~ spl1_35 ),
inference(avatar_component_clause,[],[f1666]) ).
fof(f1668,plain,
( spl1_34
| spl1_35 ),
inference(avatar_split_clause,[],[f1648,f1666,f1662]) ).
fof(f1720,plain,
( sk26 = ax0_sk7(sF0)
| ~ start_point(sk26,sk25)
| ~ spl1_34 ),
inference(resolution,[],[f1664,f147]) ).
fof(f1725,definition,
( spl1_46
<=> sk26 = ax0_sk7(sF0) ),
introduced(definition,[new_symbols(definition,[spl1_46])],[avatar_definition]) ).
fof(f1727,plain,
( sk26 = ax0_sk7(sF0)
| ~ spl1_46 ),
inference(avatar_component_clause,[],[f1725]) ).
fof(f1733,plain,
( sk26 = ax0_sk7(sF0)
| ~ spl1_34 ),
inference(forward_subsumption_resolution,[],[f1720,f124]) ).
fof(f1736,plain,
( spl1_46
| ~ spl1_34 ),
inference(avatar_split_clause,[],[f1733,f1662,f1725]) ).
fof(f1744,plain,
( end_point(sk26,sF0)
| ~ open(sF0)
| ~ spl1_46 ),
inference(superposition,[],[f42,f1727]) ).
fof(f1745,plain,
( ~ open(sF0)
| ~ spl1_46 ),
inference(forward_subsumption_resolution,[],[f1744,f135]) ).
fof(f1748,plain,
( $false
| ~ spl1_2
| ~ spl1_46 ),
inference(forward_subsumption_resolution,[],[f1745,f179]) ).
fof(f1749,plain,
( ~ spl1_2
| ~ spl1_46 ),
inference(avatar_contradiction_clause,[],[f1748]) ).
fof(f1752,plain,
( sk26 = ax0_sk6(sF0)
| ax0_sk7(sF0) = ax0_sk6(sF0)
| closed(sF0)
| ~ spl1_35 ),
inference(resolution,[],[f1667,f41]) ).
fof(f1876,plain,
( ~ closed(sF0)
| ~ spl1_2 ),
inference(resolution,[],[f179,f201]) ).
fof(f1877,plain,
( $false
| ~ spl1_2
| ~ spl1_8 ),
inference(forward_subsumption_resolution,[],[f1876,f438]) ).
fof(f1878,plain,
( ~ spl1_2
| ~ spl1_8 ),
inference(avatar_contradiction_clause,[],[f1877]) ).
fof(f1882,plain,
! [X0] :
( ordered_by(sk25,ax0_sk11(ax0_sk6(sF0),sF0),sk26)
| ~ end_point(X0,sF0)
| sk26 = X0
| ax0_sk11(ax0_sk6(sF0),sF0) = X0 ),
inference(forward_subsumption_resolution,[],[f1012,f40]) ).
fof(f1890,plain,
( sk26 = ax0_sk6(sF0)
| ax0_sk7(sF0) = ax0_sk6(sF0)
| spl1_8
| ~ spl1_35 ),
inference(forward_subsumption_resolution,[],[f1752,f437]) ).
fof(f1903,definition,
( spl1_50
<=> ! [X0] :
( ~ end_point(X0,sF0)
| ax0_sk11(ax0_sk6(sF0),sF0) = X0
| sk26 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl1_50])],[avatar_definition]) ).
fof(f1904,plain,
( ! [X0] :
( ~ end_point(X0,sF0)
| ax0_sk11(ax0_sk6(sF0),sF0) = X0
| sk26 = X0 )
| ~ spl1_50 ),
inference(avatar_component_clause,[],[f1903]) ).
fof(f1906,definition,
( spl1_51
<=> ordered_by(sk25,ax0_sk11(ax0_sk6(sF0),sF0),sk26) ),
introduced(definition,[new_symbols(definition,[spl1_51])],[avatar_definition]) ).
fof(f1908,plain,
( ordered_by(sk25,ax0_sk11(ax0_sk6(sF0),sF0),sk26)
| ~ spl1_51 ),
inference(avatar_component_clause,[],[f1906]) ).
fof(f1909,plain,
( spl1_50
| spl1_51 ),
inference(avatar_split_clause,[],[f1882,f1906,f1903]) ).
fof(f1938,definition,
( spl1_58
<=> ax0_sk7(sF0) = ax0_sk6(sF0) ),
introduced(definition,[new_symbols(definition,[spl1_58])],[avatar_definition]) ).
fof(f1940,plain,
( ax0_sk7(sF0) = ax0_sk6(sF0)
| ~ spl1_58 ),
inference(avatar_component_clause,[],[f1938]) ).
fof(f1942,definition,
( spl1_59
<=> sk26 = ax0_sk6(sF0) ),
introduced(definition,[new_symbols(definition,[spl1_59])],[avatar_definition]) ).
fof(f1943,plain,
( sk26 != ax0_sk6(sF0)
| spl1_59 ),
inference(avatar_component_clause,[],[f1942]) ).
fof(f1944,plain,
( sk26 = ax0_sk6(sF0)
| ~ spl1_59 ),
inference(avatar_component_clause,[],[f1942]) ).
fof(f1945,plain,
( spl1_58
| spl1_59
| spl1_8
| ~ spl1_35 ),
inference(avatar_split_clause,[],[f1890,f1666,f436,f1942,f1938]) ).
fof(f1947,definition,
( spl1_60
<=> sk26 = ax0_sk11(ax0_sk6(sF0),sF0) ),
introduced(definition,[new_symbols(definition,[spl1_60])],[avatar_definition]) ).
fof(f1948,plain,
( sk26 != ax0_sk11(ax0_sk6(sF0),sF0)
| spl1_60 ),
inference(avatar_component_clause,[],[f1947]) ).
fof(f1949,plain,
( sk26 = ax0_sk11(ax0_sk6(sF0),sF0)
| ~ spl1_60 ),
inference(avatar_component_clause,[],[f1947]) ).
fof(f1983,plain,
( end_point(sk26,sF0)
| closed(sF0)
| ~ spl1_59 ),
inference(superposition,[],[f41,f1944]) ).
fof(f1984,plain,
( closed(sF0)
| ~ spl1_59 ),
inference(forward_subsumption_resolution,[],[f1983,f135]) ).
fof(f1987,plain,
( $false
| spl1_8
| ~ spl1_59 ),
inference(forward_subsumption_resolution,[],[f1984,f437]) ).
fof(f1988,plain,
( spl1_8
| ~ spl1_59 ),
inference(avatar_contradiction_clause,[],[f1987]) ).
fof(f1992,plain,
( ax0_sk6(sF0) = ax0_sk11(ax0_sk6(sF0),sF0)
| sk26 = ax0_sk6(sF0)
| closed(sF0)
| ~ spl1_50 ),
inference(resolution,[],[f1904,f41]) ).
fof(f1998,plain,
( ax0_sk6(sF0) = ax0_sk11(ax0_sk6(sF0),sF0)
| closed(sF0)
| ~ spl1_50
| spl1_59 ),
inference(forward_subsumption_resolution,[],[f1992,f1943]) ).
fof(f2000,plain,
( ax0_sk6(sF0) = ax0_sk11(ax0_sk6(sF0),sF0)
| spl1_8
| ~ spl1_50
| spl1_59 ),
inference(forward_subsumption_resolution,[],[f1998,f437]) ).
fof(f2033,plain,
( end_point(ax0_sk6(sF0),sF0)
| ~ open(sF0)
| ~ spl1_58 ),
inference(superposition,[],[f42,f1940]) ).
fof(f2042,plain,
( ax0_sk6(sF0) != ax0_sk6(sF0)
| ~ end_point(ax0_sk6(sF0),sF0)
| spl1_8
| ~ spl1_50
| spl1_59 ),
inference(superposition,[],[f53,f2000]) ).
fof(f2045,plain,
( ~ end_point(ax0_sk6(sF0),sF0)
| spl1_8
| ~ spl1_50
| spl1_59 ),
inference(trivial_inequality_removal,[],[f2042]) ).
fof(f2046,plain,
( $false
| spl1_8
| ~ spl1_11
| ~ spl1_50
| spl1_59 ),
inference(forward_subsumption_resolution,[],[f2045,f457]) ).
fof(f2047,plain,
( spl1_8
| ~ spl1_11
| ~ spl1_50
| spl1_59 ),
inference(avatar_contradiction_clause,[],[f2046]) ).
fof(f2048,plain,
( ~ open(sF0)
| spl1_11
| ~ spl1_58 ),
inference(forward_subsumption_resolution,[],[f2033,f456]) ).
fof(f2049,plain,
( $false
| ~ spl1_2
| spl1_11
| ~ spl1_58 ),
inference(forward_subsumption_resolution,[],[f2048,f179]) ).
fof(f2050,plain,
( ~ spl1_2
| spl1_11
| ~ spl1_58 ),
inference(avatar_contradiction_clause,[],[f2049]) ).
fof(f2058,plain,
( sk26 = ax0_sk11(ax0_sk6(sF0),sF0)
| ~ start_point(sk26,sk25)
| ~ spl1_51 ),
inference(resolution,[],[f1908,f147]) ).
fof(f2064,plain,
( ~ start_point(sk26,sk25)
| ~ spl1_51
| spl1_60 ),
inference(forward_subsumption_resolution,[],[f2058,f1948]) ).
fof(f2069,plain,
( $false
| ~ spl1_51
| spl1_60 ),
inference(forward_subsumption_resolution,[],[f2064,f124]) ).
fof(f2070,plain,
( ~ spl1_51
| spl1_60 ),
inference(avatar_contradiction_clause,[],[f2069]) ).
fof(f2112,plain,
( end_point(sk26,sF0)
| ~ end_point(ax0_sk6(sF0),sF0)
| ~ spl1_60 ),
inference(superposition,[],[f51,f1949]) ).
fof(f2113,plain,
( ~ end_point(ax0_sk6(sF0),sF0)
| ~ spl1_60 ),
inference(forward_subsumption_resolution,[],[f2112,f135]) ).
fof(f2116,plain,
( $false
| ~ spl1_11
| ~ spl1_60 ),
inference(forward_subsumption_resolution,[],[f2113,f457]) ).
fof(f2117,plain,
( ~ spl1_11
| ~ spl1_60 ),
inference(avatar_contradiction_clause,[],[f2116]) ).
cnf(s44,plain,
spl1_2,
inference(sat_conversion,[],[f1636]) ).
cnf(s47,plain,
( spl1_34
| spl1_35 ),
inference(sat_conversion,[],[f1668]) ).
cnf(s58,plain,
( ~ spl1_34
| spl1_46 ),
inference(sat_conversion,[],[f1736]) ).
cnf(s60,plain,
( ~ spl1_2
| ~ spl1_46 ),
inference(sat_conversion,[],[f1749]) ).
cnf(s62,plain,
( ~ spl1_2
| ~ spl1_8 ),
inference(sat_conversion,[],[f1878]) ).
cnf(s64,plain,
( spl1_50
| spl1_51 ),
inference(sat_conversion,[],[f1909]) ).
cnf(s71,plain,
( spl1_8
| ~ spl1_35
| spl1_58
| spl1_59 ),
inference(sat_conversion,[],[f1945]) ).
cnf(s81,plain,
( spl1_8
| ~ spl1_59 ),
inference(sat_conversion,[],[f1988]) ).
cnf(s85,plain,
( spl1_8
| ~ spl1_11
| ~ spl1_50
| spl1_59 ),
inference(sat_conversion,[],[f2047]) ).
cnf(s86,plain,
( ~ spl1_2
| spl1_11
| ~ spl1_58 ),
inference(sat_conversion,[],[f2050]) ).
cnf(s87,plain,
( ~ spl1_51
| spl1_60 ),
inference(sat_conversion,[],[f2070]) ).
cnf(s92,plain,
( ~ spl1_11
| ~ spl1_60 ),
inference(sat_conversion,[],[f2117]) ).
cnf(s93,plain,
~ spl1_8,
inference(rat,[],[s62,s44]) ).
cnf(s94,plain,
~ spl1_46,
inference(rat,[],[s60,s44]) ).
cnf(s95,plain,
~ spl1_59,
inference(rat,[],[s81,s93]) ).
cnf(s96,plain,
~ spl1_34,
inference(rat,[],[s58,s94]) ).
cnf(s100,plain,
spl1_35,
inference(rat,[],[s47,s96]) ).
cnf(s104,plain,
spl1_58,
inference(rat,[],[s71,s95,s93,s100]) ).
cnf(s105,plain,
spl1_11,
inference(rat,[],[s86,s44,s104]) ).
cnf(s106,plain,
~ spl1_60,
inference(rat,[],[s92,s105]) ).
cnf(s107,plain,
~ spl1_50,
inference(rat,[],[s85,s95,s93,s105]) ).
cnf(s108,plain,
~ spl1_51,
inference(rat,[],[s87,s106]) ).
cnf(s110,plain,
$false,
inference(rat,[],[s64,s108,s107]) ).
fof(f2118,plain,
$false,
inference(avatar_sat_refutation,[],[s110]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO119-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n017.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 07:00:50 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 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
% 9.34/2.15 % (2202988)Input is clausal, will run a generic CNF schedule.
% 9.34/2.15 % (2202995)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3655275713:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.34/2.15 % (2202997)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1489456818:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.34/2.15 % (2202994)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3723817433:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.34/2.15 % (2202998)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3570564093:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.34/2.15 % (2202993)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=2618725871:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.34/2.15 % (2202996)lrs+10_1_sil=8000:sp=occurrence:random_seed=2395726832:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.34/2.15 % (2202999)dis-21_1_sil=8000:lcm=predicate:random_seed=778223390: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)
% 9.34/2.15 % (2202997)Refutation not found, incomplete strategy
% 9.34/2.15 % (2202997)------------------------------
% 9.34/2.15 % (2202997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.34/2.15 % (2202996)Refutation not found, incomplete strategy
% 9.34/2.15 % (2202996)------------------------------
% 9.34/2.15 % (2202996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.34/2.15 % (2202997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/2.15 % (2202997)CaDiCaL version: 2.1.3
% 9.34/2.15 % (2202997)Termination reason: Refutation not found, incomplete strategy
% 9.34/2.15 % (2202997)Time elapsed: 0.002 s
% 9.34/2.15 % (2202997)Peak memory usage: 88 MB
% 9.34/2.15 % (2202996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/2.15 % (2202997)Instructions burned: 1 (million)
% 9.34/2.15 % (2202996)CaDiCaL version: 2.1.3
% 9.34/2.15 % (2202996)Termination reason: Refutation not found, incomplete strategy
% 9.34/2.15 % (2202996)Time elapsed: 0.002 s
% 9.34/2.15 % (2202996)Peak memory usage: 87 MB
% 9.34/2.15 % (2202996)Instructions burned: 1 (million)
% 9.34/2.15 % (2202999)Instruction limit reached!
% 9.34/2.15 % (2202999)------------------------------
% 9.34/2.15 % (2202999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.34/2.15 % (2202999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/2.15 % (2202999)CaDiCaL version: 2.1.3
% 9.34/2.15 % (2202999)Termination reason: Instruction limit
% 9.34/2.15 % (2202999)Termination phase: Saturation
% 9.34/2.15 % (2202999)Time elapsed: 0.055 s
% 9.34/2.15 % (2202999)Peak memory usage: 89 MB
% 9.34/2.15 % (2202999)Instructions burned: 118 (million)
% 9.34/2.15 % (2202998)Instruction limit reached!
% 9.34/2.15 % (2202998)------------------------------
% 9.34/2.15 % (2202998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.34/2.15 % (2202998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/2.15 % (2202998)CaDiCaL version: 2.1.3
% 9.34/2.15 % (2202998)Termination reason: Instruction limit
% 9.34/2.15 % (2202998)Termination phase: Saturation
% 9.34/2.15 % (2202998)Time elapsed: 0.119 s
% 9.34/2.15 % (2202998)Peak memory usage: 89 MB
% 9.34/2.15 % (2202998)Instructions burned: 181 (million)
% 9.34/2.15 % (2203007)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=4286073155:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 9.34/2.15 % (2203007)Refutation not found, incomplete strategy
% 9.34/2.15 % (2203007)------------------------------
% 9.34/2.15 % (2203007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.34/2.15 % (2203007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/2.15 % (2203007)CaDiCaL version: 2.1.3
% 9.34/2.15 % (2203007)Termination reason: Refutation not found, incomplete strategy
% 9.34/2.15 % (2203007)Time elapsed: 0.001 s
% 9.34/2.15 % (2203007)Peak memory usage: 88 MB
% 9.34/2.15 % (2203007)Instructions burned: 1 (million)
% 9.34/2.15 % (2202997)------------------------------
% 9.34/2.15 % (2202997)------------------------------
% 9.34/2.15 % (2202996)------------------------------
% 9.34/2.15 % (2202996)------------------------------
% 9.34/2.15 % (2203008)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=753825767: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)
% 9.34/2.15 % (2203008)Instruction limit reached!
% 9.34/2.15 % (2203008)------------------------------
% 9.34/2.15 % (2203008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.34/2.15 % (2203008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/2.15 % (2203008)CaDiCaL version: 2.1.3
% 9.34/2.15 % (2203008)Termination reason: Instruction limit
% 9.34/2.15 % (2203008)Termination phase: Saturation
% 9.34/2.15 % (2203008)Time elapsed: 0.100 s
% 9.34/2.15 % (2203008)Peak memory usage: 89 MB
% 9.34/2.15 % (2203008)Instructions burned: 191 (million)
% 9.34/2.15 % (2203011)lrs+10_64_to=lpo:sil=8000:random_seed=3272840244:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 9.34/2.15 % (2203010)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3793984539:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 9.34/2.15 % (2203010)Refutation not found, incomplete strategy
% 9.34/2.15 % (2203010)------------------------------
% 9.34/2.15 % (2203010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.34/2.15 % (2203010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/2.15 % (2203010)CaDiCaL version: 2.1.3
% 9.34/2.15 % (2203010)Termination reason: Refutation not found, incomplete strategy
% 9.34/2.15 % (2203010)Time elapsed: 0.002 s
% 9.34/2.15 % (2203010)Peak memory usage: 88 MB
% 9.34/2.15 % (2203010)Instructions burned: 3 (million)
% 9.34/2.15 % (2203007)------------------------------
% 9.34/2.15 % (2203007)------------------------------
% 9.34/2.15 % (2203011)Instruction limit reached!
% 9.34/2.15 % (2203011)------------------------------
% 9.34/2.15 % (2203011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.34/2.15 % (2203011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/2.15 % (2203011)CaDiCaL version: 2.1.3
% 9.34/2.15 % (2203011)Termination reason: Instruction limit
% 9.34/2.15 % (2203011)Termination phase: Saturation
% 9.34/2.15 % (2203011)Time elapsed: 0.075 s
% 9.34/2.15 % (2203011)Peak memory usage: 89 MB
% 9.34/2.15 % (2203011)Instructions burned: 126 (million)
% 9.34/2.15 % (2203013)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=687518668:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 9.34/2.15 % (2203016)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1520809505:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 9.34/2.15 % (2203017)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4055800894:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 9.34/2.15 % (2203013)Instruction limit reached!
% 9.34/2.15 % (2203013)------------------------------
% 9.34/2.15 % (2203013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.34/2.15 % (2203013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/2.15 % (2203013)CaDiCaL version: 2.1.3
% 9.34/2.15 % (2203013)Termination reason: Instruction limit
% 9.34/2.15 % (2203013)Termination phase: Saturation
% 9.34/2.15 % (2203013)Time elapsed: 0.124 s
% 9.34/2.15 % (2203013)Peak memory usage: 90 MB
% 9.34/2.15 % (2203013)Instructions burned: 194 (million)
% 9.34/2.15 % (2203010)------------------------------
% 9.34/2.15 % (2203010)------------------------------
% 9.34/2.15 % (2203016)Instruction limit reached!
% 9.34/2.15 % (2203016)------------------------------
% 9.34/2.15 % (2203016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.34/2.15 % (2203016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/2.15 % (2203016)CaDiCaL version: 2.1.3
% 9.34/2.15 % (2203016)Termination reason: Instruction limit
% 9.34/2.15 % (2203016)Termination phase: Saturation
% 9.34/2.15 % (2203016)Time elapsed: 0.106 s
% 9.34/2.15 % (2203016)Peak memory usage: 90 MB
% 9.34/2.15 % (2203016)Instructions burned: 158 (million)
% 9.34/2.15 % (2203021)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=1744631563:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 9.34/2.15 % (2203021)Refutation not found, incomplete strategy
% 9.34/2.15 % (2203021)------------------------------
% 9.34/2.15 % (2203021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.34/2.15 % (2203021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/2.15 % (2203021)CaDiCaL version: 2.1.3
% 9.34/2.15 % (2203021)Termination reason: Refutation not found, incomplete strategy
% 9.34/2.15 % (2203021)Time elapsed: 0.002 s
% 9.34/2.15 % (2203021)Peak memory usage: 88 MB
% 9.34/2.15 % (2203021)Instructions burned: 1 (million)
% 9.34/2.15 % (2203022)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2962613493:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 9.34/2.15 % (2203023)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2541814896:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 9.34/2.15 % (2203022)Instruction limit reached!
% 9.34/2.15 % (2203022)------------------------------
% 9.34/2.15 % (2203022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.34/2.15 % (2203022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/2.15 % (2203022)CaDiCaL version: 2.1.3
% 9.34/2.15 % (2203022)Termination reason: Instruction limit
% 9.34/2.15 % (2203022)Termination phase: Saturation
% 9.34/2.15 % (2203022)Time elapsed: 0.068 s
% 9.34/2.15 % (2203022)Peak memory usage: 88 MB
% 9.34/2.15 % (2203022)Instructions burned: 107 (million)
% 9.34/2.15 % (2202993)First to succeed.
% 9.34/2.15 % (2202993)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2202988"
% 9.34/2.15 % (2203023)Instruction limit reached!
% 9.34/2.15 % (2203023)------------------------------
% 9.34/2.15 % (2203023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.34/2.15 % (2203023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/2.15 % (2203023)CaDiCaL version: 2.1.3
% 9.34/2.15 % (2203023)Termination reason: Instruction limit
% 9.34/2.15 % (2203023)Termination phase: Saturation
% 9.34/2.15 % (2203023)Time elapsed: 0.152 s
% 9.34/2.15 % (2203023)Peak memory usage: 89 MB
% 9.34/2.15 % (2203023)Instructions burned: 242 (million)
% 9.34/2.15 % (2203027)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=122265183:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 9.34/2.15 % (2203021)------------------------------
% 9.34/2.15 % (2203021)------------------------------
% 9.34/2.15 % (2203028)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2606651867:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 9.34/2.15 % (2203030)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=772014898:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 9.34/2.15 % (2202993)Refutation found. Thanks to Tanya!
% 9.34/2.15 % SZS status Unsatisfiable for theBenchmark
% 9.34/2.15 % SZS output start Proof for theBenchmark
% See solution above
% 9.69/2.35 % (2202993)------------------------------
% 9.69/2.35 % (2202993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.69/2.35 % (2202993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.69/2.35 % (2202993)CaDiCaL version: 2.1.3
% 9.69/2.35 % (2202993)Termination reason: Refutation
% 9.69/2.35 % (2202993)Time elapsed: 0.875 s
% 9.69/2.35 % (2202993)Peak memory usage: 132 MB
% 9.69/2.35 % (2202993)Instructions burned: 1282 (million)
% 9.69/2.35 % (2202993)------------------------------
% 9.69/2.35 % (2202993)------------------------------
% 9.69/2.35 % (2202988)Success in time 1.29 s
% 9.69/2.35 % Vampire exiting
%------------------------------------------------------------------------------