%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL658+1.001 : 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 : n004.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:29 AM UTC 2026
% Result : Theorem 12.11s 2.17s
% Output : Refutation 12.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 40
% Syntax : Number of formulae : 460 ( 25 unt; 38 def)
% Number of atoms : 2446 ( 0 equ)
% Maximal formula atoms : 62 ( 5 avg)
% Number of connectives : 3624 (1638 ~;1906 |; 42 &)
% ( 38 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 42 ( 41 usr; 39 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 4 con; 0-1 aty)
% Number of variables : 715 ( 0 sgn 694 !; 21 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : r1(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity) ).
fof(f2,conjecture,
~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ( ( ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) )
| ~ ( ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) ) )
& ( p1(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)
| p1(X0) )
| ~ p1(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)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) ) ) )
| ~ ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',main) ).
fof(f3,negated_conjecture,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ( ( ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) )
| ~ ( ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) ) )
& ( p1(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)
| p1(X0) )
| ~ p1(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)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) ) ) )
| ~ ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f2]) ).
fof(f4,plain,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ( ( ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
| ~ p1(X1)
| ! [X3] :
( ~ r1(X1,X3)
| ~ ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p1(X5) )
| ~ p1(X4) ) )
| ~ ! [X6] :
( ~ r1(X1,X6)
| ! [X7] :
( ~ r1(X6,X7)
| p1(X7) )
| ~ p1(X6)
| ~ ! [X8] :
( ~ r1(X6,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| p1(X10) )
| ~ p1(X9) )
| ~ ( ! [X11] :
( ~ r1(X8,X11)
| p1(X11) )
| ~ p1(X8) ) ) ) )
& ( p1(X1)
| ! [X12] :
( ~ r1(X1,X12)
| ~ ! [X13] :
( ~ r1(X12,X13)
| p1(X13) ) )
| ~ ! [X14] :
( ~ r1(X1,X14)
| p1(X14)
| ~ ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| p1(X16) )
| ~ p1(X15) ) ) )
& ! [X17] :
( ~ r1(X1,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p1(X19) ) )
| ~ ! [X20] :
( ~ r1(X17,X20)
| p1(X20) ) )
& ( ! [X21] :
( ~ r1(X1,X21)
| ! [X22] :
( ~ r1(X21,X22)
| p1(X22)
| ~ ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| p1(X24) )
| ~ p1(X23) ) ) )
| ~ ! [X25] :
( ~ r1(X1,X25)
| p1(X25)
| ~ ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| p1(X27) )
| ~ p1(X26) ) ) ) ) )
| ~ ~ ! [X28] :
( ~ r1(X0,X28)
| ! [X29] :
( ~ r1(X28,X29)
| p1(X29) )
| ! [X30] :
( ~ r1(X28,X30)
| ~ ! [X31] :
( ~ r1(X30,X31)
| p1(X31) ) )
| ~ ! [X32] :
( ~ r1(X28,X32)
| p1(X32)
| ~ ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) )
| ~ p1(X33) ) ) ) ),
inference(rectify,[],[f3]) ).
fof(f5,plain,
? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ( ( ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
| ~ p1(X1)
| ! [X3] :
( ~ r1(X1,X3)
| ~ ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p1(X5) )
| ~ p1(X4) ) )
| ~ ! [X6] :
( ~ r1(X1,X6)
| ! [X7] :
( ~ r1(X6,X7)
| p1(X7) )
| ~ p1(X6)
| ~ ! [X8] :
( ~ r1(X6,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| p1(X10) )
| ~ p1(X9) )
| ~ ( ! [X11] :
( ~ r1(X8,X11)
| p1(X11) )
| ~ p1(X8) ) ) ) )
& ( p1(X1)
| ! [X12] :
( ~ r1(X1,X12)
| ~ ! [X13] :
( ~ r1(X12,X13)
| p1(X13) ) )
| ~ ! [X14] :
( ~ r1(X1,X14)
| p1(X14)
| ~ ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| p1(X16) )
| ~ p1(X15) ) ) )
& ! [X17] :
( ~ r1(X1,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p1(X19) ) )
| ~ ! [X20] :
( ~ r1(X17,X20)
| p1(X20) ) )
& ( ! [X21] :
( ~ r1(X1,X21)
| ! [X22] :
( ~ r1(X21,X22)
| p1(X22)
| ~ ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| p1(X24) )
| ~ p1(X23) ) ) )
| ~ ! [X25] :
( ~ r1(X1,X25)
| p1(X25)
| ~ ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| p1(X27) )
| ~ p1(X26) ) ) ) ) )
| ! [X28] :
( ~ r1(X0,X28)
| ! [X29] :
( ~ r1(X28,X29)
| p1(X29) )
| ! [X30] :
( ~ r1(X28,X30)
| ~ ! [X31] :
( ~ r1(X30,X31)
| p1(X31) ) )
| ~ ! [X32] :
( ~ r1(X28,X32)
| p1(X32)
| ~ ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) )
| ~ p1(X33) ) ) ) ),
inference(flattening,[],[f4]) ).
fof(f6,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ( ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
| ~ p1(X1)
| ! [X3] :
( ~ r1(X1,X3)
| ? [X4] :
( r1(X3,X4)
& ? [X5] :
( r1(X4,X5)
& ~ p1(X5) )
& p1(X4) ) )
| ? [X6] :
( r1(X1,X6)
& ? [X7] :
( r1(X6,X7)
& ~ p1(X7) )
& p1(X6)
& ! [X8] :
( ~ r1(X6,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| p1(X10) )
| ~ p1(X9) )
| ( ? [X11] :
( r1(X8,X11)
& ~ p1(X11) )
& p1(X8) ) ) ) )
& ( p1(X1)
| ! [X12] :
( ~ r1(X1,X12)
| ? [X13] :
( r1(X12,X13)
& ~ p1(X13) ) )
| ? [X14] :
( r1(X1,X14)
& ~ p1(X14)
& ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| p1(X16) )
| ~ p1(X15) ) ) )
& ! [X17] :
( ~ r1(X1,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p1(X19) ) )
| ? [X20] :
( r1(X17,X20)
& ~ p1(X20) ) )
& ( ! [X21] :
( ~ r1(X1,X21)
| ! [X22] :
( ~ r1(X21,X22)
| p1(X22)
| ? [X23] :
( r1(X22,X23)
& ? [X24] :
( r1(X23,X24)
& ~ p1(X24) )
& p1(X23) ) ) )
| ? [X25] :
( r1(X1,X25)
& ~ p1(X25)
& ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| p1(X27) )
| ~ p1(X26) ) ) ) ) )
& ? [X28] :
( r1(X0,X28)
& ? [X29] :
( r1(X28,X29)
& ~ p1(X29) )
& ? [X30] :
( r1(X28,X30)
& ! [X31] :
( ~ r1(X30,X31)
| p1(X31) ) )
& ! [X32] :
( ~ r1(X28,X32)
| p1(X32)
| ? [X33] :
( r1(X32,X33)
& ? [X34] :
( r1(X33,X34)
& ~ p1(X34) )
& p1(X33) ) ) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f7,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f8,plain,
! [X10,X9] :
( p1(X10)
| ~ r1(X9,X10)
| ~ sP17(X9) ),
inference(cnf_transformation,[],[f6]) ).
fof(f9,plain,
! [X21,X1,X26,X27,X22] :
( ~ p1(X26)
| p1(X27)
| ~ r1(X26,X27)
| ~ r1(sK5(X1),X26)
| ~ p1(sK16(X22))
| p1(X22)
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f10,plain,
! [X21,X1,X26,X27,X22] :
( ~ p1(X26)
| p1(X27)
| ~ r1(X26,X27)
| ~ r1(sK5(X1),X26)
| r1(sK13(X22),sK16(X22))
| p1(X22)
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f11,plain,
! [X21,X1,X22] :
( ~ p1(sK5(X1))
| ~ p1(sK16(X22))
| p1(X22)
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f12,plain,
! [X21,X1,X22] :
( ~ p1(sK5(X1))
| r1(sK13(X22),sK16(X22))
| p1(X22)
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f13,plain,
! [X21,X1,X22] :
( r1(X1,sK5(X1))
| ~ p1(sK16(X22))
| p1(X22)
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f14,plain,
! [X21,X1,X22] :
( r1(X1,sK5(X1))
| r1(sK13(X22),sK16(X22))
| p1(X22)
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f23,plain,
! [X2,X3,X1] :
( ~ p1(sK11(X1))
| ~ p1(sK14(X3))
| ~ r1(X1,X3)
| ~ p1(X1)
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f24,plain,
! [X2,X3,X1] :
( ~ p1(sK11(X1))
| r1(sK12(X3),sK14(X3))
| ~ r1(X1,X3)
| ~ p1(X1)
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f25,plain,
! [X2,X3,X1] :
( r1(sK7(X1),sK11(X1))
| ~ p1(sK14(X3))
| ~ r1(X1,X3)
| ~ p1(X1)
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f26,plain,
! [X2,X3,X1] :
( r1(sK7(X1),sK11(X1))
| r1(sK12(X3),sK14(X3))
| ~ r1(X1,X3)
| ~ p1(X1)
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f29,plain,
! [X2,X3,X1] :
( r1(X1,sK7(X1))
| ~ p1(sK14(X3))
| ~ r1(X1,X3)
| ~ p1(X1)
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f30,plain,
! [X2,X3,X1] :
( r1(X1,sK7(X1))
| r1(sK12(X3),sK14(X3))
| ~ r1(X1,X3)
| ~ p1(X1)
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f31,plain,
! [X2,X3,X1,X8,X9] :
( p1(X8)
| ~ p1(X9)
| sP17(X9)
| ~ r1(X8,X9)
| ~ r1(sK7(X1),X8)
| ~ p1(sK14(X3))
| ~ r1(X1,X3)
| ~ p1(X1)
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f32,plain,
! [X2,X3,X1,X8,X9] :
( p1(X8)
| ~ p1(X9)
| sP17(X9)
| ~ r1(X8,X9)
| ~ r1(sK7(X1),X8)
| r1(sK12(X3),sK14(X3))
| ~ r1(X1,X3)
| ~ p1(X1)
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f34,plain,
! [X2,X3,X1,X8,X9] :
( p1(X8)
| ~ p1(X9)
| sP17(X9)
| ~ r1(X8,X9)
| ~ r1(sK7(X1),X8)
| r1(X3,sK12(X3))
| ~ r1(X1,X3)
| ~ p1(X1)
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f35,plain,
! [X1,X16,X15,X12] :
( ~ p1(X15)
| p1(X16)
| ~ r1(X15,X16)
| ~ r1(sK6(X1),X15)
| r1(X12,sK10(X12))
| ~ r1(X1,X12)
| p1(X1)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f36,plain,
! [X1,X16,X15,X12] :
( ~ p1(X15)
| p1(X16)
| ~ r1(X15,X16)
| ~ r1(sK6(X1),X15)
| ~ p1(sK10(X12))
| ~ r1(X1,X12)
| p1(X1)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f37,plain,
! [X21,X1,X22] :
( r1(X1,sK5(X1))
| p1(sK13(X22))
| p1(X22)
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f38,plain,
! [X21,X1,X22] :
( r1(X1,sK5(X1))
| r1(X22,sK13(X22))
| p1(X22)
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f39,plain,
! [X21,X1,X22] :
( ~ p1(sK5(X1))
| p1(sK13(X22))
| p1(X22)
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f40,plain,
! [X21,X1,X22] :
( ~ p1(sK5(X1))
| r1(X22,sK13(X22))
| p1(X22)
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f41,plain,
! [X21,X1,X26,X27,X22] :
( ~ p1(X26)
| p1(X27)
| ~ r1(X26,X27)
| ~ r1(sK5(X1),X26)
| p1(sK13(X22))
| p1(X22)
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f42,plain,
! [X21,X1,X26,X27,X22] :
( ~ p1(X26)
| p1(X27)
| ~ r1(X26,X27)
| ~ r1(sK5(X1),X26)
| r1(X22,sK13(X22))
| p1(X22)
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f43,plain,
! [X18,X1,X19,X17] :
( ~ p1(sK8(X17))
| p1(X19)
| ~ r1(X18,X19)
| ~ r1(X17,X18)
| ~ r1(X1,X17)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f44,plain,
! [X18,X1,X19,X17] :
( r1(X17,sK8(X17))
| p1(X19)
| ~ r1(X18,X19)
| ~ r1(X17,X18)
| ~ r1(X1,X17)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f46,plain,
! [X2,X3,X1] :
( r1(X1,sK7(X1))
| r1(X3,sK12(X3))
| ~ r1(X1,X3)
| ~ p1(X1)
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f50,plain,
! [X2,X3,X1] :
( r1(sK7(X1),sK11(X1))
| r1(X3,sK12(X3))
| ~ r1(X1,X3)
| ~ p1(X1)
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f52,plain,
! [X2,X3,X1] :
( ~ p1(sK11(X1))
| r1(X3,sK12(X3))
| ~ r1(X1,X3)
| ~ p1(X1)
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f53,plain,
! [X1,X12] :
( ~ p1(sK6(X1))
| ~ p1(sK10(X12))
| ~ r1(X1,X12)
| p1(X1)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f54,plain,
! [X1,X12] :
( ~ p1(sK6(X1))
| r1(X12,sK10(X12))
| ~ r1(X1,X12)
| p1(X1)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f55,plain,
! [X1,X12] :
( r1(X1,sK6(X1))
| ~ p1(sK10(X12))
| ~ r1(X1,X12)
| p1(X1)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f56,plain,
! [X1,X12] :
( r1(X1,sK6(X1))
| r1(X12,sK10(X12))
| ~ r1(X1,X12)
| p1(X1)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f57,plain,
! [X32] :
( ~ p1(sK9(X32))
| p1(X32)
| ~ r1(sK1,X32) ),
inference(cnf_transformation,[],[f6]) ).
fof(f58,plain,
! [X32] :
( r1(sK4(X32),sK9(X32))
| p1(X32)
| ~ r1(sK1,X32) ),
inference(cnf_transformation,[],[f6]) ).
fof(f59,plain,
! [X31] :
( p1(X31)
| ~ r1(sK2,X31) ),
inference(cnf_transformation,[],[f6]) ).
fof(f60,plain,
! [X32] :
( p1(sK4(X32))
| p1(X32)
| ~ r1(sK1,X32) ),
inference(cnf_transformation,[],[f6]) ).
fof(f61,plain,
! [X32] :
( r1(X32,sK4(X32))
| p1(X32)
| ~ r1(sK1,X32) ),
inference(cnf_transformation,[],[f6]) ).
fof(f62,plain,
~ p1(sK3),
inference(cnf_transformation,[],[f6]) ).
fof(f63,plain,
r1(sK1,sK3),
inference(cnf_transformation,[],[f6]) ).
fof(f64,plain,
r1(sK1,sK2),
inference(cnf_transformation,[],[f6]) ).
fof(f65,plain,
r1(sK0,sK1),
inference(cnf_transformation,[],[f6]) ).
fof(f66,plain,
p1(sK3),
inference(consistent_polarity_flipping,[],[f62]) ).
fof(f67,plain,
! [X32] :
( r1(X32,sK4(X32))
| ~ p1(X32)
| ~ r1(sK1,X32) ),
inference(consistent_polarity_flipping,[],[f61]) ).
fof(f68,plain,
! [X32] :
( ~ p1(sK4(X32))
| ~ p1(X32)
| ~ r1(sK1,X32) ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f69,plain,
! [X31] :
( ~ r1(sK2,X31)
| ~ p1(X31) ),
inference(consistent_polarity_flipping,[],[f59]) ).
fof(f70,plain,
! [X32] :
( r1(sK4(X32),sK9(X32))
| ~ p1(X32)
| ~ r1(sK1,X32) ),
inference(consistent_polarity_flipping,[],[f58]) ).
fof(f71,plain,
! [X32] :
( ~ r1(sK1,X32)
| ~ p1(X32)
| p1(sK9(X32)) ),
inference(consistent_polarity_flipping,[],[f57]) ).
fof(f72,plain,
! [X1,X12] :
( ~ p1(X1)
| r1(X12,sK10(X12))
| ~ r1(X1,X12)
| r1(X1,sK6(X1))
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f56]) ).
fof(f73,plain,
! [X1,X12] :
( ~ p1(X1)
| p1(sK10(X12))
| ~ r1(X1,X12)
| r1(X1,sK6(X1))
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f55]) ).
fof(f74,plain,
! [X1,X12] :
( ~ p1(X1)
| r1(X12,sK10(X12))
| ~ r1(X1,X12)
| p1(sK6(X1))
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f54]) ).
fof(f75,plain,
! [X1,X12] :
( ~ p1(X1)
| p1(sK10(X12))
| ~ r1(X1,X12)
| p1(sK6(X1))
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f53]) ).
fof(f76,plain,
! [X2,X3,X1] :
( ~ p1(X2)
| r1(X3,sK12(X3))
| ~ r1(X1,X3)
| p1(X1)
| p1(sK11(X1))
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f52]) ).
fof(f78,plain,
! [X2,X3,X1] :
( ~ p1(X2)
| r1(X3,sK12(X3))
| ~ r1(X1,X3)
| p1(X1)
| r1(sK7(X1),sK11(X1))
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f50]) ).
fof(f82,plain,
! [X2,X3,X1] :
( ~ p1(X2)
| r1(X3,sK12(X3))
| ~ r1(X1,X3)
| p1(X1)
| r1(X1,sK7(X1))
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f46]) ).
fof(f84,plain,
! [X18,X1,X19,X17] :
( ~ p1(X19)
| r1(X17,sK8(X17))
| ~ r1(X18,X19)
| ~ r1(X17,X18)
| ~ r1(X1,X17)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f44]) ).
fof(f85,plain,
! [X18,X1,X19,X17] :
( ~ p1(X19)
| p1(sK8(X17))
| ~ r1(X18,X19)
| ~ r1(X17,X18)
| ~ r1(X1,X17)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f43]) ).
fof(f86,plain,
! [X21,X1,X26,X27,X22] :
( ~ r1(sK5(X1),X26)
| ~ p1(X27)
| ~ r1(X26,X27)
| p1(X26)
| r1(X22,sK13(X22))
| ~ p1(X22)
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f42]) ).
fof(f87,plain,
! [X21,X1,X26,X27,X22] :
( ~ p1(sK13(X22))
| ~ p1(X27)
| ~ r1(X26,X27)
| ~ r1(sK5(X1),X26)
| p1(X26)
| ~ p1(X22)
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f41]) ).
fof(f88,plain,
! [X21,X1,X22] :
( ~ p1(X22)
| r1(X22,sK13(X22))
| p1(sK5(X1))
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f40]) ).
fof(f89,plain,
! [X21,X1,X22] :
( ~ p1(sK13(X22))
| p1(sK5(X1))
| ~ p1(X22)
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f39]) ).
fof(f90,plain,
! [X21,X1,X22] :
( ~ p1(X22)
| r1(X22,sK13(X22))
| r1(X1,sK5(X1))
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f38]) ).
fof(f91,plain,
! [X21,X1,X22] :
( ~ p1(sK13(X22))
| r1(X1,sK5(X1))
| ~ p1(X22)
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f37]) ).
fof(f92,plain,
! [X1,X16,X15,X12] :
( ~ r1(sK6(X1),X15)
| ~ p1(X16)
| ~ r1(X15,X16)
| p1(X15)
| p1(sK10(X12))
| ~ r1(X1,X12)
| ~ p1(X1)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f36]) ).
fof(f93,plain,
! [X1,X16,X15,X12] :
( ~ r1(sK6(X1),X15)
| ~ p1(X16)
| ~ r1(X15,X16)
| p1(X15)
| r1(X12,sK10(X12))
| ~ r1(X1,X12)
| ~ p1(X1)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f35]) ).
fof(f94,plain,
! [X2,X3,X1,X8,X9] :
( ~ r1(sK7(X1),X8)
| p1(X9)
| ~ sP17(X9)
| ~ r1(X8,X9)
| ~ p1(X8)
| r1(X3,sK12(X3))
| ~ r1(X1,X3)
| p1(X1)
| ~ p1(X2)
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f34]) ).
fof(f96,plain,
! [X2,X3,X1,X8,X9] :
( ~ sP17(X9)
| p1(X9)
| ~ p1(X8)
| ~ r1(X8,X9)
| ~ r1(sK7(X1),X8)
| r1(sK12(X3),sK14(X3))
| ~ r1(X1,X3)
| p1(X1)
| ~ p1(X2)
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f32]) ).
fof(f97,plain,
! [X2,X3,X1,X8,X9] :
( ~ r1(sK7(X1),X8)
| p1(X9)
| ~ sP17(X9)
| ~ r1(X8,X9)
| ~ p1(X8)
| p1(sK14(X3))
| ~ r1(X1,X3)
| p1(X1)
| ~ p1(X2)
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f31]) ).
fof(f98,plain,
! [X2,X3,X1] :
( ~ p1(X2)
| r1(sK12(X3),sK14(X3))
| ~ r1(X1,X3)
| p1(X1)
| r1(X1,sK7(X1))
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f30]) ).
fof(f99,plain,
! [X2,X3,X1] :
( ~ p1(X2)
| p1(sK14(X3))
| ~ r1(X1,X3)
| p1(X1)
| r1(X1,sK7(X1))
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f29]) ).
fof(f102,plain,
! [X2,X3,X1] :
( ~ p1(X2)
| r1(sK12(X3),sK14(X3))
| ~ r1(X1,X3)
| p1(X1)
| r1(sK7(X1),sK11(X1))
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f26]) ).
fof(f103,plain,
! [X2,X3,X1] :
( ~ p1(X2)
| p1(sK14(X3))
| ~ r1(X1,X3)
| p1(X1)
| r1(sK7(X1),sK11(X1))
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f25]) ).
fof(f104,plain,
! [X2,X3,X1] :
( ~ p1(X2)
| r1(sK12(X3),sK14(X3))
| ~ r1(X1,X3)
| p1(X1)
| p1(sK11(X1))
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f24]) ).
fof(f105,plain,
! [X2,X3,X1] :
( ~ p1(X2)
| p1(sK14(X3))
| ~ r1(X1,X3)
| p1(X1)
| p1(sK11(X1))
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f23]) ).
fof(f114,plain,
! [X21,X1,X22] :
( ~ p1(X22)
| r1(sK13(X22),sK16(X22))
| r1(X1,sK5(X1))
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f14]) ).
fof(f115,plain,
! [X21,X1,X22] :
( ~ p1(X22)
| p1(sK16(X22))
| r1(X1,sK5(X1))
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f116,plain,
! [X21,X1,X22] :
( ~ p1(X22)
| r1(sK13(X22),sK16(X22))
| p1(sK5(X1))
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f12]) ).
fof(f117,plain,
! [X21,X1,X22] :
( ~ p1(X22)
| p1(sK16(X22))
| p1(sK5(X1))
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f11]) ).
fof(f118,plain,
! [X21,X1,X26,X27,X22] :
( ~ r1(sK5(X1),X26)
| ~ p1(X27)
| ~ r1(X26,X27)
| p1(X26)
| r1(sK13(X22),sK16(X22))
| ~ p1(X22)
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f10]) ).
fof(f119,plain,
! [X21,X1,X26,X27,X22] :
( ~ r1(sK5(X1),X26)
| ~ p1(X27)
| ~ r1(X26,X27)
| p1(X26)
| p1(sK16(X22))
| ~ p1(X22)
| ~ r1(X21,X22)
| ~ r1(X1,X21)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f9]) ).
fof(f120,plain,
! [X10,X9] :
( ~ r1(X9,X10)
| ~ p1(X10)
| sP17(X9) ),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f129,definition,
( spl18_2
<=> p1(sK1) ),
introduced(definition,[new_symbols(definition,[spl18_2])],[avatar_definition]) ).
fof(f130,plain,
( p1(sK1)
| ~ spl18_2 ),
inference(avatar_component_clause,[],[f129]) ).
fof(f131,plain,
( ~ p1(sK1)
| spl18_2 ),
inference(avatar_component_clause,[],[f129]) ).
fof(f209,plain,
! [X2,X0,X1] :
( ~ r1(X1,sK3)
| p1(sK8(X0))
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| ~ r1(sK0,X2) ),
inference(resolution,[],[f85,f66]) ).
fof(f230,plain,
! [X2,X0,X1] :
( ~ r1(X1,sK3)
| r1(X0,sK8(X0))
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| ~ r1(sK0,X2) ),
inference(resolution,[],[f84,f66]) ).
fof(f267,plain,
! [X0,X1] :
( ~ r1(X1,sK3)
| ~ r1(X1,X0)
| p1(X1)
| p1(sK11(X1))
| p1(sK14(X0))
| ~ r1(sK0,X1) ),
inference(resolution,[],[f105,f66]) ).
fof(f388,plain,
! [X0,X1] :
( ~ r1(X1,sK3)
| ~ r1(X1,X0)
| p1(X1)
| p1(sK11(X1))
| r1(X0,sK12(X0))
| ~ r1(sK0,X1) ),
inference(resolution,[],[f76,f66]) ).
fof(f390,plain,
! [X0,X1] :
( ~ r1(X1,sK3)
| ~ r1(X1,X0)
| p1(X1)
| r1(X1,sK7(X1))
| p1(sK14(X0))
| ~ r1(sK0,X1) ),
inference(resolution,[],[f99,f66]) ).
fof(f402,plain,
! [X0,X1] :
( ~ r1(X1,sK3)
| ~ r1(X1,X0)
| p1(X1)
| r1(X1,sK7(X1))
| r1(X0,sK12(X0))
| ~ r1(sK0,X1) ),
inference(resolution,[],[f82,f66]) ).
fof(f407,plain,
! [X0,X1] :
( ~ r1(X1,sK3)
| ~ r1(X1,X0)
| p1(X1)
| r1(sK7(X1),sK11(X1))
| p1(sK14(X0))
| ~ r1(sK0,X1) ),
inference(resolution,[],[f103,f66]) ).
fof(f412,plain,
! [X0,X1] :
( ~ r1(X1,sK3)
| ~ r1(X1,X0)
| p1(X1)
| r1(sK7(X1),sK11(X1))
| r1(X0,sK12(X0))
| ~ r1(sK0,X1) ),
inference(resolution,[],[f78,f66]) ).
fof(f414,plain,
! [X2,X0,X1] :
( ~ p1(X0)
| ~ r1(sK4(sK6(X1)),X0)
| p1(sK4(sK6(X1)))
| p1(sK10(X2))
| ~ r1(X1,X2)
| ~ p1(X1)
| ~ r1(sK0,X1)
| ~ p1(sK6(X1))
| ~ r1(sK1,sK6(X1)) ),
inference(resolution,[],[f92,f67]) ).
fof(f415,plain,
! [X2,X0,X1] :
( ~ r1(sK1,sK6(X1))
| ~ r1(sK4(sK6(X1)),X0)
| p1(sK4(sK6(X1)))
| p1(sK10(X2))
| ~ r1(X1,X2)
| ~ p1(X1)
| ~ r1(sK0,X1)
| ~ p1(X0) ),
inference(forward_subsumption_resolution,[],[f414,f75]) ).
fof(f432,plain,
! [X2,X0,X1] :
( ~ p1(X0)
| ~ r1(sK4(sK6(X1)),X0)
| p1(sK4(sK6(X1)))
| r1(X2,sK10(X2))
| ~ r1(X1,X2)
| ~ p1(X1)
| ~ r1(sK0,X1)
| ~ p1(sK6(X1))
| ~ r1(sK1,sK6(X1)) ),
inference(resolution,[],[f93,f67]) ).
fof(f433,plain,
! [X2,X0,X1] :
( ~ r1(sK1,sK6(X1))
| ~ r1(sK4(sK6(X1)),X0)
| p1(sK4(sK6(X1)))
| r1(X2,sK10(X2))
| ~ r1(X1,X2)
| ~ p1(X1)
| ~ r1(sK0,X1)
| ~ p1(X0) ),
inference(forward_subsumption_resolution,[],[f432,f74]) ).
fof(f435,plain,
! [X0,X1] :
( ~ r1(X1,sK3)
| ~ r1(X1,X0)
| p1(X1)
| r1(sK7(X1),sK11(X1))
| r1(sK12(X0),sK14(X0))
| ~ r1(sK0,X1) ),
inference(resolution,[],[f102,f66]) ).
fof(f441,plain,
! [X2,X3,X0,X1] :
( ~ p1(X0)
| ~ r1(sK4(sK5(X1)),X0)
| p1(sK4(sK5(X1)))
| p1(sK16(X2))
| ~ p1(X2)
| ~ r1(X3,X2)
| ~ r1(X1,X3)
| ~ r1(sK0,X1)
| ~ p1(sK5(X1))
| ~ r1(sK1,sK5(X1)) ),
inference(resolution,[],[f119,f67]) ).
fof(f442,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK1,sK5(X1))
| ~ r1(sK4(sK5(X1)),X0)
| p1(sK4(sK5(X1)))
| p1(sK16(X2))
| ~ p1(X2)
| ~ r1(X3,X2)
| ~ r1(X1,X3)
| ~ r1(sK0,X1)
| ~ p1(X0) ),
inference(forward_subsumption_resolution,[],[f441,f117]) ).
fof(f443,plain,
! [X2,X3,X0,X1] :
( ~ p1(X0)
| ~ r1(sK4(sK5(X1)),X0)
| p1(sK4(sK5(X1)))
| r1(X2,sK13(X2))
| ~ p1(X2)
| ~ r1(X3,X2)
| ~ r1(X1,X3)
| ~ r1(sK0,X1)
| ~ p1(sK5(X1))
| ~ r1(sK1,sK5(X1)) ),
inference(resolution,[],[f86,f67]) ).
fof(f444,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK1,sK5(X1))
| ~ r1(sK4(sK5(X1)),X0)
| p1(sK4(sK5(X1)))
| r1(X2,sK13(X2))
| ~ p1(X2)
| ~ r1(X3,X2)
| ~ r1(X1,X3)
| ~ r1(sK0,X1)
| ~ p1(X0) ),
inference(forward_subsumption_resolution,[],[f443,f88]) ).
fof(f445,plain,
! [X2,X3,X0,X1] :
( ~ p1(X0)
| ~ r1(sK4(sK5(X1)),X0)
| p1(sK4(sK5(X1)))
| r1(sK13(X2),sK16(X2))
| ~ p1(X2)
| ~ r1(X3,X2)
| ~ r1(X1,X3)
| ~ r1(sK0,X1)
| ~ p1(sK5(X1))
| ~ r1(sK1,sK5(X1)) ),
inference(resolution,[],[f118,f67]) ).
fof(f446,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK1,sK5(X1))
| ~ r1(sK4(sK5(X1)),X0)
| p1(sK4(sK5(X1)))
| r1(sK13(X2),sK16(X2))
| ~ p1(X2)
| ~ r1(X3,X2)
| ~ r1(X1,X3)
| ~ r1(sK0,X1)
| ~ p1(X0) ),
inference(forward_subsumption_resolution,[],[f445,f116]) ).
fof(f538,plain,
! [X0,X1] :
( ~ r1(X0,sK3)
| r1(X0,sK8(X0))
| ~ r1(X1,X0)
| ~ r1(sK0,X1) ),
inference(resolution,[],[f7,f230]) ).
fof(f539,plain,
! [X0,X1] :
( ~ r1(X0,sK3)
| p1(sK8(X0))
| ~ r1(X1,X0)
| ~ r1(sK0,X1) ),
inference(resolution,[],[f7,f209]) ).
fof(f584,definition,
( spl18_67
<=> ! [X0] :
( ~ r1(X0,sK1)
| ~ r1(sK0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl18_67])],[avatar_definition]) ).
fof(f585,plain,
( ! [X0] :
( ~ r1(X0,sK1)
| ~ r1(sK0,X0) )
| ~ spl18_67 ),
inference(avatar_component_clause,[],[f584]) ).
fof(f587,definition,
( spl18_68
<=> p1(sK8(sK1)) ),
introduced(definition,[new_symbols(definition,[spl18_68])],[avatar_definition]) ).
fof(f589,plain,
( p1(sK8(sK1))
| ~ spl18_68 ),
inference(avatar_component_clause,[],[f587]) ).
fof(f592,definition,
( spl18_69
<=> r1(sK1,sK8(sK1)) ),
introduced(definition,[new_symbols(definition,[spl18_69])],[avatar_definition]) ).
fof(f594,plain,
( r1(sK1,sK8(sK1))
| ~ spl18_69 ),
inference(avatar_component_clause,[],[f592]) ).
fof(f829,plain,
! [X0] :
( ~ r1(sK1,X0)
| p1(sK1)
| p1(sK11(sK1))
| p1(sK14(X0))
| ~ r1(sK0,sK1) ),
inference(resolution,[],[f267,f63]) ).
fof(f830,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| p1(sK11(sK1))
| p1(sK14(X0))
| ~ r1(sK0,sK1) )
| spl18_2 ),
inference(forward_subsumption_resolution,[],[f829,f131]) ).
fof(f831,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| p1(sK11(sK1))
| p1(sK14(X0)) )
| spl18_2 ),
inference(forward_subsumption_resolution,[],[f830,f65]) ).
fof(f833,definition,
( spl18_93
<=> p1(sK11(sK1)) ),
introduced(definition,[new_symbols(definition,[spl18_93])],[avatar_definition]) ).
fof(f835,plain,
( p1(sK11(sK1))
| ~ spl18_93 ),
inference(avatar_component_clause,[],[f833]) ).
fof(f837,definition,
( spl18_94
<=> ! [X0] :
( ~ r1(sK1,X0)
| p1(sK14(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl18_94])],[avatar_definition]) ).
fof(f838,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| p1(sK14(X0)) )
| ~ spl18_94 ),
inference(avatar_component_clause,[],[f837]) ).
fof(f981,plain,
! [X0] :
( ~ r1(sK1,X0)
| p1(sK1)
| p1(sK11(sK1))
| r1(X0,sK12(X0))
| ~ r1(sK0,sK1) ),
inference(resolution,[],[f388,f63]) ).
fof(f982,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| p1(sK11(sK1))
| r1(X0,sK12(X0))
| ~ r1(sK0,sK1) )
| spl18_2 ),
inference(forward_subsumption_resolution,[],[f981,f131]) ).
fof(f983,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| p1(sK11(sK1))
| r1(X0,sK12(X0)) )
| spl18_2 ),
inference(forward_subsumption_resolution,[],[f982,f65]) ).
fof(f985,definition,
( spl18_119
<=> ! [X0] :
( ~ r1(sK1,X0)
| r1(X0,sK12(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl18_119])],[avatar_definition]) ).
fof(f986,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| r1(X0,sK12(X0)) )
| ~ spl18_119 ),
inference(avatar_component_clause,[],[f985]) ).
fof(f995,plain,
! [X0] :
( ~ r1(sK1,X0)
| p1(sK1)
| r1(sK1,sK7(sK1))
| p1(sK14(X0))
| ~ r1(sK0,sK1) ),
inference(resolution,[],[f390,f63]) ).
fof(f996,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| r1(sK1,sK7(sK1))
| p1(sK14(X0))
| ~ r1(sK0,sK1) )
| spl18_2 ),
inference(forward_subsumption_resolution,[],[f995,f131]) ).
fof(f997,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| r1(sK1,sK7(sK1))
| p1(sK14(X0)) )
| spl18_2 ),
inference(forward_subsumption_resolution,[],[f996,f65]) ).
fof(f999,definition,
( spl18_120
<=> r1(sK1,sK7(sK1)) ),
introduced(definition,[new_symbols(definition,[spl18_120])],[avatar_definition]) ).
fof(f1001,plain,
( r1(sK1,sK7(sK1))
| ~ spl18_120 ),
inference(avatar_component_clause,[],[f999]) ).
fof(f1004,plain,
! [X0] :
( ~ r1(sK1,X0)
| p1(sK1)
| r1(sK1,sK7(sK1))
| r1(X0,sK12(X0))
| ~ r1(sK0,sK1) ),
inference(resolution,[],[f402,f63]) ).
fof(f1005,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| r1(sK1,sK7(sK1))
| r1(X0,sK12(X0))
| ~ r1(sK0,sK1) )
| spl18_2 ),
inference(forward_subsumption_resolution,[],[f1004,f131]) ).
fof(f1006,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| r1(sK1,sK7(sK1))
| r1(X0,sK12(X0)) )
| spl18_2 ),
inference(forward_subsumption_resolution,[],[f1005,f65]) ).
fof(f1093,definition,
( spl18_126
<=> p1(sK6(sK1)) ),
introduced(definition,[new_symbols(definition,[spl18_126])],[avatar_definition]) ).
fof(f1095,plain,
( p1(sK6(sK1))
| ~ spl18_126 ),
inference(avatar_component_clause,[],[f1093]) ).
fof(f1097,definition,
( spl18_127
<=> ! [X0] :
( p1(sK10(X0))
| ~ r1(sK1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl18_127])],[avatar_definition]) ).
fof(f1098,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| p1(sK10(X0)) )
| ~ spl18_127 ),
inference(avatar_component_clause,[],[f1097]) ).
fof(f1101,definition,
( spl18_128
<=> ! [X0] :
( r1(X0,sK10(X0))
| ~ r1(sK1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl18_128])],[avatar_definition]) ).
fof(f1102,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| r1(X0,sK10(X0)) )
| ~ spl18_128 ),
inference(avatar_component_clause,[],[f1101]) ).
fof(f1105,definition,
( spl18_129
<=> r1(sK1,sK6(sK1)) ),
introduced(definition,[new_symbols(definition,[spl18_129])],[avatar_definition]) ).
fof(f1107,plain,
( r1(sK1,sK6(sK1))
| ~ spl18_129 ),
inference(avatar_component_clause,[],[f1105]) ).
fof(f1111,plain,
( spl18_120
| spl18_94
| spl18_2 ),
inference(avatar_split_clause,[],[f997,f129,f837,f999]) ).
fof(f1112,plain,
( spl18_93
| spl18_119
| spl18_2 ),
inference(avatar_split_clause,[],[f983,f129,f985,f833]) ).
fof(f1147,plain,
! [X0] :
( ~ r1(sK1,X0)
| p1(sK1)
| r1(sK7(sK1),sK11(sK1))
| p1(sK14(X0))
| ~ r1(sK0,sK1) ),
inference(resolution,[],[f407,f63]) ).
fof(f1148,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| r1(sK7(sK1),sK11(sK1))
| p1(sK14(X0))
| ~ r1(sK0,sK1) )
| spl18_2 ),
inference(forward_subsumption_resolution,[],[f1147,f131]) ).
fof(f1149,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| r1(sK7(sK1),sK11(sK1))
| p1(sK14(X0)) )
| spl18_2 ),
inference(forward_subsumption_resolution,[],[f1148,f65]) ).
fof(f1151,definition,
( spl18_130
<=> r1(sK7(sK1),sK11(sK1)) ),
introduced(definition,[new_symbols(definition,[spl18_130])],[avatar_definition]) ).
fof(f1153,plain,
( r1(sK7(sK1),sK11(sK1))
| ~ spl18_130 ),
inference(avatar_component_clause,[],[f1151]) ).
fof(f1160,definition,
( spl18_131
<=> ! [X0] :
( ~ r1(sK1,X0)
| r1(sK12(X0),sK14(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl18_131])],[avatar_definition]) ).
fof(f1161,plain,
( ! [X0] :
( r1(sK12(X0),sK14(X0))
| ~ r1(sK1,X0) )
| ~ spl18_131 ),
inference(avatar_component_clause,[],[f1160]) ).
fof(f1232,plain,
! [X0] :
( ~ r1(sK1,X0)
| p1(sK1)
| r1(sK7(sK1),sK11(sK1))
| r1(X0,sK12(X0))
| ~ r1(sK0,sK1) ),
inference(resolution,[],[f412,f63]) ).
fof(f1242,plain,
! [X0] :
( ~ r1(sK1,X0)
| p1(sK1)
| r1(sK7(sK1),sK11(sK1))
| r1(sK12(X0),sK14(X0))
| ~ r1(sK0,sK1) ),
inference(resolution,[],[f435,f63]) ).
fof(f1243,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| r1(sK7(sK1),sK11(sK1))
| r1(sK12(X0),sK14(X0))
| ~ r1(sK0,sK1) )
| spl18_2 ),
inference(forward_subsumption_resolution,[],[f1242,f131]) ).
fof(f1244,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| r1(sK7(sK1),sK11(sK1))
| r1(sK12(X0),sK14(X0)) )
| spl18_2 ),
inference(forward_subsumption_resolution,[],[f1243,f65]) ).
fof(f1258,plain,
! [X0] :
( ~ r1(sK1,X0)
| p1(sK1)
| r1(sK7(sK1),sK11(sK1))
| r1(X0,sK12(X0)) ),
inference(forward_subsumption_resolution,[],[f1232,f65]) ).
fof(f1263,plain,
( spl18_130
| spl18_2
| spl18_119 ),
inference(avatar_split_clause,[],[f1258,f985,f129,f1151]) ).
fof(f1340,definition,
( spl18_141
<=> ! [X0,X1] :
( p1(sK5(X0))
| ~ r1(sK0,X0)
| ~ r1(X0,X1)
| ~ r1(X1,sK11(sK1)) ) ),
introduced(definition,[new_symbols(definition,[spl18_141])],[avatar_definition]) ).
fof(f1341,plain,
( ! [X0,X1] :
( ~ r1(X1,sK11(sK1))
| ~ r1(sK0,X0)
| ~ r1(X0,X1)
| p1(sK5(X0)) )
| ~ spl18_141 ),
inference(avatar_component_clause,[],[f1340]) ).
fof(f1343,definition,
( spl18_142
<=> p1(sK16(sK11(sK1))) ),
introduced(definition,[new_symbols(definition,[spl18_142])],[avatar_definition]) ).
fof(f1345,plain,
( p1(sK16(sK11(sK1)))
| ~ spl18_142 ),
inference(avatar_component_clause,[],[f1343]) ).
fof(f1348,definition,
( spl18_143
<=> r1(sK13(sK11(sK1)),sK16(sK11(sK1))) ),
introduced(definition,[new_symbols(definition,[spl18_143])],[avatar_definition]) ).
fof(f1350,plain,
( r1(sK13(sK11(sK1)),sK16(sK11(sK1)))
| ~ spl18_143 ),
inference(avatar_component_clause,[],[f1348]) ).
fof(f1353,definition,
( spl18_144
<=> ! [X0,X1] :
( r1(X0,sK5(X0))
| ~ r1(sK0,X0)
| ~ r1(X0,X1)
| ~ r1(X1,sK11(sK1)) ) ),
introduced(definition,[new_symbols(definition,[spl18_144])],[avatar_definition]) ).
fof(f1354,plain,
( ! [X0,X1] :
( ~ r1(X1,sK11(sK1))
| ~ r1(sK0,X0)
| ~ r1(X0,X1)
| r1(X0,sK5(X0)) )
| ~ spl18_144 ),
inference(avatar_component_clause,[],[f1353]) ).
fof(f1358,definition,
( spl18_145
<=> r1(sK11(sK1),sK13(sK11(sK1))) ),
introduced(definition,[new_symbols(definition,[spl18_145])],[avatar_definition]) ).
fof(f1360,plain,
( r1(sK11(sK1),sK13(sK11(sK1)))
| ~ spl18_145 ),
inference(avatar_component_clause,[],[f1358]) ).
fof(f1409,plain,
( p1(sK14(sK2))
| ~ spl18_94 ),
inference(resolution,[],[f838,f64]) ).
fof(f1416,plain,
( p1(sK10(sK2))
| ~ spl18_127 ),
inference(resolution,[],[f1098,f64]) ).
fof(f1423,plain,
( r1(sK2,sK12(sK2))
| ~ spl18_119 ),
inference(resolution,[],[f986,f64]) ).
fof(f1430,plain,
( r1(sK2,sK10(sK2))
| ~ spl18_128 ),
inference(resolution,[],[f1102,f64]) ).
fof(f1440,plain,
! [X0] :
( p1(sK8(sK1))
| ~ r1(X0,sK1)
| ~ r1(sK0,X0) ),
inference(resolution,[],[f539,f63]) ).
fof(f1441,plain,
( spl18_67
| spl18_68 ),
inference(avatar_split_clause,[],[f1440,f587,f584]) ).
fof(f1447,plain,
! [X0] :
( r1(sK1,sK8(sK1))
| ~ r1(X0,sK1)
| ~ r1(sK0,X0) ),
inference(resolution,[],[f538,f63]) ).
fof(f1448,plain,
( spl18_67
| spl18_69 ),
inference(avatar_split_clause,[],[f1447,f592,f584]) ).
fof(f1666,plain,
( spl18_93
| spl18_94
| spl18_2 ),
inference(avatar_split_clause,[],[f831,f129,f837,f833]) ).
fof(f1667,plain,
( spl18_130
| spl18_94
| spl18_2 ),
inference(avatar_split_clause,[],[f1149,f129,f837,f1151]) ).
fof(f1668,plain,
( spl18_130
| spl18_131
| spl18_2 ),
inference(avatar_split_clause,[],[f1244,f129,f1160,f1151]) ).
fof(f1737,plain,
( ! [X2,X0,X1] :
( p1(X0)
| ~ sP17(X0)
| ~ r1(sK11(sK1),X0)
| ~ p1(sK11(sK1))
| r1(X1,sK12(X1))
| ~ r1(sK1,X1)
| p1(sK1)
| ~ p1(X2)
| ~ r1(sK1,X2)
| ~ r1(sK0,sK1) )
| ~ spl18_130 ),
inference(resolution,[],[f1153,f94]) ).
fof(f1738,plain,
( ! [X2,X0,X1] :
( p1(X0)
| ~ sP17(X0)
| ~ r1(sK11(sK1),X0)
| ~ p1(sK11(sK1))
| p1(sK14(X1))
| ~ r1(sK1,X1)
| p1(sK1)
| ~ p1(X2)
| ~ r1(sK1,X2)
| ~ r1(sK0,sK1) )
| ~ spl18_130 ),
inference(resolution,[],[f1153,f97]) ).
fof(f1741,plain,
( ! [X2,X0,X1] :
( p1(X0)
| ~ sP17(X0)
| ~ r1(sK11(sK1),X0)
| p1(sK14(X1))
| ~ r1(sK1,X1)
| p1(sK1)
| ~ p1(X2)
| ~ r1(sK1,X2)
| ~ r1(sK0,sK1) )
| ~ spl18_130 ),
inference(forward_subsumption_resolution,[],[f1738,f105]) ).
fof(f1742,plain,
( ! [X2,X0,X1] :
( p1(X0)
| ~ sP17(X0)
| ~ r1(sK11(sK1),X0)
| r1(X1,sK12(X1))
| ~ r1(sK1,X1)
| p1(sK1)
| ~ p1(X2)
| ~ r1(sK1,X2)
| ~ r1(sK0,sK1) )
| ~ spl18_130 ),
inference(forward_subsumption_resolution,[],[f1737,f76]) ).
fof(f1744,plain,
( ! [X2,X0,X1] :
( p1(X0)
| ~ sP17(X0)
| ~ r1(sK11(sK1),X0)
| p1(sK14(X1))
| ~ r1(sK1,X1)
| ~ p1(X2)
| ~ r1(sK1,X2)
| ~ r1(sK0,sK1) )
| spl18_2
| ~ spl18_130 ),
inference(forward_subsumption_resolution,[],[f1741,f131]) ).
fof(f1746,plain,
( ! [X2,X0,X1] :
( p1(X0)
| ~ sP17(X0)
| ~ r1(sK11(sK1),X0)
| p1(sK14(X1))
| ~ r1(sK1,X1)
| ~ p1(X2)
| ~ r1(sK1,X2) )
| spl18_2
| ~ spl18_130 ),
inference(forward_subsumption_resolution,[],[f1744,f65]) ).
fof(f1748,definition,
( spl18_187
<=> ! [X2] :
( ~ p1(X2)
| ~ r1(sK1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl18_187])],[avatar_definition]) ).
fof(f1749,plain,
( ! [X2] :
( ~ r1(sK1,X2)
| ~ p1(X2) )
| ~ spl18_187 ),
inference(avatar_component_clause,[],[f1748]) ).
fof(f1755,definition,
( spl18_189
<=> ! [X0] :
( p1(X0)
| ~ r1(sK11(sK1),X0)
| ~ sP17(X0) ) ),
introduced(definition,[new_symbols(definition,[spl18_189])],[avatar_definition]) ).
fof(f1756,plain,
( ! [X0] :
( ~ r1(sK11(sK1),X0)
| p1(X0)
| ~ sP17(X0) )
| ~ spl18_189 ),
inference(avatar_component_clause,[],[f1755]) ).
fof(f1758,plain,
( spl18_187
| spl18_94
| spl18_189
| spl18_2
| ~ spl18_130 ),
inference(avatar_split_clause,[],[f1746,f1151,f129,f1755,f837,f1748]) ).
fof(f1834,plain,
( ! [X2,X0,X1] :
( ~ r1(X1,sK14(sK2))
| r1(X0,sK8(X0))
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| ~ r1(sK0,X2) )
| ~ spl18_94 ),
inference(resolution,[],[f1409,f84]) ).
fof(f1835,plain,
( ! [X2,X0,X1] :
( ~ r1(X1,sK14(sK2))
| p1(sK8(X0))
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| ~ r1(sK0,X2) )
| ~ spl18_94 ),
inference(resolution,[],[f1409,f85]) ).
fof(f2130,definition,
( spl18_224
<=> p1(sK5(sK1)) ),
introduced(definition,[new_symbols(definition,[spl18_224])],[avatar_definition]) ).
fof(f2131,plain,
( p1(sK5(sK1))
| ~ spl18_224 ),
inference(avatar_component_clause,[],[f2130]) ).
fof(f2138,definition,
( spl18_225
<=> ! [X2,X1] :
( p1(sK16(X1))
| ~ r1(sK1,X2)
| ~ r1(X2,X1)
| ~ p1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl18_225])],[avatar_definition]) ).
fof(f2139,plain,
( ! [X2,X1] :
( ~ r1(sK1,X2)
| p1(sK16(X1))
| ~ r1(X2,X1)
| ~ p1(X1) )
| ~ spl18_225 ),
inference(avatar_component_clause,[],[f2138]) ).
fof(f2141,definition,
( spl18_226
<=> p1(sK4(sK5(sK1))) ),
introduced(definition,[new_symbols(definition,[spl18_226])],[avatar_definition]) ).
fof(f2142,plain,
( ~ p1(sK4(sK5(sK1)))
| spl18_226 ),
inference(avatar_component_clause,[],[f2141]) ).
fof(f2143,plain,
( p1(sK4(sK5(sK1)))
| ~ spl18_226 ),
inference(avatar_component_clause,[],[f2141]) ).
fof(f2145,definition,
( spl18_227
<=> ! [X0] :
( ~ r1(sK4(sK5(sK1)),X0)
| ~ p1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl18_227])],[avatar_definition]) ).
fof(f2146,plain,
( ! [X0] :
( ~ r1(sK4(sK5(sK1)),X0)
| ~ p1(X0) )
| ~ spl18_227 ),
inference(avatar_component_clause,[],[f2145]) ).
fof(f2149,definition,
( spl18_228
<=> ! [X2,X1] :
( r1(X1,sK13(X1))
| ~ r1(sK1,X2)
| ~ r1(X2,X1)
| ~ p1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl18_228])],[avatar_definition]) ).
fof(f2150,plain,
( ! [X2,X1] :
( ~ r1(sK1,X2)
| r1(X1,sK13(X1))
| ~ r1(X2,X1)
| ~ p1(X1) )
| ~ spl18_228 ),
inference(avatar_component_clause,[],[f2149]) ).
fof(f2153,definition,
( spl18_229
<=> ! [X2,X1] :
( r1(sK13(X1),sK16(X1))
| ~ r1(sK1,X2)
| ~ r1(X2,X1)
| ~ p1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl18_229])],[avatar_definition]) ).
fof(f2154,plain,
( ! [X2,X1] :
( ~ r1(sK1,X2)
| r1(sK13(X1),sK16(X1))
| ~ r1(X2,X1)
| ~ p1(X1) )
| ~ spl18_229 ),
inference(avatar_component_clause,[],[f2153]) ).
fof(f2509,plain,
( ~ p1(sK10(sK2))
| ~ spl18_128 ),
inference(resolution,[],[f1430,f69]) ).
fof(f2512,definition,
( spl18_273
<=> p1(sK10(sK2)) ),
introduced(definition,[new_symbols(definition,[spl18_273])],[avatar_definition]) ).
fof(f2514,plain,
( ~ p1(sK10(sK2))
| spl18_273 ),
inference(avatar_component_clause,[],[f2512]) ).
fof(f2516,plain,
( ~ spl18_273
| ~ spl18_128 ),
inference(avatar_split_clause,[],[f2509,f1101,f2512]) ).
fof(f2615,plain,
( ~ r1(sK0,sK1)
| ~ spl18_67 ),
inference(resolution,[],[f585,f7]) ).
fof(f2619,plain,
( $false
| ~ spl18_67 ),
inference(forward_subsumption_resolution,[],[f2615,f65]) ).
fof(f2620,plain,
~ spl18_67,
inference(avatar_contradiction_clause,[],[f2619]) ).
fof(f2632,plain,
( ! [X0,X1] :
( ~ r1(X1,sK8(sK1))
| ~ r1(X1,X0)
| p1(X1)
| r1(X1,sK7(X1))
| r1(sK12(X0),sK14(X0))
| ~ r1(sK0,X1) )
| ~ spl18_68 ),
inference(resolution,[],[f589,f98]) ).
fof(f2636,plain,
( ! [X0,X1] :
( ~ r1(X1,sK8(sK1))
| ~ r1(X1,X0)
| p1(X1)
| p1(sK11(X1))
| r1(sK12(X0),sK14(X0))
| ~ r1(sK0,X1) )
| ~ spl18_68 ),
inference(resolution,[],[f589,f104]) ).
fof(f2735,plain,
( ~ p1(sK5(sK1))
| ~ r1(sK1,sK5(sK1))
| ~ spl18_226 ),
inference(resolution,[],[f2143,f68]) ).
fof(f2885,plain,
( spl18_120
| spl18_119
| spl18_2 ),
inference(avatar_split_clause,[],[f1006,f129,f985,f999]) ).
fof(f3150,plain,
( ! [X0] :
( ~ r1(X0,sK7(sK1))
| ~ r1(sK0,X0)
| p1(sK5(X0)) )
| ~ spl18_130
| ~ spl18_141 ),
inference(resolution,[],[f1341,f1153]) ).
fof(f3335,plain,
( ! [X0] :
( ~ r1(X0,sK7(sK1))
| ~ r1(sK0,X0)
| r1(X0,sK5(X0)) )
| ~ spl18_130
| ~ spl18_144 ),
inference(resolution,[],[f1354,f1153]) ).
fof(f4106,plain,
( ~ r1(sK0,sK1)
| p1(sK5(sK1))
| ~ spl18_120
| ~ spl18_130
| ~ spl18_141 ),
inference(resolution,[],[f3150,f1001]) ).
fof(f4107,plain,
( p1(sK5(sK1))
| ~ spl18_120
| ~ spl18_130
| ~ spl18_141 ),
inference(forward_subsumption_resolution,[],[f4106,f65]) ).
fof(f4110,plain,
( spl18_224
| ~ spl18_120
| ~ spl18_130
| ~ spl18_141 ),
inference(avatar_split_clause,[],[f4107,f1340,f1151,f999,f2130]) ).
fof(f4192,plain,
( ~ r1(sK0,sK1)
| r1(sK1,sK5(sK1))
| ~ spl18_120
| ~ spl18_130
| ~ spl18_144 ),
inference(resolution,[],[f3335,f1001]) ).
fof(f4193,plain,
( r1(sK1,sK5(sK1))
| ~ spl18_120
| ~ spl18_130
| ~ spl18_144 ),
inference(forward_subsumption_resolution,[],[f4192,f65]) ).
fof(f4345,plain,
( ! [X2,X0,X1] :
( ~ r1(sK4(sK5(sK1)),X0)
| p1(sK4(sK5(sK1)))
| r1(X1,sK13(X1))
| ~ p1(X1)
| ~ r1(X2,X1)
| ~ r1(sK1,X2)
| ~ r1(sK0,sK1)
| ~ p1(X0) )
| ~ spl18_120
| ~ spl18_130
| ~ spl18_144 ),
inference(resolution,[],[f4193,f444]) ).
fof(f4352,plain,
( ! [X2,X0,X1] :
( ~ r1(sK4(sK5(sK1)),X0)
| r1(X1,sK13(X1))
| ~ p1(X1)
| ~ r1(X2,X1)
| ~ r1(sK1,X2)
| ~ r1(sK0,sK1)
| ~ p1(X0) )
| ~ spl18_120
| ~ spl18_130
| ~ spl18_144
| spl18_226 ),
inference(forward_subsumption_resolution,[],[f4345,f2142]) ).
fof(f4355,plain,
( ! [X2,X0,X1] :
( ~ r1(sK4(sK5(sK1)),X0)
| r1(X1,sK13(X1))
| ~ p1(X1)
| ~ r1(X2,X1)
| ~ r1(sK1,X2)
| ~ p1(X0) )
| ~ spl18_120
| ~ spl18_130
| ~ spl18_144
| spl18_226 ),
inference(forward_subsumption_resolution,[],[f4352,f65]) ).
fof(f4358,plain,
( spl18_228
| spl18_227
| ~ spl18_120
| ~ spl18_130
| ~ spl18_144
| spl18_226 ),
inference(avatar_split_clause,[],[f4355,f2141,f1353,f1151,f999,f2145,f2149]) ).
fof(f4360,plain,
( ~ p1(sK9(sK5(sK1)))
| ~ p1(sK5(sK1))
| ~ r1(sK1,sK5(sK1))
| ~ spl18_227 ),
inference(resolution,[],[f2146,f70]) ).
fof(f4617,plain,
( ! [X0,X1] :
( p1(sK8(X0))
| ~ r1(X0,sK12(sK2))
| ~ r1(X1,X0)
| ~ r1(sK0,X1)
| ~ r1(sK1,sK2) )
| ~ spl18_94
| ~ spl18_131 ),
inference(resolution,[],[f1835,f1161]) ).
fof(f4618,plain,
( ! [X0,X1] :
( ~ r1(X0,sK12(sK2))
| p1(sK8(X0))
| ~ r1(X1,X0)
| ~ r1(sK0,X1) )
| ~ spl18_94
| ~ spl18_131 ),
inference(forward_subsumption_resolution,[],[f4617,f64]) ).
fof(f4631,plain,
( ! [X0,X1] :
( r1(X0,sK8(X0))
| ~ r1(X0,sK12(sK2))
| ~ r1(X1,X0)
| ~ r1(sK0,X1)
| ~ r1(sK1,sK2) )
| ~ spl18_94
| ~ spl18_131 ),
inference(resolution,[],[f1834,f1161]) ).
fof(f4632,plain,
( ! [X0,X1] :
( ~ r1(X0,sK12(sK2))
| r1(X0,sK8(X0))
| ~ r1(X1,X0)
| ~ r1(sK0,X1) )
| ~ spl18_94
| ~ spl18_131 ),
inference(forward_subsumption_resolution,[],[f4631,f64]) ).
fof(f5347,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| p1(sK1)
| p1(sK11(sK1))
| r1(sK12(X0),sK14(X0))
| ~ r1(sK0,sK1) )
| ~ spl18_68
| ~ spl18_69 ),
inference(resolution,[],[f2636,f594]) ).
fof(f5614,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| p1(sK1)
| r1(sK1,sK7(sK1))
| r1(sK12(X0),sK14(X0))
| ~ r1(sK0,sK1) )
| ~ spl18_68
| ~ spl18_69 ),
inference(resolution,[],[f2632,f594]) ).
fof(f7204,plain,
( ~ p1(sK5(sK1))
| ~ r1(sK1,sK5(sK1))
| ~ spl18_227 ),
inference(forward_subsumption_resolution,[],[f4360,f71]) ).
fof(f7206,definition,
( spl18_790
<=> r1(sK1,sK5(sK1)) ),
introduced(definition,[new_symbols(definition,[spl18_790])],[avatar_definition]) ).
fof(f7207,plain,
( r1(sK1,sK5(sK1))
| ~ spl18_790 ),
inference(avatar_component_clause,[],[f7206]) ).
fof(f7209,plain,
( ~ spl18_790
| ~ spl18_224
| ~ spl18_227 ),
inference(avatar_split_clause,[],[f7204,f2145,f2130,f7206]) ).
fof(f7524,plain,
( ! [X2,X0,X1] :
( ~ r1(sK4(sK5(sK1)),X0)
| p1(sK4(sK5(sK1)))
| r1(sK13(X1),sK16(X1))
| ~ p1(X1)
| ~ r1(X2,X1)
| ~ r1(sK1,X2)
| ~ r1(sK0,sK1)
| ~ p1(X0) )
| ~ spl18_790 ),
inference(resolution,[],[f7207,f446]) ).
fof(f7526,plain,
( ! [X2,X0,X1] :
( ~ r1(sK4(sK5(sK1)),X0)
| p1(sK4(sK5(sK1)))
| p1(sK16(X1))
| ~ p1(X1)
| ~ r1(X2,X1)
| ~ r1(sK1,X2)
| ~ r1(sK0,sK1)
| ~ p1(X0) )
| ~ spl18_790 ),
inference(resolution,[],[f7207,f442]) ).
fof(f7532,plain,
( ! [X2,X0,X1] :
( ~ r1(sK4(sK5(sK1)),X0)
| p1(sK16(X1))
| ~ p1(X1)
| ~ r1(X2,X1)
| ~ r1(sK1,X2)
| ~ r1(sK0,sK1)
| ~ p1(X0) )
| spl18_226
| ~ spl18_790 ),
inference(forward_subsumption_resolution,[],[f7526,f2142]) ).
fof(f7534,plain,
( ! [X2,X0,X1] :
( ~ r1(sK4(sK5(sK1)),X0)
| r1(sK13(X1),sK16(X1))
| ~ p1(X1)
| ~ r1(X2,X1)
| ~ r1(sK1,X2)
| ~ r1(sK0,sK1)
| ~ p1(X0) )
| spl18_226
| ~ spl18_790 ),
inference(forward_subsumption_resolution,[],[f7524,f2142]) ).
fof(f7536,plain,
( ! [X2,X0,X1] :
( ~ r1(sK4(sK5(sK1)),X0)
| p1(sK16(X1))
| ~ p1(X1)
| ~ r1(X2,X1)
| ~ r1(sK1,X2)
| ~ p1(X0) )
| spl18_226
| ~ spl18_790 ),
inference(forward_subsumption_resolution,[],[f7532,f65]) ).
fof(f7538,plain,
( ! [X2,X0,X1] :
( ~ r1(sK4(sK5(sK1)),X0)
| r1(sK13(X1),sK16(X1))
| ~ p1(X1)
| ~ r1(X2,X1)
| ~ r1(sK1,X2)
| ~ p1(X0) )
| spl18_226
| ~ spl18_790 ),
inference(forward_subsumption_resolution,[],[f7534,f65]) ).
fof(f7539,plain,
( spl18_225
| spl18_227
| spl18_226
| ~ spl18_790 ),
inference(avatar_split_clause,[],[f7536,f7206,f2141,f2145,f2138]) ).
fof(f7613,plain,
( ! [X0] :
( ~ r1(sK7(sK1),X0)
| p1(sK16(X0))
| ~ p1(X0) )
| ~ spl18_120
| ~ spl18_225 ),
inference(resolution,[],[f2139,f1001]) ).
fof(f7622,plain,
( ! [X0] :
( ~ r1(sK7(sK1),X0)
| r1(X0,sK13(X0))
| ~ p1(X0) )
| ~ spl18_120
| ~ spl18_228 ),
inference(resolution,[],[f2150,f1001]) ).
fof(f7631,plain,
( ! [X0] :
( ~ r1(sK7(sK1),X0)
| r1(sK13(X0),sK16(X0))
| ~ p1(X0) )
| ~ spl18_120
| ~ spl18_229 ),
inference(resolution,[],[f2154,f1001]) ).
fof(f8190,plain,
( r1(sK11(sK1),sK13(sK11(sK1)))
| ~ p1(sK11(sK1))
| ~ spl18_120
| ~ spl18_130
| ~ spl18_228 ),
inference(resolution,[],[f7622,f1153]) ).
fof(f8216,plain,
( ~ r1(sK1,sK5(sK1))
| ~ spl18_224
| ~ spl18_226 ),
inference(forward_subsumption_resolution,[],[f2735,f2131]) ).
fof(f8240,plain,
( spl18_229
| spl18_227
| spl18_226
| ~ spl18_790 ),
inference(avatar_split_clause,[],[f7538,f7206,f2141,f2145,f2153]) ).
fof(f8638,plain,
( r1(sK13(sK11(sK1)),sK16(sK11(sK1)))
| ~ p1(sK11(sK1))
| ~ spl18_120
| ~ spl18_130
| ~ spl18_229 ),
inference(resolution,[],[f7631,f1153]) ).
fof(f9034,plain,
( ! [X0] :
( p1(sK8(sK2))
| ~ r1(X0,sK2)
| ~ r1(sK0,X0) )
| ~ spl18_94
| ~ spl18_119
| ~ spl18_131 ),
inference(resolution,[],[f4618,f1423]) ).
fof(f9036,definition,
( spl18_993
<=> ! [X0] :
( ~ r1(X0,sK2)
| ~ r1(sK0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl18_993])],[avatar_definition]) ).
fof(f9037,plain,
( ! [X0] :
( ~ r1(X0,sK2)
| ~ r1(sK0,X0) )
| ~ spl18_993 ),
inference(avatar_component_clause,[],[f9036]) ).
fof(f9039,definition,
( spl18_994
<=> p1(sK8(sK2)) ),
introduced(definition,[new_symbols(definition,[spl18_994])],[avatar_definition]) ).
fof(f9041,plain,
( p1(sK8(sK2))
| ~ spl18_994 ),
inference(avatar_component_clause,[],[f9039]) ).
fof(f9042,plain,
( spl18_993
| spl18_994
| ~ spl18_94
| ~ spl18_119
| ~ spl18_131 ),
inference(avatar_split_clause,[],[f9034,f1160,f985,f837,f9039,f9036]) ).
fof(f9616,plain,
( ! [X0] :
( r1(sK2,sK8(sK2))
| ~ r1(X0,sK2)
| ~ r1(sK0,X0) )
| ~ spl18_94
| ~ spl18_119
| ~ spl18_131 ),
inference(resolution,[],[f4632,f1423]) ).
fof(f9618,definition,
( spl18_1076
<=> r1(sK2,sK8(sK2)) ),
introduced(definition,[new_symbols(definition,[spl18_1076])],[avatar_definition]) ).
fof(f9620,plain,
( r1(sK2,sK8(sK2))
| ~ spl18_1076 ),
inference(avatar_component_clause,[],[f9618]) ).
fof(f9621,plain,
( spl18_993
| spl18_1076
| ~ spl18_94
| ~ spl18_119
| ~ spl18_131 ),
inference(avatar_split_clause,[],[f9616,f1160,f985,f837,f9618,f9036]) ).
fof(f10068,plain,
( ~ r1(sK0,sK1)
| ~ spl18_993 ),
inference(resolution,[],[f9037,f64]) ).
fof(f10069,plain,
( $false
| ~ spl18_993 ),
inference(forward_subsumption_resolution,[],[f10068,f65]) ).
fof(f10070,plain,
~ spl18_993,
inference(avatar_contradiction_clause,[],[f10069]) ).
fof(f10155,plain,
( ~ p1(sK8(sK2))
| ~ spl18_1076 ),
inference(resolution,[],[f9620,f69]) ).
fof(f10158,plain,
( $false
| ~ spl18_994
| ~ spl18_1076 ),
inference(forward_subsumption_resolution,[],[f10155,f9041]) ).
fof(f10159,plain,
( ~ spl18_994
| ~ spl18_1076 ),
inference(avatar_contradiction_clause,[],[f10158]) ).
fof(f10180,plain,
( ~ spl18_93
| spl18_145
| ~ spl18_120
| ~ spl18_130
| ~ spl18_228 ),
inference(avatar_split_clause,[],[f8190,f2149,f1151,f999,f1358,f833]) ).
fof(f10181,plain,
( ~ spl18_93
| spl18_143
| ~ spl18_120
| ~ spl18_130
| ~ spl18_229 ),
inference(avatar_split_clause,[],[f8638,f2153,f1151,f999,f1348,f833]) ).
fof(f10187,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| p1(sK11(sK1))
| r1(sK12(X0),sK14(X0))
| ~ r1(sK0,sK1) )
| spl18_2
| ~ spl18_68
| ~ spl18_69 ),
inference(forward_subsumption_resolution,[],[f5347,f131]) ).
fof(f10188,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| r1(sK1,sK7(sK1))
| r1(sK12(X0),sK14(X0))
| ~ r1(sK0,sK1) )
| spl18_2
| ~ spl18_68
| ~ spl18_69 ),
inference(forward_subsumption_resolution,[],[f5614,f131]) ).
fof(f10190,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| p1(sK11(sK1))
| r1(sK12(X0),sK14(X0)) )
| spl18_2
| ~ spl18_68
| ~ spl18_69 ),
inference(forward_subsumption_resolution,[],[f10187,f65]) ).
fof(f10191,plain,
( ! [X0] :
( ~ r1(sK1,X0)
| r1(sK1,sK7(sK1))
| r1(sK12(X0),sK14(X0)) )
| spl18_2
| ~ spl18_68
| ~ spl18_69 ),
inference(forward_subsumption_resolution,[],[f10188,f65]) ).
fof(f10198,plain,
( spl18_120
| spl18_131
| spl18_2
| ~ spl18_68
| ~ spl18_69 ),
inference(avatar_split_clause,[],[f10191,f592,f587,f129,f1160,f999]) ).
fof(f10208,plain,
( ! [X0,X1] :
( r1(sK11(sK1),sK13(sK11(sK1)))
| p1(sK5(X0))
| ~ r1(X1,sK11(sK1))
| ~ r1(X0,X1)
| ~ r1(sK0,X0) )
| ~ spl18_93 ),
inference(resolution,[],[f835,f88]) ).
fof(f10209,plain,
( ! [X0,X1] :
( r1(sK11(sK1),sK13(sK11(sK1)))
| r1(X0,sK5(X0))
| ~ r1(X1,sK11(sK1))
| ~ r1(X0,X1)
| ~ r1(sK0,X0) )
| ~ spl18_93 ),
inference(resolution,[],[f835,f90]) ).
fof(f10216,plain,
( ! [X0,X1] :
( r1(sK13(sK11(sK1)),sK16(sK11(sK1)))
| r1(X0,sK5(X0))
| ~ r1(X1,sK11(sK1))
| ~ r1(X0,X1)
| ~ r1(sK0,X0) )
| ~ spl18_93 ),
inference(resolution,[],[f835,f114]) ).
fof(f10218,plain,
( ! [X0,X1] :
( r1(sK13(sK11(sK1)),sK16(sK11(sK1)))
| p1(sK5(X0))
| ~ r1(X1,sK11(sK1))
| ~ r1(X0,X1)
| ~ r1(sK0,X0) )
| ~ spl18_93 ),
inference(resolution,[],[f835,f116]) ).
fof(f10219,plain,
( ! [X0,X1] :
( p1(sK16(sK11(sK1)))
| p1(sK5(X0))
| ~ r1(X1,sK11(sK1))
| ~ r1(X0,X1)
| ~ r1(sK0,X0) )
| ~ spl18_93 ),
inference(resolution,[],[f835,f117]) ).
fof(f10221,plain,
( spl18_141
| spl18_142
| ~ spl18_93 ),
inference(avatar_split_clause,[],[f10219,f833,f1343,f1340]) ).
fof(f10222,plain,
( spl18_141
| spl18_143
| ~ spl18_93 ),
inference(avatar_split_clause,[],[f10218,f833,f1348,f1340]) ).
fof(f10224,plain,
( spl18_144
| spl18_143
| ~ spl18_93 ),
inference(avatar_split_clause,[],[f10216,f833,f1348,f1353]) ).
fof(f10225,plain,
( spl18_144
| spl18_145
| ~ spl18_93 ),
inference(avatar_split_clause,[],[f10209,f833,f1358,f1353]) ).
fof(f10226,plain,
( spl18_141
| spl18_145
| ~ spl18_93 ),
inference(avatar_split_clause,[],[f10208,f833,f1358,f1340]) ).
fof(f10356,plain,
( ~ p1(sK16(sK11(sK1)))
| sP17(sK13(sK11(sK1)))
| ~ spl18_143 ),
inference(resolution,[],[f1350,f120]) ).
fof(f10357,plain,
( sP17(sK13(sK11(sK1)))
| ~ spl18_142
| ~ spl18_143 ),
inference(forward_subsumption_resolution,[],[f10356,f1345]) ).
fof(f10385,plain,
( ! [X2,X3,X0,X1] :
( p1(sK13(sK11(sK1)))
| ~ p1(X0)
| ~ r1(X0,sK13(sK11(sK1)))
| ~ r1(sK7(X1),X0)
| r1(sK12(X2),sK14(X2))
| ~ r1(X1,X2)
| p1(X1)
| ~ p1(X3)
| ~ r1(X1,X3)
| ~ r1(sK0,X1) )
| ~ spl18_142
| ~ spl18_143 ),
inference(resolution,[],[f10357,f96]) ).
fof(f10387,definition,
( spl18_1142
<=> ! [X0,X3,X2,X1] :
( ~ p1(X0)
| ~ r1(sK0,X1)
| ~ r1(X1,X3)
| ~ p1(X3)
| p1(X1)
| ~ r1(X1,X2)
| r1(sK12(X2),sK14(X2))
| ~ r1(sK7(X1),X0)
| ~ r1(X0,sK13(sK11(sK1))) ) ),
introduced(definition,[new_symbols(definition,[spl18_1142])],[avatar_definition]) ).
fof(f10388,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(X0,sK13(sK11(sK1)))
| ~ r1(sK0,X1)
| ~ r1(X1,X3)
| ~ p1(X3)
| p1(X1)
| ~ r1(X1,X2)
| r1(sK12(X2),sK14(X2))
| ~ r1(sK7(X1),X0)
| ~ p1(X0) )
| ~ spl18_1142 ),
inference(avatar_component_clause,[],[f10387]) ).
fof(f10390,definition,
( spl18_1143
<=> p1(sK13(sK11(sK1))) ),
introduced(definition,[new_symbols(definition,[spl18_1143])],[avatar_definition]) ).
fof(f10391,plain,
( ~ p1(sK13(sK11(sK1)))
| spl18_1143 ),
inference(avatar_component_clause,[],[f10390]) ).
fof(f10392,plain,
( p1(sK13(sK11(sK1)))
| ~ spl18_1143 ),
inference(avatar_component_clause,[],[f10390]) ).
fof(f10414,plain,
( ! [X2,X3,X0,X1] :
( ~ p1(X0)
| ~ r1(X1,X0)
| ~ r1(sK5(X2),X1)
| p1(X1)
| ~ p1(sK11(sK1))
| ~ r1(X3,sK11(sK1))
| ~ r1(X2,X3)
| ~ r1(sK0,X2) )
| ~ spl18_1143 ),
inference(resolution,[],[f10392,f87]) ).
fof(f10415,plain,
( ! [X0,X1] :
( r1(X0,sK5(X0))
| ~ p1(sK11(sK1))
| ~ r1(X1,sK11(sK1))
| ~ r1(X0,X1)
| ~ r1(sK0,X0) )
| ~ spl18_1143 ),
inference(resolution,[],[f10392,f91]) ).
fof(f10416,plain,
( ! [X0,X1] :
( p1(sK5(X0))
| ~ p1(sK11(sK1))
| ~ r1(X1,sK11(sK1))
| ~ r1(X0,X1)
| ~ r1(sK0,X0) )
| ~ spl18_1143 ),
inference(resolution,[],[f10392,f89]) ).
fof(f10485,plain,
( ! [X0,X1] :
( p1(sK5(X0))
| ~ r1(X1,sK11(sK1))
| ~ r1(X0,X1)
| ~ r1(sK0,X0) )
| ~ spl18_93
| ~ spl18_1143 ),
inference(forward_subsumption_resolution,[],[f10416,f835]) ).
fof(f10486,plain,
( ! [X0,X1] :
( r1(X0,sK5(X0))
| ~ r1(X1,sK11(sK1))
| ~ r1(X0,X1)
| ~ r1(sK0,X0) )
| ~ spl18_93
| ~ spl18_1143 ),
inference(forward_subsumption_resolution,[],[f10415,f835]) ).
fof(f10487,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(X3,sK11(sK1))
| ~ r1(X1,X0)
| ~ r1(sK5(X2),X1)
| p1(X1)
| ~ p1(X0)
| ~ r1(X2,X3)
| ~ r1(sK0,X2) )
| ~ spl18_93
| ~ spl18_1143 ),
inference(forward_subsumption_resolution,[],[f10414,f835]) ).
fof(f10488,plain,
( spl18_141
| ~ spl18_93
| ~ spl18_1143 ),
inference(avatar_split_clause,[],[f10485,f10390,f833,f1340]) ).
fof(f10489,plain,
( spl18_144
| ~ spl18_93
| ~ spl18_1143 ),
inference(avatar_split_clause,[],[f10486,f10390,f833,f1353]) ).
fof(f11304,plain,
( p1(sK16(sK11(sK1)))
| ~ p1(sK11(sK1))
| ~ spl18_120
| ~ spl18_130
| ~ spl18_225 ),
inference(resolution,[],[f7613,f1153]) ).
fof(f16650,plain,
( ! [X2,X0,X1] :
( ~ r1(X2,sK7(sK1))
| ~ r1(sK5(X2),X0)
| p1(X0)
| ~ p1(X1)
| ~ r1(X0,X1)
| ~ r1(sK0,X2) )
| ~ spl18_93
| ~ spl18_130
| ~ spl18_1143 ),
inference(resolution,[],[f10487,f1153]) ).
fof(f29992,plain,
( ! [X0,X1] :
( ~ r1(sK5(sK1),X0)
| p1(X0)
| ~ p1(X1)
| ~ r1(X0,X1)
| ~ r1(sK0,sK1) )
| ~ spl18_93
| ~ spl18_120
| ~ spl18_130
| ~ spl18_1143 ),
inference(resolution,[],[f16650,f1001]) ).
fof(f29993,plain,
( ! [X0,X1] :
( ~ r1(sK5(sK1),X0)
| p1(X0)
| ~ p1(X1)
| ~ r1(X0,X1) )
| ~ spl18_93
| ~ spl18_120
| ~ spl18_130
| ~ spl18_1143 ),
inference(forward_subsumption_resolution,[],[f29992,f65]) ).
fof(f37880,plain,
( ! [X0] :
( p1(sK4(sK5(sK1)))
| ~ p1(X0)
| ~ r1(sK4(sK5(sK1)),X0)
| ~ p1(sK5(sK1))
| ~ r1(sK1,sK5(sK1)) )
| ~ spl18_93
| ~ spl18_120
| ~ spl18_130
| ~ spl18_1143 ),
inference(resolution,[],[f29993,f67]) ).
fof(f37882,plain,
( ! [X0] :
( ~ p1(X0)
| ~ r1(sK4(sK5(sK1)),X0)
| ~ p1(sK5(sK1))
| ~ r1(sK1,sK5(sK1)) )
| ~ spl18_93
| ~ spl18_120
| ~ spl18_130
| ~ spl18_1143 ),
inference(forward_subsumption_resolution,[],[f37880,f68]) ).
fof(f37885,plain,
( ! [X0] :
( ~ p1(X0)
| ~ r1(sK4(sK5(sK1)),X0)
| ~ r1(sK1,sK5(sK1)) )
| ~ spl18_93
| ~ spl18_120
| ~ spl18_130
| ~ spl18_224
| ~ spl18_1143 ),
inference(forward_subsumption_resolution,[],[f37882,f2131]) ).
fof(f37888,plain,
( ! [X0] :
( ~ p1(X0)
| ~ r1(sK4(sK5(sK1)),X0) )
| ~ spl18_93
| ~ spl18_120
| ~ spl18_130
| ~ spl18_224
| ~ spl18_790
| ~ spl18_1143 ),
inference(forward_subsumption_resolution,[],[f37885,f7207]) ).
fof(f37889,plain,
( spl18_227
| ~ spl18_93
| ~ spl18_120
| ~ spl18_130
| ~ spl18_224
| ~ spl18_790
| ~ spl18_1143 ),
inference(avatar_split_clause,[],[f37888,f10390,f7206,f2130,f1151,f999,f833,f2145]) ).
fof(f37891,plain,
( ! [X2,X0,X1] :
( ~ r1(sK0,X0)
| ~ r1(X0,X1)
| ~ p1(X1)
| p1(X0)
| ~ r1(X0,X2)
| r1(sK12(X2),sK14(X2))
| ~ r1(sK7(X0),sK11(sK1))
| ~ p1(sK11(sK1)) )
| ~ spl18_145
| ~ spl18_1142 ),
inference(resolution,[],[f10388,f1360]) ).
fof(f37928,definition,
( spl18_4230
<=> ! [X2,X0,X1] :
( ~ r1(sK0,X0)
| ~ r1(sK7(X0),sK11(sK1))
| r1(sK12(X2),sK14(X2))
| ~ r1(X0,X2)
| p1(X0)
| ~ p1(X1)
| ~ r1(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl18_4230])],[avatar_definition]) ).
fof(f37929,plain,
( ! [X2,X0,X1] :
( ~ r1(sK7(X0),sK11(sK1))
| ~ r1(sK0,X0)
| r1(sK12(X2),sK14(X2))
| ~ r1(X0,X2)
| p1(X0)
| ~ p1(X1)
| ~ r1(X0,X1) )
| ~ spl18_4230 ),
inference(avatar_component_clause,[],[f37928]) ).
fof(f38021,plain,
( ! [X0,X1] :
( ~ r1(sK0,sK1)
| r1(sK12(X0),sK14(X0))
| ~ r1(sK1,X0)
| p1(sK1)
| ~ p1(X1)
| ~ r1(sK1,X1) )
| ~ spl18_130
| ~ spl18_4230 ),
inference(resolution,[],[f37929,f1153]) ).
fof(f38022,plain,
( ! [X0,X1] :
( r1(sK12(X0),sK14(X0))
| ~ r1(sK1,X0)
| p1(sK1)
| ~ p1(X1)
| ~ r1(sK1,X1) )
| ~ spl18_130
| ~ spl18_4230 ),
inference(forward_subsumption_resolution,[],[f38021,f65]) ).
fof(f38075,definition,
( spl18_4243
<=> sP17(sK13(sK11(sK1))) ),
introduced(definition,[new_symbols(definition,[spl18_4243])],[avatar_definition]) ).
fof(f38077,plain,
( sP17(sK13(sK11(sK1)))
| ~ spl18_4243 ),
inference(avatar_component_clause,[],[f38075]) ).
fof(f38079,plain,
( ~ spl18_93
| spl18_142
| ~ spl18_120
| ~ spl18_130
| ~ spl18_225 ),
inference(avatar_split_clause,[],[f11304,f2138,f1151,f999,f1343,f833]) ).
fof(f38121,definition,
( spl18_4245
<=> p1(sK4(sK6(sK1))) ),
introduced(definition,[new_symbols(definition,[spl18_4245])],[avatar_definition]) ).
fof(f38122,plain,
( ~ p1(sK4(sK6(sK1)))
| spl18_4245 ),
inference(avatar_component_clause,[],[f38121]) ).
fof(f38123,plain,
( p1(sK4(sK6(sK1)))
| ~ spl18_4245 ),
inference(avatar_component_clause,[],[f38121]) ).
fof(f38125,definition,
( spl18_4246
<=> ! [X0] :
( ~ r1(sK4(sK6(sK1)),X0)
| ~ p1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl18_4246])],[avatar_definition]) ).
fof(f38126,plain,
( ! [X0] :
( ~ r1(sK4(sK6(sK1)),X0)
| ~ p1(X0) )
| ~ spl18_4246 ),
inference(avatar_component_clause,[],[f38125]) ).
fof(f38231,plain,
( ! [X0] :
( r1(X0,sK10(X0))
| ~ r1(sK1,X0)
| r1(sK1,sK6(sK1))
| ~ r1(sK0,sK1) )
| ~ spl18_2 ),
inference(resolution,[],[f130,f72]) ).
fof(f38232,plain,
( ! [X0] :
( p1(sK10(X0))
| ~ r1(sK1,X0)
| r1(sK1,sK6(sK1))
| ~ r1(sK0,sK1) )
| ~ spl18_2 ),
inference(resolution,[],[f130,f73]) ).
fof(f38233,plain,
( ! [X0] :
( r1(X0,sK10(X0))
| ~ r1(sK1,X0)
| p1(sK6(sK1))
| ~ r1(sK0,sK1) )
| ~ spl18_2 ),
inference(resolution,[],[f130,f74]) ).
fof(f38234,plain,
( ! [X0] :
( p1(sK10(X0))
| ~ r1(sK1,X0)
| p1(sK6(sK1))
| ~ r1(sK0,sK1) )
| ~ spl18_2 ),
inference(resolution,[],[f130,f75]) ).
fof(f38259,plain,
( ! [X0] :
( p1(sK10(X0))
| ~ r1(sK1,X0)
| p1(sK6(sK1)) )
| ~ spl18_2 ),
inference(forward_subsumption_resolution,[],[f38234,f65]) ).
fof(f38260,plain,
( ! [X0] :
( r1(X0,sK10(X0))
| ~ r1(sK1,X0)
| p1(sK6(sK1)) )
| ~ spl18_2 ),
inference(forward_subsumption_resolution,[],[f38233,f65]) ).
fof(f38261,plain,
( ! [X0] :
( p1(sK10(X0))
| ~ r1(sK1,X0)
| r1(sK1,sK6(sK1)) )
| ~ spl18_2 ),
inference(forward_subsumption_resolution,[],[f38232,f65]) ).
fof(f38262,plain,
( ! [X0] :
( r1(X0,sK10(X0))
| ~ r1(sK1,X0)
| r1(sK1,sK6(sK1)) )
| ~ spl18_2 ),
inference(forward_subsumption_resolution,[],[f38231,f65]) ).
fof(f38263,plain,
( spl18_126
| spl18_127
| ~ spl18_2 ),
inference(avatar_split_clause,[],[f38259,f129,f1097,f1093]) ).
fof(f38264,plain,
( spl18_126
| spl18_128
| ~ spl18_2 ),
inference(avatar_split_clause,[],[f38260,f129,f1101,f1093]) ).
fof(f38265,plain,
( spl18_129
| spl18_127
| ~ spl18_2 ),
inference(avatar_split_clause,[],[f38261,f129,f1097,f1105]) ).
fof(f38266,plain,
( spl18_129
| spl18_128
| ~ spl18_2 ),
inference(avatar_split_clause,[],[f38262,f129,f1101,f1105]) ).
fof(f38481,plain,
( ! [X0,X1] :
( ~ r1(sK4(sK6(sK1)),X0)
| p1(sK4(sK6(sK1)))
| r1(X1,sK10(X1))
| ~ r1(sK1,X1)
| ~ p1(sK1)
| ~ r1(sK0,sK1)
| ~ p1(X0) )
| ~ spl18_129 ),
inference(resolution,[],[f1107,f433]) ).
fof(f38482,plain,
( ! [X0,X1] :
( ~ r1(sK4(sK6(sK1)),X0)
| p1(sK4(sK6(sK1)))
| p1(sK10(X1))
| ~ r1(sK1,X1)
| ~ p1(sK1)
| ~ r1(sK0,sK1)
| ~ p1(X0) )
| ~ spl18_129 ),
inference(resolution,[],[f1107,f415]) ).
fof(f38727,plain,
( ~ p1(sK6(sK1))
| ~ r1(sK1,sK6(sK1))
| ~ spl18_4245 ),
inference(resolution,[],[f38123,f68]) ).
fof(f38796,plain,
( ~ r1(sK1,sK6(sK1))
| ~ spl18_126
| ~ spl18_4245 ),
inference(forward_subsumption_resolution,[],[f38727,f1095]) ).
fof(f38797,plain,
( $false
| ~ spl18_126
| ~ spl18_129
| ~ spl18_4245 ),
inference(forward_subsumption_resolution,[],[f38796,f1107]) ).
fof(f38798,plain,
( ~ spl18_126
| ~ spl18_129
| ~ spl18_4245 ),
inference(avatar_contradiction_clause,[],[f38797]) ).
fof(f39058,plain,
( ! [X2,X3,X0,X1] :
( p1(sK13(sK11(sK1)))
| ~ p1(X0)
| ~ r1(X0,sK13(sK11(sK1)))
| ~ r1(sK7(X1),X0)
| r1(sK12(X2),sK14(X2))
| ~ r1(X1,X2)
| p1(X1)
| ~ p1(X3)
| ~ r1(X1,X3)
| ~ r1(sK0,X1) )
| ~ spl18_4243 ),
inference(resolution,[],[f38077,f96]) ).
fof(f39059,plain,
( ! [X2,X3,X0,X1] :
( ~ p1(X0)
| ~ r1(X0,sK13(sK11(sK1)))
| ~ r1(sK7(X1),X0)
| r1(sK12(X2),sK14(X2))
| ~ r1(X1,X2)
| p1(X1)
| ~ p1(X3)
| ~ r1(X1,X3)
| ~ r1(sK0,X1) )
| spl18_1143
| ~ spl18_4243 ),
inference(forward_subsumption_resolution,[],[f39058,f10391]) ).
fof(f39061,plain,
( spl18_1142
| spl18_1143
| ~ spl18_4243 ),
inference(avatar_split_clause,[],[f39059,f38075,f10390,f10387]) ).
fof(f39118,plain,
( ~ p1(sK9(sK6(sK1)))
| ~ p1(sK6(sK1))
| ~ r1(sK1,sK6(sK1))
| ~ spl18_4246 ),
inference(resolution,[],[f38126,f70]) ).
fof(f39121,plain,
( ~ p1(sK6(sK1))
| ~ r1(sK1,sK6(sK1))
| ~ spl18_4246 ),
inference(forward_subsumption_resolution,[],[f39118,f71]) ).
fof(f39122,plain,
( ~ r1(sK1,sK6(sK1))
| ~ spl18_126
| ~ spl18_4246 ),
inference(forward_subsumption_resolution,[],[f39121,f1095]) ).
fof(f39123,plain,
( $false
| ~ spl18_126
| ~ spl18_129
| ~ spl18_4246 ),
inference(forward_subsumption_resolution,[],[f39122,f1107]) ).
fof(f39124,plain,
( ~ spl18_126
| ~ spl18_129
| ~ spl18_4246 ),
inference(avatar_contradiction_clause,[],[f39123]) ).
fof(f39125,plain,
( $false
| ~ spl18_127
| spl18_273 ),
inference(forward_subsumption_resolution,[],[f1416,f2514]) ).
fof(f39126,plain,
( ~ spl18_127
| spl18_273 ),
inference(avatar_contradiction_clause,[],[f39125]) ).
fof(f39144,plain,
( spl18_93
| spl18_131
| spl18_2
| ~ spl18_68
| ~ spl18_69 ),
inference(avatar_split_clause,[],[f10190,f592,f587,f129,f1160,f833]) ).
fof(f39153,plain,
( spl18_4243
| ~ spl18_142
| ~ spl18_143 ),
inference(avatar_split_clause,[],[f10357,f1348,f1343,f38075]) ).
fof(f39155,plain,
( ! [X2,X3,X0,X1] :
( ~ p1(X0)
| ~ r1(X0,sK13(sK11(sK1)))
| ~ r1(sK7(X1),X0)
| r1(sK12(X2),sK14(X2))
| ~ r1(X1,X2)
| p1(X1)
| ~ p1(X3)
| ~ r1(X1,X3)
| ~ r1(sK0,X1) )
| ~ spl18_142
| ~ spl18_143
| spl18_1143 ),
inference(forward_subsumption_resolution,[],[f10385,f10391]) ).
fof(f39156,plain,
( ~ spl18_93
| spl18_4230
| ~ spl18_145
| ~ spl18_1142 ),
inference(avatar_split_clause,[],[f37891,f10387,f1358,f37928,f833]) ).
fof(f39182,plain,
( ! [X0,X1] :
( ~ r1(sK4(sK6(sK1)),X0)
| p1(sK10(X1))
| ~ r1(sK1,X1)
| ~ p1(sK1)
| ~ r1(sK0,sK1)
| ~ p1(X0) )
| ~ spl18_129
| spl18_4245 ),
inference(forward_subsumption_resolution,[],[f38482,f38122]) ).
fof(f39183,plain,
( ! [X0,X1] :
( ~ r1(sK4(sK6(sK1)),X0)
| r1(X1,sK10(X1))
| ~ r1(sK1,X1)
| ~ p1(sK1)
| ~ r1(sK0,sK1)
| ~ p1(X0) )
| ~ spl18_129
| spl18_4245 ),
inference(forward_subsumption_resolution,[],[f38481,f38122]) ).
fof(f39190,plain,
( spl18_1142
| ~ spl18_142
| ~ spl18_143
| spl18_1143 ),
inference(avatar_split_clause,[],[f39155,f10390,f1348,f1343,f10387]) ).
fof(f39238,plain,
( ! [X0,X1] :
( ~ r1(sK4(sK6(sK1)),X0)
| p1(sK10(X1))
| ~ r1(sK1,X1)
| ~ p1(sK1)
| ~ p1(X0) )
| ~ spl18_129
| spl18_4245 ),
inference(forward_subsumption_resolution,[],[f39182,f65]) ).
fof(f39239,plain,
( ! [X0,X1] :
( ~ r1(sK4(sK6(sK1)),X0)
| r1(X1,sK10(X1))
| ~ r1(sK1,X1)
| ~ p1(sK1)
| ~ p1(X0) )
| ~ spl18_129
| spl18_4245 ),
inference(forward_subsumption_resolution,[],[f39183,f65]) ).
fof(f39244,plain,
( ~ spl18_2
| spl18_127
| spl18_4246
| ~ spl18_129
| spl18_4245 ),
inference(avatar_split_clause,[],[f39238,f38121,f1105,f38125,f1097,f129]) ).
fof(f39245,plain,
( ~ spl18_2
| spl18_128
| spl18_4246
| ~ spl18_129
| spl18_4245 ),
inference(avatar_split_clause,[],[f39239,f38121,f1105,f38125,f1101,f129]) ).
fof(f39264,plain,
( ! [X0,X1] :
( p1(sK16(sK11(sK1)))
| r1(X0,sK5(X0))
| ~ r1(X1,sK11(sK1))
| ~ r1(X0,X1)
| ~ r1(sK0,X0) )
| ~ spl18_93 ),
inference(resolution,[],[f835,f115]) ).
fof(f39320,plain,
( ~ p1(sK3)
| ~ spl18_187 ),
inference(resolution,[],[f1749,f63]) ).
fof(f39335,plain,
( $false
| ~ spl18_187 ),
inference(forward_subsumption_resolution,[],[f39320,f66]) ).
fof(f39336,plain,
~ spl18_187,
inference(avatar_contradiction_clause,[],[f39335]) ).
fof(f39338,plain,
( ~ spl18_790
| ~ spl18_224
| ~ spl18_226 ),
inference(avatar_split_clause,[],[f8216,f2141,f2130,f7206]) ).
fof(f39347,plain,
( spl18_790
| ~ spl18_120
| ~ spl18_130
| ~ spl18_144 ),
inference(avatar_split_clause,[],[f4193,f1353,f1151,f999,f7206]) ).
fof(f39409,plain,
( ! [X0,X1] :
( r1(sK12(X0),sK14(X0))
| ~ r1(sK1,X0)
| ~ p1(X1)
| ~ r1(sK1,X1) )
| spl18_2
| ~ spl18_130
| ~ spl18_4230 ),
inference(forward_subsumption_resolution,[],[f38022,f131]) ).
fof(f39416,plain,
( spl18_144
| spl18_142
| ~ spl18_93 ),
inference(avatar_split_clause,[],[f39264,f833,f1343,f1353]) ).
fof(f39422,plain,
( ! [X2,X0,X1] :
( p1(X0)
| ~ sP17(X0)
| ~ r1(sK11(sK1),X0)
| r1(X1,sK12(X1))
| ~ r1(sK1,X1)
| ~ p1(X2)
| ~ r1(sK1,X2)
| ~ r1(sK0,sK1) )
| spl18_2
| ~ spl18_130 ),
inference(forward_subsumption_resolution,[],[f1742,f131]) ).
fof(f39428,plain,
( spl18_187
| spl18_131
| spl18_2
| ~ spl18_130
| ~ spl18_4230 ),
inference(avatar_split_clause,[],[f39409,f37928,f1151,f129,f1160,f1748]) ).
fof(f39434,plain,
( ! [X2,X0,X1] :
( p1(X0)
| ~ sP17(X0)
| ~ r1(sK11(sK1),X0)
| r1(X1,sK12(X1))
| ~ r1(sK1,X1)
| ~ p1(X2)
| ~ r1(sK1,X2) )
| spl18_2
| ~ spl18_130 ),
inference(forward_subsumption_resolution,[],[f39422,f65]) ).
fof(f39445,plain,
( spl18_187
| spl18_119
| spl18_189
| spl18_2
| ~ spl18_130 ),
inference(avatar_split_clause,[],[f39434,f1151,f129,f1755,f985,f1748]) ).
fof(f40026,plain,
( p1(sK13(sK11(sK1)))
| ~ sP17(sK13(sK11(sK1)))
| ~ spl18_145
| ~ spl18_189 ),
inference(resolution,[],[f1756,f1360]) ).
fof(f40033,plain,
( ~ sP17(sK13(sK11(sK1)))
| ~ spl18_145
| ~ spl18_189
| spl18_1143 ),
inference(forward_subsumption_resolution,[],[f40026,f10391]) ).
fof(f40036,plain,
( $false
| ~ spl18_145
| ~ spl18_189
| spl18_1143
| ~ spl18_4243 ),
inference(forward_subsumption_resolution,[],[f40033,f38077]) ).
fof(f40037,plain,
( ~ spl18_145
| ~ spl18_189
| spl18_1143
| ~ spl18_4243 ),
inference(avatar_contradiction_clause,[],[f40036]) ).
cnf(s182,plain,
( spl18_2
| spl18_94
| spl18_120 ),
inference(sat_conversion,[],[f1111]) ).
cnf(s183,plain,
( spl18_2
| spl18_93
| spl18_119 ),
inference(sat_conversion,[],[f1112]) ).
cnf(s222,plain,
( spl18_2
| spl18_119
| spl18_130 ),
inference(sat_conversion,[],[f1263]) ).
cnf(s246,plain,
( spl18_67
| spl18_68 ),
inference(sat_conversion,[],[f1441]) ).
cnf(s247,plain,
( spl18_67
| spl18_69 ),
inference(sat_conversion,[],[f1448]) ).
cnf(s285,plain,
( spl18_2
| spl18_93
| spl18_94 ),
inference(sat_conversion,[],[f1666]) ).
cnf(s286,plain,
( spl18_2
| spl18_94
| spl18_130 ),
inference(sat_conversion,[],[f1667]) ).
cnf(s287,plain,
( spl18_2
| spl18_130
| spl18_131 ),
inference(sat_conversion,[],[f1668]) ).
cnf(s313,plain,
( spl18_2
| spl18_94
| ~ spl18_130
| spl18_187
| spl18_189 ),
inference(sat_conversion,[],[f1758]) ).
cnf(s424,plain,
( ~ spl18_128
| ~ spl18_273 ),
inference(sat_conversion,[],[f2516]) ).
cnf(s437,plain,
~ spl18_67,
inference(sat_conversion,[],[f2620]) ).
cnf(s482,plain,
( spl18_2
| spl18_119
| spl18_120 ),
inference(sat_conversion,[],[f2885]) ).
cnf(s695,plain,
( ~ spl18_120
| ~ spl18_130
| ~ spl18_141
| spl18_224 ),
inference(sat_conversion,[],[f4110]) ).
cnf(s733,plain,
( ~ spl18_120
| ~ spl18_130
| ~ spl18_144
| spl18_226
| spl18_227
| spl18_228 ),
inference(sat_conversion,[],[f4358]) ).
cnf(s1150,plain,
( ~ spl18_224
| ~ spl18_227
| ~ spl18_790 ),
inference(sat_conversion,[],[f7209]) ).
cnf(s1203,plain,
( spl18_225
| spl18_226
| spl18_227
| ~ spl18_790 ),
inference(sat_conversion,[],[f7539]) ).
cnf(s1304,plain,
( spl18_226
| spl18_227
| spl18_229
| ~ spl18_790 ),
inference(sat_conversion,[],[f8240]) ).
cnf(s1421,plain,
( ~ spl18_94
| ~ spl18_119
| ~ spl18_131
| spl18_993
| spl18_994 ),
inference(sat_conversion,[],[f9042]) ).
cnf(s1499,plain,
( ~ spl18_94
| ~ spl18_119
| ~ spl18_131
| spl18_993
| spl18_1076 ),
inference(sat_conversion,[],[f9621]) ).
cnf(s1545,plain,
~ spl18_993,
inference(sat_conversion,[],[f10070]) ).
cnf(s1556,plain,
( ~ spl18_994
| ~ spl18_1076 ),
inference(sat_conversion,[],[f10159]) ).
cnf(s1571,plain,
( ~ spl18_93
| ~ spl18_120
| ~ spl18_130
| spl18_145
| ~ spl18_228 ),
inference(sat_conversion,[],[f10180]) ).
cnf(s1572,plain,
( ~ spl18_93
| ~ spl18_120
| ~ spl18_130
| spl18_143
| ~ spl18_229 ),
inference(sat_conversion,[],[f10181]) ).
cnf(s1579,plain,
( spl18_2
| ~ spl18_68
| ~ spl18_69
| spl18_120
| spl18_131 ),
inference(sat_conversion,[],[f10198]) ).
cnf(s1580,plain,
( ~ spl18_93
| spl18_141
| spl18_142 ),
inference(sat_conversion,[],[f10221]) ).
cnf(s1581,plain,
( ~ spl18_93
| spl18_141
| spl18_143 ),
inference(sat_conversion,[],[f10222]) ).
cnf(s1583,plain,
( ~ spl18_93
| spl18_143
| spl18_144 ),
inference(sat_conversion,[],[f10224]) ).
cnf(s1584,plain,
( ~ spl18_93
| spl18_144
| spl18_145 ),
inference(sat_conversion,[],[f10225]) ).
cnf(s1585,plain,
( ~ spl18_93
| spl18_141
| spl18_145 ),
inference(sat_conversion,[],[f10226]) ).
cnf(s1612,plain,
( ~ spl18_93
| spl18_141
| ~ spl18_1143 ),
inference(sat_conversion,[],[f10488]) ).
cnf(s1613,plain,
( ~ spl18_93
| spl18_144
| ~ spl18_1143 ),
inference(sat_conversion,[],[f10489]) ).
cnf(s5907,plain,
( ~ spl18_93
| ~ spl18_120
| ~ spl18_130
| ~ spl18_224
| spl18_227
| ~ spl18_790
| ~ spl18_1143 ),
inference(sat_conversion,[],[f37889]) ).
cnf(s5974,plain,
( ~ spl18_93
| ~ spl18_120
| ~ spl18_130
| spl18_142
| ~ spl18_225 ),
inference(sat_conversion,[],[f38079]) ).
cnf(s6019,plain,
( ~ spl18_2
| spl18_126
| spl18_127 ),
inference(sat_conversion,[],[f38263]) ).
cnf(s6020,plain,
( ~ spl18_2
| spl18_126
| spl18_128 ),
inference(sat_conversion,[],[f38264]) ).
cnf(s6021,plain,
( ~ spl18_2
| spl18_127
| spl18_129 ),
inference(sat_conversion,[],[f38265]) ).
cnf(s6022,plain,
( ~ spl18_2
| spl18_128
| spl18_129 ),
inference(sat_conversion,[],[f38266]) ).
cnf(s6110,plain,
( ~ spl18_126
| ~ spl18_129
| ~ spl18_4245 ),
inference(sat_conversion,[],[f38798]) ).
cnf(s6147,plain,
( spl18_1142
| spl18_1143
| ~ spl18_4243 ),
inference(sat_conversion,[],[f39061]) ).
cnf(s6155,plain,
( ~ spl18_126
| ~ spl18_129
| ~ spl18_4246 ),
inference(sat_conversion,[],[f39124]) ).
cnf(s6156,plain,
( ~ spl18_127
| spl18_273 ),
inference(sat_conversion,[],[f39126]) ).
cnf(s6171,plain,
( spl18_2
| ~ spl18_68
| ~ spl18_69
| spl18_93
| spl18_131 ),
inference(sat_conversion,[],[f39144]) ).
cnf(s6175,plain,
( ~ spl18_142
| ~ spl18_143
| spl18_4243 ),
inference(sat_conversion,[],[f39153]) ).
cnf(s6176,plain,
( ~ spl18_93
| ~ spl18_145
| ~ spl18_1142
| spl18_4230 ),
inference(sat_conversion,[],[f39156]) ).
cnf(s6191,plain,
( ~ spl18_142
| ~ spl18_143
| spl18_1142
| spl18_1143 ),
inference(sat_conversion,[],[f39190]) ).
cnf(s6212,plain,
( ~ spl18_2
| spl18_127
| ~ spl18_129
| spl18_4245
| spl18_4246 ),
inference(sat_conversion,[],[f39244]) ).
cnf(s6213,plain,
( ~ spl18_2
| spl18_128
| ~ spl18_129
| spl18_4245
| spl18_4246 ),
inference(sat_conversion,[],[f39245]) ).
cnf(s6222,plain,
~ spl18_187,
inference(sat_conversion,[],[f39336]) ).
cnf(s6223,plain,
( ~ spl18_224
| ~ spl18_226
| ~ spl18_790 ),
inference(sat_conversion,[],[f39338]) ).
cnf(s6226,plain,
( ~ spl18_120
| ~ spl18_130
| ~ spl18_144
| spl18_790 ),
inference(sat_conversion,[],[f39347]) ).
cnf(s6261,plain,
( ~ spl18_93
| spl18_142
| spl18_144 ),
inference(sat_conversion,[],[f39416]) ).
cnf(s6269,plain,
( spl18_2
| ~ spl18_130
| spl18_131
| spl18_187
| ~ spl18_4230 ),
inference(sat_conversion,[],[f39428]) ).
cnf(s6276,plain,
( spl18_2
| spl18_119
| ~ spl18_130
| spl18_187
| spl18_189 ),
inference(sat_conversion,[],[f39445]) ).
cnf(s6349,plain,
( ~ spl18_145
| ~ spl18_189
| spl18_1143
| ~ spl18_4243 ),
inference(sat_conversion,[],[f40037]) ).
cnf(s6357,plain,
( ~ spl18_94
| ~ spl18_119
| ~ spl18_131
| spl18_1076 ),
inference(rat,[],[s1499,s1545]) ).
cnf(s6358,plain,
( ~ spl18_94
| ~ spl18_119
| ~ spl18_131
| spl18_994 ),
inference(rat,[],[s1421,s1545]) ).
cnf(s6360,plain,
( spl18_2
| spl18_94
| ~ spl18_130
| spl18_189 ),
inference(rat,[],[s313,s6222]) ).
cnf(s6362,plain,
spl18_69,
inference(rat,[],[s247,s437]) ).
cnf(s6364,plain,
spl18_68,
inference(rat,[],[s246,s437]) ).
cnf(s6377,plain,
( ~ spl18_94
| ~ spl18_119
| ~ spl18_131 ),
inference(rat,[],[s1556,s6358,s6357]) ).
cnf(s6378,plain,
( spl18_93
| spl18_2 ),
inference(rat,[],[s6377,s183,s285,s6171,s6364,s6362]) ).
cnf(s6379,plain,
( spl18_141
| spl18_4230
| ~ spl18_93 ),
inference(rat,[],[s6191,s6176,s1580,s1581,s1585,s1612]) ).
cnf(s6380,plain,
( ~ spl18_1143
| ~ spl18_224
| ~ spl18_130
| ~ spl18_120
| ~ spl18_93 ),
inference(rat,[],[s5907,s1150,s6226,s1613]) ).
cnf(s6381,plain,
( spl18_145
| ~ spl18_224
| ~ spl18_130
| ~ spl18_120
| ~ spl18_93 ),
inference(rat,[],[s733,s1150,s6223,s6226,s1571,s1584]) ).
cnf(s6382,plain,
( spl18_143
| ~ spl18_224
| ~ spl18_130
| ~ spl18_120
| ~ spl18_93 ),
inference(rat,[],[s1304,s1150,s6223,s6226,s1572,s1583]) ).
cnf(s6383,plain,
( spl18_131
| spl18_2 ),
inference(rat,[],[s1203,s1150,s6223,s6226,s5974,s6261,s6175,s6382,s6147,s6176,s6381,s6380,s695,s6379,s6269,s287,s1579,s6378,s6222,s6362,s6364]) ).
cnf(s6384,plain,
( ~ spl18_224
| ~ spl18_189
| ~ spl18_130
| ~ spl18_120
| ~ spl18_93 ),
inference(rat,[],[s1203,s1150,s6223,s6226,s5974,s6261,s6175,s6349,s6382,s6381,s6380]) ).
cnf(s6385,plain,
( ~ spl18_189
| ~ spl18_130
| ~ spl18_93
| ~ spl18_120 ),
inference(rat,[],[s6175,s6349,s1580,s1581,s1585,s1612,s695,s6384]) ).
cnf(s6386,plain,
( spl18_119
| spl18_2 ),
inference(rat,[],[s6385,s6276,s222,s482,s6378,s6222]) ).
cnf(s6387,plain,
spl18_2,
inference(rat,[],[s6385,s6360,s182,s286,s6377,s6386,s6383,s6378]) ).
cnf(s6392,plain,
spl18_126,
inference(rat,[],[s6156,s424,s6019,s6020,s6387]) ).
cnf(s6393,plain,
spl18_128,
inference(rat,[],[s6213,s6110,s6155,s6022,s6387,s6392]) ).
cnf(s6396,plain,
~ spl18_273,
inference(rat,[],[s424,s6393]) ).
cnf(s6397,plain,
~ spl18_127,
inference(rat,[],[s6156,s6396]) ).
cnf(s6398,plain,
spl18_129,
inference(rat,[],[s6021,s6387,s6397]) ).
cnf(s6400,plain,
~ spl18_4246,
inference(rat,[],[s6155,s6392,s6398]) ).
cnf(s6401,plain,
~ spl18_4245,
inference(rat,[],[s6110,s6392,s6398]) ).
cnf(s6402,plain,
$false,
inference(rat,[],[s6212,s6400,s6397,s6387,s6398,s6401]) ).
fof(f40038,plain,
$false,
inference(avatar_sat_refutation,[],[s6402]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL658+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.37 % Computer : n004.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 16:21:07 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.41 Running first-order model finding
% 0.10/0.41 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
% 12.11/2.17 % (3712059)Will run a generic schedule for satisfiability detection.
% 12.11/2.17 % (3712064)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2199090310_2999 on theBenchmark for (2999ds/0Mi)
% 12.11/2.17 % TRYING [1]
% 12.11/2.17 % TRYING [2]
% 12.11/2.17 % TRYING [3]
% 12.11/2.17 % (3712065)% WARNING: option uhcvi not known.
% 12.11/2.17 % TRYING [4]
% 12.11/2.17 % (3712065)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=472532981:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 12.11/2.17 % (3712066)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3223066099:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 12.11/2.17 % (3712067)dis+10_1_sil=32000:sp=arity:random_seed=3091748405:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 12.11/2.17 % (3712069)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=382126619:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 12.11/2.17 % (3712068)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2207549234:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 12.11/2.17 % (3712070)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2092236933:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 12.11/2.17 % TRYING [5]
% 12.11/2.17 % TRYING [6]
% 12.11/2.17 % (3712068)Instruction limit reached!
% 12.11/2.17 % (3712068)------------------------------
% 12.11/2.17 % (3712068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.11/2.17 % (3712068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.17 % (3712068)CaDiCaL version: 2.1.3
% 12.11/2.17 % (3712068)Termination reason: Instruction limit
% 12.11/2.17 % (3712068)Termination phase: Saturation
% 12.11/2.17 % (3712068)Time elapsed: 0.060 s
% 12.11/2.17 % (3712068)Peak memory usage: 12 MB
% 12.11/2.17 % (3712068)Instructions burned: 118 (million)
% 12.11/2.17 % (3712067)Instruction limit reached!
% 12.11/2.17 % (3712067)------------------------------
% 12.11/2.17 % (3712067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.11/2.17 % (3712067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.17 % (3712067)CaDiCaL version: 2.1.3
% 12.11/2.17 % (3712067)Termination reason: Instruction limit
% 12.11/2.17 % (3712067)Termination phase: Saturation
% 12.11/2.17 % (3712067)Time elapsed: 0.066 s
% 12.11/2.17 % (3712067)Peak memory usage: 13 MB
% 12.11/2.17 % (3712067)Instructions burned: 104 (million)
% 12.11/2.17 % (3712078)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=161350293:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 12.11/2.17 % (3712069)Instruction limit reached!
% 12.11/2.17 % (3712069)------------------------------
% 12.11/2.17 % (3712069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.11/2.17 % (3712069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.17 % (3712069)CaDiCaL version: 2.1.3
% 12.11/2.17 % (3712069)Termination reason: Instruction limit
% 12.11/2.17 % (3712069)Termination phase: Saturation
% 12.11/2.17 % (3712069)Time elapsed: 0.082 s
% 12.11/2.17 % (3712069)Peak memory usage: 13 MB
% 12.11/2.17 % (3712069)Instructions burned: 132 (million)
% 12.11/2.17 % TRYING [1]
% 12.11/2.17 % TRYING [2]
% 12.11/2.17 % TRYING [3]
% 12.11/2.17 % TRYING [4]
% 12.11/2.17 % (3712079)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2469958453:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 12.11/2.17 % TRYING [5]
% 12.11/2.17 % (3712070)Instruction limit reached!
% 12.11/2.17 % (3712070)------------------------------
% 12.11/2.17 % (3712070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.11/2.17 % (3712070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.17 % (3712070)CaDiCaL version: 2.1.3
% 12.11/2.17 % (3712070)Termination reason: Instruction limit
% 12.11/2.17 % (3712070)Termination phase: Saturation
% 12.11/2.17 % (3712070)Time elapsed: 0.099 s
% 12.11/2.17 % (3712070)Peak memory usage: 14 MB
% 12.11/2.17 % (3712070)Instructions burned: 160 (million)
% 12.11/2.17 % (3712081)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=3814455991:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 12.11/2.17 % TRYING [7]
% 12.11/2.17 % (3712083)ott-21_1_sil=16000:fs=off:random_seed=518455278:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 12.11/2.17 % TRYING [6]
% 12.11/2.17 % (3712079)Instruction limit reached!
% 12.11/2.17 % (3712079)------------------------------
% 12.11/2.17 % (3712079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.11/2.17 % (3712079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.17 % (3712079)CaDiCaL version: 2.1.3
% 12.11/2.17 % (3712079)Termination reason: Instruction limit
% 12.11/2.17 % (3712079)Termination phase: Saturation
% 12.11/2.17 % (3712079)Time elapsed: 0.083 s
% 12.11/2.17 % (3712079)Peak memory usage: 13 MB
% 12.11/2.17 % (3712079)Instructions burned: 131 (million)
% 12.11/2.17 % (3712086)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3282008129:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 12.11/2.17 % (3712083)Instruction limit reached!
% 12.11/2.17 % (3712083)------------------------------
% 12.11/2.17 % (3712083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.11/2.17 % (3712083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.17 % (3712083)CaDiCaL version: 2.1.3
% 12.11/2.17 % (3712083)Termination reason: Instruction limit
% 12.11/2.17 % (3712083)Termination phase: Saturation
% 12.11/2.17 % (3712083)Time elapsed: 0.095 s
% 12.11/2.17 % (3712083)Peak memory usage: 13 MB
% 12.11/2.17 % (3712083)Instructions burned: 181 (million)
% 12.11/2.17 % (3712088)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3401041569:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 12.11/2.17 % TRYING [1]
% 12.11/2.17 % TRYING [2]
% 12.11/2.17 % TRYING [3]
% 12.11/2.17 % TRYING [7]
% 12.11/2.17 % TRYING [4]
% 12.11/2.17 % TRYING [5]
% 12.11/2.17 % TRYING [6]
% 12.11/2.17 % TRYING [7]
% 12.11/2.17 % (3712078)Instruction limit reached!
% 12.11/2.17 % (3712078)------------------------------
% 12.11/2.17 % (3712078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.11/2.17 % (3712078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.17 % (3712078)CaDiCaL version: 2.1.3
% 12.11/2.17 % (3712078)Termination reason: Instruction limit
% 12.11/2.17 % (3712078)Termination phase: Finite model building SAT solving
% 12.11/2.17 % (3712078)Time elapsed: 0.395 s
% 12.11/2.17 % (3712078)Peak memory usage: 13 MB
% 12.11/2.17 % (3712078)Instructions burned: 714 (million)
% 12.11/2.17 % (3712081)Instruction limit reached!
% 12.11/2.17 % (3712081)------------------------------
% 12.11/2.17 % (3712081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.11/2.17 % (3712081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.17 % (3712081)CaDiCaL version: 2.1.3
% 12.11/2.17 % (3712081)Termination reason: Instruction limit
% 12.11/2.17 % (3712081)Termination phase: Saturation
% 12.11/2.17 % (3712081)Time elapsed: 0.383 s
% 12.11/2.17 % (3712081)Peak memory usage: 17 MB
% 12.11/2.17 % (3712081)Instructions burned: 684 (million)
% 12.11/2.17 % (3712086)Instruction limit reached!
% 12.11/2.17 % (3712086)------------------------------
% 12.11/2.17 % (3712086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.11/2.17 % (3712086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.17 % (3712086)CaDiCaL version: 2.1.3
% 12.11/2.17 % (3712086)Termination reason: Instruction limit
% 12.11/2.17 % (3712086)Termination phase: Saturation
% 12.11/2.17 % (3712086)Time elapsed: 0.305 s
% 12.11/2.17 % (3712086)Peak memory usage: 15 MB
% 12.11/2.17 % (3712086)Instructions burned: 478 (million)
% 12.11/2.17 % (3712090)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3170865160:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 12.11/2.17 % TRYING [8]
% 12.11/2.17 % (3712091)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=960987796:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 12.11/2.17 % TRYING [14]
% 12.11/2.17 % (3712093)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=3035053698: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)
% 12.11/2.17 % (3712088)Instruction limit reached!
% 12.11/2.17 % (3712088)------------------------------
% 12.11/2.17 % (3712088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.11/2.17 % (3712088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.17 % (3712088)CaDiCaL version: 2.1.3
% 12.11/2.17 % (3712088)Termination reason: Instruction limit
% 12.11/2.17 % (3712088)Termination phase: Finite model building SAT solving
% 12.11/2.17 % (3712088)Time elapsed: 0.497 s
% 12.11/2.17 % (3712088)Peak memory usage: 13 MB
% 12.11/2.17 % (3712088)Instructions burned: 866 (million)
% 12.11/2.17 % (3712096)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3130564392:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 12.11/2.17 % (3712091)Instruction limit reached!
% 12.11/2.17 % (3712091)------------------------------
% 12.11/2.17 % (3712091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.11/2.17 % (3712091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.17 % (3712091)CaDiCaL version: 2.1.3
% 12.11/2.17 % (3712091)Termination reason: Instruction limit
% 12.11/2.17 % (3712091)Termination phase: Finite model building SAT solving
% 12.11/2.17 % (3712091)Time elapsed: 0.376 s
% 12.11/2.17 % (3712091)Peak memory usage: 19 MB
% 12.11/2.17 % (3712091)Instructions burned: 890 (million)
% 12.11/2.17 % (3712098)fmb+10_1_sil=64000:random_seed=2873276482:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 12.11/2.17 % TRYING [1]
% 12.11/2.17 % TRYING [2]
% 12.11/2.17 % (3712093)Instruction limit reached!
% 12.11/2.17 % (3712093)------------------------------
% 12.11/2.17 % (3712093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.11/2.17 % (3712093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.17 % (3712093)CaDiCaL version: 2.1.3
% 12.11/2.17 % (3712093)Termination reason: Instruction limit
% 12.11/2.17 % (3712093)Termination phase: Saturation
% 12.11/2.17 % (3712093)Time elapsed: 0.391 s
% 12.11/2.17 % (3712093)Peak memory usage: 16 MB
% 12.11/2.17 % (3712093)Instructions burned: 692 (million)
% 12.11/2.17 % TRYING [3]
% 12.11/2.17 % TRYING [4]
% 12.11/2.17 % TRYING [5]
% 12.11/2.17 % (3712100)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1834037983:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 12.11/2.17 % TRYING [20]
% 12.11/2.17 % TRYING [6]
% 12.11/2.17 % TRYING [7]
% 12.11/2.17 % TRYING [8]
% 12.11/2.17 % (3712090)Instruction limit reached!
% 12.11/2.17 % (3712090)------------------------------
% 12.11/2.17 % (3712090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.11/2.17 % (3712090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.17 % (3712090)CaDiCaL version: 2.1.3
% 12.11/2.17 % (3712090)Termination reason: Instruction limit
% 12.11/2.17 % (3712090)Termination phase: Saturation
% 12.11/2.17 % (3712090)Time elapsed: 0.646 s
% 12.11/2.17 % (3712090)Peak memory usage: 23 MB
% 12.11/2.17 % (3712090)Instructions burned: 1179 (million)
% 12.11/2.17 % (3712102)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=585717388:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 12.11/2.17 % TRYING [8]
% 12.11/2.17 % (3712096)Instruction limit reached!
% 12.11/2.17 % (3712096)------------------------------
% 12.11/2.17 % (3712096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.11/2.17 % (3712096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.17 % (3712096)CaDiCaL version: 2.1.3
% 12.11/2.17 % (3712096)Termination reason: Instruction limit
% 12.11/2.17 % (3712096)Termination phase: Saturation
% 12.11/2.17 % (3712096)Time elapsed: 0.459 s
% 12.11/2.17 % (3712096)Peak memory usage: 15 MB
% 12.11/2.17 % (3712096)Instructions burned: 881 (million)
% 12.11/2.17 % (3712104)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=348936599:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 12.11/2.17 % (3712102)Instruction limit reached!
% 12.11/2.17 % (3712102)------------------------------
% 12.11/2.17 % (3712102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.11/2.17 % (3712102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.17 % (3712102)CaDiCaL version: 2.1.3
% 12.11/2.17 % (3712102)Termination reason: Instruction limit
% 12.11/2.17 % (3712102)Termination phase: Finite model building SAT solving
% 12.11/2.17 % (3712102)Time elapsed: 0.464 s
% 12.11/2.17 % (3712102)Peak memory usage: 14 MB
% 12.11/2.17 % (3712102)Instructions burned: 920 (million)
% 12.11/2.17 % (3712106)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3027407582:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 12.11/2.17 % (3712065) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3712059-3712065"...
% 12.11/2.17 % (3712065)...printing done.
% 12.11/2.17 % (3712065)Refutation found. Thanks to Tanya!
% 12.11/2.17 % SZS status Theorem for theBenchmark
% 12.11/2.17 % SZS output start Proof for theBenchmark
% See solution above
% 12.11/2.17 % (3712065)------------------------------
% 12.11/2.17 % (3712065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.11/2.17 % (3712065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.17 % (3712065)CaDiCaL version: 2.1.3
% 12.11/2.17 % (3712065)Termination reason: Refutation
% 12.11/2.17 % (3712065)Time elapsed: 1.705 s
% 12.11/2.17 % (3712065)Peak memory usage: 32 MB
% 12.11/2.17 % (3712065)Instructions burned: 2966 (million)
% 12.11/2.17 % (3712059)Success in time 1.75 s
% 12.11/2.17 % Vampire exiting
%------------------------------------------------------------------------------