%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL652+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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 11:59:25 AM UTC 2026
% Result : Theorem 58.66s 8.92s
% Output : Refutation 58.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 43
% Syntax : Number of formulae : 244 ( 26 unt; 42 def)
% Number of atoms : 2482 ( 0 equ)
% Maximal formula atoms : 186 ( 10 avg)
% Number of connectives : 4461 (2223 ~;1721 |; 503 &)
% ( 14 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 57 ( 7 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 48 ( 47 usr; 15 prp; 0-2 aty)
% Number of functors : 43 ( 43 usr; 21 con; 0-1 aty)
% Number of variables : 1476 ( 0 sgn1245 !; 231 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p4(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p3(X0) )
| ~ p2(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ! [X0] :
( ~ r1(X1,X0)
| p3(X0) )
| ~ p2(X1) ) )
& p2(X0)
& ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p2(X1) ) ) ) ) )
| ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ p2(X0) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p2(X1) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p2(X0) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p3(X0) )
| ~ p2(X1) ) ) ) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ p2(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p2(X1) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
& ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
& ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
& ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
& ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
& ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',main) ).
fof(f2,negated_conjecture,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p4(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p3(X0) )
| ~ p2(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ! [X0] :
( ~ r1(X1,X0)
| p3(X0) )
| ~ p2(X1) ) )
& p2(X0)
& ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p2(X1) ) ) ) ) )
| ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ p2(X0) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p2(X1) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p2(X0) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p3(X0) )
| ~ p2(X1) ) ) ) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ p2(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p2(X1) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
& ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
& ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
& ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
& ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
& ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p4(X1) )
| ~ ! [X2] :
( ~ r1(X0,X2)
| ~ ( ~ ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ~ ! [X5] :
( ~ r1(X4,X5)
| ~ p1(X5) ) ) )
& ! [X6] :
( ~ r1(X2,X6)
| ~ ! [X7] :
( ~ r1(X6,X7)
| ~ p1(X7) ) ) ) )
| ~ ! [X8] :
( ~ r1(X0,X8)
| ~ ( ~ ! [X9] :
( ~ r1(X8,X9)
| ~ ( ~ ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ~ ! [X12] :
( ~ r1(X11,X12)
| ~ p1(X12) ) ) )
& ! [X13] :
( ~ r1(X9,X13)
| ~ ! [X14] :
( ~ r1(X13,X14)
| ~ p1(X14) ) ) ) )
| ~ ! [X15] :
( ~ r1(X8,X15)
| ~ ( ~ ! [X16] :
( ~ r1(X15,X16)
| ~ ( ~ ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ~ ! [X19] :
( ~ r1(X18,X19)
| ~ p1(X19) ) ) )
& ! [X20] :
( ~ r1(X16,X20)
| ~ ! [X21] :
( ~ r1(X20,X21)
| ~ p1(X21) ) ) ) )
| ~ ! [X22] :
( ~ r1(X15,X22)
| ~ ( ~ ! [X23] :
( ~ r1(X22,X23)
| ~ ( ~ ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ~ ! [X26] :
( ~ r1(X25,X26)
| ~ p1(X26) ) ) )
& ! [X27] :
( ~ r1(X23,X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| ~ p1(X28) ) ) ) )
| ~ ! [X29] :
( ~ r1(X22,X29)
| ~ ( ~ ! [X30] :
( ~ r1(X29,X30)
| ~ ( ~ ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| ~ ! [X33] :
( ~ r1(X32,X33)
| ~ p1(X33) ) ) )
& ! [X34] :
( ~ r1(X30,X34)
| ~ ! [X35] :
( ~ r1(X34,X35)
| ~ p1(X35) ) ) ) )
| ~ ! [X36] :
( ~ r1(X29,X36)
| ~ ( ~ ! [X37] :
( ~ r1(X36,X37)
| ~ ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| p3(X39) )
| ~ p2(X38) ) )
| ~ ! [X40] :
( ~ r1(X36,X40)
| ~ ( ~ ! [X41] :
( ~ r1(X40,X41)
| ~ ( ! [X42] :
( ~ r1(X41,X42)
| p3(X42) )
| ~ p2(X41) ) )
& p2(X40)
& ~ ! [X43] :
( ~ r1(X40,X43)
| ~ ! [X44] :
( ~ r1(X43,X44)
| ~ ! [X45] :
( ~ r1(X44,X45)
| ~ p2(X45) ) ) ) ) )
| ( ~ ! [X46] :
( ~ r1(X36,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ~ ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p3(X49) )
| ~ p2(X48) ) ) )
& ! [X50] :
( ~ r1(X36,X50)
| ~ ! [X51] :
( ~ r1(X50,X51)
| ~ p2(X51) ) ) )
| ~ ! [X52] :
( ~ r1(X36,X52)
| ~ ( ! [X53] :
( ~ r1(X52,X53)
| ~ ! [X54] :
( ~ r1(X53,X54)
| ~ p2(X54) ) )
& ! [X55] :
( ~ r1(X52,X55)
| ~ ! [X56] :
( ~ r1(X55,X56)
| ~ ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p3(X58) )
| ~ p2(X57) ) ) ) ) )
| ( ! [X59] :
( ~ r1(X36,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p3(X60) )
| ~ p2(X59) )
& ! [X61] :
( ~ r1(X36,X61)
| ~ ! [X62] :
( ~ r1(X61,X62)
| ~ p2(X62) ) ) ) ) )
| ~ ! [X63] :
( ~ r1(X29,X63)
| ~ ( ~ ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| p1(X65) ) )
& ! [X66] :
( ~ r1(X63,X66)
| p1(X66) ) ) ) ) )
| ~ ! [X67] :
( ~ r1(X22,X67)
| ~ ( ~ ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| p1(X69) ) )
& ! [X70] :
( ~ r1(X67,X70)
| p1(X70) ) ) ) ) )
| ~ ! [X71] :
( ~ r1(X15,X71)
| ~ ( ~ ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| p1(X73) ) )
& ! [X74] :
( ~ r1(X71,X74)
| p1(X74) ) ) ) ) )
| ~ ! [X75] :
( ~ r1(X8,X75)
| ~ ( ~ ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| p1(X77) ) )
& ! [X78] :
( ~ r1(X75,X78)
| p1(X78) ) ) ) ) )
| ~ ! [X79] :
( ~ r1(X0,X79)
| ~ ( ~ ! [X80] :
( ~ r1(X79,X80)
| ! [X81] :
( ~ r1(X80,X81)
| p1(X81) ) )
& ! [X82] :
( ~ r1(X79,X82)
| p1(X82) ) ) )
| ! [X83] :
( ~ r1(X0,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ~ ! [X85] :
( ~ r1(X84,X85)
| p1(X85) ) )
| ! [X86] :
( ~ r1(X83,X86)
| p1(X86) ) )
| ! [X87] :
( ~ r1(X0,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ~ ! [X90] :
( ~ r1(X89,X90)
| p1(X90) ) )
| ! [X91] :
( ~ r1(X88,X91)
| p1(X91) ) )
| ! [X92] :
( ~ r1(X87,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ~ ! [X95] :
( ~ r1(X94,X95)
| p1(X95) ) )
| ! [X96] :
( ~ r1(X93,X96)
| p1(X96) ) )
| ! [X97] :
( ~ r1(X92,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ~ ! [X100] :
( ~ r1(X99,X100)
| p1(X100) ) )
| ! [X101] :
( ~ r1(X98,X101)
| p1(X101) ) )
| ! [X102] :
( ~ r1(X97,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ! [X104] :
( ~ r1(X103,X104)
| ~ ! [X105] :
( ~ r1(X104,X105)
| p1(X105) ) )
| ! [X106] :
( ~ r1(X103,X106)
| p1(X106) ) )
| ! [X107] :
( ~ r1(X102,X107)
| ~ ! [X108] :
( ~ r1(X107,X108)
| ~ ! [X109] :
( ~ r1(X108,X109)
| p2(X109) ) ) )
| ~ ! [X110] :
( ~ r1(X102,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ~ p1(X112) ) )
| ~ ! [X113] :
( ~ r1(X110,X113)
| ~ p1(X113) ) ) )
| ~ ! [X114] :
( ~ r1(X97,X114)
| ! [X115] :
( ~ r1(X114,X115)
| ! [X116] :
( ~ r1(X115,X116)
| ~ p1(X116) ) )
| ~ ! [X117] :
( ~ r1(X114,X117)
| ~ p1(X117) ) ) )
| ~ ! [X118] :
( ~ r1(X92,X118)
| ! [X119] :
( ~ r1(X118,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ~ p1(X120) ) )
| ~ ! [X121] :
( ~ r1(X118,X121)
| ~ p1(X121) ) ) )
| ~ ! [X122] :
( ~ r1(X87,X122)
| ! [X123] :
( ~ r1(X122,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ~ p1(X124) ) )
| ~ ! [X125] :
( ~ r1(X122,X125)
| ~ p1(X125) ) ) )
| ~ ! [X126] :
( ~ r1(X0,X126)
| ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ~ p1(X128) ) )
| ~ ! [X129] :
( ~ r1(X126,X129)
| ~ p1(X129) ) ) ),
inference(rectify,[],[f2]) ).
fof(f4,plain,
? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p4(X1) )
| ~ ! [X2] :
( ~ r1(X0,X2)
| ~ ( ~ ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ~ ! [X5] :
( ~ r1(X4,X5)
| ~ p1(X5) ) ) )
& ! [X6] :
( ~ r1(X2,X6)
| ~ ! [X7] :
( ~ r1(X6,X7)
| ~ p1(X7) ) ) ) )
| ~ ! [X8] :
( ~ r1(X0,X8)
| ~ ( ~ ! [X9] :
( ~ r1(X8,X9)
| ~ ( ~ ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ~ ! [X12] :
( ~ r1(X11,X12)
| ~ p1(X12) ) ) )
& ! [X13] :
( ~ r1(X9,X13)
| ~ ! [X14] :
( ~ r1(X13,X14)
| ~ p1(X14) ) ) ) )
| ~ ! [X15] :
( ~ r1(X8,X15)
| ~ ( ~ ! [X16] :
( ~ r1(X15,X16)
| ~ ( ~ ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ~ ! [X19] :
( ~ r1(X18,X19)
| ~ p1(X19) ) ) )
& ! [X20] :
( ~ r1(X16,X20)
| ~ ! [X21] :
( ~ r1(X20,X21)
| ~ p1(X21) ) ) ) )
| ~ ! [X22] :
( ~ r1(X15,X22)
| ~ ( ~ ! [X23] :
( ~ r1(X22,X23)
| ~ ( ~ ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ~ ! [X26] :
( ~ r1(X25,X26)
| ~ p1(X26) ) ) )
& ! [X27] :
( ~ r1(X23,X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| ~ p1(X28) ) ) ) )
| ~ ! [X29] :
( ~ r1(X22,X29)
| ~ ( ~ ! [X30] :
( ~ r1(X29,X30)
| ~ ( ~ ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| ~ ! [X33] :
( ~ r1(X32,X33)
| ~ p1(X33) ) ) )
& ! [X34] :
( ~ r1(X30,X34)
| ~ ! [X35] :
( ~ r1(X34,X35)
| ~ p1(X35) ) ) ) )
| ~ ! [X36] :
( ~ r1(X29,X36)
| ~ ( ~ ! [X37] :
( ~ r1(X36,X37)
| ~ ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| p3(X39) )
| ~ p2(X38) ) )
| ~ ! [X40] :
( ~ r1(X36,X40)
| ~ ( ~ ! [X41] :
( ~ r1(X40,X41)
| ~ ( ! [X42] :
( ~ r1(X41,X42)
| p3(X42) )
| ~ p2(X41) ) )
& p2(X40)
& ~ ! [X43] :
( ~ r1(X40,X43)
| ~ ! [X44] :
( ~ r1(X43,X44)
| ~ ! [X45] :
( ~ r1(X44,X45)
| ~ p2(X45) ) ) ) ) )
| ( ~ ! [X46] :
( ~ r1(X36,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ~ ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p3(X49) )
| ~ p2(X48) ) ) )
& ! [X50] :
( ~ r1(X36,X50)
| ~ ! [X51] :
( ~ r1(X50,X51)
| ~ p2(X51) ) ) )
| ~ ! [X52] :
( ~ r1(X36,X52)
| ~ ( ! [X53] :
( ~ r1(X52,X53)
| ~ ! [X54] :
( ~ r1(X53,X54)
| ~ p2(X54) ) )
& ! [X55] :
( ~ r1(X52,X55)
| ~ ! [X56] :
( ~ r1(X55,X56)
| ~ ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p3(X58) )
| ~ p2(X57) ) ) ) ) )
| ( ! [X59] :
( ~ r1(X36,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p3(X60) )
| ~ p2(X59) )
& ! [X61] :
( ~ r1(X36,X61)
| ~ ! [X62] :
( ~ r1(X61,X62)
| ~ p2(X62) ) ) ) ) )
| ~ ! [X63] :
( ~ r1(X29,X63)
| ~ ( ~ ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| p1(X65) ) )
& ! [X66] :
( ~ r1(X63,X66)
| p1(X66) ) ) ) ) )
| ~ ! [X67] :
( ~ r1(X22,X67)
| ~ ( ~ ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| p1(X69) ) )
& ! [X70] :
( ~ r1(X67,X70)
| p1(X70) ) ) ) ) )
| ~ ! [X71] :
( ~ r1(X15,X71)
| ~ ( ~ ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| p1(X73) ) )
& ! [X74] :
( ~ r1(X71,X74)
| p1(X74) ) ) ) ) )
| ~ ! [X75] :
( ~ r1(X8,X75)
| ~ ( ~ ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| p1(X77) ) )
& ! [X78] :
( ~ r1(X75,X78)
| p1(X78) ) ) ) ) )
| ~ ! [X79] :
( ~ r1(X0,X79)
| ~ ( ~ ! [X80] :
( ~ r1(X79,X80)
| ! [X81] :
( ~ r1(X80,X81)
| p1(X81) ) )
& ! [X82] :
( ~ r1(X79,X82)
| p1(X82) ) ) )
| ! [X83] :
( ~ r1(X0,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ~ ! [X85] :
( ~ r1(X84,X85)
| p1(X85) ) )
| ! [X86] :
( ~ r1(X83,X86)
| p1(X86) ) )
| ! [X87] :
( ~ r1(X0,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ~ ! [X90] :
( ~ r1(X89,X90)
| p1(X90) ) )
| ! [X91] :
( ~ r1(X88,X91)
| p1(X91) ) )
| ! [X92] :
( ~ r1(X87,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ~ ! [X95] :
( ~ r1(X94,X95)
| p1(X95) ) )
| ! [X96] :
( ~ r1(X93,X96)
| p1(X96) ) )
| ! [X97] :
( ~ r1(X92,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ~ ! [X100] :
( ~ r1(X99,X100)
| p1(X100) ) )
| ! [X101] :
( ~ r1(X98,X101)
| p1(X101) ) )
| ! [X102] :
( ~ r1(X97,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ! [X104] :
( ~ r1(X103,X104)
| ~ ! [X105] :
( ~ r1(X104,X105)
| p1(X105) ) )
| ! [X106] :
( ~ r1(X103,X106)
| p1(X106) ) )
| ! [X107] :
( ~ r1(X102,X107)
| ~ ! [X108] :
( ~ r1(X107,X108)
| ~ ! [X109] :
( ~ r1(X108,X109)
| p2(X109) ) ) )
| ~ ! [X110] :
( ~ r1(X102,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ~ p1(X112) ) )
| ~ ! [X113] :
( ~ r1(X110,X113)
| ~ p1(X113) ) ) )
| ~ ! [X114] :
( ~ r1(X97,X114)
| ! [X115] :
( ~ r1(X114,X115)
| ! [X116] :
( ~ r1(X115,X116)
| ~ p1(X116) ) )
| ~ ! [X117] :
( ~ r1(X114,X117)
| ~ p1(X117) ) ) )
| ~ ! [X118] :
( ~ r1(X92,X118)
| ! [X119] :
( ~ r1(X118,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ~ p1(X120) ) )
| ~ ! [X121] :
( ~ r1(X118,X121)
| ~ p1(X121) ) ) )
| ~ ! [X122] :
( ~ r1(X87,X122)
| ! [X123] :
( ~ r1(X122,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ~ p1(X124) ) )
| ~ ! [X125] :
( ~ r1(X122,X125)
| ~ p1(X125) ) ) )
| ~ ! [X126] :
( ~ r1(X0,X126)
| ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ~ p1(X128) ) )
| ~ ! [X129] :
( ~ r1(X126,X129)
| ~ p1(X129) ) ) ),
inference(flattening,[],[f3]) ).
fof(f5,plain,
? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p4(X1) )
| ~ ! [X2] :
( ~ r1(X0,X2)
| ~ ( ~ ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ~ ! [X5] :
( ~ r1(X4,X5)
| ~ p1(X5) ) ) )
& ! [X6] :
( ~ r1(X2,X6)
| ~ ! [X7] :
( ~ r1(X6,X7)
| ~ p1(X7) ) ) ) )
| ~ ! [X8] :
( ~ r1(X0,X8)
| ~ ( ~ ! [X9] :
( ~ r1(X8,X9)
| ~ ( ~ ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ~ ! [X12] :
( ~ r1(X11,X12)
| ~ p1(X12) ) ) )
& ! [X13] :
( ~ r1(X9,X13)
| ~ ! [X14] :
( ~ r1(X13,X14)
| ~ p1(X14) ) ) ) )
| ~ ! [X15] :
( ~ r1(X8,X15)
| ~ ( ~ ! [X16] :
( ~ r1(X15,X16)
| ~ ( ~ ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ~ ! [X19] :
( ~ r1(X18,X19)
| ~ p1(X19) ) ) )
& ! [X20] :
( ~ r1(X16,X20)
| ~ ! [X21] :
( ~ r1(X20,X21)
| ~ p1(X21) ) ) ) )
| ~ ! [X22] :
( ~ r1(X15,X22)
| ~ ( ~ ! [X23] :
( ~ r1(X22,X23)
| ~ ( ~ ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ~ ! [X26] :
( ~ r1(X25,X26)
| ~ p1(X26) ) ) )
& ! [X27] :
( ~ r1(X23,X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| ~ p1(X28) ) ) ) )
| ~ ! [X29] :
( ~ r1(X22,X29)
| ~ ( ~ ! [X30] :
( ~ r1(X29,X30)
| ~ ( ~ ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| ~ ! [X33] :
( ~ r1(X32,X33)
| ~ p1(X33) ) ) )
& ! [X34] :
( ~ r1(X30,X34)
| ~ ! [X35] :
( ~ r1(X34,X35)
| ~ p1(X35) ) ) ) )
| ~ ! [X36] :
( ~ r1(X29,X36)
| ~ ( ~ ! [X37] :
( ~ r1(X36,X37)
| ~ ! [X38] :
( ~ r1(X37,X38)
| ! [X39] : ~ r1(X38,X39)
| ~ p2(X38) ) )
| ~ ! [X40] :
( ~ r1(X36,X40)
| ~ ( ~ ! [X41] :
( ~ r1(X40,X41)
| ~ ( ! [X42] : ~ r1(X41,X42)
| ~ p2(X41) ) )
& p2(X40)
& ~ ! [X43] :
( ~ r1(X40,X43)
| ~ ! [X44] :
( ~ r1(X43,X44)
| ~ ! [X45] :
( ~ r1(X44,X45)
| ~ p2(X45) ) ) ) ) )
| ( ~ ! [X46] :
( ~ r1(X36,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ~ ! [X48] :
( ~ r1(X47,X48)
| ! [X49] : ~ r1(X48,X49)
| ~ p2(X48) ) ) )
& ! [X50] :
( ~ r1(X36,X50)
| ~ ! [X51] :
( ~ r1(X50,X51)
| ~ p2(X51) ) ) )
| ~ ! [X52] :
( ~ r1(X36,X52)
| ~ ( ! [X53] :
( ~ r1(X52,X53)
| ~ ! [X54] :
( ~ r1(X53,X54)
| ~ p2(X54) ) )
& ! [X55] :
( ~ r1(X52,X55)
| ~ ! [X56] :
( ~ r1(X55,X56)
| ~ ! [X57] :
( ~ r1(X56,X57)
| ! [X58] : ~ r1(X57,X58)
| ~ p2(X57) ) ) ) ) )
| ( ! [X59] :
( ~ r1(X36,X59)
| ! [X60] : ~ r1(X59,X60)
| ~ p2(X59) )
& ! [X61] :
( ~ r1(X36,X61)
| ~ ! [X62] :
( ~ r1(X61,X62)
| ~ p2(X62) ) ) ) ) )
| ~ ! [X63] :
( ~ r1(X29,X63)
| ~ ( ~ ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| p1(X65) ) )
& ! [X66] :
( ~ r1(X63,X66)
| p1(X66) ) ) ) ) )
| ~ ! [X67] :
( ~ r1(X22,X67)
| ~ ( ~ ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| p1(X69) ) )
& ! [X70] :
( ~ r1(X67,X70)
| p1(X70) ) ) ) ) )
| ~ ! [X71] :
( ~ r1(X15,X71)
| ~ ( ~ ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| p1(X73) ) )
& ! [X74] :
( ~ r1(X71,X74)
| p1(X74) ) ) ) ) )
| ~ ! [X75] :
( ~ r1(X8,X75)
| ~ ( ~ ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| p1(X77) ) )
& ! [X78] :
( ~ r1(X75,X78)
| p1(X78) ) ) ) ) )
| ~ ! [X79] :
( ~ r1(X0,X79)
| ~ ( ~ ! [X80] :
( ~ r1(X79,X80)
| ! [X81] :
( ~ r1(X80,X81)
| p1(X81) ) )
& ! [X82] :
( ~ r1(X79,X82)
| p1(X82) ) ) )
| ! [X83] :
( ~ r1(X0,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ~ ! [X85] :
( ~ r1(X84,X85)
| p1(X85) ) )
| ! [X86] :
( ~ r1(X83,X86)
| p1(X86) ) )
| ! [X87] :
( ~ r1(X0,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ~ ! [X90] :
( ~ r1(X89,X90)
| p1(X90) ) )
| ! [X91] :
( ~ r1(X88,X91)
| p1(X91) ) )
| ! [X92] :
( ~ r1(X87,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ~ ! [X95] :
( ~ r1(X94,X95)
| p1(X95) ) )
| ! [X96] :
( ~ r1(X93,X96)
| p1(X96) ) )
| ! [X97] :
( ~ r1(X92,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ~ ! [X100] :
( ~ r1(X99,X100)
| p1(X100) ) )
| ! [X101] :
( ~ r1(X98,X101)
| p1(X101) ) )
| ! [X102] :
( ~ r1(X97,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ! [X104] :
( ~ r1(X103,X104)
| ~ ! [X105] :
( ~ r1(X104,X105)
| p1(X105) ) )
| ! [X106] :
( ~ r1(X103,X106)
| p1(X106) ) )
| ! [X107] :
( ~ r1(X102,X107)
| ~ ! [X108] :
( ~ r1(X107,X108)
| ~ ! [X109] :
( ~ r1(X108,X109)
| p2(X109) ) ) )
| ~ ! [X110] :
( ~ r1(X102,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ~ p1(X112) ) )
| ~ ! [X113] :
( ~ r1(X110,X113)
| ~ p1(X113) ) ) )
| ~ ! [X114] :
( ~ r1(X97,X114)
| ! [X115] :
( ~ r1(X114,X115)
| ! [X116] :
( ~ r1(X115,X116)
| ~ p1(X116) ) )
| ~ ! [X117] :
( ~ r1(X114,X117)
| ~ p1(X117) ) ) )
| ~ ! [X118] :
( ~ r1(X92,X118)
| ! [X119] :
( ~ r1(X118,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ~ p1(X120) ) )
| ~ ! [X121] :
( ~ r1(X118,X121)
| ~ p1(X121) ) ) )
| ~ ! [X122] :
( ~ r1(X87,X122)
| ! [X123] :
( ~ r1(X122,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ~ p1(X124) ) )
| ~ ! [X125] :
( ~ r1(X122,X125)
| ~ p1(X125) ) ) )
| ~ ! [X126] :
( ~ r1(X0,X126)
| ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ~ p1(X128) ) )
| ~ ! [X129] :
( ~ r1(X126,X129)
| ~ p1(X129) ) ) ),
inference(pure_predicate_removal,[],[f4]) ).
fof(f6,plain,
? [X0] :
~ ( ~ ! [X2] :
( ~ r1(X0,X2)
| ~ ( ~ ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ~ ! [X5] :
( ~ r1(X4,X5)
| ~ p1(X5) ) ) )
& ! [X6] :
( ~ r1(X2,X6)
| ~ ! [X7] :
( ~ r1(X6,X7)
| ~ p1(X7) ) ) ) )
| ~ ! [X8] :
( ~ r1(X0,X8)
| ~ ( ~ ! [X9] :
( ~ r1(X8,X9)
| ~ ( ~ ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ~ ! [X12] :
( ~ r1(X11,X12)
| ~ p1(X12) ) ) )
& ! [X13] :
( ~ r1(X9,X13)
| ~ ! [X14] :
( ~ r1(X13,X14)
| ~ p1(X14) ) ) ) )
| ~ ! [X15] :
( ~ r1(X8,X15)
| ~ ( ~ ! [X16] :
( ~ r1(X15,X16)
| ~ ( ~ ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ~ ! [X19] :
( ~ r1(X18,X19)
| ~ p1(X19) ) ) )
& ! [X20] :
( ~ r1(X16,X20)
| ~ ! [X21] :
( ~ r1(X20,X21)
| ~ p1(X21) ) ) ) )
| ~ ! [X22] :
( ~ r1(X15,X22)
| ~ ( ~ ! [X23] :
( ~ r1(X22,X23)
| ~ ( ~ ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ~ ! [X26] :
( ~ r1(X25,X26)
| ~ p1(X26) ) ) )
& ! [X27] :
( ~ r1(X23,X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| ~ p1(X28) ) ) ) )
| ~ ! [X29] :
( ~ r1(X22,X29)
| ~ ( ~ ! [X30] :
( ~ r1(X29,X30)
| ~ ( ~ ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| ~ ! [X33] :
( ~ r1(X32,X33)
| ~ p1(X33) ) ) )
& ! [X34] :
( ~ r1(X30,X34)
| ~ ! [X35] :
( ~ r1(X34,X35)
| ~ p1(X35) ) ) ) )
| ~ ! [X36] :
( ~ r1(X29,X36)
| ~ ( ~ ! [X37] :
( ~ r1(X36,X37)
| ~ ! [X38] :
( ~ r1(X37,X38)
| ! [X39] : ~ r1(X38,X39)
| ~ p2(X38) ) )
| ~ ! [X40] :
( ~ r1(X36,X40)
| ~ ( ~ ! [X41] :
( ~ r1(X40,X41)
| ~ ( ! [X42] : ~ r1(X41,X42)
| ~ p2(X41) ) )
& p2(X40)
& ~ ! [X43] :
( ~ r1(X40,X43)
| ~ ! [X44] :
( ~ r1(X43,X44)
| ~ ! [X45] :
( ~ r1(X44,X45)
| ~ p2(X45) ) ) ) ) )
| ( ~ ! [X46] :
( ~ r1(X36,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ~ ! [X48] :
( ~ r1(X47,X48)
| ! [X49] : ~ r1(X48,X49)
| ~ p2(X48) ) ) )
& ! [X50] :
( ~ r1(X36,X50)
| ~ ! [X51] :
( ~ r1(X50,X51)
| ~ p2(X51) ) ) )
| ~ ! [X52] :
( ~ r1(X36,X52)
| ~ ( ! [X53] :
( ~ r1(X52,X53)
| ~ ! [X54] :
( ~ r1(X53,X54)
| ~ p2(X54) ) )
& ! [X55] :
( ~ r1(X52,X55)
| ~ ! [X56] :
( ~ r1(X55,X56)
| ~ ! [X57] :
( ~ r1(X56,X57)
| ! [X58] : ~ r1(X57,X58)
| ~ p2(X57) ) ) ) ) )
| ( ! [X59] :
( ~ r1(X36,X59)
| ! [X60] : ~ r1(X59,X60)
| ~ p2(X59) )
& ! [X61] :
( ~ r1(X36,X61)
| ~ ! [X62] :
( ~ r1(X61,X62)
| ~ p2(X62) ) ) ) ) )
| ~ ! [X63] :
( ~ r1(X29,X63)
| ~ ( ~ ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| p1(X65) ) )
& ! [X66] :
( ~ r1(X63,X66)
| p1(X66) ) ) ) ) )
| ~ ! [X67] :
( ~ r1(X22,X67)
| ~ ( ~ ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| p1(X69) ) )
& ! [X70] :
( ~ r1(X67,X70)
| p1(X70) ) ) ) ) )
| ~ ! [X71] :
( ~ r1(X15,X71)
| ~ ( ~ ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| p1(X73) ) )
& ! [X74] :
( ~ r1(X71,X74)
| p1(X74) ) ) ) ) )
| ~ ! [X75] :
( ~ r1(X8,X75)
| ~ ( ~ ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| p1(X77) ) )
& ! [X78] :
( ~ r1(X75,X78)
| p1(X78) ) ) ) ) )
| ~ ! [X79] :
( ~ r1(X0,X79)
| ~ ( ~ ! [X80] :
( ~ r1(X79,X80)
| ! [X81] :
( ~ r1(X80,X81)
| p1(X81) ) )
& ! [X82] :
( ~ r1(X79,X82)
| p1(X82) ) ) )
| ! [X83] :
( ~ r1(X0,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ~ ! [X85] :
( ~ r1(X84,X85)
| p1(X85) ) )
| ! [X86] :
( ~ r1(X83,X86)
| p1(X86) ) )
| ! [X87] :
( ~ r1(X0,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ~ ! [X90] :
( ~ r1(X89,X90)
| p1(X90) ) )
| ! [X91] :
( ~ r1(X88,X91)
| p1(X91) ) )
| ! [X92] :
( ~ r1(X87,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ~ ! [X95] :
( ~ r1(X94,X95)
| p1(X95) ) )
| ! [X96] :
( ~ r1(X93,X96)
| p1(X96) ) )
| ! [X97] :
( ~ r1(X92,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ~ ! [X100] :
( ~ r1(X99,X100)
| p1(X100) ) )
| ! [X101] :
( ~ r1(X98,X101)
| p1(X101) ) )
| ! [X102] :
( ~ r1(X97,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ! [X104] :
( ~ r1(X103,X104)
| ~ ! [X105] :
( ~ r1(X104,X105)
| p1(X105) ) )
| ! [X106] :
( ~ r1(X103,X106)
| p1(X106) ) )
| ! [X107] :
( ~ r1(X102,X107)
| ~ ! [X108] :
( ~ r1(X107,X108)
| ~ ! [X109] :
( ~ r1(X108,X109)
| p2(X109) ) ) )
| ~ ! [X110] :
( ~ r1(X102,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ~ p1(X112) ) )
| ~ ! [X113] :
( ~ r1(X110,X113)
| ~ p1(X113) ) ) )
| ~ ! [X114] :
( ~ r1(X97,X114)
| ! [X115] :
( ~ r1(X114,X115)
| ! [X116] :
( ~ r1(X115,X116)
| ~ p1(X116) ) )
| ~ ! [X117] :
( ~ r1(X114,X117)
| ~ p1(X117) ) ) )
| ~ ! [X118] :
( ~ r1(X92,X118)
| ! [X119] :
( ~ r1(X118,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ~ p1(X120) ) )
| ~ ! [X121] :
( ~ r1(X118,X121)
| ~ p1(X121) ) ) )
| ~ ! [X122] :
( ~ r1(X87,X122)
| ! [X123] :
( ~ r1(X122,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ~ p1(X124) ) )
| ~ ! [X125] :
( ~ r1(X122,X125)
| ~ p1(X125) ) ) )
| ~ ! [X126] :
( ~ r1(X0,X126)
| ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ~ p1(X128) ) )
| ~ ! [X129] :
( ~ r1(X126,X129)
| ~ p1(X129) ) ) ),
inference(pure_predicate_removal,[],[f5]) ).
fof(f7,plain,
? [X0] :
( ! [X2] :
( ~ r1(X0,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ? [X5] :
( r1(X4,X5)
& p1(X5) ) ) )
| ? [X6] :
( r1(X2,X6)
& ! [X7] :
( ~ r1(X6,X7)
| ~ p1(X7) ) ) )
& ! [X8] :
( ~ r1(X0,X8)
| ( ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ? [X12] :
( r1(X11,X12)
& p1(X12) ) ) )
| ? [X13] :
( r1(X9,X13)
& ! [X14] :
( ~ r1(X13,X14)
| ~ p1(X14) ) ) )
& ! [X15] :
( ~ r1(X8,X15)
| ( ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ? [X19] :
( r1(X18,X19)
& p1(X19) ) ) )
| ? [X20] :
( r1(X16,X20)
& ! [X21] :
( ~ r1(X20,X21)
| ~ p1(X21) ) ) )
& ! [X22] :
( ~ r1(X15,X22)
| ( ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ? [X26] :
( r1(X25,X26)
& p1(X26) ) ) )
| ? [X27] :
( r1(X23,X27)
& ! [X28] :
( ~ r1(X27,X28)
| ~ p1(X28) ) ) )
& ! [X29] :
( ~ r1(X22,X29)
| ( ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| ? [X33] :
( r1(X32,X33)
& p1(X33) ) ) )
| ? [X34] :
( r1(X30,X34)
& ! [X35] :
( ~ r1(X34,X35)
| ~ p1(X35) ) ) )
& ! [X36] :
( ~ r1(X29,X36)
| ( ! [X37] :
( ~ r1(X36,X37)
| ? [X38] :
( r1(X37,X38)
& ? [X39] : r1(X38,X39)
& p2(X38) ) )
& ! [X40] :
( ~ r1(X36,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ( ? [X42] : r1(X41,X42)
& p2(X41) ) )
| ~ p2(X40)
| ! [X43] :
( ~ r1(X40,X43)
| ? [X44] :
( r1(X43,X44)
& ! [X45] :
( ~ r1(X44,X45)
| ~ p2(X45) ) ) ) )
& ( ! [X46] :
( ~ r1(X36,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ? [X48] :
( r1(X47,X48)
& ? [X49] : r1(X48,X49)
& p2(X48) ) ) )
| ? [X50] :
( r1(X36,X50)
& ! [X51] :
( ~ r1(X50,X51)
| ~ p2(X51) ) ) )
& ! [X52] :
( ~ r1(X36,X52)
| ? [X53] :
( r1(X52,X53)
& ! [X54] :
( ~ r1(X53,X54)
| ~ p2(X54) ) )
| ? [X55] :
( r1(X52,X55)
& ! [X56] :
( ~ r1(X55,X56)
| ? [X57] :
( r1(X56,X57)
& ? [X58] : r1(X57,X58)
& p2(X57) ) ) ) )
& ( ? [X59] :
( r1(X36,X59)
& ? [X60] : r1(X59,X60)
& p2(X59) )
| ? [X61] :
( r1(X36,X61)
& ! [X62] :
( ~ r1(X61,X62)
| ~ p2(X62) ) ) ) ) )
& ! [X63] :
( ~ r1(X29,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| p1(X65) ) )
| ? [X66] :
( r1(X63,X66)
& ~ p1(X66) ) ) ) )
& ! [X67] :
( ~ r1(X22,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| p1(X69) ) )
| ? [X70] :
( r1(X67,X70)
& ~ p1(X70) ) ) ) )
& ! [X71] :
( ~ r1(X15,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| p1(X73) ) )
| ? [X74] :
( r1(X71,X74)
& ~ p1(X74) ) ) ) )
& ! [X75] :
( ~ r1(X8,X75)
| ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| p1(X77) ) )
| ? [X78] :
( r1(X75,X78)
& ~ p1(X78) ) ) ) )
& ! [X79] :
( ~ r1(X0,X79)
| ! [X80] :
( ~ r1(X79,X80)
| ! [X81] :
( ~ r1(X80,X81)
| p1(X81) ) )
| ? [X82] :
( r1(X79,X82)
& ~ p1(X82) ) )
& ? [X83] :
( r1(X0,X83)
& ? [X84] :
( r1(X83,X84)
& ! [X85] :
( ~ r1(X84,X85)
| p1(X85) ) )
& ? [X86] :
( r1(X83,X86)
& ~ p1(X86) ) )
& ? [X87] :
( r1(X0,X87)
& ? [X88] :
( r1(X87,X88)
& ? [X89] :
( r1(X88,X89)
& ! [X90] :
( ~ r1(X89,X90)
| p1(X90) ) )
& ? [X91] :
( r1(X88,X91)
& ~ p1(X91) ) )
& ? [X92] :
( r1(X87,X92)
& ? [X93] :
( r1(X92,X93)
& ? [X94] :
( r1(X93,X94)
& ! [X95] :
( ~ r1(X94,X95)
| p1(X95) ) )
& ? [X96] :
( r1(X93,X96)
& ~ p1(X96) ) )
& ? [X97] :
( r1(X92,X97)
& ? [X98] :
( r1(X97,X98)
& ? [X99] :
( r1(X98,X99)
& ! [X100] :
( ~ r1(X99,X100)
| p1(X100) ) )
& ? [X101] :
( r1(X98,X101)
& ~ p1(X101) ) )
& ? [X102] :
( r1(X97,X102)
& ? [X103] :
( r1(X102,X103)
& ? [X104] :
( r1(X103,X104)
& ! [X105] :
( ~ r1(X104,X105)
| p1(X105) ) )
& ? [X106] :
( r1(X103,X106)
& ~ p1(X106) ) )
& ? [X107] :
( r1(X102,X107)
& ! [X108] :
( ~ r1(X107,X108)
| ? [X109] :
( r1(X108,X109)
& ~ p2(X109) ) ) )
& ! [X110] :
( ~ r1(X102,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ~ p1(X112) ) )
| ? [X113] :
( r1(X110,X113)
& p1(X113) ) ) )
& ! [X114] :
( ~ r1(X97,X114)
| ! [X115] :
( ~ r1(X114,X115)
| ! [X116] :
( ~ r1(X115,X116)
| ~ p1(X116) ) )
| ? [X117] :
( r1(X114,X117)
& p1(X117) ) ) )
& ! [X118] :
( ~ r1(X92,X118)
| ! [X119] :
( ~ r1(X118,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ~ p1(X120) ) )
| ? [X121] :
( r1(X118,X121)
& p1(X121) ) ) )
& ! [X122] :
( ~ r1(X87,X122)
| ! [X123] :
( ~ r1(X122,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ~ p1(X124) ) )
| ? [X125] :
( r1(X122,X125)
& p1(X125) ) ) )
& ! [X126] :
( ~ r1(X0,X126)
| ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ~ p1(X128) ) )
| ? [X129] :
( r1(X126,X129)
& p1(X129) ) ) ),
inference(ennf_transformation,[],[f6]) ).
fof(f8,plain,
? [X0] :
( ! [X2] :
( ~ r1(X0,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ? [X5] :
( r1(X4,X5)
& p1(X5) ) ) )
| ? [X6] :
( r1(X2,X6)
& ! [X7] :
( ~ r1(X6,X7)
| ~ p1(X7) ) ) )
& ! [X8] :
( ~ r1(X0,X8)
| ( ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ? [X12] :
( r1(X11,X12)
& p1(X12) ) ) )
| ? [X13] :
( r1(X9,X13)
& ! [X14] :
( ~ r1(X13,X14)
| ~ p1(X14) ) ) )
& ! [X15] :
( ~ r1(X8,X15)
| ( ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ? [X19] :
( r1(X18,X19)
& p1(X19) ) ) )
| ? [X20] :
( r1(X16,X20)
& ! [X21] :
( ~ r1(X20,X21)
| ~ p1(X21) ) ) )
& ! [X22] :
( ~ r1(X15,X22)
| ( ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ? [X26] :
( r1(X25,X26)
& p1(X26) ) ) )
| ? [X27] :
( r1(X23,X27)
& ! [X28] :
( ~ r1(X27,X28)
| ~ p1(X28) ) ) )
& ! [X29] :
( ~ r1(X22,X29)
| ( ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| ? [X33] :
( r1(X32,X33)
& p1(X33) ) ) )
| ? [X34] :
( r1(X30,X34)
& ! [X35] :
( ~ r1(X34,X35)
| ~ p1(X35) ) ) )
& ! [X36] :
( ~ r1(X29,X36)
| ( ! [X37] :
( ~ r1(X36,X37)
| ? [X38] :
( r1(X37,X38)
& ? [X39] : r1(X38,X39)
& p2(X38) ) )
& ! [X40] :
( ~ r1(X36,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ( ? [X42] : r1(X41,X42)
& p2(X41) ) )
| ~ p2(X40)
| ! [X43] :
( ~ r1(X40,X43)
| ? [X44] :
( r1(X43,X44)
& ! [X45] :
( ~ r1(X44,X45)
| ~ p2(X45) ) ) ) )
& ( ! [X46] :
( ~ r1(X36,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ? [X48] :
( r1(X47,X48)
& ? [X49] : r1(X48,X49)
& p2(X48) ) ) )
| ? [X50] :
( r1(X36,X50)
& ! [X51] :
( ~ r1(X50,X51)
| ~ p2(X51) ) ) )
& ! [X52] :
( ~ r1(X36,X52)
| ? [X53] :
( r1(X52,X53)
& ! [X54] :
( ~ r1(X53,X54)
| ~ p2(X54) ) )
| ? [X55] :
( r1(X52,X55)
& ! [X56] :
( ~ r1(X55,X56)
| ? [X57] :
( r1(X56,X57)
& ? [X58] : r1(X57,X58)
& p2(X57) ) ) ) )
& ( ? [X59] :
( r1(X36,X59)
& ? [X60] : r1(X59,X60)
& p2(X59) )
| ? [X61] :
( r1(X36,X61)
& ! [X62] :
( ~ r1(X61,X62)
| ~ p2(X62) ) ) ) ) )
& ! [X63] :
( ~ r1(X29,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| p1(X65) ) )
| ? [X66] :
( r1(X63,X66)
& ~ p1(X66) ) ) ) )
& ! [X67] :
( ~ r1(X22,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| p1(X69) ) )
| ? [X70] :
( r1(X67,X70)
& ~ p1(X70) ) ) ) )
& ! [X71] :
( ~ r1(X15,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| p1(X73) ) )
| ? [X74] :
( r1(X71,X74)
& ~ p1(X74) ) ) ) )
& ! [X75] :
( ~ r1(X8,X75)
| ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| p1(X77) ) )
| ? [X78] :
( r1(X75,X78)
& ~ p1(X78) ) ) ) )
& ! [X79] :
( ~ r1(X0,X79)
| ! [X80] :
( ~ r1(X79,X80)
| ! [X81] :
( ~ r1(X80,X81)
| p1(X81) ) )
| ? [X82] :
( r1(X79,X82)
& ~ p1(X82) ) )
& ? [X83] :
( r1(X0,X83)
& ? [X84] :
( r1(X83,X84)
& ! [X85] :
( ~ r1(X84,X85)
| p1(X85) ) )
& ? [X86] :
( r1(X83,X86)
& ~ p1(X86) ) )
& ? [X87] :
( r1(X0,X87)
& ? [X88] :
( r1(X87,X88)
& ? [X89] :
( r1(X88,X89)
& ! [X90] :
( ~ r1(X89,X90)
| p1(X90) ) )
& ? [X91] :
( r1(X88,X91)
& ~ p1(X91) ) )
& ? [X92] :
( r1(X87,X92)
& ? [X93] :
( r1(X92,X93)
& ? [X94] :
( r1(X93,X94)
& ! [X95] :
( ~ r1(X94,X95)
| p1(X95) ) )
& ? [X96] :
( r1(X93,X96)
& ~ p1(X96) ) )
& ? [X97] :
( r1(X92,X97)
& ? [X98] :
( r1(X97,X98)
& ? [X99] :
( r1(X98,X99)
& ! [X100] :
( ~ r1(X99,X100)
| p1(X100) ) )
& ? [X101] :
( r1(X98,X101)
& ~ p1(X101) ) )
& ? [X102] :
( r1(X97,X102)
& ? [X103] :
( r1(X102,X103)
& ? [X104] :
( r1(X103,X104)
& ! [X105] :
( ~ r1(X104,X105)
| p1(X105) ) )
& ? [X106] :
( r1(X103,X106)
& ~ p1(X106) ) )
& ? [X107] :
( r1(X102,X107)
& ! [X108] :
( ~ r1(X107,X108)
| ? [X109] :
( r1(X108,X109)
& ~ p2(X109) ) ) )
& ! [X110] :
( ~ r1(X102,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ~ p1(X112) ) )
| ? [X113] :
( r1(X110,X113)
& p1(X113) ) ) )
& ! [X114] :
( ~ r1(X97,X114)
| ! [X115] :
( ~ r1(X114,X115)
| ! [X116] :
( ~ r1(X115,X116)
| ~ p1(X116) ) )
| ? [X117] :
( r1(X114,X117)
& p1(X117) ) ) )
& ! [X118] :
( ~ r1(X92,X118)
| ! [X119] :
( ~ r1(X118,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ~ p1(X120) ) )
| ? [X121] :
( r1(X118,X121)
& p1(X121) ) ) )
& ! [X122] :
( ~ r1(X87,X122)
| ! [X123] :
( ~ r1(X122,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ~ p1(X124) ) )
| ? [X125] :
( r1(X122,X125)
& p1(X125) ) ) )
& ! [X126] :
( ~ r1(X0,X126)
| ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ~ p1(X128) ) )
| ? [X129] :
( r1(X126,X129)
& p1(X129) ) ) ),
inference(flattening,[],[f7]) ).
fof(f9,definition,
! [X36] :
( ? [X59] :
( r1(X36,X59)
& ? [X60] : r1(X59,X60)
& p2(X59) )
| ~ sP0(X36) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f10,definition,
! [X56] :
( ? [X57] :
( r1(X56,X57)
& ? [X58] : r1(X57,X58)
& p2(X57) )
| ~ sP1(X56) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f11,definition,
! [X52] :
( ? [X55] :
( r1(X52,X55)
& ! [X56] :
( ~ r1(X55,X56)
| sP1(X56) ) )
| ~ sP2(X52) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f12,definition,
! [X47] :
( ? [X48] :
( r1(X47,X48)
& ? [X49] : r1(X48,X49)
& p2(X48) )
| ~ sP3(X47) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f13,definition,
! [X40] :
( ! [X43] :
( ~ r1(X40,X43)
| ? [X44] :
( r1(X43,X44)
& ! [X45] :
( ~ r1(X44,X45)
| ~ p2(X45) ) ) )
| ~ sP4(X40) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f14,definition,
! [X37] :
( ? [X38] :
( r1(X37,X38)
& ? [X39] : r1(X38,X39)
& p2(X38) )
| ~ sP5(X37) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f15,definition,
! [X36] :
( sP0(X36)
| ? [X61] :
( r1(X36,X61)
& ! [X62] :
( ~ r1(X61,X62)
| ~ p2(X62) ) )
| ~ sP6(X36) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f16,definition,
! [X36] :
( ! [X52] :
( ~ r1(X36,X52)
| ? [X53] :
( r1(X52,X53)
& ! [X54] :
( ~ r1(X53,X54)
| ~ p2(X54) ) )
| sP2(X52) )
| ~ sP7(X36) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f17,definition,
! [X36] :
( ! [X46] :
( ~ r1(X36,X46)
| ! [X47] :
( ~ r1(X46,X47)
| sP3(X47) ) )
| ? [X50] :
( r1(X36,X50)
& ! [X51] :
( ~ r1(X50,X51)
| ~ p2(X51) ) )
| ~ sP8(X36) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f18,definition,
! [X36] :
( ! [X40] :
( ~ r1(X36,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ( ? [X42] : r1(X41,X42)
& p2(X41) ) )
| ~ p2(X40)
| sP4(X40) )
| ~ sP9(X36) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f19,definition,
! [X36] :
( ( ! [X37] :
( ~ r1(X36,X37)
| sP5(X37) )
& sP9(X36)
& sP8(X36)
& sP7(X36)
& sP6(X36) )
| ~ sP10(X36) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f20,definition,
! [X30] :
( ? [X34] :
( r1(X30,X34)
& ! [X35] :
( ~ r1(X34,X35)
| ~ p1(X35) ) )
| ~ sP11(X30) ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f21,definition,
! [X29] :
( ! [X63] :
( ~ r1(X29,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| p1(X65) ) )
| ? [X66] :
( r1(X63,X66)
& ~ p1(X66) ) )
| ~ sP12(X29) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f22,definition,
! [X29] :
( ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| ? [X33] :
( r1(X32,X33)
& p1(X33) ) ) )
| sP11(X30) )
| ~ sP13(X29) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f23,definition,
! [X29] :
( ( sP13(X29)
& ! [X36] :
( ~ r1(X29,X36)
| sP10(X36) )
& sP12(X29) )
| ~ sP14(X29) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f24,definition,
! [X23] :
( ? [X27] :
( r1(X23,X27)
& ! [X28] :
( ~ r1(X27,X28)
| ~ p1(X28) ) )
| ~ sP15(X23) ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f25,definition,
! [X22] :
( ! [X67] :
( ~ r1(X22,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| p1(X69) ) )
| ? [X70] :
( r1(X67,X70)
& ~ p1(X70) ) )
| ~ sP16(X22) ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f26,definition,
! [X22] :
( ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ? [X26] :
( r1(X25,X26)
& p1(X26) ) ) )
| sP15(X23) )
| ~ sP17(X22) ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f27,definition,
! [X22] :
( ( sP17(X22)
& ! [X29] :
( ~ r1(X22,X29)
| sP14(X29) )
& sP16(X22) )
| ~ sP18(X22) ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f28,definition,
! [X16] :
( ? [X20] :
( r1(X16,X20)
& ! [X21] :
( ~ r1(X20,X21)
| ~ p1(X21) ) )
| ~ sP19(X16) ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f29,definition,
! [X15] :
( ! [X71] :
( ~ r1(X15,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| p1(X73) ) )
| ? [X74] :
( r1(X71,X74)
& ~ p1(X74) ) )
| ~ sP20(X15) ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f30,definition,
! [X15] :
( ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ? [X19] :
( r1(X18,X19)
& p1(X19) ) ) )
| sP19(X16) )
| ~ sP21(X15) ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f31,definition,
! [X15] :
( ( sP21(X15)
& ! [X22] :
( ~ r1(X15,X22)
| sP18(X22) )
& sP20(X15) )
| ~ sP22(X15) ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f32,definition,
! [X9] :
( ? [X13] :
( r1(X9,X13)
& ! [X14] :
( ~ r1(X13,X14)
| ~ p1(X14) ) )
| ~ sP23(X9) ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f33,definition,
! [X8] :
( ! [X75] :
( ~ r1(X8,X75)
| ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| p1(X77) ) )
| ? [X78] :
( r1(X75,X78)
& ~ p1(X78) ) )
| ~ sP24(X8) ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f34,definition,
! [X8] :
( ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ? [X12] :
( r1(X11,X12)
& p1(X12) ) ) )
| sP23(X9) )
| ~ sP25(X8) ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f35,definition,
! [X8] :
( ( sP25(X8)
& ! [X15] :
( ~ r1(X8,X15)
| sP22(X15) )
& sP24(X8) )
| ~ sP26(X8) ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f36,definition,
! [X2] :
( ? [X6] :
( r1(X2,X6)
& ! [X7] :
( ~ r1(X6,X7)
| ~ p1(X7) ) )
| ~ sP27(X2) ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f37,plain,
? [X0] :
( ! [X2] :
( ~ r1(X0,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ? [X5] :
( r1(X4,X5)
& p1(X5) ) ) )
| sP27(X2) )
& ! [X8] :
( ~ r1(X0,X8)
| sP26(X8) )
& ! [X79] :
( ~ r1(X0,X79)
| ! [X80] :
( ~ r1(X79,X80)
| ! [X81] :
( ~ r1(X80,X81)
| p1(X81) ) )
| ? [X82] :
( r1(X79,X82)
& ~ p1(X82) ) )
& ? [X83] :
( r1(X0,X83)
& ? [X84] :
( r1(X83,X84)
& ! [X85] :
( ~ r1(X84,X85)
| p1(X85) ) )
& ? [X86] :
( r1(X83,X86)
& ~ p1(X86) ) )
& ? [X87] :
( r1(X0,X87)
& ? [X88] :
( r1(X87,X88)
& ? [X89] :
( r1(X88,X89)
& ! [X90] :
( ~ r1(X89,X90)
| p1(X90) ) )
& ? [X91] :
( r1(X88,X91)
& ~ p1(X91) ) )
& ? [X92] :
( r1(X87,X92)
& ? [X93] :
( r1(X92,X93)
& ? [X94] :
( r1(X93,X94)
& ! [X95] :
( ~ r1(X94,X95)
| p1(X95) ) )
& ? [X96] :
( r1(X93,X96)
& ~ p1(X96) ) )
& ? [X97] :
( r1(X92,X97)
& ? [X98] :
( r1(X97,X98)
& ? [X99] :
( r1(X98,X99)
& ! [X100] :
( ~ r1(X99,X100)
| p1(X100) ) )
& ? [X101] :
( r1(X98,X101)
& ~ p1(X101) ) )
& ? [X102] :
( r1(X97,X102)
& ? [X103] :
( r1(X102,X103)
& ? [X104] :
( r1(X103,X104)
& ! [X105] :
( ~ r1(X104,X105)
| p1(X105) ) )
& ? [X106] :
( r1(X103,X106)
& ~ p1(X106) ) )
& ? [X107] :
( r1(X102,X107)
& ! [X108] :
( ~ r1(X107,X108)
| ? [X109] :
( r1(X108,X109)
& ~ p2(X109) ) ) )
& ! [X110] :
( ~ r1(X102,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ~ p1(X112) ) )
| ? [X113] :
( r1(X110,X113)
& p1(X113) ) ) )
& ! [X114] :
( ~ r1(X97,X114)
| ! [X115] :
( ~ r1(X114,X115)
| ! [X116] :
( ~ r1(X115,X116)
| ~ p1(X116) ) )
| ? [X117] :
( r1(X114,X117)
& p1(X117) ) ) )
& ! [X118] :
( ~ r1(X92,X118)
| ! [X119] :
( ~ r1(X118,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ~ p1(X120) ) )
| ? [X121] :
( r1(X118,X121)
& p1(X121) ) ) )
& ! [X122] :
( ~ r1(X87,X122)
| ! [X123] :
( ~ r1(X122,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ~ p1(X124) ) )
| ? [X125] :
( r1(X122,X125)
& p1(X125) ) ) )
& ! [X126] :
( ~ r1(X0,X126)
| ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ~ p1(X128) ) )
| ? [X129] :
( r1(X126,X129)
& p1(X129) ) ) ),
inference(definition_folding,[],[f8,f36,f35,f34,f33,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10,f9]) ).
fof(f41,plain,
! [X8] :
( ( sP25(X8)
& ! [X15] :
( ~ r1(X8,X15)
| sP22(X15) )
& sP24(X8) )
| ~ sP26(X8) ),
inference(nnf_transformation,[],[f35]) ).
fof(f42,plain,
! [X0] :
( ( sP25(X0)
& ! [X1] :
( ~ r1(X0,X1)
| sP22(X1) )
& sP24(X0) )
| ~ sP26(X0) ),
inference(rectify,[],[f41]) ).
fof(f52,plain,
! [X15] :
( ( sP21(X15)
& ! [X22] :
( ~ r1(X15,X22)
| sP18(X22) )
& sP20(X15) )
| ~ sP22(X15) ),
inference(nnf_transformation,[],[f31]) ).
fof(f53,plain,
! [X0] :
( ( sP21(X0)
& ! [X1] :
( ~ r1(X0,X1)
| sP18(X1) )
& sP20(X0) )
| ~ sP22(X0) ),
inference(rectify,[],[f52]) ).
fof(f63,plain,
! [X22] :
( ( sP17(X22)
& ! [X29] :
( ~ r1(X22,X29)
| sP14(X29) )
& sP16(X22) )
| ~ sP18(X22) ),
inference(nnf_transformation,[],[f27]) ).
fof(f64,plain,
! [X0] :
( ( sP17(X0)
& ! [X1] :
( ~ r1(X0,X1)
| sP14(X1) )
& sP16(X0) )
| ~ sP18(X0) ),
inference(rectify,[],[f63]) ).
fof(f74,plain,
! [X29] :
( ( sP13(X29)
& ! [X36] :
( ~ r1(X29,X36)
| sP10(X36) )
& sP12(X29) )
| ~ sP14(X29) ),
inference(nnf_transformation,[],[f23]) ).
fof(f75,plain,
! [X0] :
( ( sP13(X0)
& ! [X1] :
( ~ r1(X0,X1)
| sP10(X1) )
& sP12(X0) )
| ~ sP14(X0) ),
inference(rectify,[],[f74]) ).
fof(f85,plain,
! [X36] :
( ( ! [X37] :
( ~ r1(X36,X37)
| sP5(X37) )
& sP9(X36)
& sP8(X36)
& sP7(X36)
& sP6(X36) )
| ~ sP10(X36) ),
inference(nnf_transformation,[],[f19]) ).
fof(f86,plain,
! [X0] :
( ( ! [X1] :
( ~ r1(X0,X1)
| sP5(X1) )
& sP9(X0)
& sP8(X0)
& sP7(X0)
& sP6(X0) )
| ~ sP10(X0) ),
inference(rectify,[],[f85]) ).
fof(f87,plain,
! [X36] :
( ! [X40] :
( ~ r1(X36,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ( ? [X42] : r1(X41,X42)
& p2(X41) ) )
| ~ p2(X40)
| sP4(X40) )
| ~ sP9(X36) ),
inference(nnf_transformation,[],[f18]) ).
fof(f88,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ( ? [X3] : r1(X2,X3)
& p2(X2) ) )
| ~ p2(X1)
| sP4(X1) )
| ~ sP9(X0) ),
inference(rectify,[],[f87]) ).
fof(f89,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ( r1(X2,sK41(X2))
& p2(X2) ) )
| ~ p2(X1)
| sP4(X1) )
| ~ sP9(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41]),skolemize(X3,sK41(X2))],[f88]) ).
fof(f90,plain,
! [X36] :
( ! [X46] :
( ~ r1(X36,X46)
| ! [X47] :
( ~ r1(X46,X47)
| sP3(X47) ) )
| ? [X50] :
( r1(X36,X50)
& ! [X51] :
( ~ r1(X50,X51)
| ~ p2(X51) ) )
| ~ sP8(X36) ),
inference(nnf_transformation,[],[f17]) ).
fof(f91,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| sP3(X2) ) )
| ? [X3] :
( r1(X0,X3)
& ! [X4] :
( ~ r1(X3,X4)
| ~ p2(X4) ) )
| ~ sP8(X0) ),
inference(rectify,[],[f90]) ).
fof(f92,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| sP3(X2) ) )
| ( r1(X0,sK42(X0))
& ! [X4] :
( ~ r1(sK42(X0),X4)
| ~ p2(X4) ) )
| ~ sP8(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42]),skolemize(X3,sK42(X0))],[f91]) ).
fof(f93,plain,
! [X36] :
( ! [X52] :
( ~ r1(X36,X52)
| ? [X53] :
( r1(X52,X53)
& ! [X54] :
( ~ r1(X53,X54)
| ~ p2(X54) ) )
| sP2(X52) )
| ~ sP7(X36) ),
inference(nnf_transformation,[],[f16]) ).
fof(f94,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ? [X2] :
( r1(X1,X2)
& ! [X3] :
( ~ r1(X2,X3)
| ~ p2(X3) ) )
| sP2(X1) )
| ~ sP7(X0) ),
inference(rectify,[],[f93]) ).
fof(f95,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( r1(X1,sK43(X1))
& ! [X3] :
( ~ r1(sK43(X1),X3)
| ~ p2(X3) ) )
| sP2(X1) )
| ~ sP7(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43]),skolemize(X2,sK43(X1))],[f94]) ).
fof(f96,plain,
! [X36] :
( sP0(X36)
| ? [X61] :
( r1(X36,X61)
& ! [X62] :
( ~ r1(X61,X62)
| ~ p2(X62) ) )
| ~ sP6(X36) ),
inference(nnf_transformation,[],[f15]) ).
fof(f97,plain,
! [X0] :
( sP0(X0)
| ? [X1] :
( r1(X0,X1)
& ! [X2] :
( ~ r1(X1,X2)
| ~ p2(X2) ) )
| ~ sP6(X0) ),
inference(rectify,[],[f96]) ).
fof(f98,plain,
! [X0] :
( sP0(X0)
| ( r1(X0,sK44(X0))
& ! [X2] :
( ~ r1(sK44(X0),X2)
| ~ p2(X2) ) )
| ~ sP6(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44]),skolemize(X1,sK44(X0))],[f97]) ).
fof(f99,plain,
! [X37] :
( ? [X38] :
( r1(X37,X38)
& ? [X39] : r1(X38,X39)
& p2(X38) )
| ~ sP5(X37) ),
inference(nnf_transformation,[],[f14]) ).
fof(f100,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ? [X2] : r1(X1,X2)
& p2(X1) )
| ~ sP5(X0) ),
inference(rectify,[],[f99]) ).
fof(f101,plain,
! [X0] :
( ( r1(X0,sK45(X0))
& r1(sK45(X0),sK46(X0))
& p2(sK45(X0)) )
| ~ sP5(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK45,sK46]),skolemize(X1,sK45(X0)),skolemize(X2,sK46(X0))],[f100]) ).
fof(f102,plain,
! [X40] :
( ! [X43] :
( ~ r1(X40,X43)
| ? [X44] :
( r1(X43,X44)
& ! [X45] :
( ~ r1(X44,X45)
| ~ p2(X45) ) ) )
| ~ sP4(X40) ),
inference(nnf_transformation,[],[f13]) ).
fof(f103,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ? [X2] :
( r1(X1,X2)
& ! [X3] :
( ~ r1(X2,X3)
| ~ p2(X3) ) ) )
| ~ sP4(X0) ),
inference(rectify,[],[f102]) ).
fof(f104,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( r1(X1,sK47(X1))
& ! [X3] :
( ~ r1(sK47(X1),X3)
| ~ p2(X3) ) ) )
| ~ sP4(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47]),skolemize(X2,sK47(X1))],[f103]) ).
fof(f105,plain,
! [X47] :
( ? [X48] :
( r1(X47,X48)
& ? [X49] : r1(X48,X49)
& p2(X48) )
| ~ sP3(X47) ),
inference(nnf_transformation,[],[f12]) ).
fof(f106,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ? [X2] : r1(X1,X2)
& p2(X1) )
| ~ sP3(X0) ),
inference(rectify,[],[f105]) ).
fof(f107,plain,
! [X0] :
( ( r1(X0,sK48(X0))
& r1(sK48(X0),sK49(X0))
& p2(sK48(X0)) )
| ~ sP3(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK48,sK49]),skolemize(X1,sK48(X0)),skolemize(X2,sK49(X0))],[f106]) ).
fof(f108,plain,
! [X52] :
( ? [X55] :
( r1(X52,X55)
& ! [X56] :
( ~ r1(X55,X56)
| sP1(X56) ) )
| ~ sP2(X52) ),
inference(nnf_transformation,[],[f11]) ).
fof(f109,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ! [X2] :
( ~ r1(X1,X2)
| sP1(X2) ) )
| ~ sP2(X0) ),
inference(rectify,[],[f108]) ).
fof(f110,plain,
! [X0] :
( ( r1(X0,sK50(X0))
& ! [X2] :
( ~ r1(sK50(X0),X2)
| sP1(X2) ) )
| ~ sP2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50]),skolemize(X1,sK50(X0))],[f109]) ).
fof(f111,plain,
! [X56] :
( ? [X57] :
( r1(X56,X57)
& ? [X58] : r1(X57,X58)
& p2(X57) )
| ~ sP1(X56) ),
inference(nnf_transformation,[],[f10]) ).
fof(f112,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ? [X2] : r1(X1,X2)
& p2(X1) )
| ~ sP1(X0) ),
inference(rectify,[],[f111]) ).
fof(f113,plain,
! [X0] :
( ( r1(X0,sK51(X0))
& r1(sK51(X0),sK52(X0))
& p2(sK51(X0)) )
| ~ sP1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51,sK52]),skolemize(X1,sK51(X0)),skolemize(X2,sK52(X0))],[f112]) ).
fof(f114,plain,
! [X36] :
( ? [X59] :
( r1(X36,X59)
& ? [X60] : r1(X59,X60)
& p2(X59) )
| ~ sP0(X36) ),
inference(nnf_transformation,[],[f9]) ).
fof(f115,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ? [X2] : r1(X1,X2)
& p2(X1) )
| ~ sP0(X0) ),
inference(rectify,[],[f114]) ).
fof(f116,plain,
! [X0] :
( ( r1(X0,sK53(X0))
& r1(sK53(X0),sK54(X0))
& p2(sK53(X0)) )
| ~ sP0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK53,sK54]),skolemize(X1,sK53(X0)),skolemize(X2,sK54(X0))],[f115]) ).
fof(f117,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ? [X4] :
( r1(X3,X4)
& p1(X4) ) ) )
| sP27(X1) )
& ! [X5] :
( ~ r1(X0,X5)
| sP26(X5) )
& ! [X6] :
( ~ r1(X0,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| p1(X8) ) )
| ? [X9] :
( r1(X6,X9)
& ~ p1(X9) ) )
& ? [X10] :
( r1(X0,X10)
& ? [X11] :
( r1(X10,X11)
& ! [X12] :
( ~ r1(X11,X12)
| p1(X12) ) )
& ? [X13] :
( r1(X10,X13)
& ~ p1(X13) ) )
& ? [X14] :
( r1(X0,X14)
& ? [X15] :
( r1(X14,X15)
& ? [X16] :
( r1(X15,X16)
& ! [X17] :
( ~ r1(X16,X17)
| p1(X17) ) )
& ? [X18] :
( r1(X15,X18)
& ~ p1(X18) ) )
& ? [X19] :
( r1(X14,X19)
& ? [X20] :
( r1(X19,X20)
& ? [X21] :
( r1(X20,X21)
& ! [X22] :
( ~ r1(X21,X22)
| p1(X22) ) )
& ? [X23] :
( r1(X20,X23)
& ~ p1(X23) ) )
& ? [X24] :
( r1(X19,X24)
& ? [X25] :
( r1(X24,X25)
& ? [X26] :
( r1(X25,X26)
& ! [X27] :
( ~ r1(X26,X27)
| p1(X27) ) )
& ? [X28] :
( r1(X25,X28)
& ~ p1(X28) ) )
& ? [X29] :
( r1(X24,X29)
& ? [X30] :
( r1(X29,X30)
& ? [X31] :
( r1(X30,X31)
& ! [X32] :
( ~ r1(X31,X32)
| p1(X32) ) )
& ? [X33] :
( r1(X30,X33)
& ~ p1(X33) ) )
& ? [X34] :
( r1(X29,X34)
& ! [X35] :
( ~ r1(X34,X35)
| ? [X36] :
( r1(X35,X36)
& ~ p2(X36) ) ) )
& ! [X37] :
( ~ r1(X29,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ~ p1(X39) ) )
| ? [X40] :
( r1(X37,X40)
& p1(X40) ) ) )
& ! [X41] :
( ~ r1(X24,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ~ p1(X43) ) )
| ? [X44] :
( r1(X41,X44)
& p1(X44) ) ) )
& ! [X45] :
( ~ r1(X19,X45)
| ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ~ p1(X47) ) )
| ? [X48] :
( r1(X45,X48)
& p1(X48) ) ) )
& ! [X49] :
( ~ r1(X14,X49)
| ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ~ p1(X51) ) )
| ? [X52] :
( r1(X49,X52)
& p1(X52) ) ) )
& ! [X53] :
( ~ r1(X0,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ~ p1(X55) ) )
| ? [X56] :
( r1(X53,X56)
& p1(X56) ) ) ),
inference(rectify,[],[f37]) ).
fof(f118,plain,
( ! [X1] :
( ~ r1(sK55,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ( r1(X3,sK56(X3))
& p1(sK56(X3)) ) ) )
| sP27(X1) )
& ! [X5] :
( ~ r1(sK55,X5)
| sP26(X5) )
& ! [X6] :
( ~ r1(sK55,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| p1(X8) ) )
| ( r1(X6,sK57(X6))
& ~ p1(sK57(X6)) ) )
& r1(sK55,sK58)
& r1(sK58,sK59)
& ! [X12] :
( ~ r1(sK59,X12)
| p1(X12) )
& r1(sK58,sK60)
& ~ p1(sK60)
& r1(sK55,sK61)
& r1(sK61,sK62)
& r1(sK62,sK63)
& ! [X17] :
( ~ r1(sK63,X17)
| p1(X17) )
& r1(sK62,sK64)
& ~ p1(sK64)
& r1(sK61,sK65)
& r1(sK65,sK66)
& r1(sK66,sK67)
& ! [X22] :
( ~ r1(sK67,X22)
| p1(X22) )
& r1(sK66,sK68)
& ~ p1(sK68)
& r1(sK65,sK69)
& r1(sK69,sK70)
& r1(sK70,sK71)
& ! [X27] :
( ~ r1(sK71,X27)
| p1(X27) )
& r1(sK70,sK72)
& ~ p1(sK72)
& r1(sK69,sK73)
& r1(sK73,sK74)
& r1(sK74,sK75)
& ! [X32] :
( ~ r1(sK75,X32)
| p1(X32) )
& r1(sK74,sK76)
& ~ p1(sK76)
& r1(sK73,sK77)
& ! [X35] :
( ~ r1(sK77,X35)
| ( r1(X35,sK78(X35))
& ~ p2(sK78(X35)) ) )
& ! [X37] :
( ~ r1(sK73,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ~ p1(X39) ) )
| ( r1(X37,sK79(X37))
& p1(sK79(X37)) ) )
& ! [X41] :
( ~ r1(sK69,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ~ p1(X43) ) )
| ( r1(X41,sK80(X41))
& p1(sK80(X41)) ) )
& ! [X45] :
( ~ r1(sK65,X45)
| ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ~ p1(X47) ) )
| ( r1(X45,sK81(X45))
& p1(sK81(X45)) ) )
& ! [X49] :
( ~ r1(sK61,X49)
| ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ~ p1(X51) ) )
| ( r1(X49,sK82(X49))
& p1(sK82(X49)) ) )
& ! [X53] :
( ~ r1(sK55,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ~ p1(X55) ) )
| ( r1(X53,sK83(X53))
& p1(sK83(X53)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55,sK56,sK57,sK58,sK59,sK60,sK61,sK62,sK63,sK64,sK65,sK66,sK67,sK68,sK69,sK70,sK71,sK72,sK73,sK74,sK75,sK76,sK77,sK78,sK79,sK80,sK81,sK82,sK83]),skolemize(X0,sK55),skolemize(X4,sK56(X3)),skolemize(X9,sK57(X6)),skolemize(X10,sK58),skolemize(X11,sK59),skolemize(X13,sK60),skolemize(X14,sK61),skolemize(X15,sK62),skolemize(X16,sK63),skolemize(X18,sK64),skolemize(X19,sK65),skolemize(X20,sK66),skolemize(X21,sK67),skolemize(X23,sK68),skolemize(X24,sK69),skolemize(X25,sK70),skolemize(X26,sK71),skolemize(X28,sK72),skolemize(X29,sK73),skolemize(X30,sK74),skolemize(X31,sK75),skolemize(X33,sK76),skolemize(X34,sK77),skolemize(X36,sK78(X35)),skolemize(X40,sK79(X37)),skolemize(X44,sK80(X41)),skolemize(X48,sK81(X45)),skolemize(X52,sK82(X49)),skolemize(X56,sK83(X53))],[f117]) ).
fof(f122,plain,
! [X0,X1] :
( ~ sP26(X0)
| sP22(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f42]) ).
fof(f131,plain,
! [X0,X1] :
( ~ sP22(X0)
| sP18(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f53]) ).
fof(f140,plain,
! [X0,X1] :
( ~ sP18(X0)
| sP14(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f64]) ).
fof(f149,plain,
! [X0,X1] :
( ~ sP14(X0)
| sP10(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f75]) ).
fof(f157,plain,
! [X0] :
( ~ sP10(X0)
| sP6(X0) ),
inference(cnf_transformation,[],[f86]) ).
fof(f158,plain,
! [X0] :
( ~ sP10(X0)
| sP7(X0) ),
inference(cnf_transformation,[],[f86]) ).
fof(f159,plain,
! [X0] :
( ~ sP10(X0)
| sP8(X0) ),
inference(cnf_transformation,[],[f86]) ).
fof(f160,plain,
! [X0] :
( ~ sP10(X0)
| sP9(X0) ),
inference(cnf_transformation,[],[f86]) ).
fof(f161,plain,
! [X0,X1] :
( ~ sP10(X0)
| sP5(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f86]) ).
fof(f162,plain,
! [X2,X0,X1] :
( ~ sP9(X0)
| ~ r1(X1,X2)
| p2(X2)
| ~ p2(X1)
| sP4(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f89]) ).
fof(f164,plain,
! [X2,X0,X1,X4] :
( ~ sP8(X0)
| ~ r1(X1,X2)
| sP3(X2)
| ~ r1(sK42(X0),X4)
| ~ p2(X4)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f92]) ).
fof(f165,plain,
! [X2,X0,X1] :
( ~ sP8(X0)
| ~ r1(X1,X2)
| sP3(X2)
| r1(X0,sK42(X0))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f92]) ).
fof(f166,plain,
! [X3,X0,X1] :
( ~ sP7(X0)
| ~ r1(sK43(X1),X3)
| ~ p2(X3)
| sP2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f95]) ).
fof(f167,plain,
! [X0,X1] :
( ~ sP7(X0)
| r1(X1,sK43(X1))
| sP2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f95]) ).
fof(f168,plain,
! [X2,X0] :
( ~ sP6(X0)
| ~ r1(sK44(X0),X2)
| ~ p2(X2)
| sP0(X0) ),
inference(cnf_transformation,[],[f98]) ).
fof(f169,plain,
! [X0] :
( ~ sP6(X0)
| r1(X0,sK44(X0))
| sP0(X0) ),
inference(cnf_transformation,[],[f98]) ).
fof(f170,plain,
! [X0] :
( p2(sK45(X0))
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f101]) ).
fof(f172,plain,
! [X0] :
( ~ sP5(X0)
| r1(X0,sK45(X0)) ),
inference(cnf_transformation,[],[f101]) ).
fof(f173,plain,
! [X3,X0,X1] :
( ~ sP4(X0)
| ~ r1(sK47(X1),X3)
| ~ p2(X3)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f104]) ).
fof(f174,plain,
! [X0,X1] :
( ~ sP4(X0)
| r1(X1,sK47(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f104]) ).
fof(f175,plain,
! [X0] :
( p2(sK48(X0))
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f107]) ).
fof(f177,plain,
! [X0] :
( ~ sP3(X0)
| r1(X0,sK48(X0)) ),
inference(cnf_transformation,[],[f107]) ).
fof(f178,plain,
! [X2,X0] :
( ~ sP2(X0)
| sP1(X2)
| ~ r1(sK50(X0),X2) ),
inference(cnf_transformation,[],[f110]) ).
fof(f179,plain,
! [X0] :
( ~ sP2(X0)
| r1(X0,sK50(X0)) ),
inference(cnf_transformation,[],[f110]) ).
fof(f180,plain,
! [X0] :
( p2(sK51(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f113]) ).
fof(f182,plain,
! [X0] :
( ~ sP1(X0)
| r1(X0,sK51(X0)) ),
inference(cnf_transformation,[],[f113]) ).
fof(f183,plain,
! [X0] :
( p2(sK53(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f185,plain,
! [X0] :
( ~ sP0(X0)
| r1(X0,sK53(X0)) ),
inference(cnf_transformation,[],[f116]) ).
fof(f196,plain,
! [X35] :
( ~ p2(sK78(X35))
| ~ r1(sK77,X35) ),
inference(cnf_transformation,[],[f118]) ).
fof(f197,plain,
! [X35] :
( ~ r1(sK77,X35)
| r1(X35,sK78(X35)) ),
inference(cnf_transformation,[],[f118]) ).
fof(f198,plain,
r1(sK73,sK77),
inference(cnf_transformation,[],[f118]) ).
fof(f204,plain,
r1(sK69,sK73),
inference(cnf_transformation,[],[f118]) ).
fof(f210,plain,
r1(sK65,sK69),
inference(cnf_transformation,[],[f118]) ).
fof(f216,plain,
r1(sK61,sK65),
inference(cnf_transformation,[],[f118]) ).
fof(f222,plain,
r1(sK55,sK61),
inference(cnf_transformation,[],[f118]) ).
fof(f230,plain,
! [X5] :
( ~ r1(sK55,X5)
| sP26(X5) ),
inference(cnf_transformation,[],[f118]) ).
fof(f233,plain,
sP26(sK61),
inference(resolution,[],[f230,f222]) ).
fof(f283,plain,
! [X0] :
( ~ r1(sK61,X0)
| sP22(X0) ),
inference(resolution,[],[f122,f233]) ).
fof(f288,plain,
sP22(sK65),
inference(resolution,[],[f283,f216]) ).
fof(f292,plain,
! [X0] :
( ~ r1(sK65,X0)
| sP18(X0) ),
inference(resolution,[],[f288,f131]) ).
fof(f338,plain,
sP18(sK69),
inference(resolution,[],[f292,f210]) ).
fof(f348,plain,
! [X0] :
( ~ r1(sK69,X0)
| sP14(X0) ),
inference(resolution,[],[f338,f140]) ).
fof(f539,plain,
sP14(sK73),
inference(resolution,[],[f348,f204]) ).
fof(f541,plain,
! [X0] :
( ~ r1(sK73,X0)
| sP10(X0) ),
inference(resolution,[],[f539,f149]) ).
fof(f567,plain,
sP10(sK77),
inference(resolution,[],[f541,f198]) ).
fof(f569,plain,
! [X0] :
( ~ r1(sK77,X0)
| sP5(X0) ),
inference(resolution,[],[f567,f161]) ).
fof(f570,plain,
sP9(sK77),
inference(resolution,[],[f567,f160]) ).
fof(f571,plain,
sP8(sK77),
inference(resolution,[],[f567,f159]) ).
fof(f572,plain,
sP7(sK77),
inference(resolution,[],[f567,f158]) ).
fof(f573,plain,
sP6(sK77),
inference(resolution,[],[f567,f157]) ).
fof(f580,plain,
! [X0,X1] :
( ~ r1(sK77,X0)
| p2(X1)
| ~ p2(X0)
| sP4(X0)
| ~ r1(X0,X1) ),
inference(resolution,[],[f570,f162]) ).
fof(f581,plain,
! [X2,X0,X1] :
( ~ r1(X0,X1)
| sP3(X1)
| ~ r1(sK42(sK77),X2)
| ~ p2(X2)
| ~ r1(sK77,X0) ),
inference(resolution,[],[f571,f164]) ).
fof(f582,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| sP3(X1)
| r1(sK77,sK42(sK77))
| ~ r1(sK77,X0) ),
inference(resolution,[],[f571,f165]) ).
fof(f584,definition,
( spl84_19
<=> r1(sK77,sK42(sK77)) ),
introduced(definition,[new_symbols(definition,[spl84_19])],[avatar_definition]) ).
fof(f586,plain,
( r1(sK77,sK42(sK77))
| ~ spl84_19 ),
inference(avatar_component_clause,[],[f584]) ).
fof(f588,definition,
( spl84_20
<=> ! [X0,X1] :
( ~ r1(X0,X1)
| ~ r1(sK77,X0)
| sP3(X1) ) ),
introduced(definition,[new_symbols(definition,[spl84_20])],[avatar_definition]) ).
fof(f589,plain,
( ! [X0,X1] :
( ~ r1(sK77,X0)
| ~ r1(X0,X1)
| sP3(X1) )
| ~ spl84_20 ),
inference(avatar_component_clause,[],[f588]) ).
fof(f590,plain,
( spl84_19
| spl84_20 ),
inference(avatar_split_clause,[],[f582,f588,f584]) ).
fof(f592,definition,
( spl84_21
<=> ! [X2] :
( ~ r1(sK42(sK77),X2)
| ~ p2(X2) ) ),
introduced(definition,[new_symbols(definition,[spl84_21])],[avatar_definition]) ).
fof(f593,plain,
( ! [X2] :
( ~ r1(sK42(sK77),X2)
| ~ p2(X2) )
| ~ spl84_21 ),
inference(avatar_component_clause,[],[f592]) ).
fof(f594,plain,
( spl84_21
| spl84_20 ),
inference(avatar_split_clause,[],[f581,f588,f592]) ).
fof(f595,plain,
! [X0,X1] :
( ~ r1(sK77,X0)
| ~ p2(X1)
| sP2(X0)
| ~ r1(sK43(X0),X1) ),
inference(resolution,[],[f572,f166]) ).
fof(f596,plain,
! [X0] :
( ~ r1(sK77,X0)
| sP2(X0)
| r1(X0,sK43(X0)) ),
inference(resolution,[],[f572,f167]) ).
fof(f597,plain,
! [X0] :
( ~ r1(sK44(sK77),X0)
| ~ p2(X0)
| sP0(sK77) ),
inference(resolution,[],[f573,f168]) ).
fof(f598,plain,
( r1(sK77,sK44(sK77))
| sP0(sK77) ),
inference(resolution,[],[f573,f169]) ).
fof(f600,definition,
( spl84_22
<=> sP0(sK77) ),
introduced(definition,[new_symbols(definition,[spl84_22])],[avatar_definition]) ).
fof(f602,plain,
( sP0(sK77)
| ~ spl84_22 ),
inference(avatar_component_clause,[],[f600]) ).
fof(f604,definition,
( spl84_23
<=> r1(sK77,sK44(sK77)) ),
introduced(definition,[new_symbols(definition,[spl84_23])],[avatar_definition]) ).
fof(f606,plain,
( r1(sK77,sK44(sK77))
| ~ spl84_23 ),
inference(avatar_component_clause,[],[f604]) ).
fof(f607,plain,
( spl84_22
| spl84_23 ),
inference(avatar_split_clause,[],[f598,f604,f600]) ).
fof(f609,definition,
( spl84_24
<=> ! [X0] :
( ~ r1(sK44(sK77),X0)
| ~ p2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl84_24])],[avatar_definition]) ).
fof(f610,plain,
( ! [X0] :
( ~ r1(sK44(sK77),X0)
| ~ p2(X0) )
| ~ spl84_24 ),
inference(avatar_component_clause,[],[f609]) ).
fof(f611,plain,
( spl84_22
| spl84_24 ),
inference(avatar_split_clause,[],[f597,f609,f600]) ).
fof(f645,plain,
( r1(sK77,sK53(sK77))
| ~ spl84_22 ),
inference(resolution,[],[f602,f185]) ).
fof(f7211,plain,
( ! [X0] :
( ~ r1(sK53(sK77),X0)
| sP3(X0) )
| ~ spl84_20
| ~ spl84_22 ),
inference(resolution,[],[f589,f645]) ).
fof(f10386,plain,
( sP2(sK53(sK77))
| r1(sK53(sK77),sK43(sK53(sK77)))
| ~ spl84_22 ),
inference(resolution,[],[f596,f645]) ).
fof(f10408,definition,
( spl84_847
<=> r1(sK53(sK77),sK43(sK53(sK77))) ),
introduced(definition,[new_symbols(definition,[spl84_847])],[avatar_definition]) ).
fof(f10410,plain,
( r1(sK53(sK77),sK43(sK53(sK77)))
| ~ spl84_847 ),
inference(avatar_component_clause,[],[f10408]) ).
fof(f10412,definition,
( spl84_848
<=> sP2(sK53(sK77)) ),
introduced(definition,[new_symbols(definition,[spl84_848])],[avatar_definition]) ).
fof(f10414,plain,
( sP2(sK53(sK77))
| ~ spl84_848 ),
inference(avatar_component_clause,[],[f10412]) ).
fof(f10415,plain,
( spl84_847
| spl84_848
| ~ spl84_22 ),
inference(avatar_split_clause,[],[f10386,f600,f10412,f10408]) ).
fof(f10421,plain,
( sP5(sK44(sK77))
| ~ spl84_23 ),
inference(resolution,[],[f606,f569]) ).
fof(f10433,plain,
( r1(sK77,sK53(sK77))
| ~ spl84_22 ),
inference(resolution,[],[f602,f185]) ).
fof(f10654,plain,
( sP3(sK43(sK53(sK77)))
| ~ spl84_20
| ~ spl84_22
| ~ spl84_847 ),
inference(resolution,[],[f10410,f7211]) ).
fof(f10658,plain,
( r1(sK43(sK53(sK77)),sK48(sK43(sK53(sK77))))
| ~ spl84_20
| ~ spl84_22
| ~ spl84_847 ),
inference(resolution,[],[f10654,f177]) ).
fof(f10915,plain,
( ! [X0] :
( ~ p2(X0)
| sP2(sK53(sK77))
| ~ r1(sK43(sK53(sK77)),X0) )
| ~ spl84_22 ),
inference(resolution,[],[f595,f10433]) ).
fof(f10917,definition,
( spl84_885
<=> ! [X0] :
( ~ p2(X0)
| ~ r1(sK43(sK53(sK77)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl84_885])],[avatar_definition]) ).
fof(f10918,plain,
( ! [X0] :
( ~ r1(sK43(sK53(sK77)),X0)
| ~ p2(X0) )
| ~ spl84_885 ),
inference(avatar_component_clause,[],[f10917]) ).
fof(f10919,plain,
( spl84_848
| spl84_885
| ~ spl84_22 ),
inference(avatar_split_clause,[],[f10915,f600,f10917,f10412]) ).
fof(f10941,plain,
( ! [X0] :
( ~ r1(sK50(sK53(sK77)),X0)
| sP1(X0) )
| ~ spl84_848 ),
inference(resolution,[],[f10414,f178]) ).
fof(f10942,plain,
( r1(sK53(sK77),sK50(sK53(sK77)))
| ~ spl84_848 ),
inference(resolution,[],[f10414,f179]) ).
fof(f11275,plain,
( ! [X0] :
( p2(X0)
| ~ p2(sK53(sK77))
| sP4(sK53(sK77))
| ~ r1(sK53(sK77),X0) )
| ~ spl84_22 ),
inference(resolution,[],[f580,f10433]) ).
fof(f11277,definition,
( spl84_937
<=> sP4(sK53(sK77)) ),
introduced(definition,[new_symbols(definition,[spl84_937])],[avatar_definition]) ).
fof(f11279,plain,
( sP4(sK53(sK77))
| ~ spl84_937 ),
inference(avatar_component_clause,[],[f11277]) ).
fof(f11281,definition,
( spl84_938
<=> p2(sK53(sK77)) ),
introduced(definition,[new_symbols(definition,[spl84_938])],[avatar_definition]) ).
fof(f11283,plain,
( ~ p2(sK53(sK77))
| spl84_938 ),
inference(avatar_component_clause,[],[f11281]) ).
fof(f11285,definition,
( spl84_939
<=> ! [X0] :
( p2(X0)
| ~ r1(sK53(sK77),X0) ) ),
introduced(definition,[new_symbols(definition,[spl84_939])],[avatar_definition]) ).
fof(f11286,plain,
( ! [X0] :
( ~ r1(sK53(sK77),X0)
| p2(X0) )
| ~ spl84_939 ),
inference(avatar_component_clause,[],[f11285]) ).
fof(f11287,plain,
( spl84_937
| ~ spl84_938
| spl84_939
| ~ spl84_22 ),
inference(avatar_split_clause,[],[f11275,f600,f11285,f11281,f11277]) ).
fof(f11423,plain,
( ~ sP0(sK77)
| spl84_938 ),
inference(resolution,[],[f11283,f183]) ).
fof(f11424,plain,
( ~ spl84_22
| spl84_938 ),
inference(avatar_split_clause,[],[f11423,f11281,f600]) ).
fof(f11425,plain,
( ! [X0,X1] :
( ~ r1(sK47(X0),X1)
| ~ p2(X1)
| ~ r1(sK53(sK77),X0) )
| ~ spl84_937 ),
inference(resolution,[],[f11279,f173]) ).
fof(f11426,plain,
( ! [X0] :
( ~ r1(sK53(sK77),X0)
| r1(X0,sK47(X0)) )
| ~ spl84_937 ),
inference(resolution,[],[f11279,f174]) ).
fof(f14600,plain,
( r1(sK50(sK53(sK77)),sK47(sK50(sK53(sK77))))
| ~ spl84_848
| ~ spl84_937 ),
inference(resolution,[],[f11426,f10942]) ).
fof(f16464,plain,
( sP1(sK47(sK50(sK53(sK77))))
| ~ spl84_848
| ~ spl84_937 ),
inference(resolution,[],[f14600,f10941]) ).
fof(f16466,plain,
( r1(sK47(sK50(sK53(sK77))),sK51(sK47(sK50(sK53(sK77)))))
| ~ spl84_848
| ~ spl84_937 ),
inference(resolution,[],[f16464,f182]) ).
fof(f18853,plain,
( ~ p2(sK51(sK47(sK50(sK53(sK77)))))
| ~ r1(sK53(sK77),sK50(sK53(sK77)))
| ~ spl84_848
| ~ spl84_937 ),
inference(resolution,[],[f16466,f11425]) ).
fof(f18866,definition,
( spl84_1538
<=> p2(sK51(sK47(sK50(sK53(sK77))))) ),
introduced(definition,[new_symbols(definition,[spl84_1538])],[avatar_definition]) ).
fof(f18868,plain,
( ~ p2(sK51(sK47(sK50(sK53(sK77)))))
| spl84_1538 ),
inference(avatar_component_clause,[],[f18866]) ).
fof(f18900,plain,
( ~ p2(sK51(sK47(sK50(sK53(sK77)))))
| ~ spl84_848
| ~ spl84_937 ),
inference(global_subsumption,[],[f18853,f10942]) ).
fof(f18901,plain,
( ~ spl84_1538
| ~ spl84_848
| ~ spl84_937 ),
inference(avatar_split_clause,[],[f18900,f11277,f10412,f18866]) ).
fof(f18903,plain,
( ~ sP1(sK47(sK50(sK53(sK77))))
| spl84_1538 ),
inference(resolution,[],[f18868,f180]) ).
fof(f18905,plain,
( $false
| ~ spl84_848
| ~ spl84_937
| spl84_1538 ),
inference(resolution,[],[f18903,f16464]) ).
fof(f18906,plain,
( ~ spl84_848
| ~ spl84_937
| spl84_1538 ),
inference(avatar_contradiction_clause,[],[f18905]) ).
fof(f18911,plain,
( r1(sK44(sK77),sK45(sK44(sK77)))
| ~ spl84_23 ),
inference(resolution,[],[f10421,f172]) ).
fof(f18932,plain,
( ~ p2(sK45(sK44(sK77)))
| ~ spl84_23
| ~ spl84_24 ),
inference(resolution,[],[f18911,f610]) ).
fof(f18934,plain,
( ~ sP5(sK44(sK77))
| ~ spl84_23
| ~ spl84_24 ),
inference(resolution,[],[f18932,f170]) ).
fof(f18935,plain,
( $false
| ~ spl84_23
| ~ spl84_24 ),
inference(global_subsumption,[],[f18934,f10421]) ).
fof(f18936,plain,
( ~ spl84_23
| ~ spl84_24 ),
inference(avatar_contradiction_clause,[],[f18935]) ).
fof(f18942,plain,
( r1(sK77,sK53(sK77))
| ~ spl84_22 ),
inference(resolution,[],[f602,f185]) ).
fof(f18943,plain,
( r1(sK53(sK77),sK78(sK53(sK77)))
| ~ spl84_22 ),
inference(resolution,[],[f18942,f197]) ).
fof(f18960,plain,
( p2(sK78(sK53(sK77)))
| ~ spl84_22
| ~ spl84_939 ),
inference(resolution,[],[f18943,f11286]) ).
fof(f18964,plain,
( ~ r1(sK77,sK53(sK77))
| ~ spl84_22
| ~ spl84_939 ),
inference(resolution,[],[f18960,f196]) ).
fof(f18965,plain,
( $false
| ~ spl84_22
| ~ spl84_939 ),
inference(global_subsumption,[],[f18964,f18942]) ).
fof(f18966,plain,
( ~ spl84_22
| ~ spl84_939 ),
inference(avatar_contradiction_clause,[],[f18965]) ).
fof(f19012,plain,
( ~ p2(sK48(sK43(sK53(sK77))))
| ~ spl84_20
| ~ spl84_22
| ~ spl84_847
| ~ spl84_885 ),
inference(resolution,[],[f10658,f10918]) ).
fof(f19022,definition,
( spl84_1553
<=> p2(sK48(sK43(sK53(sK77)))) ),
introduced(definition,[new_symbols(definition,[spl84_1553])],[avatar_definition]) ).
fof(f19024,plain,
( ~ p2(sK48(sK43(sK53(sK77))))
| spl84_1553 ),
inference(avatar_component_clause,[],[f19022]) ).
fof(f19041,plain,
( ~ spl84_1553
| ~ spl84_20
| ~ spl84_22
| ~ spl84_847
| ~ spl84_885 ),
inference(avatar_split_clause,[],[f19012,f10917,f10408,f600,f588,f19022]) ).
fof(f19043,plain,
( ~ sP3(sK43(sK53(sK77)))
| spl84_1553 ),
inference(resolution,[],[f19024,f175]) ).
fof(f19045,plain,
( $false
| ~ spl84_20
| ~ spl84_22
| ~ spl84_847
| spl84_1553 ),
inference(resolution,[],[f19043,f10654]) ).
fof(f19046,plain,
( ~ spl84_20
| ~ spl84_22
| ~ spl84_847
| spl84_1553 ),
inference(avatar_contradiction_clause,[],[f19045]) ).
fof(f19048,plain,
( sP5(sK42(sK77))
| ~ spl84_19 ),
inference(resolution,[],[f586,f569]) ).
fof(f19083,plain,
( r1(sK42(sK77),sK45(sK42(sK77)))
| ~ spl84_19 ),
inference(resolution,[],[f19048,f172]) ).
fof(f19088,plain,
( ~ p2(sK45(sK42(sK77)))
| ~ spl84_19
| ~ spl84_21 ),
inference(resolution,[],[f19083,f593]) ).
fof(f19090,plain,
( ~ sP5(sK42(sK77))
| ~ spl84_19
| ~ spl84_21 ),
inference(resolution,[],[f19088,f170]) ).
fof(f19091,plain,
( $false
| ~ spl84_19
| ~ spl84_21 ),
inference(global_subsumption,[],[f19090,f19048]) ).
fof(f19092,plain,
( ~ spl84_19
| ~ spl84_21 ),
inference(avatar_contradiction_clause,[],[f19091]) ).
cnf(s414,plain,
( spl84_19
| spl84_20 ),
inference(sat_conversion,[],[f590]) ).
cnf(s416,plain,
( spl84_20
| spl84_21 ),
inference(sat_conversion,[],[f594]) ).
cnf(s421,plain,
( spl84_22
| spl84_23 ),
inference(sat_conversion,[],[f607]) ).
cnf(s423,plain,
( spl84_22
| spl84_24 ),
inference(sat_conversion,[],[f611]) ).
cnf(s7510,plain,
( ~ spl84_22
| spl84_847
| spl84_848 ),
inference(sat_conversion,[],[f10415]) ).
cnf(s7890,plain,
( ~ spl84_22
| spl84_848
| spl84_885 ),
inference(sat_conversion,[],[f10919]) ).
cnf(s8075,plain,
( ~ spl84_22
| spl84_937
| ~ spl84_938
| spl84_939 ),
inference(sat_conversion,[],[f11287]) ).
cnf(s8111,plain,
( ~ spl84_22
| spl84_938 ),
inference(sat_conversion,[],[f11424]) ).
cnf(s13372,plain,
( ~ spl84_848
| ~ spl84_937
| ~ spl84_1538 ),
inference(sat_conversion,[],[f18901]) ).
cnf(s13377,plain,
( ~ spl84_848
| ~ spl84_937
| spl84_1538 ),
inference(sat_conversion,[],[f18906]) ).
cnf(s13405,plain,
( ~ spl84_23
| ~ spl84_24 ),
inference(sat_conversion,[],[f18936]) ).
cnf(s13435,plain,
( ~ spl84_22
| ~ spl84_939 ),
inference(sat_conversion,[],[f18966]) ).
cnf(s13468,plain,
( ~ spl84_20
| ~ spl84_22
| ~ spl84_847
| ~ spl84_885
| ~ spl84_1553 ),
inference(sat_conversion,[],[f19041]) ).
cnf(s13473,plain,
( ~ spl84_20
| ~ spl84_22
| ~ spl84_847
| spl84_1553 ),
inference(sat_conversion,[],[f19046]) ).
cnf(s13497,plain,
( ~ spl84_19
| ~ spl84_21 ),
inference(sat_conversion,[],[f19092]) ).
cnf(s13504,plain,
spl84_22,
inference(rat,[],[s13405,s421,s423]) ).
cnf(s13505,plain,
~ spl84_939,
inference(rat,[],[s13435,s13504]) ).
cnf(s13506,plain,
spl84_938,
inference(rat,[],[s8111,s13504]) ).
cnf(s13507,plain,
spl84_937,
inference(rat,[],[s8075,s13505,s13506,s13504]) ).
cnf(s13515,plain,
~ spl84_848,
inference(rat,[],[s13372,s13377,s13507]) ).
cnf(s13516,plain,
spl84_885,
inference(rat,[],[s7890,s13504,s13515]) ).
cnf(s13517,plain,
spl84_847,
inference(rat,[],[s7510,s13504,s13515]) ).
cnf(s13518,plain,
~ spl84_20,
inference(rat,[],[s13468,s13473,s13517,s13504,s13516]) ).
cnf(s13519,plain,
spl84_21,
inference(rat,[],[s416,s13518]) ).
cnf(s13520,plain,
spl84_19,
inference(rat,[],[s414,s13518]) ).
cnf(s13521,plain,
$false,
inference(rat,[],[s13497,s13519,s13520]) ).
fof(f19093,plain,
$false,
inference(avatar_sat_refutation,[],[s13521]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL652+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39 % Computer : n013.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 16:16:07 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 Running first-order model finding
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.70/3.52 % (387642)Will run a generic schedule for satisfiability detection.
% 21.70/3.52 % (387647)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1167513507_2999 on theBenchmark for (2999ds/0Mi)
% 21.70/3.52 % (387648)% WARNING: option uhcvi not known.
% 21.70/3.52 % TRYING [1]
% 21.70/3.52 % TRYING [2]
% 21.70/3.52 % (387648)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1082100373:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 21.70/3.52 % (387649)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=451348580:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 21.70/3.52 % (387650)dis+10_1_sil=32000:sp=arity:random_seed=3680453142:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 21.70/3.52 % (387652)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4062575737:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 21.70/3.52 % (387651)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1054394526:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 21.70/3.52 % (387653)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1402148431:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 21.70/3.52 % TRYING [3]
% 21.70/3.52 % TRYING [4]
% 21.70/3.52 % (387651)Instruction limit reached!
% 21.70/3.52 % (387651)------------------------------
% 21.70/3.52 % (387651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.70/3.52 % (387651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.70/3.52 % (387651)CaDiCaL version: 2.1.3
% 21.70/3.52 % (387651)Termination reason: Instruction limit
% 21.70/3.52 % (387651)Termination phase: Saturation
% 21.70/3.52 % (387651)Time elapsed: 0.055 s
% 21.70/3.52 % (387651)Peak memory usage: 12 MB
% 21.70/3.52 % (387651)Instructions burned: 118 (million)
% 21.70/3.52 % (387650)Instruction limit reached!
% 21.70/3.52 % (387650)------------------------------
% 21.70/3.52 % (387650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.70/3.52 % (387650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.70/3.52 % (387650)CaDiCaL version: 2.1.3
% 21.70/3.52 % (387650)Termination reason: Instruction limit
% 21.70/3.52 % (387650)Termination phase: Saturation
% 21.70/3.52 % (387650)Time elapsed: 0.058 s
% 21.70/3.52 % (387650)Peak memory usage: 14 MB
% 21.70/3.52 % (387650)Instructions burned: 104 (million)
% 21.70/3.52 % (387652)Instruction limit reached!
% 21.70/3.52 % (387652)------------------------------
% 21.70/3.52 % (387652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.70/3.52 % (387652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.70/3.52 % (387652)CaDiCaL version: 2.1.3
% 21.70/3.52 % (387652)Termination reason: Instruction limit
% 21.70/3.52 % (387652)Termination phase: Saturation
% 21.70/3.52 % (387652)Time elapsed: 0.069 s
% 21.70/3.52 % (387652)Peak memory usage: 13 MB
% 21.70/3.52 % (387652)Instructions burned: 131 (million)
% 21.70/3.52 % TRYING [5]
% 21.70/3.52 % (387662)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3947950394:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 21.70/3.52 % (387661)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2173587135:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 21.70/3.52 % (387653)Instruction limit reached!
% 21.70/3.52 % (387653)------------------------------
% 21.70/3.52 % (387653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.70/3.52 % (387653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.70/3.52 % (387653)CaDiCaL version: 2.1.3
% 21.70/3.52 % (387653)Termination reason: Instruction limit
% 21.70/3.52 % (387653)Termination phase: Saturation
% 21.70/3.52 % (387653)Time elapsed: 0.085 s
% 21.70/3.52 % (387653)Peak memory usage: 14 MB
% 21.70/3.52 % (387653)Instructions burned: 159 (million)
% 21.70/3.52 % TRYING [1]
% 21.70/3.52 % TRYING [2]
% 21.70/3.52 % (387663)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3477137672:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 21.70/3.52 % TRYING [3]
% 21.70/3.52 % TRYING [4]
% 21.70/3.52 % (387666)ott-21_1_sil=16000:fs=off:random_seed=2091857552:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 21.70/3.52 % (387662)Instruction limit reached!
% 21.70/3.52 % (387662)------------------------------
% 21.70/3.52 % (387662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.70/3.52 % (387662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.35/7.67 % (387662)CaDiCaL version: 2.1.3
% 50.35/7.67 % (387662)Termination reason: Instruction limit
% 50.35/7.67 % (387662)Termination phase: Saturation
% 50.35/7.67 % (387662)Time elapsed: 0.072 s
% 50.35/7.67 % (387662)Peak memory usage: 13 MB
% 50.35/7.67 % (387662)Instructions burned: 132 (million)
% 50.35/7.67 % (387669)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2534377964:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 50.35/7.67 % TRYING [5]
% 50.35/7.67 % (387666)Instruction limit reached!
% 50.35/7.67 % (387666)------------------------------
% 50.35/7.67 % (387666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.35/7.67 % (387666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.35/7.67 % (387666)CaDiCaL version: 2.1.3
% 50.35/7.67 % (387666)Termination reason: Instruction limit
% 50.35/7.67 % (387666)Termination phase: Saturation
% 50.35/7.67 % (387666)Time elapsed: 0.089 s
% 50.35/7.67 % (387666)Peak memory usage: 13 MB
% 50.35/7.67 % (387666)Instructions burned: 180 (million)
% 50.35/7.67 % (387671)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1118420166:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 50.35/7.67 % TRYING [1]
% 50.35/7.67 % TRYING [2]
% 50.35/7.67 % TRYING [3]
% 50.35/7.67 % TRYING [4]
% 50.35/7.67 % TRYING [5]
% 50.35/7.67 % (387669)Instruction limit reached!
% 50.35/7.67 % (387669)------------------------------
% 50.35/7.67 % (387669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.35/7.67 % (387669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.35/7.67 % (387669)CaDiCaL version: 2.1.3
% 50.35/7.67 % (387669)Termination reason: Instruction limit
% 50.35/7.67 % (387669)Termination phase: Saturation
% 50.35/7.67 % (387669)Time elapsed: 0.261 s
% 50.35/7.67 % (387669)Peak memory usage: 15 MB
% 50.35/7.67 % (387669)Instructions burned: 477 (million)
% 50.35/7.67 % (387673)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2190972001:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 50.35/7.67 % (387663)Instruction limit reached!
% 50.35/7.67 % (387663)------------------------------
% 50.35/7.67 % (387663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.35/7.67 % (387663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.35/7.67 % (387663)CaDiCaL version: 2.1.3
% 50.35/7.67 % (387663)Termination reason: Instruction limit
% 50.35/7.67 % (387663)Termination phase: Saturation
% 50.35/7.67 % (387663)Time elapsed: 0.370 s
% 50.35/7.67 % (387663)Peak memory usage: 18 MB
% 50.35/7.67 % (387663)Instructions burned: 686 (million)
% 50.35/7.67 % (387661)Instruction limit reached!
% 50.35/7.67 % (387661)------------------------------
% 50.35/7.67 % (387661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.35/7.67 % (387661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.35/7.67 % (387661)CaDiCaL version: 2.1.3
% 50.35/7.67 % (387661)Termination reason: Instruction limit
% 50.35/7.67 % (387661)Termination phase: Finite model building SAT solving
% 50.35/7.67 % (387661)Time elapsed: 0.394 s
% 50.35/7.67 % (387661)Peak memory usage: 14 MB
% 50.35/7.67 % (387661)Instructions burned: 715 (million)
% 50.35/7.67 % (387675)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3686542179:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 50.35/7.67 % (387676)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=4082240290:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 50.35/7.67 % TRYING [14]
% 50.35/7.67 % TRYING [6]
% 50.35/7.67 % (387671)Instruction limit reached!
% 50.35/7.67 % (387671)------------------------------
% 50.35/7.67 % (387671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.35/7.67 % (387671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.35/7.67 % (387671)CaDiCaL version: 2.1.3
% 50.35/7.67 % (387671)Termination reason: Instruction limit
% 50.35/7.67 % (387671)Termination phase: Finite model building SAT solving
% 50.35/7.67 % (387671)Time elapsed: 0.447 s
% 50.35/7.67 % (387671)Peak memory usage: 14 MB
% 50.35/7.67 % (387671)Instructions burned: 866 (million)
% 50.35/7.67 % (387679)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3945517242:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 50.35/7.67 % (387675)Instruction limit reached!
% 50.35/7.67 % (387675)------------------------------
% 50.35/7.67 % (387675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.66/8.92 % (387675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.66/8.92 % (387675)CaDiCaL version: 2.1.3
% 58.66/8.92 % (387675)Termination reason: Instruction limit
% 58.66/8.92 % (387675)Termination phase: Finite model building SAT solving
% 58.66/8.92 % (387675)Time elapsed: 0.299 s
% 58.66/8.92 % (387675)Peak memory usage: 29 MB
% 58.66/8.92 % (387675)Instructions burned: 890 (million)
% 58.66/8.92 % (387681)fmb+10_1_sil=64000:random_seed=2371432321:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 58.66/8.92 % TRYING [1]
% 58.66/8.92 % TRYING [2]
% 58.66/8.92 % TRYING [3]
% 58.66/8.92 % TRYING [4]
% 58.66/8.92 % (387676)Instruction limit reached!
% 58.66/8.92 % (387676)------------------------------
% 58.66/8.92 % (387676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.66/8.92 % (387676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.66/8.92 % (387676)CaDiCaL version: 2.1.3
% 58.66/8.92 % (387676)Termination reason: Instruction limit
% 58.66/8.92 % (387676)Termination phase: Saturation
% 58.66/8.92 % (387676)Time elapsed: 0.354 s
% 58.66/8.92 % (387676)Peak memory usage: 17 MB
% 58.66/8.92 % (387676)Instructions burned: 693 (million)
% 58.66/8.92 % TRYING [5]
% 58.66/8.92 % (387683)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2292673005:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 58.66/8.92 % TRYING [20]
% 58.66/8.92 % (387673)Instruction limit reached!
% 58.66/8.92 % (387673)------------------------------
% 58.66/8.92 % (387673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.66/8.92 % (387673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.66/8.92 % (387673)CaDiCaL version: 2.1.3
% 58.66/8.92 % (387673)Termination reason: Instruction limit
% 58.66/8.92 % (387673)Termination phase: Saturation
% 58.66/8.92 % (387673)Time elapsed: 0.599 s
% 58.66/8.92 % (387673)Peak memory usage: 29 MB
% 58.66/8.92 % (387673)Instructions burned: 1180 (million)
% 58.66/8.92 % (387679)Instruction limit reached!
% 58.66/8.92 % (387679)------------------------------
% 58.66/8.92 % (387679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.66/8.92 % (387679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.66/8.92 % (387679)CaDiCaL version: 2.1.3
% 58.66/8.92 % (387679)Termination reason: Instruction limit
% 58.66/8.92 % (387679)Termination phase: Saturation
% 58.66/8.92 % (387679)Time elapsed: 0.388 s
% 58.66/8.92 % (387679)Peak memory usage: 17 MB
% 58.66/8.92 % (387679)Instructions burned: 881 (million)
% 58.66/8.92 % (387685)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=749601432:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 58.66/8.92 % TRYING [8]
% 58.66/8.92 % (387686)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1874945565:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 58.66/8.92 % TRYING [6]
% 58.66/8.92 % (387685)Instruction limit reached!
% 58.66/8.92 % (387685)------------------------------
% 58.66/8.92 % (387685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.66/8.92 % (387685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.66/8.92 % (387685)CaDiCaL version: 2.1.3
% 58.66/8.92 % (387685)Termination reason: Instruction limit
% 58.66/8.92 % (387685)Termination phase: Finite model building SAT solving
% 58.66/8.92 % (387685)Time elapsed: 0.485 s
% 58.66/8.92 % (387685)Peak memory usage: 22 MB
% 58.66/8.92 % (387685)Instructions burned: 921 (million)
% 58.66/8.92 % (387689)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2751301061:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 58.66/8.92 % (387689)Instruction limit reached!
% 58.66/8.92 % (387689)------------------------------
% 58.66/8.92 % (387689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.66/8.92 % (387689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.66/8.92 % (387689)CaDiCaL version: 2.1.3
% 58.66/8.92 % (387689)Termination reason: Instruction limit
% 58.66/8.92 % (387689)Termination phase: Saturation
% 58.66/8.92 % (387689)Time elapsed: 0.619 s
% 58.66/8.92 % (387689)Peak memory usage: 23 MB
% 58.66/8.92 % (387689)Instructions burned: 1473 (million)
% 58.66/8.92 % (387691)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=215918613:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 58.66/8.92 % TRYING [77]
% 58.66/8.92 % (387686)Instruction limit reached!
% 58.66/8.92 % (387686)------------------------------
% 58.66/8.92 % (387686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.66/8.92 % (387686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.66/8.92 % (387686)CaDiCaL version: 2.1.3
% 58.66/8.92 % (387686)Termination reason: Instruction limit
% 58.66/8.92 % (387686)Termination phase: Saturation
% 58.66/8.92 % (387686)Time elapsed: 1.964 s
% 58.66/8.92 % (387686)Peak memory usage: 18 MB
% 58.66/8.92 % (387686)Instructions burned: 5132 (million)
% 58.66/8.92 % (387693)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3513122097:fmbsr=2.30978:i=2174_2969 on theBenchmark for (2969ds/2174Mi)
% 58.66/8.92 % TRYING [16]
% 58.66/8.92 % (387693)Instruction limit reached!
% 58.66/8.92 % (387693)------------------------------
% 58.66/8.92 % (387693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.66/8.92 % (387693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.66/8.92 % (387693)CaDiCaL version: 2.1.3
% 58.66/8.92 % (387693)Termination reason: Instruction limit
% 58.66/8.92 % (387693)Termination phase: Finite model building SAT solving
% 58.66/8.92 % (387693)Time elapsed: 1.083 s
% 58.66/8.92 % (387693)Peak memory usage: 58 MB
% 58.66/8.92 % (387693)Instructions burned: 2174 (million)
% 58.66/8.92 % (387695)ott-2_1_sil=16000:newcnf=on:random_seed=125024049:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 58.66/8.92 % (387695)Instruction limit reached!
% 58.66/8.92 % (387695)------------------------------
% 58.66/8.92 % (387695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.66/8.92 % (387695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.66/8.92 % (387695)CaDiCaL version: 2.1.3
% 58.66/8.92 % (387695)Termination reason: Instruction limit
% 58.66/8.92 % (387695)Termination phase: Saturation
% 58.66/8.92 % (387695)Time elapsed: 0.460 s
% 58.66/8.92 % (387695)Peak memory usage: 16 MB
% 58.66/8.92 % (387695)Instructions burned: 870 (million)
% 58.66/8.92 % (387697)ott+10_1_sil=32000:tgt=ground:random_seed=2820426210:i=5114:av=off_2953 on theBenchmark for (2953ds/5114Mi)
% 58.66/8.92 % (387691)Instruction limit reached!
% 58.66/8.92 % (387691)------------------------------
% 58.66/8.92 % (387691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.66/8.92 % (387691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.66/8.92 % (387691)CaDiCaL version: 2.1.3
% 58.66/8.92 % (387691)Termination reason: Instruction limit
% 58.66/8.92 % (387691)Termination phase: Finite model building constraint generation
% 58.66/8.92 % (387691)Time elapsed: 2.448 s
% 58.66/8.92 % (387691)Peak memory usage: 531 MB
% 58.66/8.92 % (387691)Instructions burned: 6326 (million)
% 58.66/8.92 % (387699)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=597114537:i=54282_2952 on theBenchmark for (2952ds/54282Mi)
% 58.66/8.92 % TRYING [1]
% 58.66/8.92 % TRYING [2]
% 58.66/8.92 % TRYING [3]
% 58.66/8.92 % TRYING [4]
% 58.66/8.92 % (387683)Instruction limit reached!
% 58.66/8.92 % (387683)------------------------------
% 58.66/8.92 % (387683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.66/8.92 % (387683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.66/8.92 % (387683)CaDiCaL version: 2.1.3
% 58.66/8.92 % (387683)Termination reason: Instruction limit
% 58.66/8.92 % (387683)Termination phase: Finite model building SAT solving
% 58.66/8.92 % (387683)Time elapsed: 3.935 s
% 58.66/8.92 % (387683)Peak memory usage: 87 MB
% 58.66/8.92 % (387683)Instructions burned: 9515 (million)
% 58.66/8.92 % (387701)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4063579366:i=3512:aac=none_2951 on theBenchmark for (2951ds/3512Mi)
% 58.66/8.92 % TRYING [5]
% 58.66/8.92 % TRYING [6]
% 58.66/8.92 % (387701)Instruction limit reached!
% 58.66/8.92 % (387701)------------------------------
% 58.66/8.92 % (387701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.66/8.92 % (387701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.66/8.92 % (387701)CaDiCaL version: 2.1.3
% 58.66/8.92 % (387701)Termination reason: Instruction limit
% 58.66/8.92 % (387701)Termination phase: Saturation
% 58.66/8.92 % (387701)Time elapsed: 1.811 s
% 58.66/8.92 % (387701)Peak memory usage: 26 MB
% 58.66/8.92 % (387701)Instructions burned: 3512 (million)
% 58.66/8.92 % (387703)dis+21_1_sil=32000:sas=cadical:random_seed=1212575773:i=3773:amm=off_2933 on theBenchmark for (2933ds/3773Mi)
% 58.66/8.92 % (387697)Instruction limit reached!
% 58.66/8.92 % (387697)------------------------------
% 58.66/8.92 % (387697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.66/8.92 % (387697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.66/8.92 % (387697)CaDiCaL version: 2.1.3
% 58.66/8.92 % (387697)Termination reason: Instruction limit
% 58.66/8.92 % (387697)Termination phase: Saturation
% 58.66/8.92 % (387697)Time elapsed: 2.539 s
% 58.66/8.92 % (387697)Peak memory usage: 43 MB
% 58.66/8.92 % (387697)Instructions burned: 5114 (million)
% 58.66/8.92 % (387705)ott+11_1_sil=16000:gs=on:random_seed=4211855604:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2927 on theBenchmark for (2927ds/2251Mi)
% 58.66/8.92 % (387703)Instruction limit reached!
% 58.66/8.92 % (387703)------------------------------
% 58.66/8.92 % (387703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.66/8.92 % (387703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.66/8.92 % (387703)CaDiCaL version: 2.1.3
% 58.66/8.92 % (387703)Termination reason: Instruction limit
% 58.66/8.92 % (387703)Termination phase: Saturation
% 58.66/8.92 % (387703)Time elapsed: 1.625 s
% 58.66/8.92 % (387703)Peak memory usage: 45 MB
% 58.66/8.92 % (387703)Instructions burned: 3775 (million)
% 58.66/8.92 % (387707)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=680621494:fmbsr=1.6:i=67534_2916 on theBenchmark for (2916ds/67534Mi)
% 58.66/8.92 % TRYING [7]
% 58.66/8.92 % (387705) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-387642-387705"...
% 58.66/8.92 % (387705)...printing done.
% 58.66/8.92 % (387705)Refutation found. Thanks to Tanya!
% 58.66/8.92 % SZS status Theorem for theBenchmark
% 58.66/8.92 % SZS output start Proof for theBenchmark
% See solution above
% 58.66/8.92 % (387705)------------------------------
% 58.66/8.92 % (387705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.66/8.92 % (387705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.66/8.92 % (387705)CaDiCaL version: 2.1.3
% 58.66/8.92 % (387705)Termination reason: Refutation
% 58.66/8.92 % (387705)Time elapsed: 1.195 s
% 58.66/8.92 % (387705)Peak memory usage: 27 MB
% 58.66/8.92 % (387705)Instructions burned: 1954 (million)
% 58.66/8.92 % (387642)Success in time 8.486 s
% 58.66/8.92 % Vampire exiting
%------------------------------------------------------------------------------