%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO138+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.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 : Theorem 14.89s 13.09s
% Output : Refutation 15.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 47
% Syntax : Number of formulae : 557 ( 27 unt; 37 def)
% Number of atoms : 2107 ( 387 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 2472 ( 922 ~;1411 |; 85 &)
% ( 46 <=>; 7 =>; 0 <=; 1 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 46 ( 44 usr; 36 prp; 0-4 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-4 aty)
% Number of variables : 527 ( 0 sgn 498 !; 29 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0,X1] :
( inner_point(X0,X1)
<=> ( incident_c(X0,X1)
& ~ end_point(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inner_point_defn) ).
fof(f17,axiom,
! [X0,X1,X2,X3] :
( between_c(X0,X1,X2,X3)
<=> ( X1 != X3
& ? [X4] :
( part_of(X4,X0)
& end_point(X1,X4)
& end_point(X3,X4)
& inner_point(X2,X4) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',between_c_defn) ).
fof(f18,axiom,
! [X0,X1,X2,X3] :
( between_o(X0,X1,X2,X3)
<=> ( ( ordered_by(X0,X1,X2)
& ordered_by(X0,X2,X3) )
| ( ordered_by(X0,X3,X2)
& ordered_by(X0,X2,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',between_o_defn) ).
fof(f19,axiom,
! [X0,X1] :
( start_point(X0,X1)
<=> ( incident_o(X0,X1)
& ! [X2] :
( ( X0 != X2
& incident_o(X2,X1) )
=> ordered_by(X1,X0,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',start_point_defn) ).
fof(f21,axiom,
! [X0,X1,X2] :
( ordered_by(X0,X1,X2)
=> ( incident_o(X1,X0)
& incident_o(X2,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',o1) ).
fof(f23,axiom,
! [X0,X1,X2,X3] :
( between_o(X3,X0,X1,X2)
<=> ? [X4] :
( ! [X0] :
( incident_o(X0,X3)
<=> incident_c(X0,X4) )
& between_c(X4,X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',o3) ).
fof(f24,axiom,
! [X0] :
? [X1] : start_point(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',o4) ).
fof(f26,axiom,
! [X0,X1] :
( ! [X2,X3] :
( ordered_by(X0,X2,X3)
<=> ordered_by(X1,X2,X3) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',o6) ).
fof(f27,axiom,
! [X0,X1] :
( X0 = underlying_curve(X1)
<=> ! [X2] :
( incident_o(X2,X1)
<=> incident_c(X2,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',underlying_curve_defn) ).
fof(f28,conjecture,
! [X0,X1] :
( ( underlying_curve(X0) = underlying_curve(X1)
& ? [X2,X3] :
( ordered_by(X0,X2,X3)
& ordered_by(X1,X2,X3) ) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',corollary_4_21) ).
fof(f29,negated_conjecture,
~ ! [X0,X1] :
( ( underlying_curve(X0) = underlying_curve(X1)
& ? [X2,X3] :
( ordered_by(X0,X2,X3)
& ordered_by(X1,X2,X3) ) )
=> X0 = X1 ),
inference(negated_conjecture,[status(cth)],[f28]) ).
fof(f30,plain,
! [X0,X1,X2,X3] :
( between_o(X3,X0,X1,X2)
<=> ? [X4] :
( ! [X5] :
( incident_o(X5,X3)
<=> incident_c(X5,X4) )
& between_c(X4,X0,X1,X2) ) ),
inference(rectify,[],[f23]) ).
fof(f31,plain,
! [X0,X1] :
( start_point(X0,X1)
=> ( incident_o(X0,X1)
& ! [X2] :
( ( X0 != X2
& incident_o(X2,X1) )
=> ordered_by(X1,X0,X2) ) ) ),
inference(unused_predicate_definition_removal,[],[f19]) ).
fof(f51,plain,
! [X0,X1] :
( ( incident_o(X0,X1)
& ! [X2] :
( ordered_by(X1,X0,X2)
| X0 = X2
| ~ incident_o(X2,X1) ) )
| ~ start_point(X0,X1) ),
inference(ennf_transformation,[],[f31]) ).
fof(f52,plain,
! [X0,X1] :
( ( incident_o(X0,X1)
& ! [X2] :
( ordered_by(X1,X0,X2)
| X0 = X2
| ~ incident_o(X2,X1) ) )
| ~ start_point(X0,X1) ),
inference(flattening,[],[f51]) ).
fof(f53,plain,
! [X0,X1,X2] :
( ( incident_o(X1,X0)
& incident_o(X2,X0) )
| ~ ordered_by(X0,X1,X2) ),
inference(ennf_transformation,[],[f21]) ).
fof(f56,plain,
! [X0,X1] :
( X0 = X1
| ? [X2,X3] :
( ordered_by(X0,X2,X3)
<~> ordered_by(X1,X2,X3) ) ),
inference(ennf_transformation,[],[f26]) ).
fof(f57,plain,
? [X0,X1] :
( X0 != X1
& underlying_curve(X0) = underlying_curve(X1)
& ? [X2,X3] :
( ordered_by(X0,X2,X3)
& ordered_by(X1,X2,X3) ) ),
inference(ennf_transformation,[],[f29]) ).
fof(f58,plain,
? [X0,X1] :
( X0 != X1
& underlying_curve(X0) = underlying_curve(X1)
& ? [X2,X3] :
( ordered_by(X0,X2,X3)
& ordered_by(X1,X2,X3) ) ),
inference(flattening,[],[f57]) ).
fof(f70,plain,
! [X0,X1] :
( ( inner_point(X0,X1)
| ~ incident_c(X0,X1)
| end_point(X0,X1) )
& ( ( incident_c(X0,X1)
& ~ end_point(X0,X1) )
| ~ inner_point(X0,X1) ) ),
inference(nnf_transformation,[],[f4]) ).
fof(f71,plain,
! [X0,X1] :
( ( inner_point(X0,X1)
| ~ incident_c(X0,X1)
| end_point(X0,X1) )
& ( ( incident_c(X0,X1)
& ~ end_point(X0,X1) )
| ~ inner_point(X0,X1) ) ),
inference(flattening,[],[f70]) ).
fof(f87,plain,
! [X0,X1,X2,X3] :
( ( between_c(X0,X1,X2,X3)
| X1 = X3
| ! [X4] :
( ~ part_of(X4,X0)
| ~ end_point(X1,X4)
| ~ end_point(X3,X4)
| ~ inner_point(X2,X4) ) )
& ( ( X1 != X3
& ? [X4] :
( part_of(X4,X0)
& end_point(X1,X4)
& end_point(X3,X4)
& inner_point(X2,X4) ) )
| ~ between_c(X0,X1,X2,X3) ) ),
inference(nnf_transformation,[],[f17]) ).
fof(f88,plain,
! [X0,X1,X2,X3] :
( ( between_c(X0,X1,X2,X3)
| X1 = X3
| ! [X4] :
( ~ part_of(X4,X0)
| ~ end_point(X1,X4)
| ~ end_point(X3,X4)
| ~ inner_point(X2,X4) ) )
& ( ( X1 != X3
& ? [X4] :
( part_of(X4,X0)
& end_point(X1,X4)
& end_point(X3,X4)
& inner_point(X2,X4) ) )
| ~ between_c(X0,X1,X2,X3) ) ),
inference(flattening,[],[f87]) ).
fof(f89,plain,
! [X0,X1,X2,X3] :
( ( between_c(X0,X1,X2,X3)
| X1 = X3
| ! [X4] :
( ~ part_of(X4,X0)
| ~ end_point(X1,X4)
| ~ end_point(X3,X4)
| ~ inner_point(X2,X4) ) )
& ( ( X1 != X3
& ? [X5] :
( part_of(X5,X0)
& end_point(X1,X5)
& end_point(X3,X5)
& inner_point(X2,X5) ) )
| ~ between_c(X0,X1,X2,X3) ) ),
inference(rectify,[],[f88]) ).
fof(f90,plain,
! [X0,X1,X2,X3] :
( ( between_c(X0,X1,X2,X3)
| X1 = X3
| ! [X4] :
( ~ part_of(X4,X0)
| ~ end_point(X1,X4)
| ~ end_point(X3,X4)
| ~ inner_point(X2,X4) ) )
& ( ( X1 != X3
& part_of(sK13(X0,X1,X2,X3),X0)
& end_point(X1,sK13(X0,X1,X2,X3))
& end_point(X3,sK13(X0,X1,X2,X3))
& inner_point(X2,sK13(X0,X1,X2,X3)) )
| ~ between_c(X0,X1,X2,X3) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(X5,sK13(X0,X1,X2,X3))],[f89]) ).
fof(f91,plain,
! [X0,X1,X2,X3] :
( ( between_o(X0,X1,X2,X3)
| ( ( ~ ordered_by(X0,X1,X2)
| ~ ordered_by(X0,X2,X3) )
& ( ~ ordered_by(X0,X3,X2)
| ~ ordered_by(X0,X2,X1) ) ) )
& ( ( ordered_by(X0,X1,X2)
& ordered_by(X0,X2,X3) )
| ( ordered_by(X0,X3,X2)
& ordered_by(X0,X2,X1) )
| ~ between_o(X0,X1,X2,X3) ) ),
inference(nnf_transformation,[],[f18]) ).
fof(f92,plain,
! [X0,X1,X2,X3] :
( ( between_o(X0,X1,X2,X3)
| ( ( ~ ordered_by(X0,X1,X2)
| ~ ordered_by(X0,X2,X3) )
& ( ~ ordered_by(X0,X3,X2)
| ~ ordered_by(X0,X2,X1) ) ) )
& ( ( ordered_by(X0,X1,X2)
& ordered_by(X0,X2,X3) )
| ( ordered_by(X0,X3,X2)
& ordered_by(X0,X2,X1) )
| ~ between_o(X0,X1,X2,X3) ) ),
inference(flattening,[],[f91]) ).
fof(f95,plain,
! [X0,X1,X2,X3] :
( ( between_o(X3,X0,X1,X2)
| ! [X4] :
( ? [X5] :
( ( ~ incident_c(X5,X4)
| ~ incident_o(X5,X3) )
& ( incident_c(X5,X4)
| incident_o(X5,X3) ) )
| ~ between_c(X4,X0,X1,X2) ) )
& ( ? [X4] :
( ! [X5] :
( ( incident_o(X5,X3)
| ~ incident_c(X5,X4) )
& ( incident_c(X5,X4)
| ~ incident_o(X5,X3) ) )
& between_c(X4,X0,X1,X2) )
| ~ between_o(X3,X0,X1,X2) ) ),
inference(nnf_transformation,[],[f30]) ).
fof(f96,plain,
! [X0,X1,X2,X3] :
( ( between_o(X3,X0,X1,X2)
| ! [X4] :
( ? [X5] :
( ( ~ incident_c(X5,X4)
| ~ incident_o(X5,X3) )
& ( incident_c(X5,X4)
| incident_o(X5,X3) ) )
| ~ between_c(X4,X0,X1,X2) ) )
& ( ? [X6] :
( ! [X7] :
( ( incident_o(X7,X3)
| ~ incident_c(X7,X6) )
& ( incident_c(X7,X6)
| ~ incident_o(X7,X3) ) )
& between_c(X6,X0,X1,X2) )
| ~ between_o(X3,X0,X1,X2) ) ),
inference(rectify,[],[f95]) ).
fof(f97,plain,
! [X0,X1,X2,X3] :
( ( between_o(X3,X0,X1,X2)
| ! [X4] :
( ( ( ~ incident_c(sK15(X3,X4),X4)
| ~ incident_o(sK15(X3,X4),X3) )
& ( incident_c(sK15(X3,X4),X4)
| incident_o(sK15(X3,X4),X3) ) )
| ~ between_c(X4,X0,X1,X2) ) )
& ( ( ! [X7] :
( ( incident_o(X7,X3)
| ~ incident_c(X7,sK16(X0,X1,X2,X3)) )
& ( incident_c(X7,sK16(X0,X1,X2,X3))
| ~ incident_o(X7,X3) ) )
& between_c(sK16(X0,X1,X2,X3),X0,X1,X2) )
| ~ between_o(X3,X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16]),skolemize(X5,sK15(X3,X4)),skolemize(X6,sK16(X0,X1,X2,X3))],[f96]) ).
fof(f98,plain,
! [X0] : start_point(sK17(X0),X0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(X1,sK17(X0))],[f24]) ).
fof(f101,plain,
! [X0,X1] :
( X0 = X1
| ? [X2,X3] :
( ( ~ ordered_by(X1,X2,X3)
| ~ ordered_by(X0,X2,X3) )
& ( ordered_by(X1,X2,X3)
| ordered_by(X0,X2,X3) ) ) ),
inference(nnf_transformation,[],[f56]) ).
fof(f102,plain,
! [X0,X1] :
( X0 = X1
| ( ( ~ ordered_by(X1,sK19(X0,X1),sK20(X0,X1))
| ~ ordered_by(X0,sK19(X0,X1),sK20(X0,X1)) )
& ( ordered_by(X1,sK19(X0,X1),sK20(X0,X1))
| ordered_by(X0,sK19(X0,X1),sK20(X0,X1)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19,sK20]),skolemize(X2,sK19(X0,X1)),skolemize(X3,sK20(X0,X1))],[f101]) ).
fof(f103,plain,
! [X0,X1] :
( ( X0 = underlying_curve(X1)
| ? [X2] :
( ( ~ incident_c(X2,X0)
| ~ incident_o(X2,X1) )
& ( incident_c(X2,X0)
| incident_o(X2,X1) ) ) )
& ( ! [X2] :
( ( incident_o(X2,X1)
| ~ incident_c(X2,X0) )
& ( incident_c(X2,X0)
| ~ incident_o(X2,X1) ) )
| underlying_curve(X1) != X0 ) ),
inference(nnf_transformation,[],[f27]) ).
fof(f104,plain,
! [X0,X1] :
( ( X0 = underlying_curve(X1)
| ? [X2] :
( ( ~ incident_c(X2,X0)
| ~ incident_o(X2,X1) )
& ( incident_c(X2,X0)
| incident_o(X2,X1) ) ) )
& ( ! [X3] :
( ( incident_o(X3,X1)
| ~ incident_c(X3,X0) )
& ( incident_c(X3,X0)
| ~ incident_o(X3,X1) ) )
| underlying_curve(X1) != X0 ) ),
inference(rectify,[],[f103]) ).
fof(f105,plain,
! [X0,X1] :
( ( X0 = underlying_curve(X1)
| ( ( ~ incident_c(sK21(X0,X1),X0)
| ~ incident_o(sK21(X0,X1),X1) )
& ( incident_c(sK21(X0,X1),X0)
| incident_o(sK21(X0,X1),X1) ) ) )
& ( ! [X3] :
( ( incident_o(X3,X1)
| ~ incident_c(X3,X0) )
& ( incident_c(X3,X0)
| ~ incident_o(X3,X1) ) )
| underlying_curve(X1) != X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(X2,sK21(X0,X1))],[f104]) ).
fof(f106,plain,
( sK22 != sK23
& underlying_curve(sK23) = underlying_curve(sK22)
& ordered_by(sK22,sK24,sK25)
& ordered_by(sK23,sK24,sK25) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22,sK23,sK24,sK25]),skolemize(X0,sK22),skolemize(X1,sK23),skolemize(X2,sK24),skolemize(X3,sK25)],[f58]) ).
fof(f124,plain,
! [X0,X1] :
( ~ inner_point(X0,X1)
| ~ end_point(X0,X1) ),
inference(cnf_transformation,[],[f71]) ).
fof(f149,plain,
! [X2,X3,X0,X1] :
( inner_point(X2,sK13(X0,X1,X2,X3))
| ~ between_c(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f90]) ).
fof(f150,plain,
! [X2,X3,X0,X1] :
( end_point(X3,sK13(X0,X1,X2,X3))
| ~ between_c(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f90]) ).
fof(f151,plain,
! [X2,X3,X0,X1] :
( end_point(X1,sK13(X0,X1,X2,X3))
| ~ between_c(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f90]) ).
fof(f152,plain,
! [X2,X3,X0,X1] :
( part_of(sK13(X0,X1,X2,X3),X0)
| ~ between_c(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f90]) ).
fof(f153,plain,
! [X2,X3,X0,X1] :
( X1 != X3
| ~ between_c(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f90]) ).
fof(f154,plain,
! [X2,X3,X0,X1,X4] :
( ~ inner_point(X2,X4)
| X1 = X3
| ~ part_of(X4,X0)
| ~ end_point(X1,X4)
| ~ end_point(X3,X4)
| between_c(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f90]) ).
fof(f155,plain,
! [X2,X3,X0,X1] :
( ~ between_o(X0,X1,X2,X3)
| ordered_by(X0,X2,X1)
| ordered_by(X0,X2,X3) ),
inference(cnf_transformation,[],[f92]) ).
fof(f156,plain,
! [X2,X3,X0,X1] :
( ~ between_o(X0,X1,X2,X3)
| ordered_by(X0,X3,X2)
| ordered_by(X0,X2,X3) ),
inference(cnf_transformation,[],[f92]) ).
fof(f158,plain,
! [X2,X3,X0,X1] :
( ~ between_o(X0,X1,X2,X3)
| ordered_by(X0,X3,X2)
| ordered_by(X0,X1,X2) ),
inference(cnf_transformation,[],[f92]) ).
fof(f159,plain,
! [X2,X3,X0,X1] :
( between_o(X0,X1,X2,X3)
| ~ ordered_by(X0,X3,X2)
| ~ ordered_by(X0,X2,X1) ),
inference(cnf_transformation,[],[f92]) ).
fof(f160,plain,
! [X2,X3,X0,X1] :
( between_o(X0,X1,X2,X3)
| ~ ordered_by(X0,X1,X2)
| ~ ordered_by(X0,X2,X3) ),
inference(cnf_transformation,[],[f92]) ).
fof(f161,plain,
! [X2,X0,X1] :
( ordered_by(X1,X0,X2)
| X0 = X2
| ~ incident_o(X2,X1)
| ~ start_point(X0,X1) ),
inference(cnf_transformation,[],[f52]) ).
fof(f163,plain,
! [X2,X0,X1] :
( ~ ordered_by(X0,X1,X2)
| incident_o(X2,X0) ),
inference(cnf_transformation,[],[f53]) ).
fof(f164,plain,
! [X2,X0,X1] :
( ~ ordered_by(X0,X1,X2)
| incident_o(X1,X0) ),
inference(cnf_transformation,[],[f53]) ).
fof(f168,plain,
! [X2,X3,X0,X1] :
( between_c(sK16(X0,X1,X2,X3),X0,X1,X2)
| ~ between_o(X3,X0,X1,X2) ),
inference(cnf_transformation,[],[f97]) ).
fof(f169,plain,
! [X2,X3,X0,X1,X7] :
( incident_c(X7,sK16(X0,X1,X2,X3))
| ~ incident_o(X7,X3)
| ~ between_o(X3,X0,X1,X2) ),
inference(cnf_transformation,[],[f97]) ).
fof(f170,plain,
! [X2,X3,X0,X1,X7] :
( ~ incident_c(X7,sK16(X0,X1,X2,X3))
| incident_o(X7,X3)
| ~ between_o(X3,X0,X1,X2) ),
inference(cnf_transformation,[],[f97]) ).
fof(f171,plain,
! [X2,X3,X0,X1,X4] :
( ~ between_c(X4,X0,X1,X2)
| incident_c(sK15(X3,X4),X4)
| incident_o(sK15(X3,X4),X3)
| between_o(X3,X0,X1,X2) ),
inference(cnf_transformation,[],[f97]) ).
fof(f172,plain,
! [X2,X3,X0,X1,X4] :
( ~ incident_o(sK15(X3,X4),X3)
| ~ incident_c(sK15(X3,X4),X4)
| between_o(X3,X0,X1,X2)
| ~ between_c(X4,X0,X1,X2) ),
inference(cnf_transformation,[],[f97]) ).
fof(f173,plain,
! [X0] : start_point(sK17(X0),X0),
inference(cnf_transformation,[],[f98]) ).
fof(f177,plain,
! [X0,X1] :
( ordered_by(X1,sK19(X0,X1),sK20(X0,X1))
| ordered_by(X0,sK19(X0,X1),sK20(X0,X1))
| X0 = X1 ),
inference(cnf_transformation,[],[f102]) ).
fof(f178,plain,
! [X0,X1] :
( ~ ordered_by(X1,sK19(X0,X1),sK20(X0,X1))
| X0 = X1
| ~ ordered_by(X0,sK19(X0,X1),sK20(X0,X1)) ),
inference(cnf_transformation,[],[f102]) ).
fof(f179,plain,
! [X3,X0,X1] :
( incident_c(X3,X0)
| ~ incident_o(X3,X1)
| underlying_curve(X1) != X0 ),
inference(cnf_transformation,[],[f105]) ).
fof(f180,plain,
! [X3,X0,X1] :
( incident_o(X3,X1)
| ~ incident_c(X3,X0)
| underlying_curve(X1) != X0 ),
inference(cnf_transformation,[],[f105]) ).
fof(f183,plain,
ordered_by(sK23,sK24,sK25),
inference(cnf_transformation,[],[f106]) ).
fof(f184,plain,
ordered_by(sK22,sK24,sK25),
inference(cnf_transformation,[],[f106]) ).
fof(f185,plain,
underlying_curve(sK23) = underlying_curve(sK22),
inference(cnf_transformation,[],[f106]) ).
fof(f186,plain,
sK22 != sK23,
inference(cnf_transformation,[],[f106]) ).
fof(f191,plain,
! [X2,X3,X0] : ~ between_c(X0,X3,X2,X3),
inference(equality_resolution,[],[f153]) ).
fof(f192,plain,
! [X3,X1] :
( ~ incident_c(X3,underlying_curve(X1))
| incident_o(X3,X1) ),
inference(equality_resolution,[],[f180]) ).
fof(f193,plain,
! [X3,X1] :
( incident_c(X3,underlying_curve(X1))
| ~ incident_o(X3,X1) ),
inference(equality_resolution,[],[f179]) ).
fof(f194,definition,
sF26 = underlying_curve(sK23),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f195,plain,
underlying_curve(sK23) = sF26,
inference(reorient_equations,[],[f194]) ).
fof(f196,definition,
sF27 = underlying_curve(sK22),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f197,plain,
underlying_curve(sK22) = sF27,
inference(reorient_equations,[],[f196]) ).
fof(f198,plain,
sF26 = sF27,
inference(definition_folding,[],[f185,f197,f195]) ).
fof(f199,plain,
underlying_curve(sK22) = sF26,
inference(forward_demodulation,[],[f197,f198]) ).
fof(f200,plain,
! [X0] :
( ~ incident_c(X0,sF26)
| incident_o(X0,sK22) ),
inference(superposition,[],[f192,f199]) ).
fof(f201,plain,
! [X0] :
( ~ incident_c(X0,sF26)
| incident_o(X0,sK23) ),
inference(superposition,[],[f192,f195]) ).
fof(f202,plain,
! [X2,X0,X1] : ~ between_o(X0,X1,X2,X1),
inference(resolution,[],[f191,f168]) ).
fof(f204,plain,
! [X2,X0,X1] :
( ~ ordered_by(X0,X2,X1)
| ~ ordered_by(X0,X1,X2) ),
inference(resolution,[],[f202,f159]) ).
fof(f205,plain,
~ ordered_by(sK22,sK25,sK24),
inference(resolution,[],[f204,f184]) ).
fof(f206,plain,
~ ordered_by(sK23,sK25,sK24),
inference(resolution,[],[f204,f183]) ).
fof(f208,plain,
! [X0] :
( ~ incident_o(X0,sK22)
| incident_c(X0,sF26) ),
inference(superposition,[],[f193,f199]) ).
fof(f209,plain,
! [X0] :
( ~ incident_o(X0,sK23)
| incident_c(X0,sF26) ),
inference(superposition,[],[f193,f195]) ).
fof(f210,plain,
incident_o(sK24,sK22),
inference(resolution,[],[f164,f184]) ).
fof(f211,plain,
incident_o(sK24,sK23),
inference(resolution,[],[f164,f183]) ).
fof(f253,plain,
! [X2,X3,X0,X1] :
( ~ end_point(X2,sK13(X0,X1,X2,X3))
| ~ between_c(X0,X1,X2,X3) ),
inference(resolution,[],[f149,f124]) ).
fof(f254,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ end_point(X5,sK13(X0,X1,X2,X3))
| X4 = X5
| ~ part_of(sK13(X0,X1,X2,X3),X6)
| ~ end_point(X4,sK13(X0,X1,X2,X3))
| ~ between_c(X0,X1,X2,X3)
| between_c(X6,X4,X2,X5) ),
inference(resolution,[],[f149,f154]) ).
fof(f257,plain,
! [X2,X3,X0,X1,X4,X5] :
( X0 = X1
| ~ part_of(sK13(X2,X1,X3,X4),X5)
| ~ end_point(X0,sK13(X2,X1,X3,X4))
| ~ between_c(X2,X1,X3,X4)
| between_c(X5,X0,X3,X1)
| ~ between_c(X2,X1,X3,X4) ),
inference(resolution,[],[f254,f151]) ).
fof(f258,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ end_point(X0,sK13(X2,X1,X3,X4))
| ~ part_of(sK13(X2,X1,X3,X4),X5)
| X0 = X1
| ~ between_c(X2,X1,X3,X4)
| between_c(X5,X0,X3,X1) ),
inference(duplicate_literal_removal,[],[f257]) ).
fof(f260,plain,
! [X2,X3,X0,X1,X4] :
( ~ part_of(sK13(X0,X1,X2,X3),X4)
| X1 = X3
| ~ between_c(X0,X1,X2,X3)
| between_c(X4,X3,X2,X1)
| ~ between_c(X0,X1,X2,X3) ),
inference(resolution,[],[f258,f150]) ).
fof(f263,plain,
! [X2,X3,X0,X1,X4] :
( ~ part_of(sK13(X0,X1,X2,X3),X4)
| X1 = X3
| ~ between_c(X0,X1,X2,X3)
| between_c(X4,X3,X2,X1) ),
inference(duplicate_literal_removal,[],[f260]) ).
fof(f264,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| ~ between_c(X2,X0,X3,X1)
| between_c(X2,X1,X3,X0)
| ~ between_c(X2,X0,X3,X1) ),
inference(resolution,[],[f263,f152]) ).
fof(f265,plain,
! [X2,X3,X0,X1] :
( ~ between_c(X2,X0,X3,X1)
| X0 = X1
| between_c(X2,X1,X3,X0) ),
inference(duplicate_literal_removal,[],[f264]) ).
fof(f266,plain,
! [X2,X3,X0,X1] :
( between_c(sK16(X0,X2,X1,X3),X1,X2,X0)
| X0 = X1
| ~ between_o(X3,X0,X2,X1) ),
inference(resolution,[],[f265,f168]) ).
fof(f292,plain,
! [X2,X3,X0,X1,X4] :
( incident_c(sK15(X0,sK16(X1,X2,X3,X4)),sK16(X1,X2,X3,X4))
| incident_o(sK15(X0,sK16(X1,X2,X3,X4)),X0)
| between_o(X0,X3,X2,X1)
| X1 = X3
| ~ between_o(X4,X1,X2,X3) ),
inference(resolution,[],[f171,f266]) ).
fof(f296,plain,
! [X2,X0,X1] :
( X0 = X1
| ~ incident_o(X1,X2)
| ~ start_point(X0,X2)
| ~ ordered_by(X2,X1,X0) ),
inference(resolution,[],[f161,f204]) ).
fof(f297,plain,
( sK24 = sK25
| ~ incident_o(sK24,sK22)
| ~ start_point(sK25,sK22) ),
inference(resolution,[],[f161,f205]) ).
fof(f298,plain,
( sK24 = sK25
| ~ incident_o(sK24,sK23)
| ~ start_point(sK25,sK23) ),
inference(resolution,[],[f161,f206]) ).
fof(f299,plain,
( sK24 = sK25
| ~ start_point(sK25,sK23) ),
inference(forward_subsumption_resolution,[],[f298,f211]) ).
fof(f300,plain,
( sK24 = sK25
| ~ start_point(sK25,sK22) ),
inference(forward_subsumption_resolution,[],[f297,f210]) ).
fof(f301,plain,
! [X2,X0,X1] :
( ~ ordered_by(X2,X1,X0)
| ~ start_point(X0,X2)
| X0 = X1 ),
inference(forward_subsumption_resolution,[],[f296,f164]) ).
fof(f303,definition,
( spl28_1
<=> start_point(sK25,sK23) ),
introduced(definition,[new_symbols(definition,[spl28_1])],[avatar_definition]) ).
fof(f305,plain,
( ~ start_point(sK25,sK23)
| spl28_1 ),
inference(avatar_component_clause,[],[f303]) ).
fof(f307,definition,
( spl28_2
<=> sK24 = sK25 ),
introduced(definition,[new_symbols(definition,[spl28_2])],[avatar_definition]) ).
fof(f309,plain,
( sK24 = sK25
| ~ spl28_2 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f310,plain,
( ~ spl28_1
| spl28_2 ),
inference(avatar_split_clause,[],[f299,f307,f303]) ).
fof(f312,definition,
( spl28_3
<=> start_point(sK25,sK22) ),
introduced(definition,[new_symbols(definition,[spl28_3])],[avatar_definition]) ).
fof(f314,plain,
( ~ start_point(sK25,sK22)
| spl28_3 ),
inference(avatar_component_clause,[],[f312]) ).
fof(f315,plain,
( ~ spl28_3
| spl28_2 ),
inference(avatar_split_clause,[],[f300,f307,f312]) ).
fof(f437,plain,
! [X0,X1] :
( ordered_by(X1,sK19(X1,X0),sK20(X1,X0))
| X0 = X1
| incident_o(sK19(X1,X0),X0) ),
inference(resolution,[],[f177,f164]) ).
fof(f442,plain,
! [X0,X1] :
( ~ ordered_by(X0,sK20(X0,X1),sK19(X0,X1))
| X0 = X1
| ordered_by(X1,sK19(X0,X1),sK20(X0,X1)) ),
inference(resolution,[],[f177,f204]) ).
fof(f475,plain,
! [X2,X0,X1] :
( ~ between_c(X0,X1,X1,X2)
| ~ between_c(X0,X1,X1,X2) ),
inference(resolution,[],[f253,f151]) ).
fof(f476,plain,
! [X2,X0,X1] : ~ between_c(X0,X1,X1,X2),
inference(duplicate_literal_removal,[],[f475]) ).
fof(f478,plain,
! [X2,X0,X1] : ~ between_o(X0,X1,X1,X2),
inference(resolution,[],[f476,f168]) ).
fof(f486,plain,
! [X2,X0,X1] :
( ~ ordered_by(X0,X1,X2)
| ~ ordered_by(X0,X1,X1) ),
inference(resolution,[],[f478,f160]) ).
fof(f960,plain,
! [X2,X3,X0,X1,X4] :
( incident_o(sK15(X0,sK16(X1,X2,X3,X4)),X4)
| ~ between_o(X4,X1,X2,X3)
| incident_o(sK15(X0,sK16(X1,X2,X3,X4)),X0)
| between_o(X0,X3,X2,X1)
| X1 = X3
| ~ between_o(X4,X1,X2,X3) ),
inference(resolution,[],[f170,f292]) ).
fof(f965,plain,
! [X2,X3,X0,X1,X4] :
( incident_o(sK15(X0,sK16(X1,X2,X3,X4)),X4)
| incident_o(sK15(X0,sK16(X1,X2,X3,X4)),X0)
| ~ between_o(X4,X1,X2,X3)
| between_o(X0,X3,X2,X1)
| X1 = X3 ),
inference(duplicate_literal_removal,[],[f960]) ).
fof(f978,plain,
! [X2,X3,X0,X1] :
( incident_o(sK15(X0,sK16(X1,X2,X3,sK22)),X0)
| ~ between_o(sK22,X1,X2,X3)
| between_o(X0,X3,X2,X1)
| X1 = X3
| incident_c(sK15(X0,sK16(X1,X2,X3,sK22)),sF26) ),
inference(resolution,[],[f965,f208]) ).
fof(f979,plain,
! [X2,X3,X0,X1] :
( incident_o(sK15(X0,sK16(X1,X2,X3,sK23)),X0)
| ~ between_o(sK23,X1,X2,X3)
| between_o(X0,X3,X2,X1)
| X1 = X3
| incident_c(sK15(X0,sK16(X1,X2,X3,sK23)),sF26) ),
inference(resolution,[],[f965,f209]) ).
fof(f1012,plain,
! [X2,X0,X1] :
( ~ between_o(sK22,X0,X1,X2)
| between_o(sK23,X2,X1,X0)
| X0 = X2
| incident_c(sK15(sK23,sK16(X0,X1,X2,sK22)),sF26)
| incident_c(sK15(sK23,sK16(X0,X1,X2,sK22)),sF26) ),
inference(resolution,[],[f978,f209]) ).
fof(f1014,plain,
! [X2,X0,X1] :
( incident_c(sK15(sK23,sK16(X0,X1,X2,sK22)),sF26)
| between_o(sK23,X2,X1,X0)
| X0 = X2
| ~ between_o(sK22,X0,X1,X2) ),
inference(duplicate_literal_removal,[],[f1012]) ).
fof(f1016,plain,
! [X2,X0,X1] :
( incident_o(sK15(sK23,sK16(X2,X1,X0,sK22)),sK23)
| X0 = X2
| ~ between_o(sK22,X2,X1,X0)
| between_o(sK23,X0,X1,X2) ),
inference(resolution,[],[f1014,f201]) ).
fof(f1017,plain,
! [X2,X0,X1] :
( incident_o(sK15(sK23,sK16(X2,X1,X0,sK22)),sK22)
| X0 = X2
| ~ between_o(sK22,X2,X1,X0)
| between_o(sK23,X0,X1,X2) ),
inference(resolution,[],[f1014,f200]) ).
fof(f1022,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ incident_c(sK15(sK23,sK16(X1,X2,X0,sK22)),sK16(X1,X2,X0,sK22))
| ~ between_o(sK22,X1,X2,X0)
| between_o(sK23,X0,X2,X1)
| X0 = X1
| between_o(sK23,X3,X4,X5)
| ~ between_c(sK16(X1,X2,X0,sK22),X3,X4,X5) ),
inference(resolution,[],[f1016,f172]) ).
fof(f1028,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ between_o(sK22,X0,X1,X2)
| between_o(sK23,X2,X1,X0)
| X0 = X2
| between_o(sK23,X3,X4,X5)
| ~ between_c(sK16(X0,X1,X2,sK22),X3,X4,X5)
| ~ incident_o(sK15(sK23,sK16(X0,X1,X2,sK22)),sK22)
| ~ between_o(sK22,X0,X1,X2) ),
inference(resolution,[],[f1022,f169]) ).
fof(f1029,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ between_o(sK22,X0,X1,X2)
| between_o(sK23,X2,X1,X0)
| X0 = X2
| between_o(sK23,X3,X4,X5)
| ~ between_c(sK16(X0,X1,X2,sK22),X3,X4,X5)
| ~ incident_o(sK15(sK23,sK16(X0,X1,X2,sK22)),sK22) ),
inference(duplicate_literal_removal,[],[f1028]) ).
fof(f1034,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ between_c(sK16(X0,X1,X2,sK22),X3,X4,X5)
| between_o(sK23,X2,X1,X0)
| X0 = X2
| between_o(sK23,X3,X4,X5)
| ~ between_o(sK22,X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f1029,f1017]) ).
fof(f1036,plain,
! [X2,X0,X1] :
( between_o(sK23,X0,X1,X2)
| X0 = X2
| between_o(sK23,X0,X1,X2)
| ~ between_o(sK22,X2,X1,X0)
| X0 = X2
| ~ between_o(sK22,X2,X1,X0) ),
inference(resolution,[],[f1034,f266]) ).
fof(f1038,plain,
! [X2,X0,X1] :
( ~ between_o(sK22,X2,X1,X0)
| X0 = X2
| between_o(sK23,X0,X1,X2) ),
inference(duplicate_literal_removal,[],[f1036]) ).
fof(f1041,plain,
! [X2,X0,X1] :
( between_o(sK23,X0,X2,X1)
| X0 = X1
| ~ ordered_by(sK22,X0,X2)
| ~ ordered_by(sK22,X2,X1) ),
inference(resolution,[],[f1038,f159]) ).
fof(f1044,plain,
! [X2,X0,X1] :
( ~ ordered_by(sK22,X2,X1)
| ~ ordered_by(sK22,X0,X2)
| X0 = X1
| ordered_by(sK23,X1,X2)
| ordered_by(sK23,X2,X1) ),
inference(resolution,[],[f1041,f156]) ).
fof(f1045,plain,
! [X2,X0,X1] :
( ~ ordered_by(sK22,X2,X1)
| ~ ordered_by(sK22,X0,X2)
| X0 = X1
| ordered_by(sK23,X2,X0)
| ordered_by(sK23,X2,X1) ),
inference(resolution,[],[f1041,f155]) ).
fof(f1046,plain,
! [X2,X0,X1] :
( ~ ordered_by(sK22,X2,X1)
| ~ ordered_by(sK22,X0,X2)
| X0 = X1
| ordered_by(sK23,X1,X2)
| ordered_by(sK23,X0,X2) ),
inference(resolution,[],[f1041,f158]) ).
fof(f1063,plain,
! [X0] :
( ~ ordered_by(sK22,X0,sK24)
| sK25 = X0
| ordered_by(sK23,sK25,sK24)
| ordered_by(sK23,X0,sK24) ),
inference(resolution,[],[f1046,f184]) ).
fof(f1064,plain,
! [X0] :
( ~ ordered_by(sK22,X0,sK24)
| sK25 = X0
| ordered_by(sK23,X0,sK24) ),
inference(forward_subsumption_resolution,[],[f1063,f206]) ).
fof(f1065,plain,
! [X0] :
( sK25 = X0
| ordered_by(sK23,X0,sK24)
| sK24 = X0
| ~ incident_o(sK24,sK22)
| ~ start_point(X0,sK22) ),
inference(resolution,[],[f1064,f161]) ).
fof(f1066,plain,
! [X0] :
( ordered_by(sK23,X0,sK24)
| sK25 = X0
| sK24 = X0
| ~ start_point(X0,sK22) ),
inference(forward_subsumption_resolution,[],[f1065,f210]) ).
fof(f1068,plain,
! [X0,X1] :
( ~ ordered_by(sK22,X0,sK19(X1,sK22))
| sK20(X1,sK22) = X0
| ordered_by(sK23,sK19(X1,sK22),X0)
| ordered_by(sK23,sK19(X1,sK22),sK20(X1,sK22))
| ordered_by(X1,sK19(X1,sK22),sK20(X1,sK22))
| sK22 = X1 ),
inference(resolution,[],[f1045,f177]) ).
fof(f1074,plain,
! [X0] :
( sK25 = X0
| sK24 = X0
| ~ start_point(X0,sK22)
| ~ start_point(sK24,sK23)
| sK24 = X0 ),
inference(resolution,[],[f1066,f301]) ).
fof(f1082,plain,
! [X0] :
( sK25 = X0
| sK24 = X0
| ~ start_point(X0,sK22)
| ~ start_point(sK24,sK23) ),
inference(duplicate_literal_removal,[],[f1074]) ).
fof(f1084,definition,
( spl28_22
<=> start_point(sK24,sK23) ),
introduced(definition,[new_symbols(definition,[spl28_22])],[avatar_definition]) ).
fof(f1085,plain,
( start_point(sK24,sK23)
| ~ spl28_22 ),
inference(avatar_component_clause,[],[f1084]) ).
fof(f1086,plain,
( ~ start_point(sK24,sK23)
| spl28_22 ),
inference(avatar_component_clause,[],[f1084]) ).
fof(f1088,definition,
( spl28_23
<=> ! [X0] :
( sK25 = X0
| ~ start_point(X0,sK22)
| sK24 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl28_23])],[avatar_definition]) ).
fof(f1089,plain,
( ! [X0] :
( ~ start_point(X0,sK22)
| sK25 = X0
| sK24 = X0 )
| ~ spl28_23 ),
inference(avatar_component_clause,[],[f1088]) ).
fof(f1090,plain,
( ~ spl28_22
| spl28_23 ),
inference(avatar_split_clause,[],[f1082,f1088,f1084]) ).
fof(f1107,plain,
! [X0,X1] :
( sK20(X0,sK22) = X1
| ordered_by(sK23,sK19(X0,sK22),X1)
| ordered_by(sK23,sK19(X0,sK22),sK20(X0,sK22))
| ordered_by(X0,sK19(X0,sK22),sK20(X0,sK22))
| sK22 = X0
| sK19(X0,sK22) = X1
| ~ incident_o(sK19(X0,sK22),sK22)
| ~ start_point(X1,sK22) ),
inference(resolution,[],[f1068,f161]) ).
fof(f1108,plain,
! [X0,X1] :
( ordered_by(sK23,sK19(X0,sK22),sK20(X0,sK22))
| ordered_by(X0,sK19(X0,sK22),sK20(X0,sK22))
| ordered_by(sK23,sK19(X0,sK22),X1)
| sK20(X0,sK22) = X1
| sK22 = X0
| sK19(X0,sK22) = X1
| ~ start_point(X1,sK22) ),
inference(forward_subsumption_resolution,[],[f1107,f437]) ).
fof(f1148,plain,
! [X0] :
( ordered_by(sK23,sK19(sK23,sK22),sK20(sK23,sK22))
| ordered_by(sK23,sK19(sK23,sK22),X0)
| sK20(sK23,sK22) = X0
| sK22 = sK23
| sK19(sK23,sK22) = X0
| ~ start_point(X0,sK22) ),
inference(factoring,[],[f1108]) ).
fof(f1153,plain,
! [X0] :
( ordered_by(sK23,sK19(sK23,sK22),sK20(sK23,sK22))
| ordered_by(sK23,sK19(sK23,sK22),X0)
| sK20(sK23,sK22) = X0
| sK19(sK23,sK22) = X0
| ~ start_point(X0,sK22) ),
inference(forward_subsumption_resolution,[],[f1148,f186]) ).
fof(f1157,definition,
( spl28_24
<=> ! [X0] :
( ordered_by(sK23,sK19(sK23,sK22),X0)
| ~ start_point(X0,sK22)
| sK19(sK23,sK22) = X0
| sK20(sK23,sK22) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl28_24])],[avatar_definition]) ).
fof(f1158,plain,
( ! [X0] :
( ordered_by(sK23,sK19(sK23,sK22),X0)
| ~ start_point(X0,sK22)
| sK19(sK23,sK22) = X0
| sK20(sK23,sK22) = X0 )
| ~ spl28_24 ),
inference(avatar_component_clause,[],[f1157]) ).
fof(f1160,definition,
( spl28_25
<=> ordered_by(sK23,sK19(sK23,sK22),sK20(sK23,sK22)) ),
introduced(definition,[new_symbols(definition,[spl28_25])],[avatar_definition]) ).
fof(f1161,plain,
( ~ ordered_by(sK23,sK19(sK23,sK22),sK20(sK23,sK22))
| spl28_25 ),
inference(avatar_component_clause,[],[f1160]) ).
fof(f1162,plain,
( ordered_by(sK23,sK19(sK23,sK22),sK20(sK23,sK22))
| ~ spl28_25 ),
inference(avatar_component_clause,[],[f1160]) ).
fof(f1163,plain,
( spl28_24
| spl28_25 ),
inference(avatar_split_clause,[],[f1153,f1160,f1157]) ).
fof(f1165,plain,
( ! [X0] :
( ~ start_point(X0,sK22)
| sK19(sK23,sK22) = X0
| sK20(sK23,sK22) = X0
| ~ start_point(X0,sK23)
| sK19(sK23,sK22) = X0 )
| ~ spl28_24 ),
inference(resolution,[],[f1158,f301]) ).
fof(f1173,plain,
( ! [X0] :
( ~ start_point(X0,sK23)
| sK19(sK23,sK22) = X0
| sK20(sK23,sK22) = X0
| ~ start_point(X0,sK22) )
| ~ spl28_24 ),
inference(duplicate_literal_removal,[],[f1165]) ).
fof(f1175,definition,
( spl28_26
<=> incident_o(sK19(sK23,sK22),sK23) ),
introduced(definition,[new_symbols(definition,[spl28_26])],[avatar_definition]) ).
fof(f1177,plain,
( incident_o(sK19(sK23,sK22),sK23)
| ~ spl28_26 ),
inference(avatar_component_clause,[],[f1175]) ).
fof(f1179,definition,
( spl28_27
<=> ! [X0] :
( ~ start_point(X0,sK22)
| sK20(sK23,sK22) = X0
| sK19(sK23,sK22) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl28_27])],[avatar_definition]) ).
fof(f1180,plain,
( ! [X0] :
( ~ start_point(X0,sK22)
| sK20(sK23,sK22) = X0
| sK19(sK23,sK22) = X0 )
| ~ spl28_27 ),
inference(avatar_component_clause,[],[f1179]) ).
fof(f1183,definition,
( spl28_28
<=> ordered_by(sK23,sK19(sK23,sK22),sK19(sK23,sK22)) ),
introduced(definition,[new_symbols(definition,[spl28_28])],[avatar_definition]) ).
fof(f1185,plain,
( ~ ordered_by(sK23,sK19(sK23,sK22),sK19(sK23,sK22))
| spl28_28 ),
inference(avatar_component_clause,[],[f1183]) ).
fof(f1187,plain,
( ~ ordered_by(sK23,sK19(sK23,sK22),sK19(sK23,sK22))
| ~ spl28_25 ),
inference(resolution,[],[f1162,f486]) ).
fof(f1190,plain,
( incident_o(sK19(sK23,sK22),sK23)
| ~ spl28_25 ),
inference(resolution,[],[f1162,f164]) ).
fof(f1191,plain,
( ~ ordered_by(sK23,sK20(sK23,sK22),sK19(sK23,sK22))
| ~ spl28_25 ),
inference(resolution,[],[f1162,f204]) ).
fof(f1192,plain,
( spl28_26
| ~ spl28_25 ),
inference(avatar_split_clause,[],[f1190,f1160,f1175]) ).
fof(f1194,definition,
( spl28_29
<=> sK20(sK23,sK22) = sK19(sK23,sK22) ),
introduced(definition,[new_symbols(definition,[spl28_29])],[avatar_definition]) ).
fof(f1196,plain,
( sK20(sK23,sK22) = sK19(sK23,sK22)
| ~ spl28_29 ),
inference(avatar_component_clause,[],[f1194]) ).
fof(f1198,definition,
( spl28_30
<=> start_point(sK20(sK23,sK22),sK23) ),
introduced(definition,[new_symbols(definition,[spl28_30])],[avatar_definition]) ).
fof(f1199,plain,
( start_point(sK20(sK23,sK22),sK23)
| ~ spl28_30 ),
inference(avatar_component_clause,[],[f1198]) ).
fof(f1200,plain,
( ~ start_point(sK20(sK23,sK22),sK23)
| spl28_30 ),
inference(avatar_component_clause,[],[f1198]) ).
fof(f1202,plain,
( ~ spl28_28
| ~ spl28_25 ),
inference(avatar_split_clause,[],[f1187,f1160,f1183]) ).
fof(f1204,plain,
( ordered_by(sK22,sK19(sK23,sK22),sK20(sK23,sK22))
| sK22 = sK23
| spl28_25 ),
inference(resolution,[],[f1161,f177]) ).
fof(f1205,plain,
( sK20(sK23,sK22) = sK19(sK23,sK22)
| ~ incident_o(sK20(sK23,sK22),sK23)
| ~ start_point(sK19(sK23,sK22),sK23)
| spl28_25 ),
inference(resolution,[],[f1161,f161]) ).
fof(f1207,definition,
( spl28_31
<=> start_point(sK19(sK23,sK22),sK23) ),
introduced(definition,[new_symbols(definition,[spl28_31])],[avatar_definition]) ).
fof(f1209,plain,
( ~ start_point(sK19(sK23,sK22),sK23)
| spl28_31 ),
inference(avatar_component_clause,[],[f1207]) ).
fof(f1211,definition,
( spl28_32
<=> incident_o(sK20(sK23,sK22),sK23) ),
introduced(definition,[new_symbols(definition,[spl28_32])],[avatar_definition]) ).
fof(f1212,plain,
( incident_o(sK20(sK23,sK22),sK23)
| ~ spl28_32 ),
inference(avatar_component_clause,[],[f1211]) ).
fof(f1213,plain,
( ~ incident_o(sK20(sK23,sK22),sK23)
| spl28_32 ),
inference(avatar_component_clause,[],[f1211]) ).
fof(f1214,plain,
( ~ spl28_31
| ~ spl28_32
| spl28_29
| spl28_25 ),
inference(avatar_split_clause,[],[f1205,f1160,f1194,f1211,f1207]) ).
fof(f1215,plain,
( ordered_by(sK22,sK19(sK23,sK22),sK20(sK23,sK22))
| spl28_25 ),
inference(forward_subsumption_resolution,[],[f1204,f186]) ).
fof(f1216,plain,
( ! [X0] :
( ~ ordered_by(sK22,X0,sK19(sK23,sK22))
| sK20(sK23,sK22) = X0
| ordered_by(sK23,sK20(sK23,sK22),sK19(sK23,sK22))
| ordered_by(sK23,sK19(sK23,sK22),sK20(sK23,sK22)) )
| spl28_25 ),
inference(resolution,[],[f1215,f1044]) ).
fof(f1221,plain,
( ~ ordered_by(sK22,sK19(sK23,sK22),sK19(sK23,sK22))
| spl28_25 ),
inference(resolution,[],[f1215,f486]) ).
fof(f1223,plain,
( incident_o(sK20(sK23,sK22),sK22)
| spl28_25 ),
inference(resolution,[],[f1215,f163]) ).
fof(f1224,plain,
( incident_o(sK19(sK23,sK22),sK22)
| spl28_25 ),
inference(resolution,[],[f1215,f164]) ).
fof(f1225,plain,
( ~ ordered_by(sK22,sK20(sK23,sK22),sK19(sK23,sK22))
| spl28_25 ),
inference(resolution,[],[f1215,f204]) ).
fof(f1232,definition,
( spl28_34
<=> ordered_by(sK23,sK20(sK23,sK22),sK19(sK23,sK22)) ),
introduced(definition,[new_symbols(definition,[spl28_34])],[avatar_definition]) ).
fof(f1233,plain,
( ~ ordered_by(sK23,sK20(sK23,sK22),sK19(sK23,sK22))
| spl28_34 ),
inference(avatar_component_clause,[],[f1232]) ).
fof(f1234,plain,
( ordered_by(sK23,sK20(sK23,sK22),sK19(sK23,sK22))
| ~ spl28_34 ),
inference(avatar_component_clause,[],[f1232]) ).
fof(f1240,plain,
( ! [X0] :
( ~ ordered_by(sK22,X0,sK19(sK23,sK22))
| sK20(sK23,sK22) = X0
| ordered_by(sK23,sK20(sK23,sK22),sK19(sK23,sK22)) )
| spl28_25 ),
inference(forward_subsumption_resolution,[],[f1216,f1161]) ).
fof(f1242,definition,
( spl28_36
<=> ! [X0] :
( ~ ordered_by(sK22,X0,sK19(sK23,sK22))
| sK20(sK23,sK22) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl28_36])],[avatar_definition]) ).
fof(f1243,plain,
( ! [X0] :
( ~ ordered_by(sK22,X0,sK19(sK23,sK22))
| sK20(sK23,sK22) = X0 )
| ~ spl28_36 ),
inference(avatar_component_clause,[],[f1242]) ).
fof(f1244,plain,
( spl28_34
| spl28_36
| spl28_25 ),
inference(avatar_split_clause,[],[f1240,f1160,f1242,f1232]) ).
fof(f1253,plain,
( ! [X0] :
( sK20(sK23,sK22) = X0
| sK19(sK23,sK22) = X0
| ~ incident_o(sK19(sK23,sK22),sK22)
| ~ start_point(X0,sK22) )
| ~ spl28_36 ),
inference(resolution,[],[f1243,f161]) ).
fof(f1254,plain,
( ! [X0] :
( sK20(sK23,sK22) = X0
| sK19(sK23,sK22) = X0
| ~ start_point(X0,sK22) )
| spl28_25
| ~ spl28_36 ),
inference(forward_subsumption_resolution,[],[f1253,f1224]) ).
fof(f1255,plain,
( spl28_27
| spl28_25
| ~ spl28_36 ),
inference(avatar_split_clause,[],[f1254,f1242,f1160,f1179]) ).
fof(f1289,plain,
( incident_c(sK20(sK23,sK22),sF26)
| spl28_25 ),
inference(resolution,[],[f1223,f208]) ).
fof(f1290,plain,
( incident_o(sK20(sK23,sK22),sK23)
| spl28_25 ),
inference(resolution,[],[f1289,f201]) ).
fof(f1303,plain,
( incident_c(sK20(sK23,sK22),sF26)
| ~ spl28_32 ),
inference(resolution,[],[f1212,f209]) ).
fof(f1336,definition,
( spl28_42
<=> sK17(sK23) = sK20(sK23,sK22) ),
introduced(definition,[new_symbols(definition,[spl28_42])],[avatar_definition]) ).
fof(f1337,plain,
( sK17(sK23) != sK20(sK23,sK22)
| spl28_42 ),
inference(avatar_component_clause,[],[f1336]) ).
fof(f1338,plain,
( sK17(sK23) = sK20(sK23,sK22)
| ~ spl28_42 ),
inference(avatar_component_clause,[],[f1336]) ).
fof(f1340,definition,
( spl28_43
<=> sK17(sK23) = sK19(sK23,sK22) ),
introduced(definition,[new_symbols(definition,[spl28_43])],[avatar_definition]) ).
fof(f1341,plain,
( sK17(sK23) != sK19(sK23,sK22)
| spl28_43 ),
inference(avatar_component_clause,[],[f1340]) ).
fof(f1342,plain,
( sK17(sK23) = sK19(sK23,sK22)
| ~ spl28_43 ),
inference(avatar_component_clause,[],[f1340]) ).
fof(f1448,plain,
! [X2,X0,X1] :
( ~ between_o(sK23,X0,X1,X2)
| between_o(sK22,X2,X1,X0)
| X0 = X2
| incident_c(sK15(sK22,sK16(X0,X1,X2,sK23)),sF26)
| incident_c(sK15(sK22,sK16(X0,X1,X2,sK23)),sF26) ),
inference(resolution,[],[f979,f208]) ).
fof(f1452,plain,
! [X2,X0,X1] :
( incident_c(sK15(sK22,sK16(X0,X1,X2,sK23)),sF26)
| between_o(sK22,X2,X1,X0)
| X0 = X2
| ~ between_o(sK23,X0,X1,X2) ),
inference(duplicate_literal_removal,[],[f1448]) ).
fof(f1453,plain,
! [X2,X0,X1] :
( between_o(sK22,X0,X1,X2)
| X0 = X2
| ~ between_o(sK23,X2,X1,X0)
| incident_o(sK15(sK22,sK16(X2,X1,X0,sK23)),sK23) ),
inference(resolution,[],[f1452,f201]) ).
fof(f1454,plain,
! [X2,X0,X1] :
( incident_o(sK15(sK22,sK16(X2,X1,X0,sK23)),sK22)
| X0 = X2
| ~ between_o(sK23,X2,X1,X0)
| between_o(sK22,X0,X1,X2) ),
inference(resolution,[],[f1452,f200]) ).
fof(f1457,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ incident_c(sK15(sK22,sK16(X1,X2,X0,sK23)),sK16(X1,X2,X0,sK23))
| ~ between_o(sK23,X1,X2,X0)
| between_o(sK22,X0,X2,X1)
| X0 = X1
| between_o(sK22,X3,X4,X5)
| ~ between_c(sK16(X1,X2,X0,sK23),X3,X4,X5) ),
inference(resolution,[],[f1454,f172]) ).
fof(f1464,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ between_o(sK23,X0,X1,X2)
| between_o(sK22,X2,X1,X0)
| X0 = X2
| between_o(sK22,X3,X4,X5)
| ~ between_c(sK16(X0,X1,X2,sK23),X3,X4,X5)
| ~ incident_o(sK15(sK22,sK16(X0,X1,X2,sK23)),sK23)
| ~ between_o(sK23,X0,X1,X2) ),
inference(resolution,[],[f1457,f169]) ).
fof(f1465,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ between_o(sK23,X0,X1,X2)
| between_o(sK22,X2,X1,X0)
| X0 = X2
| between_o(sK22,X3,X4,X5)
| ~ between_c(sK16(X0,X1,X2,sK23),X3,X4,X5)
| ~ incident_o(sK15(sK22,sK16(X0,X1,X2,sK23)),sK23) ),
inference(duplicate_literal_removal,[],[f1464]) ).
fof(f1470,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ between_c(sK16(X0,X1,X2,sK23),X3,X4,X5)
| between_o(sK22,X2,X1,X0)
| X0 = X2
| between_o(sK22,X3,X4,X5)
| ~ between_o(sK23,X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f1465,f1453]) ).
fof(f1472,plain,
! [X2,X0,X1] :
( between_o(sK22,X0,X1,X2)
| X0 = X2
| between_o(sK22,X0,X1,X2)
| ~ between_o(sK23,X2,X1,X0)
| X0 = X2
| ~ between_o(sK23,X2,X1,X0) ),
inference(resolution,[],[f1470,f266]) ).
fof(f1475,plain,
! [X2,X0,X1] :
( ~ between_o(sK23,X2,X1,X0)
| X0 = X2
| between_o(sK22,X0,X1,X2) ),
inference(duplicate_literal_removal,[],[f1472]) ).
fof(f1487,plain,
! [X2,X0,X1] :
( between_o(sK22,X0,X2,X1)
| X0 = X1
| ~ ordered_by(sK23,X0,X2)
| ~ ordered_by(sK23,X2,X1) ),
inference(resolution,[],[f1475,f159]) ).
fof(f1494,plain,
! [X2,X0,X1] :
( ~ ordered_by(sK23,X2,X1)
| ~ ordered_by(sK23,X0,X2)
| X0 = X1
| ordered_by(sK22,X2,X0)
| ordered_by(sK22,X2,X1) ),
inference(resolution,[],[f1487,f155]) ).
fof(f1495,plain,
! [X2,X0,X1] :
( ~ ordered_by(sK23,X2,X1)
| ~ ordered_by(sK23,X0,X2)
| X0 = X1
| ordered_by(sK22,X1,X2)
| ordered_by(sK22,X0,X2) ),
inference(resolution,[],[f1487,f158]) ).
fof(f1527,plain,
! [X0] :
( ~ ordered_by(sK23,X0,sK24)
| sK25 = X0
| ordered_by(sK22,sK25,sK24)
| ordered_by(sK22,X0,sK24) ),
inference(resolution,[],[f1495,f183]) ).
fof(f1528,plain,
! [X0] :
( ~ ordered_by(sK23,X0,sK24)
| sK25 = X0
| ordered_by(sK22,X0,sK24) ),
inference(forward_subsumption_resolution,[],[f1527,f205]) ).
fof(f1535,plain,
! [X0] :
( sK25 = X0
| ordered_by(sK22,X0,sK24)
| sK24 = X0
| ~ incident_o(sK24,sK23)
| ~ start_point(X0,sK23) ),
inference(resolution,[],[f1528,f161]) ).
fof(f1539,plain,
! [X0] :
( ordered_by(sK22,X0,sK24)
| sK25 = X0
| sK24 = X0
| ~ start_point(X0,sK23) ),
inference(forward_subsumption_resolution,[],[f1535,f211]) ).
fof(f1541,definition,
( spl28_46
<=> sK24 = sK20(sK23,sK22) ),
introduced(definition,[new_symbols(definition,[spl28_46])],[avatar_definition]) ).
fof(f1542,plain,
( sK24 != sK20(sK23,sK22)
| spl28_46 ),
inference(avatar_component_clause,[],[f1541]) ).
fof(f1543,plain,
( sK24 = sK20(sK23,sK22)
| ~ spl28_46 ),
inference(avatar_component_clause,[],[f1541]) ).
fof(f1545,definition,
( spl28_47
<=> sK24 = sK19(sK23,sK22) ),
introduced(definition,[new_symbols(definition,[spl28_47])],[avatar_definition]) ).
fof(f1546,plain,
( sK24 != sK19(sK23,sK22)
| spl28_47 ),
inference(avatar_component_clause,[],[f1545]) ).
fof(f1547,plain,
( sK24 = sK19(sK23,sK22)
| ~ spl28_47 ),
inference(avatar_component_clause,[],[f1545]) ).
fof(f1549,definition,
( spl28_48
<=> start_point(sK24,sK22) ),
introduced(definition,[new_symbols(definition,[spl28_48])],[avatar_definition]) ).
fof(f1550,plain,
( start_point(sK24,sK22)
| ~ spl28_48 ),
inference(avatar_component_clause,[],[f1549]) ).
fof(f1551,plain,
( ~ start_point(sK24,sK22)
| spl28_48 ),
inference(avatar_component_clause,[],[f1549]) ).
fof(f1553,definition,
( spl28_49
<=> sK25 = sK19(sK23,sK22) ),
introduced(definition,[new_symbols(definition,[spl28_49])],[avatar_definition]) ).
fof(f1554,plain,
( sK25 != sK19(sK23,sK22)
| spl28_49 ),
inference(avatar_component_clause,[],[f1553]) ).
fof(f1555,plain,
( sK25 = sK19(sK23,sK22)
| ~ spl28_49 ),
inference(avatar_component_clause,[],[f1553]) ).
fof(f1570,plain,
( ! [X0] :
( ~ ordered_by(sK23,X0,sK20(sK23,sK22))
| sK19(sK23,sK22) = X0
| ordered_by(sK22,sK20(sK23,sK22),X0)
| ordered_by(sK22,sK20(sK23,sK22),sK19(sK23,sK22)) )
| ~ spl28_34 ),
inference(resolution,[],[f1494,f1234]) ).
fof(f1573,plain,
( ! [X0] :
( ~ ordered_by(sK23,X0,sK20(sK23,sK22))
| sK19(sK23,sK22) = X0
| ordered_by(sK22,sK20(sK23,sK22),X0) )
| spl28_25
| ~ spl28_34 ),
inference(forward_subsumption_resolution,[],[f1570,f1225]) ).
fof(f1581,plain,
( ! [X0] :
( sK19(sK23,sK22) = X0
| ordered_by(sK22,sK20(sK23,sK22),X0)
| sK20(sK23,sK22) = X0
| ~ incident_o(sK20(sK23,sK22),sK23)
| ~ start_point(X0,sK23) )
| spl28_25
| ~ spl28_34 ),
inference(resolution,[],[f1573,f161]) ).
fof(f1588,plain,
( ! [X0] :
( ordered_by(sK22,sK20(sK23,sK22),X0)
| sK19(sK23,sK22) = X0
| sK20(sK23,sK22) = X0
| ~ start_point(X0,sK23) )
| spl28_25
| ~ spl28_32
| ~ spl28_34 ),
inference(forward_subsumption_resolution,[],[f1581,f1212]) ).
fof(f1633,definition,
( spl28_51
<=> ! [X0] :
( sK19(sK23,sK22) = X0
| ~ start_point(X0,sK23)
| sK20(sK23,sK22) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl28_51])],[avatar_definition]) ).
fof(f1634,plain,
( ! [X0] :
( ~ start_point(X0,sK23)
| sK19(sK23,sK22) = X0
| sK20(sK23,sK22) = X0 )
| ~ spl28_51 ),
inference(avatar_component_clause,[],[f1633]) ).
fof(f1672,plain,
! [X0,X1] :
( sK25 = X0
| sK24 = X0
| ~ start_point(X0,sK23)
| ~ ordered_by(sK22,X1,X0)
| sK24 = X1
| ordered_by(sK23,sK24,X0)
| ordered_by(sK23,X1,X0) ),
inference(resolution,[],[f1539,f1046]) ).
fof(f1674,plain,
! [X0] :
( sK25 = X0
| sK24 = X0
| ~ start_point(X0,sK23)
| ~ start_point(sK24,sK22)
| sK24 = X0 ),
inference(resolution,[],[f1539,f301]) ).
fof(f1676,plain,
! [X0] :
( ~ start_point(X0,sK23)
| sK24 = X0
| sK25 = X0
| incident_o(X0,sK22) ),
inference(resolution,[],[f1539,f164]) ).
fof(f1677,plain,
! [X0] :
( ~ ordered_by(sK22,sK24,X0)
| sK24 = X0
| ~ start_point(X0,sK23)
| sK25 = X0 ),
inference(resolution,[],[f1539,f204]) ).
fof(f1682,plain,
! [X0] :
( sK25 = X0
| sK24 = X0
| ~ start_point(X0,sK23)
| ~ start_point(sK24,sK22) ),
inference(duplicate_literal_removal,[],[f1674]) ).
fof(f1684,plain,
! [X0,X1] :
( ~ ordered_by(sK22,X1,X0)
| sK24 = X0
| ~ start_point(X0,sK23)
| sK25 = X0
| sK24 = X1
| ordered_by(sK23,X1,X0) ),
inference(forward_subsumption_resolution,[],[f1672,f301]) ).
fof(f1873,plain,
! [X0,X1] :
( sK24 = X0
| ~ start_point(X0,sK23)
| sK25 = X0
| sK24 = X1
| ordered_by(sK23,X1,X0)
| X0 = X1
| ~ incident_o(X0,sK22)
| ~ start_point(X1,sK22) ),
inference(resolution,[],[f1684,f161]) ).
fof(f1874,plain,
( sK24 = sK20(sK23,sK22)
| ~ start_point(sK20(sK23,sK22),sK23)
| sK25 = sK20(sK23,sK22)
| sK24 = sK19(sK23,sK22)
| ordered_by(sK23,sK19(sK23,sK22),sK20(sK23,sK22))
| spl28_25 ),
inference(resolution,[],[f1684,f1215]) ).
fof(f1877,plain,
( ! [X0] :
( sK24 = X0
| ~ start_point(X0,sK23)
| sK25 = X0
| sK24 = sK20(sK23,sK22)
| ordered_by(sK23,sK20(sK23,sK22),X0)
| sK19(sK23,sK22) = X0
| sK20(sK23,sK22) = X0
| ~ start_point(X0,sK23) )
| spl28_25
| ~ spl28_32
| ~ spl28_34 ),
inference(resolution,[],[f1684,f1588]) ).
fof(f1880,plain,
( ! [X0] :
( sK24 = X0
| ~ start_point(X0,sK23)
| sK25 = X0
| sK24 = sK20(sK23,sK22)
| ordered_by(sK23,sK20(sK23,sK22),X0)
| sK19(sK23,sK22) = X0
| sK20(sK23,sK22) = X0 )
| spl28_25
| ~ spl28_32
| ~ spl28_34 ),
inference(duplicate_literal_removal,[],[f1877]) ).
fof(f1884,plain,
( ! [X0] :
( sK24 = X0
| ~ start_point(X0,sK23)
| sK25 = X0
| sK24 = sK20(sK23,sK22)
| sK19(sK23,sK22) = X0
| sK20(sK23,sK22) = X0 )
| spl28_25
| ~ spl28_32
| ~ spl28_34 ),
inference(forward_subsumption_resolution,[],[f1880,f301]) ).
fof(f1885,plain,
( sK24 = sK20(sK23,sK22)
| ~ start_point(sK20(sK23,sK22),sK23)
| sK25 = sK20(sK23,sK22)
| sK24 = sK19(sK23,sK22)
| spl28_25 ),
inference(forward_subsumption_resolution,[],[f1874,f1161]) ).
fof(f1886,plain,
! [X0,X1] :
( sK24 = X0
| ~ start_point(X0,sK23)
| sK25 = X0
| sK24 = X1
| X0 = X1
| ~ incident_o(X0,sK22)
| ~ start_point(X1,sK22) ),
inference(forward_subsumption_resolution,[],[f1873,f301]) ).
fof(f1888,definition,
( spl28_52
<=> ! [X0] :
( sK24 = X0
| sK20(sK23,sK22) = X0
| sK19(sK23,sK22) = X0
| sK25 = X0
| ~ start_point(X0,sK23) ) ),
introduced(definition,[new_symbols(definition,[spl28_52])],[avatar_definition]) ).
fof(f1889,plain,
( ! [X0] :
( ~ start_point(X0,sK23)
| sK20(sK23,sK22) = X0
| sK19(sK23,sK22) = X0
| sK25 = X0
| sK24 = X0 )
| ~ spl28_52 ),
inference(avatar_component_clause,[],[f1888]) ).
fof(f1890,plain,
( spl28_46
| spl28_52
| spl28_25
| ~ spl28_32
| ~ spl28_34 ),
inference(avatar_split_clause,[],[f1884,f1232,f1211,f1160,f1888,f1541]) ).
fof(f1892,definition,
( spl28_53
<=> sK25 = sK20(sK23,sK22) ),
introduced(definition,[new_symbols(definition,[spl28_53])],[avatar_definition]) ).
fof(f1893,plain,
( sK25 != sK20(sK23,sK22)
| spl28_53 ),
inference(avatar_component_clause,[],[f1892]) ).
fof(f1894,plain,
( sK25 = sK20(sK23,sK22)
| ~ spl28_53 ),
inference(avatar_component_clause,[],[f1892]) ).
fof(f1895,plain,
( spl28_47
| spl28_53
| ~ spl28_30
| spl28_46
| spl28_25 ),
inference(avatar_split_clause,[],[f1885,f1160,f1541,f1198,f1892,f1545]) ).
fof(f1896,plain,
! [X0,X1] :
( ~ start_point(X1,sK22)
| ~ start_point(X0,sK23)
| sK25 = X0
| sK24 = X1
| X0 = X1
| sK24 = X0 ),
inference(forward_subsumption_resolution,[],[f1886,f1676]) ).
fof(f1897,plain,
( sK17(sK23) = sK20(sK23,sK22)
| sK17(sK23) = sK19(sK23,sK22)
| sK25 = sK17(sK23)
| sK24 = sK17(sK23)
| ~ spl28_52 ),
inference(resolution,[],[f1889,f173]) ).
fof(f1899,definition,
( spl28_54
<=> sK24 = sK17(sK23) ),
introduced(definition,[new_symbols(definition,[spl28_54])],[avatar_definition]) ).
fof(f1900,plain,
( sK24 != sK17(sK23)
| spl28_54 ),
inference(avatar_component_clause,[],[f1899]) ).
fof(f1901,plain,
( sK24 = sK17(sK23)
| ~ spl28_54 ),
inference(avatar_component_clause,[],[f1899]) ).
fof(f1903,definition,
( spl28_55
<=> sK25 = sK17(sK23) ),
introduced(definition,[new_symbols(definition,[spl28_55])],[avatar_definition]) ).
fof(f1904,plain,
( sK25 != sK17(sK23)
| spl28_55 ),
inference(avatar_component_clause,[],[f1903]) ).
fof(f1905,plain,
( sK25 = sK17(sK23)
| ~ spl28_55 ),
inference(avatar_component_clause,[],[f1903]) ).
fof(f1906,plain,
( spl28_54
| spl28_55
| spl28_43
| spl28_42
| ~ spl28_52 ),
inference(avatar_split_clause,[],[f1897,f1888,f1336,f1340,f1903,f1899]) ).
fof(f1912,plain,
( start_point(sK24,sK23)
| ~ spl28_54 ),
inference(superposition,[],[f173,f1901]) ).
fof(f1913,plain,
( $false
| spl28_22
| ~ spl28_54 ),
inference(forward_subsumption_resolution,[],[f1912,f1086]) ).
fof(f1914,plain,
( spl28_22
| ~ spl28_54 ),
inference(avatar_contradiction_clause,[],[f1913]) ).
fof(f1920,plain,
( ~ start_point(sK17(sK23),sK23)
| spl28_31
| ~ spl28_43 ),
inference(superposition,[],[f1209,f1342]) ).
fof(f1921,plain,
( ordered_by(sK22,sK17(sK23),sK20(sK23,sK22))
| spl28_25
| ~ spl28_43 ),
inference(superposition,[],[f1215,f1342]) ).
fof(f1923,plain,
( ~ ordered_by(sK22,sK17(sK23),sK17(sK23))
| spl28_25
| ~ spl28_43 ),
inference(superposition,[],[f1221,f1342]) ).
fof(f1976,plain,
( $false
| spl28_31
| ~ spl28_43 ),
inference(forward_subsumption_resolution,[],[f1920,f173]) ).
fof(f1977,plain,
( spl28_31
| ~ spl28_43 ),
inference(avatar_contradiction_clause,[],[f1976]) ).
fof(f1983,plain,
( start_point(sK25,sK23)
| ~ spl28_55 ),
inference(superposition,[],[f173,f1905]) ).
fof(f1984,plain,
( $false
| spl28_1
| ~ spl28_55 ),
inference(forward_subsumption_resolution,[],[f1983,f305]) ).
fof(f1985,plain,
( spl28_1
| ~ spl28_55 ),
inference(avatar_contradiction_clause,[],[f1984]) ).
fof(f1987,plain,
( ~ start_point(sK17(sK23),sK23)
| spl28_30
| ~ spl28_42 ),
inference(superposition,[],[f1200,f1338]) ).
fof(f2030,plain,
( $false
| spl28_30
| ~ spl28_42 ),
inference(forward_subsumption_resolution,[],[f1987,f173]) ).
fof(f2031,plain,
( spl28_30
| ~ spl28_42 ),
inference(avatar_contradiction_clause,[],[f2030]) ).
fof(f2034,plain,
( sK24 = sK17(sK23)
| ~ spl28_2
| ~ spl28_55 ),
inference(forward_demodulation,[],[f1905,f309]) ).
fof(f2035,plain,
( $false
| ~ spl28_2
| spl28_54
| ~ spl28_55 ),
inference(forward_subsumption_resolution,[],[f2034,f1900]) ).
fof(f2036,plain,
( ~ spl28_2
| spl28_54
| ~ spl28_55 ),
inference(avatar_contradiction_clause,[],[f2035]) ).
fof(f2037,plain,
( ~ ordered_by(sK23,sK19(sK23,sK22),sK24)
| spl28_25
| ~ spl28_46 ),
inference(superposition,[],[f1161,f1543]) ).
fof(f2040,plain,
( ordered_by(sK22,sK19(sK23,sK22),sK24)
| spl28_25
| ~ spl28_46 ),
inference(superposition,[],[f1215,f1543]) ).
fof(f2083,plain,
( sK25 = sK19(sK23,sK22)
| ordered_by(sK23,sK19(sK23,sK22),sK24)
| spl28_25
| ~ spl28_46 ),
inference(resolution,[],[f2040,f1064]) ).
fof(f2097,plain,
( sK25 = sK19(sK23,sK22)
| spl28_25
| ~ spl28_46 ),
inference(forward_subsumption_resolution,[],[f2083,f2037]) ).
fof(f2098,plain,
( spl28_49
| spl28_25
| ~ spl28_46 ),
inference(avatar_split_clause,[],[f2097,f1541,f1160,f1553]) ).
fof(f2102,plain,
( ordered_by(sK22,sK17(sK23),sK19(sK23,sK22))
| spl28_25
| ~ spl28_29
| ~ spl28_43 ),
inference(forward_demodulation,[],[f1921,f1196]) ).
fof(f2114,plain,
( ordered_by(sK22,sK17(sK23),sK17(sK23))
| spl28_25
| ~ spl28_29
| ~ spl28_43 ),
inference(forward_demodulation,[],[f2102,f1342]) ).
fof(f2121,plain,
( $false
| spl28_25
| ~ spl28_29
| ~ spl28_43 ),
inference(forward_subsumption_resolution,[],[f2114,f1923]) ).
fof(f2122,plain,
( spl28_25
| ~ spl28_29
| ~ spl28_43 ),
inference(avatar_contradiction_clause,[],[f2121]) ).
fof(f2125,plain,
( sK25 = sK17(sK23)
| ~ spl28_42
| ~ spl28_53 ),
inference(forward_demodulation,[],[f1894,f1338]) ).
fof(f2128,plain,
( $false
| ~ spl28_42
| ~ spl28_53
| spl28_55 ),
inference(forward_subsumption_resolution,[],[f2125,f1904]) ).
fof(f2129,plain,
( ~ spl28_42
| ~ spl28_53
| spl28_55 ),
inference(avatar_contradiction_clause,[],[f2128]) ).
fof(f2132,plain,
( sK24 != sK25
| ~ spl28_46
| spl28_53 ),
inference(forward_demodulation,[],[f1893,f1543]) ).
fof(f2133,plain,
( ~ spl28_2
| ~ spl28_46
| spl28_53 ),
inference(avatar_split_clause,[],[f2132,f1892,f1541,f307]) ).
fof(f2211,plain,
( ~ ordered_by(sK23,sK20(sK23,sK22),sK25)
| sK22 = sK23
| ordered_by(sK22,sK25,sK20(sK23,sK22))
| ~ spl28_49 ),
inference(superposition,[],[f442,f1555]) ).
fof(f2224,plain,
( ~ ordered_by(sK23,sK20(sK23,sK22),sK25)
| ordered_by(sK22,sK25,sK20(sK23,sK22))
| ~ spl28_49 ),
inference(forward_subsumption_resolution,[],[f2211,f186]) ).
fof(f2249,plain,
( ~ ordered_by(sK23,sK24,sK25)
| ordered_by(sK22,sK25,sK20(sK23,sK22))
| ~ spl28_46
| ~ spl28_49 ),
inference(forward_demodulation,[],[f2224,f1543]) ).
fof(f2267,plain,
( ordered_by(sK22,sK25,sK20(sK23,sK22))
| ~ spl28_46
| ~ spl28_49 ),
inference(forward_subsumption_resolution,[],[f2249,f183]) ).
fof(f2276,plain,
( ordered_by(sK22,sK25,sK24)
| ~ spl28_46
| ~ spl28_49 ),
inference(forward_demodulation,[],[f2267,f1543]) ).
fof(f2287,plain,
( $false
| ~ spl28_46
| ~ spl28_49 ),
inference(forward_subsumption_resolution,[],[f2276,f205]) ).
fof(f2288,plain,
( ~ spl28_46
| ~ spl28_49 ),
inference(avatar_contradiction_clause,[],[f2287]) ).
fof(f2353,plain,
( ordered_by(sK22,sK24,sK20(sK23,sK22))
| spl28_25
| ~ spl28_47 ),
inference(superposition,[],[f1215,f1547]) ).
fof(f2405,plain,
( ordered_by(sK22,sK24,sK17(sK23))
| spl28_25
| ~ spl28_42
| ~ spl28_47 ),
inference(forward_demodulation,[],[f2353,f1338]) ).
fof(f2515,plain,
! [X0] :
( ~ start_point(X0,sK23)
| sK25 = X0
| sK24 = sK17(sK22)
| sK17(sK22) = X0
| sK24 = X0 ),
inference(resolution,[],[f1896,f173]) ).
fof(f2517,definition,
( spl28_56
<=> sK24 = sK17(sK22) ),
introduced(definition,[new_symbols(definition,[spl28_56])],[avatar_definition]) ).
fof(f2518,plain,
( sK24 != sK17(sK22)
| spl28_56 ),
inference(avatar_component_clause,[],[f2517]) ).
fof(f2519,plain,
( sK24 = sK17(sK22)
| ~ spl28_56 ),
inference(avatar_component_clause,[],[f2517]) ).
fof(f2521,definition,
( spl28_57
<=> ! [X0] :
( ~ start_point(X0,sK23)
| sK24 = X0
| sK17(sK22) = X0
| sK25 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl28_57])],[avatar_definition]) ).
fof(f2522,plain,
( ! [X0] :
( ~ start_point(X0,sK23)
| sK24 = X0
| sK17(sK22) = X0
| sK25 = X0 )
| ~ spl28_57 ),
inference(avatar_component_clause,[],[f2521]) ).
fof(f2523,plain,
( spl28_56
| spl28_57 ),
inference(avatar_split_clause,[],[f2515,f2521,f2517]) ).
fof(f2528,plain,
( start_point(sK24,sK22)
| ~ spl28_56 ),
inference(superposition,[],[f173,f2519]) ).
fof(f2529,plain,
( $false
| spl28_48
| ~ spl28_56 ),
inference(forward_subsumption_resolution,[],[f2528,f1551]) ).
fof(f2530,plain,
( spl28_48
| ~ spl28_56 ),
inference(avatar_contradiction_clause,[],[f2529]) ).
fof(f2583,plain,
( sK24 = sK17(sK23)
| sK17(sK22) = sK17(sK23)
| sK25 = sK17(sK23)
| ~ spl28_57 ),
inference(resolution,[],[f2522,f173]) ).
fof(f2584,plain,
( sK24 = sK20(sK23,sK22)
| sK17(sK22) = sK20(sK23,sK22)
| sK25 = sK20(sK23,sK22)
| ~ spl28_30
| ~ spl28_57 ),
inference(resolution,[],[f2522,f1199]) ).
fof(f2585,plain,
( sK17(sK22) = sK20(sK23,sK22)
| sK25 = sK20(sK23,sK22)
| ~ spl28_30
| spl28_46
| ~ spl28_57 ),
inference(forward_subsumption_resolution,[],[f2584,f1542]) ).
fof(f2586,plain,
( sK17(sK22) = sK17(sK23)
| sK25 = sK17(sK23)
| spl28_54
| ~ spl28_57 ),
inference(forward_subsumption_resolution,[],[f2583,f1900]) ).
fof(f2587,plain,
( sK17(sK22) = sK20(sK23,sK22)
| ~ spl28_30
| spl28_46
| spl28_53
| ~ spl28_57 ),
inference(forward_subsumption_resolution,[],[f2585,f1893]) ).
fof(f2588,plain,
( sK17(sK22) = sK17(sK23)
| spl28_54
| spl28_55
| ~ spl28_57 ),
inference(forward_subsumption_resolution,[],[f2586,f1904]) ).
fof(f2641,plain,
( sK24 = sK17(sK23)
| ~ start_point(sK17(sK23),sK23)
| sK25 = sK17(sK23)
| spl28_25
| ~ spl28_42
| ~ spl28_47 ),
inference(resolution,[],[f2405,f1677]) ).
fof(f2654,plain,
( ~ start_point(sK17(sK23),sK23)
| sK25 = sK17(sK23)
| spl28_25
| ~ spl28_42
| ~ spl28_47
| spl28_54 ),
inference(forward_subsumption_resolution,[],[f2641,f1900]) ).
fof(f2655,plain,
( sK25 = sK17(sK23)
| spl28_25
| ~ spl28_42
| ~ spl28_47
| spl28_54 ),
inference(forward_subsumption_resolution,[],[f2654,f173]) ).
fof(f2656,plain,
( $false
| spl28_25
| ~ spl28_42
| ~ spl28_47
| spl28_54
| spl28_55 ),
inference(forward_subsumption_resolution,[],[f2655,f1904]) ).
fof(f2657,plain,
( spl28_25
| ~ spl28_42
| ~ spl28_47
| spl28_54
| spl28_55 ),
inference(avatar_contradiction_clause,[],[f2656]) ).
fof(f2658,plain,
( sK17(sK22) != sK20(sK23,sK22)
| spl28_42
| spl28_54
| spl28_55
| ~ spl28_57 ),
inference(forward_demodulation,[],[f1337,f2588]) ).
fof(f2662,plain,
( sK17(sK22) = sK20(sK23,sK22)
| sK17(sK22) = sK19(sK23,sK22)
| ~ spl28_27 ),
inference(resolution,[],[f1180,f173]) ).
fof(f2663,plain,
( sK17(sK22) = sK19(sK23,sK22)
| ~ spl28_27
| spl28_42
| spl28_54
| spl28_55
| ~ spl28_57 ),
inference(forward_subsumption_resolution,[],[f2662,f2658]) ).
fof(f2685,plain,
( sK17(sK22) != sK17(sK23)
| ~ spl28_27
| spl28_42
| spl28_43
| spl28_54
| spl28_55
| ~ spl28_57 ),
inference(superposition,[],[f1341,f2663]) ).
fof(f2726,plain,
( $false
| ~ spl28_27
| spl28_42
| spl28_43
| spl28_54
| spl28_55
| ~ spl28_57 ),
inference(forward_subsumption_resolution,[],[f2685,f2588]) ).
fof(f2727,plain,
( ~ spl28_27
| spl28_42
| spl28_43
| spl28_54
| spl28_55
| ~ spl28_57 ),
inference(avatar_contradiction_clause,[],[f2726]) ).
fof(f2730,plain,
( ! [X0] :
( ~ start_point(X0,sK23)
| sK24 = X0
| sK25 = X0 )
| ~ spl28_48 ),
inference(forward_subsumption_resolution,[],[f1682,f1550]) ).
fof(f2746,plain,
( ~ ordered_by(sK23,sK20(sK23,sK22),sK24)
| spl28_34
| ~ spl28_47 ),
inference(superposition,[],[f1233,f1547]) ).
fof(f2821,plain,
( sK24 = sK17(sK23)
| sK25 = sK17(sK23)
| ~ spl28_48 ),
inference(resolution,[],[f2730,f173]) ).
fof(f2822,plain,
( sK25 = sK17(sK23)
| ~ spl28_48
| spl28_54 ),
inference(forward_subsumption_resolution,[],[f2821,f1900]) ).
fof(f2823,plain,
( $false
| ~ spl28_48
| spl28_54
| spl28_55 ),
inference(forward_subsumption_resolution,[],[f2822,f1904]) ).
fof(f2824,plain,
( ~ spl28_48
| spl28_54
| spl28_55 ),
inference(avatar_contradiction_clause,[],[f2823]) ).
fof(f2834,plain,
( $false
| spl28_25
| spl28_32 ),
inference(forward_subsumption_resolution,[],[f1290,f1213]) ).
fof(f2835,plain,
( spl28_25
| spl28_32 ),
inference(avatar_contradiction_clause,[],[f2834]) ).
fof(f2853,plain,
( sK24 != sK17(sK23)
| spl28_43
| ~ spl28_47 ),
inference(forward_demodulation,[],[f1341,f1547]) ).
fof(f2861,plain,
( $false
| spl28_43
| ~ spl28_47
| ~ spl28_54 ),
inference(forward_subsumption_resolution,[],[f2853,f1901]) ).
fof(f2862,plain,
( spl28_43
| ~ spl28_47
| ~ spl28_54 ),
inference(avatar_contradiction_clause,[],[f2861]) ).
fof(f2873,definition,
( spl28_58
<=> sK17(sK22) = sK19(sK23,sK22) ),
introduced(definition,[new_symbols(definition,[spl28_58])],[avatar_definition]) ).
fof(f2874,plain,
( sK17(sK22) != sK19(sK23,sK22)
| spl28_58 ),
inference(avatar_component_clause,[],[f2873]) ).
fof(f2875,plain,
( sK17(sK22) = sK19(sK23,sK22)
| ~ spl28_58 ),
inference(avatar_component_clause,[],[f2873]) ).
fof(f2877,definition,
( spl28_59
<=> sK17(sK22) = sK20(sK23,sK22) ),
introduced(definition,[new_symbols(definition,[spl28_59])],[avatar_definition]) ).
fof(f2878,plain,
( sK17(sK22) != sK20(sK23,sK22)
| spl28_59 ),
inference(avatar_component_clause,[],[f2877]) ).
fof(f2879,plain,
( sK17(sK22) = sK20(sK23,sK22)
| ~ spl28_59 ),
inference(avatar_component_clause,[],[f2877]) ).
fof(f2880,plain,
( spl28_58
| spl28_59
| ~ spl28_27 ),
inference(avatar_split_clause,[],[f2662,f1179,f2877,f2873]) ).
fof(f2881,plain,
( sK25 = sK17(sK22)
| sK24 = sK17(sK22)
| ~ spl28_23 ),
inference(resolution,[],[f1089,f173]) ).
fof(f2882,plain,
( sK25 = sK17(sK22)
| ~ spl28_23
| spl28_56 ),
inference(forward_subsumption_resolution,[],[f2881,f2518]) ).
fof(f2884,plain,
( sK24 = sK19(sK23,sK22)
| sK24 = sK20(sK23,sK22)
| ~ start_point(sK24,sK22)
| ~ spl28_22
| ~ spl28_24 ),
inference(resolution,[],[f1085,f1173]) ).
fof(f2895,plain,
( ~ ordered_by(sK23,sK17(sK22),sK17(sK22))
| spl28_28
| ~ spl28_58 ),
inference(superposition,[],[f1185,f2875]) ).
fof(f3015,plain,
( start_point(sK25,sK22)
| ~ spl28_23
| spl28_56 ),
inference(superposition,[],[f173,f2882]) ).
fof(f3016,plain,
( $false
| spl28_3
| ~ spl28_23
| spl28_56 ),
inference(forward_subsumption_resolution,[],[f3015,f314]) ).
fof(f3017,plain,
( spl28_3
| ~ spl28_23
| spl28_56 ),
inference(avatar_contradiction_clause,[],[f3016]) ).
fof(f3020,plain,
( start_point(sK24,sK22)
| ~ spl28_2
| ~ spl28_23
| spl28_56 ),
inference(forward_demodulation,[],[f3015,f309]) ).
fof(f3024,plain,
( $false
| ~ spl28_2
| ~ spl28_23
| spl28_48
| spl28_56 ),
inference(forward_subsumption_resolution,[],[f3020,f1551]) ).
fof(f3025,plain,
( ~ spl28_2
| ~ spl28_23
| spl28_48
| spl28_56 ),
inference(avatar_contradiction_clause,[],[f3024]) ).
fof(f3034,plain,
( sK24 = sK20(sK23,sK22)
| ~ start_point(sK24,sK22)
| ~ spl28_22
| ~ spl28_24
| spl28_47 ),
inference(forward_subsumption_resolution,[],[f2884,f1546]) ).
fof(f3038,plain,
( ~ start_point(sK24,sK22)
| ~ spl28_22
| ~ spl28_24
| spl28_46
| spl28_47 ),
inference(forward_subsumption_resolution,[],[f3034,f1542]) ).
fof(f3040,plain,
( $false
| ~ spl28_22
| ~ spl28_24
| spl28_46
| spl28_47
| ~ spl28_48 ),
inference(forward_subsumption_resolution,[],[f3038,f1550]) ).
fof(f3041,plain,
( ~ spl28_22
| ~ spl28_24
| spl28_46
| spl28_47
| ~ spl28_48 ),
inference(avatar_contradiction_clause,[],[f3040]) ).
fof(f3042,plain,
( ordered_by(sK23,sK25,sK20(sK23,sK22))
| ~ spl28_25
| ~ spl28_49 ),
inference(forward_demodulation,[],[f1162,f1555]) ).
fof(f3043,plain,
( $false
| ~ spl28_25
| ~ spl28_34 ),
inference(forward_subsumption_resolution,[],[f1191,f1234]) ).
fof(f3044,plain,
( ~ spl28_25
| ~ spl28_34 ),
inference(avatar_contradiction_clause,[],[f3043]) ).
fof(f3100,plain,
( ~ ordered_by(sK22,sK25,sK20(sK23,sK22))
| sK22 = sK23
| ~ ordered_by(sK23,sK25,sK20(sK23,sK22))
| ~ spl28_49 ),
inference(superposition,[],[f178,f1555]) ).
fof(f3114,plain,
( ~ ordered_by(sK22,sK25,sK20(sK23,sK22))
| ~ ordered_by(sK23,sK25,sK20(sK23,sK22))
| ~ spl28_49 ),
inference(forward_subsumption_resolution,[],[f3100,f186]) ).
fof(f3116,plain,
( ~ ordered_by(sK22,sK25,sK20(sK23,sK22))
| ~ spl28_25
| ~ spl28_49 ),
inference(forward_subsumption_resolution,[],[f3114,f3042]) ).
fof(f3133,plain,
( ! [X0] :
( ~ ordered_by(sK23,X0,sK25)
| sK20(sK23,sK22) = X0
| ordered_by(sK22,sK25,X0)
| ordered_by(sK22,sK25,sK20(sK23,sK22)) )
| ~ spl28_25
| ~ spl28_49 ),
inference(resolution,[],[f3042,f1494]) ).
fof(f3144,plain,
( ! [X0] :
( ~ ordered_by(sK23,X0,sK25)
| sK20(sK23,sK22) = X0
| ordered_by(sK22,sK25,X0) )
| ~ spl28_25
| ~ spl28_49 ),
inference(forward_subsumption_resolution,[],[f3133,f3116]) ).
fof(f3173,plain,
( sK24 = sK20(sK23,sK22)
| ordered_by(sK22,sK25,sK24)
| ~ spl28_25
| ~ spl28_49 ),
inference(resolution,[],[f3144,f183]) ).
fof(f3174,plain,
( ordered_by(sK22,sK25,sK24)
| ~ spl28_25
| spl28_46
| ~ spl28_49 ),
inference(forward_subsumption_resolution,[],[f3173,f1542]) ).
fof(f3176,plain,
( $false
| ~ spl28_25
| spl28_46
| ~ spl28_49 ),
inference(forward_subsumption_resolution,[],[f3174,f205]) ).
fof(f3177,plain,
( ~ spl28_25
| spl28_46
| ~ spl28_49 ),
inference(avatar_contradiction_clause,[],[f3176]) ).
fof(f3178,plain,
( sK24 != sK19(sK23,sK22)
| ~ spl28_56
| spl28_58 ),
inference(forward_demodulation,[],[f2874,f2519]) ).
fof(f3201,plain,
( ! [X0] :
( ~ ordered_by(sK23,X0,sK19(sK23,sK22))
| sK20(sK23,sK22) = X0
| ordered_by(sK22,sK19(sK23,sK22),X0)
| ordered_by(sK22,sK19(sK23,sK22),sK20(sK23,sK22)) )
| ~ spl28_25 ),
inference(resolution,[],[f1162,f1494]) ).
fof(f3202,plain,
( ! [X0] :
( ~ ordered_by(sK23,X0,sK19(sK23,sK22))
| sK20(sK23,sK22) = X0
| ordered_by(sK22,sK20(sK23,sK22),sK19(sK23,sK22))
| ordered_by(sK22,X0,sK19(sK23,sK22)) )
| ~ spl28_25 ),
inference(resolution,[],[f1162,f1495]) ).
fof(f3204,plain,
( ~ start_point(sK20(sK23,sK22),sK23)
| sK20(sK23,sK22) = sK19(sK23,sK22)
| ~ spl28_25 ),
inference(resolution,[],[f1162,f301]) ).
fof(f3205,plain,
( incident_o(sK20(sK23,sK22),sK23)
| ~ spl28_25 ),
inference(resolution,[],[f1162,f163]) ).
fof(f3209,definition,
( spl28_69
<=> ordered_by(sK22,sK20(sK23,sK22),sK19(sK23,sK22)) ),
introduced(definition,[new_symbols(definition,[spl28_69])],[avatar_definition]) ).
fof(f3211,plain,
( ordered_by(sK22,sK20(sK23,sK22),sK19(sK23,sK22))
| ~ spl28_69 ),
inference(avatar_component_clause,[],[f3209]) ).
fof(f3213,definition,
( spl28_70
<=> ! [X0] :
( ~ ordered_by(sK23,X0,sK19(sK23,sK22))
| ordered_by(sK22,X0,sK19(sK23,sK22))
| sK20(sK23,sK22) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl28_70])],[avatar_definition]) ).
fof(f3214,plain,
( ! [X0] :
( ~ ordered_by(sK23,X0,sK19(sK23,sK22))
| ordered_by(sK22,X0,sK19(sK23,sK22))
| sK20(sK23,sK22) = X0 )
| ~ spl28_70 ),
inference(avatar_component_clause,[],[f3213]) ).
fof(f3215,plain,
( spl28_69
| spl28_70
| ~ spl28_25 ),
inference(avatar_split_clause,[],[f3202,f1160,f3213,f3209]) ).
fof(f3217,definition,
( spl28_71
<=> ordered_by(sK22,sK19(sK23,sK22),sK20(sK23,sK22)) ),
introduced(definition,[new_symbols(definition,[spl28_71])],[avatar_definition]) ).
fof(f3218,plain,
( ~ ordered_by(sK22,sK19(sK23,sK22),sK20(sK23,sK22))
| spl28_71 ),
inference(avatar_component_clause,[],[f3217]) ).
fof(f3219,plain,
( ordered_by(sK22,sK19(sK23,sK22),sK20(sK23,sK22))
| ~ spl28_71 ),
inference(avatar_component_clause,[],[f3217]) ).
fof(f3221,definition,
( spl28_72
<=> ! [X0] :
( ~ ordered_by(sK23,X0,sK19(sK23,sK22))
| ordered_by(sK22,sK19(sK23,sK22),X0)
| sK20(sK23,sK22) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl28_72])],[avatar_definition]) ).
fof(f3222,plain,
( ! [X0] :
( ~ ordered_by(sK23,X0,sK19(sK23,sK22))
| ordered_by(sK22,sK19(sK23,sK22),X0)
| sK20(sK23,sK22) = X0 )
| ~ spl28_72 ),
inference(avatar_component_clause,[],[f3221]) ).
fof(f3223,plain,
( spl28_71
| spl28_72
| ~ spl28_25 ),
inference(avatar_split_clause,[],[f3201,f1160,f3221,f3217]) ).
fof(f3259,plain,
( sK22 = sK23
| ~ ordered_by(sK23,sK19(sK23,sK22),sK20(sK23,sK22))
| ~ spl28_71 ),
inference(resolution,[],[f3219,f178]) ).
fof(f3265,plain,
( ~ ordered_by(sK23,sK19(sK23,sK22),sK20(sK23,sK22))
| ~ spl28_71 ),
inference(forward_subsumption_resolution,[],[f3259,f186]) ).
fof(f3267,plain,
( $false
| ~ spl28_25
| ~ spl28_71 ),
inference(forward_subsumption_resolution,[],[f3265,f1162]) ).
fof(f3268,plain,
( ~ spl28_25
| ~ spl28_71 ),
inference(avatar_contradiction_clause,[],[f3267]) ).
fof(f3295,plain,
( sK20(sK23,sK22) = sK19(sK23,sK22)
| ~ incident_o(sK20(sK23,sK22),sK22)
| ~ start_point(sK19(sK23,sK22),sK22)
| spl28_71 ),
inference(resolution,[],[f3218,f161]) ).
fof(f3297,plain,
( ! [X0] :
( ordered_by(sK22,X0,sK19(sK23,sK22))
| sK20(sK23,sK22) = X0
| sK19(sK23,sK22) = X0
| ~ incident_o(sK19(sK23,sK22),sK23)
| ~ start_point(X0,sK23) )
| ~ spl28_70 ),
inference(resolution,[],[f3214,f161]) ).
fof(f3302,plain,
( ! [X0] :
( ordered_by(sK22,X0,sK19(sK23,sK22))
| sK20(sK23,sK22) = X0
| sK19(sK23,sK22) = X0
| ~ start_point(X0,sK23) )
| ~ spl28_26
| ~ spl28_70 ),
inference(forward_subsumption_resolution,[],[f3297,f1177]) ).
fof(f3304,plain,
( ! [X0] :
( ordered_by(sK22,sK19(sK23,sK22),X0)
| sK20(sK23,sK22) = X0
| sK19(sK23,sK22) = X0
| ~ incident_o(sK19(sK23,sK22),sK23)
| ~ start_point(X0,sK23) )
| ~ spl28_72 ),
inference(resolution,[],[f3222,f161]) ).
fof(f3310,plain,
( ! [X0] :
( ordered_by(sK22,sK19(sK23,sK22),X0)
| sK20(sK23,sK22) = X0
| sK19(sK23,sK22) = X0
| ~ start_point(X0,sK23) )
| ~ spl28_26
| ~ spl28_72 ),
inference(forward_subsumption_resolution,[],[f3304,f1177]) ).
fof(f3314,plain,
( sK20(sK23,sK22) = sK19(sK23,sK22)
| ~ incident_o(sK19(sK23,sK22),sK23)
| ~ start_point(sK20(sK23,sK22),sK23)
| spl28_34 ),
inference(resolution,[],[f1233,f161]) ).
fof(f3326,plain,
( ! [X0] :
( sK20(sK23,sK22) = X0
| sK19(sK23,sK22) = X0
| ~ start_point(X0,sK23)
| sK24 = X0
| ~ start_point(X0,sK23)
| sK25 = X0
| sK24 = sK19(sK23,sK22)
| ordered_by(sK23,sK19(sK23,sK22),X0) )
| ~ spl28_26
| ~ spl28_72 ),
inference(resolution,[],[f3310,f1684]) ).
fof(f3331,plain,
( sK24 = sK20(sK23,sK22)
| sK24 = sK19(sK23,sK22)
| ~ start_point(sK24,sK23)
| sK25 = sK19(sK23,sK22)
| ordered_by(sK23,sK19(sK23,sK22),sK24)
| ~ spl28_26
| ~ spl28_72 ),
inference(resolution,[],[f3310,f1064]) ).
fof(f3337,plain,
( ! [X0] :
( sK20(sK23,sK22) = X0
| sK19(sK23,sK22) = X0
| ~ start_point(X0,sK23)
| ~ ordered_by(sK22,X0,sK19(sK23,sK22)) )
| ~ spl28_26
| ~ spl28_72 ),
inference(resolution,[],[f3310,f204]) ).
fof(f3343,plain,
( ! [X0] :
( sK20(sK23,sK22) = X0
| sK19(sK23,sK22) = X0
| ~ start_point(X0,sK23)
| sK24 = X0
| sK25 = X0
| sK24 = sK19(sK23,sK22)
| ordered_by(sK23,sK19(sK23,sK22),X0) )
| ~ spl28_26
| ~ spl28_72 ),
inference(duplicate_literal_removal,[],[f3326]) ).
fof(f3344,plain,
( ! [X0] :
( sK20(sK23,sK22) = X0
| sK19(sK23,sK22) = X0
| ~ start_point(X0,sK23) )
| ~ spl28_26
| ~ spl28_70
| ~ spl28_72 ),
inference(forward_subsumption_resolution,[],[f3337,f3302]) ).
fof(f3350,plain,
( sK24 = sK19(sK23,sK22)
| ~ start_point(sK24,sK23)
| sK25 = sK19(sK23,sK22)
| ordered_by(sK23,sK19(sK23,sK22),sK24)
| ~ spl28_26
| spl28_46
| ~ spl28_72 ),
inference(forward_subsumption_resolution,[],[f3331,f1542]) ).
fof(f3355,plain,
( spl28_51
| ~ spl28_26
| ~ spl28_70
| ~ spl28_72 ),
inference(avatar_split_clause,[],[f3344,f3221,f3213,f1175,f1633]) ).
fof(f3356,plain,
( ~ start_point(sK24,sK23)
| sK25 = sK19(sK23,sK22)
| ordered_by(sK23,sK19(sK23,sK22),sK24)
| ~ spl28_26
| spl28_46
| spl28_47
| ~ spl28_72 ),
inference(forward_subsumption_resolution,[],[f3350,f1546]) ).
fof(f3357,plain,
( sK25 = sK19(sK23,sK22)
| ordered_by(sK23,sK19(sK23,sK22),sK24)
| ~ spl28_22
| ~ spl28_26
| spl28_46
| spl28_47
| ~ spl28_72 ),
inference(forward_subsumption_resolution,[],[f3356,f1085]) ).
fof(f3358,plain,
( ordered_by(sK23,sK19(sK23,sK22),sK24)
| ~ spl28_22
| ~ spl28_26
| spl28_46
| spl28_47
| spl28_49
| ~ spl28_72 ),
inference(forward_subsumption_resolution,[],[f3357,f1554]) ).
fof(f3365,plain,
( ~ start_point(sK24,sK23)
| sK24 = sK19(sK23,sK22)
| ~ spl28_22
| ~ spl28_26
| spl28_46
| spl28_47
| spl28_49
| ~ spl28_72 ),
inference(resolution,[],[f3358,f301]) ).
fof(f3369,plain,
( sK24 = sK19(sK23,sK22)
| ~ spl28_22
| ~ spl28_26
| spl28_46
| spl28_47
| spl28_49
| ~ spl28_72 ),
inference(forward_subsumption_resolution,[],[f3365,f1085]) ).
fof(f3391,plain,
( $false
| ~ spl28_22
| ~ spl28_26
| spl28_46
| spl28_47
| spl28_49
| ~ spl28_72 ),
inference(forward_subsumption_resolution,[],[f3369,f1546]) ).
fof(f3392,plain,
( ~ spl28_22
| ~ spl28_26
| spl28_46
| spl28_47
| spl28_49
| ~ spl28_72 ),
inference(avatar_contradiction_clause,[],[f3391]) ).
fof(f3396,plain,
( $false
| ~ spl28_47
| ~ spl28_56
| spl28_58 ),
inference(forward_subsumption_resolution,[],[f3178,f1547]) ).
fof(f3397,plain,
( ~ spl28_47
| ~ spl28_56
| spl28_58 ),
inference(avatar_contradiction_clause,[],[f3396]) ).
fof(f3410,plain,
( ordered_by(sK22,sK20(sK23,sK22),sK24)
| ~ spl28_47
| ~ spl28_69 ),
inference(superposition,[],[f3211,f1547]) ).
fof(f3463,plain,
( incident_o(sK20(sK23,sK22),sK22)
| ~ spl28_32 ),
inference(resolution,[],[f1303,f200]) ).
fof(f3476,plain,
( sK24 = sK20(sK23,sK22)
| ~ incident_o(sK20(sK23,sK22),sK22)
| ~ start_point(sK19(sK23,sK22),sK22)
| ~ spl28_47
| spl28_71 ),
inference(forward_demodulation,[],[f3295,f1547]) ).
fof(f3479,plain,
( ~ incident_o(sK20(sK23,sK22),sK22)
| ~ start_point(sK19(sK23,sK22),sK22)
| spl28_46
| ~ spl28_47
| spl28_71 ),
inference(forward_subsumption_resolution,[],[f3476,f1542]) ).
fof(f3480,plain,
( ~ start_point(sK19(sK23,sK22),sK22)
| ~ spl28_32
| spl28_46
| ~ spl28_47
| spl28_71 ),
inference(forward_subsumption_resolution,[],[f3479,f3463]) ).
fof(f3481,plain,
( ~ start_point(sK24,sK22)
| ~ spl28_32
| spl28_46
| ~ spl28_47
| spl28_71 ),
inference(forward_demodulation,[],[f3480,f1547]) ).
fof(f3488,plain,
( $false
| ~ spl28_25
| spl28_32 ),
inference(forward_subsumption_resolution,[],[f3205,f1213]) ).
fof(f3489,plain,
( ~ spl28_25
| spl28_32 ),
inference(avatar_contradiction_clause,[],[f3488]) ).
fof(f3491,plain,
( ~ spl28_48
| ~ spl28_32
| spl28_46
| ~ spl28_47
| spl28_71 ),
inference(avatar_split_clause,[],[f3481,f3217,f1545,f1541,f1211,f1549]) ).
fof(f3494,plain,
( ~ spl28_59
| spl28_42
| spl28_54
| spl28_55
| ~ spl28_57 ),
inference(avatar_split_clause,[],[f2658,f2521,f1903,f1899,f1336,f2877]) ).
fof(f3526,plain,
( sK17(sK23) = sK19(sK23,sK22)
| sK17(sK23) = sK20(sK23,sK22)
| ~ spl28_51 ),
inference(resolution,[],[f1634,f173]) ).
fof(f3541,plain,
( sK25 = sK20(sK23,sK22)
| ordered_by(sK23,sK20(sK23,sK22),sK24)
| ~ spl28_47
| ~ spl28_69 ),
inference(resolution,[],[f3410,f1064]) ).
fof(f3555,plain,
( ordered_by(sK23,sK20(sK23,sK22),sK24)
| ~ spl28_47
| spl28_53
| ~ spl28_69 ),
inference(forward_subsumption_resolution,[],[f3541,f1893]) ).
fof(f3556,plain,
( $false
| spl28_34
| ~ spl28_47
| spl28_53
| ~ spl28_69 ),
inference(forward_subsumption_resolution,[],[f3555,f2746]) ).
fof(f3557,plain,
( spl28_34
| ~ spl28_47
| spl28_53
| ~ spl28_69 ),
inference(avatar_contradiction_clause,[],[f3556]) ).
fof(f3582,plain,
( ~ ordered_by(sK22,sK19(sK23,sK22),sK25)
| sK22 = sK23
| ~ ordered_by(sK23,sK19(sK23,sK22),sK25)
| ~ spl28_53 ),
inference(superposition,[],[f178,f1894]) ).
fof(f3596,plain,
( ~ ordered_by(sK22,sK19(sK23,sK22),sK25)
| ~ ordered_by(sK23,sK19(sK23,sK22),sK25)
| ~ spl28_53 ),
inference(forward_subsumption_resolution,[],[f3582,f186]) ).
fof(f3612,plain,
( ~ ordered_by(sK22,sK24,sK25)
| ~ ordered_by(sK23,sK19(sK23,sK22),sK25)
| ~ spl28_47
| ~ spl28_53 ),
inference(forward_demodulation,[],[f3596,f1547]) ).
fof(f3619,plain,
( ~ ordered_by(sK23,sK19(sK23,sK22),sK25)
| ~ spl28_47
| ~ spl28_53 ),
inference(forward_subsumption_resolution,[],[f3612,f184]) ).
fof(f3621,plain,
( ~ ordered_by(sK23,sK24,sK25)
| ~ spl28_47
| ~ spl28_53 ),
inference(forward_demodulation,[],[f3619,f1547]) ).
fof(f3623,plain,
( $false
| ~ spl28_47
| ~ spl28_53 ),
inference(forward_subsumption_resolution,[],[f3621,f183]) ).
fof(f3624,plain,
( ~ spl28_47
| ~ spl28_53 ),
inference(avatar_contradiction_clause,[],[f3623]) ).
fof(f3625,plain,
( sK17(sK22) = sK19(sK23,sK22)
| sK17(sK23) = sK20(sK23,sK22)
| ~ spl28_51
| spl28_54
| spl28_55
| ~ spl28_57 ),
inference(forward_demodulation,[],[f3526,f2588]) ).
fof(f3627,plain,
( sK20(sK23,sK22) = sK19(sK23,sK22)
| ~ start_point(sK19(sK23,sK22),sK22)
| ~ spl28_32
| spl28_71 ),
inference(forward_subsumption_resolution,[],[f3295,f3463]) ).
fof(f3629,plain,
( sK17(sK23) = sK20(sK23,sK22)
| ~ spl28_51
| spl28_54
| spl28_55
| ~ spl28_57
| spl28_58 ),
inference(forward_subsumption_resolution,[],[f3625,f2874]) ).
fof(f3631,plain,
( sK17(sK22) = sK20(sK23,sK22)
| ~ spl28_51
| spl28_54
| spl28_55
| ~ spl28_57
| spl28_58 ),
inference(forward_demodulation,[],[f3629,f2588]) ).
fof(f3632,plain,
( $false
| ~ spl28_51
| spl28_54
| spl28_55
| ~ spl28_57
| spl28_58
| spl28_59 ),
inference(forward_subsumption_resolution,[],[f3631,f2878]) ).
fof(f3633,plain,
( ~ spl28_51
| spl28_54
| spl28_55
| ~ spl28_57
| spl28_58
| spl28_59 ),
inference(avatar_contradiction_clause,[],[f3632]) ).
fof(f3634,plain,
( ! [X0] :
( sK20(sK23,sK22) = X0
| sK19(sK23,sK22) = X0
| ~ start_point(X0,sK23)
| sK24 = X0
| sK25 = X0
| ordered_by(sK23,sK19(sK23,sK22),X0) )
| ~ spl28_26
| spl28_47
| ~ spl28_72 ),
inference(forward_subsumption_resolution,[],[f3343,f1546]) ).
fof(f3635,plain,
( ! [X0] :
( sK20(sK23,sK22) = X0
| sK19(sK23,sK22) = X0
| ~ start_point(X0,sK23)
| sK24 = X0
| sK25 = X0 )
| ~ spl28_26
| spl28_47
| ~ spl28_72 ),
inference(forward_subsumption_resolution,[],[f3634,f301]) ).
fof(f3636,plain,
( spl28_52
| ~ spl28_26
| spl28_47
| ~ spl28_72 ),
inference(avatar_split_clause,[],[f3635,f3221,f1545,f1175,f1888]) ).
fof(f3637,plain,
( sK17(sK22) = sK19(sK23,sK22)
| ~ spl28_43
| spl28_54
| spl28_55
| ~ spl28_57 ),
inference(forward_demodulation,[],[f1342,f2588]) ).
fof(f3639,plain,
( $false
| ~ spl28_43
| spl28_54
| spl28_55
| ~ spl28_57
| spl28_58 ),
inference(forward_subsumption_resolution,[],[f3637,f2874]) ).
fof(f3640,plain,
( ~ spl28_43
| spl28_54
| spl28_55
| ~ spl28_57
| spl28_58 ),
inference(avatar_contradiction_clause,[],[f3639]) ).
fof(f3744,plain,
( sK17(sK22) = sK20(sK23,sK22)
| ~ spl28_29
| ~ spl28_58 ),
inference(forward_demodulation,[],[f1196,f2875]) ).
fof(f3748,plain,
( sK17(sK22) = sK20(sK23,sK22)
| ~ start_point(sK19(sK23,sK22),sK22)
| ~ spl28_32
| ~ spl28_58
| spl28_71 ),
inference(forward_demodulation,[],[f3627,f2875]) ).
fof(f3749,plain,
( $false
| ~ spl28_29
| ~ spl28_58
| spl28_59 ),
inference(forward_subsumption_resolution,[],[f3744,f2878]) ).
fof(f3750,plain,
( ~ spl28_29
| ~ spl28_58
| spl28_59 ),
inference(avatar_contradiction_clause,[],[f3749]) ).
fof(f3751,plain,
( ~ start_point(sK19(sK23,sK22),sK22)
| ~ spl28_32
| ~ spl28_58
| spl28_59
| spl28_71 ),
inference(forward_subsumption_resolution,[],[f3748,f2878]) ).
fof(f3752,plain,
( ~ start_point(sK17(sK22),sK22)
| ~ spl28_32
| ~ spl28_58
| spl28_59
| spl28_71 ),
inference(forward_demodulation,[],[f3751,f2875]) ).
fof(f3753,plain,
( $false
| ~ spl28_32
| ~ spl28_58
| spl28_59
| spl28_71 ),
inference(forward_subsumption_resolution,[],[f3752,f173]) ).
fof(f3754,plain,
( ~ spl28_32
| ~ spl28_58
| spl28_59
| spl28_71 ),
inference(avatar_contradiction_clause,[],[f3753]) ).
fof(f3756,plain,
( spl28_59
| ~ spl28_30
| spl28_46
| spl28_53
| ~ spl28_57 ),
inference(avatar_split_clause,[],[f2587,f2521,f1892,f1541,f1198,f2877]) ).
fof(f3758,plain,
( sK17(sK22) = sK20(sK23,sK22)
| ~ spl28_42
| spl28_54
| spl28_55
| ~ spl28_57 ),
inference(forward_demodulation,[],[f1338,f2588]) ).
fof(f3763,plain,
( sK20(sK23,sK22) = sK19(sK23,sK22)
| ~ start_point(sK20(sK23,sK22),sK23)
| ~ spl28_26
| spl28_34 ),
inference(forward_subsumption_resolution,[],[f3314,f1177]) ).
fof(f3769,plain,
( sK20(sK23,sK22) = sK19(sK23,sK22)
| ~ spl28_26
| ~ spl28_30
| spl28_34 ),
inference(forward_subsumption_resolution,[],[f3763,f1199]) ).
fof(f3772,plain,
( ordered_by(sK23,sK19(sK23,sK22),sK17(sK22))
| ~ spl28_25
| ~ spl28_59 ),
inference(superposition,[],[f1162,f2879]) ).
fof(f3824,plain,
( ordered_by(sK23,sK17(sK22),sK17(sK22))
| ~ spl28_25
| ~ spl28_58
| ~ spl28_59 ),
inference(forward_demodulation,[],[f3772,f2875]) ).
fof(f3893,plain,
( $false
| ~ spl28_25
| spl28_28
| ~ spl28_58
| ~ spl28_59 ),
inference(forward_subsumption_resolution,[],[f3824,f2895]) ).
fof(f3894,plain,
( ~ spl28_25
| spl28_28
| ~ spl28_58
| ~ spl28_59 ),
inference(avatar_contradiction_clause,[],[f3893]) ).
fof(f3947,plain,
( sK17(sK22) = sK19(sK23,sK22)
| ~ spl28_26
| ~ spl28_30
| spl28_34
| ~ spl28_59 ),
inference(forward_demodulation,[],[f3769,f2879]) ).
fof(f3962,plain,
( $false
| ~ spl28_26
| ~ spl28_30
| spl28_34
| spl28_58
| ~ spl28_59 ),
inference(forward_subsumption_resolution,[],[f3947,f2874]) ).
fof(f3963,plain,
( ~ spl28_26
| ~ spl28_30
| spl28_34
| spl28_58
| ~ spl28_59 ),
inference(avatar_contradiction_clause,[],[f3962]) ).
fof(f3969,plain,
( sK24 = sK17(sK22)
| ~ spl28_42
| ~ spl28_46
| spl28_54
| spl28_55
| ~ spl28_57 ),
inference(forward_demodulation,[],[f3758,f1543]) ).
fof(f3978,plain,
( $false
| ~ spl28_42
| ~ spl28_46
| spl28_54
| spl28_55
| spl28_56
| ~ spl28_57 ),
inference(forward_subsumption_resolution,[],[f3969,f2518]) ).
fof(f3979,plain,
( ~ spl28_42
| ~ spl28_46
| spl28_54
| spl28_55
| spl28_56
| ~ spl28_57 ),
inference(avatar_contradiction_clause,[],[f3978]) ).
fof(f4012,plain,
( ~ start_point(sK24,sK23)
| sK20(sK23,sK22) = sK19(sK23,sK22)
| ~ spl28_25
| ~ spl28_46 ),
inference(forward_demodulation,[],[f3204,f1543]) ).
fof(f4019,plain,
( sK20(sK23,sK22) = sK19(sK23,sK22)
| ~ spl28_22
| ~ spl28_25
| ~ spl28_46 ),
inference(forward_subsumption_resolution,[],[f4012,f1085]) ).
fof(f4021,plain,
( sK24 = sK19(sK23,sK22)
| ~ spl28_22
| ~ spl28_25
| ~ spl28_46 ),
inference(forward_demodulation,[],[f4019,f1543]) ).
fof(f4023,plain,
( $false
| ~ spl28_22
| ~ spl28_25
| ~ spl28_46
| spl28_47 ),
inference(forward_subsumption_resolution,[],[f4021,f1546]) ).
fof(f4024,plain,
( ~ spl28_22
| ~ spl28_25
| ~ spl28_46
| spl28_47 ),
inference(avatar_contradiction_clause,[],[f4023]) ).
cnf(s1,plain,
( ~ spl28_1
| spl28_2 ),
inference(sat_conversion,[],[f310]) ).
cnf(s2,plain,
( spl28_2
| ~ spl28_3 ),
inference(sat_conversion,[],[f315]) ).
cnf(s17,plain,
( ~ spl28_22
| spl28_23 ),
inference(sat_conversion,[],[f1090]) ).
cnf(s18,plain,
( spl28_24
| spl28_25 ),
inference(sat_conversion,[],[f1163]) ).
cnf(s21,plain,
( ~ spl28_25
| spl28_26 ),
inference(sat_conversion,[],[f1192]) ).
cnf(s23,plain,
( ~ spl28_25
| ~ spl28_28 ),
inference(sat_conversion,[],[f1202]) ).
cnf(s25,plain,
( spl28_25
| spl28_29
| ~ spl28_31
| ~ spl28_32 ),
inference(sat_conversion,[],[f1214]) ).
cnf(s28,plain,
( spl28_25
| spl28_34
| spl28_36 ),
inference(sat_conversion,[],[f1244]) ).
cnf(s30,plain,
( spl28_25
| spl28_27
| ~ spl28_36 ),
inference(sat_conversion,[],[f1255]) ).
cnf(s39,plain,
( spl28_25
| ~ spl28_32
| ~ spl28_34
| spl28_46
| spl28_52 ),
inference(sat_conversion,[],[f1890]) ).
cnf(s40,plain,
( spl28_25
| ~ spl28_30
| spl28_46
| spl28_47
| spl28_53 ),
inference(sat_conversion,[],[f1895]) ).
cnf(s41,plain,
( spl28_42
| spl28_43
| ~ spl28_52
| spl28_54
| spl28_55 ),
inference(sat_conversion,[],[f1906]) ).
cnf(s42,plain,
( spl28_22
| ~ spl28_54 ),
inference(sat_conversion,[],[f1914]) ).
cnf(s45,plain,
( spl28_31
| ~ spl28_43 ),
inference(sat_conversion,[],[f1977]) ).
cnf(s46,plain,
( spl28_1
| ~ spl28_55 ),
inference(sat_conversion,[],[f1985]) ).
cnf(s47,plain,
( spl28_30
| ~ spl28_42 ),
inference(sat_conversion,[],[f2031]) ).
cnf(s48,plain,
( ~ spl28_2
| spl28_54
| ~ spl28_55 ),
inference(sat_conversion,[],[f2036]) ).
cnf(s49,plain,
( spl28_25
| ~ spl28_46
| spl28_49 ),
inference(sat_conversion,[],[f2098]) ).
cnf(s50,plain,
( spl28_25
| ~ spl28_29
| ~ spl28_43 ),
inference(sat_conversion,[],[f2122]) ).
cnf(s52,plain,
( ~ spl28_42
| ~ spl28_53
| spl28_55 ),
inference(sat_conversion,[],[f2129]) ).
cnf(s55,plain,
( ~ spl28_2
| ~ spl28_46
| spl28_53 ),
inference(sat_conversion,[],[f2133]) ).
cnf(s61,plain,
( ~ spl28_46
| ~ spl28_49 ),
inference(sat_conversion,[],[f2288]) ).
cnf(s64,plain,
( spl28_56
| spl28_57 ),
inference(sat_conversion,[],[f2523]) ).
cnf(s65,plain,
( spl28_48
| ~ spl28_56 ),
inference(sat_conversion,[],[f2530]) ).
cnf(s67,plain,
( spl28_25
| ~ spl28_42
| ~ spl28_47
| spl28_54
| spl28_55 ),
inference(sat_conversion,[],[f2657]) ).
cnf(s68,plain,
( ~ spl28_27
| spl28_42
| spl28_43
| spl28_54
| spl28_55
| ~ spl28_57 ),
inference(sat_conversion,[],[f2727]) ).
cnf(s70,plain,
( ~ spl28_48
| spl28_54
| spl28_55 ),
inference(sat_conversion,[],[f2824]) ).
cnf(s72,plain,
( spl28_25
| spl28_32 ),
inference(sat_conversion,[],[f2835]) ).
cnf(s82,plain,
( spl28_43
| ~ spl28_47
| ~ spl28_54 ),
inference(sat_conversion,[],[f2862]) ).
cnf(s85,plain,
( ~ spl28_27
| spl28_58
| spl28_59 ),
inference(sat_conversion,[],[f2880]) ).
cnf(s88,plain,
( spl28_3
| ~ spl28_23
| spl28_56 ),
inference(sat_conversion,[],[f3017]) ).
cnf(s90,plain,
( ~ spl28_2
| ~ spl28_23
| spl28_48
| spl28_56 ),
inference(sat_conversion,[],[f3025]) ).
cnf(s95,plain,
( ~ spl28_22
| ~ spl28_24
| spl28_46
| spl28_47
| ~ spl28_48 ),
inference(sat_conversion,[],[f3041]) ).
cnf(s96,plain,
( ~ spl28_25
| ~ spl28_34 ),
inference(sat_conversion,[],[f3044]) ).
cnf(s105,plain,
( ~ spl28_25
| spl28_46
| ~ spl28_49 ),
inference(sat_conversion,[],[f3177]) ).
cnf(s109,plain,
( ~ spl28_25
| spl28_69
| spl28_70 ),
inference(sat_conversion,[],[f3215]) ).
cnf(s110,plain,
( ~ spl28_25
| spl28_71
| spl28_72 ),
inference(sat_conversion,[],[f3223]) ).
cnf(s113,plain,
( ~ spl28_25
| ~ spl28_71 ),
inference(sat_conversion,[],[f3268]) ).
cnf(s117,plain,
( ~ spl28_26
| spl28_51
| ~ spl28_70
| ~ spl28_72 ),
inference(sat_conversion,[],[f3355]) ).
cnf(s121,plain,
( ~ spl28_22
| ~ spl28_26
| spl28_46
| spl28_47
| spl28_49
| ~ spl28_72 ),
inference(sat_conversion,[],[f3392]) ).
cnf(s123,plain,
( ~ spl28_47
| ~ spl28_56
| spl28_58 ),
inference(sat_conversion,[],[f3397]) ).
cnf(s133,plain,
( ~ spl28_25
| spl28_32 ),
inference(sat_conversion,[],[f3489]) ).
cnf(s134,plain,
( ~ spl28_32
| spl28_46
| ~ spl28_47
| ~ spl28_48
| spl28_71 ),
inference(sat_conversion,[],[f3491]) ).
cnf(s138,plain,
( spl28_42
| spl28_54
| spl28_55
| ~ spl28_57
| ~ spl28_59 ),
inference(sat_conversion,[],[f3494]) ).
cnf(s141,plain,
( spl28_34
| ~ spl28_47
| spl28_53
| ~ spl28_69 ),
inference(sat_conversion,[],[f3557]) ).
cnf(s145,plain,
( ~ spl28_47
| ~ spl28_53 ),
inference(sat_conversion,[],[f3624]) ).
cnf(s146,plain,
( ~ spl28_51
| spl28_54
| spl28_55
| ~ spl28_57
| spl28_58
| spl28_59 ),
inference(sat_conversion,[],[f3633]) ).
cnf(s147,plain,
( ~ spl28_26
| spl28_47
| spl28_52
| ~ spl28_72 ),
inference(sat_conversion,[],[f3636]) ).
cnf(s148,plain,
( ~ spl28_43
| spl28_54
| spl28_55
| ~ spl28_57
| spl28_58 ),
inference(sat_conversion,[],[f3640]) ).
cnf(s151,plain,
( ~ spl28_29
| ~ spl28_58
| spl28_59 ),
inference(sat_conversion,[],[f3750]) ).
cnf(s152,plain,
( ~ spl28_32
| ~ spl28_58
| spl28_59
| spl28_71 ),
inference(sat_conversion,[],[f3754]) ).
cnf(s153,plain,
( ~ spl28_30
| spl28_46
| spl28_53
| ~ spl28_57
| spl28_59 ),
inference(sat_conversion,[],[f3756]) ).
cnf(s163,plain,
( ~ spl28_25
| spl28_28
| ~ spl28_58
| ~ spl28_59 ),
inference(sat_conversion,[],[f3894]) ).
cnf(s175,plain,
( ~ spl28_26
| ~ spl28_30
| spl28_34
| spl28_58
| ~ spl28_59 ),
inference(sat_conversion,[],[f3963]) ).
cnf(s178,plain,
( ~ spl28_42
| ~ spl28_46
| spl28_54
| spl28_55
| spl28_56
| ~ spl28_57 ),
inference(sat_conversion,[],[f3979]) ).
cnf(s190,plain,
( ~ spl28_22
| ~ spl28_25
| ~ spl28_46
| spl28_47 ),
inference(sat_conversion,[],[f4024]) ).
cnf(s200,plain,
( spl28_42
| ~ spl28_25
| spl28_54
| spl28_55 ),
inference(rat,[],[s141,s145,s109,s147,s117,s41,s146,s148,s152,s138,s64,s65,s70,s133,s96,s21,s110,s113]) ).
cnf(s201,plain,
( ~ spl28_25
| spl28_54
| spl28_55 ),
inference(rat,[],[s163,s175,s153,s178,s47,s52,s200,s21,s23,s96,s64,s65,s70]) ).
cnf(s202,plain,
( ~ spl28_27
| spl28_42
| spl28_54
| spl28_55 ),
inference(rat,[],[s25,s45,s151,s68,s85,s72,s201,s138,s64,s65,s70]) ).
cnf(s203,plain,
( ~ spl28_46
| spl28_25 ),
inference(rat,[],[s49,s61]) ).
cnf(s204,plain,
( ~ spl28_43
| spl28_25 ),
inference(rat,[],[s25,s50,s45,s72]) ).
cnf(s205,plain,
( ~ spl28_42
| spl28_54
| spl28_55 ),
inference(rat,[],[s40,s67,s47,s52,s203,s201]) ).
cnf(s206,plain,
( spl28_54
| spl28_55 ),
inference(rat,[],[s28,s39,s30,s41,s202,s205,s204,s203,s72,s201]) ).
cnf(s207,plain,
( spl28_25
| ~ spl28_48
| ~ spl28_54 ),
inference(rat,[],[s82,s95,s204,s203,s18,s42]) ).
cnf(s208,plain,
( spl28_47
| ~ spl28_25
| ~ spl28_22 ),
inference(rat,[],[s121,s105,s190,s21,s110,s113]) ).
cnf(s209,plain,
( ~ spl28_56
| ~ spl28_54 ),
inference(rat,[],[s163,s152,s123,s208,s23,s113,s133,s207,s65,s42]) ).
cnf(s210,plain,
~ spl28_54,
inference(rat,[],[s55,s134,s145,s208,s113,s133,s207,s90,s2,s88,s209,s17,s42]) ).
cnf(s211,plain,
spl28_55,
inference(rat,[],[s206,s210]) ).
cnf(s212,plain,
spl28_1,
inference(rat,[],[s46,s211]) ).
cnf(s213,plain,
~ spl28_2,
inference(rat,[],[s48,s210,s211]) ).
cnf(s214,plain,
$false,
inference(rat,[],[s1,s213,s212]) ).
fof(f4027,plain,
$false,
inference(avatar_sat_refutation,[],[s214]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GEO138+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/10.44 % Computer : n020.cluster.edu
% 0.17/10.44 % Model : x86_64 x86_64
% 0.17/10.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/10.44 % Memory : 8046.5625MB
% 0.17/10.44 % OS : Linux 6.8.0-71-generic
% 0.17/10.44 % CPULimit : 300
% 0.17/10.44 % WCLimit : 300
% 0.17/10.44 % DateTime : Sun Sep 27 07:14:00 UTC 2026
% 0.17/10.44 % CPUTime :
% 0.17/10.44 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/10.49 Running first-order theorem proving
% 0.17/10.49 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.89/13.09 % (3062797)Detected formulas, will run a generic FOF schedule.
% 14.89/13.09 % (3062807)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=88749809:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 14.89/13.09 % (3062807)Refutation not found, incomplete strategy
% 14.89/13.09 % (3062807)------------------------------
% 14.89/13.09 % (3062807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.89/13.09 % (3062807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.89/13.09 % (3062807)CaDiCaL version: 2.1.3
% 14.89/13.09 % (3062807)Termination reason: Refutation not found, incomplete strategy
% 14.89/13.09 % (3062807)Time elapsed: 0.001 s
% 14.89/13.09 % (3062807)Peak memory usage: 88 MB
% 14.89/13.09 % (3062807)Instructions burned: 1 (million)
% 14.89/13.09 % (3062808)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1803332912:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 14.89/13.09 % (3062808)Refutation not found, incomplete strategy
% 14.89/13.09 % (3062808)------------------------------
% 14.89/13.09 % (3062808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.89/13.09 % (3062808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.89/13.09 % (3062808)CaDiCaL version: 2.1.3
% 14.89/13.09 % (3062808)Termination reason: Refutation not found, incomplete strategy
% 14.89/13.09 % (3062808)Time elapsed: 0.006 s
% 14.89/13.09 % (3062808)Peak memory usage: 88 MB
% 14.89/13.09 % (3062808)Instructions burned: 3 (million)
% 14.89/13.09 % (3062806)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3960720924:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 14.89/13.09 % (3062804)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=3442898232:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 14.89/13.09 % (3062805)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3940287941:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 14.89/13.09 % (3062809)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3707339972:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 14.89/13.09 % (3062810)dis-21_1_sil=8000:lcm=predicate:random_seed=835693011:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 14.89/13.09 % (3062810)Instruction limit reached!
% 14.89/13.09 % (3062810)------------------------------
% 14.89/13.09 % (3062810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.89/13.09 % (3062810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.89/13.09 % (3062810)CaDiCaL version: 2.1.3
% 14.89/13.09 % (3062810)Termination reason: Instruction limit
% 14.89/13.09 % (3062810)Termination phase: Saturation
% 14.89/13.09 % (3062810)Time elapsed: 0.127 s
% 14.89/13.09 % (3062810)Peak memory usage: 88 MB
% 14.89/13.09 % (3062810)Instructions burned: 129 (million)
% 14.89/13.09 % (3062807)------------------------------
% 14.89/13.09 % (3062807)------------------------------
% 14.89/13.09 % (3062809)Instruction limit reached!
% 14.89/13.09 % (3062809)------------------------------
% 14.89/13.09 % (3062809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.89/13.09 % (3062809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.89/13.09 % (3062809)CaDiCaL version: 2.1.3
% 14.89/13.09 % (3062809)Termination reason: Instruction limit
% 14.89/13.09 % (3062809)Termination phase: Saturation
% 14.89/13.09 % (3062809)Time elapsed: 0.147 s
% 14.89/13.09 % (3062809)Peak memory usage: 89 MB
% 14.89/13.09 % (3062809)Instructions burned: 140 (million)
% 14.89/13.09 % (3062820)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3442165618:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 14.89/13.09 % (3062819)lrs+10_1_sil=8000:sp=occurrence:random_seed=678238076:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 14.89/13.09 % (3062820)Refutation not found, incomplete strategy
% 14.89/13.09 % (3062820)------------------------------
% 14.89/13.09 % (3062820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.89/13.09 % (3062820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.89/13.09 % (3062820)CaDiCaL version: 2.1.3
% 14.89/13.09 % (3062820)Termination reason: Refutation not found, incomplete strategy
% 14.89/13.09 % (3062820)Time elapsed: 0.002 s
% 14.89/13.09 % (3062820)Peak memory usage: 89 MB
% 14.89/13.09 % (3062820)Instructions burned: 1 (million)
% 14.89/13.09 % (3062808)------------------------------
% 14.89/13.09 % (3062808)------------------------------
% 14.89/13.09 % (3062821)lrs+1011_1_sil=32000:sp=occurrence:random_seed=137113138:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 14.89/13.09 % (3062820)------------------------------
% 14.89/13.09 % (3062820)------------------------------
% 14.89/13.09 % (3062824)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2632968914:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 14.89/13.09 % (3062819)Instruction limit reached!
% 14.89/13.09 % (3062819)------------------------------
% 14.89/13.09 % (3062819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.89/13.09 % (3062819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.89/13.09 % (3062819)CaDiCaL version: 2.1.3
% 14.89/13.09 % (3062819)Termination reason: Instruction limit
% 14.89/13.09 % (3062819)Termination phase: Saturation
% 14.89/13.09 % (3062819)Time elapsed: 0.287 s
% 14.89/13.09 % (3062819)Peak memory usage: 91 MB
% 14.89/13.09 % (3062819)Instructions burned: 285 (million)
% 14.89/13.09 % (3062826)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=403218198:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 14.89/13.09 % (3062821)Instruction limit reached!
% 14.89/13.09 % (3062821)------------------------------
% 14.89/13.09 % (3062821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.89/13.09 % (3062821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.89/13.09 % (3062821)CaDiCaL version: 2.1.3
% 14.89/13.09 % (3062821)Termination reason: Instruction limit
% 14.89/13.09 % (3062821)Termination phase: Saturation
% 14.89/13.09 % (3062821)Time elapsed: 0.345 s
% 14.89/13.09 % (3062821)Peak memory usage: 91 MB
% 14.89/13.09 % (3062821)Instructions burned: 325 (million)
% 14.89/13.09 % (3062824)Instruction limit reached!
% 14.89/13.09 % (3062824)------------------------------
% 14.89/13.09 % (3062824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.89/13.09 % (3062824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.89/13.09 % (3062824)CaDiCaL version: 2.1.3
% 14.89/13.09 % (3062824)Termination reason: Instruction limit
% 14.89/13.09 % (3062824)Termination phase: Saturation
% 14.89/13.09 % (3062824)Time elapsed: 0.232 s
% 14.89/13.09 % (3062824)Peak memory usage: 90 MB
% 14.89/13.09 % (3062824)Instructions burned: 248 (million)
% 14.89/13.09 % (3062828)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3171168605:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 14.89/13.09 % (3062826)Instruction limit reached!
% 14.89/13.09 % (3062826)------------------------------
% 14.89/13.09 % (3062826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.89/13.09 % (3062826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.89/13.09 % (3062826)CaDiCaL version: 2.1.3
% 14.89/13.09 % (3062826)Termination reason: Instruction limit
% 14.89/13.09 % (3062826)Termination phase: Saturation
% 14.89/13.09 % (3062826)Time elapsed: 0.162 s
% 14.89/13.09 % (3062826)Peak memory usage: 90 MB
% 14.89/13.09 % (3062826)Instructions burned: 294 (million)
% 14.89/13.09 % (3062830)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3478398775:cts=off:i=113:fsr=off:ss=included:sgt=4_2989 on theBenchmark for (2989ds/113Mi)
% 14.89/13.09 % (3062831)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2557739405:i=127:av=off:fsr=off:sup=off_2988 on theBenchmark for (2988ds/127Mi)
% 14.89/13.09 % (3062833)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4052670660:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 14.89/13.09 % (3062833)Instruction limit reached!
% 14.89/13.09 % (3062833)------------------------------
% 14.89/13.09 % (3062833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.89/13.09 % (3062833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.89/13.09 % (3062833)CaDiCaL version: 2.1.3
% 14.89/13.09 % (3062833)Termination reason: Instruction limit
% 14.89/13.09 % (3062833)Termination phase: Saturation
% 14.89/13.09 % (3062833)Time elapsed: 0.058 s
% 14.89/13.09 % (3062833)Peak memory usage: 88 MB
% 14.89/13.09 % (3062833)Instructions burned: 115 (million)
% 14.89/13.09 % (3062830)Instruction limit reached!
% 14.89/13.09 % (3062830)------------------------------
% 14.89/13.09 % (3062830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.89/13.09 % (3062830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.89/13.09 % (3062830)CaDiCaL version: 2.1.3
% 14.89/13.09 % (3062830)Termination reason: Instruction limit
% 14.89/13.09 % (3062830)Termination phase: Saturation
% 14.89/13.09 % (3062830)Time elapsed: 0.131 s
% 14.89/13.09 % (3062830)Peak memory usage: 89 MB
% 14.89/13.09 % (3062830)Instructions burned: 114 (million)
% 14.89/13.09 % (3062831)Instruction limit reached!
% 14.89/13.09 % (3062831)------------------------------
% 14.89/13.09 % (3062831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.89/13.09 % (3062831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.89/13.09 % (3062831)CaDiCaL version: 2.1.3
% 14.89/13.09 % (3062831)Termination reason: Instruction limit
% 14.89/13.09 % (3062831)Termination phase: Saturation
% 14.89/13.09 % (3062831)Time elapsed: 0.114 s
% 14.89/13.09 % (3062831)Peak memory usage: 89 MB
% 14.89/13.09 % (3062831)Instructions burned: 127 (million)
% 14.89/13.09 % (3062837)lrs+10_1_sil=8000:sp=occurrence:random_seed=983655772:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 14.89/13.09 % (3062838)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1411818691:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 14.89/13.09 % (3062838)Refutation not found, incomplete strategy
% 14.89/13.09 % (3062838)------------------------------
% 14.89/13.09 % (3062838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.89/13.09 % (3062838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.89/13.09 % (3062838)CaDiCaL version: 2.1.3
% 14.89/13.09 % (3062838)Termination reason: Refutation not found, incomplete strategy
% 14.89/13.09 % (3062838)Time elapsed: 0.002 s
% 14.89/13.09 % (3062838)Peak memory usage: 88 MB
% 14.89/13.09 % (3062838)Instructions burned: 1 (million)
% 14.89/13.09 % (3062839)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1616096715:i=5202:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/5202Mi)
% 14.89/13.09 % (3062804)First to succeed.
% 14.89/13.09 % (3062804)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3062797"
% 14.89/13.09 % (3062838)------------------------------
% 14.89/13.09 % (3062838)------------------------------
% 14.89/13.09 % (3062837)Instruction limit reached!
% 14.89/13.09 % (3062837)------------------------------
% 14.89/13.09 % (3062837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.89/13.09 % (3062837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.89/13.09 % (3062837)CaDiCaL version: 2.1.3
% 14.89/13.09 % (3062837)Termination reason: Instruction limit
% 14.89/13.09 % (3062837)Termination phase: Saturation
% 14.89/13.09 % (3062837)Time elapsed: 0.284 s
% 14.89/13.09 % (3062837)Peak memory usage: 95 MB
% 14.89/13.09 % (3062837)Instructions burned: 908 (million)
% 14.89/13.09 % (3062804)Refutation found. Thanks to Tanya!
% 14.89/13.09 % SZS status Theorem for theBenchmark
% 14.89/13.09 % SZS output start Proof for theBenchmark
% See solution above
% 15.35/13.19 % (3062804)------------------------------
% 15.35/13.19 % (3062804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.35/13.19 % (3062804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.35/13.19 % (3062804)CaDiCaL version: 2.1.3
% 15.35/13.19 % (3062804)Termination reason: Refutation
% 15.35/13.19 % (3062804)Time elapsed: 1.529 s
% 15.35/13.19 % (3062804)Peak memory usage: 133 MB
% 15.35/13.19 % (3062804)Instructions burned: 1443 (million)
% 15.35/13.19 % (3062804)------------------------------
% 15.35/13.19 % (3062804)------------------------------
% 15.35/13.19 % (3062797)Success in time 2.079 s
% 15.35/13.19 % Vampire exiting
%------------------------------------------------------------------------------