%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN522+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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 : Thu Sep 24 03:19:55 PM UTC 2026
% Result : CounterSatisfiable 0.11s 0.46s
% Output : Saturation 0.11s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ( ( ( ~ c5_1(a139)
& ~ c4_2(a139,a140)
& c1_2(a139,a140)
& c2_2(a139,a140)
& ndr1_1(a139)
& ndr1_0 )
| c3_0
| ! [X21] :
( ndr1_0
=> ( ~ c5_1(X21)
| ~ c4_1(X21)
| ! [X22] :
( ndr1_1(X21)
=> ( c3_2(X21,X22)
| c2_2(X21,X22)
| c1_2(X21,X22) ) ) ) ) )
& c4_0
& ( ~ c4_0
| ! [X19] :
( ndr1_0
=> ( ! [X20] :
( ndr1_1(X19)
=> ( c3_2(X19,X20)
| c2_2(X19,X20)
| c5_2(X19,X20) ) )
| c5_1(X19)
| ( ~ c4_2(X19,a138)
& c5_2(X19,a138)
& ndr1_1(X19) ) ) )
| ~ c2_0 )
& ( ~ c4_0
| ~ c3_0
| ( c1_1(a137)
& c4_1(a137)
& ndr1_0 ) )
& ( c4_0
| ( c1_1(a135)
& ~ c1_2(a135,a136)
& ~ c3_2(a135,a136)
& ndr1_1(a135)
& ~ c3_1(a135)
& ndr1_0 )
| ( ~ c2_1(a134)
& ! [X18] :
( ndr1_1(a134)
=> ( ~ c1_2(a134,X18)
| ~ c3_2(a134,X18)
| ~ c2_2(a134,X18) ) )
& ! [X17] :
( ndr1_1(a134)
=> ( c1_2(a134,X17)
| ~ c5_2(a134,X17)
| c4_2(a134,X17) ) )
& ndr1_0 ) )
& ( ( ~ c2_1(a133)
& ~ c5_1(a133)
& ndr1_0 )
| c2_0
| ! [X16] :
( ndr1_0
=> ( ( c1_2(X16,a132)
& c5_2(X16,a132)
& c2_2(X16,a132)
& ndr1_1(X16) )
| c5_1(X16)
| ( ~ c1_2(X16,a131)
& ~ c4_2(X16,a131)
& ndr1_1(X16) ) ) ) )
& ( ( ~ c1_1(a130)
& ! [X15] :
( ndr1_1(a130)
=> ( c2_2(a130,X15)
| c5_2(a130,X15) ) )
& ! [X14] :
( ndr1_1(a130)
=> ( ~ c4_2(a130,X14)
| ~ c2_2(a130,X14)
| ~ c3_2(a130,X14) ) )
& ndr1_0 )
| ( c3_1(a128)
& ~ c2_1(a128)
& c2_2(a128,a129)
& c4_2(a128,a129)
& ~ c1_2(a128,a129)
& ndr1_1(a128)
& ndr1_0 )
| ( ~ c2_2(a125,a127)
& ~ c3_2(a125,a127)
& ~ c4_2(a125,a127)
& ndr1_1(a125)
& ~ c4_1(a125)
& c1_2(a125,a126)
& ~ c5_2(a125,a126)
& ~ c3_2(a125,a126)
& ndr1_1(a125)
& ndr1_0 ) )
& ( ( ~ c1_1(a123)
& c5_1(a123)
& ~ c2_2(a123,a124)
& c1_2(a123,a124)
& ndr1_1(a123)
& ndr1_0 )
| c4_0 )
& ( ( ! [X13] :
( ndr1_1(a121)
=> ( c3_2(a121,X13)
| ~ c1_2(a121,X13)
| ~ c5_2(a121,X13) ) )
& ! [X12] :
( ndr1_1(a121)
=> ( ~ c4_2(a121,X12)
| ~ c1_2(a121,X12)
| c3_2(a121,X12) ) )
& ~ c2_2(a121,a122)
& c3_2(a121,a122)
& ndr1_1(a121)
& ndr1_0 )
| ~ c1_0 )
& ( ! [X11] :
( ndr1_0
=> ( ( ~ c1_2(X11,a120)
& c5_2(X11,a120)
& c2_2(X11,a120)
& ndr1_1(X11) )
| c4_1(X11)
| ( ~ c2_2(X11,a119)
& c4_2(X11,a119)
& ~ c3_2(X11,a119)
& ndr1_1(X11) ) ) )
| c3_0
| ~ c4_0 )
& ( c1_0
| ( ~ c2_1(a118)
& c1_1(a118)
& c5_1(a118)
& ndr1_0 ) )
& ( ~ c1_0
| c3_0
| ~ c5_0 )
& ( ! [X10] :
( ndr1_0
=> ( ~ c4_1(X10)
| c2_1(X10) ) )
| ! [X9] :
( ndr1_0
=> ( ( c3_2(X9,a117)
& ~ c5_2(X9,a117)
& c4_2(X9,a117)
& ndr1_1(X9) )
| ( c1_2(X9,a116)
& ~ c2_2(X9,a116)
& c5_2(X9,a116)
& ndr1_1(X9) )
| ( ~ c4_2(X9,a115)
& c5_2(X9,a115)
& c2_2(X9,a115)
& ndr1_1(X9) ) ) )
| ~ c3_0 )
& ( ( ! [X8] :
( ndr1_1(a114)
=> ( c4_2(a114,X8)
| c5_2(a114,X8)
| c1_2(a114,X8) ) )
& ! [X7] :
( ndr1_1(a114)
=> ( c5_2(a114,X7)
| ~ c3_2(a114,X7) ) )
& ~ c1_1(a114)
& ndr1_0 )
| c2_0 )
& ( ! [X5] :
( ndr1_0
=> ( ! [X6] :
( ndr1_1(X5)
=> ( c5_2(X5,X6)
| c4_2(X5,X6) ) )
| ~ c4_1(X5)
| ~ c3_1(X5) ) )
| c5_0
| ~ c1_0 )
& ( ( ~ c3_2(a112,a113)
& ~ c5_2(a112,a113)
& c2_2(a112,a113)
& ndr1_1(a112)
& ! [X4] :
( ndr1_1(a112)
=> ( c5_2(a112,X4)
| c1_2(a112,X4) ) )
& ! [X3] :
( ndr1_1(a112)
=> ( c1_2(a112,X3)
| c5_2(a112,X3) ) )
& ndr1_0 )
| ~ c1_0
| ! [X1] :
( ndr1_0
=> ( ~ c4_1(X1)
| ! [X2] :
( ndr1_1(X1)
=> ( ~ c2_2(X1,X2)
| c4_2(X1,X2)
| c1_2(X1,X2) ) )
| ( c2_2(X1,a111)
& ~ c3_2(X1,a111)
& c5_2(X1,a111)
& ndr1_1(X1) ) ) ) )
& ( ! [Y] :
( ndr1_0
=> ( ~ c3_1(Y)
| ! [Z] :
( ndr1_1(Y)
=> ( ~ c3_2(Y,Z)
| ~ c1_2(Y,Z)
| ~ c5_2(Y,Z) ) )
| ~ c5_1(Y) ) )
| ( ! [X] :
( ndr1_1(a110)
=> ( c5_2(a110,X)
| c1_2(a110,X) ) )
& ~ c3_1(a110)
& ~ c4_1(a110)
& ndr1_0 )
| ( c3_1(a109)
& ~ c1_1(a109)
& ndr1_0 ) )
& ( ( ! [W] :
( ndr1_1(a108)
=> ( c1_2(a108,W)
| c2_2(a108,W)
| c4_2(a108,W) ) )
& ~ c4_1(a108)
& c3_1(a108)
& ndr1_0 )
| ( c2_2(a106,a107)
& c4_2(a106,a107)
& c1_2(a106,a107)
& ndr1_1(a106)
& ~ c5_1(a106)
& ndr1_0 )
| ! [U] :
( ndr1_0
=> ( ( c2_2(U,a105)
& ~ c3_2(U,a105)
& ~ c4_2(U,a105)
& ndr1_1(U) )
| ( ~ c1_2(U,a104)
& c3_2(U,a104)
& c4_2(U,a104)
& ndr1_1(U) )
| ! [V] :
( ndr1_1(U)
=> ( c3_2(U,V)
| ~ c5_2(U,V)
| c2_2(U,V) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ~ ( ( ( ~ c5_1(a139)
& ~ c4_2(a139,a140)
& c1_2(a139,a140)
& c2_2(a139,a140)
& ndr1_1(a139)
& ndr1_0 )
| c3_0
| ! [X21] :
( ndr1_0
=> ( ~ c5_1(X21)
| ~ c4_1(X21)
| ! [X22] :
( ndr1_1(X21)
=> ( c3_2(X21,X22)
| c2_2(X21,X22)
| c1_2(X21,X22) ) ) ) ) )
& c4_0
& ( ~ c4_0
| ! [X19] :
( ndr1_0
=> ( ! [X20] :
( ndr1_1(X19)
=> ( c3_2(X19,X20)
| c2_2(X19,X20)
| c5_2(X19,X20) ) )
| c5_1(X19)
| ( ~ c4_2(X19,a138)
& c5_2(X19,a138)
& ndr1_1(X19) ) ) )
| ~ c2_0 )
& ( ~ c4_0
| ~ c3_0
| ( c1_1(a137)
& c4_1(a137)
& ndr1_0 ) )
& ( c4_0
| ( c1_1(a135)
& ~ c1_2(a135,a136)
& ~ c3_2(a135,a136)
& ndr1_1(a135)
& ~ c3_1(a135)
& ndr1_0 )
| ( ~ c2_1(a134)
& ! [X18] :
( ndr1_1(a134)
=> ( ~ c1_2(a134,X18)
| ~ c3_2(a134,X18)
| ~ c2_2(a134,X18) ) )
& ! [X17] :
( ndr1_1(a134)
=> ( c1_2(a134,X17)
| ~ c5_2(a134,X17)
| c4_2(a134,X17) ) )
& ndr1_0 ) )
& ( ( ~ c2_1(a133)
& ~ c5_1(a133)
& ndr1_0 )
| c2_0
| ! [X16] :
( ndr1_0
=> ( ( c1_2(X16,a132)
& c5_2(X16,a132)
& c2_2(X16,a132)
& ndr1_1(X16) )
| c5_1(X16)
| ( ~ c1_2(X16,a131)
& ~ c4_2(X16,a131)
& ndr1_1(X16) ) ) ) )
& ( ( ~ c1_1(a130)
& ! [X15] :
( ndr1_1(a130)
=> ( c2_2(a130,X15)
| c5_2(a130,X15) ) )
& ! [X14] :
( ndr1_1(a130)
=> ( ~ c4_2(a130,X14)
| ~ c2_2(a130,X14)
| ~ c3_2(a130,X14) ) )
& ndr1_0 )
| ( c3_1(a128)
& ~ c2_1(a128)
& c2_2(a128,a129)
& c4_2(a128,a129)
& ~ c1_2(a128,a129)
& ndr1_1(a128)
& ndr1_0 )
| ( ~ c2_2(a125,a127)
& ~ c3_2(a125,a127)
& ~ c4_2(a125,a127)
& ndr1_1(a125)
& ~ c4_1(a125)
& c1_2(a125,a126)
& ~ c5_2(a125,a126)
& ~ c3_2(a125,a126)
& ndr1_1(a125)
& ndr1_0 ) )
& ( ( ~ c1_1(a123)
& c5_1(a123)
& ~ c2_2(a123,a124)
& c1_2(a123,a124)
& ndr1_1(a123)
& ndr1_0 )
| c4_0 )
& ( ( ! [X13] :
( ndr1_1(a121)
=> ( c3_2(a121,X13)
| ~ c1_2(a121,X13)
| ~ c5_2(a121,X13) ) )
& ! [X12] :
( ndr1_1(a121)
=> ( ~ c4_2(a121,X12)
| ~ c1_2(a121,X12)
| c3_2(a121,X12) ) )
& ~ c2_2(a121,a122)
& c3_2(a121,a122)
& ndr1_1(a121)
& ndr1_0 )
| ~ c1_0 )
& ( ! [X11] :
( ndr1_0
=> ( ( ~ c1_2(X11,a120)
& c5_2(X11,a120)
& c2_2(X11,a120)
& ndr1_1(X11) )
| c4_1(X11)
| ( ~ c2_2(X11,a119)
& c4_2(X11,a119)
& ~ c3_2(X11,a119)
& ndr1_1(X11) ) ) )
| c3_0
| ~ c4_0 )
& ( c1_0
| ( ~ c2_1(a118)
& c1_1(a118)
& c5_1(a118)
& ndr1_0 ) )
& ( ~ c1_0
| c3_0
| ~ c5_0 )
& ( ! [X10] :
( ndr1_0
=> ( ~ c4_1(X10)
| c2_1(X10) ) )
| ! [X9] :
( ndr1_0
=> ( ( c3_2(X9,a117)
& ~ c5_2(X9,a117)
& c4_2(X9,a117)
& ndr1_1(X9) )
| ( c1_2(X9,a116)
& ~ c2_2(X9,a116)
& c5_2(X9,a116)
& ndr1_1(X9) )
| ( ~ c4_2(X9,a115)
& c5_2(X9,a115)
& c2_2(X9,a115)
& ndr1_1(X9) ) ) )
| ~ c3_0 )
& ( ( ! [X8] :
( ndr1_1(a114)
=> ( c4_2(a114,X8)
| c5_2(a114,X8)
| c1_2(a114,X8) ) )
& ! [X7] :
( ndr1_1(a114)
=> ( c5_2(a114,X7)
| ~ c3_2(a114,X7) ) )
& ~ c1_1(a114)
& ndr1_0 )
| c2_0 )
& ( ! [X5] :
( ndr1_0
=> ( ! [X6] :
( ndr1_1(X5)
=> ( c5_2(X5,X6)
| c4_2(X5,X6) ) )
| ~ c4_1(X5)
| ~ c3_1(X5) ) )
| c5_0
| ~ c1_0 )
& ( ( ~ c3_2(a112,a113)
& ~ c5_2(a112,a113)
& c2_2(a112,a113)
& ndr1_1(a112)
& ! [X4] :
( ndr1_1(a112)
=> ( c5_2(a112,X4)
| c1_2(a112,X4) ) )
& ! [X3] :
( ndr1_1(a112)
=> ( c1_2(a112,X3)
| c5_2(a112,X3) ) )
& ndr1_0 )
| ~ c1_0
| ! [X1] :
( ndr1_0
=> ( ~ c4_1(X1)
| ! [X2] :
( ndr1_1(X1)
=> ( ~ c2_2(X1,X2)
| c4_2(X1,X2)
| c1_2(X1,X2) ) )
| ( c2_2(X1,a111)
& ~ c3_2(X1,a111)
& c5_2(X1,a111)
& ndr1_1(X1) ) ) ) )
& ( ! [Y] :
( ndr1_0
=> ( ~ c3_1(Y)
| ! [Z] :
( ndr1_1(Y)
=> ( ~ c3_2(Y,Z)
| ~ c1_2(Y,Z)
| ~ c5_2(Y,Z) ) )
| ~ c5_1(Y) ) )
| ( ! [X] :
( ndr1_1(a110)
=> ( c5_2(a110,X)
| c1_2(a110,X) ) )
& ~ c3_1(a110)
& ~ c4_1(a110)
& ndr1_0 )
| ( c3_1(a109)
& ~ c1_1(a109)
& ndr1_0 ) )
& ( ( ! [W] :
( ndr1_1(a108)
=> ( c1_2(a108,W)
| c2_2(a108,W)
| c4_2(a108,W) ) )
& ~ c4_1(a108)
& c3_1(a108)
& ndr1_0 )
| ( c2_2(a106,a107)
& c4_2(a106,a107)
& c1_2(a106,a107)
& ndr1_1(a106)
& ~ c5_1(a106)
& ndr1_0 )
| ! [U] :
( ndr1_0
=> ( ( c2_2(U,a105)
& ~ c3_2(U,a105)
& ~ c4_2(U,a105)
& ndr1_1(U) )
| ( ~ c1_2(U,a104)
& c3_2(U,a104)
& c4_2(U,a104)
& ndr1_1(U) )
| ! [V] :
( ndr1_1(U)
=> ( c3_2(U,V)
| ~ c5_2(U,V)
| c2_2(U,V) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( ( ( ~ c5_1(a139)
& ~ c4_2(a139,a140)
& c1_2(a139,a140)
& c2_2(a139,a140)
& ndr1_1(a139)
& ndr1_0 )
| c3_0
| ! [X21] :
( ~ c5_1(X21)
| ~ c4_1(X21)
| ! [X22] :
( c3_2(X21,X22)
| c2_2(X21,X22)
| c1_2(X21,X22)
| ~ ndr1_1(X21) )
| ~ ndr1_0 ) )
& c4_0
& ( ~ c4_0
| ! [X19] :
( ! [X20] :
( c3_2(X19,X20)
| c2_2(X19,X20)
| c5_2(X19,X20)
| ~ ndr1_1(X19) )
| c5_1(X19)
| ( ~ c4_2(X19,a138)
& c5_2(X19,a138)
& ndr1_1(X19) )
| ~ ndr1_0 )
| ~ c2_0 )
& ( ~ c4_0
| ~ c3_0
| ( c1_1(a137)
& c4_1(a137)
& ndr1_0 ) )
& ( c4_0
| ( c1_1(a135)
& ~ c1_2(a135,a136)
& ~ c3_2(a135,a136)
& ndr1_1(a135)
& ~ c3_1(a135)
& ndr1_0 )
| ( ~ c2_1(a134)
& ! [X18] :
( ~ c1_2(a134,X18)
| ~ c3_2(a134,X18)
| ~ c2_2(a134,X18)
| ~ ndr1_1(a134) )
& ! [X17] :
( c1_2(a134,X17)
| ~ c5_2(a134,X17)
| c4_2(a134,X17)
| ~ ndr1_1(a134) )
& ndr1_0 ) )
& ( ( ~ c2_1(a133)
& ~ c5_1(a133)
& ndr1_0 )
| c2_0
| ! [X16] :
( ( c1_2(X16,a132)
& c5_2(X16,a132)
& c2_2(X16,a132)
& ndr1_1(X16) )
| c5_1(X16)
| ( ~ c1_2(X16,a131)
& ~ c4_2(X16,a131)
& ndr1_1(X16) )
| ~ ndr1_0 ) )
& ( ( ~ c1_1(a130)
& ! [X15] :
( c2_2(a130,X15)
| c5_2(a130,X15)
| ~ ndr1_1(a130) )
& ! [X14] :
( ~ c4_2(a130,X14)
| ~ c2_2(a130,X14)
| ~ c3_2(a130,X14)
| ~ ndr1_1(a130) )
& ndr1_0 )
| ( c3_1(a128)
& ~ c2_1(a128)
& c2_2(a128,a129)
& c4_2(a128,a129)
& ~ c1_2(a128,a129)
& ndr1_1(a128)
& ndr1_0 )
| ( ~ c2_2(a125,a127)
& ~ c3_2(a125,a127)
& ~ c4_2(a125,a127)
& ndr1_1(a125)
& ~ c4_1(a125)
& c1_2(a125,a126)
& ~ c5_2(a125,a126)
& ~ c3_2(a125,a126)
& ndr1_1(a125)
& ndr1_0 ) )
& ( ( ~ c1_1(a123)
& c5_1(a123)
& ~ c2_2(a123,a124)
& c1_2(a123,a124)
& ndr1_1(a123)
& ndr1_0 )
| c4_0 )
& ( ( ! [X13] :
( c3_2(a121,X13)
| ~ c1_2(a121,X13)
| ~ c5_2(a121,X13)
| ~ ndr1_1(a121) )
& ! [X12] :
( ~ c4_2(a121,X12)
| ~ c1_2(a121,X12)
| c3_2(a121,X12)
| ~ ndr1_1(a121) )
& ~ c2_2(a121,a122)
& c3_2(a121,a122)
& ndr1_1(a121)
& ndr1_0 )
| ~ c1_0 )
& ( ! [X11] :
( ( ~ c1_2(X11,a120)
& c5_2(X11,a120)
& c2_2(X11,a120)
& ndr1_1(X11) )
| c4_1(X11)
| ( ~ c2_2(X11,a119)
& c4_2(X11,a119)
& ~ c3_2(X11,a119)
& ndr1_1(X11) )
| ~ ndr1_0 )
| c3_0
| ~ c4_0 )
& ( c1_0
| ( ~ c2_1(a118)
& c1_1(a118)
& c5_1(a118)
& ndr1_0 ) )
& ( ~ c1_0
| c3_0
| ~ c5_0 )
& ( ! [X10] :
( ~ c4_1(X10)
| c2_1(X10)
| ~ ndr1_0 )
| ! [X9] :
( ( c3_2(X9,a117)
& ~ c5_2(X9,a117)
& c4_2(X9,a117)
& ndr1_1(X9) )
| ( c1_2(X9,a116)
& ~ c2_2(X9,a116)
& c5_2(X9,a116)
& ndr1_1(X9) )
| ( ~ c4_2(X9,a115)
& c5_2(X9,a115)
& c2_2(X9,a115)
& ndr1_1(X9) )
| ~ ndr1_0 )
| ~ c3_0 )
& ( ( ! [X8] :
( c4_2(a114,X8)
| c5_2(a114,X8)
| c1_2(a114,X8)
| ~ ndr1_1(a114) )
& ! [X7] :
( c5_2(a114,X7)
| ~ c3_2(a114,X7)
| ~ ndr1_1(a114) )
& ~ c1_1(a114)
& ndr1_0 )
| c2_0 )
& ( ! [X5] :
( ! [X6] :
( c5_2(X5,X6)
| c4_2(X5,X6)
| ~ ndr1_1(X5) )
| ~ c4_1(X5)
| ~ c3_1(X5)
| ~ ndr1_0 )
| c5_0
| ~ c1_0 )
& ( ( ~ c3_2(a112,a113)
& ~ c5_2(a112,a113)
& c2_2(a112,a113)
& ndr1_1(a112)
& ! [X4] :
( c5_2(a112,X4)
| c1_2(a112,X4)
| ~ ndr1_1(a112) )
& ! [X3] :
( c1_2(a112,X3)
| c5_2(a112,X3)
| ~ ndr1_1(a112) )
& ndr1_0 )
| ~ c1_0
| ! [X1] :
( ~ c4_1(X1)
| ! [X2] :
( ~ c2_2(X1,X2)
| c4_2(X1,X2)
| c1_2(X1,X2)
| ~ ndr1_1(X1) )
| ( c2_2(X1,a111)
& ~ c3_2(X1,a111)
& c5_2(X1,a111)
& ndr1_1(X1) )
| ~ ndr1_0 ) )
& ( ! [Y] :
( ~ c3_1(Y)
| ! [Z] :
( ~ c3_2(Y,Z)
| ~ c1_2(Y,Z)
| ~ c5_2(Y,Z)
| ~ ndr1_1(Y) )
| ~ c5_1(Y)
| ~ ndr1_0 )
| ( ! [X] :
( c5_2(a110,X)
| c1_2(a110,X)
| ~ ndr1_1(a110) )
& ~ c3_1(a110)
& ~ c4_1(a110)
& ndr1_0 )
| ( c3_1(a109)
& ~ c1_1(a109)
& ndr1_0 ) )
& ( ( ! [W] :
( c1_2(a108,W)
| c2_2(a108,W)
| c4_2(a108,W)
| ~ ndr1_1(a108) )
& ~ c4_1(a108)
& c3_1(a108)
& ndr1_0 )
| ( c2_2(a106,a107)
& c4_2(a106,a107)
& c1_2(a106,a107)
& ndr1_1(a106)
& ~ c5_1(a106)
& ndr1_0 )
| ! [U] :
( ( c2_2(U,a105)
& ~ c3_2(U,a105)
& ~ c4_2(U,a105)
& ndr1_1(U) )
| ( ~ c1_2(U,a104)
& c3_2(U,a104)
& c4_2(U,a104)
& ndr1_1(U) )
| ! [V] :
( c3_2(U,V)
| ~ c5_2(U,V)
| c2_2(U,V)
| ~ ndr1_1(U) )
| ~ ndr1_0 ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f4,definition,
! [U] :
( sP0_prd(U)
<=> ( ~ c1_2(U,a104)
& c3_2(U,a104)
& c4_2(U,a104)
& ndr1_1(U) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f5,definition,
! [U] :
( sP1_prd(U)
<=> ( c2_2(U,a105)
& ~ c3_2(U,a105)
& ~ c4_2(U,a105)
& ndr1_1(U) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f6,definition,
( sP2_prd
<=> ( c2_2(a106,a107)
& c4_2(a106,a107)
& c1_2(a106,a107)
& ndr1_1(a106)
& ~ c5_1(a106)
& ndr1_0 ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f7,definition,
( sP3_prd
<=> ( c3_1(a109)
& ~ c1_1(a109)
& ndr1_0 ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f8,definition,
! [X1] :
( sP4_prd(X1)
<=> ( ~ c4_1(X1)
| ! [X2] :
( ~ c2_2(X1,X2)
| c4_2(X1,X2)
| c1_2(X1,X2)
| ~ ndr1_1(X1) )
| ( c2_2(X1,a111)
& ~ c3_2(X1,a111)
& c5_2(X1,a111)
& ndr1_1(X1) ) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f9,definition,
! [X9] :
( sP5_prd(X9)
<=> ( ( c1_2(X9,a116)
& ~ c2_2(X9,a116)
& c5_2(X9,a116)
& ndr1_1(X9) )
| ( ~ c4_2(X9,a115)
& c5_2(X9,a115)
& c2_2(X9,a115)
& ndr1_1(X9) ) ) ),
introduced(definition,[new_symbols(definition,[sP5_prd])],[]) ).
fof(f10,definition,
! [X11] :
( sP6_prd(X11)
<=> ( c4_1(X11)
| ( ~ c2_2(X11,a119)
& c4_2(X11,a119)
& ~ c3_2(X11,a119)
& ndr1_1(X11) ) ) ),
introduced(definition,[new_symbols(definition,[sP6_prd])],[]) ).
fof(f11,definition,
( sP7_prd
<=> ( ( c3_1(a128)
& ~ c2_1(a128)
& c2_2(a128,a129)
& c4_2(a128,a129)
& ~ c1_2(a128,a129)
& ndr1_1(a128)
& ndr1_0 )
| ( ~ c2_2(a125,a127)
& ~ c3_2(a125,a127)
& ~ c4_2(a125,a127)
& ndr1_1(a125)
& ~ c4_1(a125)
& c1_2(a125,a126)
& ~ c5_2(a125,a126)
& ~ c3_2(a125,a126)
& ndr1_1(a125)
& ndr1_0 ) ) ),
introduced(definition,[new_symbols(definition,[sP7_prd])],[]) ).
fof(f12,definition,
! [X16] :
( sP8_prd(X16)
<=> ( ( c1_2(X16,a132)
& c5_2(X16,a132)
& c2_2(X16,a132)
& ndr1_1(X16) )
| c5_1(X16)
| ( ~ c1_2(X16,a131)
& ~ c4_2(X16,a131)
& ndr1_1(X16) ) ) ),
introduced(definition,[new_symbols(definition,[sP8_prd])],[]) ).
fof(f13,definition,
( sP9_prd
<=> ( ~ c2_1(a134)
& ! [X18] :
( ~ c1_2(a134,X18)
| ~ c3_2(a134,X18)
| ~ c2_2(a134,X18)
| ~ ndr1_1(a134) )
& ! [X17] :
( c1_2(a134,X17)
| ~ c5_2(a134,X17)
| c4_2(a134,X17)
| ~ ndr1_1(a134) )
& ndr1_0 ) ),
introduced(definition,[new_symbols(definition,[sP9_prd])],[]) ).
fof(f14,plain,
( ( ( ~ c5_1(a139)
& ~ c4_2(a139,a140)
& c1_2(a139,a140)
& c2_2(a139,a140)
& ndr1_1(a139)
& ndr1_0 )
| c3_0
| ! [X21] :
( ~ c5_1(X21)
| ~ c4_1(X21)
| ! [X22] :
( c3_2(X21,X22)
| c2_2(X21,X22)
| c1_2(X21,X22)
| ~ ndr1_1(X21) )
| ~ ndr1_0 ) )
& c4_0
& ( ~ c4_0
| ! [X19] :
( ! [X20] :
( c3_2(X19,X20)
| c2_2(X19,X20)
| c5_2(X19,X20)
| ~ ndr1_1(X19) )
| c5_1(X19)
| ( ~ c4_2(X19,a138)
& c5_2(X19,a138)
& ndr1_1(X19) )
| ~ ndr1_0 )
| ~ c2_0 )
& ( ~ c4_0
| ~ c3_0
| ( c1_1(a137)
& c4_1(a137)
& ndr1_0 ) )
& ( c4_0
| ( c1_1(a135)
& ~ c1_2(a135,a136)
& ~ c3_2(a135,a136)
& ndr1_1(a135)
& ~ c3_1(a135)
& ndr1_0 )
| sP9_prd )
& ( ( ~ c2_1(a133)
& ~ c5_1(a133)
& ndr1_0 )
| c2_0
| ! [X16] :
( sP8_prd(X16)
| ~ ndr1_0 ) )
& ( ( ~ c1_1(a130)
& ! [X15] :
( c2_2(a130,X15)
| c5_2(a130,X15)
| ~ ndr1_1(a130) )
& ! [X14] :
( ~ c4_2(a130,X14)
| ~ c2_2(a130,X14)
| ~ c3_2(a130,X14)
| ~ ndr1_1(a130) )
& ndr1_0 )
| sP7_prd )
& ( ( ~ c1_1(a123)
& c5_1(a123)
& ~ c2_2(a123,a124)
& c1_2(a123,a124)
& ndr1_1(a123)
& ndr1_0 )
| c4_0 )
& ( ( ! [X13] :
( c3_2(a121,X13)
| ~ c1_2(a121,X13)
| ~ c5_2(a121,X13)
| ~ ndr1_1(a121) )
& ! [X12] :
( ~ c4_2(a121,X12)
| ~ c1_2(a121,X12)
| c3_2(a121,X12)
| ~ ndr1_1(a121) )
& ~ c2_2(a121,a122)
& c3_2(a121,a122)
& ndr1_1(a121)
& ndr1_0 )
| ~ c1_0 )
& ( ! [X11] :
( ( ~ c1_2(X11,a120)
& c5_2(X11,a120)
& c2_2(X11,a120)
& ndr1_1(X11) )
| sP6_prd(X11)
| ~ ndr1_0 )
| c3_0
| ~ c4_0 )
& ( c1_0
| ( ~ c2_1(a118)
& c1_1(a118)
& c5_1(a118)
& ndr1_0 ) )
& ( ~ c1_0
| c3_0
| ~ c5_0 )
& ( ! [X10] :
( ~ c4_1(X10)
| c2_1(X10)
| ~ ndr1_0 )
| ! [X9] :
( ( c3_2(X9,a117)
& ~ c5_2(X9,a117)
& c4_2(X9,a117)
& ndr1_1(X9) )
| sP5_prd(X9)
| ~ ndr1_0 )
| ~ c3_0 )
& ( ( ! [X8] :
( c4_2(a114,X8)
| c5_2(a114,X8)
| c1_2(a114,X8)
| ~ ndr1_1(a114) )
& ! [X7] :
( c5_2(a114,X7)
| ~ c3_2(a114,X7)
| ~ ndr1_1(a114) )
& ~ c1_1(a114)
& ndr1_0 )
| c2_0 )
& ( ! [X5] :
( ! [X6] :
( c5_2(X5,X6)
| c4_2(X5,X6)
| ~ ndr1_1(X5) )
| ~ c4_1(X5)
| ~ c3_1(X5)
| ~ ndr1_0 )
| c5_0
| ~ c1_0 )
& ( ( ~ c3_2(a112,a113)
& ~ c5_2(a112,a113)
& c2_2(a112,a113)
& ndr1_1(a112)
& ! [X4] :
( c5_2(a112,X4)
| c1_2(a112,X4)
| ~ ndr1_1(a112) )
& ! [X3] :
( c1_2(a112,X3)
| c5_2(a112,X3)
| ~ ndr1_1(a112) )
& ndr1_0 )
| ~ c1_0
| ! [X1] :
( sP4_prd(X1)
| ~ ndr1_0 ) )
& ( ! [Y] :
( ~ c3_1(Y)
| ! [Z] :
( ~ c3_2(Y,Z)
| ~ c1_2(Y,Z)
| ~ c5_2(Y,Z)
| ~ ndr1_1(Y) )
| ~ c5_1(Y)
| ~ ndr1_0 )
| ( ! [X] :
( c5_2(a110,X)
| c1_2(a110,X)
| ~ ndr1_1(a110) )
& ~ c3_1(a110)
& ~ c4_1(a110)
& ndr1_0 )
| sP3_prd )
& ( ( ! [W] :
( c1_2(a108,W)
| c2_2(a108,W)
| c4_2(a108,W)
| ~ ndr1_1(a108) )
& ~ c4_1(a108)
& c3_1(a108)
& ndr1_0 )
| sP2_prd
| ! [U] :
( sP1_prd(U)
| sP0_prd(U)
| ! [V] :
( c3_2(U,V)
| ~ c5_2(U,V)
| c2_2(U,V)
| ~ ndr1_1(U) )
| ~ ndr1_0 ) ) ),
inference(formula_renaming,[status(thm)],[f3,f13,f12,f11,f10,f9,f8,f7,f6,f5,f4]) ).
fof(f15,plain,
( ( ( ~ c5_1(a139)
& ~ c4_2(a139,a140)
& c1_2(a139,a140)
& c2_2(a139,a140)
& ndr1_1(a139)
& ndr1_0 )
| c3_0
| ! [X21] :
( ~ c5_1(X21)
| ~ c4_1(X21)
| ! [X22] :
( c3_2(X21,X22)
| c2_2(X21,X22)
| c1_2(X21,X22) )
| ~ ndr1_1(X21) )
| ~ ndr1_0 )
& c4_0
& ( ~ c4_0
| ! [X19] :
( ! [X20] :
( c3_2(X19,X20)
| c2_2(X19,X20)
| c5_2(X19,X20) )
| ~ ndr1_1(X19)
| c5_1(X19)
| ( ~ c4_2(X19,a138)
& c5_2(X19,a138)
& ndr1_1(X19) ) )
| ~ ndr1_0
| ~ c2_0 )
& ( ~ c4_0
| ~ c3_0
| ( c1_1(a137)
& c4_1(a137)
& ndr1_0 ) )
& ( c4_0
| ( c1_1(a135)
& ~ c1_2(a135,a136)
& ~ c3_2(a135,a136)
& ndr1_1(a135)
& ~ c3_1(a135)
& ndr1_0 )
| sP9_prd )
& ( ( ~ c2_1(a133)
& ~ c5_1(a133)
& ndr1_0 )
| c2_0
| ! [X16] : sP8_prd(X16)
| ~ ndr1_0 )
& ( ( ~ c1_1(a130)
& ( ! [X15] :
( c2_2(a130,X15)
| c5_2(a130,X15) )
| ~ ndr1_1(a130) )
& ( ! [X14] :
( ~ c4_2(a130,X14)
| ~ c2_2(a130,X14)
| ~ c3_2(a130,X14) )
| ~ ndr1_1(a130) )
& ndr1_0 )
| sP7_prd )
& ( ( ~ c1_1(a123)
& c5_1(a123)
& ~ c2_2(a123,a124)
& c1_2(a123,a124)
& ndr1_1(a123)
& ndr1_0 )
| c4_0 )
& ( ( ( ! [X13] :
( c3_2(a121,X13)
| ~ c1_2(a121,X13)
| ~ c5_2(a121,X13) )
| ~ ndr1_1(a121) )
& ( ! [X12] :
( ~ c4_2(a121,X12)
| ~ c1_2(a121,X12)
| c3_2(a121,X12) )
| ~ ndr1_1(a121) )
& ~ c2_2(a121,a122)
& c3_2(a121,a122)
& ndr1_1(a121)
& ndr1_0 )
| ~ c1_0 )
& ( ! [X11] :
( ( ~ c1_2(X11,a120)
& c5_2(X11,a120)
& c2_2(X11,a120)
& ndr1_1(X11) )
| sP6_prd(X11) )
| ~ ndr1_0
| c3_0
| ~ c4_0 )
& ( c1_0
| ( ~ c2_1(a118)
& c1_1(a118)
& c5_1(a118)
& ndr1_0 ) )
& ( ~ c1_0
| c3_0
| ~ c5_0 )
& ( ! [X10] :
( ~ c4_1(X10)
| c2_1(X10) )
| ~ ndr1_0
| ! [X9] :
( ( c3_2(X9,a117)
& ~ c5_2(X9,a117)
& c4_2(X9,a117)
& ndr1_1(X9) )
| sP5_prd(X9) )
| ~ ndr1_0
| ~ c3_0 )
& ( ( ( ! [X8] :
( c4_2(a114,X8)
| c5_2(a114,X8)
| c1_2(a114,X8) )
| ~ ndr1_1(a114) )
& ( ! [X7] :
( c5_2(a114,X7)
| ~ c3_2(a114,X7) )
| ~ ndr1_1(a114) )
& ~ c1_1(a114)
& ndr1_0 )
| c2_0 )
& ( ! [X5] :
( ! [X6] :
( c5_2(X5,X6)
| c4_2(X5,X6) )
| ~ ndr1_1(X5)
| ~ c4_1(X5)
| ~ c3_1(X5) )
| ~ ndr1_0
| c5_0
| ~ c1_0 )
& ( ( ~ c3_2(a112,a113)
& ~ c5_2(a112,a113)
& c2_2(a112,a113)
& ndr1_1(a112)
& ( ! [X4] :
( c5_2(a112,X4)
| c1_2(a112,X4) )
| ~ ndr1_1(a112) )
& ( ! [X3] :
( c1_2(a112,X3)
| c5_2(a112,X3) )
| ~ ndr1_1(a112) )
& ndr1_0 )
| ~ c1_0
| ! [X1] : sP4_prd(X1)
| ~ ndr1_0 )
& ( ! [Y] :
( ~ c3_1(Y)
| ! [Z] :
( ~ c3_2(Y,Z)
| ~ c1_2(Y,Z)
| ~ c5_2(Y,Z) )
| ~ ndr1_1(Y)
| ~ c5_1(Y) )
| ~ ndr1_0
| ( ( ! [X] :
( c5_2(a110,X)
| c1_2(a110,X) )
| ~ ndr1_1(a110) )
& ~ c3_1(a110)
& ~ c4_1(a110)
& ndr1_0 )
| sP3_prd )
& ( ( ( ! [W] :
( c1_2(a108,W)
| c2_2(a108,W)
| c4_2(a108,W) )
| ~ ndr1_1(a108) )
& ~ c4_1(a108)
& c3_1(a108)
& ndr1_0 )
| sP2_prd
| ! [U] :
( sP1_prd(U)
| sP0_prd(U)
| ! [V] :
( c3_2(U,V)
| ~ c5_2(U,V)
| c2_2(U,V) )
| ~ ndr1_1(U) )
| ~ ndr1_0 ) ),
inference(miniscoping,[status(thm)],[f14]) ).
fof(f17,plain,
! [X0,X1] :
( c3_1(a108)
| sP2_prd
| sP1_prd(X0)
| sP0_prd(X0)
| c3_2(X0,X1)
| ~ c5_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f18,plain,
! [X0,X1] :
( ~ c4_1(a108)
| sP2_prd
| sP1_prd(X0)
| sP0_prd(X0)
| c3_2(X0,X1)
| ~ c5_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f19,plain,
! [X0,X1,X2] :
( c1_2(a108,X2)
| c2_2(a108,X2)
| c4_2(a108,X2)
| ~ ndr1_1(a108)
| sP2_prd
| sP1_prd(X0)
| sP0_prd(X0)
| c3_2(X0,X1)
| ~ c5_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f21,plain,
! [X0,X1] :
( ~ c3_1(X0)
| ~ c3_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ ndr1_0
| ~ c4_1(a110)
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f22,plain,
! [X0,X1] :
( ~ c3_1(X0)
| ~ c3_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ ndr1_0
| ~ c3_1(a110)
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f23,plain,
! [X0,X1,X2] :
( ~ c3_1(X1)
| ~ c3_2(X1,X2)
| ~ c1_2(X1,X2)
| ~ c5_2(X1,X2)
| ~ ndr1_1(X1)
| ~ c5_1(X1)
| ~ ndr1_0
| c5_2(a110,X0)
| c1_2(a110,X0)
| ~ ndr1_1(a110)
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f25,plain,
! [X0,X1] :
( c1_2(a112,X1)
| c5_2(a112,X1)
| ~ ndr1_1(a112)
| ~ c1_0
| sP4_prd(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f27,plain,
! [X0] :
( ndr1_1(a112)
| ~ c1_0
| sP4_prd(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f28,plain,
! [X0] :
( c2_2(a112,a113)
| ~ c1_0
| sP4_prd(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f29,plain,
! [X0] :
( ~ c5_2(a112,a113)
| ~ c1_0
| sP4_prd(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f30,plain,
! [X0] :
( ~ c3_2(a112,a113)
| ~ c1_0
| sP4_prd(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f31,plain,
! [X0,X1] :
( c5_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c5_0
| ~ c1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f33,plain,
( ~ c1_1(a114)
| c2_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f34,plain,
! [X0] :
( c5_2(a114,X0)
| ~ c3_2(a114,X0)
| ~ ndr1_1(a114)
| c2_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f35,plain,
! [X0] :
( c4_2(a114,X0)
| c5_2(a114,X0)
| c1_2(a114,X0)
| ~ ndr1_1(a114)
| c2_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f36,plain,
! [X0,X1] :
( ~ c4_1(X1)
| c2_1(X1)
| ~ ndr1_0
| ndr1_1(X0)
| sP5_prd(X0)
| ~ ndr1_0
| ~ c3_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f37,plain,
! [X0,X1] :
( ~ c4_1(X1)
| c2_1(X1)
| ~ ndr1_0
| c4_2(X0,a117)
| sP5_prd(X0)
| ~ ndr1_0
| ~ c3_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f38,plain,
! [X0,X1] :
( ~ c4_1(X1)
| c2_1(X1)
| ~ ndr1_0
| ~ c5_2(X0,a117)
| sP5_prd(X0)
| ~ ndr1_0
| ~ c3_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f39,plain,
! [X0,X1] :
( ~ c4_1(X1)
| c2_1(X1)
| ~ ndr1_0
| c3_2(X0,a117)
| sP5_prd(X0)
| ~ ndr1_0
| ~ c3_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f40,plain,
( ~ c1_0
| c3_0
| ~ c5_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f41,plain,
( c1_0
| ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f42,plain,
( c1_0
| c5_1(a118) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f43,plain,
( c1_0
| c1_1(a118) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f44,plain,
( c1_0
| ~ c2_1(a118) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f45,plain,
! [X0] :
( ndr1_1(X0)
| sP6_prd(X0)
| ~ ndr1_0
| c3_0
| ~ c4_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f46,plain,
! [X0] :
( c2_2(X0,a120)
| sP6_prd(X0)
| ~ ndr1_0
| c3_0
| ~ c4_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f47,plain,
! [X0] :
( c5_2(X0,a120)
| sP6_prd(X0)
| ~ ndr1_0
| c3_0
| ~ c4_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f48,plain,
! [X0] :
( ~ c1_2(X0,a120)
| sP6_prd(X0)
| ~ ndr1_0
| c3_0
| ~ c4_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f49,plain,
( ndr1_0
| ~ c1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f50,plain,
( ndr1_1(a121)
| ~ c1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f51,plain,
( c3_2(a121,a122)
| ~ c1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f52,plain,
( ~ c2_2(a121,a122)
| ~ c1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f53,plain,
! [X0] :
( ~ c4_2(a121,X0)
| ~ c1_2(a121,X0)
| c3_2(a121,X0)
| ~ ndr1_1(a121)
| ~ c1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f54,plain,
! [X0] :
( c3_2(a121,X0)
| ~ c1_2(a121,X0)
| ~ c5_2(a121,X0)
| ~ ndr1_1(a121)
| ~ c1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f62,plain,
! [X0] :
( ~ c4_2(a130,X0)
| ~ c2_2(a130,X0)
| ~ c3_2(a130,X0)
| ~ ndr1_1(a130)
| sP7_prd ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f63,plain,
! [X0] :
( c2_2(a130,X0)
| c5_2(a130,X0)
| ~ ndr1_1(a130)
| sP7_prd ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f64,plain,
( ~ c1_1(a130)
| sP7_prd ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f66,plain,
! [X0] :
( ~ c5_1(a133)
| c2_0
| sP8_prd(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f67,plain,
! [X0] :
( ~ c2_1(a133)
| c2_0
| sP8_prd(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f75,plain,
( ~ c4_0
| ~ c3_0
| c4_1(a137) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f76,plain,
( ~ c4_0
| ~ c3_0
| c1_1(a137) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f78,plain,
! [X0,X1] :
( ~ c4_0
| c3_2(X0,X1)
| c2_2(X0,X1)
| c5_2(X0,X1)
| ~ ndr1_1(X0)
| c5_1(X0)
| c5_2(X0,a138)
| ~ ndr1_0
| ~ c2_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f79,plain,
! [X0,X1] :
( ~ c4_0
| c3_2(X0,X1)
| c2_2(X0,X1)
| c5_2(X0,X1)
| ~ ndr1_1(X0)
| c5_1(X0)
| ~ c4_2(X0,a138)
| ~ ndr1_0
| ~ c2_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f80,plain,
c4_0,
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f82,plain,
! [X0,X1] :
( ndr1_1(a139)
| c3_0
| ~ c5_1(X0)
| ~ c4_1(X0)
| c3_2(X0,X1)
| c2_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f83,plain,
! [X0,X1] :
( c2_2(a139,a140)
| c3_0
| ~ c5_1(X0)
| ~ c4_1(X0)
| c3_2(X0,X1)
| c2_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f84,plain,
! [X0,X1] :
( c1_2(a139,a140)
| c3_0
| ~ c5_1(X0)
| ~ c4_1(X0)
| c3_2(X0,X1)
| c2_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f85,plain,
! [X0,X1] :
( ~ c4_2(a139,a140)
| c3_0
| ~ c5_1(X0)
| ~ c4_1(X0)
| c3_2(X0,X1)
| c2_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f86,plain,
! [X0,X1] :
( ~ c5_1(a139)
| c3_0
| ~ c5_1(X0)
| ~ c4_1(X0)
| c3_2(X0,X1)
| c2_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f87,plain,
! [U] :
( ( c1_2(U,a104)
| ~ c3_2(U,a104)
| ~ c4_2(U,a104)
| ~ ndr1_1(U)
| sP0_prd(U) )
& ( ( ~ c1_2(U,a104)
& c3_2(U,a104)
& c4_2(U,a104)
& ndr1_1(U) )
| ~ sP0_prd(U) ) ),
inference(NNF_transformation,[status(thm)],[f4]) ).
fof(f88,plain,
( ! [U] :
( c1_2(U,a104)
| ~ c3_2(U,a104)
| ~ c4_2(U,a104)
| ~ ndr1_1(U)
| sP0_prd(U) )
& ! [U] :
( ( ~ c1_2(U,a104)
& c3_2(U,a104)
& c4_2(U,a104)
& ndr1_1(U) )
| ~ sP0_prd(U) ) ),
inference(miniscoping,[status(thm)],[f87]) ).
fof(f89,plain,
! [X0] :
( ndr1_1(X0)
| ~ sP0_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f90,plain,
! [X0] :
( c4_2(X0,a104)
| ~ sP0_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f91,plain,
! [X0] :
( c3_2(X0,a104)
| ~ sP0_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f92,plain,
! [X0] :
( ~ c1_2(X0,a104)
| ~ sP0_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f93,plain,
! [X0] :
( c1_2(X0,a104)
| ~ c3_2(X0,a104)
| ~ c4_2(X0,a104)
| ~ ndr1_1(X0)
| sP0_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f94,plain,
! [U] :
( ( ~ c2_2(U,a105)
| c3_2(U,a105)
| c4_2(U,a105)
| ~ ndr1_1(U)
| sP1_prd(U) )
& ( ( c2_2(U,a105)
& ~ c3_2(U,a105)
& ~ c4_2(U,a105)
& ndr1_1(U) )
| ~ sP1_prd(U) ) ),
inference(NNF_transformation,[status(thm)],[f5]) ).
fof(f95,plain,
( ! [U] :
( ~ c2_2(U,a105)
| c3_2(U,a105)
| c4_2(U,a105)
| ~ ndr1_1(U)
| sP1_prd(U) )
& ! [U] :
( ( c2_2(U,a105)
& ~ c3_2(U,a105)
& ~ c4_2(U,a105)
& ndr1_1(U) )
| ~ sP1_prd(U) ) ),
inference(miniscoping,[status(thm)],[f94]) ).
fof(f96,plain,
! [X0] :
( ndr1_1(X0)
| ~ sP1_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f97,plain,
! [X0] :
( ~ c4_2(X0,a105)
| ~ sP1_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f98,plain,
! [X0] :
( ~ c3_2(X0,a105)
| ~ sP1_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f99,plain,
! [X0] :
( c2_2(X0,a105)
| ~ sP1_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f100,plain,
! [X0] :
( ~ c2_2(X0,a105)
| c3_2(X0,a105)
| c4_2(X0,a105)
| ~ ndr1_1(X0)
| sP1_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f101,plain,
( ( ~ c2_2(a106,a107)
| ~ c4_2(a106,a107)
| ~ c1_2(a106,a107)
| ~ ndr1_1(a106)
| c5_1(a106)
| ~ ndr1_0
| sP2_prd )
& ( ( c2_2(a106,a107)
& c4_2(a106,a107)
& c1_2(a106,a107)
& ndr1_1(a106)
& ~ c5_1(a106)
& ndr1_0 )
| ~ sP2_prd ) ),
inference(NNF_transformation,[status(thm)],[f6]) ).
fof(f103,plain,
( ~ c5_1(a106)
| ~ sP2_prd ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f104,plain,
( ndr1_1(a106)
| ~ sP2_prd ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f105,plain,
( c1_2(a106,a107)
| ~ sP2_prd ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f106,plain,
( c4_2(a106,a107)
| ~ sP2_prd ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f107,plain,
( c2_2(a106,a107)
| ~ sP2_prd ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f108,plain,
( ~ c2_2(a106,a107)
| ~ c4_2(a106,a107)
| ~ c1_2(a106,a107)
| ~ ndr1_1(a106)
| c5_1(a106)
| ~ ndr1_0
| sP2_prd ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f109,plain,
( ( ~ c3_1(a109)
| c1_1(a109)
| ~ ndr1_0
| sP3_prd )
& ( ( c3_1(a109)
& ~ c1_1(a109)
& ndr1_0 )
| ~ sP3_prd ) ),
inference(NNF_transformation,[status(thm)],[f7]) ).
fof(f111,plain,
( ~ c1_1(a109)
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f112,plain,
( c3_1(a109)
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f113,plain,
( ~ c3_1(a109)
| c1_1(a109)
| ~ ndr1_0
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f114,plain,
! [X1] :
( ( ( c4_1(X1)
& ? [X2] :
( c2_2(X1,X2)
& ~ c4_2(X1,X2)
& ~ c1_2(X1,X2)
& ndr1_1(X1) )
& ( ~ c2_2(X1,a111)
| c3_2(X1,a111)
| ~ c5_2(X1,a111)
| ~ ndr1_1(X1) ) )
| sP4_prd(X1) )
& ( ~ c4_1(X1)
| ! [X2] :
( ~ c2_2(X1,X2)
| c4_2(X1,X2)
| c1_2(X1,X2)
| ~ ndr1_1(X1) )
| ( c2_2(X1,a111)
& ~ c3_2(X1,a111)
& c5_2(X1,a111)
& ndr1_1(X1) )
| ~ sP4_prd(X1) ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f115,plain,
( ! [X1] :
( ( c4_1(X1)
& ? [X2] :
( c2_2(X1,X2)
& ~ c4_2(X1,X2)
& ~ c1_2(X1,X2) )
& ndr1_1(X1)
& ( ~ c2_2(X1,a111)
| c3_2(X1,a111)
| ~ c5_2(X1,a111)
| ~ ndr1_1(X1) ) )
| sP4_prd(X1) )
& ! [X1] :
( ~ c4_1(X1)
| ! [X2] :
( ~ c2_2(X1,X2)
| c4_2(X1,X2)
| c1_2(X1,X2) )
| ~ ndr1_1(X1)
| ( c2_2(X1,a111)
& ~ c3_2(X1,a111)
& c5_2(X1,a111)
& ndr1_1(X1) )
| ~ sP4_prd(X1) ) ),
inference(miniscoping,[status(thm)],[f114]) ).
fof(f116,plain,
( ! [X1] :
( ( c4_1(X1)
& c2_2(X1,sK0_skl(X1))
& ~ c4_2(X1,sK0_skl(X1))
& ~ c1_2(X1,sK0_skl(X1))
& ndr1_1(X1)
& ( ~ c2_2(X1,a111)
| c3_2(X1,a111)
| ~ c5_2(X1,a111)
| ~ ndr1_1(X1) ) )
| sP4_prd(X1) )
& ! [X1] :
( ~ c4_1(X1)
| ! [X2] :
( ~ c2_2(X1,X2)
| c4_2(X1,X2)
| c1_2(X1,X2) )
| ~ ndr1_1(X1)
| ( c2_2(X1,a111)
& ~ c3_2(X1,a111)
& c5_2(X1,a111)
& ndr1_1(X1) )
| ~ sP4_prd(X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X2,sK0_skl(X1))],[f115]) ).
fof(f118,plain,
! [X0,X1] :
( ~ c4_1(X0)
| ~ c2_2(X0,X1)
| c4_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| c5_2(X0,a111)
| ~ sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f119,plain,
! [X0,X1] :
( ~ c4_1(X0)
| ~ c2_2(X0,X1)
| c4_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,a111)
| ~ sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f120,plain,
! [X0,X1] :
( ~ c4_1(X0)
| ~ c2_2(X0,X1)
| c4_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| c2_2(X0,a111)
| ~ sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f121,plain,
! [X0] :
( ~ c2_2(X0,a111)
| c3_2(X0,a111)
| ~ c5_2(X0,a111)
| ~ ndr1_1(X0)
| sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f122,plain,
! [X0] :
( ndr1_1(X0)
| sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f123,plain,
! [X0] :
( ~ c1_2(X0,sK0_skl(X0))
| sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f124,plain,
! [X0] :
( ~ c4_2(X0,sK0_skl(X0))
| sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f125,plain,
! [X0] :
( c2_2(X0,sK0_skl(X0))
| sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f126,plain,
! [X0] :
( c4_1(X0)
| sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f127,definition,
! [X9] :
( sP10_prd(X9)
<=> ( ~ c4_2(X9,a115)
& c5_2(X9,a115)
& c2_2(X9,a115)
& ndr1_1(X9) ) ),
introduced(definition,[new_symbols(definition,[sP10_prd])],[]) ).
fof(f128,plain,
! [X9] :
( sP5_prd(X9)
<=> ( ( c1_2(X9,a116)
& ~ c2_2(X9,a116)
& c5_2(X9,a116)
& ndr1_1(X9) )
| sP10_prd(X9) ) ),
inference(formula_renaming,[status(thm)],[f9,f127]) ).
fof(f129,plain,
! [X9] :
( ( ( ( ~ c1_2(X9,a116)
| c2_2(X9,a116)
| ~ c5_2(X9,a116)
| ~ ndr1_1(X9) )
& ~ sP10_prd(X9) )
| sP5_prd(X9) )
& ( ( c1_2(X9,a116)
& ~ c2_2(X9,a116)
& c5_2(X9,a116)
& ndr1_1(X9) )
| sP10_prd(X9)
| ~ sP5_prd(X9) ) ),
inference(NNF_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
( ! [X9] :
( ( ( ~ c1_2(X9,a116)
| c2_2(X9,a116)
| ~ c5_2(X9,a116)
| ~ ndr1_1(X9) )
& ~ sP10_prd(X9) )
| sP5_prd(X9) )
& ! [X9] :
( ( c1_2(X9,a116)
& ~ c2_2(X9,a116)
& c5_2(X9,a116)
& ndr1_1(X9) )
| sP10_prd(X9)
| ~ sP5_prd(X9) ) ),
inference(miniscoping,[status(thm)],[f129]) ).
fof(f131,plain,
! [X0] :
( ndr1_1(X0)
| sP10_prd(X0)
| ~ sP5_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f132,plain,
! [X0] :
( c5_2(X0,a116)
| sP10_prd(X0)
| ~ sP5_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f133,plain,
! [X0] :
( ~ c2_2(X0,a116)
| sP10_prd(X0)
| ~ sP5_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f134,plain,
! [X0] :
( c1_2(X0,a116)
| sP10_prd(X0)
| ~ sP5_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f135,plain,
! [X0] :
( ~ sP10_prd(X0)
| sP5_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f136,plain,
! [X0] :
( ~ c1_2(X0,a116)
| c2_2(X0,a116)
| ~ c5_2(X0,a116)
| ~ ndr1_1(X0)
| sP5_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f137,plain,
! [X11] :
( ( ( ~ c4_1(X11)
& ( c2_2(X11,a119)
| ~ c4_2(X11,a119)
| c3_2(X11,a119)
| ~ ndr1_1(X11) ) )
| sP6_prd(X11) )
& ( c4_1(X11)
| ( ~ c2_2(X11,a119)
& c4_2(X11,a119)
& ~ c3_2(X11,a119)
& ndr1_1(X11) )
| ~ sP6_prd(X11) ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f138,plain,
( ! [X11] :
( ( ~ c4_1(X11)
& ( c2_2(X11,a119)
| ~ c4_2(X11,a119)
| c3_2(X11,a119)
| ~ ndr1_1(X11) ) )
| sP6_prd(X11) )
& ! [X11] :
( c4_1(X11)
| ( ~ c2_2(X11,a119)
& c4_2(X11,a119)
& ~ c3_2(X11,a119)
& ndr1_1(X11) )
| ~ sP6_prd(X11) ) ),
inference(miniscoping,[status(thm)],[f137]) ).
fof(f139,plain,
! [X0] :
( c4_1(X0)
| ndr1_1(X0)
| ~ sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f140,plain,
! [X0] :
( c4_1(X0)
| ~ c3_2(X0,a119)
| ~ sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f141,plain,
! [X0] :
( c4_1(X0)
| c4_2(X0,a119)
| ~ sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f142,plain,
! [X0] :
( c4_1(X0)
| ~ c2_2(X0,a119)
| ~ sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f143,plain,
! [X0] :
( c2_2(X0,a119)
| ~ c4_2(X0,a119)
| c3_2(X0,a119)
| ~ ndr1_1(X0)
| sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f144,plain,
! [X0] :
( ~ c4_1(X0)
| sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f145,definition,
( sP11_prd
<=> ( ~ c2_2(a125,a127)
& ~ c3_2(a125,a127)
& ~ c4_2(a125,a127)
& ndr1_1(a125)
& ~ c4_1(a125)
& c1_2(a125,a126)
& ~ c5_2(a125,a126)
& ~ c3_2(a125,a126)
& ndr1_1(a125)
& ndr1_0 ) ),
introduced(definition,[new_symbols(definition,[sP11_prd])],[]) ).
fof(f146,plain,
( sP7_prd
<=> ( ( c3_1(a128)
& ~ c2_1(a128)
& c2_2(a128,a129)
& c4_2(a128,a129)
& ~ c1_2(a128,a129)
& ndr1_1(a128)
& ndr1_0 )
| sP11_prd ) ),
inference(formula_renaming,[status(thm)],[f11,f145]) ).
fof(f147,plain,
( ( ( ( ~ c3_1(a128)
| c2_1(a128)
| ~ c2_2(a128,a129)
| ~ c4_2(a128,a129)
| c1_2(a128,a129)
| ~ ndr1_1(a128)
| ~ ndr1_0 )
& ~ sP11_prd )
| sP7_prd )
& ( ( c3_1(a128)
& ~ c2_1(a128)
& c2_2(a128,a129)
& c4_2(a128,a129)
& ~ c1_2(a128,a129)
& ndr1_1(a128)
& ndr1_0 )
| sP11_prd
| ~ sP7_prd ) ),
inference(NNF_transformation,[status(thm)],[f146]) ).
fof(f149,plain,
( ndr1_1(a128)
| sP11_prd
| ~ sP7_prd ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f150,plain,
( ~ c1_2(a128,a129)
| sP11_prd
| ~ sP7_prd ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f151,plain,
( c4_2(a128,a129)
| sP11_prd
| ~ sP7_prd ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f152,plain,
( c2_2(a128,a129)
| sP11_prd
| ~ sP7_prd ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f153,plain,
( ~ c2_1(a128)
| sP11_prd
| ~ sP7_prd ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f154,plain,
( c3_1(a128)
| sP11_prd
| ~ sP7_prd ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f155,plain,
( ~ sP11_prd
| sP7_prd ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f156,plain,
( ~ c3_1(a128)
| c2_1(a128)
| ~ c2_2(a128,a129)
| ~ c4_2(a128,a129)
| c1_2(a128,a129)
| ~ ndr1_1(a128)
| ~ ndr1_0
| sP7_prd ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f157,definition,
! [X16] :
( sP12_prd(X16)
<=> ( c5_1(X16)
| ( ~ c1_2(X16,a131)
& ~ c4_2(X16,a131)
& ndr1_1(X16) ) ) ),
introduced(definition,[new_symbols(definition,[sP12_prd])],[]) ).
fof(f158,plain,
! [X16] :
( sP8_prd(X16)
<=> ( ( c1_2(X16,a132)
& c5_2(X16,a132)
& c2_2(X16,a132)
& ndr1_1(X16) )
| sP12_prd(X16) ) ),
inference(formula_renaming,[status(thm)],[f12,f157]) ).
fof(f159,plain,
! [X16] :
( ( ( ( ~ c1_2(X16,a132)
| ~ c5_2(X16,a132)
| ~ c2_2(X16,a132)
| ~ ndr1_1(X16) )
& ~ sP12_prd(X16) )
| sP8_prd(X16) )
& ( ( c1_2(X16,a132)
& c5_2(X16,a132)
& c2_2(X16,a132)
& ndr1_1(X16) )
| sP12_prd(X16)
| ~ sP8_prd(X16) ) ),
inference(NNF_transformation,[status(thm)],[f158]) ).
fof(f160,plain,
( ! [X16] :
( ( ( ~ c1_2(X16,a132)
| ~ c5_2(X16,a132)
| ~ c2_2(X16,a132)
| ~ ndr1_1(X16) )
& ~ sP12_prd(X16) )
| sP8_prd(X16) )
& ! [X16] :
( ( c1_2(X16,a132)
& c5_2(X16,a132)
& c2_2(X16,a132)
& ndr1_1(X16) )
| sP12_prd(X16)
| ~ sP8_prd(X16) ) ),
inference(miniscoping,[status(thm)],[f159]) ).
fof(f161,plain,
! [X0] :
( ndr1_1(X0)
| sP12_prd(X0)
| ~ sP8_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f162,plain,
! [X0] :
( c2_2(X0,a132)
| sP12_prd(X0)
| ~ sP8_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f163,plain,
! [X0] :
( c5_2(X0,a132)
| sP12_prd(X0)
| ~ sP8_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f164,plain,
! [X0] :
( c1_2(X0,a132)
| sP12_prd(X0)
| ~ sP8_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f165,plain,
! [X0] :
( ~ sP12_prd(X0)
| sP8_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f166,plain,
! [X0] :
( ~ c1_2(X0,a132)
| ~ c5_2(X0,a132)
| ~ c2_2(X0,a132)
| ~ ndr1_1(X0)
| sP8_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f167,definition,
! [X17] :
( sP13_prd(X17)
<=> ( c1_2(a134,X17)
| ~ c5_2(a134,X17)
| c4_2(a134,X17) ) ),
introduced(definition,[new_symbols(definition,[sP13_prd])],[]) ).
fof(f168,plain,
( sP9_prd
<=> ( ~ c2_1(a134)
& ! [X18] :
( ~ c1_2(a134,X18)
| ~ c3_2(a134,X18)
| ~ c2_2(a134,X18)
| ~ ndr1_1(a134) )
& ! [X17] :
( sP13_prd(X17)
| ~ ndr1_1(a134) )
& ndr1_0 ) ),
inference(formula_renaming,[status(thm)],[f13,f167]) ).
fof(f169,plain,
( ( c2_1(a134)
| ? [X18] :
( c1_2(a134,X18)
& c3_2(a134,X18)
& c2_2(a134,X18)
& ndr1_1(a134) )
| ? [X17] :
( ~ sP13_prd(X17)
& ndr1_1(a134) )
| ~ ndr1_0
| sP9_prd )
& ( ( ~ c2_1(a134)
& ! [X18] :
( ~ c1_2(a134,X18)
| ~ c3_2(a134,X18)
| ~ c2_2(a134,X18)
| ~ ndr1_1(a134) )
& ! [X17] :
( sP13_prd(X17)
| ~ ndr1_1(a134) )
& ndr1_0 )
| ~ sP9_prd ) ),
inference(NNF_transformation,[status(thm)],[f168]) ).
fof(f170,plain,
( ( c2_1(a134)
| ( ? [X18] :
( c1_2(a134,X18)
& c3_2(a134,X18)
& c2_2(a134,X18) )
& ndr1_1(a134) )
| ( ? [X17] : ~ sP13_prd(X17)
& ndr1_1(a134) )
| ~ ndr1_0
| sP9_prd )
& ( ( ~ c2_1(a134)
& ( ! [X18] :
( ~ c1_2(a134,X18)
| ~ c3_2(a134,X18)
| ~ c2_2(a134,X18) )
| ~ ndr1_1(a134) )
& ( ! [X17] : sP13_prd(X17)
| ~ ndr1_1(a134) )
& ndr1_0 )
| ~ sP9_prd ) ),
inference(miniscoping,[status(thm)],[f169]) ).
fof(f171,plain,
( ( c2_1(a134)
| ( c1_2(a134,sK2_skl)
& c3_2(a134,sK2_skl)
& c2_2(a134,sK2_skl)
& ndr1_1(a134) )
| ( ~ sP13_prd(sK1_skl)
& ndr1_1(a134) )
| ~ ndr1_0
| sP9_prd )
& ( ( ~ c2_1(a134)
& ( ! [X18] :
( ~ c1_2(a134,X18)
| ~ c3_2(a134,X18)
| ~ c2_2(a134,X18) )
| ~ ndr1_1(a134) )
& ( ! [X17] : sP13_prd(X17)
| ~ ndr1_1(a134) )
& ndr1_0 )
| ~ sP9_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(X17,sK1_skl),skolemize(X18,sK2_skl)],[f170]) ).
fof(f173,plain,
! [X0] :
( sP13_prd(X0)
| ~ ndr1_1(a134)
| ~ sP9_prd ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f174,plain,
! [X0] :
( ~ c1_2(a134,X0)
| ~ c3_2(a134,X0)
| ~ c2_2(a134,X0)
| ~ ndr1_1(a134)
| ~ sP9_prd ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f175,plain,
( ~ c2_1(a134)
| ~ sP9_prd ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f176,plain,
( c2_1(a134)
| ndr1_1(a134)
| ndr1_1(a134)
| ~ ndr1_0
| sP9_prd ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f181,plain,
( c2_1(a134)
| c2_2(a134,sK2_skl)
| ~ sP13_prd(sK1_skl)
| ~ ndr1_0
| sP9_prd ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f182,plain,
( c2_1(a134)
| c3_2(a134,sK2_skl)
| ~ sP13_prd(sK1_skl)
| ~ ndr1_0
| sP9_prd ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f183,plain,
( c2_1(a134)
| c1_2(a134,sK2_skl)
| ~ sP13_prd(sK1_skl)
| ~ ndr1_0
| sP9_prd ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f184,plain,
! [X9] :
( ( c4_2(X9,a115)
| ~ c5_2(X9,a115)
| ~ c2_2(X9,a115)
| ~ ndr1_1(X9)
| sP10_prd(X9) )
& ( ( ~ c4_2(X9,a115)
& c5_2(X9,a115)
& c2_2(X9,a115)
& ndr1_1(X9) )
| ~ sP10_prd(X9) ) ),
inference(NNF_transformation,[status(thm)],[f127]) ).
fof(f185,plain,
( ! [X9] :
( c4_2(X9,a115)
| ~ c5_2(X9,a115)
| ~ c2_2(X9,a115)
| ~ ndr1_1(X9)
| sP10_prd(X9) )
& ! [X9] :
( ( ~ c4_2(X9,a115)
& c5_2(X9,a115)
& c2_2(X9,a115)
& ndr1_1(X9) )
| ~ sP10_prd(X9) ) ),
inference(miniscoping,[status(thm)],[f184]) ).
fof(f186,plain,
! [X0] :
( ndr1_1(X0)
| ~ sP10_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f187,plain,
! [X0] :
( c2_2(X0,a115)
| ~ sP10_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f188,plain,
! [X0] :
( c5_2(X0,a115)
| ~ sP10_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f189,plain,
! [X0] :
( ~ c4_2(X0,a115)
| ~ sP10_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f190,plain,
! [X0] :
( c4_2(X0,a115)
| ~ c5_2(X0,a115)
| ~ c2_2(X0,a115)
| ~ ndr1_1(X0)
| sP10_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f191,plain,
( ( c2_2(a125,a127)
| c3_2(a125,a127)
| c4_2(a125,a127)
| ~ ndr1_1(a125)
| c4_1(a125)
| ~ c1_2(a125,a126)
| c5_2(a125,a126)
| c3_2(a125,a126)
| ~ ndr1_1(a125)
| ~ ndr1_0
| sP11_prd )
& ( ( ~ c2_2(a125,a127)
& ~ c3_2(a125,a127)
& ~ c4_2(a125,a127)
& ndr1_1(a125)
& ~ c4_1(a125)
& c1_2(a125,a126)
& ~ c5_2(a125,a126)
& ~ c3_2(a125,a126)
& ndr1_1(a125)
& ndr1_0 )
| ~ sP11_prd ) ),
inference(NNF_transformation,[status(thm)],[f145]) ).
fof(f193,plain,
( ndr1_1(a125)
| ~ sP11_prd ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f194,plain,
( ~ c3_2(a125,a126)
| ~ sP11_prd ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f195,plain,
( ~ c5_2(a125,a126)
| ~ sP11_prd ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f196,plain,
( c1_2(a125,a126)
| ~ sP11_prd ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f197,plain,
( ~ c4_1(a125)
| ~ sP11_prd ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f199,plain,
( ~ c4_2(a125,a127)
| ~ sP11_prd ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f200,plain,
( ~ c3_2(a125,a127)
| ~ sP11_prd ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f201,plain,
( ~ c2_2(a125,a127)
| ~ sP11_prd ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f202,plain,
( c2_2(a125,a127)
| c3_2(a125,a127)
| c4_2(a125,a127)
| ~ ndr1_1(a125)
| c4_1(a125)
| ~ c1_2(a125,a126)
| c5_2(a125,a126)
| c3_2(a125,a126)
| ~ ndr1_1(a125)
| ~ ndr1_0
| sP11_prd ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f203,plain,
! [X16] :
( ( ( ~ c5_1(X16)
& ( c1_2(X16,a131)
| c4_2(X16,a131)
| ~ ndr1_1(X16) ) )
| sP12_prd(X16) )
& ( c5_1(X16)
| ( ~ c1_2(X16,a131)
& ~ c4_2(X16,a131)
& ndr1_1(X16) )
| ~ sP12_prd(X16) ) ),
inference(NNF_transformation,[status(thm)],[f157]) ).
fof(f204,plain,
( ! [X16] :
( ( ~ c5_1(X16)
& ( c1_2(X16,a131)
| c4_2(X16,a131)
| ~ ndr1_1(X16) ) )
| sP12_prd(X16) )
& ! [X16] :
( c5_1(X16)
| ( ~ c1_2(X16,a131)
& ~ c4_2(X16,a131)
& ndr1_1(X16) )
| ~ sP12_prd(X16) ) ),
inference(miniscoping,[status(thm)],[f203]) ).
fof(f205,plain,
! [X0] :
( c5_1(X0)
| ndr1_1(X0)
| ~ sP12_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f206,plain,
! [X0] :
( c5_1(X0)
| ~ c4_2(X0,a131)
| ~ sP12_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f207,plain,
! [X0] :
( c5_1(X0)
| ~ c1_2(X0,a131)
| ~ sP12_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f208,plain,
! [X0] :
( c1_2(X0,a131)
| c4_2(X0,a131)
| ~ ndr1_1(X0)
| sP12_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f209,plain,
! [X0] :
( ~ c5_1(X0)
| sP12_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f210,plain,
! [X17] :
( ( ( ~ c1_2(a134,X17)
& c5_2(a134,X17)
& ~ c4_2(a134,X17) )
| sP13_prd(X17) )
& ( c1_2(a134,X17)
| ~ c5_2(a134,X17)
| c4_2(a134,X17)
| ~ sP13_prd(X17) ) ),
inference(NNF_transformation,[status(thm)],[f167]) ).
fof(f211,plain,
( ! [X17] :
( ( ~ c1_2(a134,X17)
& c5_2(a134,X17)
& ~ c4_2(a134,X17) )
| sP13_prd(X17) )
& ! [X17] :
( c1_2(a134,X17)
| ~ c5_2(a134,X17)
| c4_2(a134,X17)
| ~ sP13_prd(X17) ) ),
inference(miniscoping,[status(thm)],[f210]) ).
fof(f212,plain,
! [X0] :
( c1_2(a134,X0)
| ~ c5_2(a134,X0)
| c4_2(a134,X0)
| ~ sP13_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f213,plain,
! [X0] :
( ~ c4_2(a134,X0)
| sP13_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f214,plain,
! [X0] :
( c5_2(a134,X0)
| sP13_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f215,plain,
! [X0] :
( ~ c1_2(a134,X0)
| sP13_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f216,plain,
! [X0,X1] :
( ~ c4_1(X1)
| c2_1(X1)
| ndr1_1(X0)
| sP5_prd(X0)
| ~ ndr1_0
| ~ c3_0 ),
inference(duplicate_literals_removal,[status(thm)],[f36]) ).
fof(f217,plain,
! [X0,X1] :
( ~ c4_1(X1)
| c2_1(X1)
| c4_2(X0,a117)
| sP5_prd(X0)
| ~ ndr1_0
| ~ c3_0 ),
inference(duplicate_literals_removal,[status(thm)],[f37]) ).
fof(f218,plain,
! [X0,X1] :
( ~ c4_1(X1)
| c2_1(X1)
| ~ c5_2(X0,a117)
| sP5_prd(X0)
| ~ ndr1_0
| ~ c3_0 ),
inference(duplicate_literals_removal,[status(thm)],[f38]) ).
fof(f219,plain,
! [X0,X1] :
( ~ c4_1(X1)
| c2_1(X1)
| c3_2(X0,a117)
| sP5_prd(X0)
| ~ ndr1_0
| ~ c3_0 ),
inference(duplicate_literals_removal,[status(thm)],[f39]) ).
fof(f220,plain,
( c2_1(a134)
| ndr1_1(a134)
| ~ ndr1_0
| sP9_prd ),
inference(duplicate_literals_removal,[status(thm)],[f176]) ).
fof(f221,plain,
( c2_2(a125,a127)
| c3_2(a125,a127)
| c4_2(a125,a127)
| c4_1(a125)
| ~ c1_2(a125,a126)
| c5_2(a125,a126)
| c3_2(a125,a126)
| ~ ndr1_1(a125)
| ~ ndr1_0
| sP11_prd ),
inference(duplicate_literals_removal,[status(thm)],[f202]) ).
fof(f222,plain,
! [X0,X1] :
( c3_1(a108)
| sP2_prd
| sP1_prd(X0)
| sP0_prd(X0)
| c3_2(X0,X1)
| ~ c5_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f17,f223]) ).
fof(f223,plain,
ndr1_0,
inference(forward_subsumption_resolution,[status(thm)],[f49,f41]) ).
fof(f224,plain,
! [X0,X1] :
( ~ c4_1(a108)
| sP2_prd
| sP1_prd(X0)
| sP0_prd(X0)
| c3_2(X0,X1)
| ~ c5_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f18,f223]) ).
fof(f225,plain,
! [X0,X1,X2] :
( c1_2(a108,X2)
| c2_2(a108,X2)
| c4_2(a108,X2)
| ~ ndr1_1(a108)
| sP2_prd
| sP1_prd(X0)
| sP0_prd(X0)
| c3_2(X0,X1)
| ~ c5_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f19,f223]) ).
fof(f226,plain,
! [X0,X1] :
( ~ c3_1(X0)
| ~ c3_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c4_1(a110)
| sP3_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f21,f223]) ).
fof(f227,plain,
! [X0,X1] :
( ~ c3_1(X0)
| ~ c3_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c3_1(a110)
| sP3_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f22,f223]) ).
fof(f228,plain,
! [X0,X1,X2] :
( ~ c3_1(X1)
| ~ c3_2(X1,X2)
| ~ c1_2(X1,X2)
| ~ c5_2(X1,X2)
| ~ ndr1_1(X1)
| ~ c5_1(X1)
| c5_2(a110,X0)
| c1_2(a110,X0)
| ~ ndr1_1(a110)
| sP3_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f23,f223]) ).
fof(f229,plain,
! [X0,X1] :
( c1_2(a112,X1)
| c5_2(a112,X1)
| ~ ndr1_1(a112)
| ~ c1_0
| sP4_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f25,f223]) ).
fof(f230,plain,
! [X0,X1] :
( c1_2(a112,X1)
| c5_2(a112,X1)
| ~ c1_0
| sP4_prd(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f229,f231]) ).
fof(f231,plain,
! [X0] :
( ndr1_1(a112)
| ~ c1_0
| sP4_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f27,f223]) ).
fof(f232,plain,
! [X0] :
( c2_2(a112,a113)
| ~ c1_0
| sP4_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f28,f223]) ).
fof(f233,plain,
! [X0] :
( ~ c5_2(a112,a113)
| ~ c1_0
| sP4_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f29,f223]) ).
fof(f234,plain,
! [X0] :
( ~ c3_2(a112,a113)
| ~ c1_0
| sP4_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f30,f223]) ).
fof(f235,plain,
! [X0,X1] :
( c5_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_1(X0)
| ~ c3_1(X0)
| c5_0
| ~ c1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f31,f223]) ).
fof(f236,plain,
! [X0,X1] :
( ~ c4_1(X1)
| c2_1(X1)
| ndr1_1(X0)
| sP5_prd(X0)
| ~ c3_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f216,f223]) ).
fof(f237,plain,
! [X0,X1] :
( ~ c4_1(X1)
| c2_1(X1)
| c4_2(X0,a117)
| sP5_prd(X0)
| ~ c3_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f217,f223]) ).
fof(f238,plain,
! [X0,X1] :
( ~ c4_1(X1)
| c2_1(X1)
| ~ c5_2(X0,a117)
| sP5_prd(X0)
| ~ c3_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f218,f223]) ).
fof(f239,plain,
! [X0,X1] :
( ~ c4_1(X1)
| c2_1(X1)
| c3_2(X0,a117)
| sP5_prd(X0)
| ~ c3_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f219,f223]) ).
fof(f240,plain,
( c1_0
| sP12_prd(a118) ),
inference(resolution,[status(thm)],[f209,f42]) ).
fof(f241,plain,
! [X0] :
( ndr1_1(X0)
| sP6_prd(X0)
| ~ ndr1_0
| c3_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f45,f80]) ).
fof(f242,plain,
! [X0] :
( ndr1_1(X0)
| sP6_prd(X0)
| c3_0 ),
inference(resolution,[status(thm)],[f241,f223]) ).
fof(f243,plain,
! [X0] :
( c2_2(X0,a120)
| sP6_prd(X0)
| ~ ndr1_0
| c3_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f46,f80]) ).
fof(f244,plain,
! [X0] :
( c2_2(X0,a120)
| sP6_prd(X0)
| c3_0 ),
inference(resolution,[status(thm)],[f243,f223]) ).
fof(f245,plain,
! [X0] :
( c5_2(X0,a120)
| sP6_prd(X0)
| ~ ndr1_0
| c3_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f47,f80]) ).
fof(f246,plain,
! [X0] :
( c5_2(X0,a120)
| sP6_prd(X0)
| c3_0 ),
inference(resolution,[status(thm)],[f245,f223]) ).
fof(f247,plain,
! [X0] :
( ~ c1_2(X0,a120)
| sP6_prd(X0)
| ~ ndr1_0
| c3_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f48,f80]) ).
fof(f248,plain,
! [X0] :
( ~ c4_2(a121,X0)
| ~ c1_2(a121,X0)
| c3_2(a121,X0)
| ~ c1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f53,f50]) ).
fof(f249,plain,
( ~ c3_0
| c4_1(a137) ),
inference(forward_subsumption_resolution,[status(thm)],[f75,f80]) ).
fof(f250,plain,
( ~ c3_0
| c1_1(a137) ),
inference(forward_subsumption_resolution,[status(thm)],[f76,f80]) ).
fof(f251,plain,
! [X0] :
( c3_2(a121,X0)
| ~ c1_2(a121,X0)
| ~ c5_2(a121,X0)
| ~ c1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f54,f50]) ).
fof(f252,plain,
! [X0] :
( ~ c5_1(a133)
| c2_0
| sP8_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f66,f223]) ).
fof(f253,plain,
! [X0] :
( ~ c2_1(a133)
| c2_0
| sP8_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f67,f223]) ).
fof(f254,plain,
! [X0,X1] :
( ~ c4_0
| c3_2(X0,X1)
| c2_2(X0,X1)
| c5_2(X0,X1)
| ~ ndr1_1(X0)
| c5_1(X0)
| c5_2(X0,a138)
| ~ c2_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f78,f223]) ).
fof(f255,plain,
! [X0,X1] :
( ~ c4_0
| c3_2(X0,X1)
| c2_2(X0,X1)
| c5_2(X0,X1)
| ~ ndr1_1(X0)
| c5_1(X0)
| ~ c4_2(X0,a138)
| ~ c2_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f79,f223]) ).
fof(f256,plain,
! [X0,X1] :
( ndr1_1(a139)
| c3_0
| ~ c5_1(X0)
| ~ c4_1(X0)
| c3_2(X0,X1)
| c2_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f82,f223]) ).
fof(f257,plain,
! [X0] :
( c1_0
| ndr1_1(a139)
| c3_0
| ~ c4_1(a118)
| c3_2(a118,X0)
| c2_2(a118,X0)
| c1_2(a118,X0)
| ~ ndr1_1(a118) ),
inference(resolution,[status(thm)],[f256,f42]) ).
fof(f258,plain,
! [X0,X1] :
( c2_2(a139,a140)
| c3_0
| ~ c5_1(X0)
| ~ c4_1(X0)
| c3_2(X0,X1)
| c2_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f83,f223]) ).
fof(f259,plain,
! [X0] :
( c1_0
| c2_2(a139,a140)
| c3_0
| ~ c4_1(a118)
| c3_2(a118,X0)
| c2_2(a118,X0)
| c1_2(a118,X0)
| ~ ndr1_1(a118) ),
inference(resolution,[status(thm)],[f258,f42]) ).
fof(f260,plain,
! [X0,X1] :
( c1_2(a139,a140)
| c3_0
| ~ c5_1(X0)
| ~ c4_1(X0)
| c3_2(X0,X1)
| c2_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f84,f223]) ).
fof(f261,plain,
! [X0] :
( c1_0
| c1_2(a139,a140)
| c3_0
| ~ c4_1(a118)
| c3_2(a118,X0)
| c2_2(a118,X0)
| c1_2(a118,X0)
| ~ ndr1_1(a118) ),
inference(resolution,[status(thm)],[f260,f42]) ).
fof(f262,plain,
! [X0] :
( ~ c4_1(X0)
| c2_1(X0)
| sP5_prd(a134)
| ~ c3_0
| sP13_prd(a117) ),
inference(resolution,[status(thm)],[f214,f238]) ).
fof(f266,plain,
! [X0,X1] :
( c1_2(a108,X1)
| c2_2(a108,X1)
| c4_2(a108,X1)
| ~ ndr1_1(a108)
| sP2_prd
| sP1_prd(a134)
| sP0_prd(a134)
| c3_2(a134,X0)
| c2_2(a134,X0)
| ~ ndr1_1(a134)
| sP13_prd(X0) ),
inference(resolution,[status(thm)],[f214,f225]) ).
fof(f267,plain,
! [X0] :
( ~ c4_1(a108)
| sP2_prd
| sP1_prd(a134)
| sP0_prd(a134)
| c3_2(a134,X0)
| c2_2(a134,X0)
| ~ ndr1_1(a134)
| sP13_prd(X0) ),
inference(resolution,[status(thm)],[f214,f224]) ).
fof(f268,plain,
! [X0,X1] :
( ~ c4_2(a139,a140)
| c3_0
| ~ c5_1(X0)
| ~ c4_1(X0)
| c3_2(X0,X1)
| c2_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f85,f223]) ).
fof(f269,plain,
! [X0,X1] :
( ~ c4_1(X1)
| c2_1(X1)
| ndr1_1(X0)
| ~ c3_0 ),
inference(backward_subsumption_resolution,[status(thm)],[f236,f270]) ).
fof(f270,plain,
! [X0] :
( ndr1_1(X0)
| ~ sP5_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f131,f186]) ).
fof(f271,plain,
! [X0] :
( ndr1_1(X0)
| c3_0
| c4_1(X0)
| ndr1_1(X0) ),
inference(resolution,[status(thm)],[f139,f242]) ).
fof(f272,plain,
! [X0] :
( c3_0
| c4_1(X0)
| ndr1_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f271]) ).
fof(f277,plain,
! [X0,X1] :
( ~ c5_1(a139)
| c3_0
| ~ c5_1(X0)
| ~ c4_1(X0)
| c3_2(X0,X1)
| c2_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f86,f223]) ).
fof(f278,plain,
( ~ c2_2(a106,a107)
| ~ c4_2(a106,a107)
| ~ c1_2(a106,a107)
| ~ ndr1_1(a106)
| c5_1(a106)
| sP2_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f108,f223]) ).
fof(f279,plain,
( ~ c3_1(a109)
| c1_1(a109)
| sP3_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f113,f223]) ).
fof(f280,plain,
( c3_2(a121,a120)
| ~ c1_2(a121,a120)
| ~ c1_0
| sP6_prd(a121)
| c3_0 ),
inference(resolution,[status(thm)],[f246,f251]) ).
fof(f281,plain,
! [X0,X1] :
( ~ c3_1(X0)
| ~ c3_2(X0,a120)
| ~ c1_2(X0,a120)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| c5_2(a110,X1)
| c1_2(a110,X1)
| ~ ndr1_1(a110)
| sP3_prd
| sP6_prd(X0)
| c3_0 ),
inference(resolution,[status(thm)],[f246,f228]) ).
fof(f282,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c3_2(X0,a120)
| ~ c1_2(X0,a120)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c3_1(a110)
| sP3_prd
| sP6_prd(X0)
| c3_0 ),
inference(resolution,[status(thm)],[f246,f227]) ).
fof(f283,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c3_2(X0,a120)
| ~ c1_2(X0,a120)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c4_1(a110)
| sP3_prd
| sP6_prd(X0)
| c3_0 ),
inference(resolution,[status(thm)],[f246,f226]) ).
fof(f286,plain,
! [X0,X1] :
( ~ c3_1(X0)
| ~ c3_2(X0,a120)
| ~ c1_2(X0,a120)
| ~ c5_1(X0)
| c5_2(a110,X1)
| c1_2(a110,X1)
| ~ ndr1_1(a110)
| sP3_prd
| sP6_prd(X0)
| c3_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f281,f242]) ).
fof(f287,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c3_2(X0,a120)
| ~ c1_2(X0,a120)
| ~ c5_1(X0)
| ~ c3_1(a110)
| sP3_prd
| sP6_prd(X0)
| c3_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f282,f242]) ).
fof(f288,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c3_2(X0,a120)
| ~ c1_2(X0,a120)
| ~ c5_1(X0)
| ~ c4_1(a110)
| sP3_prd
| sP6_prd(X0)
| c3_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f283,f242]) ).
fof(f292,plain,
! [X0] :
( ~ c2_2(X0,a111)
| c3_2(X0,a111)
| ~ c5_2(X0,a111)
| sP4_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f121,f122]) ).
fof(f293,plain,
( sP13_prd(a111)
| ~ c2_2(a134,a111)
| c3_2(a134,a111)
| sP4_prd(a134) ),
inference(resolution,[status(thm)],[f292,f214]) ).
fof(f298,plain,
( sP6_prd(a134)
| c3_0
| c1_2(a134,a120)
| c4_2(a134,a120)
| ~ sP13_prd(a120) ),
inference(resolution,[status(thm)],[f212,f246]) ).
fof(f300,plain,
( ~ c3_1(a128)
| c2_1(a128)
| ~ c2_2(a128,a129)
| ~ c4_2(a128,a129)
| c1_2(a128,a129)
| ~ ndr1_1(a128)
| sP7_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f156,f223]) ).
fof(f302,plain,
( sP13_prd(a115)
| c4_2(a134,a115)
| ~ c2_2(a134,a115)
| ~ ndr1_1(a134)
| sP10_prd(a134) ),
inference(resolution,[status(thm)],[f190,f214]) ).
fof(f303,plain,
( sP13_prd(a115)
| ~ c2_2(a134,a115)
| ~ ndr1_1(a134)
| sP10_prd(a134) ),
inference(forward_subsumption_resolution,[status(thm)],[f302,f213]) ).
fof(f306,plain,
( c2_2(a125,a127)
| c3_2(a125,a127)
| c4_2(a125,a127)
| c4_1(a125)
| ~ c1_2(a125,a126)
| c5_2(a125,a126)
| c3_2(a125,a126)
| ~ ndr1_1(a125)
| sP11_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f221,f223]) ).
fof(f308,plain,
( sP8_prd(a118)
| c1_0 ),
inference(resolution,[status(thm)],[f240,f165]) ).
fof(f313,plain,
( c2_1(a134)
| ndr1_1(a134)
| sP9_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f220,f223]) ).
fof(f316,plain,
( c2_1(a134)
| c2_2(a134,sK2_skl)
| ~ sP13_prd(sK1_skl)
| sP9_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f181,f223]) ).
fof(f317,plain,
( c2_1(a134)
| c3_2(a134,sK2_skl)
| ~ sP13_prd(sK1_skl)
| sP9_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f182,f223]) ).
fof(f318,plain,
( c2_1(a134)
| c1_2(a134,sK2_skl)
| ~ sP13_prd(sK1_skl)
| sP9_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f183,f223]) ).
fof(f319,plain,
! [X0] :
( sP13_prd(X0)
| c3_1(a108)
| sP2_prd
| sP1_prd(a134)
| sP0_prd(a134)
| c3_2(a134,X0)
| c2_2(a134,X0)
| ~ ndr1_1(a134) ),
inference(resolution,[status(thm)],[f222,f214]) ).
fof(f322,plain,
! [X0] :
( c3_0
| ndr1_1(a108)
| sP2_prd
| sP1_prd(a134)
| sP0_prd(a134)
| c3_2(a134,X0)
| c2_2(a134,X0)
| ~ ndr1_1(a134)
| sP13_prd(X0) ),
inference(resolution,[status(thm)],[f267,f272]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN522+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n011.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 11:05:56 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.11/0.37 % Drodi V4.1.1
% 0.11/0.46 % SZS status CounterSatisfiable for theBenchmark: Theorem is counter-satisfiable, conjecture is false
% 0.11/0.46 % SZS output start Saturation for theBenchmark
% See solution above
% 0.11/0.47 % Elapsed time: 0.105239 seconds
% 0.11/0.47 % CPU time: 0.547450 seconds
% 0.11/0.47 % Total memory used: 31.331 MB
% 0.11/0.47 % Net memory used: 31.152 MB
%------------------------------------------------------------------------------