%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO137-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 : n011.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:40 AM UTC 2026
% Result : Unsatisfiable 8.83s 2.08s
% Output : Refutation 9.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 43
% Syntax : Number of formulae : 328 ( 26 unt; 19 def)
% Number of atoms : 1168 ( 129 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 1485 ( 645 ~; 821 |; 0 &)
% ( 19 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 29 ( 27 usr; 20 prp; 0-4 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-5 aty)
% Number of variables : 347 ( 0 sgn 347 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f31,axiom,
! [X0,X1] :
( ~ inner_point(X0,X1)
| ~ end_point(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inner_point_defn_22) ).
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(f69,axiom,
! [X2,X3,X0,X1] :
( end_point(X3,ax1_sk1(X3,X2,X1,X0))
| ~ between_c(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',between_c_defn_4) ).
fof(f70,axiom,
! [X2,X3,X0,X1] :
( inner_point(X2,ax1_sk1(X3,X2,X1,X0))
| ~ between_c(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',between_c_defn_5) ).
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(f77,axiom,
! [X2,X3,X0,X1] :
( between_o(X0,X3,X2,X1)
| ~ ordered_by(X0,X2,X3)
| ~ ordered_by(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',between_o_defn_6) ).
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(f91,axiom,
! [X2,X0,X1] :
( ~ ordered_by(X0,X1,X2)
| incident_o(X2,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',o1_18) ).
fof(f95,axiom,
! [X2,X3,X0,X1,X4] :
( incident_c(X4,ax2_sk4(X0,X3,X2,X1))
| ~ incident_o(X4,X0)
| ~ between_o(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',o3_22) ).
fof(f96,axiom,
! [X2,X3,X0,X1,X4] :
( ~ incident_c(X4,ax2_sk4(X0,X3,X2,X1))
| ~ between_o(X0,X1,X2,X3)
| incident_o(X4,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',o3_23) ).
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(f106,axiom,
! [X0,X1] :
( ordered_by(X1,ax2_sk8(X1,X0),ax2_sk9(X1,X0))
| ordered_by(X0,ax2_sk8(X1,X0),ax2_sk9(X1,X0))
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',o6_33) ).
fof(f110,axiom,
! [X0,X1] :
( ~ ordered_by(X0,ax2_sk8(X0,X1),ax2_sk9(X0,X1))
| ~ ordered_by(X1,ax2_sk8(X0,X1),ax2_sk9(X0,X1))
| X1 = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',o6_36) ).
fof(f111,plain,
! [X0,X1] :
( ~ ordered_by(X1,ax2_sk8(X0,X1),ax2_sk9(X0,X1))
| ~ ordered_by(X0,ax2_sk8(X0,X1),ax2_sk9(X0,X1))
| X0 = X1 ),
inference(reorient_equations,[],[f110]) ).
fof(f124,negated_conjecture,
! [X0] :
( ~ incident_o(X0,sk25)
| incident_o(X0,sk26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_4_20_133) ).
fof(f125,negated_conjecture,
! [X0] :
( ~ incident_o(X0,sk26)
| incident_o(X0,sk25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_4_20_134) ).
fof(f126,negated_conjecture,
ordered_by(sk25,sk27,sk28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_4_20_135) ).
fof(f127,negated_conjecture,
ordered_by(sk26,sk27,sk28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_4_20_136) ).
fof(f128,negated_conjecture,
sk25 != sk26,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_4_20_137) ).
fof(f133,plain,
! [X2,X3,X0] : ~ between_c(X0,X3,X2,X3),
inference(equality_resolution,[],[f66]) ).
fof(f138,plain,
! [X2,X0,X1] : ~ between_o(X0,X1,X2,X1),
inference(resolution,[],[f97,f133]) ).
fof(f147,plain,
! [X2,X0,X1] :
( ~ ordered_by(X0,X2,X1)
| ~ ordered_by(X0,X1,X2) ),
inference(resolution,[],[f77,f138]) ).
fof(f148,plain,
~ ordered_by(sk25,sk28,sk27),
inference(resolution,[],[f147,f126]) ).
fof(f149,plain,
~ ordered_by(sk26,sk28,sk27),
inference(resolution,[],[f147,f127]) ).
fof(f151,plain,
! [X2,X0,X1] :
( X0 = X1
| ~ incident_o(X1,X2)
| ~ start_point(X0,X2)
| ~ ordered_by(X2,X1,X0) ),
inference(resolution,[],[f79,f147]) ).
fof(f154,plain,
! [X2,X0,X1] :
( ~ ordered_by(X2,X1,X0)
| ~ start_point(X0,X2)
| X0 = X1 ),
inference(forward_subsumption_resolution,[],[f151,f90]) ).
fof(f211,plain,
! [X0,X1] :
( ~ ordered_by(X0,ax2_sk8(X0,X1),ax2_sk9(X0,X1))
| X0 = X1
| ax2_sk8(X0,X1) = ax2_sk9(X0,X1)
| ~ incident_o(ax2_sk9(X0,X1),X1)
| ~ start_point(ax2_sk8(X0,X1),X1) ),
inference(resolution,[],[f111,f79]) ).
fof(f340,plain,
! [X0,X1] :
( ordered_by(X1,ax2_sk8(X0,X1),ax2_sk9(X0,X1))
| X0 = X1
| incident_o(ax2_sk9(X0,X1),X0) ),
inference(resolution,[],[f106,f91]) ).
fof(f354,plain,
! [X0,X1] :
( incident_o(ax2_sk9(X0,X1),X1)
| incident_o(ax2_sk9(X0,X1),X0)
| X0 = X1 ),
inference(resolution,[],[f340,f91]) ).
fof(f377,plain,
! [X0] :
( incident_o(ax2_sk9(X0,sk25),sk26)
| incident_o(ax2_sk9(X0,sk25),X0)
| sk25 = X0 ),
inference(resolution,[],[f354,f124]) ).
fof(f386,plain,
( incident_o(ax2_sk9(sk26,sk25),sk26)
| sk25 = sk26 ),
inference(factoring,[],[f377]) ).
fof(f387,plain,
incident_o(ax2_sk9(sk26,sk25),sk26),
inference(forward_subsumption_resolution,[],[f386,f128]) ).
fof(f388,plain,
incident_o(ax2_sk9(sk26,sk25),sk25),
inference(resolution,[],[f387,f125]) ).
fof(f455,plain,
! [X2,X3,X0,X1] :
( ~ end_point(X2,ax1_sk1(X3,X2,X1,X0))
| ~ between_c(X0,X1,X2,X3) ),
inference(resolution,[],[f70,f31]) ).
fof(f483,plain,
! [X2,X0,X1] :
( ~ between_c(X0,X1,X2,X2)
| ~ between_c(X0,X1,X2,X2) ),
inference(resolution,[],[f455,f69]) ).
fof(f486,plain,
! [X2,X0,X1] : ~ between_c(X0,X1,X2,X2),
inference(duplicate_literal_removal,[],[f483]) ).
fof(f487,plain,
! [X2,X0,X1] : ~ between_o(X0,X1,X2,X2),
inference(resolution,[],[f486,f97]) ).
fof(f495,plain,
! [X2,X0,X1] :
( ~ ordered_by(X0,X2,X1)
| ~ ordered_by(X0,X1,X1) ),
inference(resolution,[],[f487,f76]) ).
fof(f496,plain,
! [X2,X0,X1] :
( ~ ordered_by(X0,X1,X2)
| ~ ordered_by(X0,X1,X1) ),
inference(resolution,[],[f487,f77]) ).
fof(f497,plain,
~ ordered_by(sk25,sk27,sk27),
inference(resolution,[],[f496,f126]) ).
fof(f498,plain,
~ ordered_by(sk26,sk27,sk27),
inference(resolution,[],[f496,f127]) ).
fof(f614,definition,
( spl0_9
<=> start_point(ax2_sk8(sk26,sk25),sk26) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f615,plain,
( start_point(ax2_sk8(sk26,sk25),sk26)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f614]) ).
fof(f616,plain,
( ~ start_point(ax2_sk8(sk26,sk25),sk26)
| spl0_9 ),
inference(avatar_component_clause,[],[f614]) ).
fof(f622,definition,
( spl0_11
<=> ax2_sk9(sk26,sk25) = ax2_sk8(sk26,sk25) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f623,plain,
( ax2_sk9(sk26,sk25) != ax2_sk8(sk26,sk25)
| spl0_11 ),
inference(avatar_component_clause,[],[f622]) ).
fof(f624,plain,
( ax2_sk9(sk26,sk25) = ax2_sk8(sk26,sk25)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f622]) ).
fof(f778,plain,
! [X2,X3,X0,X1] :
( incident_o(ax2_sk5(X0,sk25,X1,X2,X3),sk26)
| 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,f124]) ).
fof(f779,plain,
! [X2,X3,X0,X1] :
( incident_o(ax2_sk5(X0,sk26,X1,X2,X3),sk25)
| incident_c(ax2_sk5(X0,sk26,X1,X2,X3),X0)
| between_o(sk26,X3,X2,X1)
| ~ between_c(X0,X3,X2,X1) ),
inference(resolution,[],[f98,f125]) ).
fof(f784,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( incident_o(ax2_sk5(ax2_sk4(X0,X1,X2,X3),X4,X5,X6,X7),X4)
| incident_o(ax2_sk5(ax2_sk4(X0,X1,X2,X3),X4,X5,X6,X7),X0)
| between_o(X4,X7,X6,X5)
| ~ between_o(X0,X3,X2,X1)
| ~ between_c(ax2_sk4(X0,X1,X2,X3),X7,X6,X5) ),
inference(resolution,[],[f98,f96]) ).
fof(f791,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( incident_o(ax2_sk5(ax2_sk4(X0,X1,X2,X3),sk26,X4,X5,X6),sk25)
| incident_o(ax2_sk5(ax2_sk4(X0,X1,X2,X3),sk26,X4,X5,X6),X0)
| ~ between_c(ax2_sk4(X0,X1,X2,X3),X6,X5,X4)
| ~ between_o(X0,X3,X2,X1)
| between_o(sk26,X6,X5,X4) ),
inference(resolution,[],[f779,f96]) ).
fof(f797,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( incident_o(ax2_sk5(ax2_sk4(X0,X1,X2,X3),sk25,X4,X5,X6),sk26)
| incident_o(ax2_sk5(ax2_sk4(X0,X1,X2,X3),sk25,X4,X5,X6),X0)
| ~ between_c(ax2_sk4(X0,X1,X2,X3),X6,X5,X4)
| ~ between_o(X0,X3,X2,X1)
| between_o(sk25,X6,X5,X4) ),
inference(resolution,[],[f778,f96]) ).
fof(f845,plain,
! [X2,X3,X0,X1,X4,X5] :
( incident_o(ax2_sk5(ax2_sk4(sk25,X0,X1,X2),sk26,X3,X4,X5),sk25)
| ~ between_c(ax2_sk4(sk25,X0,X1,X2),X5,X4,X3)
| ~ between_o(sk25,X2,X1,X0)
| between_o(sk26,X5,X4,X3) ),
inference(factoring,[],[f791]) ).
fof(f868,plain,
! [X2,X3,X0,X1,X4,X5] :
( incident_o(ax2_sk5(ax2_sk4(sk26,X0,X1,X2),sk25,X3,X4,X5),sk26)
| ~ between_c(ax2_sk4(sk26,X0,X1,X2),X5,X4,X3)
| ~ between_o(sk26,X2,X1,X0)
| between_o(sk25,X5,X4,X3) ),
inference(factoring,[],[f797]) ).
fof(f1266,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( incident_o(ax2_sk5(ax2_sk4(sk25,X0,X1,X2),X3,X4,X5,X6),sk26)
| incident_o(ax2_sk5(ax2_sk4(sk25,X0,X1,X2),X3,X4,X5,X6),X3)
| ~ between_o(sk25,X2,X1,X0)
| ~ between_c(ax2_sk4(sk25,X0,X1,X2),X6,X5,X4)
| between_o(X3,X6,X5,X4) ),
inference(resolution,[],[f784,f124]) ).
fof(f1267,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( incident_o(ax2_sk5(ax2_sk4(sk26,X0,X1,X2),X3,X4,X5,X6),sk25)
| incident_o(ax2_sk5(ax2_sk4(sk26,X0,X1,X2),X3,X4,X5,X6),X3)
| ~ between_o(sk26,X2,X1,X0)
| ~ between_c(ax2_sk4(sk26,X0,X1,X2),X6,X5,X4)
| between_o(X3,X6,X5,X4) ),
inference(resolution,[],[f784,f125]) ).
fof(f1275,plain,
! [X2,X3,X0,X1,X4,X5] :
( incident_o(ax2_sk5(ax2_sk4(sk26,X0,X1,X2),sk25,X3,X4,X5),sk25)
| ~ between_o(sk26,X2,X1,X0)
| ~ between_c(ax2_sk4(sk26,X0,X1,X2),X5,X4,X3)
| between_o(sk25,X5,X4,X3) ),
inference(factoring,[],[f1267]) ).
fof(f1281,plain,
! [X2,X3,X0,X1,X4,X5] :
( incident_o(ax2_sk5(ax2_sk4(sk25,X0,X1,X2),sk26,X3,X4,X5),sk26)
| ~ between_o(sk25,X2,X1,X0)
| ~ between_c(ax2_sk4(sk25,X0,X1,X2),X5,X4,X3)
| between_o(sk26,X5,X4,X3) ),
inference(factoring,[],[f1266]) ).
fof(f1309,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ between_o(sk26,X0,X1,X2)
| ~ between_c(ax2_sk4(sk26,X2,X1,X0),X3,X4,X5)
| between_o(sk25,X3,X4,X5)
| ~ incident_c(ax2_sk5(ax2_sk4(sk26,X2,X1,X0),sk25,X5,X4,X3),ax2_sk4(sk26,X2,X1,X0))
| ~ between_c(ax2_sk4(sk26,X2,X1,X0),X3,X4,X5)
| between_o(sk25,X3,X4,X5) ),
inference(resolution,[],[f1275,f101]) ).
fof(f1311,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ incident_c(ax2_sk5(ax2_sk4(sk26,X2,X1,X0),sk25,X5,X4,X3),ax2_sk4(sk26,X2,X1,X0))
| ~ between_c(ax2_sk4(sk26,X2,X1,X0),X3,X4,X5)
| between_o(sk25,X3,X4,X5)
| ~ between_o(sk26,X0,X1,X2) ),
inference(duplicate_literal_removal,[],[f1309]) ).
fof(f1315,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ between_c(ax2_sk4(sk26,X0,X1,X2),X3,X4,X5)
| between_o(sk25,X3,X4,X5)
| ~ between_o(sk26,X2,X1,X0)
| ~ incident_o(ax2_sk5(ax2_sk4(sk26,X0,X1,X2),sk25,X5,X4,X3),sk26)
| ~ between_o(sk26,X2,X1,X0) ),
inference(resolution,[],[f1311,f95]) ).
fof(f1316,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ between_c(ax2_sk4(sk26,X0,X1,X2),X3,X4,X5)
| between_o(sk25,X3,X4,X5)
| ~ between_o(sk26,X2,X1,X0)
| ~ incident_o(ax2_sk5(ax2_sk4(sk26,X0,X1,X2),sk25,X5,X4,X3),sk26) ),
inference(duplicate_literal_removal,[],[f1315]) ).
fof(f1320,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ between_c(ax2_sk4(sk26,X0,X1,X2),X3,X4,X5)
| between_o(sk25,X3,X4,X5)
| ~ between_o(sk26,X2,X1,X0) ),
inference(forward_subsumption_resolution,[],[f1316,f868]) ).
fof(f1321,plain,
! [X2,X0,X1] :
( between_o(sk25,X0,X1,X2)
| ~ between_o(sk26,X0,X1,X2)
| ~ between_o(sk26,X0,X1,X2) ),
inference(resolution,[],[f1320,f97]) ).
fof(f1325,plain,
! [X2,X0,X1] :
( ~ between_o(sk26,X0,X1,X2)
| between_o(sk25,X0,X1,X2) ),
inference(duplicate_literal_removal,[],[f1321]) ).
fof(f1328,plain,
! [X2,X0,X1] :
( between_o(sk25,X0,X1,X2)
| ~ ordered_by(sk26,X1,X2)
| ~ ordered_by(sk26,X0,X1) ),
inference(resolution,[],[f1325,f76]) ).
fof(f1334,plain,
! [X2,X0,X1] :
( ~ ordered_by(sk26,X2,X0)
| ~ ordered_by(sk26,X0,X1)
| ordered_by(sk25,X2,X0)
| ordered_by(sk25,X1,X0) ),
inference(resolution,[],[f1328,f72]) ).
fof(f1335,plain,
! [X2,X0,X1] :
( ~ ordered_by(sk26,X2,X0)
| ~ ordered_by(sk26,X0,X1)
| ordered_by(sk25,X0,X1)
| ordered_by(sk25,X0,X2) ),
inference(resolution,[],[f1328,f75]) ).
fof(f1350,plain,
! [X2,X0,X1] :
( ~ ordered_by(sk26,X0,X1)
| ordered_by(sk25,X0,X1)
| ordered_by(sk25,X0,X2)
| X0 = X2
| ~ incident_o(X0,sk26)
| ~ start_point(X2,sk26) ),
inference(resolution,[],[f1335,f79]) ).
fof(f1363,plain,
! [X2,X0,X1] :
( ~ ordered_by(sk26,X0,X1)
| ordered_by(sk25,X0,X1)
| ordered_by(sk25,X0,X2)
| X0 = X2
| ~ start_point(X2,sk26) ),
inference(forward_subsumption_resolution,[],[f1350,f90]) ).
fof(f1383,plain,
! [X0,X1] :
( ordered_by(sk25,ax2_sk8(sk26,X0),ax2_sk9(sk26,X0))
| ordered_by(X0,ax2_sk8(sk26,X0),ax2_sk9(sk26,X0))
| ordered_by(sk25,ax2_sk8(sk26,X0),X1)
| ~ start_point(X1,sk26)
| ax2_sk8(sk26,X0) = X1
| sk26 = X0 ),
inference(resolution,[],[f1363,f106]) ).
fof(f1393,plain,
! [X2,X0,X1] :
( ~ ordered_by(sk26,X0,X1)
| ordered_by(sk25,X2,X0)
| ordered_by(sk25,X1,X0)
| X0 = X2
| ~ incident_o(X0,sk26)
| ~ start_point(X2,sk26) ),
inference(resolution,[],[f1334,f79]) ).
fof(f1405,plain,
! [X2,X0,X1] :
( ~ ordered_by(sk26,X0,X1)
| ordered_by(sk25,X2,X0)
| ordered_by(sk25,X1,X0)
| X0 = X2
| ~ start_point(X2,sk26) ),
inference(forward_subsumption_resolution,[],[f1393,f90]) ).
fof(f1422,plain,
! [X0] :
( ordered_by(sk25,X0,sk27)
| ordered_by(sk25,sk28,sk27)
| sk27 = X0
| ~ start_point(X0,sk26) ),
inference(resolution,[],[f1405,f127]) ).
fof(f1423,plain,
! [X0] :
( ordered_by(sk25,X0,sk27)
| sk27 = X0
| ~ start_point(X0,sk26) ),
inference(forward_subsumption_resolution,[],[f1422,f148]) ).
fof(f1429,plain,
! [X0] :
( sk27 = X0
| ~ start_point(X0,sk26)
| ~ start_point(sk27,sk25)
| sk27 = X0 ),
inference(resolution,[],[f1423,f154]) ).
fof(f1439,plain,
! [X0] :
( sk27 = X0
| ~ start_point(X0,sk26)
| ~ start_point(sk27,sk25) ),
inference(duplicate_literal_removal,[],[f1429]) ).
fof(f1442,definition,
( spl0_14
<=> start_point(sk27,sk25) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f1443,plain,
( start_point(sk27,sk25)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f1442]) ).
fof(f1444,plain,
( ~ start_point(sk27,sk25)
| spl0_14 ),
inference(avatar_component_clause,[],[f1442]) ).
fof(f1446,definition,
( spl0_15
<=> ! [X0] :
( sk27 = X0
| ~ start_point(X0,sk26) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f1447,plain,
( ! [X0] :
( ~ start_point(X0,sk26)
| sk27 = X0 )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f1446]) ).
fof(f1448,plain,
( ~ spl0_14
| spl0_15 ),
inference(avatar_split_clause,[],[f1439,f1446,f1442]) ).
fof(f1932,plain,
! [X0] :
( ordered_by(sk25,ax2_sk8(sk26,sk25),ax2_sk9(sk26,sk25))
| ordered_by(sk25,ax2_sk8(sk26,sk25),X0)
| ~ start_point(X0,sk26)
| ax2_sk8(sk26,sk25) = X0
| sk25 = sk26 ),
inference(factoring,[],[f1383]) ).
fof(f1945,plain,
! [X0] :
( ordered_by(sk25,ax2_sk8(sk26,sk25),ax2_sk9(sk26,sk25))
| ordered_by(sk25,ax2_sk8(sk26,sk25),X0)
| ~ start_point(X0,sk26)
| ax2_sk8(sk26,sk25) = X0 ),
inference(forward_subsumption_resolution,[],[f1932,f128]) ).
fof(f1948,definition,
( spl0_28
<=> ! [X0] :
( ordered_by(sk25,ax2_sk8(sk26,sk25),X0)
| ax2_sk8(sk26,sk25) = X0
| ~ start_point(X0,sk26) ) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f1949,plain,
( ! [X0] :
( ordered_by(sk25,ax2_sk8(sk26,sk25),X0)
| ax2_sk8(sk26,sk25) = X0
| ~ start_point(X0,sk26) )
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f1948]) ).
fof(f1951,definition,
( spl0_29
<=> ordered_by(sk25,ax2_sk8(sk26,sk25),ax2_sk9(sk26,sk25)) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f1952,plain,
( ~ ordered_by(sk25,ax2_sk8(sk26,sk25),ax2_sk9(sk26,sk25))
| spl0_29 ),
inference(avatar_component_clause,[],[f1951]) ).
fof(f1953,plain,
( ordered_by(sk25,ax2_sk8(sk26,sk25),ax2_sk9(sk26,sk25))
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f1951]) ).
fof(f1954,plain,
( spl0_28
| spl0_29 ),
inference(avatar_split_clause,[],[f1945,f1951,f1948]) ).
fof(f1960,plain,
( ! [X0] :
( ax2_sk8(sk26,sk25) = X0
| ~ start_point(X0,sk26)
| ~ start_point(X0,sk25)
| ax2_sk8(sk26,sk25) = X0 )
| ~ spl0_28 ),
inference(resolution,[],[f1949,f154]) ).
fof(f1970,plain,
( ! [X0] :
( ~ start_point(X0,sk26)
| ax2_sk8(sk26,sk25) = X0
| ~ start_point(X0,sk25) )
| ~ spl0_28 ),
inference(duplicate_literal_removal,[],[f1960]) ).
fof(f1974,definition,
( spl0_30
<=> ordered_by(sk25,ax2_sk8(sk26,sk25),ax2_sk8(sk26,sk25)) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f1975,plain,
( ordered_by(sk25,ax2_sk8(sk26,sk25),ax2_sk8(sk26,sk25))
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f1974]) ).
fof(f1976,plain,
( ~ ordered_by(sk25,ax2_sk8(sk26,sk25),ax2_sk8(sk26,sk25))
| spl0_30 ),
inference(avatar_component_clause,[],[f1974]) ).
fof(f2018,definition,
( spl0_35
<=> ordered_by(sk25,ax2_sk9(sk26,sk25),ax2_sk8(sk26,sk25)) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f2019,plain,
( ~ ordered_by(sk25,ax2_sk9(sk26,sk25),ax2_sk8(sk26,sk25))
| spl0_35 ),
inference(avatar_component_clause,[],[f2018]) ).
fof(f2020,plain,
( ordered_by(sk25,ax2_sk9(sk26,sk25),ax2_sk8(sk26,sk25))
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f2018]) ).
fof(f2028,plain,
( ~ ordered_by(sk25,ax2_sk8(sk26,sk25),ax2_sk8(sk26,sk25))
| ~ spl0_35 ),
inference(resolution,[],[f2020,f495]) ).
fof(f2075,definition,
( spl0_38
<=> start_point(ax2_sk6(sk26),sk25) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f2076,plain,
( start_point(ax2_sk6(sk26),sk25)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f2075]) ).
fof(f2077,plain,
( ~ start_point(ax2_sk6(sk26),sk25)
| spl0_38 ),
inference(avatar_component_clause,[],[f2075]) ).
fof(f2083,plain,
( ax2_sk6(sk26) = ax2_sk8(sk26,sk25)
| ~ start_point(ax2_sk6(sk26),sk25)
| ~ spl0_28 ),
inference(resolution,[],[f1970,f102]) ).
fof(f2963,plain,
( sk27 = ax2_sk6(sk26)
| ~ spl0_15 ),
inference(resolution,[],[f1447,f102]) ).
fof(f2967,plain,
( start_point(sk27,sk26)
| ~ spl0_15 ),
inference(superposition,[],[f102,f2963]) ).
fof(f2981,plain,
( sk27 = ax2_sk8(sk26,sk25)
| ~ start_point(sk27,sk25)
| ~ spl0_15
| ~ spl0_28 ),
inference(resolution,[],[f2967,f1970]) ).
fof(f3106,plain,
( ~ ordered_by(sk26,ax2_sk8(sk26,sk25),ax2_sk9(sk26,sk25))
| sk25 = sk26
| ~ spl0_29 ),
inference(resolution,[],[f1953,f111]) ).
fof(f3113,plain,
( ~ ordered_by(sk25,ax2_sk8(sk26,sk25),ax2_sk8(sk26,sk25))
| ~ spl0_29 ),
inference(resolution,[],[f1953,f496]) ).
fof(f3119,plain,
( ~ ordered_by(sk26,ax2_sk8(sk26,sk25),ax2_sk9(sk26,sk25))
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f3106,f128]) ).
fof(f3124,plain,
( ax2_sk9(sk26,sk25) = ax2_sk8(sk26,sk25)
| ~ incident_o(ax2_sk9(sk26,sk25),sk26)
| ~ start_point(ax2_sk8(sk26,sk25),sk26)
| ~ spl0_29 ),
inference(resolution,[],[f3119,f79]) ).
fof(f3125,plain,
( ax2_sk9(sk26,sk25) = ax2_sk8(sk26,sk25)
| ~ start_point(ax2_sk8(sk26,sk25),sk26)
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f3124,f387]) ).
fof(f3127,plain,
( ~ spl0_9
| spl0_11
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f3125,f1951,f622,f614]) ).
fof(f3264,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ between_o(sk25,X0,X1,X2)
| ~ between_c(ax2_sk4(sk25,X2,X1,X0),X3,X4,X5)
| between_o(sk26,X3,X4,X5)
| ~ incident_c(ax2_sk5(ax2_sk4(sk25,X2,X1,X0),sk26,X5,X4,X3),ax2_sk4(sk25,X2,X1,X0))
| ~ between_c(ax2_sk4(sk25,X2,X1,X0),X3,X4,X5)
| between_o(sk26,X3,X4,X5) ),
inference(resolution,[],[f1281,f101]) ).
fof(f3266,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ incident_c(ax2_sk5(ax2_sk4(sk25,X2,X1,X0),sk26,X5,X4,X3),ax2_sk4(sk25,X2,X1,X0))
| ~ between_c(ax2_sk4(sk25,X2,X1,X0),X3,X4,X5)
| between_o(sk26,X3,X4,X5)
| ~ between_o(sk25,X0,X1,X2) ),
inference(duplicate_literal_removal,[],[f3264]) ).
fof(f3270,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ between_c(ax2_sk4(sk25,X0,X1,X2),X3,X4,X5)
| between_o(sk26,X3,X4,X5)
| ~ between_o(sk25,X2,X1,X0)
| ~ incident_o(ax2_sk5(ax2_sk4(sk25,X0,X1,X2),sk26,X5,X4,X3),sk25)
| ~ between_o(sk25,X2,X1,X0) ),
inference(resolution,[],[f3266,f95]) ).
fof(f3271,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ between_c(ax2_sk4(sk25,X0,X1,X2),X3,X4,X5)
| between_o(sk26,X3,X4,X5)
| ~ between_o(sk25,X2,X1,X0)
| ~ incident_o(ax2_sk5(ax2_sk4(sk25,X0,X1,X2),sk26,X5,X4,X3),sk25) ),
inference(duplicate_literal_removal,[],[f3270]) ).
fof(f3275,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ between_c(ax2_sk4(sk25,X0,X1,X2),X3,X4,X5)
| between_o(sk26,X3,X4,X5)
| ~ between_o(sk25,X2,X1,X0) ),
inference(forward_subsumption_resolution,[],[f3271,f845]) ).
fof(f3276,plain,
! [X2,X0,X1] :
( between_o(sk26,X0,X1,X2)
| ~ between_o(sk25,X0,X1,X2)
| ~ between_o(sk25,X0,X1,X2) ),
inference(resolution,[],[f3275,f97]) ).
fof(f3280,plain,
! [X2,X0,X1] :
( ~ between_o(sk25,X0,X1,X2)
| between_o(sk26,X0,X1,X2) ),
inference(duplicate_literal_removal,[],[f3276]) ).
fof(f3285,plain,
! [X2,X0,X1] :
( between_o(sk26,X0,X1,X2)
| ~ ordered_by(sk25,X1,X0)
| ~ ordered_by(sk25,X2,X1) ),
inference(resolution,[],[f3280,f77]) ).
fof(f3293,plain,
! [X2,X0,X1] :
( ~ ordered_by(sk25,X2,X0)
| ~ ordered_by(sk25,X0,X1)
| ordered_by(sk26,X1,X0)
| ordered_by(sk26,X2,X0) ),
inference(resolution,[],[f3285,f72]) ).
fof(f3294,plain,
! [X2,X0,X1] :
( ~ ordered_by(sk25,X2,X0)
| ~ ordered_by(sk25,X0,X1)
| ordered_by(sk26,X0,X2)
| ordered_by(sk26,X0,X1) ),
inference(resolution,[],[f3285,f75]) ).
fof(f3326,plain,
! [X2,X0,X1] :
( ~ ordered_by(sk25,X0,X1)
| ordered_by(sk26,X1,X0)
| ordered_by(sk26,X2,X0)
| X0 = X2
| ~ incident_o(X0,sk25)
| ~ start_point(X2,sk25) ),
inference(resolution,[],[f3293,f79]) ).
fof(f3391,plain,
! [X2,X0,X1] :
( ~ ordered_by(sk25,X0,X1)
| ordered_by(sk26,X1,X0)
| ordered_by(sk26,X2,X0)
| X0 = X2
| ~ start_point(X2,sk25) ),
inference(forward_subsumption_resolution,[],[f3326,f90]) ).
fof(f3717,definition,
( spl0_77
<=> start_point(sk27,sk26) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f3718,plain,
( start_point(sk27,sk26)
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f3717]) ).
fof(f3719,plain,
( ~ start_point(sk27,sk26)
| spl0_77 ),
inference(avatar_component_clause,[],[f3717]) ).
fof(f3727,definition,
( spl0_79
<=> sk27 = ax2_sk6(sk26) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f3728,plain,
( sk27 != ax2_sk6(sk26)
| spl0_79 ),
inference(avatar_component_clause,[],[f3727]) ).
fof(f3729,plain,
( sk27 = ax2_sk6(sk26)
| ~ spl0_79 ),
inference(avatar_component_clause,[],[f3727]) ).
fof(f3734,plain,
( start_point(sk27,sk26)
| ~ spl0_79 ),
inference(superposition,[],[f102,f3729]) ).
fof(f3735,plain,
( $false
| spl0_77
| ~ spl0_79 ),
inference(forward_subsumption_resolution,[],[f3734,f3719]) ).
fof(f3736,plain,
( spl0_77
| ~ spl0_79 ),
inference(avatar_contradiction_clause,[],[f3735]) ).
fof(f4155,plain,
! [X0,X1] :
( ordered_by(sk26,sk27,X0)
| ordered_by(sk26,X1,X0)
| X0 = X1
| ~ start_point(X1,sk25)
| sk27 = X0
| ~ start_point(X0,sk26) ),
inference(resolution,[],[f3391,f1423]) ).
fof(f4164,plain,
( ! [X0] :
( ordered_by(sk26,ax2_sk9(sk26,sk25),ax2_sk8(sk26,sk25))
| ordered_by(sk26,X0,ax2_sk8(sk26,sk25))
| ax2_sk8(sk26,sk25) = X0
| ~ start_point(X0,sk25) )
| ~ spl0_29 ),
inference(resolution,[],[f3391,f1953]) ).
fof(f4196,plain,
! [X0] :
( ordered_by(sk26,sk28,sk27)
| ordered_by(sk26,X0,sk27)
| sk27 = X0
| ~ start_point(X0,sk25) ),
inference(resolution,[],[f3391,f126]) ).
fof(f4198,plain,
! [X0] :
( ordered_by(sk26,X0,sk27)
| sk27 = X0
| ~ start_point(X0,sk25) ),
inference(forward_subsumption_resolution,[],[f4196,f149]) ).
fof(f4210,definition,
( spl0_80
<=> ! [X0] :
( ordered_by(sk26,X0,ax2_sk8(sk26,sk25))
| ~ start_point(X0,sk25)
| ax2_sk8(sk26,sk25) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f4211,plain,
( ! [X0] :
( ordered_by(sk26,X0,ax2_sk8(sk26,sk25))
| ~ start_point(X0,sk25)
| ax2_sk8(sk26,sk25) = X0 )
| ~ spl0_80 ),
inference(avatar_component_clause,[],[f4210]) ).
fof(f4213,definition,
( spl0_81
<=> ordered_by(sk26,ax2_sk9(sk26,sk25),ax2_sk8(sk26,sk25)) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f4215,plain,
( ordered_by(sk26,ax2_sk9(sk26,sk25),ax2_sk8(sk26,sk25))
| ~ spl0_81 ),
inference(avatar_component_clause,[],[f4213]) ).
fof(f4216,plain,
( spl0_80
| spl0_81
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f4164,f1951,f4213,f4210]) ).
fof(f4221,plain,
! [X0,X1] :
( ordered_by(sk26,X1,X0)
| X0 = X1
| ~ start_point(X1,sk25)
| sk27 = X0
| ~ start_point(X0,sk26) ),
inference(forward_subsumption_resolution,[],[f4155,f154]) ).
fof(f4234,plain,
! [X0,X1] :
( ~ start_point(X1,sk25)
| X0 = X1
| sk27 = X0
| ~ start_point(X0,sk26) ),
inference(forward_subsumption_resolution,[],[f4221,f154]) ).
fof(f4259,plain,
( ! [X0] :
( ~ start_point(X0,sk25)
| ax2_sk8(sk26,sk25) = X0
| ~ start_point(ax2_sk8(sk26,sk25),sk26)
| ax2_sk8(sk26,sk25) = X0 )
| ~ spl0_80 ),
inference(resolution,[],[f4211,f154]) ).
fof(f4269,plain,
( ! [X0] :
( ~ start_point(X0,sk25)
| ax2_sk8(sk26,sk25) = X0
| ~ start_point(ax2_sk8(sk26,sk25),sk26) )
| ~ spl0_80 ),
inference(duplicate_literal_removal,[],[f4259]) ).
fof(f4276,definition,
( spl0_84
<=> ! [X0] :
( ~ start_point(X0,sk25)
| ax2_sk8(sk26,sk25) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f4277,plain,
( ! [X0] :
( ~ start_point(X0,sk25)
| ax2_sk8(sk26,sk25) = X0 )
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f4276]) ).
fof(f4315,plain,
! [X0] :
( ~ start_point(X0,sk26)
| sk27 = X0
| ax2_sk6(sk25) = X0 ),
inference(resolution,[],[f4234,f102]) ).
fof(f4326,plain,
! [X0,X1] :
( sk27 = X0
| ~ start_point(X0,sk25)
| ordered_by(sk25,X1,X0)
| ordered_by(sk25,sk27,X0)
| X0 = X1
| ~ start_point(X1,sk26) ),
inference(resolution,[],[f4198,f1405]) ).
fof(f4335,plain,
! [X0] :
( sk27 = X0
| ~ start_point(X0,sk25)
| ~ start_point(sk27,sk26)
| sk27 = X0 ),
inference(resolution,[],[f4198,f154]) ).
fof(f4345,plain,
! [X0] :
( sk27 = X0
| ~ start_point(X0,sk25)
| ~ start_point(sk27,sk26) ),
inference(duplicate_literal_removal,[],[f4335]) ).
fof(f4351,plain,
! [X0,X1] :
( sk27 = X0
| ~ start_point(X0,sk25)
| ordered_by(sk25,sk27,X0)
| X0 = X1
| ~ start_point(X1,sk26) ),
inference(forward_subsumption_resolution,[],[f4326,f154]) ).
fof(f4365,definition,
( spl0_95
<=> ! [X0] :
( sk27 = X0
| ~ start_point(X0,sk25) ) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f4366,plain,
( ! [X0] :
( ~ start_point(X0,sk25)
| sk27 = X0 )
| ~ spl0_95 ),
inference(avatar_component_clause,[],[f4365]) ).
fof(f4377,plain,
! [X0,X1] :
( ~ start_point(X1,sk26)
| ~ start_point(X0,sk25)
| X0 = X1
| sk27 = X0 ),
inference(forward_subsumption_resolution,[],[f4351,f154]) ).
fof(f4386,plain,
( sk27 = ax2_sk6(sk25)
| ~ spl0_95 ),
inference(resolution,[],[f4366,f102]) ).
fof(f4389,plain,
( start_point(sk27,sk25)
| ~ spl0_95 ),
inference(superposition,[],[f102,f4386]) ).
fof(f4390,plain,
( $false
| spl0_14
| ~ spl0_95 ),
inference(forward_subsumption_resolution,[],[f4389,f1444]) ).
fof(f4391,plain,
( spl0_14
| ~ spl0_95 ),
inference(avatar_contradiction_clause,[],[f4390]) ).
fof(f4392,plain,
! [X0] :
( ~ start_point(X0,sk25)
| ax2_sk6(sk26) = X0
| sk27 = X0 ),
inference(resolution,[],[f4377,f102]) ).
fof(f4393,plain,
( sk27 = ax2_sk6(sk26)
| ax2_sk6(sk25) = ax2_sk6(sk26) ),
inference(resolution,[],[f4315,f102]) ).
fof(f4394,plain,
( ax2_sk6(sk25) = ax2_sk6(sk26)
| spl0_79 ),
inference(forward_subsumption_resolution,[],[f4393,f3728]) ).
fof(f4396,plain,
( ~ start_point(ax2_sk6(sk25),sk25)
| spl0_38
| spl0_79 ),
inference(superposition,[],[f2077,f4394]) ).
fof(f4397,plain,
( sk27 != ax2_sk6(sk25)
| spl0_79 ),
inference(superposition,[],[f3728,f4394]) ).
fof(f4402,plain,
( start_point(ax2_sk6(sk25),sk26)
| spl0_79 ),
inference(superposition,[],[f102,f4394]) ).
fof(f4403,plain,
( $false
| spl0_38
| spl0_79 ),
inference(forward_subsumption_resolution,[],[f4396,f102]) ).
fof(f4404,plain,
( spl0_38
| spl0_79 ),
inference(avatar_contradiction_clause,[],[f4403]) ).
fof(f4632,plain,
( ! [X0] :
( sk27 = X0
| ~ start_point(X0,sk25) )
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f4345,f3718]) ).
fof(f4639,plain,
( spl0_95
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f4632,f3717,f4365]) ).
fof(f5241,plain,
( ax2_sk6(sk25) = ax2_sk6(sk26)
| sk27 = ax2_sk6(sk25) ),
inference(resolution,[],[f4392,f102]) ).
fof(f5261,plain,
! [X2,X0,X1] :
( ~ ordered_by(sk25,X0,X1)
| ordered_by(sk26,X0,X2)
| ordered_by(sk26,X0,X1)
| X0 = X2
| ~ incident_o(X0,sk25)
| ~ start_point(X2,sk25) ),
inference(resolution,[],[f3294,f79]) ).
fof(f5321,plain,
! [X2,X0,X1] :
( ~ ordered_by(sk25,X0,X1)
| ordered_by(sk26,X0,X2)
| ordered_by(sk26,X0,X1)
| X0 = X2
| ~ start_point(X2,sk25) ),
inference(forward_subsumption_resolution,[],[f5261,f90]) ).
fof(f5414,plain,
! [X0,X1] :
( ordered_by(sk26,ax2_sk8(X0,sk25),ax2_sk9(X0,sk25))
| ordered_by(X0,ax2_sk8(X0,sk25),ax2_sk9(X0,sk25))
| ordered_by(sk26,ax2_sk8(X0,sk25),X1)
| ~ start_point(X1,sk25)
| ax2_sk8(X0,sk25) = X1
| sk25 = X0 ),
inference(resolution,[],[f5321,f106]) ).
fof(f6101,plain,
! [X0] :
( ordered_by(sk26,ax2_sk8(sk26,sk25),ax2_sk9(sk26,sk25))
| ordered_by(sk26,ax2_sk8(sk26,sk25),X0)
| ~ start_point(X0,sk25)
| ax2_sk8(sk26,sk25) = X0
| sk25 = sk26 ),
inference(factoring,[],[f5414]) ).
fof(f6667,plain,
( ax2_sk6(sk25) = ax2_sk8(sk26,sk25)
| ~ spl0_84 ),
inference(resolution,[],[f4277,f102]) ).
fof(f6668,plain,
( sk27 = ax2_sk8(sk26,sk25)
| ~ spl0_14
| ~ spl0_84 ),
inference(resolution,[],[f4277,f1443]) ).
fof(f6672,plain,
( ~ start_point(sk27,sk26)
| spl0_9
| ~ spl0_14
| ~ spl0_84 ),
inference(superposition,[],[f616,f6668]) ).
fof(f6743,plain,
( $false
| spl0_9
| ~ spl0_14
| ~ spl0_77
| ~ spl0_84 ),
inference(forward_subsumption_resolution,[],[f6672,f3718]) ).
fof(f6744,plain,
( spl0_9
| ~ spl0_14
| ~ spl0_77
| ~ spl0_84 ),
inference(avatar_contradiction_clause,[],[f6743]) ).
fof(f6864,plain,
( sk27 = ax2_sk8(sk26,sk25)
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f2981,f1443]) ).
fof(f6865,plain,
! [X0] :
( ordered_by(sk26,ax2_sk8(sk26,sk25),ax2_sk9(sk26,sk25))
| ordered_by(sk26,ax2_sk8(sk26,sk25),X0)
| ~ start_point(X0,sk25)
| ax2_sk8(sk26,sk25) = X0 ),
inference(forward_subsumption_resolution,[],[f6101,f128]) ).
fof(f6907,plain,
( ~ ordered_by(sk25,sk27,ax2_sk9(sk26,sk25))
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28
| spl0_29 ),
inference(superposition,[],[f1952,f6864]) ).
fof(f6941,plain,
( ordered_by(sk25,sk27,ax2_sk9(sk26,sk25))
| ordered_by(sk26,sk27,ax2_sk9(sk26,sk25))
| sk25 = sk26
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28 ),
inference(superposition,[],[f106,f6864]) ).
fof(f6942,plain,
( ordered_by(sk26,sk27,ax2_sk9(sk26,sk25))
| ordered_by(sk25,sk27,ax2_sk9(sk26,sk25))
| sk25 = sk26
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28 ),
inference(superposition,[],[f106,f6864]) ).
fof(f6945,plain,
( ~ ordered_by(sk26,sk27,ax2_sk9(sk26,sk25))
| sk25 = sk26
| sk27 = ax2_sk9(sk26,sk25)
| ~ incident_o(ax2_sk9(sk26,sk25),sk25)
| ~ start_point(sk27,sk25)
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28 ),
inference(superposition,[],[f211,f6864]) ).
fof(f6964,plain,
( ~ ordered_by(sk26,sk27,ax2_sk9(sk26,sk25))
| sk27 = ax2_sk9(sk26,sk25)
| ~ incident_o(ax2_sk9(sk26,sk25),sk25)
| ~ start_point(sk27,sk25)
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f6945,f128]) ).
fof(f6972,plain,
( ~ ordered_by(sk26,sk27,ax2_sk9(sk26,sk25))
| sk27 = ax2_sk9(sk26,sk25)
| ~ start_point(sk27,sk25)
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f6964,f388]) ).
fof(f6976,plain,
( ~ ordered_by(sk26,sk27,ax2_sk9(sk26,sk25))
| sk27 = ax2_sk9(sk26,sk25)
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f6972,f1443]) ).
fof(f6981,plain,
( ordered_by(sk26,sk27,ax2_sk9(sk26,sk25))
| sk25 = sk26
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28
| spl0_29 ),
inference(forward_subsumption_resolution,[],[f6942,f6907]) ).
fof(f6984,definition,
( spl0_130
<=> sk27 = ax2_sk9(sk26,sk25) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f6985,plain,
( sk27 != ax2_sk9(sk26,sk25)
| spl0_130 ),
inference(avatar_component_clause,[],[f6984]) ).
fof(f6986,plain,
( sk27 = ax2_sk9(sk26,sk25)
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f6984]) ).
fof(f6988,definition,
( spl0_131
<=> ordered_by(sk26,sk27,ax2_sk9(sk26,sk25)) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f6991,plain,
( spl0_130
| ~ spl0_131
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f6976,f1948,f1446,f1442,f6988,f6984]) ).
fof(f6992,plain,
( ordered_by(sk26,sk27,ax2_sk9(sk26,sk25))
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28
| spl0_29 ),
inference(forward_subsumption_resolution,[],[f6981,f128]) ).
fof(f6994,plain,
( spl0_131
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28
| spl0_29 ),
inference(avatar_split_clause,[],[f6992,f1951,f1948,f1446,f1442,f6988]) ).
fof(f7007,plain,
( ! [X0] :
( ~ start_point(X0,sk25)
| ax2_sk8(sk26,sk25) = X0 )
| ~ spl0_9
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f4269,f615]) ).
fof(f7015,plain,
( ordered_by(sk25,sk27,ax2_sk9(sk26,sk25))
| ordered_by(sk26,sk27,ax2_sk9(sk26,sk25))
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f6941,f128]) ).
fof(f7024,plain,
( ordered_by(sk25,sk27,sk27)
| ordered_by(sk26,sk27,ax2_sk9(sk26,sk25))
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28
| ~ spl0_130 ),
inference(forward_demodulation,[],[f7015,f6986]) ).
fof(f7030,plain,
( ordered_by(sk26,sk27,ax2_sk9(sk26,sk25))
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f7024,f497]) ).
fof(f7032,plain,
( ordered_by(sk26,sk27,sk27)
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28
| ~ spl0_130 ),
inference(forward_demodulation,[],[f7030,f6986]) ).
fof(f7035,plain,
( $false
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f7032,f498]) ).
fof(f7036,plain,
( ~ spl0_14
| ~ spl0_15
| ~ spl0_28
| ~ spl0_130 ),
inference(avatar_contradiction_clause,[],[f7035]) ).
fof(f7042,plain,
( sk27 = ax2_sk8(sk26,sk25)
| ~ spl0_11
| ~ spl0_130 ),
inference(forward_demodulation,[],[f624,f6986]) ).
fof(f7044,plain,
( spl0_84
| ~ spl0_9
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f7007,f4210,f614,f4276]) ).
fof(f7048,plain,
( ordered_by(sk26,ax2_sk9(sk26,sk25),sk27)
| ~ spl0_11
| ~ spl0_81
| ~ spl0_130 ),
inference(forward_demodulation,[],[f4215,f7042]) ).
fof(f7054,plain,
( ordered_by(sk26,sk27,sk27)
| ~ spl0_11
| ~ spl0_81
| ~ spl0_130 ),
inference(forward_demodulation,[],[f7048,f6986]) ).
fof(f7060,plain,
( $false
| ~ spl0_11
| ~ spl0_81
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f7054,f498]) ).
fof(f7061,plain,
( ~ spl0_11
| ~ spl0_81
| ~ spl0_130 ),
inference(avatar_contradiction_clause,[],[f7060]) ).
fof(f7156,plain,
( ! [X0] :
( ordered_by(sk26,ax2_sk8(sk26,sk25),X0)
| ~ start_point(X0,sk25)
| ax2_sk8(sk26,sk25) = X0 )
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f6865,f3119]) ).
fof(f7252,plain,
( ! [X0,X1] :
( ~ start_point(X0,sk25)
| ax2_sk8(sk26,sk25) = X0
| ordered_by(sk25,ax2_sk8(sk26,sk25),X0)
| ordered_by(sk25,ax2_sk8(sk26,sk25),X1)
| ax2_sk8(sk26,sk25) = X1
| ~ start_point(X1,sk26) )
| ~ spl0_29 ),
inference(resolution,[],[f7156,f1363]) ).
fof(f7396,plain,
( ! [X0,X1] :
( ~ start_point(X0,sk25)
| ax2_sk8(sk26,sk25) = X0
| ordered_by(sk25,ax2_sk8(sk26,sk25),X1)
| ax2_sk8(sk26,sk25) = X1
| ~ start_point(X1,sk26) )
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f7252,f154]) ).
fof(f7397,plain,
( spl0_28
| spl0_84
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f7396,f1951,f4276,f1948]) ).
fof(f7411,plain,
( ~ start_point(sk27,sk26)
| spl0_9
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28 ),
inference(superposition,[],[f616,f6864]) ).
fof(f7475,plain,
( $false
| spl0_9
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f7411,f3718]) ).
fof(f7476,plain,
( spl0_9
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28
| ~ spl0_77 ),
inference(avatar_contradiction_clause,[],[f7475]) ).
fof(f7479,plain,
( sk27 = ax2_sk9(sk26,sk25)
| ~ spl0_11
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28 ),
inference(forward_demodulation,[],[f624,f6864]) ).
fof(f7482,plain,
( $false
| ~ spl0_11
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28
| spl0_130 ),
inference(forward_subsumption_resolution,[],[f7479,f6985]) ).
fof(f7483,plain,
( ~ spl0_11
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28
| spl0_130 ),
inference(avatar_contradiction_clause,[],[f7482]) ).
fof(f7484,plain,
( ax2_sk6(sk25) = ax2_sk6(sk26)
| spl0_79 ),
inference(forward_subsumption_resolution,[],[f5241,f4397]) ).
fof(f7490,plain,
( ax2_sk6(sk26) = ax2_sk8(sk26,sk25)
| ~ spl0_28
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f2083,f2076]) ).
fof(f7505,plain,
( ax2_sk6(sk25) = ax2_sk8(sk26,sk25)
| ~ spl0_28
| ~ spl0_38
| spl0_79 ),
inference(forward_demodulation,[],[f7490,f7484]) ).
fof(f7594,plain,
( ~ ordered_by(sk25,ax2_sk6(sk25),ax2_sk6(sk25))
| ~ spl0_28
| spl0_30
| ~ spl0_38
| spl0_79 ),
inference(superposition,[],[f1976,f7505]) ).
fof(f7630,plain,
( ordered_by(sk25,ax2_sk6(sk25),ax2_sk9(sk26,sk25))
| ordered_by(sk26,ax2_sk6(sk25),ax2_sk9(sk26,sk25))
| sk25 = sk26
| ~ spl0_28
| ~ spl0_38
| spl0_79 ),
inference(superposition,[],[f106,f7505]) ).
fof(f7656,plain,
( ordered_by(sk25,ax2_sk6(sk25),ax2_sk9(sk26,sk25))
| ordered_by(sk26,ax2_sk6(sk25),ax2_sk9(sk26,sk25))
| ~ spl0_28
| ~ spl0_38
| spl0_79 ),
inference(forward_subsumption_resolution,[],[f7630,f128]) ).
fof(f7671,plain,
( ~ start_point(ax2_sk6(sk25),sk26)
| spl0_9
| ~ spl0_28
| ~ spl0_38
| spl0_79 ),
inference(superposition,[],[f616,f7505]) ).
fof(f7672,plain,
( $false
| spl0_9
| ~ spl0_28
| ~ spl0_38
| spl0_79 ),
inference(forward_subsumption_resolution,[],[f7671,f4402]) ).
fof(f7673,plain,
( spl0_9
| ~ spl0_28
| ~ spl0_38
| spl0_79 ),
inference(avatar_contradiction_clause,[],[f7672]) ).
fof(f7675,plain,
( ax2_sk6(sk25) = ax2_sk9(sk26,sk25)
| ~ spl0_11
| ~ spl0_28
| ~ spl0_38
| spl0_79 ),
inference(forward_demodulation,[],[f624,f7505]) ).
fof(f7679,plain,
( ~ ordered_by(sk25,ax2_sk6(sk25),ax2_sk8(sk26,sk25))
| ~ spl0_11
| ~ spl0_28
| spl0_35
| ~ spl0_38
| spl0_79 ),
inference(superposition,[],[f2019,f7675]) ).
fof(f7683,plain,
( ~ ordered_by(sk26,ax2_sk8(sk26,sk25),ax2_sk6(sk25))
| ~ spl0_11
| ~ spl0_28
| ~ spl0_29
| ~ spl0_38
| spl0_79 ),
inference(superposition,[],[f3119,f7675]) ).
fof(f7685,plain,
( ordered_by(sk26,ax2_sk6(sk25),ax2_sk8(sk26,sk25))
| ~ spl0_11
| ~ spl0_28
| ~ spl0_38
| spl0_79
| ~ spl0_81 ),
inference(superposition,[],[f4215,f7675]) ).
fof(f7710,plain,
( ordered_by(sk25,ax2_sk8(sk26,sk25),ax2_sk6(sk25))
| ordered_by(sk26,ax2_sk8(sk26,sk25),ax2_sk6(sk25))
| sk25 = sk26
| ~ spl0_11
| ~ spl0_28
| ~ spl0_38
| spl0_79 ),
inference(superposition,[],[f106,f7675]) ).
fof(f7736,plain,
( ordered_by(sk25,ax2_sk8(sk26,sk25),ax2_sk6(sk25))
| ordered_by(sk26,ax2_sk8(sk26,sk25),ax2_sk6(sk25))
| ~ spl0_11
| ~ spl0_28
| ~ spl0_38
| spl0_79 ),
inference(forward_subsumption_resolution,[],[f7710,f128]) ).
fof(f7744,plain,
( ordered_by(sk26,ax2_sk6(sk25),ax2_sk6(sk25))
| ~ spl0_11
| ~ spl0_28
| ~ spl0_38
| spl0_79
| ~ spl0_81 ),
inference(forward_demodulation,[],[f7685,f7505]) ).
fof(f7745,plain,
( ~ ordered_by(sk26,ax2_sk6(sk25),ax2_sk6(sk25))
| ~ spl0_11
| ~ spl0_28
| ~ spl0_29
| ~ spl0_38
| spl0_79 ),
inference(forward_demodulation,[],[f7683,f7505]) ).
fof(f7753,plain,
( ordered_by(sk25,ax2_sk6(sk25),ax2_sk6(sk25))
| ordered_by(sk26,ax2_sk8(sk26,sk25),ax2_sk6(sk25))
| ~ spl0_11
| ~ spl0_28
| ~ spl0_38
| spl0_79 ),
inference(forward_demodulation,[],[f7736,f7505]) ).
fof(f7758,plain,
( $false
| ~ spl0_11
| ~ spl0_28
| ~ spl0_29
| ~ spl0_38
| spl0_79
| ~ spl0_81 ),
inference(forward_subsumption_resolution,[],[f7745,f7744]) ).
fof(f7759,plain,
( ~ spl0_11
| ~ spl0_28
| ~ spl0_29
| ~ spl0_38
| spl0_79
| ~ spl0_81 ),
inference(avatar_contradiction_clause,[],[f7758]) ).
fof(f7774,plain,
( ordered_by(sk25,ax2_sk6(sk25),ax2_sk6(sk25))
| ~ spl0_28
| ~ spl0_30
| ~ spl0_38
| spl0_79 ),
inference(forward_demodulation,[],[f1975,f7505]) ).
fof(f7930,plain,
( ~ ordered_by(sk25,ax2_sk6(sk25),ax2_sk6(sk25))
| ~ spl0_29
| ~ spl0_84 ),
inference(forward_demodulation,[],[f3113,f6667]) ).
fof(f7967,plain,
( ordered_by(sk25,ax2_sk8(sk26,sk25),ax2_sk8(sk26,sk25))
| ~ spl0_11
| ~ spl0_29 ),
inference(superposition,[],[f1953,f624]) ).
fof(f8037,plain,
( ordered_by(sk25,ax2_sk6(sk25),ax2_sk6(sk25))
| ~ spl0_11
| ~ spl0_29
| ~ spl0_84 ),
inference(forward_demodulation,[],[f7967,f6667]) ).
fof(f8042,plain,
( $false
| ~ spl0_11
| ~ spl0_29
| ~ spl0_84 ),
inference(forward_subsumption_resolution,[],[f8037,f7930]) ).
fof(f8043,plain,
( ~ spl0_11
| ~ spl0_29
| ~ spl0_84 ),
inference(avatar_contradiction_clause,[],[f8042]) ).
fof(f8047,plain,
( ~ start_point(ax2_sk6(sk25),sk26)
| spl0_9
| ~ spl0_84 ),
inference(forward_demodulation,[],[f616,f6667]) ).
fof(f8051,plain,
( $false
| spl0_9
| spl0_79
| ~ spl0_84 ),
inference(forward_subsumption_resolution,[],[f8047,f4402]) ).
fof(f8052,plain,
( spl0_9
| spl0_79
| ~ spl0_84 ),
inference(avatar_contradiction_clause,[],[f8051]) ).
fof(f8064,definition,
( spl0_150
<=> ordered_by(sk26,ax2_sk6(sk25),ax2_sk9(sk26,sk25)) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f8065,plain,
( ordered_by(sk26,ax2_sk6(sk25),ax2_sk9(sk26,sk25))
| ~ spl0_150 ),
inference(avatar_component_clause,[],[f8064]) ).
fof(f8068,definition,
( spl0_151
<=> ordered_by(sk25,ax2_sk6(sk25),ax2_sk9(sk26,sk25)) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f8073,plain,
( spl0_150
| spl0_151
| ~ spl0_28
| ~ spl0_38
| spl0_79 ),
inference(avatar_split_clause,[],[f7656,f3727,f2075,f1948,f8068,f8064]) ).
fof(f8075,plain,
( ~ ordered_by(sk25,ax2_sk6(sk25),ax2_sk9(sk26,sk25))
| ~ spl0_28
| spl0_29
| ~ spl0_38
| spl0_79 ),
inference(forward_demodulation,[],[f1952,f7505]) ).
fof(f8078,plain,
( ax2_sk6(sk25) != ax2_sk9(sk26,sk25)
| spl0_11
| ~ spl0_28
| ~ spl0_38
| spl0_79 ),
inference(forward_demodulation,[],[f623,f7505]) ).
fof(f8082,plain,
( ~ spl0_151
| ~ spl0_28
| spl0_29
| ~ spl0_38
| spl0_79 ),
inference(avatar_split_clause,[],[f8075,f3727,f2075,f1951,f1948,f8068]) ).
fof(f8118,plain,
( ~ ordered_by(sk26,ax2_sk6(sk25),ax2_sk6(sk25))
| ~ spl0_150 ),
inference(resolution,[],[f8065,f496]) ).
fof(f8126,plain,
( ~ ordered_by(sk25,ax2_sk6(sk25),ax2_sk6(sk25))
| ~ spl0_28
| ~ spl0_35
| ~ spl0_38
| spl0_79 ),
inference(forward_demodulation,[],[f2028,f7505]) ).
fof(f8196,plain,
( ~ ordered_by(sk26,ax2_sk6(sk25),ax2_sk9(sk26,sk25))
| sk25 = sk26
| ax2_sk6(sk25) = ax2_sk9(sk26,sk25)
| ~ incident_o(ax2_sk9(sk26,sk25),sk25)
| ~ start_point(ax2_sk6(sk25),sk25)
| ~ spl0_28
| ~ spl0_38
| spl0_79 ),
inference(superposition,[],[f211,f7505]) ).
fof(f8215,plain,
( sk25 = sk26
| ax2_sk6(sk25) = ax2_sk9(sk26,sk25)
| ~ incident_o(ax2_sk9(sk26,sk25),sk25)
| ~ start_point(ax2_sk6(sk25),sk25)
| ~ spl0_28
| ~ spl0_38
| spl0_79
| ~ spl0_150 ),
inference(forward_subsumption_resolution,[],[f8196,f8065]) ).
fof(f8220,plain,
( ax2_sk6(sk25) = ax2_sk9(sk26,sk25)
| ~ incident_o(ax2_sk9(sk26,sk25),sk25)
| ~ start_point(ax2_sk6(sk25),sk25)
| ~ spl0_28
| ~ spl0_38
| spl0_79
| ~ spl0_150 ),
inference(forward_subsumption_resolution,[],[f8215,f128]) ).
fof(f8221,plain,
( ~ incident_o(ax2_sk9(sk26,sk25),sk25)
| ~ start_point(ax2_sk6(sk25),sk25)
| spl0_11
| ~ spl0_28
| ~ spl0_38
| spl0_79
| ~ spl0_150 ),
inference(forward_subsumption_resolution,[],[f8220,f8078]) ).
fof(f8222,plain,
( ~ start_point(ax2_sk6(sk25),sk25)
| spl0_11
| ~ spl0_28
| ~ spl0_38
| spl0_79
| ~ spl0_150 ),
inference(forward_subsumption_resolution,[],[f8221,f388]) ).
fof(f8223,plain,
( $false
| spl0_11
| ~ spl0_28
| ~ spl0_38
| spl0_79
| ~ spl0_150 ),
inference(forward_subsumption_resolution,[],[f8222,f102]) ).
fof(f8224,plain,
( spl0_11
| ~ spl0_28
| ~ spl0_38
| spl0_79
| ~ spl0_150 ),
inference(avatar_contradiction_clause,[],[f8223]) ).
fof(f8236,plain,
( ordered_by(sk26,ax2_sk8(sk26,sk25),ax2_sk6(sk25))
| ~ spl0_11
| ~ spl0_28
| spl0_30
| ~ spl0_38
| spl0_79 ),
inference(forward_subsumption_resolution,[],[f7753,f7594]) ).
fof(f8244,plain,
( ordered_by(sk26,ax2_sk6(sk25),ax2_sk6(sk25))
| ~ spl0_11
| ~ spl0_28
| spl0_30
| ~ spl0_38
| spl0_79 ),
inference(forward_demodulation,[],[f8236,f7505]) ).
fof(f8248,plain,
( $false
| ~ spl0_11
| ~ spl0_28
| spl0_30
| ~ spl0_38
| spl0_79
| ~ spl0_150 ),
inference(forward_subsumption_resolution,[],[f8244,f8118]) ).
fof(f8249,plain,
( ~ spl0_11
| ~ spl0_28
| spl0_30
| ~ spl0_38
| spl0_79
| ~ spl0_150 ),
inference(avatar_contradiction_clause,[],[f8248]) ).
fof(f8251,plain,
( $false
| ~ spl0_28
| ~ spl0_30
| ~ spl0_35
| ~ spl0_38
| spl0_79 ),
inference(forward_subsumption_resolution,[],[f8126,f7774]) ).
fof(f8252,plain,
( ~ spl0_28
| ~ spl0_30
| ~ spl0_35
| ~ spl0_38
| spl0_79 ),
inference(avatar_contradiction_clause,[],[f8251]) ).
fof(f8260,plain,
( ~ ordered_by(sk25,ax2_sk6(sk25),ax2_sk6(sk25))
| ~ spl0_11
| ~ spl0_28
| spl0_35
| ~ spl0_38
| spl0_79 ),
inference(forward_demodulation,[],[f7679,f7505]) ).
fof(f8268,plain,
( $false
| ~ spl0_11
| ~ spl0_28
| ~ spl0_30
| spl0_35
| ~ spl0_38
| spl0_79 ),
inference(forward_subsumption_resolution,[],[f8260,f7774]) ).
fof(f8269,plain,
( ~ spl0_11
| ~ spl0_28
| ~ spl0_30
| spl0_35
| ~ spl0_38
| spl0_79 ),
inference(avatar_contradiction_clause,[],[f8268]) ).
cnf(s8,plain,
( ~ spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f1448]) ).
cnf(s19,plain,
( spl0_28
| spl0_29 ),
inference(sat_conversion,[],[f1954]) ).
cnf(s39,plain,
( ~ spl0_9
| spl0_11
| ~ spl0_29 ),
inference(sat_conversion,[],[f3127]) ).
cnf(s60,plain,
( spl0_77
| ~ spl0_79 ),
inference(sat_conversion,[],[f3736]) ).
cnf(s77,plain,
( ~ spl0_29
| spl0_80
| spl0_81 ),
inference(sat_conversion,[],[f4216]) ).
cnf(s90,plain,
( spl0_14
| ~ spl0_95 ),
inference(sat_conversion,[],[f4391]) ).
cnf(s91,plain,
( spl0_38
| spl0_79 ),
inference(sat_conversion,[],[f4404]) ).
cnf(s104,plain,
( ~ spl0_77
| spl0_95 ),
inference(sat_conversion,[],[f4639]) ).
cnf(s229,plain,
( spl0_9
| ~ spl0_14
| ~ spl0_77
| ~ spl0_84 ),
inference(sat_conversion,[],[f6744]) ).
cnf(s237,plain,
( ~ spl0_14
| ~ spl0_15
| ~ spl0_28
| spl0_130
| ~ spl0_131 ),
inference(sat_conversion,[],[f6991]) ).
cnf(s238,plain,
( ~ spl0_14
| ~ spl0_15
| ~ spl0_28
| spl0_29
| spl0_131 ),
inference(sat_conversion,[],[f6994]) ).
cnf(s244,plain,
( ~ spl0_14
| ~ spl0_15
| ~ spl0_28
| ~ spl0_130 ),
inference(sat_conversion,[],[f7036]) ).
cnf(s245,plain,
( ~ spl0_9
| ~ spl0_80
| spl0_84 ),
inference(sat_conversion,[],[f7044]) ).
cnf(s246,plain,
( ~ spl0_11
| ~ spl0_81
| ~ spl0_130 ),
inference(sat_conversion,[],[f7061]) ).
cnf(s275,plain,
( spl0_28
| ~ spl0_29
| spl0_84 ),
inference(sat_conversion,[],[f7397]) ).
cnf(s277,plain,
( spl0_9
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28
| ~ spl0_77 ),
inference(sat_conversion,[],[f7476]) ).
cnf(s279,plain,
( ~ spl0_11
| ~ spl0_14
| ~ spl0_15
| ~ spl0_28
| spl0_130 ),
inference(sat_conversion,[],[f7483]) ).
cnf(s287,plain,
( spl0_9
| ~ spl0_28
| ~ spl0_38
| spl0_79 ),
inference(sat_conversion,[],[f7673]) ).
cnf(s290,plain,
( ~ spl0_11
| ~ spl0_28
| ~ spl0_29
| ~ spl0_38
| spl0_79
| ~ spl0_81 ),
inference(sat_conversion,[],[f7759]) ).
cnf(s308,plain,
( ~ spl0_11
| ~ spl0_29
| ~ spl0_84 ),
inference(sat_conversion,[],[f8043]) ).
cnf(s310,plain,
( spl0_9
| spl0_79
| ~ spl0_84 ),
inference(sat_conversion,[],[f8052]) ).
cnf(s314,plain,
( ~ spl0_28
| ~ spl0_38
| spl0_79
| spl0_150
| spl0_151 ),
inference(sat_conversion,[],[f8073]) ).
cnf(s315,plain,
( ~ spl0_28
| spl0_29
| ~ spl0_38
| spl0_79
| ~ spl0_151 ),
inference(sat_conversion,[],[f8082]) ).
cnf(s325,plain,
( spl0_11
| ~ spl0_28
| ~ spl0_38
| spl0_79
| ~ spl0_150 ),
inference(sat_conversion,[],[f8224]) ).
cnf(s329,plain,
( ~ spl0_11
| ~ spl0_28
| spl0_30
| ~ spl0_38
| spl0_79
| ~ spl0_150 ),
inference(sat_conversion,[],[f8249]) ).
cnf(s330,plain,
( ~ spl0_28
| ~ spl0_30
| ~ spl0_35
| ~ spl0_38
| spl0_79 ),
inference(sat_conversion,[],[f8252]) ).
cnf(s334,plain,
( ~ spl0_11
| ~ spl0_28
| ~ spl0_30
| spl0_35
| ~ spl0_38
| spl0_79 ),
inference(sat_conversion,[],[f8269]) ).
cnf(s341,plain,
( spl0_79
| spl0_9 ),
inference(rat,[],[s275,s19,s287,s91,s310]) ).
cnf(s342,plain,
( ~ spl0_14
| ~ spl0_77
| ~ spl0_15
| spl0_9 ),
inference(rat,[],[s275,s19,s229,s277]) ).
cnf(s343,plain,
spl0_9,
inference(rat,[],[s342,s8,s90,s104,s60,s341]) ).
cnf(s344,plain,
( ~ spl0_29
| spl0_28 ),
inference(rat,[],[s308,s39,s275,s343]) ).
cnf(s345,plain,
spl0_28,
inference(rat,[],[s344,s19]) ).
cnf(s346,plain,
( spl0_79
| ~ spl0_29 ),
inference(rat,[],[s290,s91,s77,s245,s308,s39,s345,s343]) ).
cnf(s347,plain,
( ~ spl0_11
| ~ spl0_29 ),
inference(rat,[],[s279,s8,s90,s104,s60,s346,s246,s77,s245,s308,s343,s345]) ).
cnf(s348,plain,
~ spl0_29,
inference(rat,[],[s347,s39,s343]) ).
cnf(s349,plain,
( ~ spl0_150
| ~ spl0_38
| ~ spl0_11
| spl0_79 ),
inference(rat,[],[s334,s330,s329,s345]) ).
cnf(s350,plain,
( spl0_79
| ~ spl0_11 ),
inference(rat,[],[s349,s314,s315,s91,s345,s348]) ).
cnf(s352,plain,
( ~ spl0_38
| spl0_79
| spl0_11 ),
inference(rat,[],[s314,s315,s325,s348,s345]) ).
cnf(s353,plain,
spl0_79,
inference(rat,[],[s352,s350,s91]) ).
cnf(s354,plain,
spl0_77,
inference(rat,[],[s60,s353]) ).
cnf(s355,plain,
spl0_95,
inference(rat,[],[s104,s354]) ).
cnf(s356,plain,
spl0_14,
inference(rat,[],[s90,s355]) ).
cnf(s357,plain,
spl0_15,
inference(rat,[],[s8,s356]) ).
cnf(s359,plain,
spl0_131,
inference(rat,[],[s238,s345,s348,s357,s356]) ).
cnf(s361,plain,
~ spl0_130,
inference(rat,[],[s244,s345,s357,s356]) ).
cnf(s363,plain,
$false,
inference(rat,[],[s237,s359,s361,s345,s356,s357]) ).
fof(f8271,plain,
$false,
inference(avatar_sat_refutation,[],[s363]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO137-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.09/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 07:13:15 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.39 Running first-order theorem proving
% 0.14/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
% 8.83/2.08 % (2055039)Input is clausal, will run a generic CNF schedule.
% 8.83/2.08 % (2055045)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2090486696:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.83/2.08 % (2055044)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=3479826391:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.83/2.08 % (2055050)dis-21_1_sil=8000:lcm=predicate:random_seed=2866553257: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)
% 8.83/2.08 % (2055049)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=422093033:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.83/2.08 % (2055047)lrs+10_1_sil=8000:sp=occurrence:random_seed=3781341249:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.83/2.08 % (2055048)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1692246961:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.83/2.08 % (2055046)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1029649081:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.83/2.08 % (2055047)Refutation not found, incomplete strategy
% 8.83/2.08 % (2055047)------------------------------
% 8.83/2.08 % (2055047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.83/2.08 % (2055047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.83/2.08 % (2055047)CaDiCaL version: 2.1.3
% 8.83/2.08 % (2055047)Termination reason: Refutation not found, incomplete strategy
% 8.83/2.08 % (2055047)Time elapsed: 0.001 s
% 8.83/2.08 % (2055047)Peak memory usage: 87 MB
% 8.83/2.08 % (2055048)Refutation not found, incomplete strategy
% 8.83/2.08 % (2055048)------------------------------
% 8.83/2.08 % (2055048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.83/2.08 % (2055048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.83/2.08 % (2055048)CaDiCaL version: 2.1.3
% 8.83/2.08 % (2055048)Termination reason: Refutation not found, incomplete strategy
% 8.83/2.08 % (2055048)Time elapsed: 0.001 s
% 8.83/2.08 % (2055048)Peak memory usage: 88 MB
% 8.83/2.08 % (2055048)Instructions burned: 1 (million)
% 8.83/2.08 % (2055050)Instruction limit reached!
% 8.83/2.08 % (2055050)------------------------------
% 8.83/2.08 % (2055050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.83/2.08 % (2055050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.83/2.08 % (2055050)CaDiCaL version: 2.1.3
% 8.83/2.08 % (2055050)Termination reason: Instruction limit
% 8.83/2.08 % (2055050)Termination phase: Saturation
% 8.83/2.08 % (2055050)Time elapsed: 0.071 s
% 8.83/2.08 % (2055050)Peak memory usage: 88 MB
% 8.83/2.08 % (2055050)Instructions burned: 119 (million)
% 8.83/2.08 % (2055049)Instruction limit reached!
% 8.83/2.08 % (2055049)------------------------------
% 8.83/2.08 % (2055049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.83/2.08 % (2055049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.83/2.08 % (2055049)CaDiCaL version: 2.1.3
% 8.83/2.08 % (2055049)Termination reason: Instruction limit
% 8.83/2.08 % (2055049)Termination phase: Saturation
% 8.83/2.08 % (2055049)Time elapsed: 0.121 s
% 8.83/2.08 % (2055049)Peak memory usage: 89 MB
% 8.83/2.08 % (2055049)Instructions burned: 181 (million)
% 8.83/2.08 % (2055058)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=179079600:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 8.83/2.08 % (2055058)Refutation not found, incomplete strategy
% 8.83/2.08 % (2055058)------------------------------
% 8.83/2.08 % (2055058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.83/2.08 % (2055058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.83/2.08 % (2055058)CaDiCaL version: 2.1.3
% 8.83/2.08 % (2055058)Termination reason: Refutation not found, incomplete strategy
% 8.83/2.08 % (2055058)Time elapsed: 0.001 s
% 8.83/2.08 % (2055058)Peak memory usage: 88 MB
% 8.83/2.08 % (2055047)------------------------------
% 8.83/2.08 % (2055047)------------------------------
% 8.83/2.08 % (2055048)------------------------------
% 8.83/2.08 % (2055048)------------------------------
% 8.83/2.08 % (2055059)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2307633826: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)
% 8.83/2.08 % (2055059)Refutation not found, incomplete strategy
% 8.83/2.08 % (2055059)------------------------------
% 8.83/2.08 % (2055059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.83/2.08 % (2055059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.83/2.08 % (2055059)CaDiCaL version: 2.1.3
% 8.83/2.08 % (2055059)Termination reason: Refutation not found, incomplete strategy
% 8.83/2.08 % (2055059)Time elapsed: 0.007 s
% 8.83/2.08 % (2055059)Peak memory usage: 88 MB
% 8.83/2.08 % (2055059)Instructions burned: 10 (million)
% 8.83/2.08 % (2055062)lrs+10_64_to=lpo:sil=8000:random_seed=396159158:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 8.83/2.08 % (2055061)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=222041062:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 8.83/2.08 % (2055061)Refutation not found, incomplete strategy
% 8.83/2.08 % (2055061)------------------------------
% 8.83/2.08 % (2055061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.83/2.08 % (2055061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.83/2.08 % (2055061)CaDiCaL version: 2.1.3
% 8.83/2.08 % (2055061)Termination reason: Refutation not found, incomplete strategy
% 8.83/2.08 % (2055061)Time elapsed: 0.003 s
% 8.83/2.08 % (2055061)Peak memory usage: 88 MB
% 8.83/2.08 % (2055061)Instructions burned: 3 (million)
% 8.83/2.08 % (2055058)------------------------------
% 8.83/2.08 % (2055058)------------------------------
% 8.83/2.08 % (2055062)Instruction limit reached!
% 8.83/2.08 % (2055062)------------------------------
% 8.83/2.08 % (2055062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.83/2.08 % (2055062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.83/2.08 % (2055062)CaDiCaL version: 2.1.3
% 8.83/2.08 % (2055062)Termination reason: Instruction limit
% 8.83/2.08 % (2055062)Termination phase: Saturation
% 8.83/2.08 % (2055062)Time elapsed: 0.071 s
% 8.83/2.08 % (2055062)Peak memory usage: 89 MB
% 8.83/2.08 % (2055062)Instructions burned: 127 (million)
% 8.83/2.08 % (2055059)------------------------------
% 8.83/2.08 % (2055059)------------------------------
% 8.83/2.08 % (2055066)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=459487664:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 8.83/2.08 % (2055067)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=260524925:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 8.83/2.08 % (2055061)------------------------------
% 8.83/2.08 % (2055061)------------------------------
% 8.83/2.08 % (2055068)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1726961384:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 8.83/2.08 % (2055066)Instruction limit reached!
% 8.83/2.08 % (2055066)------------------------------
% 8.83/2.08 % (2055066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.83/2.08 % (2055066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.83/2.08 % (2055066)CaDiCaL version: 2.1.3
% 8.83/2.08 % (2055066)Termination reason: Instruction limit
% 8.83/2.08 % (2055066)Termination phase: Saturation
% 8.83/2.08 % (2055066)Time elapsed: 0.110 s
% 8.83/2.08 % (2055066)Peak memory usage: 89 MB
% 8.83/2.08 % (2055066)Instructions burned: 194 (million)
% 8.83/2.08 % (2055067)Instruction limit reached!
% 8.83/2.08 % (2055067)------------------------------
% 8.83/2.08 % (2055067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.83/2.08 % (2055067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.83/2.08 % (2055067)CaDiCaL version: 2.1.3
% 8.83/2.08 % (2055067)Termination reason: Instruction limit
% 8.83/2.08 % (2055067)Termination phase: Saturation
% 8.83/2.08 % (2055067)Time elapsed: 0.101 s
% 8.83/2.08 % (2055067)Peak memory usage: 90 MB
% 8.83/2.08 % (2055067)Instructions burned: 157 (million)
% 8.83/2.08 % (2055071)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=2064445054:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 8.83/2.08 % (2055071)Refutation not found, incomplete strategy
% 8.83/2.08 % (2055071)------------------------------
% 8.83/2.08 % (2055071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.83/2.08 % (2055071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.83/2.08 % (2055071)CaDiCaL version: 2.1.3
% 8.83/2.08 % (2055071)Termination reason: Refutation not found, incomplete strategy
% 8.83/2.08 % (2055071)Time elapsed: 0.001 s
% 8.83/2.08 % (2055071)Peak memory usage: 88 MB
% 8.83/2.08 % (2055071)Instructions burned: 1 (million)
% 8.83/2.08 % (2055073)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2868182317:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 8.83/2.08 % (2055074)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=285773351:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 8.83/2.08 % (2055073)Instruction limit reached!
% 8.83/2.08 % (2055073)------------------------------
% 8.83/2.08 % (2055073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.83/2.08 % (2055073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.83/2.08 % (2055073)CaDiCaL version: 2.1.3
% 8.83/2.08 % (2055073)Termination reason: Instruction limit
% 8.83/2.08 % (2055073)Termination phase: Saturation
% 8.83/2.08 % (2055073)Time elapsed: 0.064 s
% 8.83/2.08 % (2055073)Peak memory usage: 89 MB
% 8.83/2.08 % (2055073)Instructions burned: 108 (million)
% 8.83/2.08 % (2055044)First to succeed.
% 8.83/2.08 % (2055044)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2055039"
% 8.83/2.08 % (2055074)Instruction limit reached!
% 8.83/2.08 % (2055074)------------------------------
% 8.83/2.08 % (2055074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.83/2.08 % (2055074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.83/2.08 % (2055074)CaDiCaL version: 2.1.3
% 8.83/2.08 % (2055074)Termination reason: Instruction limit
% 8.83/2.08 % (2055074)Termination phase: Saturation
% 8.83/2.08 % (2055074)Time elapsed: 0.152 s
% 8.83/2.08 % (2055074)Peak memory usage: 89 MB
% 8.83/2.08 % (2055074)Instructions burned: 242 (million)
% 8.83/2.08 % (2055071)------------------------------
% 8.83/2.08 % (2055071)------------------------------
% 8.83/2.08 % (2055078)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=713005255:cond=fast:i=5208:av=off_2989 on theBenchmark for (2989ds/5208Mi)
% 8.83/2.08 % (2055044)Refutation found. Thanks to Tanya!
% 8.83/2.08 % SZS status Unsatisfiable for theBenchmark
% 8.83/2.08 % SZS output start Proof for theBenchmark
% See solution above
% 9.36/2.28 % (2055044)------------------------------
% 9.36/2.28 % (2055044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.36/2.28 % (2055044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.36/2.28 % (2055044)CaDiCaL version: 2.1.3
% 9.36/2.28 % (2055044)Termination reason: Refutation
% 9.36/2.28 % (2055044)Time elapsed: 0.938 s
% 9.36/2.28 % (2055044)Peak memory usage: 136 MB
% 9.36/2.28 % (2055044)Instructions burned: 1948 (million)
% 9.36/2.28 % (2055044)------------------------------
% 9.36/2.28 % (2055044)------------------------------
% 9.36/2.28 % (2055039)Success in time 1.248 s
% 9.36/2.28 % Vampire exiting
%------------------------------------------------------------------------------