%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO121-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 : n018.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:37 AM UTC 2026
% Result : Unsatisfiable 11.18s 2.44s
% Output : Refutation 11.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 40
% Syntax : Number of formulae : 186 ( 29 unt; 12 def)
% Number of atoms : 551 ( 102 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 615 ( 250 ~; 354 |; 0 &)
% ( 11 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 12 prp; 0-4 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-5 aty)
% Number of variables : 183 ( 0 sgn 183 !; 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(f22,axiom,
! [X0,X1] :
( ~ end_point(X0,X1)
| incident_c(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',end_point_defn_13) ).
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(f50,axiom,
! [X2,X3,X0,X1] :
( ~ end_point(X3,X1)
| ~ end_point(X2,X1)
| ~ end_point(X0,X1)
| X0 = X2
| X0 = X3
| X2 = X3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c5_40) ).
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(f75,axiom,
! [X2,X3,X0,X1] :
( ~ between_o(X0,X1,X2,X3)
| ordered_by(X0,X2,X3)
| ordered_by(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',between_o_defn_4) ).
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(f86,axiom,
! [X0,X1] :
( ~ incident_o(X0,X1)
| X0 != ax2_sk2(X1,X0)
| finish_point(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finish_point_defn_14) ).
fof(f87,plain,
! [X0,X1] :
( ax2_sk2(X1,X0) != X0
| ~ incident_o(X0,X1)
| finish_point(X0,X1) ),
inference(reorient_equations,[],[f86]) ).
fof(f88,axiom,
! [X0,X1] :
( incident_o(ax2_sk2(X1,X0),X1)
| ~ incident_o(X0,X1)
| finish_point(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finish_point_defn_15) ).
fof(f89,axiom,
! [X0,X1] :
( ~ incident_o(X0,X1)
| ~ ordered_by(X1,ax2_sk2(X1,X0),X0)
| finish_point(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finish_point_defn_16) ).
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(f91,axiom,
! [X2,X0,X1] :
( ~ ordered_by(X0,X1,X2)
| incident_o(X2,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',o1_18) ).
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(f102,axiom,
! [X0] : start_point(ax2_sk6(X0),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',o4_29) ).
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,
end_point(sk26,underlying_curve(sk25)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_4_7_133) ).
fof(f125,negated_conjecture,
~ start_point(sk26,sk25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_4_7_134) ).
fof(f126,negated_conjecture,
~ finish_point(sk26,sk25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_4_7_135) ).
fof(f131,plain,
! [X2,X3,X0] : ~ between_c(X0,X3,X2,X3),
inference(equality_resolution,[],[f66]) ).
fof(f132,plain,
! [X2,X1] :
( incident_c(X2,underlying_curve(X1))
| ~ incident_o(X2,X1) ),
inference(equality_resolution,[],[f113]) ).
fof(f133,plain,
! [X2,X1] :
( ~ incident_c(X2,underlying_curve(X1))
| incident_o(X2,X1) ),
inference(equality_resolution,[],[f115]) ).
fof(f134,definition,
sF0 = underlying_curve(sk25),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f135,plain,
underlying_curve(sk25) = sF0,
inference(reorient_equations,[],[f134]) ).
fof(f136,plain,
end_point(sk26,sF0),
inference(definition_folding,[],[f124,f135]) ).
fof(f137,plain,
! [X0,X1] :
( ~ ordered_by(X1,ax2_sk2(X1,X0),X0)
| finish_point(X0,X1) ),
inference(forward_subsumption_resolution,[],[f89,f91]) ).
fof(f139,plain,
! [X0] :
( ~ incident_c(X0,sF0)
| incident_o(X0,sk25) ),
inference(superposition,[],[f133,f135]) ).
fof(f140,plain,
incident_c(sk26,sF0),
inference(resolution,[],[f22,f136]) ).
fof(f142,plain,
! [X0] :
( ~ incident_o(X0,sk25)
| incident_c(X0,sF0) ),
inference(superposition,[],[f132,f135]) ).
fof(f143,plain,
! [X2,X0,X1] : ~ between_o(X0,X1,X2,X1),
inference(resolution,[],[f131,f97]) ).
fof(f144,plain,
incident_o(sk26,sk25),
inference(resolution,[],[f140,f139]) ).
fof(f148,plain,
! [X2,X0,X1] :
( ~ ordered_by(X0,X2,X1)
| ~ ordered_by(X0,X1,X2) ),
inference(resolution,[],[f76,f143]) ).
fof(f150,plain,
! [X0] :
( incident_c(ax2_sk2(sk25,X0),sF0)
| finish_point(X0,sk25)
| ~ incident_o(X0,sk25) ),
inference(resolution,[],[f88,f142]) ).
fof(f163,plain,
! [X0,X1] :
( ax2_sk2(X0,X1) = X1
| ~ incident_o(X1,X0)
| ~ start_point(ax2_sk2(X0,X1),X0)
| finish_point(X1,X0) ),
inference(resolution,[],[f79,f137]) ).
fof(f167,plain,
! [X2,X0,X1] :
( X0 = X1
| ~ incident_o(X1,X2)
| ~ start_point(X0,X2)
| ~ ordered_by(X2,X1,X0) ),
inference(resolution,[],[f79,f148]) ).
fof(f168,plain,
! [X2,X0,X1] :
( ~ ordered_by(X2,X1,X0)
| ~ start_point(X0,X2)
| X0 = X1 ),
inference(forward_subsumption_resolution,[],[f167,f90]) ).
fof(f169,plain,
! [X0,X1] :
( ~ start_point(ax2_sk2(X0,X1),X0)
| ~ incident_o(X1,X0)
| finish_point(X1,X0) ),
inference(forward_subsumption_resolution,[],[f163,f87]) ).
fof(f195,plain,
! [X0] : incident_o(ax2_sk6(X0),X0),
inference(resolution,[],[f102,f78]) ).
fof(f196,plain,
incident_c(ax2_sk6(sk25),sF0),
inference(resolution,[],[f195,f142]) ).
fof(f204,plain,
! [X0] :
( part_of(X0,X0)
| part_of(X0,X0) ),
inference(resolution,[],[f2,f3]) ).
fof(f208,plain,
! [X0] : part_of(X0,X0),
inference(duplicate_literal_removal,[],[f204]) ).
fof(f227,plain,
! [X0,X1] :
( ~ end_point(X1,sF0)
| ~ end_point(X0,sF0)
| X0 = X1
| sk26 = X1
| sk26 = X0 ),
inference(resolution,[],[f50,f136]) ).
fof(f228,plain,
! [X2,X3,X0,X1] :
( ~ end_point(X3,X1)
| ~ end_point(X2,X1)
| X0 = X2
| ax0_sk11(X3,X1) = X2
| ax0_sk11(X3,X1) = X0
| ~ end_point(X0,X1) ),
inference(resolution,[],[f50,f51]) ).
fof(f232,plain,
! [X0,X1] :
( ~ end_point(X1,sF0)
| ax0_sk11(X1,sF0) = X0
| sk26 = ax0_sk11(X1,sF0)
| sk26 = X0
| ~ end_point(X0,sF0) ),
inference(resolution,[],[f227,f51]) ).
fof(f251,plain,
! [X0] :
( ax0_sk11(sk26,sF0) = X0
| sk26 = ax0_sk11(sk26,sF0)
| sk26 = X0
| ~ end_point(X0,sF0) ),
inference(resolution,[],[f232,f136]) ).
fof(f256,definition,
( spl1_3
<=> sk26 = ax0_sk11(sk26,sF0) ),
introduced(definition,[new_symbols(definition,[spl1_3])],[avatar_definition]) ).
fof(f257,plain,
( sk26 != ax0_sk11(sk26,sF0)
| spl1_3 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f258,plain,
( sk26 = ax0_sk11(sk26,sF0)
| ~ spl1_3 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f260,definition,
( spl1_4
<=> ! [X0] :
( ax0_sk11(sk26,sF0) = X0
| ~ end_point(X0,sF0)
| sk26 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl1_4])],[avatar_definition]) ).
fof(f261,plain,
( ! [X0] :
( ~ end_point(X0,sF0)
| ax0_sk11(sk26,sF0) = X0
| sk26 = X0 )
| ~ spl1_4 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f262,plain,
( spl1_3
| spl1_4 ),
inference(avatar_split_clause,[],[f251,f260,f256]) ).
fof(f273,plain,
( sk26 != sk26
| ~ end_point(sk26,sF0)
| ~ spl1_3 ),
inference(superposition,[],[f53,f258]) ).
fof(f274,plain,
( ~ end_point(sk26,sF0)
| ~ spl1_3 ),
inference(trivial_inequality_removal,[],[f273]) ).
fof(f275,plain,
( $false
| ~ spl1_3 ),
inference(forward_subsumption_resolution,[],[f274,f136]) ).
fof(f276,plain,
~ spl1_3,
inference(avatar_contradiction_clause,[],[f275]) ).
fof(f356,plain,
! [X0,X1] :
( ~ end_point(X1,sF0)
| X0 = X1
| ax0_sk11(sk26,sF0) = X0
| ax0_sk11(sk26,sF0) = X1
| ~ end_point(X0,sF0) ),
inference(resolution,[],[f228,f136]) ).
fof(f416,plain,
! [X0] :
( end_point(ax2_sk2(sk25,X0),sF0)
| inner_point(ax2_sk2(sk25,X0),sF0)
| finish_point(X0,sk25)
| ~ incident_o(X0,sk25) ),
inference(resolution,[],[f32,f150]) ).
fof(f418,plain,
( end_point(ax2_sk6(sk25),sF0)
| inner_point(ax2_sk6(sk25),sF0) ),
inference(resolution,[],[f32,f196]) ).
fof(f421,definition,
( spl1_8
<=> inner_point(ax2_sk6(sk25),sF0) ),
introduced(definition,[new_symbols(definition,[spl1_8])],[avatar_definition]) ).
fof(f423,plain,
( inner_point(ax2_sk6(sk25),sF0)
| ~ spl1_8 ),
inference(avatar_component_clause,[],[f421]) ).
fof(f425,definition,
( spl1_9
<=> end_point(ax2_sk6(sk25),sF0) ),
introduced(definition,[new_symbols(definition,[spl1_9])],[avatar_definition]) ).
fof(f426,plain,
( ~ end_point(ax2_sk6(sk25),sF0)
| spl1_9 ),
inference(avatar_component_clause,[],[f425]) ).
fof(f427,plain,
( end_point(ax2_sk6(sk25),sF0)
| ~ spl1_9 ),
inference(avatar_component_clause,[],[f425]) ).
fof(f428,plain,
( spl1_8
| spl1_9 ),
inference(avatar_split_clause,[],[f418,f425,f421]) ).
fof(f439,plain,
( ! [X2,X0,X1] :
( between_c(X0,X1,ax2_sk6(sk25),X2)
| ~ end_point(X1,sF0)
| ~ end_point(X2,sF0)
| X1 = X2
| ~ part_of(sF0,X0) )
| ~ spl1_8 ),
inference(resolution,[],[f423,f71]) ).
fof(f511,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,f142]) ).
fof(f527,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,[],[f511]) ).
fof(f540,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,[],[f527,f139]) ).
fof(f543,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,[],[f540,f101]) ).
fof(f545,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,[],[f543]) ).
fof(f546,plain,
! [X2,X0,X1] :
( ~ between_c(sF0,X0,X1,X2)
| between_o(sk25,X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f545,f527]) ).
fof(f548,plain,
( ! [X0,X1] :
( between_o(sk25,X0,ax2_sk6(sk25),X1)
| ~ end_point(X0,sF0)
| ~ end_point(X1,sF0)
| X0 = X1
| ~ part_of(sF0,sF0) )
| ~ spl1_8 ),
inference(resolution,[],[f546,f439]) ).
fof(f549,plain,
( ! [X0,X1] :
( between_o(sk25,X0,ax2_sk6(sk25),X1)
| ~ end_point(X0,sF0)
| ~ end_point(X1,sF0)
| X0 = X1 )
| ~ spl1_8 ),
inference(forward_subsumption_resolution,[],[f548,f208]) ).
fof(f553,plain,
( ! [X0,X1] :
( ordered_by(sk25,X1,ax2_sk6(sk25))
| ordered_by(sk25,X0,ax2_sk6(sk25))
| X0 = X1
| ~ end_point(X1,sF0)
| ~ end_point(X0,sF0) )
| ~ spl1_8 ),
inference(resolution,[],[f549,f72]) ).
fof(f564,plain,
( ! [X0,X1] :
( ordered_by(sk25,X1,ax2_sk6(sk25))
| X0 = X1
| ~ end_point(X1,sF0)
| ~ end_point(X0,sF0)
| ~ start_point(ax2_sk6(sk25),sk25)
| ax2_sk6(sk25) = X0 )
| ~ spl1_8 ),
inference(resolution,[],[f553,f168]) ).
fof(f570,plain,
( ! [X0,X1] :
( ~ end_point(X1,sF0)
| X0 = X1
| ordered_by(sk25,X1,ax2_sk6(sk25))
| ~ end_point(X0,sF0)
| ax2_sk6(sk25) = X0 )
| ~ spl1_8 ),
inference(forward_subsumption_resolution,[],[f564,f102]) ).
fof(f609,definition,
( spl1_18
<=> ordered_by(sk25,ax2_sk6(sk25),sk26) ),
introduced(definition,[new_symbols(definition,[spl1_18])],[avatar_definition]) ).
fof(f610,plain,
( ~ ordered_by(sk25,ax2_sk6(sk25),sk26)
| spl1_18 ),
inference(avatar_component_clause,[],[f609]) ).
fof(f611,plain,
( ordered_by(sk25,ax2_sk6(sk25),sk26)
| ~ spl1_18 ),
inference(avatar_component_clause,[],[f609]) ).
fof(f630,plain,
( ~ ordered_by(sk25,sk26,ax2_sk6(sk25))
| ~ spl1_18 ),
inference(resolution,[],[f611,f148]) ).
fof(f651,plain,
( ! [X0] :
( sk26 = X0
| ordered_by(sk25,sk26,ax2_sk6(sk25))
| ~ end_point(X0,sF0)
| ax2_sk6(sk25) = X0 )
| ~ spl1_8 ),
inference(resolution,[],[f570,f136]) ).
fof(f652,plain,
( ! [X0] :
( ~ end_point(X0,sF0)
| sk26 = X0
| ax2_sk6(sk25) = X0 )
| ~ spl1_8
| ~ spl1_18 ),
inference(forward_subsumption_resolution,[],[f651,f630]) ).
fof(f661,plain,
( ! [X0] :
( ~ end_point(X0,sF0)
| ax0_sk11(X0,sF0) = ax2_sk6(sk25)
| sk26 = ax0_sk11(X0,sF0) )
| ~ spl1_8
| ~ spl1_18 ),
inference(resolution,[],[f652,f51]) ).
fof(f736,plain,
( ax2_sk6(sk25) = ax0_sk11(sk26,sF0)
| sk26 = ax0_sk11(sk26,sF0)
| ~ spl1_8
| ~ spl1_18 ),
inference(resolution,[],[f661,f136]) ).
fof(f737,plain,
( ax2_sk6(sk25) = ax0_sk11(sk26,sF0)
| spl1_3
| ~ spl1_8
| ~ spl1_18 ),
inference(forward_subsumption_resolution,[],[f736,f257]) ).
fof(f941,plain,
( end_point(ax2_sk6(sk25),sF0)
| ~ end_point(sk26,sF0)
| spl1_3
| ~ spl1_8
| ~ spl1_18 ),
inference(superposition,[],[f51,f737]) ).
fof(f944,plain,
( ~ end_point(sk26,sF0)
| spl1_3
| ~ spl1_8
| spl1_9
| ~ spl1_18 ),
inference(forward_subsumption_resolution,[],[f941,f426]) ).
fof(f945,plain,
( $false
| spl1_3
| ~ spl1_8
| spl1_9
| ~ spl1_18 ),
inference(forward_subsumption_resolution,[],[f944,f136]) ).
fof(f946,plain,
( spl1_3
| ~ spl1_8
| spl1_9
| ~ spl1_18 ),
inference(avatar_contradiction_clause,[],[f945]) ).
fof(f969,plain,
( ax2_sk6(sk25) = ax0_sk11(sk26,sF0)
| sk26 = ax2_sk6(sk25)
| ~ spl1_4
| ~ spl1_9 ),
inference(resolution,[],[f427,f261]) ).
fof(f985,definition,
( spl1_27
<=> ax2_sk6(sk25) = ax0_sk11(sk26,sF0) ),
introduced(definition,[new_symbols(definition,[spl1_27])],[avatar_definition]) ).
fof(f987,plain,
( ax2_sk6(sk25) = ax0_sk11(sk26,sF0)
| ~ spl1_27 ),
inference(avatar_component_clause,[],[f985]) ).
fof(f1002,definition,
( spl1_31
<=> sk26 = ax2_sk6(sk25) ),
introduced(definition,[new_symbols(definition,[spl1_31])],[avatar_definition]) ).
fof(f1003,plain,
( sk26 != ax2_sk6(sk25)
| spl1_31 ),
inference(avatar_component_clause,[],[f1002]) ).
fof(f1004,plain,
( sk26 = ax2_sk6(sk25)
| ~ spl1_31 ),
inference(avatar_component_clause,[],[f1002]) ).
fof(f1005,plain,
( spl1_31
| spl1_27
| ~ spl1_4
| ~ spl1_9 ),
inference(avatar_split_clause,[],[f969,f425,f260,f985,f1002]) ).
fof(f3398,definition,
( spl1_111
<=> end_point(ax2_sk2(sk25,sk26),sF0) ),
introduced(definition,[new_symbols(definition,[spl1_111])],[avatar_definition]) ).
fof(f3399,plain,
( end_point(ax2_sk2(sk25,sk26),sF0)
| ~ spl1_111 ),
inference(avatar_component_clause,[],[f3398]) ).
fof(f3400,plain,
( ~ end_point(ax2_sk2(sk25,sk26),sF0)
| spl1_111 ),
inference(avatar_component_clause,[],[f3398]) ).
fof(f3911,plain,
( inner_point(ax2_sk2(sk25,sk26),sF0)
| finish_point(sk26,sk25)
| ~ incident_o(sk26,sk25)
| spl1_111 ),
inference(resolution,[],[f416,f3400]) ).
fof(f3960,plain,
( inner_point(ax2_sk2(sk25,sk26),sF0)
| ~ incident_o(sk26,sk25)
| spl1_111 ),
inference(forward_subsumption_resolution,[],[f3911,f126]) ).
fof(f3971,plain,
( inner_point(ax2_sk2(sk25,sk26),sF0)
| spl1_111 ),
inference(forward_subsumption_resolution,[],[f3960,f144]) ).
fof(f4455,plain,
( start_point(sk26,sk25)
| ~ spl1_31 ),
inference(superposition,[],[f102,f1004]) ).
fof(f4456,plain,
( $false
| ~ spl1_31 ),
inference(forward_subsumption_resolution,[],[f4455,f125]) ).
fof(f4457,plain,
~ spl1_31,
inference(avatar_contradiction_clause,[],[f4456]) ).
fof(f4518,plain,
( ! [X2,X0,X1] :
( between_c(X0,X1,ax2_sk2(sk25,sk26),X2)
| ~ end_point(X1,sF0)
| ~ end_point(X2,sF0)
| X1 = X2
| ~ part_of(sF0,X0) )
| spl1_111 ),
inference(resolution,[],[f3971,f71]) ).
fof(f4716,definition,
( spl1_155
<=> ! [X0] :
( ax2_sk2(sk25,sk26) = X0
| ax2_sk6(sk25) = X0
| ~ end_point(X0,sF0) ) ),
introduced(definition,[new_symbols(definition,[spl1_155])],[avatar_definition]) ).
fof(f4717,plain,
( ! [X0] :
( ~ end_point(X0,sF0)
| ax2_sk6(sk25) = X0
| ax2_sk2(sk25,sk26) = X0 )
| ~ spl1_155 ),
inference(avatar_component_clause,[],[f4716]) ).
fof(f4771,plain,
( ! [X0,X1] :
( ~ end_point(X0,sF0)
| ~ end_point(X1,sF0)
| X0 = X1
| ~ part_of(sF0,sF0)
| between_o(sk25,X0,ax2_sk2(sk25,sk26),X1) )
| spl1_111 ),
inference(resolution,[],[f4518,f546]) ).
fof(f4774,plain,
( ! [X0,X1] :
( between_o(sk25,X0,ax2_sk2(sk25,sk26),X1)
| ~ end_point(X1,sF0)
| X0 = X1
| ~ end_point(X0,sF0) )
| spl1_111 ),
inference(forward_subsumption_resolution,[],[f4771,f208]) ).
fof(f4781,plain,
( ! [X0,X1] :
( ordered_by(sk25,ax2_sk2(sk25,sk26),X1)
| ordered_by(sk25,ax2_sk2(sk25,sk26),X0)
| ~ end_point(X1,sF0)
| X0 = X1
| ~ end_point(X0,sF0) )
| spl1_111 ),
inference(resolution,[],[f4774,f75]) ).
fof(f4843,plain,
( ! [X0] :
( ordered_by(sk25,ax2_sk2(sk25,sk26),X0)
| ~ end_point(X0,sF0)
| sk26 = X0
| ~ end_point(sk26,sF0)
| finish_point(sk26,sk25) )
| spl1_111 ),
inference(resolution,[],[f4781,f137]) ).
fof(f4861,plain,
( ! [X0] :
( ordered_by(sk25,ax2_sk2(sk25,sk26),X0)
| ~ end_point(X0,sF0)
| sk26 = X0
| finish_point(sk26,sk25) )
| spl1_111 ),
inference(forward_subsumption_resolution,[],[f4843,f136]) ).
fof(f4864,plain,
( ! [X0] :
( ordered_by(sk25,ax2_sk2(sk25,sk26),X0)
| ~ end_point(X0,sF0)
| sk26 = X0 )
| spl1_111 ),
inference(forward_subsumption_resolution,[],[f4861,f126]) ).
fof(f4873,plain,
( ! [X0] :
( ~ start_point(X0,sk25)
| sk26 = X0
| ~ end_point(X0,sF0)
| ax2_sk2(sk25,sk26) = X0 )
| spl1_111 ),
inference(resolution,[],[f4864,f168]) ).
fof(f4881,plain,
( sk26 = ax2_sk6(sk25)
| ~ end_point(ax2_sk6(sk25),sF0)
| ax2_sk6(sk25) = ax2_sk2(sk25,sk26)
| spl1_111 ),
inference(resolution,[],[f4873,f102]) ).
fof(f4882,plain,
( ~ end_point(ax2_sk6(sk25),sF0)
| ax2_sk6(sk25) = ax2_sk2(sk25,sk26)
| spl1_31
| spl1_111 ),
inference(forward_subsumption_resolution,[],[f4881,f1003]) ).
fof(f4883,plain,
( ax2_sk6(sk25) = ax2_sk2(sk25,sk26)
| ~ spl1_9
| spl1_31
| spl1_111 ),
inference(forward_subsumption_resolution,[],[f4882,f427]) ).
fof(f4903,plain,
( ~ start_point(ax2_sk6(sk25),sk25)
| ~ incident_o(sk26,sk25)
| finish_point(sk26,sk25)
| ~ spl1_9
| spl1_31
| spl1_111 ),
inference(superposition,[],[f169,f4883]) ).
fof(f4908,plain,
( ~ incident_o(sk26,sk25)
| finish_point(sk26,sk25)
| ~ spl1_9
| spl1_31
| spl1_111 ),
inference(forward_subsumption_resolution,[],[f4903,f102]) ).
fof(f4917,plain,
( finish_point(sk26,sk25)
| ~ spl1_9
| spl1_31
| spl1_111 ),
inference(forward_subsumption_resolution,[],[f4908,f144]) ).
fof(f4918,plain,
( $false
| ~ spl1_9
| spl1_31
| spl1_111 ),
inference(forward_subsumption_resolution,[],[f4917,f126]) ).
fof(f4919,plain,
( ~ spl1_9
| spl1_31
| spl1_111 ),
inference(avatar_contradiction_clause,[],[f4918]) ).
fof(f4937,definition,
( spl1_157
<=> sk26 = ax2_sk2(sk25,sk26) ),
introduced(definition,[new_symbols(definition,[spl1_157])],[avatar_definition]) ).
fof(f4938,plain,
( sk26 != ax2_sk2(sk25,sk26)
| spl1_157 ),
inference(avatar_component_clause,[],[f4937]) ).
fof(f4939,plain,
( sk26 = ax2_sk2(sk25,sk26)
| ~ spl1_157 ),
inference(avatar_component_clause,[],[f4937]) ).
fof(f4950,plain,
( ! [X0] :
( ax2_sk2(sk25,sk26) = X0
| ax0_sk11(sk26,sF0) = X0
| ax0_sk11(sk26,sF0) = ax2_sk2(sk25,sk26)
| ~ end_point(X0,sF0) )
| ~ spl1_111 ),
inference(resolution,[],[f3399,f356]) ).
fof(f5007,plain,
( ! [X0] :
( ax2_sk6(sk25) = X0
| ax2_sk2(sk25,sk26) = X0
| ax0_sk11(sk26,sF0) = ax2_sk2(sk25,sk26)
| ~ end_point(X0,sF0) )
| ~ spl1_27
| ~ spl1_111 ),
inference(forward_demodulation,[],[f4950,f987]) ).
fof(f5034,definition,
( spl1_167
<=> ax2_sk6(sk25) = ax2_sk2(sk25,sk26) ),
introduced(definition,[new_symbols(definition,[spl1_167])],[avatar_definition]) ).
fof(f5036,plain,
( ax2_sk6(sk25) = ax2_sk2(sk25,sk26)
| ~ spl1_167 ),
inference(avatar_component_clause,[],[f5034]) ).
fof(f5039,plain,
( ! [X0] :
( ax2_sk6(sk25) = ax2_sk2(sk25,sk26)
| ax2_sk6(sk25) = X0
| ax2_sk2(sk25,sk26) = X0
| ~ end_point(X0,sF0) )
| ~ spl1_27
| ~ spl1_111 ),
inference(forward_demodulation,[],[f5007,f987]) ).
fof(f5053,plain,
( spl1_155
| spl1_167
| ~ spl1_27
| ~ spl1_111 ),
inference(avatar_split_clause,[],[f5039,f3398,f985,f5034,f4716]) ).
fof(f5101,plain,
( ~ start_point(ax2_sk6(sk25),sk25)
| ~ incident_o(sk26,sk25)
| finish_point(sk26,sk25)
| ~ spl1_167 ),
inference(superposition,[],[f169,f5036]) ).
fof(f5106,plain,
( ~ incident_o(sk26,sk25)
| finish_point(sk26,sk25)
| ~ spl1_167 ),
inference(forward_subsumption_resolution,[],[f5101,f102]) ).
fof(f5115,plain,
( finish_point(sk26,sk25)
| ~ spl1_167 ),
inference(forward_subsumption_resolution,[],[f5106,f144]) ).
fof(f5118,plain,
( $false
| ~ spl1_167 ),
inference(forward_subsumption_resolution,[],[f5115,f126]) ).
fof(f5119,plain,
~ spl1_167,
inference(avatar_contradiction_clause,[],[f5118]) ).
fof(f5155,plain,
( sk26 != sk26
| ~ incident_o(sk26,sk25)
| finish_point(sk26,sk25)
| ~ spl1_157 ),
inference(superposition,[],[f87,f4939]) ).
fof(f5157,plain,
( ~ incident_o(sk26,sk25)
| finish_point(sk26,sk25)
| ~ spl1_157 ),
inference(trivial_inequality_removal,[],[f5155]) ).
fof(f5158,plain,
( finish_point(sk26,sk25)
| ~ spl1_157 ),
inference(forward_subsumption_resolution,[],[f5157,f144]) ).
fof(f5162,plain,
( $false
| ~ spl1_157 ),
inference(forward_subsumption_resolution,[],[f5158,f126]) ).
fof(f5163,plain,
~ spl1_157,
inference(avatar_contradiction_clause,[],[f5162]) ).
fof(f5293,plain,
( sk26 = ax2_sk6(sk25)
| sk26 = ax2_sk2(sk25,sk26)
| ~ spl1_155 ),
inference(resolution,[],[f4717,f136]) ).
fof(f5294,plain,
( sk26 = ax2_sk2(sk25,sk26)
| spl1_31
| ~ spl1_155 ),
inference(forward_subsumption_resolution,[],[f5293,f1003]) ).
fof(f5297,plain,
( $false
| spl1_31
| ~ spl1_155
| spl1_157 ),
inference(forward_subsumption_resolution,[],[f5294,f4938]) ).
fof(f5298,plain,
( spl1_31
| ~ spl1_155
| spl1_157 ),
inference(avatar_contradiction_clause,[],[f5297]) ).
fof(f5319,plain,
( sk26 = ax2_sk6(sk25)
| ~ incident_o(sk26,sk25)
| ~ start_point(ax2_sk6(sk25),sk25)
| spl1_18 ),
inference(resolution,[],[f610,f79]) ).
fof(f5320,plain,
( ~ incident_o(sk26,sk25)
| ~ start_point(ax2_sk6(sk25),sk25)
| spl1_18
| spl1_31 ),
inference(forward_subsumption_resolution,[],[f5319,f1003]) ).
fof(f5321,plain,
( ~ start_point(ax2_sk6(sk25),sk25)
| spl1_18
| spl1_31 ),
inference(forward_subsumption_resolution,[],[f5320,f144]) ).
fof(f5322,plain,
( $false
| spl1_18
| spl1_31 ),
inference(forward_subsumption_resolution,[],[f5321,f102]) ).
fof(f5323,plain,
( spl1_18
| spl1_31 ),
inference(avatar_contradiction_clause,[],[f5322]) ).
cnf(s2,plain,
( spl1_3
| spl1_4 ),
inference(sat_conversion,[],[f262]) ).
cnf(s4,plain,
~ spl1_3,
inference(sat_conversion,[],[f276]) ).
cnf(s8,plain,
( spl1_8
| spl1_9 ),
inference(sat_conversion,[],[f428]) ).
cnf(s39,plain,
( spl1_3
| ~ spl1_8
| spl1_9
| ~ spl1_18 ),
inference(sat_conversion,[],[f946]) ).
cnf(s43,plain,
( ~ spl1_4
| ~ spl1_9
| spl1_27
| spl1_31 ),
inference(sat_conversion,[],[f1005]) ).
cnf(s200,plain,
~ spl1_31,
inference(sat_conversion,[],[f4457]) ).
cnf(s244,plain,
( ~ spl1_9
| spl1_31
| spl1_111 ),
inference(sat_conversion,[],[f4919]) ).
cnf(s263,plain,
( ~ spl1_27
| ~ spl1_111
| spl1_155
| spl1_167 ),
inference(sat_conversion,[],[f5053]) ).
cnf(s268,plain,
~ spl1_167,
inference(sat_conversion,[],[f5119]) ).
cnf(s273,plain,
~ spl1_157,
inference(sat_conversion,[],[f5163]) ).
cnf(s294,plain,
( spl1_31
| ~ spl1_155
| spl1_157 ),
inference(sat_conversion,[],[f5298]) ).
cnf(s297,plain,
( spl1_18
| spl1_31 ),
inference(sat_conversion,[],[f5323]) ).
cnf(s298,plain,
( ~ spl1_27
| ~ spl1_111
| spl1_155 ),
inference(rat,[],[s263,s268]) ).
cnf(s307,plain,
spl1_18,
inference(rat,[],[s297,s200]) ).
cnf(s308,plain,
~ spl1_155,
inference(rat,[],[s294,s273,s200]) ).
cnf(s322,plain,
( ~ spl1_4
| ~ spl1_9
| spl1_27 ),
inference(rat,[],[s43,s200]) ).
cnf(s323,plain,
( spl1_3
| ~ spl1_8
| spl1_9 ),
inference(rat,[],[s39,s307]) ).
cnf(s337,plain,
spl1_4,
inference(rat,[],[s2,s4]) ).
cnf(s338,plain,
~ spl1_9,
inference(rat,[],[s298,s322,s244,s308,s337,s200]) ).
cnf(s339,plain,
spl1_8,
inference(rat,[],[s8,s338]) ).
cnf(s340,plain,
$false,
inference(rat,[],[s323,s4,s338,s339]) ).
fof(f5324,plain,
$false,
inference(avatar_sat_refutation,[],[s340]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO121-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n018.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 27 07:08:38 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 Running first-order theorem proving
% 0.12/0.40 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
% 11.18/2.43 % (1980386)Input is clausal, will run a generic CNF schedule.
% 11.18/2.43 % (1980397)dis-21_1_sil=8000:lcm=predicate:random_seed=2625932033: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)
% 11.18/2.43 % (1980393)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1411882647:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.18/2.43 % (1980391)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=3596773561:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.18/2.43 % (1980392)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1118835409:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.18/2.43 % (1980397)Instruction limit reached!
% 11.18/2.43 % (1980397)------------------------------
% 11.18/2.43 % (1980397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.43 % (1980397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.43 % (1980397)CaDiCaL version: 2.1.3
% 11.18/2.43 % (1980397)Termination reason: Instruction limit
% 11.18/2.43 % (1980397)Termination phase: Saturation
% 11.18/2.43 % (1980397)Time elapsed: 0.040 s
% 11.18/2.43 % (1980397)Peak memory usage: 89 MB
% 11.18/2.43 % (1980397)Instructions burned: 119 (million)
% 11.18/2.43 % (1980395)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1667949472:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.18/2.43 % (1980394)lrs+10_1_sil=8000:sp=occurrence:random_seed=972573625:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.18/2.43 % (1980396)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4007163449:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.18/2.43 % (1980395)Refutation not found, incomplete strategy
% 11.18/2.43 % (1980395)------------------------------
% 11.18/2.43 % (1980395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.43 % (1980395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.43 % (1980395)CaDiCaL version: 2.1.3
% 11.18/2.43 % (1980395)Termination reason: Refutation not found, incomplete strategy
% 11.18/2.43 % (1980395)Time elapsed: 0.002 s
% 11.18/2.43 % (1980395)Peak memory usage: 88 MB
% 11.18/2.43 % (1980395)Instructions burned: 1 (million)
% 11.18/2.43 % (1980394)Refutation not found, incomplete strategy
% 11.18/2.43 % (1980394)------------------------------
% 11.18/2.43 % (1980394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.43 % (1980394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.43 % (1980394)CaDiCaL version: 2.1.3
% 11.18/2.43 % (1980394)Termination reason: Refutation not found, incomplete strategy
% 11.18/2.43 % (1980394)Time elapsed: 0.002 s
% 11.18/2.43 % (1980394)Peak memory usage: 88 MB
% 11.18/2.43 % (1980394)Instructions burned: 2 (million)
% 11.18/2.43 % (1980396)Instruction limit reached!
% 11.18/2.43 % (1980396)------------------------------
% 11.18/2.43 % (1980396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.43 % (1980396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.43 % (1980396)CaDiCaL version: 2.1.3
% 11.18/2.43 % (1980396)Termination reason: Instruction limit
% 11.18/2.43 % (1980396)Termination phase: Saturation
% 11.18/2.43 % (1980396)Time elapsed: 0.122 s
% 11.18/2.43 % (1980396)Peak memory usage: 89 MB
% 11.18/2.43 % (1980396)Instructions burned: 181 (million)
% 11.18/2.43 % (1980405)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=2885040435:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 11.18/2.43 % (1980405)Refutation not found, incomplete strategy
% 11.18/2.43 % (1980405)------------------------------
% 11.18/2.43 % (1980405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.43 % (1980405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.43 % (1980405)CaDiCaL version: 2.1.3
% 11.18/2.43 % (1980405)Termination reason: Refutation not found, incomplete strategy
% 11.18/2.43 % (1980405)Time elapsed: 0.001 s
% 11.18/2.43 % (1980405)Peak memory usage: 88 MB
% 11.18/2.43 % (1980405)Instructions burned: 1 (million)
% 11.18/2.43 % (1980394)------------------------------
% 11.18/2.43 % (1980394)------------------------------
% 11.18/2.43 % (1980395)------------------------------
% 11.18/2.43 % (1980395)------------------------------
% 11.18/2.43 % (1980405)------------------------------
% 11.18/2.43 % (1980405)------------------------------
% 11.18/2.43 % (1980407)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3629629136: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)
% 11.18/2.43 % (1980410)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1381978928:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 11.18/2.43 % (1980409)lrs+10_64_to=lpo:sil=8000:random_seed=2893296932:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 11.18/2.43 % (1980408)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2343217680:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 11.18/2.43 % (1980407)Instruction limit reached!
% 11.18/2.43 % (1980407)------------------------------
% 11.18/2.43 % (1980407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.43 % (1980407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.43 % (1980407)CaDiCaL version: 2.1.3
% 11.18/2.43 % (1980407)Termination reason: Instruction limit
% 11.18/2.43 % (1980407)Termination phase: Saturation
% 11.18/2.43 % (1980407)Time elapsed: 0.101 s
% 11.18/2.43 % (1980407)Peak memory usage: 89 MB
% 11.18/2.43 % (1980407)Instructions burned: 190 (million)
% 11.18/2.43 % (1980410)Instruction limit reached!
% 11.18/2.43 % (1980410)------------------------------
% 11.18/2.43 % (1980410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.43 % (1980410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.43 % (1980410)CaDiCaL version: 2.1.3
% 11.18/2.43 % (1980410)Termination reason: Instruction limit
% 11.18/2.43 % (1980410)Termination phase: Saturation
% 11.18/2.43 % (1980410)Time elapsed: 0.062 s
% 11.18/2.43 % (1980410)Peak memory usage: 89 MB
% 11.18/2.43 % (1980410)Instructions burned: 197 (million)
% 11.18/2.43 % (1980409)Instruction limit reached!
% 11.18/2.43 % (1980409)------------------------------
% 11.18/2.43 % (1980409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.43 % (1980409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.43 % (1980409)CaDiCaL version: 2.1.3
% 11.18/2.43 % (1980409)Termination reason: Instruction limit
% 11.18/2.43 % (1980409)Termination phase: Saturation
% 11.18/2.43 % (1980409)Time elapsed: 0.074 s
% 11.18/2.43 % (1980409)Peak memory usage: 89 MB
% 11.18/2.43 % (1980409)Instructions burned: 126 (million)
% 11.18/2.43 % (1980408)Instruction limit reached!
% 11.18/2.43 % (1980408)------------------------------
% 11.18/2.43 % (1980408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.43 % (1980408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.43 % (1980408)CaDiCaL version: 2.1.3
% 11.18/2.43 % (1980408)Termination reason: Instruction limit
% 11.18/2.43 % (1980408)Termination phase: Saturation
% 11.18/2.43 % (1980408)Time elapsed: 0.130 s
% 11.18/2.43 % (1980408)Peak memory usage: 89 MB
% 11.18/2.43 % (1980408)Instructions burned: 219 (million)
% 11.18/2.43 % (1980415)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4075213627:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 11.18/2.44 % (1980416)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4245289195:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 11.18/2.44 % (1980417)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=3923723427:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 11.18/2.44 % (1980415)Instruction limit reached!
% 11.18/2.44 % (1980415)------------------------------
% 11.18/2.44 % (1980415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.44 % (1980415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.44 % (1980415)CaDiCaL version: 2.1.3
% 11.18/2.44 % (1980415)Termination reason: Instruction limit
% 11.18/2.44 % (1980415)Termination phase: Saturation
% 11.18/2.44 % (1980415)Time elapsed: 0.107 s
% 11.18/2.44 % (1980415)Peak memory usage: 90 MB
% 11.18/2.44 % (1980415)Instructions burned: 158 (million)
% 11.18/2.44 % (1980417)Instruction limit reached!
% 11.18/2.44 % (1980417)------------------------------
% 11.18/2.44 % (1980417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.44 % (1980417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.44 % (1980417)CaDiCaL version: 2.1.3
% 11.18/2.44 % (1980417)Termination reason: Instruction limit
% 11.18/2.44 % (1980417)Termination phase: Saturation
% 11.18/2.44 % (1980417)Time elapsed: 0.056 s
% 11.18/2.44 % (1980417)Peak memory usage: 88 MB
% 11.18/2.44 % (1980417)Instructions burned: 106 (million)
% 11.18/2.44 % (1980418)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2987943989:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 11.18/2.44 % (1980418)Instruction limit reached!
% 11.18/2.44 % (1980418)------------------------------
% 11.18/2.44 % (1980418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.44 % (1980418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.44 % (1980418)CaDiCaL version: 2.1.3
% 11.18/2.44 % (1980418)Termination reason: Instruction limit
% 11.18/2.44 % (1980418)Termination phase: Saturation
% 11.18/2.44 % (1980418)Time elapsed: 0.071 s
% 11.18/2.44 % (1980418)Peak memory usage: 89 MB
% 11.18/2.44 % (1980418)Instructions burned: 108 (million)
% 11.18/2.44 % (1980422)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1286086495:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 11.18/2.44 % (1980423)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3319966151:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 11.18/2.44 % (1980425)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1212217458:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 11.18/2.44 % (1980425)Refutation not found, incomplete strategy
% 11.18/2.44 % (1980425)------------------------------
% 11.18/2.44 % (1980425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.44 % (1980425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.44 % (1980425)CaDiCaL version: 2.1.3
% 11.18/2.44 % (1980425)Termination reason: Refutation not found, incomplete strategy
% 11.18/2.44 % (1980425)Time elapsed: 0.003 s
% 11.18/2.44 % (1980425)Peak memory usage: 88 MB
% 11.18/2.44 % (1980425)Instructions burned: 2 (million)
% 11.18/2.44 % (1980422)Instruction limit reached!
% 11.18/2.44 % (1980422)------------------------------
% 11.18/2.44 % (1980422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.44 % (1980422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.44 % (1980422)CaDiCaL version: 2.1.3
% 11.18/2.44 % (1980422)Termination reason: Instruction limit
% 11.18/2.44 % (1980422)Termination phase: Saturation
% 11.18/2.44 % (1980422)Time elapsed: 0.144 s
% 11.18/2.44 % (1980422)Peak memory usage: 89 MB
% 11.18/2.44 % (1980422)Instructions burned: 242 (million)
% 11.18/2.44 % (1980429)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2175676205:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 11.18/2.44 % (1980391)First to succeed.
% 11.18/2.44 % (1980391)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1980386"
% 11.18/2.44 % (1980425)------------------------------
% 11.18/2.44 % (1980425)------------------------------
% 11.18/2.44 % (1980416)Also succeeded, but the first one will report.
% 11.18/2.44 % (1980431)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=4246443642:i=191:fgj=on:bd=all_2986 on theBenchmark for (2986ds/191Mi)
% 11.18/2.44 % (1980429)Instruction limit reached!
% 11.18/2.44 % (1980429)------------------------------
% 11.18/2.44 % (1980429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.44 % (1980429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.44 % (1980429)CaDiCaL version: 2.1.3
% 11.18/2.44 % (1980429)Termination reason: Instruction limit
% 11.18/2.44 % (1980429)Termination phase: Saturation
% 11.18/2.44 % (1980429)Time elapsed: 0.300 s
% 11.18/2.44 % (1980429)Peak memory usage: 93 MB
% 11.18/2.44 % (1980429)Instructions burned: 499 (million)
% 11.18/2.44 % (1980391)Refutation found. Thanks to Tanya!
% 11.18/2.44 % SZS status Unsatisfiable for theBenchmark
% 11.18/2.44 % SZS output start Proof for theBenchmark
% See solution above
% 11.72/2.57 % (1980391)------------------------------
% 11.72/2.57 % (1980391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.57 % (1980391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.57 % (1980391)CaDiCaL version: 2.1.3
% 11.72/2.57 % (1980391)Termination reason: Refutation
% 11.72/2.57 % (1980391)Time elapsed: 1.167 s
% 11.72/2.57 % (1980391)Peak memory usage: 134 MB
% 11.72/2.57 % (1980391)Instructions burned: 1699 (million)
% 11.72/2.57 % (1980391)------------------------------
% 11.72/2.57 % (1980391)------------------------------
% 11.72/2.57 % (1980386)Success in time 1.588 s
% 11.72/2.57 % Vampire exiting
%------------------------------------------------------------------------------