%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN917+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n006.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 02:05:58 PM UTC 2026
% Result : Theorem 0.63s 0.96s
% Output : Refutation 2.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 20
% Syntax : Number of formulae : 335 ( 19 unt; 19 def)
% Number of atoms : 2224 ( 0 equ)
% Maximal formula atoms : 94 ( 6 avg)
% Number of connectives : 2817 ( 928 ~;1350 |; 371 &)
% ( 30 <=>; 108 =>; 0 <=; 30 <~>)
% Maximal formula depth : 28 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 27 ( 26 usr; 21 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 29 con; 0-1 aty)
% Number of variables : 685 ( 482 !; 203 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( ( ( ! [X0] :
( ( ( f(X0)
& g(X0) )
=> h(X0) )
=> ? [X1] :
( f(X1)
& ~ g(X1) ) )
& ( ! [X2] :
( f(X2)
=> g(X2) )
| ! [X3] :
( f(X3)
=> h(X3) ) ) )
=> ( ! [X4] :
( ( f(X4)
& h(X4) )
=> g(X4) )
=> ? [X5] :
( f(X5)
& g(X5)
& ~ h(X5) ) ) )
& ( ( ! [X0,X1] :
( r(X0,X1)
=> r(X1,X0) )
& ! [X0,X1,X3] :
( ( r(X0,X1)
& r(X1,X3) )
=> r(X0,X3) ) )
=> ! [X0,X1] :
( r(X0,X1)
=> r(X0,X0) ) )
& ( ( ( ! [X0] :
( ( f(X0)
& g(X0) )
=> h(X0) )
=> ? [X0] :
( f(X0)
& ~ g(X0) ) )
& ( ! [X2] :
( f(X2)
=> g(X2) )
| ! [X3] :
( f(X3)
=> h(X3) ) ) )
=> ( ! [X4] :
( ( f(X4)
& h(X4) )
=> g(X4) )
=> ? [X5] :
( f(X5)
& g(X5)
& ~ h(X5) ) ) )
& ? [X0] :
! [X1] :
( ( p(X1)
=> q(X0) )
=> ( p(X0)
=> q(X0) ) )
& ( ! [X0] :
( p(X0)
& q(X0) )
<=> ( ! [X0] : p(X0)
& ! [X0] : q(X0) ) )
& ( ( ! [X0] : p(X0)
| ! [X0] : q(X0) )
=> ! [X0] :
( p(X0)
| q(X0) ) )
& ( ? [X0] :
( p(X0)
| q(X0) )
<=> ( ? [X0] : p(X0)
| ? [X0] : q(X0) ) )
& ? [X1] :
( p(X1)
=> ! [X0] : p(X0) )
& ( ? [X0] :
( p(X0)
& q(X0) )
=> ( ? [X0] : p(X0)
& ? [X0] : q(X0) ) )
& ! [X1] :
( ! [X0] : p(X0)
=> p(X1) )
& ( ! [X0] : p(X0)
=> ? [X0] : p(X0) )
& ( ~ ? [X1] : p(X1)
=> ! [X1] :
( ? [X0] : p(X0)
=> p(X1) ) )
& ( ! [X0] :
( p(X0)
| c )
<=> ( ! [X0] : p(X0)
| c ) )
& ( ? [X0] :
( p(X0)
& c )
<=> ( ? [X0] : p(X0)
& c ) )
& ( ? [X0] : c
<=> c )
& ( ! [X0] : c
<=> c )
& ( ? [X0] :
( c
=> p(X0) )
<=> ( c
=> ? [X0] : p(X0) ) )
& ( ? [X0] :
( p(X0)
=> c )
<=> ( ! [X0] : p(X0)
=> c ) )
& ( ! [X0] :
( c
=> p(X0) )
<=> ( c
=> ! [X0] : p(X0) ) )
& ( ! [X0] :
( p(X0)
=> c )
<=> ( ? [X0] : p(X0)
=> c ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
fof(f2,negated_conjecture,
~ ( ( ( ! [X0] :
( ( ( f(X0)
& g(X0) )
=> h(X0) )
=> ? [X1] :
( f(X1)
& ~ g(X1) ) )
& ( ! [X2] :
( f(X2)
=> g(X2) )
| ! [X3] :
( f(X3)
=> h(X3) ) ) )
=> ( ! [X4] :
( ( f(X4)
& h(X4) )
=> g(X4) )
=> ? [X5] :
( f(X5)
& g(X5)
& ~ h(X5) ) ) )
& ( ( ! [X0,X1] :
( r(X0,X1)
=> r(X1,X0) )
& ! [X0,X1,X3] :
( ( r(X0,X1)
& r(X1,X3) )
=> r(X0,X3) ) )
=> ! [X0,X1] :
( r(X0,X1)
=> r(X0,X0) ) )
& ( ( ( ! [X0] :
( ( f(X0)
& g(X0) )
=> h(X0) )
=> ? [X0] :
( f(X0)
& ~ g(X0) ) )
& ( ! [X2] :
( f(X2)
=> g(X2) )
| ! [X3] :
( f(X3)
=> h(X3) ) ) )
=> ( ! [X4] :
( ( f(X4)
& h(X4) )
=> g(X4) )
=> ? [X5] :
( f(X5)
& g(X5)
& ~ h(X5) ) ) )
& ? [X0] :
! [X1] :
( ( p(X1)
=> q(X0) )
=> ( p(X0)
=> q(X0) ) )
& ( ! [X0] :
( p(X0)
& q(X0) )
<=> ( ! [X0] : p(X0)
& ! [X0] : q(X0) ) )
& ( ( ! [X0] : p(X0)
| ! [X0] : q(X0) )
=> ! [X0] :
( p(X0)
| q(X0) ) )
& ( ? [X0] :
( p(X0)
| q(X0) )
<=> ( ? [X0] : p(X0)
| ? [X0] : q(X0) ) )
& ? [X1] :
( p(X1)
=> ! [X0] : p(X0) )
& ( ? [X0] :
( p(X0)
& q(X0) )
=> ( ? [X0] : p(X0)
& ? [X0] : q(X0) ) )
& ! [X1] :
( ! [X0] : p(X0)
=> p(X1) )
& ( ! [X0] : p(X0)
=> ? [X0] : p(X0) )
& ( ~ ? [X1] : p(X1)
=> ! [X1] :
( ? [X0] : p(X0)
=> p(X1) ) )
& ( ! [X0] :
( p(X0)
| c )
<=> ( ! [X0] : p(X0)
| c ) )
& ( ? [X0] :
( p(X0)
& c )
<=> ( ? [X0] : p(X0)
& c ) )
& ( ? [X0] : c
<=> c )
& ( ! [X0] : c
<=> c )
& ( ? [X0] :
( c
=> p(X0) )
<=> ( c
=> ? [X0] : p(X0) ) )
& ( ? [X0] :
( p(X0)
=> c )
<=> ( ! [X0] : p(X0)
=> c ) )
& ( ! [X0] :
( c
=> p(X0) )
<=> ( c
=> ! [X0] : p(X0) ) )
& ( ! [X0] :
( p(X0)
=> c )
<=> ( ? [X0] : p(X0)
=> c ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
~ ( ( ( ! [X0] :
( ( ( f(X0)
& g(X0) )
=> h(X0) )
=> ? [X1] :
( f(X1)
& ~ g(X1) ) )
& ( ! [X2] :
( f(X2)
=> g(X2) )
| ! [X3] :
( f(X3)
=> h(X3) ) ) )
=> ( ! [X4] :
( ( f(X4)
& h(X4) )
=> g(X4) )
=> ? [X5] :
( f(X5)
& g(X5)
& ~ h(X5) ) ) )
& ( ( ! [X6,X7] :
( r(X6,X7)
=> r(X7,X6) )
& ! [X8,X9,X10] :
( ( r(X8,X9)
& r(X9,X10) )
=> r(X8,X10) ) )
=> ! [X11,X12] :
( r(X11,X12)
=> r(X11,X11) ) )
& ( ( ( ! [X13] :
( ( f(X13)
& g(X13) )
=> h(X13) )
=> ? [X14] :
( f(X14)
& ~ g(X14) ) )
& ( ! [X15] :
( f(X15)
=> g(X15) )
| ! [X16] :
( f(X16)
=> h(X16) ) ) )
=> ( ! [X17] :
( ( f(X17)
& h(X17) )
=> g(X17) )
=> ? [X18] :
( f(X18)
& g(X18)
& ~ h(X18) ) ) )
& ? [X19] :
! [X20] :
( ( p(X20)
=> q(X19) )
=> ( p(X19)
=> q(X19) ) )
& ( ! [X21] :
( p(X21)
& q(X21) )
<=> ( ! [X22] : p(X22)
& ! [X23] : q(X23) ) )
& ( ( ! [X24] : p(X24)
| ! [X25] : q(X25) )
=> ! [X26] :
( p(X26)
| q(X26) ) )
& ( ? [X27] :
( p(X27)
| q(X27) )
<=> ( ? [X28] : p(X28)
| ? [X29] : q(X29) ) )
& ? [X30] :
( p(X30)
=> ! [X31] : p(X31) )
& ( ? [X32] :
( p(X32)
& q(X32) )
=> ( ? [X33] : p(X33)
& ? [X34] : q(X34) ) )
& ! [X35] :
( ! [X36] : p(X36)
=> p(X35) )
& ( ! [X37] : p(X37)
=> ? [X38] : p(X38) )
& ( ~ ? [X39] : p(X39)
=> ! [X40] :
( ? [X41] : p(X41)
=> p(X40) ) )
& ( ! [X42] :
( p(X42)
| c )
<=> ( ! [X43] : p(X43)
| c ) )
& ( ? [X44] :
( p(X44)
& c )
<=> ( ? [X45] : p(X45)
& c ) )
& ( c
<=> c )
& ( c
<=> c )
& ( ? [X48] :
( c
=> p(X48) )
<=> ( c
=> ? [X49] : p(X49) ) )
& ( ? [X50] :
( p(X50)
=> c )
<=> ( ! [X51] : p(X51)
=> c ) )
& ( ! [X52] :
( c
=> p(X52) )
<=> ( c
=> ! [X53] : p(X53) ) )
& ( ! [X54] :
( p(X54)
=> c )
<=> ( ? [X55] : p(X55)
=> c ) ) ),
inference(rectify,[],[f2]) ).
fof(f4,plain,
( ( ! [X5] :
( ~ f(X5)
| ~ g(X5)
| h(X5) )
& ! [X4] :
( g(X4)
| ~ f(X4)
| ~ h(X4) )
& ! [X0] :
( ? [X1] :
( f(X1)
& ~ g(X1) )
| ( ~ h(X0)
& f(X0)
& g(X0) ) )
& ( ! [X2] :
( g(X2)
| ~ f(X2) )
| ! [X3] :
( h(X3)
| ~ f(X3) ) ) )
| ( ? [X11,X12] :
( ~ r(X11,X11)
& r(X11,X12) )
& ! [X6,X7] :
( r(X7,X6)
| ~ r(X6,X7) )
& ! [X8,X9,X10] :
( r(X8,X10)
| ~ r(X8,X9)
| ~ r(X9,X10) ) )
| ( ! [X18] :
( ~ f(X18)
| ~ g(X18)
| h(X18) )
& ! [X17] :
( g(X17)
| ~ f(X17)
| ~ h(X17) )
& ( ? [X14] :
( f(X14)
& ~ g(X14) )
| ? [X13] :
( ~ h(X13)
& f(X13)
& g(X13) ) )
& ( ! [X15] :
( g(X15)
| ~ f(X15) )
| ! [X16] :
( h(X16)
| ~ f(X16) ) ) )
| ! [X19] :
? [X20] :
( ~ q(X19)
& p(X19)
& ( q(X19)
| ~ p(X20) ) )
| ( ! [X21] :
( p(X21)
& q(X21) )
<~> ( ! [X22] : p(X22)
& ! [X23] : q(X23) ) )
| ( ? [X26] :
( ~ p(X26)
& ~ q(X26) )
& ( ! [X24] : p(X24)
| ! [X25] : q(X25) ) )
| ( ? [X27] :
( p(X27)
| q(X27) )
<~> ( ? [X28] : p(X28)
| ? [X29] : q(X29) ) )
| ! [X30] :
( ? [X31] : ~ p(X31)
& p(X30) )
| ( ( ! [X33] : ~ p(X33)
| ! [X34] : ~ q(X34) )
& ? [X32] :
( p(X32)
& q(X32) ) )
| ? [X35] :
( ~ p(X35)
& ! [X36] : p(X36) )
| ( ! [X38] : ~ p(X38)
& ! [X37] : p(X37) )
| ( ? [X40] :
( ~ p(X40)
& ? [X41] : p(X41) )
& ! [X39] : ~ p(X39) )
| ( ! [X42] :
( p(X42)
| c )
<~> ( ! [X43] : p(X43)
| c ) )
| ( ? [X44] :
( p(X44)
& c )
<~> ( ? [X45] : p(X45)
& c ) )
| ( c
<~> c )
| ( c
<~> c )
| ( ? [X48] :
( p(X48)
| ~ c )
<~> ( ? [X49] : p(X49)
| ~ c ) )
| ( ? [X50] :
( c
| ~ p(X50) )
<~> ( c
| ? [X51] : ~ p(X51) ) )
| ( ! [X52] :
( p(X52)
| ~ c )
<~> ( ! [X53] : p(X53)
| ~ c ) )
| ( ! [X54] :
( c
| ~ p(X54) )
<~> ( c
| ! [X55] : ~ p(X55) ) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f5,plain,
( ( ! [X5] :
( ~ f(X5)
| ~ g(X5)
| h(X5) )
& ! [X4] :
( g(X4)
| ~ f(X4)
| ~ h(X4) )
& ! [X0] :
( ? [X1] :
( f(X1)
& ~ g(X1) )
| ( ~ h(X0)
& f(X0)
& g(X0) ) )
& ( ! [X2] :
( g(X2)
| ~ f(X2) )
| ! [X3] :
( h(X3)
| ~ f(X3) ) ) )
| ( ? [X11,X12] :
( ~ r(X11,X11)
& r(X11,X12) )
& ! [X6,X7] :
( r(X7,X6)
| ~ r(X6,X7) )
& ! [X8,X9,X10] :
( r(X8,X10)
| ~ r(X8,X9)
| ~ r(X9,X10) ) )
| ( ! [X18] :
( ~ f(X18)
| ~ g(X18)
| h(X18) )
& ! [X17] :
( g(X17)
| ~ f(X17)
| ~ h(X17) )
& ( ? [X14] :
( f(X14)
& ~ g(X14) )
| ? [X13] :
( ~ h(X13)
& f(X13)
& g(X13) ) )
& ( ! [X15] :
( g(X15)
| ~ f(X15) )
| ! [X16] :
( h(X16)
| ~ f(X16) ) ) )
| ! [X19] :
? [X20] :
( ~ q(X19)
& p(X19)
& ( q(X19)
| ~ p(X20) ) )
| ( ! [X21] :
( p(X21)
& q(X21) )
<~> ( ! [X22] : p(X22)
& ! [X23] : q(X23) ) )
| ( ? [X26] :
( ~ p(X26)
& ~ q(X26) )
& ( ! [X24] : p(X24)
| ! [X25] : q(X25) ) )
| ( ? [X27] :
( p(X27)
| q(X27) )
<~> ( ? [X28] : p(X28)
| ? [X29] : q(X29) ) )
| ! [X30] :
( ? [X31] : ~ p(X31)
& p(X30) )
| ( ( ! [X33] : ~ p(X33)
| ! [X34] : ~ q(X34) )
& ? [X32] :
( p(X32)
& q(X32) ) )
| ? [X35] :
( ~ p(X35)
& ! [X36] : p(X36) )
| ( ! [X38] : ~ p(X38)
& ! [X37] : p(X37) )
| ( ? [X40] :
( ~ p(X40)
& ? [X41] : p(X41) )
& ! [X39] : ~ p(X39) )
| ( ! [X42] :
( p(X42)
| c )
<~> ( ! [X43] : p(X43)
| c ) )
| ( ? [X44] :
( p(X44)
& c )
<~> ( ? [X45] : p(X45)
& c ) )
| ( c
<~> c )
| ( c
<~> c )
| ( ? [X48] :
( p(X48)
| ~ c )
<~> ( ? [X49] : p(X49)
| ~ c ) )
| ( ? [X50] :
( c
| ~ p(X50) )
<~> ( c
| ? [X51] : ~ p(X51) ) )
| ( ! [X52] :
( p(X52)
| ~ c )
<~> ( ! [X53] : p(X53)
| ~ c ) )
| ( ! [X54] :
( c
| ~ p(X54) )
<~> ( c
| ! [X55] : ~ p(X55) ) ) ),
inference(flattening,[],[f4]) ).
fof(f6,definition,
( ? [X14] :
( f(X14)
& ~ g(X14) )
| ? [X13] :
( ~ h(X13)
& f(X13)
& g(X13) )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f7,definition,
( ! [X0] :
( ? [X1] :
( f(X1)
& ~ g(X1) )
| ( ~ h(X0)
& f(X0)
& g(X0) ) )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f8,definition,
( ( ! [X54] :
( c
| ~ p(X54) )
<~> ( c
| ! [X55] : ~ p(X55) ) )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f9,definition,
( ( ! [X52] :
( p(X52)
| ~ c )
<~> ( ! [X53] : p(X53)
| ~ c ) )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f10,definition,
( ( ? [X50] :
( c
| ~ p(X50) )
<~> ( c
| ? [X51] : ~ p(X51) ) )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f11,definition,
( ( ? [X48] :
( p(X48)
| ~ c )
<~> ( ? [X49] : p(X49)
| ~ c ) )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f12,definition,
( ( ? [X44] :
( p(X44)
& c )
<~> ( ? [X45] : p(X45)
& c ) )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f13,definition,
( ( ! [X42] :
( p(X42)
| c )
<~> ( ! [X43] : p(X43)
| c ) )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f14,definition,
( ( ? [X27] :
( p(X27)
| q(X27) )
<~> ( ? [X28] : p(X28)
| ? [X29] : q(X29) ) )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f15,definition,
( ( ! [X21] :
( p(X21)
& q(X21) )
<~> ( ! [X22] : p(X22)
& ! [X23] : q(X23) ) )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f16,definition,
( ( ! [X18] :
( ~ f(X18)
| ~ g(X18)
| h(X18) )
& ! [X17] :
( g(X17)
| ~ f(X17)
| ~ h(X17) )
& sP0
& ( ! [X15] :
( g(X15)
| ~ f(X15) )
| ! [X16] :
( h(X16)
| ~ f(X16) ) ) )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f17,definition,
( ( ? [X11,X12] :
( ~ r(X11,X11)
& r(X11,X12) )
& ! [X6,X7] :
( r(X7,X6)
| ~ r(X6,X7) )
& ! [X8,X9,X10] :
( r(X8,X10)
| ~ r(X8,X9)
| ~ r(X9,X10) ) )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f18,definition,
( ( ! [X5] :
( ~ f(X5)
| ~ g(X5)
| h(X5) )
& ! [X4] :
( g(X4)
| ~ f(X4)
| ~ h(X4) )
& sP1
& ( ! [X2] :
( g(X2)
| ~ f(X2) )
| ! [X3] :
( h(X3)
| ~ f(X3) ) ) )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f19,definition,
( ( ? [X40] :
( ~ p(X40)
& ? [X41] : p(X41) )
& ! [X39] : ~ p(X39) )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f20,definition,
( ( ( ! [X33] : ~ p(X33)
| ! [X34] : ~ q(X34) )
& ? [X32] :
( p(X32)
& q(X32) ) )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f21,definition,
( ( ? [X26] :
( ~ p(X26)
& ~ q(X26) )
& ( ! [X24] : p(X24)
| ! [X25] : q(X25) ) )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f22,definition,
( ! [X19] :
? [X20] :
( ~ q(X19)
& p(X19)
& ( q(X19)
| ~ p(X20) ) )
| ~ sP16 ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f23,definition,
( ( c
<~> c )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f24,definition,
( ( c
<~> c )
| ~ sP18 ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f25,plain,
( sP12
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| ! [X30] :
( ? [X31] : ~ p(X31)
& p(X30) )
| sP14
| ? [X35] :
( ~ p(X35)
& ! [X36] : p(X36) )
| ( ! [X38] : ~ p(X38)
& ! [X37] : p(X37) )
| sP13
| sP7
| sP6
| sP18
| sP17
| sP5
| sP4
| sP3
| sP2 ),
inference(definition_folding,[],[f5,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10,f9,f8,f7,f6]) ).
fof(f26,plain,
( ( ( ~ c
| ~ c )
& ( c
| c ) )
| ~ sP18 ),
inference(nnf_transformation,[],[f24]) ).
fof(f27,plain,
( ( ( ~ c
| ~ c )
& ( c
| c ) )
| ~ sP17 ),
inference(nnf_transformation,[],[f23]) ).
fof(f28,plain,
( ! [X19] :
? [X20] :
( ~ q(X19)
& p(X19)
& ( q(X19)
| ~ p(X20) ) )
| ~ sP16 ),
inference(nnf_transformation,[],[f22]) ).
fof(f29,plain,
( ! [X0] :
? [X1] :
( ~ q(X0)
& p(X0)
& ( q(X0)
| ~ p(X1) ) )
| ~ sP16 ),
inference(rectify,[],[f28]) ).
fof(f30,plain,
( ! [X0] :
( ~ q(X0)
& p(X0)
& ( q(X0)
| ~ p(sK19(X0)) ) )
| ~ sP16 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(X1,sK19(X0))],[f29]) ).
fof(f31,plain,
( ( ? [X26] :
( ~ p(X26)
& ~ q(X26) )
& ( ! [X24] : p(X24)
| ! [X25] : q(X25) ) )
| ~ sP15 ),
inference(nnf_transformation,[],[f21]) ).
fof(f32,plain,
( ( ? [X0] :
( ~ p(X0)
& ~ q(X0) )
& ( ! [X1] : p(X1)
| ! [X2] : q(X2) ) )
| ~ sP15 ),
inference(rectify,[],[f31]) ).
fof(f33,plain,
( ( ~ p(sK20)
& ~ q(sK20)
& ( ! [X1] : p(X1)
| ! [X2] : q(X2) ) )
| ~ sP15 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(X0,sK20)],[f32]) ).
fof(f34,plain,
( ( ( ! [X33] : ~ p(X33)
| ! [X34] : ~ q(X34) )
& ? [X32] :
( p(X32)
& q(X32) ) )
| ~ sP14 ),
inference(nnf_transformation,[],[f20]) ).
fof(f35,plain,
( ( ( ! [X0] : ~ p(X0)
| ! [X1] : ~ q(X1) )
& ? [X2] :
( p(X2)
& q(X2) ) )
| ~ sP14 ),
inference(rectify,[],[f34]) ).
fof(f36,plain,
( ( ( ! [X0] : ~ p(X0)
| ! [X1] : ~ q(X1) )
& p(sK21)
& q(sK21) )
| ~ sP14 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(X2,sK21)],[f35]) ).
fof(f37,plain,
( ( ? [X40] :
( ~ p(X40)
& ? [X41] : p(X41) )
& ! [X39] : ~ p(X39) )
| ~ sP13 ),
inference(nnf_transformation,[],[f19]) ).
fof(f38,plain,
( ( ? [X0] :
( ~ p(X0)
& ? [X1] : p(X1) )
& ! [X2] : ~ p(X2) )
| ~ sP13 ),
inference(rectify,[],[f37]) ).
fof(f39,plain,
( ( ~ p(sK22)
& p(sK23)
& ! [X2] : ~ p(X2) )
| ~ sP13 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22,sK23]),skolemize(X0,sK22),skolemize(X1,sK23)],[f38]) ).
fof(f40,plain,
( ( ! [X5] :
( ~ f(X5)
| ~ g(X5)
| h(X5) )
& ! [X4] :
( g(X4)
| ~ f(X4)
| ~ h(X4) )
& sP1
& ( ! [X2] :
( g(X2)
| ~ f(X2) )
| ! [X3] :
( h(X3)
| ~ f(X3) ) ) )
| ~ sP12 ),
inference(nnf_transformation,[],[f18]) ).
fof(f41,plain,
( ( ! [X0] :
( ~ f(X0)
| ~ g(X0)
| h(X0) )
& ! [X1] :
( g(X1)
| ~ f(X1)
| ~ h(X1) )
& sP1
& ( ! [X2] :
( g(X2)
| ~ f(X2) )
| ! [X3] :
( h(X3)
| ~ f(X3) ) ) )
| ~ sP12 ),
inference(rectify,[],[f40]) ).
fof(f42,plain,
( ( ? [X11,X12] :
( ~ r(X11,X11)
& r(X11,X12) )
& ! [X6,X7] :
( r(X7,X6)
| ~ r(X6,X7) )
& ! [X8,X9,X10] :
( r(X8,X10)
| ~ r(X8,X9)
| ~ r(X9,X10) ) )
| ~ sP11 ),
inference(nnf_transformation,[],[f17]) ).
fof(f43,plain,
( ( ? [X0,X1] :
( ~ r(X0,X0)
& r(X0,X1) )
& ! [X2,X3] :
( r(X3,X2)
| ~ r(X2,X3) )
& ! [X4,X5,X6] :
( r(X4,X6)
| ~ r(X4,X5)
| ~ r(X5,X6) ) )
| ~ sP11 ),
inference(rectify,[],[f42]) ).
fof(f44,plain,
( ( ~ r(sK24,sK24)
& r(sK24,sK25)
& ! [X2,X3] :
( r(X3,X2)
| ~ r(X2,X3) )
& ! [X4,X5,X6] :
( r(X4,X6)
| ~ r(X4,X5)
| ~ r(X5,X6) ) )
| ~ sP11 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24,sK25]),skolemize(X0,sK24),skolemize(X1,sK25)],[f43]) ).
fof(f45,plain,
( ( ! [X18] :
( ~ f(X18)
| ~ g(X18)
| h(X18) )
& ! [X17] :
( g(X17)
| ~ f(X17)
| ~ h(X17) )
& sP0
& ( ! [X15] :
( g(X15)
| ~ f(X15) )
| ! [X16] :
( h(X16)
| ~ f(X16) ) ) )
| ~ sP10 ),
inference(nnf_transformation,[],[f16]) ).
fof(f46,plain,
( ( ! [X0] :
( ~ f(X0)
| ~ g(X0)
| h(X0) )
& ! [X1] :
( g(X1)
| ~ f(X1)
| ~ h(X1) )
& sP0
& ( ! [X2] :
( g(X2)
| ~ f(X2) )
| ! [X3] :
( h(X3)
| ~ f(X3) ) ) )
| ~ sP10 ),
inference(rectify,[],[f45]) ).
fof(f47,plain,
( ( ( ? [X22] : ~ p(X22)
| ? [X23] : ~ q(X23)
| ? [X21] :
( ~ p(X21)
| ~ q(X21) ) )
& ( ( ! [X22] : p(X22)
& ! [X23] : q(X23) )
| ! [X21] :
( p(X21)
& q(X21) ) ) )
| ~ sP9 ),
inference(nnf_transformation,[],[f15]) ).
fof(f48,plain,
( ( ( ? [X22] : ~ p(X22)
| ? [X23] : ~ q(X23)
| ? [X21] :
( ~ p(X21)
| ~ q(X21) ) )
& ( ( ! [X22] : p(X22)
& ! [X23] : q(X23) )
| ! [X21] :
( p(X21)
& q(X21) ) ) )
| ~ sP9 ),
inference(flattening,[],[f47]) ).
fof(f49,plain,
( ( ( ? [X0] : ~ p(X0)
| ? [X1] : ~ q(X1)
| ? [X2] :
( ~ p(X2)
| ~ q(X2) ) )
& ( ( ! [X3] : p(X3)
& ! [X4] : q(X4) )
| ! [X5] :
( p(X5)
& q(X5) ) ) )
| ~ sP9 ),
inference(rectify,[],[f48]) ).
fof(f50,plain,
( ( ( ~ p(sK26)
| ~ q(sK27)
| ~ p(sK28)
| ~ q(sK28) )
& ( ( ! [X3] : p(X3)
& ! [X4] : q(X4) )
| ! [X5] :
( p(X5)
& q(X5) ) ) )
| ~ sP9 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26,sK27,sK28]),skolemize(X0,sK26),skolemize(X1,sK27),skolemize(X2,sK28)],[f49]) ).
fof(f51,plain,
( ( ( ( ! [X28] : ~ p(X28)
& ! [X29] : ~ q(X29) )
| ! [X27] :
( ~ p(X27)
& ~ q(X27) ) )
& ( ? [X28] : p(X28)
| ? [X29] : q(X29)
| ? [X27] :
( p(X27)
| q(X27) ) ) )
| ~ sP8 ),
inference(nnf_transformation,[],[f14]) ).
fof(f52,plain,
( ( ( ( ! [X28] : ~ p(X28)
& ! [X29] : ~ q(X29) )
| ! [X27] :
( ~ p(X27)
& ~ q(X27) ) )
& ( ? [X28] : p(X28)
| ? [X29] : q(X29)
| ? [X27] :
( p(X27)
| q(X27) ) ) )
| ~ sP8 ),
inference(flattening,[],[f51]) ).
fof(f53,plain,
( ( ( ( ! [X0] : ~ p(X0)
& ! [X1] : ~ q(X1) )
| ! [X2] :
( ~ p(X2)
& ~ q(X2) ) )
& ( ? [X3] : p(X3)
| ? [X4] : q(X4)
| ? [X5] :
( p(X5)
| q(X5) ) ) )
| ~ sP8 ),
inference(rectify,[],[f52]) ).
fof(f54,plain,
( ( ( ( ! [X0] : ~ p(X0)
& ! [X1] : ~ q(X1) )
| ! [X2] :
( ~ p(X2)
& ~ q(X2) ) )
& ( p(sK29)
| q(sK30)
| p(sK31)
| q(sK31) ) )
| ~ sP8 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29,sK30,sK31]),skolemize(X3,sK29),skolemize(X4,sK30),skolemize(X5,sK31)],[f53]) ).
fof(f55,plain,
( ( ( ( ? [X43] : ~ p(X43)
& ~ c )
| ? [X42] :
( ~ p(X42)
& ~ c ) )
& ( ! [X43] : p(X43)
| c
| ! [X42] :
( p(X42)
| c ) ) )
| ~ sP7 ),
inference(nnf_transformation,[],[f13]) ).
fof(f56,plain,
( ( ( ( ? [X43] : ~ p(X43)
& ~ c )
| ? [X42] :
( ~ p(X42)
& ~ c ) )
& ( ! [X43] : p(X43)
| c
| ! [X42] :
( p(X42)
| c ) ) )
| ~ sP7 ),
inference(flattening,[],[f55]) ).
fof(f57,plain,
( ( ( ( ? [X0] : ~ p(X0)
& ~ c )
| ? [X1] :
( ~ p(X1)
& ~ c ) )
& ( ! [X2] : p(X2)
| c
| ! [X3] :
( p(X3)
| c ) ) )
| ~ sP7 ),
inference(rectify,[],[f56]) ).
fof(f58,plain,
( ( ( ( ~ p(sK32)
& ~ c )
| ( ~ p(sK33)
& ~ c ) )
& ( ! [X2] : p(X2)
| c
| ! [X3] :
( p(X3)
| c ) ) )
| ~ sP7 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32,sK33]),skolemize(X0,sK32),skolemize(X1,sK33)],[f57]) ).
fof(f59,plain,
( ( ( ! [X45] : ~ p(X45)
| ~ c
| ! [X44] :
( ~ p(X44)
| ~ c ) )
& ( ( ? [X45] : p(X45)
& c )
| ? [X44] :
( p(X44)
& c ) ) )
| ~ sP6 ),
inference(nnf_transformation,[],[f12]) ).
fof(f60,plain,
( ( ( ! [X45] : ~ p(X45)
| ~ c
| ! [X44] :
( ~ p(X44)
| ~ c ) )
& ( ( ? [X45] : p(X45)
& c )
| ? [X44] :
( p(X44)
& c ) ) )
| ~ sP6 ),
inference(flattening,[],[f59]) ).
fof(f61,plain,
( ( ( ! [X0] : ~ p(X0)
| ~ c
| ! [X1] :
( ~ p(X1)
| ~ c ) )
& ( ( ? [X2] : p(X2)
& c )
| ? [X3] :
( p(X3)
& c ) ) )
| ~ sP6 ),
inference(rectify,[],[f60]) ).
fof(f62,plain,
( ( ( ! [X0] : ~ p(X0)
| ~ c
| ! [X1] :
( ~ p(X1)
| ~ c ) )
& ( ( p(sK34)
& c )
| ( p(sK35)
& c ) ) )
| ~ sP6 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34,sK35]),skolemize(X2,sK34),skolemize(X3,sK35)],[f61]) ).
fof(f63,plain,
( ( ( ( ! [X49] : ~ p(X49)
& c )
| ! [X48] :
( ~ p(X48)
& c ) )
& ( ? [X49] : p(X49)
| ~ c
| ? [X48] :
( p(X48)
| ~ c ) ) )
| ~ sP5 ),
inference(nnf_transformation,[],[f11]) ).
fof(f64,plain,
( ( ( ( ! [X49] : ~ p(X49)
& c )
| ! [X48] :
( ~ p(X48)
& c ) )
& ( ? [X49] : p(X49)
| ~ c
| ? [X48] :
( p(X48)
| ~ c ) ) )
| ~ sP5 ),
inference(flattening,[],[f63]) ).
fof(f65,plain,
( ( ( ( ! [X0] : ~ p(X0)
& c )
| ! [X1] :
( ~ p(X1)
& c ) )
& ( ? [X2] : p(X2)
| ~ c
| ? [X3] :
( p(X3)
| ~ c ) ) )
| ~ sP5 ),
inference(rectify,[],[f64]) ).
fof(f66,plain,
( ( ( ( ! [X0] : ~ p(X0)
& c )
| ! [X1] :
( ~ p(X1)
& c ) )
& ( p(sK36)
| ~ c
| p(sK37)
| ~ c ) )
| ~ sP5 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36,sK37]),skolemize(X2,sK36),skolemize(X3,sK37)],[f65]) ).
fof(f67,plain,
( ( ( ( ~ c
& ! [X51] : p(X51) )
| ! [X50] :
( ~ c
& p(X50) ) )
& ( c
| ? [X51] : ~ p(X51)
| ? [X50] :
( c
| ~ p(X50) ) ) )
| ~ sP4 ),
inference(nnf_transformation,[],[f10]) ).
fof(f68,plain,
( ( ( ( ~ c
& ! [X51] : p(X51) )
| ! [X50] :
( ~ c
& p(X50) ) )
& ( c
| ? [X51] : ~ p(X51)
| ? [X50] :
( c
| ~ p(X50) ) ) )
| ~ sP4 ),
inference(flattening,[],[f67]) ).
fof(f69,plain,
( ( ( ( ~ c
& ! [X0] : p(X0) )
| ! [X1] :
( ~ c
& p(X1) ) )
& ( c
| ? [X2] : ~ p(X2)
| ? [X3] :
( c
| ~ p(X3) ) ) )
| ~ sP4 ),
inference(rectify,[],[f68]) ).
fof(f70,plain,
( ( ( ( ~ c
& ! [X0] : p(X0) )
| ! [X1] :
( ~ c
& p(X1) ) )
& ( c
| ~ p(sK38)
| c
| ~ p(sK39) ) )
| ~ sP4 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38,sK39]),skolemize(X2,sK38),skolemize(X3,sK39)],[f69]) ).
fof(f71,plain,
( ( ( ( ? [X53] : ~ p(X53)
& c )
| ? [X52] :
( ~ p(X52)
& c ) )
& ( ! [X53] : p(X53)
| ~ c
| ! [X52] :
( p(X52)
| ~ c ) ) )
| ~ sP3 ),
inference(nnf_transformation,[],[f9]) ).
fof(f72,plain,
( ( ( ( ? [X53] : ~ p(X53)
& c )
| ? [X52] :
( ~ p(X52)
& c ) )
& ( ! [X53] : p(X53)
| ~ c
| ! [X52] :
( p(X52)
| ~ c ) ) )
| ~ sP3 ),
inference(flattening,[],[f71]) ).
fof(f73,plain,
( ( ( ( ? [X0] : ~ p(X0)
& c )
| ? [X1] :
( ~ p(X1)
& c ) )
& ( ! [X2] : p(X2)
| ~ c
| ! [X3] :
( p(X3)
| ~ c ) ) )
| ~ sP3 ),
inference(rectify,[],[f72]) ).
fof(f74,plain,
( ( ( ( ~ p(sK40)
& c )
| ( ~ p(sK41)
& c ) )
& ( ! [X2] : p(X2)
| ~ c
| ! [X3] :
( p(X3)
| ~ c ) ) )
| ~ sP3 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40,sK41]),skolemize(X0,sK40),skolemize(X1,sK41)],[f73]) ).
fof(f75,plain,
( ( ( ( ~ c
& ? [X55] : p(X55) )
| ? [X54] :
( ~ c
& p(X54) ) )
& ( c
| ! [X55] : ~ p(X55)
| ! [X54] :
( c
| ~ p(X54) ) ) )
| ~ sP2 ),
inference(nnf_transformation,[],[f8]) ).
fof(f76,plain,
( ( ( ( ~ c
& ? [X55] : p(X55) )
| ? [X54] :
( ~ c
& p(X54) ) )
& ( c
| ! [X55] : ~ p(X55)
| ! [X54] :
( c
| ~ p(X54) ) ) )
| ~ sP2 ),
inference(flattening,[],[f75]) ).
fof(f77,plain,
( ( ( ( ~ c
& ? [X0] : p(X0) )
| ? [X1] :
( ~ c
& p(X1) ) )
& ( c
| ! [X2] : ~ p(X2)
| ! [X3] :
( c
| ~ p(X3) ) ) )
| ~ sP2 ),
inference(rectify,[],[f76]) ).
fof(f78,plain,
( ( ( ( ~ c
& p(sK42) )
| ( ~ c
& p(sK43) ) )
& ( c
| ! [X2] : ~ p(X2)
| ! [X3] :
( c
| ~ p(X3) ) ) )
| ~ sP2 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42,sK43]),skolemize(X0,sK42),skolemize(X1,sK43)],[f77]) ).
fof(f79,plain,
( ! [X0] :
( ? [X1] :
( f(X1)
& ~ g(X1) )
| ( ~ h(X0)
& f(X0)
& g(X0) ) )
| ~ sP1 ),
inference(nnf_transformation,[],[f7]) ).
fof(f80,plain,
( ! [X0] :
( ( f(sK44)
& ~ g(sK44) )
| ( ~ h(X0)
& f(X0)
& g(X0) ) )
| ~ sP1 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44]),skolemize(X1,sK44)],[f79]) ).
fof(f81,plain,
( ? [X14] :
( f(X14)
& ~ g(X14) )
| ? [X13] :
( ~ h(X13)
& f(X13)
& g(X13) )
| ~ sP0 ),
inference(nnf_transformation,[],[f6]) ).
fof(f82,plain,
( ? [X0] :
( f(X0)
& ~ g(X0) )
| ? [X1] :
( ~ h(X1)
& f(X1)
& g(X1) )
| ~ sP0 ),
inference(rectify,[],[f81]) ).
fof(f83,plain,
( ( f(sK45)
& ~ g(sK45) )
| ( ~ h(sK46)
& f(sK46)
& g(sK46) )
| ~ sP0 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK45,sK46]),skolemize(X0,sK45),skolemize(X1,sK46)],[f82]) ).
fof(f84,plain,
( sP12
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| ! [X0] :
( ? [X1] : ~ p(X1)
& p(X0) )
| sP14
| ? [X2] :
( ~ p(X2)
& ! [X3] : p(X3) )
| ( ! [X4] : ~ p(X4)
& ! [X5] : p(X5) )
| sP13
| sP7
| sP6
| sP18
| sP17
| sP5
| sP4
| sP3
| sP2 ),
inference(rectify,[],[f25]) ).
fof(f85,plain,
( sP12
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| ! [X0] :
( ~ p(sK47)
& p(X0) )
| sP14
| ( ~ p(sK48)
& ! [X3] : p(X3) )
| ( ! [X4] : ~ p(X4)
& ! [X5] : p(X5) )
| sP13
| sP7
| sP6
| sP18
| sP17
| sP5
| sP4
| sP3
| sP2 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47,sK48]),skolemize(X1,sK47),skolemize(X2,sK48)],[f84]) ).
fof(f86,plain,
( c
| c
| ~ sP18 ),
inference(cnf_transformation,[],[f26]) ).
fof(f87,plain,
( ~ c
| ~ c
| ~ sP18 ),
inference(cnf_transformation,[],[f26]) ).
fof(f88,plain,
( c
| c
| ~ sP17 ),
inference(cnf_transformation,[],[f27]) ).
fof(f89,plain,
( ~ c
| ~ c
| ~ sP17 ),
inference(cnf_transformation,[],[f27]) ).
fof(f90,plain,
! [X0] :
( q(X0)
| ~ p(sK19(X0))
| ~ sP16 ),
inference(cnf_transformation,[],[f30]) ).
fof(f91,plain,
! [X0] :
( p(X0)
| ~ sP16 ),
inference(cnf_transformation,[],[f30]) ).
fof(f92,plain,
! [X0] :
( ~ q(X0)
| ~ sP16 ),
inference(cnf_transformation,[],[f30]) ).
fof(f93,plain,
! [X2,X1] :
( q(X2)
| p(X1)
| ~ sP15 ),
inference(cnf_transformation,[],[f33]) ).
fof(f94,plain,
( ~ q(sK20)
| ~ sP15 ),
inference(cnf_transformation,[],[f33]) ).
fof(f95,plain,
( ~ p(sK20)
| ~ sP15 ),
inference(cnf_transformation,[],[f33]) ).
fof(f96,plain,
( q(sK21)
| ~ sP14 ),
inference(cnf_transformation,[],[f36]) ).
fof(f97,plain,
( p(sK21)
| ~ sP14 ),
inference(cnf_transformation,[],[f36]) ).
fof(f98,plain,
! [X0,X1] :
( ~ q(X1)
| ~ p(X0)
| ~ sP14 ),
inference(cnf_transformation,[],[f36]) ).
fof(f99,plain,
! [X2] :
( ~ p(X2)
| ~ sP13 ),
inference(cnf_transformation,[],[f39]) ).
fof(f100,plain,
( p(sK23)
| ~ sP13 ),
inference(cnf_transformation,[],[f39]) ).
fof(f102,plain,
! [X2,X3] :
( h(X3)
| ~ f(X2)
| g(X2)
| ~ f(X3)
| ~ sP12 ),
inference(cnf_transformation,[],[f41]) ).
fof(f103,plain,
( sP1
| ~ sP12 ),
inference(cnf_transformation,[],[f41]) ).
fof(f104,plain,
! [X1] :
( g(X1)
| ~ f(X1)
| ~ h(X1)
| ~ sP12 ),
inference(cnf_transformation,[],[f41]) ).
fof(f105,plain,
! [X0] :
( h(X0)
| ~ g(X0)
| ~ f(X0)
| ~ sP12 ),
inference(cnf_transformation,[],[f41]) ).
fof(f106,plain,
! [X6,X4,X5] :
( r(X4,X6)
| ~ r(X4,X5)
| ~ r(X5,X6)
| ~ sP11 ),
inference(cnf_transformation,[],[f44]) ).
fof(f107,plain,
! [X2,X3] :
( r(X3,X2)
| ~ r(X2,X3)
| ~ sP11 ),
inference(cnf_transformation,[],[f44]) ).
fof(f108,plain,
( r(sK24,sK25)
| ~ sP11 ),
inference(cnf_transformation,[],[f44]) ).
fof(f109,plain,
( ~ r(sK24,sK24)
| ~ sP11 ),
inference(cnf_transformation,[],[f44]) ).
fof(f110,plain,
! [X2,X3] :
( h(X3)
| ~ f(X2)
| g(X2)
| ~ f(X3)
| ~ sP10 ),
inference(cnf_transformation,[],[f46]) ).
fof(f111,plain,
( sP0
| ~ sP10 ),
inference(cnf_transformation,[],[f46]) ).
fof(f112,plain,
! [X1] :
( g(X1)
| ~ f(X1)
| ~ h(X1)
| ~ sP10 ),
inference(cnf_transformation,[],[f46]) ).
fof(f113,plain,
! [X0] :
( h(X0)
| ~ g(X0)
| ~ f(X0)
| ~ sP10 ),
inference(cnf_transformation,[],[f46]) ).
fof(f114,plain,
! [X4,X5] :
( q(X5)
| q(X4)
| ~ sP9 ),
inference(cnf_transformation,[],[f50]) ).
fof(f115,plain,
! [X4,X5] :
( q(X4)
| p(X5)
| ~ sP9 ),
inference(cnf_transformation,[],[f50]) ).
fof(f117,plain,
! [X3,X5] :
( p(X5)
| p(X3)
| ~ sP9 ),
inference(cnf_transformation,[],[f50]) ).
fof(f118,plain,
( ~ q(sK28)
| ~ q(sK27)
| ~ p(sK28)
| ~ p(sK26)
| ~ sP9 ),
inference(cnf_transformation,[],[f50]) ).
fof(f119,plain,
( p(sK29)
| q(sK30)
| p(sK31)
| q(sK31)
| ~ sP8 ),
inference(cnf_transformation,[],[f54]) ).
fof(f120,plain,
! [X2,X1] :
( ~ q(X2)
| ~ q(X1)
| ~ sP8 ),
inference(cnf_transformation,[],[f54]) ).
fof(f123,plain,
! [X2,X0] :
( ~ p(X2)
| ~ p(X0)
| ~ sP8 ),
inference(cnf_transformation,[],[f54]) ).
fof(f124,plain,
! [X2,X3] :
( p(X2)
| c
| p(X3)
| c
| ~ sP7 ),
inference(cnf_transformation,[],[f58]) ).
fof(f125,plain,
( ~ c
| ~ c
| ~ sP7 ),
inference(cnf_transformation,[],[f58]) ).
fof(f128,plain,
( ~ p(sK33)
| ~ p(sK32)
| ~ sP7 ),
inference(cnf_transformation,[],[f58]) ).
fof(f129,plain,
( c
| c
| ~ sP6 ),
inference(cnf_transformation,[],[f62]) ).
fof(f132,plain,
( p(sK35)
| p(sK34)
| ~ sP6 ),
inference(cnf_transformation,[],[f62]) ).
fof(f133,plain,
! [X0,X1] :
( ~ p(X0)
| ~ c
| ~ p(X1)
| ~ c
| ~ sP6 ),
inference(cnf_transformation,[],[f62]) ).
fof(f134,plain,
( p(sK36)
| ~ c
| p(sK37)
| ~ c
| ~ sP5 ),
inference(cnf_transformation,[],[f66]) ).
fof(f135,plain,
( c
| c
| ~ sP5 ),
inference(cnf_transformation,[],[f66]) ).
fof(f138,plain,
! [X0,X1] :
( ~ p(X1)
| ~ p(X0)
| ~ sP5 ),
inference(cnf_transformation,[],[f66]) ).
fof(f139,plain,
( c
| ~ p(sK38)
| c
| ~ p(sK39)
| ~ sP4 ),
inference(cnf_transformation,[],[f70]) ).
fof(f140,plain,
! [X0,X1] :
( p(X1)
| p(X0)
| ~ sP4 ),
inference(cnf_transformation,[],[f70]) ).
fof(f143,plain,
( ~ c
| ~ c
| ~ sP4 ),
inference(cnf_transformation,[],[f70]) ).
fof(f144,plain,
! [X2,X3] :
( p(X2)
| ~ c
| p(X3)
| ~ c
| ~ sP3 ),
inference(cnf_transformation,[],[f74]) ).
fof(f145,plain,
( c
| c
| ~ sP3 ),
inference(cnf_transformation,[],[f74]) ).
fof(f148,plain,
( ~ p(sK41)
| ~ p(sK40)
| ~ sP3 ),
inference(cnf_transformation,[],[f74]) ).
fof(f149,plain,
! [X2,X3] :
( c
| ~ p(X2)
| c
| ~ p(X3)
| ~ sP2 ),
inference(cnf_transformation,[],[f78]) ).
fof(f150,plain,
( p(sK43)
| p(sK42)
| ~ sP2 ),
inference(cnf_transformation,[],[f78]) ).
fof(f153,plain,
( ~ c
| ~ c
| ~ sP2 ),
inference(cnf_transformation,[],[f78]) ).
fof(f154,plain,
! [X0] :
( g(X0)
| ~ g(sK44)
| ~ sP1 ),
inference(cnf_transformation,[],[f80]) ).
fof(f156,plain,
! [X0] :
( ~ h(X0)
| ~ g(sK44)
| ~ sP1 ),
inference(cnf_transformation,[],[f80]) ).
fof(f157,plain,
! [X0] :
( g(X0)
| f(sK44)
| ~ sP1 ),
inference(cnf_transformation,[],[f80]) ).
fof(f158,plain,
! [X0] :
( f(sK44)
| f(X0)
| ~ sP1 ),
inference(cnf_transformation,[],[f80]) ).
fof(f160,plain,
( g(sK46)
| ~ g(sK45)
| ~ sP0 ),
inference(cnf_transformation,[],[f83]) ).
fof(f161,plain,
( f(sK46)
| ~ g(sK45)
| ~ sP0 ),
inference(cnf_transformation,[],[f83]) ).
fof(f162,plain,
( ~ h(sK46)
| ~ g(sK45)
| ~ sP0 ),
inference(cnf_transformation,[],[f83]) ).
fof(f163,plain,
( g(sK46)
| f(sK45)
| ~ sP0 ),
inference(cnf_transformation,[],[f83]) ).
fof(f164,plain,
( f(sK46)
| f(sK45)
| ~ sP0 ),
inference(cnf_transformation,[],[f83]) ).
fof(f165,plain,
( f(sK45)
| ~ h(sK46)
| ~ sP0 ),
inference(cnf_transformation,[],[f83]) ).
fof(f166,plain,
! [X3,X0,X5] :
( sP12
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| p(X0)
| sP14
| p(X3)
| p(X5)
| sP13
| sP7
| sP6
| sP18
| sP17
| sP5
| sP4
| sP3
| sP2 ),
inference(cnf_transformation,[],[f85]) ).
fof(f167,plain,
! [X3,X0,X4] :
( sP12
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| p(X0)
| sP14
| p(X3)
| ~ p(X4)
| sP13
| sP7
| sP6
| sP18
| sP17
| sP5
| sP4
| sP3
| sP2 ),
inference(cnf_transformation,[],[f85]) ).
fof(f169,plain,
! [X0,X4] :
( sP12
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| p(X0)
| sP14
| ~ p(sK48)
| ~ p(X4)
| sP13
| sP7
| sP6
| sP18
| sP17
| sP5
| sP4
| sP3
| sP2 ),
inference(cnf_transformation,[],[f85]) ).
fof(f173,plain,
! [X4] :
( sP12
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| ~ p(sK47)
| sP14
| ~ p(sK48)
| ~ p(X4)
| sP13
| sP7
| sP6
| sP18
| sP17
| sP5
| sP4
| sP3
| sP2 ),
inference(cnf_transformation,[],[f85]) ).
fof(f174,plain,
! [X2,X3] :
( c
| ~ p(X2)
| ~ p(X3)
| ~ sP2 ),
inference(duplicate_literal_removal,[],[f149]) ).
fof(f175,plain,
( ~ sP2
| ~ c ),
inference(duplicate_literal_removal,[],[f153]) ).
fof(f176,plain,
! [X2,X3] :
( p(X2)
| ~ c
| p(X3)
| ~ sP3 ),
inference(duplicate_literal_removal,[],[f144]) ).
fof(f177,plain,
( c
| ~ sP3 ),
inference(duplicate_literal_removal,[],[f145]) ).
fof(f178,plain,
( c
| ~ p(sK38)
| ~ p(sK39)
| ~ sP4 ),
inference(duplicate_literal_removal,[],[f139]) ).
fof(f179,plain,
( ~ sP4
| ~ c ),
inference(duplicate_literal_removal,[],[f143]) ).
fof(f180,plain,
( p(sK36)
| ~ c
| p(sK37)
| ~ sP5 ),
inference(duplicate_literal_removal,[],[f134]) ).
fof(f181,plain,
( c
| ~ sP5 ),
inference(duplicate_literal_removal,[],[f135]) ).
fof(f182,plain,
( c
| ~ sP6 ),
inference(duplicate_literal_removal,[],[f129]) ).
fof(f183,plain,
! [X0,X1] :
( ~ p(X0)
| ~ c
| ~ p(X1)
| ~ sP6 ),
inference(duplicate_literal_removal,[],[f133]) ).
fof(f184,plain,
! [X2,X3] :
( p(X2)
| c
| p(X3)
| ~ sP7 ),
inference(duplicate_literal_removal,[],[f124]) ).
fof(f185,plain,
( ~ sP7
| ~ c ),
inference(duplicate_literal_removal,[],[f125]) ).
fof(f186,plain,
( c
| ~ sP17 ),
inference(duplicate_literal_removal,[],[f88]) ).
fof(f187,plain,
( ~ c
| ~ sP17 ),
inference(duplicate_literal_removal,[],[f89]) ).
fof(f188,plain,
( c
| ~ sP18 ),
inference(duplicate_literal_removal,[],[f86]) ).
fof(f189,plain,
( ~ c
| ~ sP18 ),
inference(duplicate_literal_removal,[],[f87]) ).
fof(f190,plain,
~ sP17,
inference(forward_subsumption_resolution,[],[f187,f186]) ).
fof(f191,plain,
~ sP18,
inference(forward_subsumption_resolution,[],[f189,f188]) ).
fof(f192,plain,
! [X3,X0,X5] :
( sP12
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| p(X0)
| sP14
| p(X3)
| p(X5)
| sP13
| sP7
| sP6
| sP17
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f166,f191]) ).
fof(f193,plain,
! [X3,X0,X5] :
( p(X5)
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| p(X0)
| sP14
| p(X3)
| sP12
| sP13
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f192,f190]) ).
fof(f194,plain,
! [X3,X0] :
( sP12
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| p(X0)
| sP14
| p(X3)
| sP13
| sP7
| sP6
| sP18
| sP17
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f167,f193]) ).
fof(f195,plain,
! [X3,X0] :
( sP12
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| p(X0)
| sP14
| p(X3)
| sP13
| sP7
| sP6
| sP17
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f194,f191]) ).
fof(f196,plain,
! [X3,X0] :
( p(X3)
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| p(X0)
| sP14
| sP12
| sP13
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f195,f190]) ).
fof(f198,plain,
! [X0] :
( sP12
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| p(X0)
| sP14
| ~ p(sK48)
| sP13
| sP7
| sP6
| sP18
| sP17
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f169,f196]) ).
fof(f199,plain,
! [X0] :
( sP12
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| p(X0)
| sP14
| sP13
| sP7
| sP6
| sP18
| sP17
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f198,f196]) ).
fof(f200,plain,
! [X0] :
( sP12
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| p(X0)
| sP14
| sP13
| sP7
| sP6
| sP17
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f199,f191]) ).
fof(f201,plain,
! [X0] :
( p(X0)
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| sP12
| sP14
| sP13
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f200,f190]) ).
fof(f202,plain,
! [X4] :
( sP12
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| sP14
| ~ p(sK48)
| ~ p(X4)
| sP13
| sP7
| sP6
| sP18
| sP17
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f173,f201]) ).
fof(f203,plain,
! [X4] :
( sP12
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| sP14
| ~ p(X4)
| sP13
| sP7
| sP6
| sP18
| sP17
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f202,f201]) ).
fof(f204,plain,
! [X4] :
( sP12
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| sP14
| ~ p(X4)
| sP13
| sP7
| sP6
| sP17
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f203,f191]) ).
fof(f205,plain,
! [X4] :
( sP12
| sP11
| sP10
| sP16
| sP9
| sP15
| sP8
| sP14
| ~ p(X4)
| sP13
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f204,f190]) ).
fof(f206,plain,
( sP16
| sP11
| sP10
| sP12
| sP9
| sP15
| sP8
| sP14
| sP13
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f205,f201]) ).
fof(f220,plain,
~ sP13,
inference(forward_subsumption_resolution,[],[f100,f99]) ).
fof(f222,plain,
! [X0] :
( p(X0)
| ~ sP15
| ~ sP15 ),
inference(resolution,[],[f93,f94]) ).
fof(f223,plain,
! [X0] :
( p(X0)
| ~ sP15 ),
inference(duplicate_literal_removal,[],[f222]) ).
fof(f224,plain,
( ~ sP15
| ~ sP15 ),
inference(resolution,[],[f223,f95]) ).
fof(f226,plain,
~ sP15,
inference(duplicate_literal_removal,[],[f224]) ).
fof(f227,plain,
! [X0] :
( ~ p(X0)
| ~ sP14
| ~ sP14 ),
inference(resolution,[],[f98,f96]) ).
fof(f229,plain,
! [X0] :
( ~ p(X0)
| ~ sP14 ),
inference(duplicate_literal_removal,[],[f227]) ).
fof(f241,plain,
( ~ sP14
| ~ sP14 ),
inference(resolution,[],[f229,f97]) ).
fof(f242,plain,
~ sP14,
inference(duplicate_literal_removal,[],[f241]) ).
fof(f253,plain,
! [X0] :
( ~ q(X0)
| ~ sP8 ),
inference(factoring,[],[f120]) ).
fof(f268,plain,
! [X0] :
( ~ p(X0)
| ~ sP8 ),
inference(factoring,[],[f123]) ).
fof(f309,plain,
! [X0] :
( ~ p(X0)
| ~ sP5 ),
inference(factoring,[],[f138]) ).
fof(f395,plain,
! [X0] :
( ~ p(sK19(X0))
| ~ sP16 ),
inference(forward_subsumption_resolution,[],[f90,f92]) ).
fof(f396,plain,
~ sP16,
inference(forward_subsumption_resolution,[],[f395,f91]) ).
fof(f397,plain,
( sP11
| sP10
| sP12
| sP9
| sP15
| sP8
| sP14
| sP13
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(resolution,[],[f396,f206]) ).
fof(f398,plain,
( sP11
| sP10
| sP12
| sP9
| sP8
| sP14
| sP13
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f397,f226]) ).
fof(f399,plain,
( sP11
| sP10
| sP12
| sP9
| sP8
| sP13
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f398,f242]) ).
fof(f400,plain,
( sP12
| sP10
| sP11
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f399,f220]) ).
fof(f401,plain,
! [X2,X3] :
( ~ p(X3)
| ~ p(X2)
| ~ sP2 ),
inference(forward_subsumption_resolution,[],[f174,f175]) ).
fof(f416,plain,
! [X0] :
( ~ p(X0)
| ~ sP2 ),
inference(factoring,[],[f401]) ).
fof(f422,plain,
! [X2,X3] :
( p(X3)
| p(X2)
| ~ sP3 ),
inference(forward_subsumption_resolution,[],[f176,f177]) ).
fof(f436,plain,
( ~ sP2
| p(sK42)
| ~ sP2 ),
inference(resolution,[],[f416,f150]) ).
fof(f437,plain,
( ~ sP2
| p(sK42) ),
inference(duplicate_literal_removal,[],[f436]) ).
fof(f438,plain,
~ sP2,
inference(forward_subsumption_resolution,[],[f437,f416]) ).
fof(f452,plain,
! [X0] :
( p(X0)
| ~ sP3
| ~ p(sK40)
| ~ sP3 ),
inference(resolution,[],[f422,f148]) ).
fof(f453,plain,
! [X0] :
( p(X0)
| ~ sP3
| ~ p(sK40) ),
inference(duplicate_literal_removal,[],[f452]) ).
fof(f454,plain,
! [X0] :
( p(X0)
| ~ sP3 ),
inference(forward_subsumption_resolution,[],[f453,f422]) ).
fof(f465,plain,
( ~ p(sK39)
| ~ p(sK38)
| ~ sP4 ),
inference(forward_subsumption_resolution,[],[f178,f179]) ).
fof(f468,plain,
! [X0] :
( ~ p(sK38)
| ~ sP4
| p(X0)
| ~ sP4 ),
inference(resolution,[],[f465,f140]) ).
fof(f480,plain,
! [X0] :
( ~ p(sK38)
| ~ sP4
| p(X0) ),
inference(duplicate_literal_removal,[],[f468]) ).
fof(f481,plain,
! [X0] :
( p(X0)
| ~ sP4 ),
inference(forward_subsumption_resolution,[],[f480,f140]) ).
fof(f483,plain,
( ~ c
| p(sK37)
| ~ sP5 ),
inference(forward_subsumption_resolution,[],[f180,f309]) ).
fof(f484,plain,
( p(sK37)
| ~ sP5 ),
inference(forward_subsumption_resolution,[],[f483,f181]) ).
fof(f485,plain,
~ sP5,
inference(forward_subsumption_resolution,[],[f484,f309]) ).
fof(f486,plain,
! [X0,X1] :
( ~ p(X1)
| ~ p(X0)
| ~ sP6 ),
inference(forward_subsumption_resolution,[],[f183,f182]) ).
fof(f502,plain,
! [X0] :
( ~ p(X0)
| ~ sP6 ),
inference(factoring,[],[f486]) ).
fof(f508,plain,
! [X2,X3] :
( p(X3)
| p(X2)
| ~ sP7 ),
inference(forward_subsumption_resolution,[],[f184,f185]) ).
fof(f519,plain,
! [X0] :
( p(X0)
| ~ sP7
| ~ p(sK32)
| ~ sP7 ),
inference(resolution,[],[f508,f128]) ).
fof(f522,plain,
! [X0] :
( p(X0)
| ~ sP7
| ~ p(sK32) ),
inference(duplicate_literal_removal,[],[f519]) ).
fof(f524,plain,
! [X0] :
( p(X0)
| ~ sP7 ),
inference(forward_subsumption_resolution,[],[f522,f508]) ).
fof(f529,plain,
! [X0] :
( ~ g(X0)
| ~ f(X0)
| ~ sP12
| ~ g(sK44)
| ~ sP1 ),
inference(resolution,[],[f105,f156]) ).
fof(f530,plain,
( ~ g(sK46)
| ~ f(sK46)
| ~ sP12
| ~ g(sK45)
| ~ sP0 ),
inference(resolution,[],[f105,f162]) ).
fof(f531,plain,
( ~ f(sK46)
| ~ sP12
| ~ g(sK45)
| ~ sP0 ),
inference(forward_subsumption_resolution,[],[f530,f160]) ).
fof(f532,plain,
! [X0] :
( ~ f(X0)
| ~ sP12
| ~ g(sK44)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f529,f154]) ).
fof(f533,plain,
( ~ g(sK45)
| ~ sP12
| ~ sP0 ),
inference(forward_subsumption_resolution,[],[f531,f161]) ).
fof(f534,plain,
! [X0] :
( ~ g(sK44)
| ~ sP12
| ~ f(X0) ),
inference(forward_subsumption_resolution,[],[f532,f103]) ).
fof(f547,plain,
( ~ sP3
| ~ p(sK40)
| ~ sP3 ),
inference(resolution,[],[f454,f148]) ).
fof(f548,plain,
( ~ sP3
| ~ p(sK40) ),
inference(duplicate_literal_removal,[],[f547]) ).
fof(f549,plain,
~ sP3,
inference(forward_subsumption_resolution,[],[f548,f454]) ).
fof(f555,plain,
( ~ g(sK46)
| ~ f(sK46)
| ~ sP10
| ~ g(sK45)
| ~ sP0 ),
inference(resolution,[],[f113,f162]) ).
fof(f556,plain,
( ~ f(sK46)
| ~ sP10
| ~ g(sK45)
| ~ sP0 ),
inference(forward_subsumption_resolution,[],[f555,f160]) ).
fof(f558,plain,
( ~ sP10
| ~ g(sK45)
| ~ sP0 ),
inference(forward_subsumption_resolution,[],[f556,f161]) ).
fof(f560,plain,
( ~ g(sK45)
| ~ sP10 ),
inference(forward_subsumption_resolution,[],[f558,f111]) ).
fof(f572,plain,
( ~ sP4
| ~ p(sK38)
| ~ sP4 ),
inference(resolution,[],[f481,f465]) ).
fof(f574,plain,
( ~ sP4
| ~ p(sK38) ),
inference(duplicate_literal_removal,[],[f572]) ).
fof(f575,plain,
~ sP4,
inference(forward_subsumption_resolution,[],[f574,f481]) ).
fof(f600,plain,
( ~ sP6
| p(sK34)
| ~ sP6 ),
inference(resolution,[],[f502,f132]) ).
fof(f602,plain,
( ~ sP6
| p(sK34) ),
inference(duplicate_literal_removal,[],[f600]) ).
fof(f603,plain,
~ sP6,
inference(forward_subsumption_resolution,[],[f602,f502]) ).
fof(f606,plain,
! [X0] :
( ~ q(sK27)
| ~ p(sK28)
| ~ p(sK26)
| ~ sP9
| p(X0)
| ~ sP9 ),
inference(resolution,[],[f118,f115]) ).
fof(f607,plain,
! [X0] :
( ~ q(sK27)
| ~ p(sK28)
| ~ p(sK26)
| ~ sP9
| q(X0)
| ~ sP9 ),
inference(resolution,[],[f118,f114]) ).
fof(f609,plain,
! [X0] :
( ~ q(sK27)
| ~ p(sK28)
| ~ p(sK26)
| ~ sP9
| q(X0) ),
inference(duplicate_literal_removal,[],[f607]) ).
fof(f610,plain,
! [X0] :
( ~ q(sK27)
| ~ p(sK28)
| ~ p(sK26)
| ~ sP9
| p(X0) ),
inference(duplicate_literal_removal,[],[f606]) ).
fof(f611,plain,
! [X0] :
( ~ p(sK28)
| ~ p(sK26)
| ~ sP9
| q(X0) ),
inference(forward_subsumption_resolution,[],[f609,f114]) ).
fof(f612,plain,
! [X0] :
( ~ q(sK27)
| ~ p(sK28)
| ~ sP9
| p(X0) ),
inference(forward_subsumption_resolution,[],[f610,f117]) ).
fof(f613,plain,
! [X0] :
( ~ p(sK26)
| ~ sP9
| q(X0) ),
inference(forward_subsumption_resolution,[],[f611,f115]) ).
fof(f614,plain,
! [X0] :
( ~ q(sK27)
| ~ sP9
| p(X0) ),
inference(forward_subsumption_resolution,[],[f612,f117]) ).
fof(f615,plain,
! [X0] :
( q(X0)
| ~ sP9 ),
inference(forward_subsumption_resolution,[],[f613,f115]) ).
fof(f616,plain,
! [X0] :
( p(X0)
| ~ sP9 ),
inference(forward_subsumption_resolution,[],[f614,f115]) ).
fof(f617,plain,
( q(sK30)
| p(sK31)
| q(sK31)
| ~ sP8 ),
inference(forward_subsumption_resolution,[],[f119,f268]) ).
fof(f618,plain,
( p(sK31)
| q(sK31)
| ~ sP8 ),
inference(forward_subsumption_resolution,[],[f617,f253]) ).
fof(f619,plain,
( q(sK31)
| ~ sP8 ),
inference(forward_subsumption_resolution,[],[f618,f268]) ).
fof(f620,plain,
~ sP8,
inference(forward_subsumption_resolution,[],[f619,f253]) ).
fof(f621,plain,
! [X0] :
( ~ r(sK24,X0)
| ~ r(X0,sK24)
| ~ sP11
| ~ sP11 ),
inference(resolution,[],[f106,f109]) ).
fof(f622,plain,
! [X0] :
( ~ r(sK24,X0)
| ~ r(X0,sK24)
| ~ sP11 ),
inference(duplicate_literal_removal,[],[f621]) ).
fof(f623,plain,
! [X0] :
( ~ r(X0,sK24)
| ~ sP11 ),
inference(forward_subsumption_resolution,[],[f622,f107]) ).
fof(f635,plain,
( ~ sP7
| ~ p(sK32)
| ~ sP7 ),
inference(resolution,[],[f524,f128]) ).
fof(f638,plain,
( ~ sP7
| ~ p(sK32) ),
inference(duplicate_literal_removal,[],[f635]) ).
fof(f639,plain,
~ sP7,
inference(forward_subsumption_resolution,[],[f638,f524]) ).
fof(f640,plain,
( ~ sP10
| ~ f(sK45)
| ~ h(sK45)
| ~ sP10 ),
inference(resolution,[],[f560,f112]) ).
fof(f644,plain,
( ~ h(sK45)
| ~ f(sK45)
| ~ sP10 ),
inference(duplicate_literal_removal,[],[f640]) ).
fof(f650,plain,
( ~ sP9
| ~ q(sK27)
| ~ p(sK28)
| ~ p(sK26)
| ~ sP9 ),
inference(resolution,[],[f615,f118]) ).
fof(f651,plain,
( ~ sP9
| ~ q(sK27)
| ~ p(sK28)
| ~ p(sK26) ),
inference(duplicate_literal_removal,[],[f650]) ).
fof(f652,plain,
( ~ sP9
| ~ p(sK28)
| ~ p(sK26) ),
inference(forward_subsumption_resolution,[],[f651,f615]) ).
fof(f670,plain,
( ~ sP12
| ~ sP0
| ~ g(sK44)
| ~ sP1 ),
inference(resolution,[],[f533,f154]) ).
fof(f672,plain,
( ~ g(sK44)
| ~ sP0
| ~ sP12 ),
inference(forward_subsumption_resolution,[],[f670,f103]) ).
fof(f686,plain,
! [X0] :
( ~ sP11
| ~ r(sK24,X0)
| ~ sP11 ),
inference(resolution,[],[f623,f107]) ).
fof(f687,plain,
! [X0] :
( ~ r(sK24,X0)
| ~ sP11 ),
inference(duplicate_literal_removal,[],[f686]) ).
fof(f690,plain,
! [X0] :
( ~ sP12
| ~ f(X0)
| ~ f(sK44)
| ~ h(sK44)
| ~ sP12 ),
inference(resolution,[],[f534,f104]) ).
fof(f691,plain,
! [X0] :
( ~ sP12
| ~ f(X0)
| f(sK44)
| ~ sP1 ),
inference(resolution,[],[f534,f157]) ).
fof(f693,plain,
! [X0] :
( ~ sP12
| ~ f(X0)
| ~ f(sK44)
| ~ h(sK44) ),
inference(duplicate_literal_removal,[],[f690]) ).
fof(f694,plain,
( ~ sP12
| f(sK44)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f691,f158]) ).
fof(f695,plain,
( f(sK44)
| ~ sP12 ),
inference(forward_subsumption_resolution,[],[f694,f103]) ).
fof(f697,plain,
( ~ sP0
| ~ sP12
| ~ f(sK44)
| ~ h(sK44)
| ~ sP12 ),
inference(resolution,[],[f672,f104]) ).
fof(f700,plain,
( ~ sP0
| ~ sP12
| ~ f(sK44)
| ~ h(sK44) ),
inference(duplicate_literal_removal,[],[f697]) ).
fof(f701,plain,
( ~ h(sK44)
| ~ sP12
| ~ sP0 ),
inference(forward_subsumption_resolution,[],[f700,f695]) ).
fof(f723,plain,
( ~ sP11
| ~ sP11 ),
inference(resolution,[],[f687,f108]) ).
fof(f728,plain,
~ sP11,
inference(duplicate_literal_removal,[],[f723]) ).
fof(f729,plain,
! [X0] :
( ~ f(sK45)
| ~ sP10
| ~ f(X0)
| g(X0)
| ~ f(sK45)
| ~ sP10 ),
inference(resolution,[],[f644,f110]) ).
fof(f736,plain,
! [X0] :
( g(X0)
| ~ sP10
| ~ f(X0)
| ~ f(sK45) ),
inference(duplicate_literal_removal,[],[f729]) ).
fof(f738,plain,
! [X0] :
( ~ sP12
| ~ sP0
| ~ f(X0)
| g(X0)
| ~ f(sK44)
| ~ sP12 ),
inference(resolution,[],[f701,f102]) ).
fof(f742,plain,
! [X0] :
( ~ sP12
| ~ sP0
| ~ f(X0)
| g(X0)
| ~ f(sK44) ),
inference(duplicate_literal_removal,[],[f738]) ).
fof(f743,plain,
! [X0] :
( g(X0)
| ~ sP0
| ~ f(X0)
| ~ sP12 ),
inference(forward_subsumption_resolution,[],[f742,f695]) ).
fof(f746,plain,
( ~ sP9
| ~ p(sK26) ),
inference(forward_subsumption_resolution,[],[f652,f616]) ).
fof(f747,plain,
~ sP9,
inference(forward_subsumption_resolution,[],[f746,f616]) ).
fof(f772,plain,
! [X0] :
( ~ h(sK44)
| ~ f(X0)
| ~ sP12 ),
inference(forward_subsumption_resolution,[],[f693,f695]) ).
fof(f775,plain,
! [X0,X1] :
( ~ f(X0)
| ~ sP12
| ~ f(X1)
| g(X1)
| ~ f(sK44)
| ~ sP12 ),
inference(resolution,[],[f772,f102]) ).
fof(f779,plain,
! [X0,X1] :
( ~ f(X0)
| ~ sP12
| ~ f(X1)
| g(X1)
| ~ f(sK44) ),
inference(duplicate_literal_removal,[],[f775]) ).
fof(f780,plain,
! [X0,X1] :
( g(X1)
| ~ sP12
| ~ f(X1)
| ~ f(X0) ),
inference(forward_subsumption_resolution,[],[f779,f695]) ).
fof(f783,plain,
( ~ sP0
| ~ f(sK44)
| ~ sP12
| ~ sP0
| ~ sP12 ),
inference(resolution,[],[f743,f672]) ).
fof(f787,plain,
( ~ sP0
| ~ f(sK44)
| ~ sP12 ),
inference(duplicate_literal_removal,[],[f783]) ).
fof(f790,plain,
( ~ sP12
| ~ sP0 ),
inference(forward_subsumption_resolution,[],[f787,f695]) ).
fof(f791,plain,
( ~ sP0
| sP10
| sP11
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(resolution,[],[f790,f400]) ).
fof(f792,plain,
( ~ sP0
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f791,f728]) ).
fof(f793,plain,
( ~ sP0
| sP10
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f792,f747]) ).
fof(f794,plain,
( ~ sP0
| sP10
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f793,f620]) ).
fof(f795,plain,
( ~ sP0
| sP10
| sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f794,f639]) ).
fof(f796,plain,
( ~ sP0
| sP10
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f795,f603]) ).
fof(f797,plain,
( ~ sP0
| sP10
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f796,f485]) ).
fof(f798,plain,
( ~ sP0
| sP10
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f797,f575]) ).
fof(f799,plain,
( ~ sP0
| sP10
| sP2 ),
inference(forward_subsumption_resolution,[],[f798,f549]) ).
fof(f800,plain,
( sP10
| ~ sP0 ),
inference(forward_subsumption_resolution,[],[f799,f438]) ).
fof(f802,plain,
( ~ sP10
| ~ f(sK45)
| ~ f(sK45)
| ~ sP10 ),
inference(resolution,[],[f736,f560]) ).
fof(f807,plain,
( ~ f(sK45)
| ~ sP10 ),
inference(duplicate_literal_removal,[],[f802]) ).
fof(f813,plain,
! [X0,X1] :
( ~ sP12
| ~ f(sK44)
| ~ f(X0)
| ~ sP12
| ~ f(X1) ),
inference(resolution,[],[f780,f534]) ).
fof(f815,plain,
! [X0,X1] :
( ~ sP12
| ~ f(sK44)
| ~ f(X0)
| ~ f(X1) ),
inference(duplicate_literal_removal,[],[f813]) ).
fof(f818,plain,
! [X0,X1] :
( ~ f(X1)
| ~ f(X0)
| ~ sP12 ),
inference(forward_subsumption_resolution,[],[f815,f695]) ).
fof(f820,plain,
( ~ sP10
| ~ h(sK46)
| ~ sP0 ),
inference(resolution,[],[f807,f165]) ).
fof(f822,plain,
( ~ h(sK46)
| ~ sP0 ),
inference(forward_subsumption_resolution,[],[f820,f800]) ).
fof(f825,plain,
( ~ sP0
| ~ g(sK46)
| ~ f(sK46)
| ~ sP10 ),
inference(resolution,[],[f822,f113]) ).
fof(f827,plain,
( ~ g(sK46)
| ~ f(sK46)
| ~ sP10 ),
inference(forward_subsumption_resolution,[],[f825,f111]) ).
fof(f829,plain,
( ~ f(sK46)
| ~ sP10
| f(sK45)
| ~ sP0 ),
inference(resolution,[],[f827,f163]) ).
fof(f845,plain,
( ~ f(sK46)
| ~ sP10
| ~ sP0 ),
inference(forward_subsumption_resolution,[],[f829,f807]) ).
fof(f846,plain,
( ~ f(sK46)
| ~ sP0 ),
inference(forward_subsumption_resolution,[],[f845,f800]) ).
fof(f847,plain,
( ~ sP0
| f(sK45)
| ~ sP0 ),
inference(resolution,[],[f846,f164]) ).
fof(f851,plain,
( f(sK45)
| ~ sP0 ),
inference(duplicate_literal_removal,[],[f847]) ).
fof(f870,plain,
! [X0] :
( ~ f(X0)
| ~ sP12 ),
inference(factoring,[],[f818]) ).
fof(f875,plain,
( ~ sP0
| ~ sP10 ),
inference(resolution,[],[f851,f807]) ).
fof(f877,plain,
~ sP10,
inference(forward_subsumption_resolution,[],[f875,f111]) ).
fof(f882,plain,
( ~ sP12
| ~ sP12 ),
inference(resolution,[],[f870,f695]) ).
fof(f889,plain,
~ sP12,
inference(duplicate_literal_removal,[],[f882]) ).
fof(f894,plain,
( sP10
| sP11
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(resolution,[],[f889,f400]) ).
fof(f895,plain,
( sP11
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f894,f877]) ).
fof(f896,plain,
( sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f895,f728]) ).
fof(f897,plain,
( sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f896,f747]) ).
fof(f898,plain,
( sP7
| sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f897,f620]) ).
fof(f899,plain,
( sP6
| sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f898,f639]) ).
fof(f900,plain,
( sP5
| sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f899,f603]) ).
fof(f901,plain,
( sP4
| sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f900,f485]) ).
fof(f902,plain,
( sP3
| sP2 ),
inference(forward_subsumption_resolution,[],[f901,f575]) ).
fof(f903,plain,
sP2,
inference(forward_subsumption_resolution,[],[f902,f549]) ).
fof(f904,plain,
$false,
inference(forward_subsumption_resolution,[],[f903,f438]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN917+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n006.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 17:12:25 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.63/0.96 % (4117578)Detected formulas, will run a generic FOF schedule.
% 0.63/0.96 % (4117587)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2959738644:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 0.63/0.96 % (4117587)First to succeed.
% 0.63/0.96 % (4117587)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4117578"
% 0.63/0.96 % (4117586)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2272303219:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 0.63/0.96 % (4117589)dis-21_1_sil=8000:lcm=predicate:random_seed=1356880594:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 0.63/0.96 % (4117583)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=259943528:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 0.63/0.96 % (4117585)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1743909153:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 0.63/0.96 % (4117584)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=420686790:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 0.63/0.96 % (4117588)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2072029695:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 0.63/0.96 % (4117586)Refutation not found, incomplete strategy
% 0.63/0.96 % (4117586)------------------------------
% 0.63/0.96 % (4117586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.63/0.96 % (4117586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.96 % (4117586)CaDiCaL version: 2.1.3
% 0.63/0.96 % (4117586)Termination reason: Refutation not found, incomplete strategy
% 0.63/0.96 % (4117586)Time elapsed: 0.006 s
% 0.63/0.96 % (4117586)Peak memory usage: 88 MB
% 0.63/0.96 % (4117586)Instructions burned: 10 (million)
% 0.63/0.96 % (4117589)Also succeeded, but the first one will report.
% 0.63/0.96 % (4117588)Also succeeded, but the first one will report.
% 0.63/0.96 % (4117587)Refutation found. Thanks to Tanya!
% 0.63/0.96 % SZS status Theorem for theBenchmark
% 0.63/0.96 % SZS output start Proof for theBenchmark
% See solution above
% 2.66/1.06 % (4117587)------------------------------
% 2.66/1.06 % (4117587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.66/1.06 % (4117587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.66/1.06 % (4117587)CaDiCaL version: 2.1.3
% 2.66/1.06 % (4117587)Termination reason: Refutation
% 2.66/1.06 % (4117587)Time elapsed: 0.007 s
% 2.66/1.06 % (4117587)Peak memory usage: 88 MB
% 2.66/1.06 % (4117587)Instructions burned: 21 (million)
% 2.66/1.06 % (4117587)------------------------------
% 2.66/1.06 % (4117587)------------------------------
% 2.66/1.06 % (4117578)Success in time 0.299 s
% 2.66/1.06 % Vampire exiting
%------------------------------------------------------------------------------