%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL658+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p 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 : Fri Sep 25 02:07:42 PM UTC 2026
% Result : Theorem 37.22s 16.35s
% Output : CNFRefutation 37.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 5
% Syntax : Number of formulae : 247 ( 27 unt; 4 def)
% Number of atoms : 2445 ( 0 equ)
% Maximal formula atoms : 151 ( 9 avg)
% Number of connectives : 3911 (1713 ~;1896 |; 302 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 41 ( 8 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 9 con; 0-1 aty)
% Number of variables : 1438 ( 0 sgn1305 !; 133 ?; 349 :)
% Comments :
%------------------------------------------------------------------------------
fof(f2,conjecture,
~ ? [X0] :
~ ( ~ ( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ( ( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
& ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0) )
& ( ~ ! [X1] :
( ~ ! [X0] :
( ~ ( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) ) )
| ! [X1] :
( ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) ) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',main) ).
fof(f3,negated_conjecture,
~ ~ ? [X0] :
~ ( ~ ( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ( ( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
& ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0) )
& ( ~ ! [X1] :
( ~ ! [X0] :
( ~ ( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) ) )
| ! [X1] :
( ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) ) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) ),
inference(negated_conjecture,[status(cth)],[f2]) ).
fof(f4,plain,
~ ~ ? [X0] :
~ ( ~ ( ! [X104] :
( ~ ! [X107] :
( p1(X107)
| ~ r1(X104,X107) )
| ! [X105] :
( ! [X106] :
( p1(X106)
| ~ r1(X105,X106) )
| ~ r1(X104,X105) )
| ~ r1(X0,X104) )
& ! [X99] :
( ! [X100] :
( ~ ! [X103] :
( p1(X103)
| ~ r1(X100,X103) )
| ! [X101] :
( ! [X102] :
( p1(X102)
| ~ r1(X101,X102) )
| ~ r1(X100,X101) )
| ~ r1(X99,X100) )
| ~ r1(X0,X99) )
& ! [X93] :
( ! [X94] :
( ! [X95] :
( ~ ! [X98] :
( p1(X98)
| ~ r1(X95,X98) )
| ! [X96] :
( ! [X97] :
( p1(X97)
| ~ r1(X96,X97) )
| ~ r1(X95,X96) )
| ~ r1(X94,X95) )
| ~ r1(X93,X94) )
| ~ r1(X0,X93) )
& ! [X86] :
( ! [X87] :
( ! [X88] :
( ! [X89] :
( ~ ! [X92] :
( p1(X92)
| ~ r1(X89,X92) )
| ! [X90] :
( ! [X91] :
( p1(X91)
| ~ r1(X90,X91) )
| ~ r1(X89,X90) )
| ~ r1(X88,X89) )
| ~ r1(X87,X88) )
| ~ r1(X86,X87) )
| ~ r1(X0,X86) )
& ! [X78] :
( ! [X79] :
( ! [X80] :
( ! [X81] :
( ! [X82] :
( ~ ! [X85] :
( p1(X85)
| ~ r1(X82,X85) )
| ! [X83] :
( ! [X84] :
( p1(X84)
| ~ r1(X83,X84) )
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
| ~ r1(X80,X81) )
| ~ r1(X79,X80) )
| ~ r1(X78,X79) )
| ~ r1(X0,X78) )
& ~ ! [X66] :
( ! [X67] :
( ! [X68] :
( ! [X69] :
( ! [X70] :
( ! [X71] :
( ~ ! [X75] :
( ~ ! [X76] :
( ~ p1(X76)
| ! [X77] :
( p1(X77)
| ~ r1(X76,X77) )
| ~ r1(X75,X76) )
| p1(X75)
| ~ r1(X71,X75) )
| ! [X73] :
( ~ ! [X74] :
( p1(X74)
| ~ r1(X73,X74) )
| ~ r1(X71,X73) )
| ! [X72] :
( p1(X72)
| ~ r1(X71,X72) )
| ~ r1(X70,X71) )
| ~ r1(X69,X70) )
| ~ r1(X68,X69) )
| ~ r1(X67,X68) )
| ~ r1(X66,X67) )
| ~ r1(X0,X66) ) )
| ~ ! [X34] :
( ! [X35] :
( ! [X36] :
( ! [X37] :
( ! [X38] :
( ! [X39] :
( ( ( ~ ! [X63] :
( ~ ! [X64] :
( ~ p1(X64)
| ! [X65] :
( p1(X65)
| ~ r1(X64,X65) )
| ~ r1(X63,X64) )
| p1(X63)
| ~ r1(X39,X63) )
| ! [X59] :
( ! [X60] :
( ~ ! [X61] :
( ~ p1(X61)
| ! [X62] :
( p1(X62)
| ~ r1(X61,X62) )
| ~ r1(X60,X61) )
| p1(X60)
| ~ r1(X59,X60) )
| ~ r1(X39,X59) ) )
& ! [X55] :
( ~ ! [X58] :
( p1(X58)
| ~ r1(X55,X58) )
| ! [X56] :
( ! [X57] :
( p1(X57)
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X39,X55) )
& ( ~ ! [X52] :
( ~ ! [X53] :
( ~ p1(X53)
| ! [X54] :
( p1(X54)
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
| p1(X52)
| ~ r1(X39,X52) )
| ! [X50] :
( ~ ! [X51] :
( p1(X51)
| ~ r1(X50,X51) )
| ~ r1(X39,X50) )
| p1(X39) )
& ( ~ ! [X44] :
( ~ ! [X46] :
( ~ ( ~ p1(X46)
| ! [X49] :
( p1(X49)
| ~ r1(X46,X49) ) )
| ! [X47] :
( ~ p1(X47)
| ! [X48] :
( p1(X48)
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X44,X46) )
| ~ p1(X44)
| ! [X45] :
( p1(X45)
| ~ r1(X44,X45) )
| ~ r1(X39,X44) )
| ! [X41] :
( ~ ! [X42] :
( ~ p1(X42)
| ! [X43] :
( p1(X43)
| ~ r1(X42,X43) )
| ~ r1(X41,X42) )
| ~ r1(X39,X41) )
| ~ p1(X39)
| ! [X40] :
( p1(X40)
| ~ r1(X39,X40) ) ) )
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(X35,X36) )
| ~ r1(X34,X35) )
| ~ r1(X0,X34) )
| ~ ! [X24] :
( ! [X25] :
( ! [X26] :
( ! [X27] :
( ! [X28] :
( ! [X29] :
( ! [X30] :
( ~ ! [X33] :
( p1(X33)
| ~ r1(X30,X33) )
| ! [X31] :
( ! [X32] :
( p1(X32)
| ~ r1(X31,X32) )
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
| ~ r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X0,X24) )
| ~ ! [X13] :
( ! [X14] :
( ! [X15] :
( ! [X16] :
( ! [X17] :
( ! [X18] :
( ! [X19] :
( ! [X20] :
( ~ ! [X23] :
( p1(X23)
| ~ r1(X20,X23) )
| ! [X21] :
( ! [X22] :
( p1(X22)
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X14,X15) )
| ~ r1(X13,X14) )
| ~ r1(X0,X13) )
| ~ ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ~ ! [X12] :
( p1(X12)
| ~ r1(X9,X12) )
| ! [X10] :
( ! [X11] :
( p1(X11)
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f3]) ).
fof(f5,plain,
? [X0] :
~ ( ~ ( ! [X104] :
( ~ ! [X107] :
( p1(X107)
| ~ r1(X104,X107) )
| ! [X105] :
( ! [X106] :
( p1(X106)
| ~ r1(X105,X106) )
| ~ r1(X104,X105) )
| ~ r1(X0,X104) )
& ! [X99] :
( ! [X100] :
( ~ ! [X103] :
( p1(X103)
| ~ r1(X100,X103) )
| ! [X101] :
( ! [X102] :
( p1(X102)
| ~ r1(X101,X102) )
| ~ r1(X100,X101) )
| ~ r1(X99,X100) )
| ~ r1(X0,X99) )
& ! [X93] :
( ! [X94] :
( ! [X95] :
( ~ ! [X98] :
( p1(X98)
| ~ r1(X95,X98) )
| ! [X96] :
( ! [X97] :
( p1(X97)
| ~ r1(X96,X97) )
| ~ r1(X95,X96) )
| ~ r1(X94,X95) )
| ~ r1(X93,X94) )
| ~ r1(X0,X93) )
& ! [X86] :
( ! [X87] :
( ! [X88] :
( ! [X89] :
( ~ ! [X92] :
( p1(X92)
| ~ r1(X89,X92) )
| ! [X90] :
( ! [X91] :
( p1(X91)
| ~ r1(X90,X91) )
| ~ r1(X89,X90) )
| ~ r1(X88,X89) )
| ~ r1(X87,X88) )
| ~ r1(X86,X87) )
| ~ r1(X0,X86) )
& ! [X78] :
( ! [X79] :
( ! [X80] :
( ! [X81] :
( ! [X82] :
( ~ ! [X85] :
( p1(X85)
| ~ r1(X82,X85) )
| ! [X83] :
( ! [X84] :
( p1(X84)
| ~ r1(X83,X84) )
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
| ~ r1(X80,X81) )
| ~ r1(X79,X80) )
| ~ r1(X78,X79) )
| ~ r1(X0,X78) )
& ~ ! [X66] :
( ! [X67] :
( ! [X68] :
( ! [X69] :
( ! [X70] :
( ! [X71] :
( ~ ! [X75] :
( ~ ! [X76] :
( ~ p1(X76)
| ! [X77] :
( p1(X77)
| ~ r1(X76,X77) )
| ~ r1(X75,X76) )
| p1(X75)
| ~ r1(X71,X75) )
| ! [X73] :
( ~ ! [X74] :
( p1(X74)
| ~ r1(X73,X74) )
| ~ r1(X71,X73) )
| ! [X72] :
( p1(X72)
| ~ r1(X71,X72) )
| ~ r1(X70,X71) )
| ~ r1(X69,X70) )
| ~ r1(X68,X69) )
| ~ r1(X67,X68) )
| ~ r1(X66,X67) )
| ~ r1(X0,X66) ) )
| ~ ! [X34] :
( ! [X35] :
( ! [X36] :
( ! [X37] :
( ! [X38] :
( ! [X39] :
( ( ( ~ ! [X63] :
( ~ ! [X64] :
( ~ p1(X64)
| ! [X65] :
( p1(X65)
| ~ r1(X64,X65) )
| ~ r1(X63,X64) )
| p1(X63)
| ~ r1(X39,X63) )
| ! [X59] :
( ! [X60] :
( ~ ! [X61] :
( ~ p1(X61)
| ! [X62] :
( p1(X62)
| ~ r1(X61,X62) )
| ~ r1(X60,X61) )
| p1(X60)
| ~ r1(X59,X60) )
| ~ r1(X39,X59) ) )
& ! [X55] :
( ~ ! [X58] :
( p1(X58)
| ~ r1(X55,X58) )
| ! [X56] :
( ! [X57] :
( p1(X57)
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X39,X55) )
& ( ~ ! [X52] :
( ~ ! [X53] :
( ~ p1(X53)
| ! [X54] :
( p1(X54)
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
| p1(X52)
| ~ r1(X39,X52) )
| ! [X50] :
( ~ ! [X51] :
( p1(X51)
| ~ r1(X50,X51) )
| ~ r1(X39,X50) )
| p1(X39) )
& ( ~ ! [X44] :
( ~ ! [X46] :
( ~ ( ~ p1(X46)
| ! [X49] :
( p1(X49)
| ~ r1(X46,X49) ) )
| ! [X47] :
( ~ p1(X47)
| ! [X48] :
( p1(X48)
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X44,X46) )
| ~ p1(X44)
| ! [X45] :
( p1(X45)
| ~ r1(X44,X45) )
| ~ r1(X39,X44) )
| ! [X41] :
( ~ ! [X42] :
( ~ p1(X42)
| ! [X43] :
( p1(X43)
| ~ r1(X42,X43) )
| ~ r1(X41,X42) )
| ~ r1(X39,X41) )
| ~ p1(X39)
| ! [X40] :
( p1(X40)
| ~ r1(X39,X40) ) ) )
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(X35,X36) )
| ~ r1(X34,X35) )
| ~ r1(X0,X34) )
| ~ ! [X24] :
( ! [X25] :
( ! [X26] :
( ! [X27] :
( ! [X28] :
( ! [X29] :
( ! [X30] :
( ~ ! [X33] :
( p1(X33)
| ~ r1(X30,X33) )
| ! [X31] :
( ! [X32] :
( p1(X32)
| ~ r1(X31,X32) )
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
| ~ r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X0,X24) )
| ~ ! [X13] :
( ! [X14] :
( ! [X15] :
( ! [X16] :
( ! [X17] :
( ! [X18] :
( ! [X19] :
( ! [X20] :
( ~ ! [X23] :
( p1(X23)
| ~ r1(X20,X23) )
| ! [X21] :
( ! [X22] :
( p1(X22)
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X14,X15) )
| ~ r1(X13,X14) )
| ~ r1(X0,X13) )
| ~ ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ~ ! [X12] :
( p1(X12)
| ~ r1(X9,X12) )
| ! [X10] :
( ! [X11] :
( p1(X11)
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(flattening,[],[f4]) ).
fof(f6,plain,
? [X0] :
( ! [X104] :
( ? [X107] :
( ~ p1(X107)
& r1(X104,X107) )
| ! [X105] :
( ! [X106] :
( p1(X106)
| ~ r1(X105,X106) )
| ~ r1(X104,X105) )
| ~ r1(X0,X104) )
& ! [X99] :
( ! [X100] :
( ? [X103] :
( ~ p1(X103)
& r1(X100,X103) )
| ! [X101] :
( ! [X102] :
( p1(X102)
| ~ r1(X101,X102) )
| ~ r1(X100,X101) )
| ~ r1(X99,X100) )
| ~ r1(X0,X99) )
& ! [X93] :
( ! [X94] :
( ! [X95] :
( ? [X98] :
( ~ p1(X98)
& r1(X95,X98) )
| ! [X96] :
( ! [X97] :
( p1(X97)
| ~ r1(X96,X97) )
| ~ r1(X95,X96) )
| ~ r1(X94,X95) )
| ~ r1(X93,X94) )
| ~ r1(X0,X93) )
& ! [X86] :
( ! [X87] :
( ! [X88] :
( ! [X89] :
( ? [X92] :
( ~ p1(X92)
& r1(X89,X92) )
| ! [X90] :
( ! [X91] :
( p1(X91)
| ~ r1(X90,X91) )
| ~ r1(X89,X90) )
| ~ r1(X88,X89) )
| ~ r1(X87,X88) )
| ~ r1(X86,X87) )
| ~ r1(X0,X86) )
& ! [X78] :
( ! [X79] :
( ! [X80] :
( ! [X81] :
( ! [X82] :
( ? [X85] :
( ~ p1(X85)
& r1(X82,X85) )
| ! [X83] :
( ! [X84] :
( p1(X84)
| ~ r1(X83,X84) )
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
| ~ r1(X80,X81) )
| ~ r1(X79,X80) )
| ~ r1(X78,X79) )
| ~ r1(X0,X78) )
& ? [X66] :
( ? [X67] :
( ? [X68] :
( ? [X69] :
( ? [X70] :
( ? [X71] :
( ! [X75] :
( ? [X76] :
( p1(X76)
& ? [X77] :
( ~ p1(X77)
& r1(X76,X77) )
& r1(X75,X76) )
| p1(X75)
| ~ r1(X71,X75) )
& ? [X73] :
( ! [X74] :
( p1(X74)
| ~ r1(X73,X74) )
& r1(X71,X73) )
& ? [X72] :
( ~ p1(X72)
& r1(X71,X72) )
& r1(X70,X71) )
& r1(X69,X70) )
& r1(X68,X69) )
& r1(X67,X68) )
& r1(X66,X67) )
& r1(X0,X66) )
& ! [X34] :
( ! [X35] :
( ! [X36] :
( ! [X37] :
( ! [X38] :
( ! [X39] :
( ( ( ? [X63] :
( ! [X64] :
( ~ p1(X64)
| ! [X65] :
( p1(X65)
| ~ r1(X64,X65) )
| ~ r1(X63,X64) )
& ~ p1(X63)
& r1(X39,X63) )
| ! [X59] :
( ! [X60] :
( ? [X61] :
( p1(X61)
& ? [X62] :
( ~ p1(X62)
& r1(X61,X62) )
& r1(X60,X61) )
| p1(X60)
| ~ r1(X59,X60) )
| ~ r1(X39,X59) ) )
& ! [X55] :
( ? [X58] :
( ~ p1(X58)
& r1(X55,X58) )
| ! [X56] :
( ! [X57] :
( p1(X57)
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X39,X55) )
& ( ? [X52] :
( ! [X53] :
( ~ p1(X53)
| ! [X54] :
( p1(X54)
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
& ~ p1(X52)
& r1(X39,X52) )
| ! [X50] :
( ? [X51] :
( ~ p1(X51)
& r1(X50,X51) )
| ~ r1(X39,X50) )
| p1(X39) )
& ( ? [X44] :
( ! [X46] :
( ( p1(X46)
& ? [X49] :
( ~ p1(X49)
& r1(X46,X49) ) )
| ! [X47] :
( ~ p1(X47)
| ! [X48] :
( p1(X48)
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X44,X46) )
& p1(X44)
& ? [X45] :
( ~ p1(X45)
& r1(X44,X45) )
& r1(X39,X44) )
| ! [X41] :
( ? [X42] :
( p1(X42)
& ? [X43] :
( ~ p1(X43)
& r1(X42,X43) )
& r1(X41,X42) )
| ~ r1(X39,X41) )
| ~ p1(X39)
| ! [X40] :
( p1(X40)
| ~ r1(X39,X40) ) ) )
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(X35,X36) )
| ~ r1(X34,X35) )
| ~ r1(X0,X34) )
& ! [X24] :
( ! [X25] :
( ! [X26] :
( ! [X27] :
( ! [X28] :
( ! [X29] :
( ! [X30] :
( ? [X33] :
( ~ p1(X33)
& r1(X30,X33) )
| ! [X31] :
( ! [X32] :
( p1(X32)
| ~ r1(X31,X32) )
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
| ~ r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X0,X24) )
& ! [X13] :
( ! [X14] :
( ! [X15] :
( ! [X16] :
( ! [X17] :
( ! [X18] :
( ! [X19] :
( ! [X20] :
( ? [X23] :
( ~ p1(X23)
& r1(X20,X23) )
| ! [X21] :
( ! [X22] :
( p1(X22)
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X14,X15) )
| ~ r1(X13,X14) )
| ~ r1(X0,X13) )
& ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ? [X12] :
( ~ p1(X12)
& r1(X9,X12) )
| ! [X10] :
( ! [X11] :
( p1(X11)
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f7,plain,
? [X0] :
( ! [X104] :
( ? [X107] :
( ~ p1(X107)
& r1(X104,X107) )
| ! [X105] :
( ! [X106] :
( p1(X106)
| ~ r1(X105,X106) )
| ~ r1(X104,X105) )
| ~ r1(X0,X104) )
& ! [X99] :
( ! [X100] :
( ? [X103] :
( ~ p1(X103)
& r1(X100,X103) )
| ! [X101] :
( ! [X102] :
( p1(X102)
| ~ r1(X101,X102) )
| ~ r1(X100,X101) )
| ~ r1(X99,X100) )
| ~ r1(X0,X99) )
& ! [X93] :
( ! [X94] :
( ! [X95] :
( ? [X98] :
( ~ p1(X98)
& r1(X95,X98) )
| ! [X96] :
( ! [X97] :
( p1(X97)
| ~ r1(X96,X97) )
| ~ r1(X95,X96) )
| ~ r1(X94,X95) )
| ~ r1(X93,X94) )
| ~ r1(X0,X93) )
& ! [X86] :
( ! [X87] :
( ! [X88] :
( ! [X89] :
( ? [X92] :
( ~ p1(X92)
& r1(X89,X92) )
| ! [X90] :
( ! [X91] :
( p1(X91)
| ~ r1(X90,X91) )
| ~ r1(X89,X90) )
| ~ r1(X88,X89) )
| ~ r1(X87,X88) )
| ~ r1(X86,X87) )
| ~ r1(X0,X86) )
& ! [X78] :
( ! [X79] :
( ! [X80] :
( ! [X81] :
( ! [X82] :
( ? [X85] :
( ~ p1(X85)
& r1(X82,X85) )
| ! [X83] :
( ! [X84] :
( p1(X84)
| ~ r1(X83,X84) )
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
| ~ r1(X80,X81) )
| ~ r1(X79,X80) )
| ~ r1(X78,X79) )
| ~ r1(X0,X78) )
& ? [X66] :
( ? [X67] :
( ? [X68] :
( ? [X69] :
( ? [X70] :
( ? [X71] :
( ! [X75] :
( ? [X76] :
( p1(X76)
& ? [X77] :
( ~ p1(X77)
& r1(X76,X77) )
& r1(X75,X76) )
| p1(X75)
| ~ r1(X71,X75) )
& ? [X73] :
( ! [X74] :
( p1(X74)
| ~ r1(X73,X74) )
& r1(X71,X73) )
& ? [X72] :
( ~ p1(X72)
& r1(X71,X72) )
& r1(X70,X71) )
& r1(X69,X70) )
& r1(X68,X69) )
& r1(X67,X68) )
& r1(X66,X67) )
& r1(X0,X66) )
& ! [X34] :
( ! [X35] :
( ! [X36] :
( ! [X37] :
( ! [X38] :
( ! [X39] :
( ( ( ? [X63] :
( ! [X64] :
( ~ p1(X64)
| ! [X65] :
( p1(X65)
| ~ r1(X64,X65) )
| ~ r1(X63,X64) )
& ~ p1(X63)
& r1(X39,X63) )
| ! [X59] :
( ! [X60] :
( ? [X61] :
( p1(X61)
& ? [X62] :
( ~ p1(X62)
& r1(X61,X62) )
& r1(X60,X61) )
| p1(X60)
| ~ r1(X59,X60) )
| ~ r1(X39,X59) ) )
& ! [X55] :
( ? [X58] :
( ~ p1(X58)
& r1(X55,X58) )
| ! [X56] :
( ! [X57] :
( p1(X57)
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X39,X55) )
& ( ? [X52] :
( ! [X53] :
( ~ p1(X53)
| ! [X54] :
( p1(X54)
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
& ~ p1(X52)
& r1(X39,X52) )
| ! [X50] :
( ? [X51] :
( ~ p1(X51)
& r1(X50,X51) )
| ~ r1(X39,X50) )
| p1(X39) )
& ( ? [X44] :
( ! [X46] :
( ( p1(X46)
& ? [X49] :
( ~ p1(X49)
& r1(X46,X49) ) )
| ! [X47] :
( ~ p1(X47)
| ! [X48] :
( p1(X48)
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X44,X46) )
& p1(X44)
& ? [X45] :
( ~ p1(X45)
& r1(X44,X45) )
& r1(X39,X44) )
| ! [X41] :
( ? [X42] :
( p1(X42)
& ? [X43] :
( ~ p1(X43)
& r1(X42,X43) )
& r1(X41,X42) )
| ~ r1(X39,X41) )
| ~ p1(X39)
| ! [X40] :
( p1(X40)
| ~ r1(X39,X40) ) ) )
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(X35,X36) )
| ~ r1(X34,X35) )
| ~ r1(X0,X34) )
& ! [X24] :
( ! [X25] :
( ! [X26] :
( ! [X27] :
( ! [X28] :
( ! [X29] :
( ! [X30] :
( ? [X33] :
( ~ p1(X33)
& r1(X30,X33) )
| ! [X31] :
( ! [X32] :
( p1(X32)
| ~ r1(X31,X32) )
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
| ~ r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X0,X24) )
& ! [X13] :
( ! [X14] :
( ! [X15] :
( ! [X16] :
( ! [X17] :
( ! [X18] :
( ! [X19] :
( ! [X20] :
( ? [X23] :
( ~ p1(X23)
& r1(X20,X23) )
| ! [X21] :
( ! [X22] :
( p1(X22)
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X14,X15) )
| ~ r1(X13,X14) )
| ~ r1(X0,X13) )
& ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ? [X12] :
( ~ p1(X12)
& r1(X9,X12) )
| ! [X10] :
( ! [X11] :
( p1(X11)
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(flattening,[],[f6]) ).
fof(f13,plain,
! [X39] :
( ~ sP3(X39)
| sP1(X39)
| ! [X41] :
( ? [X42] :
( p1(X42)
& ? [X43] :
( ~ p1(X43)
& r1(X42,X43) )
& r1(X41,X42) )
| ~ r1(X39,X41) )
| ~ p1(X39)
| ! [X40] :
( p1(X40)
| ~ r1(X39,X40) ) ),
inference(nnf_transformation,[],[f11]) ).
fof(f14,plain,
! [X0] :
( ~ sP3(X0)
| sP1(X0)
| ! [X2] :
( ? [X3] :
( p1(X3)
& ? [X4] :
( ~ p1(X4)
& r1(X3,X4) )
& r1(X2,X3) )
| ~ r1(X0,X2) )
| ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f13]) ).
fof(f15,plain,
! [X0] :
( ~ sP3(X0)
| sP1(X0)
| ! [X2] :
( ( p1(sK4(X2))
& ~ p1(sK5(X2))
& r1(sK4(X2),sK5(X2))
& r1(X2,sK4(X2)) )
| ~ r1(X0,X2) )
| ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X3,sK4(X2)),skolemize(X4,sK5(X2))],[f14]) ).
fof(f16,plain,
! [X39] :
( ~ sP2(X39)
| ? [X52] :
( ! [X53] :
( ~ p1(X53)
| ! [X54] :
( p1(X54)
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
& ~ p1(X52)
& r1(X39,X52) )
| ! [X50] :
( ? [X51] :
( ~ p1(X51)
& r1(X50,X51) )
| ~ r1(X39,X50) )
| p1(X39) ),
inference(nnf_transformation,[],[f10]) ).
fof(f17,plain,
! [X0] :
( ~ sP2(X0)
| ? [X3] :
( ! [X4] :
( ~ p1(X4)
| ! [X5] :
( p1(X5)
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
& ~ p1(X3)
& r1(X0,X3) )
| ! [X1] :
( ? [X2] :
( ~ p1(X2)
& r1(X1,X2) )
| ~ r1(X0,X1) )
| p1(X0) ),
inference(rectify,[],[f16]) ).
fof(f18,plain,
! [X0] :
( ~ sP2(X0)
| ( ! [X4] :
( ~ p1(X4)
| ! [X5] :
( p1(X5)
| ~ r1(X4,X5) )
| ~ r1(sK7(X0),X4) )
& ~ p1(sK7(X0))
& r1(X0,sK7(X0)) )
| ! [X1] :
( ( ~ p1(sK6(X1))
& r1(X1,sK6(X1)) )
| ~ r1(X0,X1) )
| p1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X2,sK6(X1)),skolemize(X3,sK7(X0))],[f17]) ).
fof(f19,plain,
! [X39] :
( ~ sP1(X39)
| ? [X44] :
( ! [X46] :
( ( p1(X46)
& ? [X49] :
( ~ p1(X49)
& r1(X46,X49) ) )
| ! [X47] :
( ~ p1(X47)
| ! [X48] :
( p1(X48)
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X44,X46) )
& p1(X44)
& ? [X45] :
( ~ p1(X45)
& r1(X44,X45) )
& r1(X39,X44) ) ),
inference(nnf_transformation,[],[f9]) ).
fof(f20,plain,
! [X0] :
( ~ sP1(X0)
| ? [X1] :
( ! [X3] :
( ( p1(X3)
& ? [X6] :
( ~ p1(X6)
& r1(X3,X6) ) )
| ! [X4] :
( ~ p1(X4)
| ! [X5] :
( p1(X5)
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X1,X3) )
& p1(X1)
& ? [X2] :
( ~ p1(X2)
& r1(X1,X2) )
& r1(X0,X1) ) ),
inference(rectify,[],[f19]) ).
fof(f21,plain,
! [X0] :
( ~ sP1(X0)
| ( ! [X3] :
( ( p1(X3)
& ~ p1(sK10(X3))
& r1(X3,sK10(X3)) )
| ! [X4] :
( ~ p1(X4)
| ! [X5] :
( p1(X5)
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(sK8(X0),X3) )
& p1(sK8(X0))
& ~ p1(sK9(X0))
& r1(sK8(X0),sK9(X0))
& r1(X0,sK8(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10]),skolemize(X1,sK8(X0)),skolemize(X2,sK9(X0)),skolemize(X6,sK10(X3))],[f20]) ).
fof(f25,plain,
? [X0] :
( ! [X85] :
( ? [X88] :
( ~ p1(X88)
& r1(X85,X88) )
| ! [X86] :
( ! [X87] :
( p1(X87)
| ~ r1(X86,X87) )
| ~ r1(X85,X86) )
| ~ r1(X0,X85) )
& ! [X80] :
( ! [X81] :
( ? [X84] :
( ~ p1(X84)
& r1(X81,X84) )
| ! [X82] :
( ! [X83] :
( p1(X83)
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
| ~ r1(X80,X81) )
| ~ r1(X0,X80) )
& ! [X74] :
( ! [X75] :
( ! [X76] :
( ? [X79] :
( ~ p1(X79)
& r1(X76,X79) )
| ! [X77] :
( ! [X78] :
( p1(X78)
| ~ r1(X77,X78) )
| ~ r1(X76,X77) )
| ~ r1(X75,X76) )
| ~ r1(X74,X75) )
| ~ r1(X0,X74) )
& ! [X67] :
( ! [X68] :
( ! [X69] :
( ! [X70] :
( ? [X73] :
( ~ p1(X73)
& r1(X70,X73) )
| ! [X71] :
( ! [X72] :
( p1(X72)
| ~ r1(X71,X72) )
| ~ r1(X70,X71) )
| ~ r1(X69,X70) )
| ~ r1(X68,X69) )
| ~ r1(X67,X68) )
| ~ r1(X0,X67) )
& ! [X59] :
( ! [X60] :
( ! [X61] :
( ! [X62] :
( ! [X63] :
( ? [X66] :
( ~ p1(X66)
& r1(X63,X66) )
| ! [X64] :
( ! [X65] :
( p1(X65)
| ~ r1(X64,X65) )
| ~ r1(X63,X64) )
| ~ r1(X62,X63) )
| ~ r1(X61,X62) )
| ~ r1(X60,X61) )
| ~ r1(X59,X60) )
| ~ r1(X0,X59) )
& ? [X47] :
( ? [X48] :
( ? [X49] :
( ? [X50] :
( ? [X51] :
( ? [X52] :
( ! [X56] :
( ? [X57] :
( p1(X57)
& ? [X58] :
( ~ p1(X58)
& r1(X57,X58) )
& r1(X56,X57) )
| p1(X56)
| ~ r1(X52,X56) )
& ? [X54] :
( ! [X55] :
( p1(X55)
| ~ r1(X54,X55) )
& r1(X52,X54) )
& ? [X53] :
( ~ p1(X53)
& r1(X52,X53) )
& r1(X51,X52) )
& r1(X50,X51) )
& r1(X49,X50) )
& r1(X48,X49) )
& r1(X47,X48) )
& r1(X0,X47) )
& ! [X34] :
( ! [X35] :
( ! [X36] :
( ! [X37] :
( ! [X38] :
( ! [X39] :
( ( ( ? [X44] :
( ! [X45] :
( ~ p1(X45)
| ! [X46] :
( p1(X46)
| ~ r1(X45,X46) )
| ~ r1(X44,X45) )
& ~ p1(X44)
& r1(X39,X44) )
| sP0(X39) )
& ! [X40] :
( ? [X43] :
( ~ p1(X43)
& r1(X40,X43) )
| ! [X41] :
( ! [X42] :
( p1(X42)
| ~ r1(X41,X42) )
| ~ r1(X40,X41) )
| ~ r1(X39,X40) )
& sP2(X39)
& sP3(X39) )
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(X35,X36) )
| ~ r1(X34,X35) )
| ~ r1(X0,X34) )
& ! [X24] :
( ! [X25] :
( ! [X26] :
( ! [X27] :
( ! [X28] :
( ! [X29] :
( ! [X30] :
( ? [X33] :
( ~ p1(X33)
& r1(X30,X33) )
| ! [X31] :
( ! [X32] :
( p1(X32)
| ~ r1(X31,X32) )
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
| ~ r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X0,X24) )
& ! [X13] :
( ! [X14] :
( ! [X15] :
( ! [X16] :
( ! [X17] :
( ! [X18] :
( ! [X19] :
( ! [X20] :
( ? [X23] :
( ~ p1(X23)
& r1(X20,X23) )
| ! [X21] :
( ! [X22] :
( p1(X22)
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X14,X15) )
| ~ r1(X13,X14) )
| ~ r1(X0,X13) )
& ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ? [X12] :
( ~ p1(X12)
& r1(X9,X12) )
| ! [X10] :
( ! [X11] :
( p1(X11)
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f12]) ).
fof(f26,plain,
( ! [X85] :
( ( ~ p1(sK33(X85))
& r1(X85,sK33(X85)) )
| ! [X86] :
( ! [X87] :
( p1(X87)
| ~ r1(X86,X87) )
| ~ r1(X85,X86) )
| ~ r1(sK13,X85) )
& ! [X80] :
( ! [X81] :
( ( ~ p1(sK32(X81))
& r1(X81,sK32(X81)) )
| ! [X82] :
( ! [X83] :
( p1(X83)
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
| ~ r1(X80,X81) )
| ~ r1(sK13,X80) )
& ! [X74] :
( ! [X75] :
( ! [X76] :
( ( ~ p1(sK31(X76))
& r1(X76,sK31(X76)) )
| ! [X77] :
( ! [X78] :
( p1(X78)
| ~ r1(X77,X78) )
| ~ r1(X76,X77) )
| ~ r1(X75,X76) )
| ~ r1(X74,X75) )
| ~ r1(sK13,X74) )
& ! [X67] :
( ! [X68] :
( ! [X69] :
( ! [X70] :
( ( ~ p1(sK30(X70))
& r1(X70,sK30(X70)) )
| ! [X71] :
( ! [X72] :
( p1(X72)
| ~ r1(X71,X72) )
| ~ r1(X70,X71) )
| ~ r1(X69,X70) )
| ~ r1(X68,X69) )
| ~ r1(X67,X68) )
| ~ r1(sK13,X67) )
& ! [X59] :
( ! [X60] :
( ! [X61] :
( ! [X62] :
( ! [X63] :
( ( ~ p1(sK29(X63))
& r1(X63,sK29(X63)) )
| ! [X64] :
( ! [X65] :
( p1(X65)
| ~ r1(X64,X65) )
| ~ r1(X63,X64) )
| ~ r1(X62,X63) )
| ~ r1(X61,X62) )
| ~ r1(X60,X61) )
| ~ r1(X59,X60) )
| ~ r1(sK13,X59) )
& ! [X56] :
( ( p1(sK27(X56))
& ~ p1(sK28(X56))
& r1(sK27(X56),sK28(X56))
& r1(X56,sK27(X56)) )
| p1(X56)
| ~ r1(sK24,X56) )
& ! [X55] :
( p1(X55)
| ~ r1(sK26,X55) )
& r1(sK24,sK26)
& ~ p1(sK25)
& r1(sK24,sK25)
& r1(sK23,sK24)
& r1(sK22,sK23)
& r1(sK21,sK22)
& r1(sK20,sK21)
& r1(sK19,sK20)
& r1(sK13,sK19)
& ! [X34] :
( ! [X35] :
( ! [X36] :
( ! [X37] :
( ! [X38] :
( ! [X39] :
( ( ( ( ! [X45] :
( ~ p1(X45)
| ! [X46] :
( p1(X46)
| ~ r1(X45,X46) )
| ~ r1(sK18(X39),X45) )
& ~ p1(sK18(X39))
& r1(X39,sK18(X39)) )
| sP0(X39) )
& ! [X40] :
( ( ~ p1(sK17(X40))
& r1(X40,sK17(X40)) )
| ! [X41] :
( ! [X42] :
( p1(X42)
| ~ r1(X41,X42) )
| ~ r1(X40,X41) )
| ~ r1(X39,X40) )
& sP2(X39)
& sP3(X39) )
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(X35,X36) )
| ~ r1(X34,X35) )
| ~ r1(sK13,X34) )
& ! [X24] :
( ! [X25] :
( ! [X26] :
( ! [X27] :
( ! [X28] :
( ! [X29] :
( ! [X30] :
( ( ~ p1(sK16(X30))
& r1(X30,sK16(X30)) )
| ! [X31] :
( ! [X32] :
( p1(X32)
| ~ r1(X31,X32) )
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
| ~ r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(sK13,X24) )
& ! [X13] :
( ! [X14] :
( ! [X15] :
( ! [X16] :
( ! [X17] :
( ! [X18] :
( ! [X19] :
( ! [X20] :
( ( ~ p1(sK15(X20))
& r1(X20,sK15(X20)) )
| ! [X21] :
( ! [X22] :
( p1(X22)
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X14,X15) )
| ~ r1(X13,X14) )
| ~ r1(sK13,X13) )
& ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ( ~ p1(sK14(X9))
& r1(X9,sK14(X9)) )
| ! [X10] :
( ! [X11] :
( p1(X11)
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(sK13,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29,sK30,sK31,sK32,sK33]),skolemize(X0,sK13),skolemize(X12,sK14(X9)),skolemize(X23,sK15(X20)),skolemize(X33,sK16(X30)),skolemize(X43,sK17(X40)),skolemize(X44,sK18(X39)),skolemize(X47,sK19),skolemize(X48,sK20),skolemize(X49,sK21),skolemize(X50,sK22),skolemize(X51,sK23),skolemize(X52,sK24),skolemize(X53,sK25),skolemize(X54,sK26),skolemize(X57,sK27(X56)),skolemize(X58,sK28(X56)),skolemize(X66,sK29(X63)),skolemize(X73,sK30(X70)),skolemize(X79,sK31(X76)),skolemize(X84,sK32(X81)),skolemize(X88,sK33(X85))],[f25]) ).
fof(f29,plain,
! [X2,X0,X1] :
( ~ sP3(X0)
| sP1(X0)
| ~ p1(sK5(X2))
| ~ r1(X0,X2)
| ~ p1(X0)
| p1(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f15]) ).
fof(f30,plain,
! [X2,X0,X1] :
( ~ sP3(X0)
| sP1(X0)
| r1(sK4(X2),sK5(X2))
| ~ r1(X0,X2)
| ~ p1(X0)
| p1(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f15]) ).
fof(f31,plain,
! [X2,X0,X1] :
( ~ sP3(X0)
| sP1(X0)
| r1(X2,sK4(X2))
| ~ r1(X0,X2)
| ~ p1(X0)
| p1(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f15]) ).
fof(f32,plain,
! [X0,X1,X4,X5] :
( ~ sP2(X0)
| ~ p1(X4)
| p1(X5)
| ~ r1(X4,X5)
| ~ r1(sK7(X0),X4)
| ~ p1(sK6(X1))
| ~ r1(X0,X1)
| p1(X0) ),
inference(cnf_transformation,[],[f18]) ).
fof(f33,plain,
! [X0,X1] :
( ~ sP2(X0)
| ~ p1(sK7(X0))
| ~ p1(sK6(X1))
| ~ r1(X0,X1)
| p1(X0) ),
inference(cnf_transformation,[],[f18]) ).
fof(f34,plain,
! [X0,X1] :
( ~ sP2(X0)
| r1(X0,sK7(X0))
| ~ p1(sK6(X1))
| ~ r1(X0,X1)
| p1(X0) ),
inference(cnf_transformation,[],[f18]) ).
fof(f35,plain,
! [X0,X1,X4,X5] :
( ~ sP2(X0)
| ~ p1(X4)
| p1(X5)
| ~ r1(X4,X5)
| ~ r1(sK7(X0),X4)
| r1(X1,sK6(X1))
| ~ r1(X0,X1)
| p1(X0) ),
inference(cnf_transformation,[],[f18]) ).
fof(f36,plain,
! [X0,X1] :
( ~ sP2(X0)
| ~ p1(sK7(X0))
| r1(X1,sK6(X1))
| ~ r1(X0,X1)
| p1(X0) ),
inference(cnf_transformation,[],[f18]) ).
fof(f37,plain,
! [X0,X1] :
( ~ sP2(X0)
| r1(X0,sK7(X0))
| r1(X1,sK6(X1))
| ~ r1(X0,X1)
| p1(X0) ),
inference(cnf_transformation,[],[f18]) ).
fof(f38,plain,
! [X3,X0,X4,X5] :
( ~ sP1(X0)
| p1(X3)
| ~ p1(X4)
| p1(X5)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(sK8(X0),X3) ),
inference(cnf_transformation,[],[f21]) ).
fof(f42,plain,
! [X0] :
( ~ sP1(X0)
| ~ p1(sK9(X0)) ),
inference(cnf_transformation,[],[f21]) ).
fof(f43,plain,
! [X0] :
( ~ sP1(X0)
| r1(sK8(X0),sK9(X0)) ),
inference(cnf_transformation,[],[f21]) ).
fof(f44,plain,
! [X0] :
( ~ sP1(X0)
| r1(X0,sK8(X0)) ),
inference(cnf_transformation,[],[f21]) ).
fof(f56,plain,
! [X72,X70,X71,X68,X69,X67] :
( r1(X70,sK30(X70))
| p1(X72)
| ~ r1(X71,X72)
| ~ r1(X70,X71)
| ~ r1(X69,X70)
| ~ r1(X68,X69)
| ~ r1(X67,X68)
| ~ r1(sK13,X67) ),
inference(cnf_transformation,[],[f26]) ).
fof(f58,plain,
! [X65,X59,X62,X63,X60,X61,X64] :
( r1(X63,sK29(X63))
| p1(X65)
| ~ r1(X64,X65)
| ~ r1(X63,X64)
| ~ r1(X62,X63)
| ~ r1(X61,X62)
| ~ r1(X60,X61)
| ~ r1(X59,X60)
| ~ r1(sK13,X59) ),
inference(cnf_transformation,[],[f26]) ).
fof(f59,plain,
! [X56] :
( p1(sK27(X56))
| p1(X56)
| ~ r1(sK24,X56) ),
inference(cnf_transformation,[],[f26]) ).
fof(f60,plain,
! [X56] :
( ~ p1(sK28(X56))
| p1(X56)
| ~ r1(sK24,X56) ),
inference(cnf_transformation,[],[f26]) ).
fof(f61,plain,
! [X56] :
( r1(sK27(X56),sK28(X56))
| p1(X56)
| ~ r1(sK24,X56) ),
inference(cnf_transformation,[],[f26]) ).
fof(f62,plain,
! [X56] :
( r1(X56,sK27(X56))
| p1(X56)
| ~ r1(sK24,X56) ),
inference(cnf_transformation,[],[f26]) ).
fof(f63,plain,
! [X55] :
( p1(X55)
| ~ r1(sK26,X55) ),
inference(cnf_transformation,[],[f26]) ).
fof(f64,plain,
r1(sK24,sK26),
inference(cnf_transformation,[],[f26]) ).
fof(f65,plain,
~ p1(sK25),
inference(cnf_transformation,[],[f26]) ).
fof(f66,plain,
r1(sK24,sK25),
inference(cnf_transformation,[],[f26]) ).
fof(f67,plain,
r1(sK23,sK24),
inference(cnf_transformation,[],[f26]) ).
fof(f68,plain,
r1(sK22,sK23),
inference(cnf_transformation,[],[f26]) ).
fof(f69,plain,
r1(sK21,sK22),
inference(cnf_transformation,[],[f26]) ).
fof(f70,plain,
r1(sK20,sK21),
inference(cnf_transformation,[],[f26]) ).
fof(f71,plain,
r1(sK19,sK20),
inference(cnf_transformation,[],[f26]) ).
fof(f72,plain,
r1(sK13,sK19),
inference(cnf_transformation,[],[f26]) ).
fof(f73,plain,
! [X38,X39,X46,X36,X37,X45,X34,X35] :
( ~ p1(X45)
| p1(X46)
| ~ r1(X45,X46)
| ~ r1(sK18(X39),X45)
| sP0(X39)
| ~ r1(X38,X39)
| ~ r1(X37,X38)
| ~ r1(X36,X37)
| ~ r1(X35,X36)
| ~ r1(X34,X35)
| ~ r1(sK13,X34) ),
inference(cnf_transformation,[],[f26]) ).
fof(f74,plain,
! [X38,X39,X36,X37,X34,X35] :
( ~ p1(sK18(X39))
| sP0(X39)
| ~ r1(X38,X39)
| ~ r1(X37,X38)
| ~ r1(X36,X37)
| ~ r1(X35,X36)
| ~ r1(X34,X35)
| ~ r1(sK13,X34) ),
inference(cnf_transformation,[],[f26]) ).
fof(f75,plain,
! [X38,X39,X36,X37,X34,X35] :
( r1(X39,sK18(X39))
| sP0(X39)
| ~ r1(X38,X39)
| ~ r1(X37,X38)
| ~ r1(X36,X37)
| ~ r1(X35,X36)
| ~ r1(X34,X35)
| ~ r1(sK13,X34) ),
inference(cnf_transformation,[],[f26]) ).
fof(f76,plain,
! [X40,X38,X41,X39,X36,X37,X34,X35,X42] :
( ~ p1(sK17(X40))
| p1(X42)
| ~ r1(X41,X42)
| ~ r1(X40,X41)
| ~ r1(X39,X40)
| ~ r1(X38,X39)
| ~ r1(X37,X38)
| ~ r1(X36,X37)
| ~ r1(X35,X36)
| ~ r1(X34,X35)
| ~ r1(sK13,X34) ),
inference(cnf_transformation,[],[f26]) ).
fof(f77,plain,
! [X40,X38,X41,X39,X36,X37,X34,X35,X42] :
( r1(X40,sK17(X40))
| p1(X42)
| ~ r1(X41,X42)
| ~ r1(X40,X41)
| ~ r1(X39,X40)
| ~ r1(X38,X39)
| ~ r1(X37,X38)
| ~ r1(X36,X37)
| ~ r1(X35,X36)
| ~ r1(X34,X35)
| ~ r1(sK13,X34) ),
inference(cnf_transformation,[],[f26]) ).
fof(f78,plain,
! [X38,X39,X36,X37,X34,X35] :
( sP2(X39)
| ~ r1(X38,X39)
| ~ r1(X37,X38)
| ~ r1(X36,X37)
| ~ r1(X35,X36)
| ~ r1(X34,X35)
| ~ r1(sK13,X34) ),
inference(cnf_transformation,[],[f26]) ).
fof(f79,plain,
! [X38,X39,X36,X37,X34,X35] :
( sP3(X39)
| ~ r1(X38,X39)
| ~ r1(X37,X38)
| ~ r1(X36,X37)
| ~ r1(X35,X36)
| ~ r1(X34,X35)
| ~ r1(sK13,X34) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X0)
| p1(X1)
| r1(X2,sK4(X2))
| ~ sP3(X0)
| ~ p1(X0)
| ~ r1(X0,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X0)
| p1(X1)
| r1(sK4(X2),sK5(X2))
| ~ sP3(X0)
| ~ p1(X0)
| ~ r1(X0,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X0)
| p1(X1)
| ~ sP3(X0)
| ~ p1(X0)
| ~ p1(sK5(X2))
| ~ r1(X0,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i] :
( p1(X0)
| r1(X1,sK6(X1))
| r1(X0,sK7(X0))
| ~ sP2(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i] :
( p1(X0)
| r1(X1,sK6(X1))
| ~ sP2(X0)
| ~ p1(sK7(X0))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X3)
| p1(X0)
| r1(X2,sK6(X2))
| ~ sP2(X0)
| ~ p1(X1)
| ~ r1(X1,X3)
| ~ r1(X0,X2)
| ~ r1(sK7(X0),X1) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i] :
( p1(X0)
| r1(X0,sK7(X0))
| ~ sP2(X0)
| ~ p1(sK6(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i] :
( p1(X0)
| ~ sP2(X0)
| ~ p1(sK7(X0))
| ~ p1(sK6(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X3)
| p1(X0)
| ~ sP2(X0)
| ~ p1(X1)
| ~ p1(sK6(X2))
| ~ r1(X1,X3)
| ~ r1(X0,X2)
| ~ r1(sK7(X0),X1) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_60,plain,
! [X0: $i] :
( r1(X0,sK8(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_61,plain,
! [X0: $i] :
( r1(sK8(X0),sK9(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_62,plain,
! [X0: $i] :
( ~ sP1(X0)
| ~ p1(sK9(X0)) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X3)
| p1(X1)
| ~ sP1(X0)
| ~ p1(X2)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(sK8(X0),X1) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_77,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( sP3(X5)
| ~ r1(sK13,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f79]) ).
tcf(c_78,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( sP2(X5)
| ~ r1(sK13,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_79,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
( p1(X8)
| r1(X6,sK17(X6))
| ~ r1(sK13,X0)
| ~ r1(X7,X8)
| ~ r1(X6,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_80,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
( p1(X8)
| ~ p1(sK17(X6))
| ~ r1(sK13,X0)
| ~ r1(X7,X8)
| ~ r1(X6,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_81,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( sP0(X5)
| r1(X5,sK18(X5))
| ~ r1(sK13,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_82,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( sP0(X5)
| ~ p1(sK18(X5))
| ~ r1(sK13,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_83,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( sP0(X0)
| p1(X7)
| ~ p1(X1)
| ~ r1(sK13,X2)
| ~ r1(X6,X0)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X7)
| ~ r1(sK18(X0),X1) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_84,negated_conjecture,
r1(sK13,sK19),
inference(cnf_transformation,[],[f72]) ).
tcf(c_85,negated_conjecture,
r1(sK19,sK20),
inference(cnf_transformation,[],[f71]) ).
tcf(c_86,negated_conjecture,
r1(sK20,sK21),
inference(cnf_transformation,[],[f70]) ).
tcf(c_87,negated_conjecture,
r1(sK21,sK22),
inference(cnf_transformation,[],[f69]) ).
tcf(c_88,negated_conjecture,
r1(sK22,sK23),
inference(cnf_transformation,[],[f68]) ).
tcf(c_89,negated_conjecture,
r1(sK23,sK24),
inference(cnf_transformation,[],[f67]) ).
tcf(c_90,negated_conjecture,
r1(sK24,sK25),
inference(cnf_transformation,[],[f66]) ).
tcf(c_91,negated_conjecture,
~ p1(sK25),
inference(cnf_transformation,[],[f65]) ).
tcf(c_92,negated_conjecture,
r1(sK24,sK26),
inference(cnf_transformation,[],[f64]) ).
tcf(c_93,negated_conjecture,
! [X0: $i] :
( p1(X0)
| ~ r1(sK26,X0) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_94,negated_conjecture,
! [X0: $i] :
( p1(X0)
| r1(X0,sK27(X0))
| ~ r1(sK24,X0) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_95,negated_conjecture,
! [X0: $i] :
( p1(X0)
| r1(sK27(X0),sK28(X0))
| ~ r1(sK24,X0) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_96,negated_conjecture,
! [X0: $i] :
( p1(X0)
| ~ p1(sK28(X0))
| ~ r1(sK24,X0) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_97,negated_conjecture,
! [X0: $i] :
( p1(X0)
| p1(sK27(X0))
| ~ r1(sK24,X0) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_98,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p1(X6)
| r1(X4,sK29(X4))
| ~ r1(sK13,X0)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_100,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(X5)
| r1(X3,sK30(X3))
| ~ r1(sK13,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_3159,plain,
( p1(sK24)
| r1(sK26,sK6(sK26))
| ~ sP2(sK24)
| ~ p1(sK7(sK24)) ),
inference(superposition,[status(thm)],[c_92,c_55]) ).
tcf(c_3409,plain,
! [X0: $i,X1: $i] :
( p1(sK25)
| sP1(X0)
| r1(X1,sK4(X1))
| ~ sP3(X0)
| ~ p1(X0)
| ~ r1(X0,sK25)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_3461,plain,
! [X0: $i,X1: $i] :
( p1(sK25)
| sP1(X0)
| r1(sK4(X1),sK5(X1))
| ~ sP3(X0)
| ~ p1(X0)
| ~ r1(X0,sK25)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_3580,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( p1(X7)
| r1(X5,sK17(X5))
| ~ r1(sK19,X0)
| ~ r1(X6,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_79,c_84]) ).
tcf(c_3598,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p1(X6)
| r1(X4,sK17(X4))
| ~ r1(sK20,X0)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_3580,c_85]) ).
tcf(c_3743,plain,
! [X0: $i] :
( sP1(sK24)
| p1(sK25)
| r1(X0,sK4(X0))
| ~ sP3(sK24)
| ~ p1(sK24)
| ~ r1(sK24,sK25)
| ~ r1(sK24,X0) ),
inference(instantiation,[status(thm)],[c_3409]) ).
tcf(c_3757,plain,
! [X0: $i] :
( sP1(sK24)
| p1(sK25)
| r1(sK4(X0),sK5(X0))
| ~ sP3(sK24)
| ~ p1(sK24)
| ~ r1(sK24,sK25)
| ~ r1(sK24,X0) ),
inference(instantiation,[status(thm)],[c_3461]) ).
tcf(c_3778,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(X5)
| r1(X3,sK17(X3))
| ~ r1(sK21,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_3598,c_86]) ).
tcf(c_3828,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(X4)
| r1(X2,sK17(X2))
| ~ r1(sK22,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_3778,c_87]) ).
tcf(c_3862,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X3)
| r1(X1,sK17(X1))
| ~ r1(sK23,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_3828,c_88]) ).
tcf(c_3881,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X2)
| r1(X0,sK17(X0))
| ~ r1(sK24,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_3862,c_89]) ).
tcf(c_3916,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| r1(sK26,sK17(sK26))
| ~ r1(sK26,X0)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_3881,c_92]) ).
tcf(c_4194,plain,
( p1(sK24)
| r1(sK24,sK7(sK24))
| ~ sP2(sK24)
| ~ p1(sK6(sK26)) ),
inference(superposition,[status(thm)],[c_92,c_57]) ).
tcf(c_4214,plain,
( p1(sK24)
| ~ sP2(sK24)
| ~ p1(sK7(sK24))
| ~ p1(sK6(sK26)) ),
inference(superposition,[status(thm)],[c_92,c_58]) ).
tcf(c_4460,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(X5)
| r1(X3,sK29(X3))
| ~ r1(sK19,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_98,c_84]) ).
tcf(c_4464,plain,
( sP1(sK24)
| p1(sK25)
| r1(sK26,sK4(sK26))
| ~ sP3(sK24)
| ~ p1(sK24)
| ~ r1(sK24,sK26)
| ~ r1(sK24,sK25) ),
inference(instantiation,[status(thm)],[c_3743]) ).
tcf(c_4466,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(X4)
| r1(X2,sK29(X2))
| ~ r1(sK20,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_4460,c_85]) ).
tcf(c_4470,plain,
( sP1(sK24)
| p1(sK25)
| r1(sK4(sK26),sK5(sK26))
| ~ sP3(sK24)
| ~ p1(sK24)
| ~ r1(sK24,sK26)
| ~ r1(sK24,sK25) ),
inference(instantiation,[status(thm)],[c_3757]) ).
tcf(c_4500,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X3)
| r1(X1,sK29(X1))
| ~ r1(sK21,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_4466,c_86]) ).
tcf(c_4507,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X2)
| r1(X0,sK29(X0))
| ~ r1(sK22,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_4500,c_87]) ).
tcf(c_4527,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| r1(sK23,sK29(sK23))
| ~ r1(sK23,X0)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_4507,c_88]) ).
tcf(c_4529,plain,
! [X0: $i] :
( p1(X0)
| r1(sK23,sK29(sK23))
| ~ r1(sK24,X0) ),
inference(resolution,[status(thm)],[c_4527,c_89]) ).
tcf(c_4566,plain,
( p1(sK25)
| r1(sK23,sK29(sK23)) ),
inference(resolution,[status(thm)],[c_4529,c_90]) ).
tcf(c_4568,plain,
r1(sK23,sK29(sK23)),
inference(global_subsumption_just,[status(thm)],[c_4566,c_91,c_4566]) ).
tcf(c_4575,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(X4)
| r1(X2,sK30(X2))
| ~ r1(sK19,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_100,c_84]) ).
tcf(c_4594,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X3)
| r1(X1,sK30(X1))
| ~ r1(sK20,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_4575,c_85]) ).
tcf(c_4612,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X2)
| r1(X0,sK30(X0))
| ~ r1(sK21,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_4594,c_86]) ).
tcf(c_4619,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| r1(sK22,sK30(sK22))
| ~ r1(sK22,X0)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_4612,c_87]) ).
tcf(c_4627,plain,
! [X0: $i] :
( p1(X0)
| r1(sK22,sK30(sK22))
| ~ r1(sK23,X0) ),
inference(resolution,[status(thm)],[c_4619,c_88]) ).
tcf(c_4674,plain,
( p1(sK29(sK23))
| r1(sK22,sK30(sK22)) ),
inference(resolution,[status(thm)],[c_4627,c_4568]) ).
tcf(c_4855,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( sP0(X4)
| r1(X4,sK18(X4))
| ~ r1(sK19,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_81,c_84]) ).
tcf(c_4919,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP0(X3)
| r1(X3,sK18(X3))
| ~ r1(sK20,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_4855,c_85]) ).
tcf(c_4943,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP0(X2)
| r1(X2,sK18(X2))
| ~ r1(sK21,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_4919,c_86]) ).
tcf(c_4948,plain,
! [X0: $i,X1: $i] :
( sP0(X1)
| r1(X1,sK18(X1))
| ~ r1(sK22,X0)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_4943,c_87]) ).
tcf(c_4953,plain,
! [X0: $i] :
( sP0(X0)
| r1(X0,sK18(X0))
| ~ r1(sK23,X0) ),
inference(resolution,[status(thm)],[c_4948,c_88]) ).
tcf(c_4978,plain,
( sP0(sK24)
| r1(sK24,sK18(sK24)) ),
inference(resolution,[status(thm)],[c_4953,c_89]) ).
tcf(c_5026,plain,
( sP0(sK24)
| p1(sK18(sK24))
| r1(sK27(sK18(sK24)),sK28(sK18(sK24))) ),
inference(resolution,[status(thm)],[c_4978,c_95]) ).
tcf(c_5027,plain,
( sP0(sK24)
| p1(sK18(sK24))
| r1(sK18(sK24),sK27(sK18(sK24))) ),
inference(resolution,[status(thm)],[c_4978,c_94]) ).
tcf(c_5028,plain,
( sP0(sK24)
| p1(sK18(sK24))
| p1(sK27(sK18(sK24))) ),
inference(resolution,[status(thm)],[c_4978,c_97]) ).
tcf(c_5115,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( sP0(sK24)
| p1(X0)
| p1(sK18(sK24))
| ~ r1(sK13,X1)
| ~ r1(X5,sK24)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ p1(sK27(sK18(sK24)))
| ~ r1(sK27(sK18(sK24)),X0) ),
inference(resolution,[status(thm)],[c_83,c_5027]) ).
tcf(c_5167,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( sP0(sK24)
| p1(X0)
| p1(sK18(sK24))
| ~ r1(sK13,X1)
| ~ r1(X5,sK24)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(sK27(sK18(sK24)),X0) ),
inference(global_subsumption_just,[status(thm)],[c_5115,c_5028,c_5115]) ).
tcf(c_5208,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( sP0(sK24)
| p1(sK18(sK24))
| p1(sK28(sK18(sK24)))
| ~ r1(sK13,X0)
| ~ r1(X4,sK24)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_5167,c_5026]) ).
tcf(c_5227,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP0(sK24)
| p1(sK18(sK24))
| p1(sK28(sK18(sK24)))
| ~ r1(sK19,X0)
| ~ r1(X3,sK24)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_5208,c_84]) ).
tcf(c_5267,plain,
( p1(sK24)
| r1(sK26,sK6(sK26))
| r1(sK24,sK7(sK24))
| ~ sP2(sK24) ),
inference(superposition,[status(thm)],[c_92,c_54]) ).
tcf(c_5273,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP0(sK24)
| p1(sK18(sK24))
| p1(sK28(sK18(sK24)))
| ~ r1(sK20,X0)
| ~ r1(X2,sK24)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_5227,c_85]) ).
tcf(c_5291,plain,
! [X0: $i,X1: $i] :
( sP0(sK24)
| p1(sK18(sK24))
| p1(sK28(sK18(sK24)))
| ~ r1(sK21,X0)
| ~ r1(X1,sK24)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_5273,c_86]) ).
tcf(c_5360,plain,
! [X0: $i] :
( sP0(sK24)
| p1(sK18(sK24))
| p1(sK28(sK18(sK24)))
| ~ r1(sK22,X0)
| ~ r1(X0,sK24) ),
inference(resolution,[status(thm)],[c_5291,c_87]) ).
tcf(c_5407,plain,
( sP0(sK24)
| p1(sK18(sK24))
| p1(sK28(sK18(sK24)))
| ~ r1(sK23,sK24) ),
inference(resolution,[status(thm)],[c_5360,c_88]) ).
tcf(c_5408,plain,
( sP0(sK24)
| p1(sK29(sK23))
| p1(sK18(sK24))
| p1(sK28(sK18(sK24)))
| ~ r1(sK30(sK22),sK24) ),
inference(resolution,[status(thm)],[c_5360,c_4674]) ).
tcf(c_5423,plain,
( sP0(sK24)
| p1(sK28(sK18(sK24)))
| p1(sK18(sK24)) ),
inference(global_subsumption_just,[status(thm)],[c_5408,c_89,c_5407]) ).
tcf(c_5424,plain,
( sP0(sK24)
| p1(sK18(sK24))
| p1(sK28(sK18(sK24))) ),
inference(renaming,[status(thm)],[c_5423]) ).
tcf(c_5425,plain,
( sP0(sK24)
| p1(sK18(sK24))
| ~ r1(sK24,sK18(sK24)) ),
inference(resolution,[status(thm)],[c_96,c_5424]) ).
tcf(c_5532,plain,
( sP0(sK24)
| p1(sK18(sK24)) ),
inference(global_subsumption_just,[status(thm)],[c_5425,c_4978,c_5425]) ).
tcf(c_5534,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( sP0(sK24)
| ~ r1(sK13,X0)
| ~ r1(X4,sK24)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_82,c_5532]) ).
tcf(c_5549,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP0(sK24)
| ~ r1(sK19,X0)
| ~ r1(X3,sK24)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_5534,c_84]) ).
tcf(c_5551,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP0(sK24)
| ~ r1(sK20,X0)
| ~ r1(X2,sK24)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_5549,c_85]) ).
tcf(c_5566,plain,
! [X0: $i,X1: $i] :
( sP0(sK24)
| ~ r1(sK21,X0)
| ~ r1(X1,sK24)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_5551,c_86]) ).
tcf(c_5581,plain,
! [X0: $i] :
( sP0(sK24)
| ~ r1(sK22,X0)
| ~ r1(X0,sK24) ),
inference(resolution,[status(thm)],[c_5566,c_87]) ).
tcf(c_5583,plain,
( sP0(sK24)
| ~ r1(sK23,sK24) ),
inference(resolution,[status(thm)],[c_5581,c_88]) ).
tcf(c_7812,plain,
( p1(sK24)
| p1(sK6(sK26))
| r1(sK24,sK7(sK24))
| ~ sP2(sK24) ),
inference(superposition,[status(thm)],[c_5267,c_93]) ).
tcf(c_7874,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( sP2(X4)
| ~ r1(sK19,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_78,c_84]) ).
tcf(c_7881,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP2(X3)
| ~ r1(sK20,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7874,c_85]) ).
tcf(c_7888,plain,
( p1(sK24)
| ~ sP2(sK24)
| r1(sK24,sK7(sK24)) ),
inference(global_subsumption_just,[status(thm)],[c_7812,c_4194,c_7812]) ).
tcf(c_7889,plain,
( p1(sK24)
| r1(sK24,sK7(sK24))
| ~ sP2(sK24) ),
inference(renaming,[status(thm)],[c_7888]) ).
tcf(c_7925,plain,
( p1(sK24)
| p1(sK7(sK24))
| ~ sP2(sK24)
| ~ p1(sK28(sK7(sK24))) ),
inference(superposition,[status(thm)],[c_7889,c_96]) ).
tcf(c_7926,plain,
( p1(sK24)
| p1(sK7(sK24))
| p1(sK27(sK7(sK24)))
| ~ sP2(sK24) ),
inference(superposition,[status(thm)],[c_7889,c_97]) ).
tcf(c_7954,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP2(X2)
| ~ r1(sK21,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7881,c_86]) ).
tcf(c_8013,plain,
! [X0: $i,X1: $i] :
( sP2(X1)
| ~ r1(sK22,X0)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7954,c_87]) ).
tcf(c_8017,plain,
! [X0: $i] :
( sP2(X0)
| ~ r1(sK23,X0) ),
inference(resolution,[status(thm)],[c_8013,c_88]) ).
tcf(c_8023,plain,
sP2(sK24),
inference(resolution,[status(thm)],[c_8017,c_89]) ).
tcf(c_8025,plain,
( p1(sK24)
| p1(sK7(sK24))
| p1(sK27(sK7(sK24))) ),
inference(global_subsumption_just,[status(thm)],[c_7926,c_7926,c_8023]) ).
tcf(c_8034,plain,
( p1(sK24)
| r1(sK26,sK6(sK26))
| r1(sK24,sK7(sK24))
| ~ sP2(sK24) ),
inference(resolution,[status(thm)],[c_54,c_92]) ).
tcf(c_8514,plain,
( p1(sK24)
| r1(sK24,sK7(sK24)) ),
inference(global_subsumption_just,[status(thm)],[c_8034,c_7889,c_8023]) ).
tcf(c_8523,plain,
( p1(sK24)
| p1(sK7(sK24))
| r1(sK27(sK7(sK24)),sK28(sK7(sK24))) ),
inference(resolution,[status(thm)],[c_8514,c_95]) ).
tcf(c_8524,plain,
( p1(sK24)
| p1(sK7(sK24))
| r1(sK7(sK24),sK27(sK7(sK24))) ),
inference(resolution,[status(thm)],[c_8514,c_94]) ).
tcf(c_8787,plain,
! [X0: $i,X1: $i] :
( p1(sK24)
| p1(X0)
| p1(sK7(sK24))
| r1(X1,sK6(X1))
| ~ sP2(sK24)
| ~ r1(sK24,X1)
| ~ p1(sK27(sK7(sK24)))
| ~ r1(sK27(sK7(sK24)),X0) ),
inference(resolution,[status(thm)],[c_56,c_8524]) ).
tcf(c_8821,plain,
! [X0: $i,X1: $i] :
( p1(sK24)
| p1(X0)
| p1(sK7(sK24))
| r1(X1,sK6(X1))
| ~ r1(sK27(sK7(sK24)),X0)
| ~ r1(sK24,X1) ),
inference(global_subsumption_just,[status(thm)],[c_8787,c_7926,c_8023,c_8787]) ).
tcf(c_8822,plain,
! [X0: $i,X1: $i] :
( p1(sK24)
| p1(X0)
| p1(sK7(sK24))
| r1(X1,sK6(X1))
| ~ r1(sK24,X1)
| ~ r1(sK27(sK7(sK24)),X0) ),
inference(renaming,[status(thm)],[c_8821]) ).
tcf(c_8829,plain,
! [X0: $i] :
( p1(sK24)
| p1(sK7(sK24))
| p1(sK28(sK7(sK24)))
| r1(X0,sK6(X0))
| ~ r1(sK24,X0) ),
inference(resolution,[status(thm)],[c_8822,c_8523]) ).
tcf(c_8854,plain,
! [X0: $i] :
( p1(sK24)
| p1(sK7(sK24))
| ~ r1(sK24,X0)
| r1(X0,sK6(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_8829,c_7925,c_8023,c_8829]) ).
tcf(c_8855,plain,
! [X0: $i] :
( p1(sK24)
| p1(sK7(sK24))
| r1(X0,sK6(X0))
| ~ r1(sK24,X0) ),
inference(renaming,[status(thm)],[c_8854]) ).
tcf(c_8871,plain,
( p1(sK24)
| p1(sK7(sK24))
| r1(sK26,sK6(sK26)) ),
inference(resolution,[status(thm)],[c_8855,c_92]) ).
tcf(c_9371,plain,
( p1(sK24)
| r1(sK26,sK6(sK26)) ),
inference(global_subsumption_just,[status(thm)],[c_8871,c_3159,c_8023,c_8871]) ).
tcf(c_9548,plain,
( p1(sK24)
| p1(sK6(sK26)) ),
inference(resolution,[status(thm)],[c_93,c_9371]) ).
tcf(c_9551,plain,
! [X0: $i,X1: $i] :
( p1(sK24)
| p1(X0)
| p1(sK7(sK24))
| ~ sP2(sK24)
| ~ p1(sK6(X1))
| ~ r1(sK24,X1)
| ~ p1(sK27(sK7(sK24)))
| ~ r1(sK27(sK7(sK24)),X0) ),
inference(resolution,[status(thm)],[c_59,c_8524]) ).
tcf(c_9735,plain,
! [X0: $i,X1: $i] :
( p1(sK24)
| p1(X0)
| ~ p1(sK6(X1))
| ~ r1(sK24,X1)
| ~ r1(sK27(sK7(sK24)),X0) ),
inference(global_subsumption_just,[status(thm)],[c_9551,c_4214,c_8023,c_8025,c_9548,c_9551]) ).
tcf(c_9745,plain,
! [X0: $i] :
( p1(sK24)
| p1(sK7(sK24))
| p1(sK28(sK7(sK24)))
| ~ p1(sK6(X0))
| ~ r1(sK24,X0) ),
inference(resolution,[status(thm)],[c_9735,c_8523]) ).
tcf(c_9757,plain,
! [X0: $i] :
( p1(sK24)
| ~ p1(sK6(X0))
| ~ r1(sK24,X0) ),
inference(global_subsumption_just,[status(thm)],[c_9745,c_4214,c_7925,c_8023,c_9548,c_9745]) ).
tcf(c_9760,plain,
( p1(sK24)
| ~ r1(sK24,sK26) ),
inference(resolution,[status(thm)],[c_9757,c_9548]) ).
tcf(c_10228,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( sP3(X4)
| ~ r1(sK19,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_77,c_84]) ).
tcf(c_10230,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP3(X3)
| ~ r1(sK20,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_10228,c_85]) ).
tcf(c_10328,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP3(X2)
| ~ r1(sK21,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_10230,c_86]) ).
tcf(c_10337,plain,
! [X0: $i,X1: $i] :
( sP3(X1)
| ~ r1(sK22,X0)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_10328,c_87]) ).
tcf(c_10351,plain,
! [X0: $i] :
( sP3(X0)
| ~ r1(sK23,X0) ),
inference(resolution,[status(thm)],[c_10337,c_88]) ).
tcf(c_10356,plain,
sP3(sK24),
inference(resolution,[status(thm)],[c_10351,c_89]) ).
tcf(c_10377,plain,
! [X0: $i] :
( sP1(sK24)
| p1(X0)
| r1(sK4(sK26),sK5(sK26))
| ~ sP3(sK24)
| ~ p1(sK24)
| ~ r1(sK24,X0) ),
inference(resolution,[status(thm)],[c_51,c_92]) ).
tcf(c_10632,plain,
( sP1(sK24)
| r1(sK4(sK26),sK5(sK26)) ),
inference(global_subsumption_just,[status(thm)],[c_10377,c_92,c_91,c_90,c_4470,c_9760,c_10356]) ).
tcf(c_10788,plain,
! [X0: $i] :
( sP1(sK24)
| p1(X0)
| r1(sK26,sK4(sK26))
| ~ sP3(sK24)
| ~ p1(sK24)
| ~ r1(sK24,X0) ),
inference(resolution,[status(thm)],[c_50,c_92]) ).
tcf(c_11110,plain,
( sP1(sK24)
| r1(sK26,sK4(sK26)) ),
inference(global_subsumption_just,[status(thm)],[c_10788,c_92,c_91,c_90,c_4464,c_9760,c_10356]) ).
tcf(c_11121,plain,
! [X0: $i] :
( sP1(sK24)
| p1(X0)
| r1(sK26,sK17(sK26))
| ~ r1(sK4(sK26),X0) ),
inference(resolution,[status(thm)],[c_11110,c_3916]) ).
tcf(c_11374,plain,
( sP1(sK24)
| p1(sK5(sK26))
| r1(sK26,sK17(sK26)) ),
inference(resolution,[status(thm)],[c_11121,c_10632]) ).
tcf(c_11384,plain,
( sP1(sK24)
| p1(sK17(sK26))
| p1(sK5(sK26)) ),
inference(resolution,[status(thm)],[c_11374,c_93]) ).
tcf(c_11452,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( sP1(sK24)
| p1(X7)
| p1(sK5(sK26))
| ~ r1(sK26,X6)
| ~ r1(sK13,X0)
| ~ r1(X5,sK26)
| ~ r1(X6,X7)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_80,c_11384]) ).
tcf(c_11471,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( sP1(sK24)
| p1(X0)
| p1(sK5(sK26))
| ~ r1(sK13,X1)
| ~ r1(X6,sK26)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(sK4(sK26),X0) ),
inference(resolution,[status(thm)],[c_11452,c_11110]) ).
tcf(c_11605,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( sP1(sK24)
| p1(sK5(sK26))
| ~ r1(sK13,X0)
| ~ r1(X5,sK26)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_11471,c_10632]) ).
tcf(c_11697,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( sP1(sK24)
| p1(sK5(sK26))
| ~ r1(sK19,X0)
| ~ r1(X4,sK26)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_11605,c_84]) ).
tcf(c_11715,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP1(sK24)
| p1(sK5(sK26))
| ~ r1(sK20,X0)
| ~ r1(X3,sK26)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_11697,c_85]) ).
tcf(c_11743,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(sK24)
| p1(sK5(sK26))
| ~ r1(sK21,X0)
| ~ r1(X2,sK26)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_11715,c_86]) ).
tcf(c_11820,plain,
! [X0: $i,X1: $i] :
( sP1(sK24)
| p1(sK5(sK26))
| ~ r1(sK22,X0)
| ~ r1(X1,sK26)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_11743,c_87]) ).
tcf(c_11845,plain,
! [X0: $i] :
( sP1(sK24)
| p1(sK5(sK26))
| ~ r1(sK23,X0)
| ~ r1(X0,sK26) ),
inference(resolution,[status(thm)],[c_11820,c_88]) ).
tcf(c_11854,plain,
( sP1(sK24)
| p1(sK5(sK26))
| ~ r1(sK24,sK26) ),
inference(resolution,[status(thm)],[c_11845,c_89]) ).
tcf(c_11855,plain,
( sP1(sK24)
| p1(sK5(sK26))
| ~ r1(sK29(sK23),sK26) ),
inference(resolution,[status(thm)],[c_11845,c_4568]) ).
tcf(c_11859,plain,
( sP1(sK24)
| p1(sK5(sK26)) ),
inference(global_subsumption_just,[status(thm)],[c_11855,c_92,c_11854]) ).
tcf(c_11865,plain,
! [X0: $i,X1: $i] :
( sP1(sK24)
| sP1(X0)
| p1(X1)
| ~ sP3(X0)
| ~ p1(X0)
| ~ r1(X0,sK26)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_52,c_11859]) ).
tcf(c_11933,plain,
! [X0: $i] :
( sP1(sK24)
| p1(X0)
| ~ sP3(sK24)
| ~ p1(sK24)
| ~ r1(sK24,X0) ),
inference(resolution,[status(thm)],[c_11865,c_92]) ).
tcf(c_11944,plain,
! [X0: $i] :
( sP1(sK24)
| p1(X0)
| ~ r1(sK24,X0) ),
inference(global_subsumption_just,[status(thm)],[c_11933,c_92,c_9760,c_10356,c_11933]) ).
tcf(c_11953,plain,
( sP1(sK24)
| p1(sK25) ),
inference(resolution,[status(thm)],[c_11944,c_90]) ).
tcf(c_11961,plain,
sP1(sK24),
inference(global_subsumption_just,[status(thm)],[c_11953,c_91,c_11953]) ).
tcf(c_11963,plain,
r1(sK8(sK24),sK9(sK24)),
inference(resolution,[status(thm)],[c_61,c_11961]) ).
tcf(c_12061,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| p1(sK9(sK24))
| ~ sP1(sK24)
| ~ p1(X0)
| ~ r1(X0,X1)
| ~ r1(sK9(sK24),X0) ),
inference(resolution,[status(thm)],[c_66,c_11963]) ).
tcf(c_12062,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| p1(sK9(sK24))
| ~ r1(sK9(sK24),X0)
| ~ r1(X0,X1)
| ~ p1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_12061,c_91,c_11953,c_12061]) ).
tcf(c_12063,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| p1(sK9(sK24))
| ~ p1(X0)
| ~ r1(X0,X1)
| ~ r1(sK9(sK24),X0) ),
inference(renaming,[status(thm)],[c_12062]) ).
tcf(c_12064,plain,
r1(sK24,sK8(sK24)),
inference(resolution,[status(thm)],[c_60,c_11961]) ).
fof(f8,definition,
! [X39] :
( ~ sP0(X39)
| ! [X59] :
( ! [X60] :
( ? [X61] :
( p1(X61)
& ? [X62] :
( ~ p1(X62)
& r1(X61,X62) )
& r1(X60,X61) )
| p1(X60)
| ~ r1(X59,X60) )
| ~ r1(X39,X59) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f9,definition,
! [X39] :
( ~ sP1(X39)
| ? [X44] :
( ! [X46] :
( ( p1(X46)
& ? [X49] :
( ~ p1(X49)
& r1(X46,X49) ) )
| ! [X47] :
( ~ p1(X47)
| ! [X48] :
( p1(X48)
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X44,X46) )
& p1(X44)
& ? [X45] :
( ~ p1(X45)
& r1(X44,X45) )
& r1(X39,X44) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f10,definition,
! [X39] :
( ~ sP2(X39)
| ? [X52] :
( ! [X53] :
( ~ p1(X53)
| ! [X54] :
( p1(X54)
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
& ~ p1(X52)
& r1(X39,X52) )
| ! [X50] :
( ? [X51] :
( ~ p1(X51)
& r1(X50,X51) )
| ~ r1(X39,X50) )
| p1(X39) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f11,definition,
! [X39] :
( ~ sP3(X39)
| sP1(X39)
| ! [X41] :
( ? [X42] :
( p1(X42)
& ? [X43] :
( ~ p1(X43)
& r1(X42,X43) )
& r1(X41,X42) )
| ~ r1(X39,X41) )
| ~ p1(X39)
| ! [X40] :
( p1(X40)
| ~ r1(X39,X40) ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f12,plain,
? [X0] :
( ! [X104] :
( ? [X107] :
( ~ p1(X107)
& r1(X104,X107) )
| ! [X105] :
( ! [X106] :
( p1(X106)
| ~ r1(X105,X106) )
| ~ r1(X104,X105) )
| ~ r1(X0,X104) )
& ! [X99] :
( ! [X100] :
( ? [X103] :
( ~ p1(X103)
& r1(X100,X103) )
| ! [X101] :
( ! [X102] :
( p1(X102)
| ~ r1(X101,X102) )
| ~ r1(X100,X101) )
| ~ r1(X99,X100) )
| ~ r1(X0,X99) )
& ! [X93] :
( ! [X94] :
( ! [X95] :
( ? [X98] :
( ~ p1(X98)
& r1(X95,X98) )
| ! [X96] :
( ! [X97] :
( p1(X97)
| ~ r1(X96,X97) )
| ~ r1(X95,X96) )
| ~ r1(X94,X95) )
| ~ r1(X93,X94) )
| ~ r1(X0,X93) )
& ! [X86] :
( ! [X87] :
( ! [X88] :
( ! [X89] :
( ? [X92] :
( ~ p1(X92)
& r1(X89,X92) )
| ! [X90] :
( ! [X91] :
( p1(X91)
| ~ r1(X90,X91) )
| ~ r1(X89,X90) )
| ~ r1(X88,X89) )
| ~ r1(X87,X88) )
| ~ r1(X86,X87) )
| ~ r1(X0,X86) )
& ! [X78] :
( ! [X79] :
( ! [X80] :
( ! [X81] :
( ! [X82] :
( ? [X85] :
( ~ p1(X85)
& r1(X82,X85) )
| ! [X83] :
( ! [X84] :
( p1(X84)
| ~ r1(X83,X84) )
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
| ~ r1(X80,X81) )
| ~ r1(X79,X80) )
| ~ r1(X78,X79) )
| ~ r1(X0,X78) )
& ? [X66] :
( ? [X67] :
( ? [X68] :
( ? [X69] :
( ? [X70] :
( ? [X71] :
( ! [X75] :
( ? [X76] :
( p1(X76)
& ? [X77] :
( ~ p1(X77)
& r1(X76,X77) )
& r1(X75,X76) )
| p1(X75)
| ~ r1(X71,X75) )
& ? [X73] :
( ! [X74] :
( p1(X74)
| ~ r1(X73,X74) )
& r1(X71,X73) )
& ? [X72] :
( ~ p1(X72)
& r1(X71,X72) )
& r1(X70,X71) )
& r1(X69,X70) )
& r1(X68,X69) )
& r1(X67,X68) )
& r1(X66,X67) )
& r1(X0,X66) )
& ! [X34] :
( ! [X35] :
( ! [X36] :
( ! [X37] :
( ! [X38] :
( ! [X39] :
( ( ( ? [X63] :
( ! [X64] :
( ~ p1(X64)
| ! [X65] :
( p1(X65)
| ~ r1(X64,X65) )
| ~ r1(X63,X64) )
& ~ p1(X63)
& r1(X39,X63) )
| sP0(X39) )
& ! [X55] :
( ? [X58] :
( ~ p1(X58)
& r1(X55,X58) )
| ! [X56] :
( ! [X57] :
( p1(X57)
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X39,X55) )
& sP2(X39)
& sP3(X39) )
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(X35,X36) )
| ~ r1(X34,X35) )
| ~ r1(X0,X34) )
& ! [X24] :
( ! [X25] :
( ! [X26] :
( ! [X27] :
( ! [X28] :
( ! [X29] :
( ! [X30] :
( ? [X33] :
( ~ p1(X33)
& r1(X30,X33) )
| ! [X31] :
( ! [X32] :
( p1(X32)
| ~ r1(X31,X32) )
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
| ~ r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X0,X24) )
& ! [X13] :
( ! [X14] :
( ! [X15] :
( ! [X16] :
( ! [X17] :
( ! [X18] :
( ! [X19] :
( ! [X20] :
( ? [X23] :
( ~ p1(X23)
& r1(X20,X23) )
| ! [X21] :
( ! [X22] :
( p1(X22)
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X14,X15) )
| ~ r1(X13,X14) )
| ~ r1(X0,X13) )
& ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ? [X12] :
( ~ p1(X12)
& r1(X9,X12) )
| ! [X10] :
( ! [X11] :
( p1(X11)
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(definition_folding,[],[f7,f11,f10,f9,f8]) ).
fof(f22,plain,
! [X39] :
( ~ sP0(X39)
| ! [X59] :
( ! [X60] :
( ? [X61] :
( p1(X61)
& ? [X62] :
( ~ p1(X62)
& r1(X61,X62) )
& r1(X60,X61) )
| p1(X60)
| ~ r1(X59,X60) )
| ~ r1(X39,X59) ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f23,plain,
! [X0] :
( ~ sP0(X0)
| ! [X1] :
( ! [X2] :
( ? [X3] :
( p1(X3)
& ? [X4] :
( ~ p1(X4)
& r1(X3,X4) )
& r1(X2,X3) )
| p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f22]) ).
fof(f24,plain,
! [X0] :
( ~ sP0(X0)
| ! [X1] :
( ! [X2] :
( ( p1(sK11(X2))
& ~ p1(sK12(X2))
& r1(sK11(X2),sK12(X2))
& r1(X2,sK11(X2)) )
| p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12]),skolemize(X3,sK11(X2)),skolemize(X4,sK12(X2))],[f23]) ).
fof(f45,plain,
! [X2,X0,X1] :
( ~ sP0(X0)
| p1(sK11(X2))
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f24]) ).
fof(f46,plain,
! [X2,X0,X1] :
( ~ sP0(X0)
| ~ p1(sK12(X2))
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f24]) ).
fof(f47,plain,
! [X2,X0,X1] :
( ~ sP0(X0)
| r1(sK11(X2),sK12(X2))
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f24]) ).
fof(f48,plain,
! [X2,X0,X1] :
( ~ sP0(X0)
| r1(X2,sK11(X2))
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X2)
| r1(X2,sK11(X2))
| ~ sP0(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X2)
| r1(sK11(X2),sK12(X2))
| ~ sP0(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X2)
| ~ sP0(X0)
| ~ p1(sK12(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X2)
| p1(sK11(X2))
| ~ sP0(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_11969,plain,
! [X0: $i] :
( p1(sK9(sK24))
| r1(sK11(sK9(sK24)),sK12(sK9(sK24)))
| ~ sP0(X0)
| ~ r1(X0,sK8(sK24)) ),
inference(resolution,[status(thm)],[c_11963,c_68]) ).
tcf(c_11970,plain,
! [X0: $i] :
( p1(sK9(sK24))
| r1(sK9(sK24),sK11(sK9(sK24)))
| ~ sP0(X0)
| ~ r1(X0,sK8(sK24)) ),
inference(resolution,[status(thm)],[c_11963,c_67]) ).
tcf(c_11971,plain,
! [X0: $i] :
( p1(sK9(sK24))
| p1(sK11(sK9(sK24)))
| ~ sP0(X0)
| ~ r1(X0,sK8(sK24)) ),
inference(resolution,[status(thm)],[c_11963,c_70]) ).
tcf(c_12166,plain,
( p1(sK9(sK24))
| r1(sK11(sK9(sK24)),sK12(sK9(sK24)))
| ~ sP0(sK24) ),
inference(resolution,[status(thm)],[c_11969,c_12064]) ).
tcf(c_12171,plain,
( p1(sK9(sK24))
| r1(sK11(sK9(sK24)),sK12(sK9(sK24))) ),
inference(global_subsumption_just,[status(thm)],[c_12166,c_89,c_5583,c_12166]) ).
tcf(c_12178,plain,
! [X0: $i] :
( p1(X0)
| p1(sK9(sK24))
| sP1(sK11(sK9(sK24)))
| r1(sK4(sK12(sK9(sK24))),sK5(sK12(sK9(sK24))))
| ~ sP3(sK11(sK9(sK24)))
| ~ p1(sK11(sK9(sK24)))
| ~ r1(sK11(sK9(sK24)),X0) ),
inference(resolution,[status(thm)],[c_12171,c_51]) ).
tcf(c_12312,plain,
( p1(sK9(sK24))
| r1(sK9(sK24),sK11(sK9(sK24)))
| ~ sP0(sK24) ),
inference(resolution,[status(thm)],[c_11970,c_12064]) ).
tcf(c_12313,plain,
( p1(sK9(sK24))
| r1(sK9(sK24),sK11(sK9(sK24))) ),
inference(global_subsumption_just,[status(thm)],[c_12312,c_89,c_5583,c_12312]) ).
tcf(c_12492,plain,
! [X0: $i] :
( p1(X0)
| p1(sK9(sK24))
| ~ p1(sK11(sK9(sK24)))
| ~ r1(sK11(sK9(sK24)),X0) ),
inference(resolution,[status(thm)],[c_12063,c_12313]) ).
tcf(c_12501,plain,
( p1(sK9(sK24))
| p1(sK11(sK9(sK24)))
| ~ sP0(sK24) ),
inference(resolution,[status(thm)],[c_11971,c_12064]) ).
tcf(c_12506,plain,
( p1(sK9(sK24))
| p1(sK11(sK9(sK24))) ),
inference(global_subsumption_just,[status(thm)],[c_12501,c_89,c_5583,c_12501]) ).
tcf(c_12512,plain,
! [X0: $i] :
( p1(X0)
| p1(sK9(sK24))
| ~ r1(sK11(sK9(sK24)),X0) ),
inference(global_subsumption_just,[status(thm)],[c_12178,c_12492,c_12506]) ).
tcf(c_12519,plain,
( p1(sK9(sK24))
| p1(sK12(sK9(sK24))) ),
inference(resolution,[status(thm)],[c_12512,c_12171]) ).
tcf(c_12520,plain,
! [X0: $i,X1: $i] :
( p1(sK9(sK24))
| ~ sP0(X1)
| ~ r1(X1,X0)
| ~ r1(X0,sK9(sK24)) ),
inference(resolution,[status(thm)],[c_69,c_12519]) ).
tcf(c_12526,plain,
! [X0: $i] :
( p1(sK9(sK24))
| ~ sP0(X0)
| ~ r1(X0,sK8(sK24)) ),
inference(resolution,[status(thm)],[c_12520,c_11963]) ).
tcf(c_12532,plain,
( p1(sK9(sK24))
| ~ sP0(sK24) ),
inference(resolution,[status(thm)],[c_12526,c_12064]) ).
tcf(c_12619,plain,
p1(sK9(sK24)),
inference(global_subsumption_just,[status(thm)],[c_12532,c_89,c_5583,c_12532]) ).
tcf(c_12621,plain,
~ sP1(sK24),
inference(resolution,[status(thm)],[c_62,c_12619]) ).
tcf(c_12622,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_12621,c_11953,c_91]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL658+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/5.37 % Computer : n006.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Thu Sep 24 00:02:51 UTC 2026
% 0.11/5.37 % CPUTime :
% 0.11/5.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/5.41 Running first-order theorem proving
% 0.14/5.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/5.42
% 0.14/5.42 % ======== iProver multi-core TPTP/SMT =========
% 0.14/5.42
% 0.14/5.42 % Detected problem language: tptp
% 0.14/5.43 % Proving...
% 37.22/16.35 % SZS status Started for theBenchmark.p
% 37.22/16.35 % SZS status Theorem for theBenchmark.p
% 37.22/16.35
% 37.22/16.35 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 37.22/16.35
% 37.22/16.35 % ------ iProver source info
% 37.22/16.35
% 37.22/16.35 % git: date: 2026-07-19 20:42:38 +0200
% 37.22/16.35 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 37.22/16.35 % git: non_committed_changes: false
% 37.22/16.35
% 37.22/16.35 % ------ Parsing...
% 37.22/16.35 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 37.22/16.35
% 37.22/16.35 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 37.22/16.35
% 37.22/16.35 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 37.22/16.35 % ------ Proving...
% 37.22/16.35 % ------ Problem Properties
% 37.22/16.35
% 37.22/16.35 %
% 37.22/16.35 % clauses 59
% 37.22/16.35 % conjectures 37
% 37.22/16.35 % EPR 13
% 37.22/16.35 % Horn 31
% 37.22/16.35 % unary 10
% 37.22/16.35 % binary 5
% 37.22/16.35 % lits 342
% 37.22/16.35 % lits eq 0
% 37.22/16.35 % fd_pure 0
% 37.22/16.35 % fd_pseudo 0
% 37.22/16.35 % fd_cond 0
% 37.22/16.35 % fd_pseudo_cond 0
% 37.22/16.35 % AC symbols 0
% 37.22/16.35
% 37.22/16.35 % ------ Input Options Time Limit: Unbounded
% 37.22/16.35
% 37.22/16.35
% 37.22/16.35 % ------
% 37.22/16.35 % Current options:
% 37.22/16.35 % ------
% 37.22/16.35
% 37.22/16.35
% 37.22/16.35 %
% 37.22/16.35
% 37.22/16.35 % ------ Proving...
% 37.22/16.35 %
% 37.22/16.35
% 37.22/16.35 % SZS status Theorem for theBenchmark.p
% 37.22/16.35
% 37.22/16.35 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 37.22/16.35
% 37.22/16.35
%------------------------------------------------------------------------------