%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN036+2 : TPTP v8.1.2. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:47:07 EDT 2024
% Result : Theorem 66.33s 66.50s
% Output : Refutation 66.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SYN036+2 : TPTP v8.1.2. Released v2.0.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n004.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 20:06:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 66.33/66.50 % Version: 1.5
% 66.33/66.50 % SZS status Theorem
% 66.33/66.50 % SZS output start CNFRefutation
% 66.33/66.50 fof(pel34,conjecture,(((?[X]:(![Y]:(big_p(X)<=>big_p(Y))))<=>((?[U]:big_q(U))<=>(![W]:big_p(W))))<=>((?[X1]:(![Y1]:(big_q(X1)<=>big_q(Y1))))<=>((?[U1]:big_p(U1))<=>(![W1]:big_q(W1))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel34)).
% 66.33/66.50 fof(c0,negated_conjecture,(~(((?[X]:(![Y]:(big_p(X)<=>big_p(Y))))<=>((?[U]:big_q(U))<=>(![W]:big_p(W))))<=>((?[X1]:(![Y1]:(big_q(X1)<=>big_q(Y1))))<=>((?[U1]:big_p(U1))<=>(![W1]:big_q(W1)))))),inference(assume_negation,[status(cth)],[pel34])).
% 66.33/66.50 fof(c1,negated_conjecture,(((((![X]:(?[Y]:((~big_p(X)|~big_p(Y))&(big_p(X)|big_p(Y)))))|(((![U]:~big_q(U))|(?[W]:~big_p(W)))&((?[U]:big_q(U))|(![W]:big_p(W)))))&((?[X]:(![Y]:((~big_p(X)|big_p(Y))&(~big_p(Y)|big_p(X)))))|(((![U]:~big_q(U))|(![W]:big_p(W)))&((?[W]:~big_p(W))|(?[U]:big_q(U))))))|(((![X1]:(?[Y1]:((~big_q(X1)|~big_q(Y1))&(big_q(X1)|big_q(Y1)))))|(((![U1]:~big_p(U1))|(?[W1]:~big_q(W1)))&((?[U1]:big_p(U1))|(![W1]:big_q(W1)))))&((?[X1]:(![Y1]:((~big_q(X1)|big_q(Y1))&(~big_q(Y1)|big_q(X1)))))|(((![U1]:~big_p(U1))|(![W1]:big_q(W1)))&((?[W1]:~big_q(W1))|(?[U1]:big_p(U1)))))))&((((![X]:(?[Y]:((~big_p(X)|~big_p(Y))&(big_p(X)|big_p(Y)))))|(((![U]:~big_q(U))|(![W]:big_p(W)))&((?[W]:~big_p(W))|(?[U]:big_q(U)))))&((((![U]:~big_q(U))|(?[W]:~big_p(W)))&((?[U]:big_q(U))|(![W]:big_p(W))))|(?[X]:(![Y]:((~big_p(X)|big_p(Y))&(~big_p(Y)|big_p(X)))))))|(((![X1]:(?[Y1]:((~big_q(X1)|~big_q(Y1))&(big_q(X1)|big_q(Y1)))))|(((![U1]:~big_p(U1))|(![W1]:big_q(W1)))&((?[W1]:~big_q(W1))|(?[U1]:big_p(U1)))))&((((![U1]:~big_p(U1))|(?[W1]:~big_q(W1)))&((?[U1]:big_p(U1))|(![W1]:big_q(W1))))|(?[X1]:(![Y1]:((~big_q(X1)|big_q(Y1))&(~big_q(Y1)|big_q(X1))))))))),inference(fof_nnf,[status(thm)],[c0])).
% 66.33/66.50 fof(c2,negated_conjecture,(((((![X]:(?[Y]:((~big_p(X)|~big_p(Y))&(big_p(X)|big_p(Y)))))|(((![U]:~big_q(U))|(?[W]:~big_p(W)))&((?[U]:big_q(U))|(![W]:big_p(W)))))&((?[X]:((~big_p(X)|(![Y]:big_p(Y)))&((![Y]:~big_p(Y))|big_p(X))))|(((![U]:~big_q(U))|(![W]:big_p(W)))&((?[W]:~big_p(W))|(?[U]:big_q(U))))))|(((![X1]:(?[Y1]:((~big_q(X1)|~big_q(Y1))&(big_q(X1)|big_q(Y1)))))|(((![U1]:~big_p(U1))|(?[W1]:~big_q(W1)))&((?[U1]:big_p(U1))|(![W1]:big_q(W1)))))&((?[X1]:((~big_q(X1)|(![Y1]:big_q(Y1)))&((![Y1]:~big_q(Y1))|big_q(X1))))|(((![U1]:~big_p(U1))|(![W1]:big_q(W1)))&((?[W1]:~big_q(W1))|(?[U1]:big_p(U1)))))))&((((![X]:(?[Y]:((~big_p(X)|~big_p(Y))&(big_p(X)|big_p(Y)))))|(((![U]:~big_q(U))|(![W]:big_p(W)))&((?[W]:~big_p(W))|(?[U]:big_q(U)))))&((((![U]:~big_q(U))|(?[W]:~big_p(W)))&((?[U]:big_q(U))|(![W]:big_p(W))))|(?[X]:((~big_p(X)|(![Y]:big_p(Y)))&((![Y]:~big_p(Y))|big_p(X))))))|(((![X1]:(?[Y1]:((~big_q(X1)|~big_q(Y1))&(big_q(X1)|big_q(Y1)))))|(((![U1]:~big_p(U1))|(![W1]:big_q(W1)))&((?[W1]:~big_q(W1))|(?[U1]:big_p(U1)))))&((((![U1]:~big_p(U1))|(?[W1]:~big_q(W1)))&((?[U1]:big_p(U1))|(![W1]:big_q(W1))))|(?[X1]:((~big_q(X1)|(![Y1]:big_q(Y1)))&((![Y1]:~big_q(Y1))|big_q(X1)))))))),inference(shift_quantors,[status(thm)],[c1])).
% 66.33/66.50 fof(c3,negated_conjecture,(((((![X2]:(?[X3]:((~big_p(X2)|~big_p(X3))&(big_p(X2)|big_p(X3)))))|(((![X4]:~big_q(X4))|(?[X5]:~big_p(X5)))&((?[X6]:big_q(X6))|(![X7]:big_p(X7)))))&((?[X8]:((~big_p(X8)|(![X9]:big_p(X9)))&((![X10]:~big_p(X10))|big_p(X8))))|(((![X11]:~big_q(X11))|(![X12]:big_p(X12)))&((?[X13]:~big_p(X13))|(?[X14]:big_q(X14))))))|(((![X15]:(?[X16]:((~big_q(X15)|~big_q(X16))&(big_q(X15)|big_q(X16)))))|(((![X17]:~big_p(X17))|(?[X18]:~big_q(X18)))&((?[X19]:big_p(X19))|(![X20]:big_q(X20)))))&((?[X21]:((~big_q(X21)|(![X22]:big_q(X22)))&((![X23]:~big_q(X23))|big_q(X21))))|(((![X24]:~big_p(X24))|(![X25]:big_q(X25)))&((?[X26]:~big_q(X26))|(?[X27]:big_p(X27)))))))&((((![X28]:(?[X29]:((~big_p(X28)|~big_p(X29))&(big_p(X28)|big_p(X29)))))|(((![X30]:~big_q(X30))|(![X31]:big_p(X31)))&((?[X32]:~big_p(X32))|(?[X33]:big_q(X33)))))&((((![X34]:~big_q(X34))|(?[X35]:~big_p(X35)))&((?[X36]:big_q(X36))|(![X37]:big_p(X37))))|(?[X38]:((~big_p(X38)|(![X39]:big_p(X39)))&((![X40]:~big_p(X40))|big_p(X38))))))|(((![X41]:(?[X42]:((~big_q(X41)|~big_q(X42))&(big_q(X41)|big_q(X42)))))|(((![X43]:~big_p(X43))|(![X44]:big_q(X44)))&((?[X45]:~big_q(X45))|(?[X46]:big_p(X46)))))&((((![X47]:~big_p(X47))|(?[X48]:~big_q(X48)))&((?[X49]:big_p(X49))|(![X50]:big_q(X50))))|(?[X51]:((~big_q(X51)|(![X52]:big_q(X52)))&((![X53]:~big_q(X53))|big_q(X51)))))))),inference(variable_rename,[status(thm)],[c2])).
% 66.33/66.50 fof(c5,negated_conjecture,(![X2]:(![X4]:(![X7]:(![X9]:(![X10]:(![X11]:(![X12]:(![X15]:(![X17]:(![X20]:(![X22]:(![X23]:(![X24]:(![X25]:(![X28]:(![X30]:(![X31]:(![X34]:(![X37]:(![X39]:(![X40]:(![X41]:(![X43]:(![X44]:(![X47]:(![X50]:(![X52]:(![X53]:((((((~big_p(X2)|~big_p(skolem0001(X2)))&(big_p(X2)|big_p(skolem0001(X2))))|((~big_q(X4)|~big_p(skolem0002))&(big_q(skolem0003)|big_p(X7))))&(((~big_p(skolem0004)|big_p(X9))&(~big_p(X10)|big_p(skolem0004)))|((~big_q(X11)|big_p(X12))&(~big_p(skolem0005)|big_q(skolem0006)))))|((((~big_q(X15)|~big_q(skolem0007(X15)))&(big_q(X15)|big_q(skolem0007(X15))))|((~big_p(X17)|~big_q(skolem0008))&(big_p(skolem0009)|big_q(X20))))&(((~big_q(skolem0010)|big_q(X22))&(~big_q(X23)|big_q(skolem0010)))|((~big_p(X24)|big_q(X25))&(~big_q(skolem0011)|big_p(skolem0012))))))&(((((~big_p(X28)|~big_p(skolem0013(X28)))&(big_p(X28)|big_p(skolem0013(X28))))|((~big_q(X30)|big_p(X31))&(~big_p(skolem0014)|big_q(skolem0015))))&(((~big_q(X34)|~big_p(skolem0016))&(big_q(skolem0017)|big_p(X37)))|((~big_p(skolem0018)|big_p(X39))&(~big_p(X40)|big_p(skolem0018)))))|((((~big_q(X41)|~big_q(skolem0019(X41)))&(big_q(X41)|big_q(skolem0019(X41))))|((~big_p(X43)|big_q(X44))&(~big_q(skolem0020)|big_p(skolem0021))))&(((~big_p(X47)|~big_q(skolem0022))&(big_p(skolem0023)|big_q(X50)))|((~big_q(skolem0024)|big_q(X52))&(~big_q(X53)|big_q(skolem0024))))))))))))))))))))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,(((((![X2]:((~big_p(X2)|~big_p(skolem0001(X2)))&(big_p(X2)|big_p(skolem0001(X2)))))|(((![X4]:~big_q(X4))|~big_p(skolem0002))&(big_q(skolem0003)|(![X7]:big_p(X7)))))&(((~big_p(skolem0004)|(![X9]:big_p(X9)))&((![X10]:~big_p(X10))|big_p(skolem0004)))|(((![X11]:~big_q(X11))|(![X12]:big_p(X12)))&(~big_p(skolem0005)|big_q(skolem0006)))))|(((![X15]:((~big_q(X15)|~big_q(skolem0007(X15)))&(big_q(X15)|big_q(skolem0007(X15)))))|(((![X17]:~big_p(X17))|~big_q(skolem0008))&(big_p(skolem0009)|(![X20]:big_q(X20)))))&(((~big_q(skolem0010)|(![X22]:big_q(X22)))&((![X23]:~big_q(X23))|big_q(skolem0010)))|(((![X24]:~big_p(X24))|(![X25]:big_q(X25)))&(~big_q(skolem0011)|big_p(skolem0012))))))&((((![X28]:((~big_p(X28)|~big_p(skolem0013(X28)))&(big_p(X28)|big_p(skolem0013(X28)))))|(((![X30]:~big_q(X30))|(![X31]:big_p(X31)))&(~big_p(skolem0014)|big_q(skolem0015))))&((((![X34]:~big_q(X34))|~big_p(skolem0016))&(big_q(skolem0017)|(![X37]:big_p(X37))))|((~big_p(skolem0018)|(![X39]:big_p(X39)))&((![X40]:~big_p(X40))|big_p(skolem0018)))))|(((![X41]:((~big_q(X41)|~big_q(skolem0019(X41)))&(big_q(X41)|big_q(skolem0019(X41)))))|(((![X43]:~big_p(X43))|(![X44]:big_q(X44)))&(~big_q(skolem0020)|big_p(skolem0021))))&((((![X47]:~big_p(X47))|~big_q(skolem0022))&(big_p(skolem0023)|(![X50]:big_q(X50))))|((~big_q(skolem0024)|(![X52]:big_q(X52)))&((![X53]:~big_q(X53))|big_q(skolem0024))))))),inference(skolemize,[status(esa)],[c3])).])).
% 66.33/66.50 fof(c6,negated_conjecture,(![X2]:(![X4]:(![X7]:(![X9]:(![X10]:(![X11]:(![X12]:(![X15]:(![X17]:(![X20]:(![X22]:(![X23]:(![X24]:(![X25]:(![X28]:(![X30]:(![X31]:(![X34]:(![X37]:(![X39]:(![X40]:(![X41]:(![X43]:(![X44]:(![X47]:(![X50]:(![X52]:(![X53]:((((((((((~big_p(X2)|~big_p(skolem0001(X2)))|(~big_q(X4)|~big_p(skolem0002)))|((~big_q(X15)|~big_q(skolem0007(X15)))|(~big_p(X17)|~big_q(skolem0008))))&(((~big_p(X2)|~big_p(skolem0001(X2)))|(~big_q(X4)|~big_p(skolem0002)))|((~big_q(X15)|~big_q(skolem0007(X15)))|(big_p(skolem0009)|big_q(X20)))))&((((~big_p(X2)|~big_p(skolem0001(X2)))|(~big_q(X4)|~big_p(skolem0002)))|((big_q(X15)|big_q(skolem0007(X15)))|(~big_p(X17)|~big_q(skolem0008))))&(((~big_p(X2)|~big_p(skolem0001(X2)))|(~big_q(X4)|~big_p(skolem0002)))|((big_q(X15)|big_q(skolem0007(X15)))|(big_p(skolem0009)|big_q(X20))))))&(((((~big_p(X2)|~big_p(skolem0001(X2)))|(~big_q(X4)|~big_p(skolem0002)))|((~big_q(skolem0010)|big_q(X22))|(~big_p(X24)|big_q(X25))))&(((~big_p(X2)|~big_p(skolem0001(X2)))|(~big_q(X4)|~big_p(skolem0002)))|((~big_q(skolem0010)|big_q(X22))|(~big_q(skolem0011)|big_p(skolem0012)))))&((((~big_p(X2)|~big_p(skolem0001(X2)))|(~big_q(X4)|~big_p(skolem0002)))|((~big_q(X23)|big_q(skolem0010))|(~big_p(X24)|big_q(X25))))&(((~big_p(X2)|~big_p(skolem0001(X2)))|(~big_q(X4)|~big_p(skolem0002)))|((~big_q(X23)|big_q(skolem0010))|(~big_q(skolem0011)|big_p(skolem0012)))))))&((((((~big_p(X2)|~big_p(skolem0001(X2)))|(big_q(skolem0003)|big_p(X7)))|((~big_q(X15)|~big_q(skolem0007(X15)))|(~big_p(X17)|~big_q(skolem0008))))&(((~big_p(X2)|~big_p(skolem0001(X2)))|(big_q(skolem0003)|big_p(X7)))|((~big_q(X15)|~big_q(skolem0007(X15)))|(big_p(skolem0009)|big_q(X20)))))&((((~big_p(X2)|~big_p(skolem0001(X2)))|(big_q(skolem0003)|big_p(X7)))|((big_q(X15)|big_q(skolem0007(X15)))|(~big_p(X17)|~big_q(skolem0008))))&(((~big_p(X2)|~big_p(skolem0001(X2)))|(big_q(skolem0003)|big_p(X7)))|((big_q(X15)|big_q(skolem0007(X15)))|(big_p(skolem0009)|big_q(X20))))))&(((((~big_p(X2)|~big_p(skolem0001(X2)))|(big_q(skolem0003)|big_p(X7)))|((~big_q(skolem0010)|big_q(X22))|(~big_p(X24)|big_q(X25))))&(((~big_p(X2)|~big_p(skolem0001(X2)))|(big_q(skolem0003)|big_p(X7)))|((~big_q(skolem0010)|big_q(X22))|(~big_q(skolem0011)|big_p(skolem0012)))))&((((~big_p(X2)|~big_p(skolem0001(X2)))|(big_q(skolem0003)|big_p(X7)))|((~big_q(X23)|big_q(skolem0010))|(~big_p(X24)|big_q(X25))))&(((~big_p(X2)|~big_p(skolem0001(X2)))|(big_q(skolem0003)|big_p(X7)))|((~big_q(X23)|big_q(skolem0010))|(~big_q(skolem0011)|big_p(skolem0012))))))))&(((((((big_p(X2)|big_p(skolem0001(X2)))|(~big_q(X4)|~big_p(skolem0002)))|((~big_q(X15)|~big_q(skolem0007(X15)))|(~big_p(X17)|~big_q(skolem0008))))&(((big_p(X2)|big_p(skolem0001(X2)))|(~big_q(X4)|~big_p(skolem0002)))|((~big_q(X15)|~big_q(skolem0007(X15)))|(big_p(skolem0009)|big_q(X20)))))&((((big_p(X2)|big_p(skolem0001(X2)))|(~big_q(X4)|~big_p(skolem0002)))|((big_q(X15)|big_q(skolem0007(X15)))|(~big_p(X17)|~big_q(skolem0008))))&(((big_p(X2)|big_p(skolem0001(X2)))|(~big_q(X4)|~big_p(skolem0002)))|((big_q(X15)|big_q(skolem0007(X15)))|(big_p(skolem0009)|big_q(X20))))))&(((((big_p(X2)|big_p(skolem0001(X2)))|(~big_q(X4)|~big_p(skolem0002)))|((~big_q(skolem0010)|big_q(X22))|(~big_p(X24)|big_q(X25))))&(((big_p(X2)|big_p(skolem0001(X2)))|(~big_q(X4)|~big_p(skolem0002)))|((~big_q(skolem0010)|big_q(X22))|(~big_q(skolem0011)|big_p(skolem0012)))))&((((big_p(X2)|big_p(skolem0001(X2)))|(~big_q(X4)|~big_p(skolem0002)))|((~big_q(X23)|big_q(skolem0010))|(~big_p(X24)|big_q(X25))))&(((big_p(X2)|big_p(skolem0001(X2)))|(~big_q(X4)|~big_p(skolem0002)))|((~big_q(X23)|big_q(skolem0010))|(~big_q(skolem0011)|big_p(skolem0012)))))))&((((((big_p(X2)|big_p(skolem0001(X2)))|(big_q(skolem0003)|big_p(X7)))|((~big_q(X15)|~big_q(skolem0007(X15)))|(~big_p(X17)|~big_q(skolem0008))))&(((big_p(X2)|big_p(skolem0001(X2)))|(big_q(skolem0003)|big_p(X7)))|((~big_q(X15)|~big_q(skolem0007(X15)))|(big_p(skolem0009)|big_q(X20)))))&((((big_p(X2)|big_p(skolem0001(X2)))|(big_q(skolem0003)|big_p(X7)))|((big_q(X15)|big_q(skolem0007(X15)))|(~big_p(X17)|~big_q(skolem0008))))&(((big_p(X2)|big_p(skolem0001(X2)))|(big_q(skolem0003)|big_p(X7)))|((big_q(X15)|big_q(skolem0007(X15)))|(big_p(skolem0009)|big_q(X20))))))&(((((big_p(X2)|big_p(skolem0001(X2)))|(big_q(skolem0003)|big_p(X7)))|((~big_q(skolem0010)|big_q(X22))|(~big_p(X24)|big_q(X25))))&(((big_p(X2)|big_p(skolem0001(X2)))|(big_q(skolem0003)|big_p(X7)))|((~big_q(skolem0010)|big_q(X22))|(~big_q(skolem0011)|big_p(skolem0012)))))&((((big_p(X2)|big_p(skolem0001(X2)))|(big_q(skolem0003)|big_p(X7)))|((~big_q(X23)|big_q(skolem0010))|(~big_p(X24)|big_q(X25))))&(((big_p(X2)|big_p(skolem0001(X2)))|(big_q(skolem0003)|big_p(X7)))|((~big_q(X23)|big_q(skolem0010))|(~big_q(skolem0011)|big_p(skolem0012)))))))))&((((((((~big_p(skolem0004)|big_p(X9))|(~big_q(X11)|big_p(X12)))|((~big_q(X15)|~big_q(skolem0007(X15)))|(~big_p(X17)|~big_q(skolem0008))))&(((~big_p(skolem0004)|big_p(X9))|(~big_q(X11)|big_p(X12)))|((~big_q(X15)|~big_q(skolem0007(X15)))|(big_p(skolem0009)|big_q(X20)))))&((((~big_p(skolem0004)|big_p(X9))|(~big_q(X11)|big_p(X12)))|((big_q(X15)|big_q(skolem0007(X15)))|(~big_p(X17)|~big_q(skolem0008))))&(((~big_p(skolem0004)|big_p(X9))|(~big_q(X11)|big_p(X12)))|((big_q(X15)|big_q(skolem0007(X15)))|(big_p(skolem0009)|big_q(X20))))))&(((((~big_p(skolem0004)|big_p(X9))|(~big_q(X11)|big_p(X12)))|((~big_q(skolem0010)|big_q(X22))|(~big_p(X24)|big_q(X25))))&(((~big_p(skolem0004)|big_p(X9))|(~big_q(X11)|big_p(X12)))|((~big_q(skolem0010)|big_q(X22))|(~big_q(skolem0011)|big_p(skolem0012)))))&((((~big_p(skolem0004)|big_p(X9))|(~big_q(X11)|big_p(X12)))|((~big_q(X23)|big_q(skolem0010))|(~big_p(X24)|big_q(X25))))&(((~big_p(skolem0004)|big_p(X9))|(~big_q(X11)|big_p(X12)))|((~big_q(X23)|big_q(skolem0010))|(~big_q(skolem0011)|big_p(skolem0012)))))))&((((((~big_p(skolem0004)|big_p(X9))|(~big_p(skolem0005)|big_q(skolem0006)))|((~big_q(X15)|~big_q(skolem0007(X15)))|(~big_p(X17)|~big_q(skolem0008))))&(((~big_p(skolem0004)|big_p(X9))|(~big_p(skolem0005)|big_q(skolem0006)))|((~big_q(X15)|~big_q(skolem0007(X15)))|(big_p(skolem0009)|big_q(X20)))))&((((~big_p(skolem0004)|big_p(X9))|(~big_p(skolem0005)|big_q(skolem0006)))|((big_q(X15)|big_q(skolem0007(X15)))|(~big_p(X17)|~big_q(skolem0008))))&(((~big_p(skolem0004)|big_p(X9))|(~big_p(skolem0005)|big_q(skolem0006)))|((big_q(X15)|big_q(skolem0007(X15)))|(big_p(skolem0009)|big_q(X20))))))&(((((~big_p(skolem0004)|big_p(X9))|(~big_p(skolem0005)|big_q(skolem0006)))|((~big_q(skolem0010)|big_q(X22))|(~big_p(X24)|big_q(X25))))&(((~big_p(skolem0004)|big_p(X9))|(~big_p(skolem0005)|big_q(skolem0006)))|((~big_q(skolem0010)|big_q(X22))|(~big_q(skolem0011)|big_p(skolem0012)))))&((((~big_p(skolem0004)|big_p(X9))|(~big_p(skolem0005)|big_q(skolem0006)))|((~big_q(X23)|big_q(skolem0010))|(~big_p(X24)|big_q(X25))))&(((~big_p(skolem0004)|big_p(X9))|(~big_p(skolem0005)|big_q(skolem0006)))|((~big_q(X23)|big_q(skolem0010))|(~big_q(skolem0011)|big_p(skolem0012))))))))&(((((((~big_p(X10)|big_p(skolem0004))|(~big_q(X11)|big_p(X12)))|((~big_q(X15)|~big_q(skolem0007(X15)))|(~big_p(X17)|~big_q(skolem0008))))&(((~big_p(X10)|big_p(skolem0004))|(~big_q(X11)|big_p(X12)))|((~big_q(X15)|~big_q(skolem0007(X15)))|(big_p(skolem0009)|big_q(X20)))))&((((~big_p(X10)|big_p(skolem0004))|(~big_q(X11)|big_p(X12)))|((big_q(X15)|big_q(skolem0007(X15)))|(~big_p(X17)|~big_q(skolem0008))))&(((~big_p(X10)|big_p(skolem0004))|(~big_q(X11)|big_p(X12)))|((big_q(X15)|big_q(skolem0007(X15)))|(big_p(skolem0009)|big_q(X20))))))&(((((~big_p(X10)|big_p(skolem0004))|(~big_q(X11)|big_p(X12)))|((~big_q(skolem0010)|big_q(X22))|(~big_p(X24)|big_q(X25))))&(((~big_p(X10)|big_p(skolem0004))|(~big_q(X11)|big_p(X12)))|((~big_q(skolem0010)|big_q(X22))|(~big_q(skolem0011)|big_p(skolem0012)))))&((((~big_p(X10)|big_p(skolem0004))|(~big_q(X11)|big_p(X12)))|((~big_q(X23)|big_q(skolem0010))|(~big_p(X24)|big_q(X25))))&(((~big_p(X10)|big_p(skolem0004))|(~big_q(X11)|big_p(X12)))|((~big_q(X23)|big_q(skolem0010))|(~big_q(skolem0011)|big_p(skolem0012)))))))&((((((~big_p(X10)|big_p(skolem0004))|(~big_p(skolem0005)|big_q(skolem0006)))|((~big_q(X15)|~big_q(skolem0007(X15)))|(~big_p(X17)|~big_q(skolem0008))))&(((~big_p(X10)|big_p(skolem0004))|(~big_p(skolem0005)|big_q(skolem0006)))|((~big_q(X15)|~big_q(skolem0007(X15)))|(big_p(skolem0009)|big_q(X20)))))&((((~big_p(X10)|big_p(skolem0004))|(~big_p(skolem0005)|big_q(skolem0006)))|((big_q(X15)|big_q(skolem0007(X15)))|(~big_p(X17)|~big_q(skolem0008))))&(((~big_p(X10)|big_p(skolem0004))|(~big_p(skolem0005)|big_q(skolem0006)))|((big_q(X15)|big_q(skolem0007(X15)))|(big_p(skolem0009)|big_q(X20))))))&(((((~big_p(X10)|big_p(skolem0004))|(~big_p(skolem0005)|big_q(skolem0006)))|((~big_q(skolem0010)|big_q(X22))|(~big_p(X24)|big_q(X25))))&(((~big_p(X10)|big_p(skolem0004))|(~big_p(skolem0005)|big_q(skolem0006)))|((~big_q(skolem0010)|big_q(X22))|(~big_q(skolem0011)|big_p(skolem0012)))))&((((~big_p(X10)|big_p(skolem0004))|(~big_p(skolem0005)|big_q(skolem0006)))|((~big_q(X23)|big_q(skolem0010))|(~big_p(X24)|big_q(X25))))&(((~big_p(X10)|big_p(skolem0004))|(~big_p(skolem0005)|big_q(skolem0006)))|((~big_q(X23)|big_q(skolem0010))|(~big_q(skolem0011)|big_p(skolem0012))))))))))&(((((((((~big_p(X28)|~big_p(skolem0013(X28)))|(~big_q(X30)|big_p(X31)))|((~big_q(X41)|~big_q(skolem0019(X41)))|(~big_p(X43)|big_q(X44))))&(((~big_p(X28)|~big_p(skolem0013(X28)))|(~big_q(X30)|big_p(X31)))|((~big_q(X41)|~big_q(skolem0019(X41)))|(~big_q(skolem0020)|big_p(skolem0021)))))&((((~big_p(X28)|~big_p(skolem0013(X28)))|(~big_q(X30)|big_p(X31)))|((big_q(X41)|big_q(skolem0019(X41)))|(~big_p(X43)|big_q(X44))))&(((~big_p(X28)|~big_p(skolem0013(X28)))|(~big_q(X30)|big_p(X31)))|((big_q(X41)|big_q(skolem0019(X41)))|(~big_q(skolem0020)|big_p(skolem0021))))))&(((((~big_p(X28)|~big_p(skolem0013(X28)))|(~big_q(X30)|big_p(X31)))|((~big_p(X47)|~big_q(skolem0022))|(~big_q(skolem0024)|big_q(X52))))&(((~big_p(X28)|~big_p(skolem0013(X28)))|(~big_q(X30)|big_p(X31)))|((~big_p(X47)|~big_q(skolem0022))|(~big_q(X53)|big_q(skolem0024)))))&((((~big_p(X28)|~big_p(skolem0013(X28)))|(~big_q(X30)|big_p(X31)))|((big_p(skolem0023)|big_q(X50))|(~big_q(skolem0024)|big_q(X52))))&(((~big_p(X28)|~big_p(skolem0013(X28)))|(~big_q(X30)|big_p(X31)))|((big_p(skolem0023)|big_q(X50))|(~big_q(X53)|big_q(skolem0024)))))))&((((((~big_p(X28)|~big_p(skolem0013(X28)))|(~big_p(skolem0014)|big_q(skolem0015)))|((~big_q(X41)|~big_q(skolem0019(X41)))|(~big_p(X43)|big_q(X44))))&(((~big_p(X28)|~big_p(skolem0013(X28)))|(~big_p(skolem0014)|big_q(skolem0015)))|((~big_q(X41)|~big_q(skolem0019(X41)))|(~big_q(skolem0020)|big_p(skolem0021)))))&((((~big_p(X28)|~big_p(skolem0013(X28)))|(~big_p(skolem0014)|big_q(skolem0015)))|((big_q(X41)|big_q(skolem0019(X41)))|(~big_p(X43)|big_q(X44))))&(((~big_p(X28)|~big_p(skolem0013(X28)))|(~big_p(skolem0014)|big_q(skolem0015)))|((big_q(X41)|big_q(skolem0019(X41)))|(~big_q(skolem0020)|big_p(skolem0021))))))&(((((~big_p(X28)|~big_p(skolem0013(X28)))|(~big_p(skolem0014)|big_q(skolem0015)))|((~big_p(X47)|~big_q(skolem0022))|(~big_q(skolem0024)|big_q(X52))))&(((~big_p(X28)|~big_p(skolem0013(X28)))|(~big_p(skolem0014)|big_q(skolem0015)))|((~big_p(X47)|~big_q(skolem0022))|(~big_q(X53)|big_q(skolem0024)))))&((((~big_p(X28)|~big_p(skolem0013(X28)))|(~big_p(skolem0014)|big_q(skolem0015)))|((big_p(skolem0023)|big_q(X50))|(~big_q(skolem0024)|big_q(X52))))&(((~big_p(X28)|~big_p(skolem0013(X28)))|(~big_p(skolem0014)|big_q(skolem0015)))|((big_p(skolem0023)|big_q(X50))|(~big_q(X53)|big_q(skolem0024))))))))&(((((((big_p(X28)|big_p(skolem0013(X28)))|(~big_q(X30)|big_p(X31)))|((~big_q(X41)|~big_q(skolem0019(X41)))|(~big_p(X43)|big_q(X44))))&(((big_p(X28)|big_p(skolem0013(X28)))|(~big_q(X30)|big_p(X31)))|((~big_q(X41)|~big_q(skolem0019(X41)))|(~big_q(skolem0020)|big_p(skolem0021)))))&((((big_p(X28)|big_p(skolem0013(X28)))|(~big_q(X30)|big_p(X31)))|((big_q(X41)|big_q(skolem0019(X41)))|(~big_p(X43)|big_q(X44))))&(((big_p(X28)|big_p(skolem0013(X28)))|(~big_q(X30)|big_p(X31)))|((big_q(X41)|big_q(skolem0019(X41)))|(~big_q(skolem0020)|big_p(skolem0021))))))&(((((big_p(X28)|big_p(skolem0013(X28)))|(~big_q(X30)|big_p(X31)))|((~big_p(X47)|~big_q(skolem0022))|(~big_q(skolem0024)|big_q(X52))))&(((big_p(X28)|big_p(skolem0013(X28)))|(~big_q(X30)|big_p(X31)))|((~big_p(X47)|~big_q(skolem0022))|(~big_q(X53)|big_q(skolem0024)))))&((((big_p(X28)|big_p(skolem0013(X28)))|(~big_q(X30)|big_p(X31)))|((big_p(skolem0023)|big_q(X50))|(~big_q(skolem0024)|big_q(X52))))&(((big_p(X28)|big_p(skolem0013(X28)))|(~big_q(X30)|big_p(X31)))|((big_p(skolem0023)|big_q(X50))|(~big_q(X53)|big_q(skolem0024)))))))&((((((big_p(X28)|big_p(skolem0013(X28)))|(~big_p(skolem0014)|big_q(skolem0015)))|((~big_q(X41)|~big_q(skolem0019(X41)))|(~big_p(X43)|big_q(X44))))&(((big_p(X28)|big_p(skolem0013(X28)))|(~big_p(skolem0014)|big_q(skolem0015)))|((~big_q(X41)|~big_q(skolem0019(X41)))|(~big_q(skolem0020)|big_p(skolem0021)))))&((((big_p(X28)|big_p(skolem0013(X28)))|(~big_p(skolem0014)|big_q(skolem0015)))|((big_q(X41)|big_q(skolem0019(X41)))|(~big_p(X43)|big_q(X44))))&(((big_p(X28)|big_p(skolem0013(X28)))|(~big_p(skolem0014)|big_q(skolem0015)))|((big_q(X41)|big_q(skolem0019(X41)))|(~big_q(skolem0020)|big_p(skolem0021))))))&(((((big_p(X28)|big_p(skolem0013(X28)))|(~big_p(skolem0014)|big_q(skolem0015)))|((~big_p(X47)|~big_q(skolem0022))|(~big_q(skolem0024)|big_q(X52))))&(((big_p(X28)|big_p(skolem0013(X28)))|(~big_p(skolem0014)|big_q(skolem0015)))|((~big_p(X47)|~big_q(skolem0022))|(~big_q(X53)|big_q(skolem0024)))))&((((big_p(X28)|big_p(skolem0013(X28)))|(~big_p(skolem0014)|big_q(skolem0015)))|((big_p(skolem0023)|big_q(X50))|(~big_q(skolem0024)|big_q(X52))))&(((big_p(X28)|big_p(skolem0013(X28)))|(~big_p(skolem0014)|big_q(skolem0015)))|((big_p(skolem0023)|big_q(X50))|(~big_q(X53)|big_q(skolem0024)))))))))&((((((((~big_q(X34)|~big_p(skolem0016))|(~big_p(skolem0018)|big_p(X39)))|((~big_q(X41)|~big_q(skolem0019(X41)))|(~big_p(X43)|big_q(X44))))&(((~big_q(X34)|~big_p(skolem0016))|(~big_p(skolem0018)|big_p(X39)))|((~big_q(X41)|~big_q(skolem0019(X41)))|(~big_q(skolem0020)|big_p(skolem0021)))))&((((~big_q(X34)|~big_p(skolem0016))|(~big_p(skolem0018)|big_p(X39)))|((big_q(X41)|big_q(skolem0019(X41)))|(~big_p(X43)|big_q(X44))))&(((~big_q(X34)|~big_p(skolem0016))|(~big_p(skolem0018)|big_p(X39)))|((big_q(X41)|big_q(skolem0019(X41)))|(~big_q(skolem0020)|big_p(skolem0021))))))&(((((~big_q(X34)|~big_p(skolem0016))|(~big_p(skolem0018)|big_p(X39)))|((~big_p(X47)|~big_q(skolem0022))|(~big_q(skolem0024)|big_q(X52))))&(((~big_q(X34)|~big_p(skolem0016))|(~big_p(skolem0018)|big_p(X39)))|((~big_p(X47)|~big_q(skolem0022))|(~big_q(X53)|big_q(skolem0024)))))&((((~big_q(X34)|~big_p(skolem0016))|(~big_p(skolem0018)|big_p(X39)))|((big_p(skolem0023)|big_q(X50))|(~big_q(skolem0024)|big_q(X52))))&(((~big_q(X34)|~big_p(skolem0016))|(~big_p(skolem0018)|big_p(X39)))|((big_p(skolem0023)|big_q(X50))|(~big_q(X53)|big_q(skolem0024)))))))&((((((~big_q(X34)|~big_p(skolem0016))|(~big_p(X40)|big_p(skolem0018)))|((~big_q(X41)|~big_q(skolem0019(X41)))|(~big_p(X43)|big_q(X44))))&(((~big_q(X34)|~big_p(skolem0016))|(~big_p(X40)|big_p(skolem0018)))|((~big_q(X41)|~big_q(skolem0019(X41)))|(~big_q(skolem0020)|big_p(skolem0021)))))&((((~big_q(X34)|~big_p(skolem0016))|(~big_p(X40)|big_p(skolem0018)))|((big_q(X41)|big_q(skolem0019(X41)))|(~big_p(X43)|big_q(X44))))&(((~big_q(X34)|~big_p(skolem0016))|(~big_p(X40)|big_p(skolem0018)))|((big_q(X41)|big_q(skolem0019(X41)))|(~big_q(skolem0020)|big_p(skolem0021))))))&(((((~big_q(X34)|~big_p(skolem0016))|(~big_p(X40)|big_p(skolem0018)))|((~big_p(X47)|~big_q(skolem0022))|(~big_q(skolem0024)|big_q(X52))))&(((~big_q(X34)|~big_p(skolem0016))|(~big_p(X40)|big_p(skolem0018)))|((~big_p(X47)|~big_q(skolem0022))|(~big_q(X53)|big_q(skolem0024)))))&((((~big_q(X34)|~big_p(skolem0016))|(~big_p(X40)|big_p(skolem0018)))|((big_p(skolem0023)|big_q(X50))|(~big_q(skolem0024)|big_q(X52))))&(((~big_q(X34)|~big_p(skolem0016))|(~big_p(X40)|big_p(skolem0018)))|((big_p(skolem0023)|big_q(X50))|(~big_q(X53)|big_q(skolem0024))))))))&(((((((big_q(skolem0017)|big_p(X37))|(~big_p(skolem0018)|big_p(X39)))|((~big_q(X41)|~big_q(skolem0019(X41)))|(~big_p(X43)|big_q(X44))))&(((big_q(skolem0017)|big_p(X37))|(~big_p(skolem0018)|big_p(X39)))|((~big_q(X41)|~big_q(skolem0019(X41)))|(~big_q(skolem0020)|big_p(skolem0021)))))&((((big_q(skolem0017)|big_p(X37))|(~big_p(skolem0018)|big_p(X39)))|((big_q(X41)|big_q(skolem0019(X41)))|(~big_p(X43)|big_q(X44))))&(((big_q(skolem0017)|big_p(X37))|(~big_p(skolem0018)|big_p(X39)))|((big_q(X41)|big_q(skolem0019(X41)))|(~big_q(skolem0020)|big_p(skolem0021))))))&(((((big_q(skolem0017)|big_p(X37))|(~big_p(skolem0018)|big_p(X39)))|((~big_p(X47)|~big_q(skolem0022))|(~big_q(skolem0024)|big_q(X52))))&(((big_q(skolem0017)|big_p(X37))|(~big_p(skolem0018)|big_p(X39)))|((~big_p(X47)|~big_q(skolem0022))|(~big_q(X53)|big_q(skolem0024)))))&((((big_q(skolem0017)|big_p(X37))|(~big_p(skolem0018)|big_p(X39)))|((big_p(skolem0023)|big_q(X50))|(~big_q(skolem0024)|big_q(X52))))&(((big_q(skolem0017)|big_p(X37))|(~big_p(skolem0018)|big_p(X39)))|((big_p(skolem0023)|big_q(X50))|(~big_q(X53)|big_q(skolem0024)))))))&((((((big_q(skolem0017)|big_p(X37))|(~big_p(X40)|big_p(skolem0018)))|((~big_q(X41)|~big_q(skolem0019(X41)))|(~big_p(X43)|big_q(X44))))&(((big_q(skolem0017)|big_p(X37))|(~big_p(X40)|big_p(skolem0018)))|((~big_q(X41)|~big_q(skolem0019(X41)))|(~big_q(skolem0020)|big_p(skolem0021)))))&((((big_q(skolem0017)|big_p(X37))|(~big_p(X40)|big_p(skolem0018)))|((big_q(X41)|big_q(skolem0019(X41)))|(~big_p(X43)|big_q(X44))))&(((big_q(skolem0017)|big_p(X37))|(~big_p(X40)|big_p(skolem0018)))|((big_q(X41)|big_q(skolem0019(X41)))|(~big_q(skolem0020)|big_p(skolem0021))))))&(((((big_q(skolem0017)|big_p(X37))|(~big_p(X40)|big_p(skolem0018)))|((~big_p(X47)|~big_q(skolem0022))|(~big_q(skolem0024)|big_q(X52))))&(((big_q(skolem0017)|big_p(X37))|(~big_p(X40)|big_p(skolem0018)))|((~big_p(X47)|~big_q(skolem0022))|(~big_q(X53)|big_q(skolem0024)))))&((((big_q(skolem0017)|big_p(X37))|(~big_p(X40)|big_p(skolem0018)))|((big_p(skolem0023)|big_q(X50))|(~big_q(skolem0024)|big_q(X52))))&(((big_q(skolem0017)|big_p(X37))|(~big_p(X40)|big_p(skolem0018)))|((big_p(skolem0023)|big_q(X50))|(~big_q(X53)|big_q(skolem0024))))))))))))))))))))))))))))))))))))))),inference(distribute,[status(thm)],[c5])).
% 66.33/66.50 cnf(c43,negated_conjecture,~big_p(skolem0004)|big_p(X54)|~big_q(X58)|big_p(X56)|~big_q(skolem0010)|big_q(X59)|~big_p(X55)|big_q(X57),inference(split_conjunct,[status(thm)],[c6])).
% 66.33/66.50 cnf(c135,plain,~big_p(skolem0004)|big_p(X61)|~big_q(X63)|big_p(X64)|~big_q(skolem0010)|big_q(X62)|big_q(X60),inference(factor,[status(thm)],[c43])).
% 66.33/66.50 cnf(c136,plain,~big_p(skolem0004)|big_p(X66)|~big_q(skolem0010)|big_p(X67)|big_q(X65)|big_q(X68),inference(factor,[status(thm)],[c135])).
% 66.33/66.50 cnf(c45,negated_conjecture,~big_p(skolem0004)|big_p(X69)|~big_q(X74)|big_p(X72)|~big_q(X70)|big_q(skolem0010)|~big_p(X71)|big_q(X73),inference(split_conjunct,[status(thm)],[c6])).
% 66.33/66.50 cnf(c137,plain,~big_p(skolem0004)|big_p(X79)|~big_q(X76)|big_p(X78)|~big_q(X75)|big_q(skolem0010)|big_q(X77),inference(factor,[status(thm)],[c45])).
% 66.33/66.50 cnf(c138,plain,~big_p(skolem0004)|big_p(X85)|~big_q(X84)|big_p(X87)|big_q(skolem0010)|big_q(X86),inference(factor,[status(thm)],[c137])).
% 66.33/66.50 cnf(c133,negated_conjecture,big_q(skolem0017)|big_p(X804)|~big_p(X802)|big_p(skolem0018)|big_p(skolem0023)|big_q(X803)|~big_q(skolem0024)|big_q(X801),inference(split_conjunct,[status(thm)],[c6])).
% 66.33/66.50 cnf(c34,negated_conjecture,big_p(X581)|big_p(skolem0001(X581))|big_q(skolem0003)|big_p(X582)|big_q(X579)|big_q(skolem0007(X579))|big_p(skolem0009)|big_q(X580),inference(split_conjunct,[status(thm)],[c6])).
% 66.33/66.50 cnf(c202,plain,big_p(X585)|big_p(skolem0001(X585))|big_q(skolem0003)|big_q(X584)|big_q(skolem0007(X584))|big_p(skolem0009)|big_q(X583),inference(factor,[status(thm)],[c34])).
% 66.33/66.50 cnf(c386,plain,big_p(X586)|big_p(skolem0001(X586))|big_q(skolem0003)|big_q(X587)|big_q(skolem0007(X587))|big_p(skolem0009),inference(factor,[status(thm)],[c202])).
% 66.33/66.50 cnf(c536,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(X588)|big_q(skolem0007(X588)),inference(factor,[status(thm)],[c386])).
% 66.33/66.50 cnf(c648,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0007(skolem0003)),inference(factor,[status(thm)],[c536])).
% 66.33/66.50 cnf(c769,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|~big_p(skolem0004)|big_p(X956)|big_p(X955)|big_q(skolem0010)|big_q(X957),inference(resolution,[status(thm)],[c648, c138])).
% 66.33/66.50 cnf(c61,negated_conjecture,~big_p(X103)|big_p(skolem0004)|~big_q(X108)|big_p(X106)|~big_q(X104)|big_q(skolem0010)|~big_p(X105)|big_q(X107),inference(split_conjunct,[status(thm)],[c6])).
% 66.33/66.50 cnf(c142,plain,~big_p(X113)|big_p(skolem0004)|~big_q(X115)|big_p(X117)|~big_q(X114)|big_q(skolem0010)|big_q(X116),inference(factor,[status(thm)],[c61])).
% 66.33/66.50 cnf(c144,plain,~big_p(X120)|big_p(skolem0004)|~big_q(X121)|big_p(X119)|big_q(skolem0010)|big_q(X118),inference(factor,[status(thm)],[c142])).
% 66.33/66.50 cnf(c765,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|~big_p(X943)|big_p(skolem0004)|big_p(X944)|big_q(skolem0010)|big_q(X945),inference(resolution,[status(thm)],[c648, c144])).
% 66.33/66.50 cnf(c94,negated_conjecture,big_p(X538)|big_p(skolem0013(X538))|~big_q(X541)|big_p(X540)|big_p(skolem0023)|big_q(X537)|~big_q(X539)|big_q(skolem0024),inference(split_conjunct,[status(thm)],[c6])).
% 66.33/66.50 cnf(c197,plain,big_p(X545)|big_p(skolem0013(X545))|~big_q(X542)|big_p(X544)|big_p(skolem0023)|big_q(X543)|big_q(skolem0024),inference(factor,[status(thm)],[c94])).
% 66.33/66.50 cnf(c772,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_p(X1333)|big_p(skolem0013(X1333))|big_p(X1335)|big_p(skolem0023)|big_q(X1334)|big_q(skolem0024),inference(resolution,[status(thm)],[c648, c197])).
% 66.33/66.50 cnf(c1435,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_p(X1336)|big_p(skolem0013(X1336))|big_p(skolem0023)|big_q(X1337)|big_q(skolem0024),inference(factor,[status(thm)],[c772])).
% 66.33/66.50 cnf(c1770,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_p(X1338)|big_p(skolem0013(X1338))|big_p(skolem0023)|big_q(skolem0024),inference(factor,[status(thm)],[c1435])).
% 66.33/66.50 cnf(c2034,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_p(skolem0013(skolem0009))|big_p(skolem0023)|big_q(skolem0024),inference(factor,[status(thm)],[c1770])).
% 66.33/66.50 cnf(c2261,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_p(skolem0023)|big_q(skolem0024)|big_p(skolem0004)|big_p(X1501)|big_q(skolem0010)|big_q(X1502),inference(resolution,[status(thm)],[c2034, c765])).
% 66.33/66.50 cnf(c3838,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_p(skolem0023)|big_q(skolem0024)|big_p(skolem0004)|big_q(skolem0010)|big_q(X1503),inference(factor,[status(thm)],[c2261])).
% 66.33/66.50 cnf(c4136,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_p(skolem0023)|big_q(skolem0024)|big_p(skolem0004)|big_q(skolem0010),inference(factor,[status(thm)],[c3838])).
% 66.33/66.50 cnf(c4417,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_p(skolem0004)|big_q(skolem0010)|big_p(X1511)|big_q(X1512),inference(resolution,[status(thm)],[c4136, c765])).
% 66.33/66.50 cnf(c4497,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_p(skolem0004)|big_q(skolem0010)|big_q(X1513),inference(factor,[status(thm)],[c4417])).
% 66.33/66.50 cnf(c4782,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_p(skolem0004)|big_q(skolem0010),inference(factor,[status(thm)],[c4497])).
% 66.33/66.50 cnf(c5085,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_q(skolem0010)|big_p(X1541)|big_p(X1539)|big_q(X1540),inference(resolution,[status(thm)],[c4782, c769])).
% 66.33/66.50 cnf(c5157,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_q(skolem0010)|big_p(X1549)|big_q(X1550),inference(factor,[status(thm)],[c5085])).
% 66.33/66.50 cnf(c5495,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_q(skolem0010)|big_q(X1551),inference(factor,[status(thm)],[c5157])).
% 66.33/66.50 cnf(c5764,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_q(skolem0010),inference(factor,[status(thm)],[c5495])).
% 66.33/66.50 cnf(c6007,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_q(skolem0010)|~big_p(skolem0004)|big_p(X1598)|big_p(X1597)|big_q(X1599),inference(resolution,[status(thm)],[c5764, c138])).
% 66.33/66.50 cnf(c5036,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(skolem0004)|big_q(skolem0010)|~big_p(X1533)|big_p(X1534)|big_q(X1535),inference(resolution,[status(thm)],[c4782, c144])).
% 66.33/66.50 cnf(c6052,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|~big_p(skolem0004)|big_p(X1873)|big_p(X1874)|big_q(X1871)|big_q(X1872),inference(resolution,[status(thm)],[c5764, c136])).
% 66.33/66.50 cnf(c59,negated_conjecture,~big_p(X88)|big_p(skolem0004)|~big_q(X92)|big_p(X90)|~big_q(skolem0010)|big_q(X93)|~big_p(X89)|big_q(X91),inference(split_conjunct,[status(thm)],[c6])).
% 66.33/66.50 cnf(c140,plain,~big_p(X97)|big_p(skolem0004)|~big_q(X95)|big_p(X96)|~big_q(skolem0010)|big_q(X98)|big_q(X94),inference(factor,[status(thm)],[c59])).
% 66.33/66.50 cnf(c141,plain,~big_p(X99)|big_p(skolem0004)|~big_q(skolem0010)|big_p(X100)|big_q(X101)|big_q(X102),inference(factor,[status(thm)],[c140])).
% 66.33/66.50 cnf(c5100,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_p(skolem0004)|~big_p(X1823)|big_p(X1822)|big_q(X1821)|big_q(X1820),inference(resolution,[status(thm)],[c4782, c141])).
% 66.33/66.50 cnf(c8143,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_p(skolem0004)|big_p(X2053)|big_q(X2054)|big_q(X2052)|big_p(skolem0023),inference(resolution,[status(thm)],[c5100, c2034])).
% 66.33/66.50 cnf(c8310,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_p(skolem0004)|big_q(X2056)|big_q(X2055)|big_p(skolem0023),inference(factor,[status(thm)],[c8143])).
% 66.33/66.50 cnf(c8741,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_p(skolem0004)|big_q(X2065)|big_p(skolem0023),inference(factor,[status(thm)],[c8310])).
% 66.33/66.50 cnf(c9091,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_p(skolem0004)|big_p(skolem0023),inference(factor,[status(thm)],[c8741])).
% 66.33/66.50 cnf(c9480,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_p(skolem0004)|big_p(X2077)|big_q(X2078)|big_q(X2076),inference(resolution,[status(thm)],[c9091, c5100])).
% 66.33/66.50 cnf(c9486,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_p(skolem0004)|big_q(X2080)|big_q(X2079),inference(factor,[status(thm)],[c9480])).
% 66.33/66.50 cnf(c9892,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_p(skolem0004)|big_q(X2081),inference(factor,[status(thm)],[c9486])).
% 66.33/66.50 cnf(c10219,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_p(skolem0004),inference(factor,[status(thm)],[c9892])).
% 66.33/66.50 cnf(c10548,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_p(X2121)|big_p(X2122)|big_q(X2123)|big_q(X2120),inference(resolution,[status(thm)],[c10219, c6052])).
% 66.33/66.50 cnf(c10568,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_p(X2124)|big_q(X2125)|big_q(X2126),inference(factor,[status(thm)],[c10548])).
% 66.33/66.50 cnf(c11021,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_q(X2135)|big_q(X2134),inference(factor,[status(thm)],[c10568])).
% 66.33/66.50 cnf(c11396,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024)|big_q(X2136),inference(factor,[status(thm)],[c11021])).
% 66.33/66.50 cnf(c11694,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0003)|big_q(skolem0024),inference(factor,[status(thm)],[c11396])).
% 66.33/66.50 cnf(c11950,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(X2425)|big_p(skolem0013(X2425))|big_p(X2427)|big_p(skolem0023)|big_q(X2426),inference(resolution,[status(thm)],[c11694, c197])).
% 66.33/66.50 cnf(c13086,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(X2429)|big_p(skolem0013(X2429))|big_p(skolem0023)|big_q(X2428),inference(factor,[status(thm)],[c11950])).
% 66.33/66.50 cnf(c13470,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(X2437)|big_p(skolem0013(X2437))|big_p(skolem0023),inference(factor,[status(thm)],[c13086])).
% 66.33/66.50 cnf(c13769,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(skolem0013(skolem0009))|big_p(skolem0023),inference(factor,[status(thm)],[c13470])).
% 66.33/66.50 cnf(c14065,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(skolem0023)|big_p(skolem0004)|big_q(skolem0010)|big_p(X2500)|big_q(X2499),inference(resolution,[status(thm)],[c13769, c5036])).
% 66.33/66.50 cnf(c14418,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(skolem0023)|big_p(skolem0004)|big_q(skolem0010)|big_q(X2507),inference(factor,[status(thm)],[c14065])).
% 66.33/66.50 cnf(c14775,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(skolem0023)|big_p(skolem0004)|big_q(skolem0010),inference(factor,[status(thm)],[c14418])).
% 66.33/66.50 cnf(c15117,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(skolem0004)|big_q(skolem0010)|big_p(X2509)|big_q(X2508),inference(resolution,[status(thm)],[c14775, c5036])).
% 66.33/66.50 cnf(c15181,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(skolem0004)|big_q(skolem0010)|big_q(X2510),inference(factor,[status(thm)],[c15117])).
% 66.33/66.50 cnf(c15495,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(skolem0004)|big_q(skolem0010),inference(factor,[status(thm)],[c15181])).
% 66.33/66.50 cnf(c16597,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_q(skolem0010)|big_p(X2532)|big_p(X2534)|big_q(X2533),inference(resolution,[status(thm)],[c15495, c6007])).
% 66.33/66.50 cnf(c16776,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_q(skolem0010)|big_p(X2536)|big_q(X2535),inference(factor,[status(thm)],[c16597])).
% 66.33/66.50 cnf(c17138,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_q(skolem0010)|big_q(X2537),inference(factor,[status(thm)],[c16776])).
% 66.33/66.50 cnf(c17421,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_q(skolem0010),inference(factor,[status(thm)],[c17138])).
% 66.33/66.50 cnf(c17711,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|~big_p(skolem0004)|big_p(X2760)|big_p(X2761)|big_q(X2758)|big_q(X2759),inference(resolution,[status(thm)],[c17421, c136])).
% 66.33/66.50 cnf(c16627,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(skolem0004)|~big_p(X2733)|big_p(X2732)|big_q(X2731)|big_q(X2730),inference(resolution,[status(thm)],[c15495, c141])).
% 66.33/66.50 cnf(c13771,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(skolem0023)|big_p(skolem0013(skolem0023)),inference(factor,[status(thm)],[c13470])).
% 66.33/66.50 cnf(c19792,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(skolem0004)|big_p(X2904)|big_q(X2902)|big_q(X2903)|big_p(skolem0023),inference(resolution,[status(thm)],[c16627, c13771])).
% 66.33/66.50 cnf(c20803,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(skolem0004)|big_q(X2906)|big_q(X2905)|big_p(skolem0023),inference(factor,[status(thm)],[c19792])).
% 66.33/66.50 cnf(c21227,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(skolem0004)|big_q(X2907)|big_p(skolem0023),inference(factor,[status(thm)],[c20803])).
% 66.33/66.50 cnf(c21567,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(skolem0004)|big_p(skolem0023),inference(factor,[status(thm)],[c21227])).
% 66.33/66.50 cnf(c21913,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(skolem0004)|big_p(X2919)|big_q(X2917)|big_q(X2918),inference(resolution,[status(thm)],[c21567, c16627])).
% 66.33/66.50 cnf(c21933,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(skolem0004)|big_q(X2921)|big_q(X2920),inference(factor,[status(thm)],[c21913])).
% 66.33/66.50 cnf(c22337,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(skolem0004)|big_q(X2922),inference(factor,[status(thm)],[c21933])).
% 66.33/66.50 cnf(c22659,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(skolem0004),inference(factor,[status(thm)],[c22337])).
% 66.33/66.50 cnf(c22951,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(X2950)|big_p(X2951)|big_q(X2949)|big_q(X2948),inference(resolution,[status(thm)],[c22659, c17711])).
% 66.33/66.50 cnf(c23050,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_p(X2952)|big_q(X2953)|big_q(X2954),inference(factor,[status(thm)],[c22951])).
% 66.33/66.50 cnf(c23513,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_q(X2956)|big_q(X2955),inference(factor,[status(thm)],[c23050])).
% 66.33/66.50 cnf(c23894,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024)|big_q(X2964),inference(factor,[status(thm)],[c23513])).
% 66.33/66.50 cnf(c24194,plain,big_p(skolem0009)|big_p(skolem0001(skolem0009))|big_q(skolem0024),inference(factor,[status(thm)],[c23894])).
% 66.33/66.50 cnf(c134,negated_conjecture,big_q(skolem0017)|big_p(X808)|~big_p(X806)|big_p(skolem0018)|big_p(skolem0023)|big_q(X807)|~big_q(X805)|big_q(skolem0024),inference(split_conjunct,[status(thm)],[c6])).
% 66.33/66.50 cnf(c129,negated_conjecture,big_q(skolem0017)|big_p(X779)|~big_p(X776)|big_p(skolem0018)|big_q(X780)|big_q(skolem0019(X780))|~big_p(X777)|big_q(X778),inference(split_conjunct,[status(thm)],[c6])).
% 66.33/66.50 cnf(c1095,plain,big_q(skolem0017)|big_p(X784)|~big_p(X782)|big_p(skolem0018)|big_q(X781)|big_q(skolem0019(X781))|big_q(X783),inference(factor,[status(thm)],[c129])).
% 66.33/66.50 cnf(c24428,plain,big_p(skolem0009)|big_q(skolem0024)|big_q(skolem0017)|big_p(X3315)|big_p(skolem0018)|big_q(X3313)|big_q(skolem0019(X3313))|big_q(X3314),inference(resolution,[status(thm)],[c24194, c1095])).
% 66.33/66.50 cnf(c26321,plain,big_p(skolem0009)|big_q(skolem0024)|big_q(skolem0017)|big_p(skolem0018)|big_q(X3316)|big_q(skolem0019(X3316))|big_q(X3317),inference(factor,[status(thm)],[c24428])).
% 66.33/66.50 cnf(c26747,plain,big_p(skolem0009)|big_q(skolem0024)|big_q(skolem0017)|big_p(skolem0018)|big_q(X3318)|big_q(skolem0019(X3318)),inference(factor,[status(thm)],[c26321])).
% 66.33/66.50 cnf(c27091,plain,big_p(skolem0009)|big_q(skolem0024)|big_q(skolem0017)|big_p(skolem0018)|big_q(skolem0019(skolem0024)),inference(factor,[status(thm)],[c26747])).
% 66.33/66.50 cnf(c27442,plain,big_p(skolem0009)|big_q(skolem0024)|big_q(skolem0017)|big_p(skolem0018)|big_p(X3362)|~big_p(X3364)|big_p(skolem0023)|big_q(X3363),inference(resolution,[status(thm)],[c27091, c134])).
% 66.33/66.50 cnf(c27711,plain,big_p(skolem0009)|big_q(skolem0024)|big_q(skolem0017)|big_p(skolem0018)|big_p(X3374)|big_p(skolem0023)|big_q(X3373),inference(resolution,[status(thm)],[c27442, c24194])).
% 66.33/66.50 cnf(c27791,plain,big_p(skolem0009)|big_q(skolem0024)|big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023)|big_q(X3375),inference(factor,[status(thm)],[c27711])).
% 66.33/66.50 cnf(c28096,plain,big_p(skolem0009)|big_q(skolem0024)|big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023),inference(factor,[status(thm)],[c27791])).
% 66.33/66.50 cnf(c28331,plain,big_q(skolem0024)|big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023)|big_p(X3484)|big_q(X3482)|big_q(skolem0019(X3482))|big_q(X3483),inference(resolution,[status(thm)],[c28096, c1095])).
% 66.33/66.50 cnf(c28536,plain,big_q(skolem0024)|big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023)|big_p(X3485)|big_q(X3486)|big_q(skolem0019(X3486)),inference(factor,[status(thm)],[c28331])).
% 66.33/66.50 cnf(c28983,plain,big_q(skolem0024)|big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023)|big_q(X3487)|big_q(skolem0019(X3487)),inference(factor,[status(thm)],[c28536])).
% 66.33/66.50 cnf(c29313,plain,big_q(skolem0024)|big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023)|big_q(skolem0019(skolem0024)),inference(factor,[status(thm)],[c28983])).
% 66.33/66.50 cnf(c29684,plain,big_q(skolem0024)|big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023)|big_p(X3498)|~big_p(X3500)|big_q(X3499),inference(resolution,[status(thm)],[c29313, c134])).
% 66.33/66.50 cnf(c29886,plain,big_q(skolem0024)|big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023)|big_p(X3507)|big_q(X3508),inference(resolution,[status(thm)],[c29684, c28096])).
% 66.33/66.50 cnf(c29896,plain,big_q(skolem0024)|big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023)|big_p(X3509),inference(factor,[status(thm)],[c29886])).
% 66.33/66.50 cnf(c30187,plain,big_q(skolem0024)|big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023),inference(factor,[status(thm)],[c29896])).
% 66.33/66.50 cnf(c30367,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023)|big_p(X3532)|~big_p(X3530)|big_q(X3531)|big_q(X3533),inference(resolution,[status(thm)],[c30187, c133])).
% 66.33/66.50 cnf(c93,negated_conjecture,big_p(X525)|big_p(skolem0013(X525))|~big_q(X528)|big_p(X526)|big_p(skolem0023)|big_q(X524)|~big_q(skolem0024)|big_q(X527),inference(split_conjunct,[status(thm)],[c6])).
% 66.33/66.50 cnf(c196,plain,big_p(X535)|big_p(skolem0013(X535))|~big_q(skolem0024)|big_p(X534)|big_p(skolem0023)|big_q(X533)|big_q(X536),inference(factor,[status(thm)],[c93])).
% 66.33/66.50 cnf(c30374,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023)|big_p(X4007)|big_p(skolem0013(X4007))|big_p(X4009)|big_q(X4010)|big_q(X4008),inference(resolution,[status(thm)],[c30187, c196])).
% 66.33/66.50 cnf(c33811,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023)|big_p(X4011)|big_p(skolem0013(X4011))|big_p(X4013)|big_q(X4012),inference(factor,[status(thm)],[c30374])).
% 66.33/66.50 cnf(c34308,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023)|big_p(X4015)|big_p(skolem0013(X4015))|big_p(X4014),inference(factor,[status(thm)],[c33811])).
% 66.33/66.50 cnf(c34696,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023)|big_p(X4022)|big_p(skolem0013(X4022)),inference(factor,[status(thm)],[c34308])).
% 66.33/66.50 cnf(c35039,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023)|big_p(skolem0013(skolem0018)),inference(factor,[status(thm)],[c34696])).
% 66.33/66.50 cnf(c35284,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023)|big_p(X4035)|big_q(X4034)|big_q(X4036),inference(resolution,[status(thm)],[c35039, c30367])).
% 66.33/66.50 cnf(c35484,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023)|big_p(X4038)|big_q(X4037),inference(factor,[status(thm)],[c35284])).
% 66.33/66.50 cnf(c35851,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023)|big_p(X4045),inference(factor,[status(thm)],[c35484])).
% 66.33/66.50 cnf(c36180,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0023),inference(factor,[status(thm)],[c35851])).
% 66.33/66.50 cnf(c36386,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(X4078)|big_q(X4076)|big_q(skolem0019(X4076))|big_q(X4077),inference(resolution,[status(thm)],[c36180, c1095])).
% 66.33/66.50 cnf(c36435,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(X4079)|big_q(X4080)|big_q(skolem0019(X4080)),inference(factor,[status(thm)],[c36386])).
% 66.33/66.50 cnf(c36819,plain,big_q(skolem0017)|big_p(skolem0018)|big_q(X4087)|big_q(skolem0019(X4087)),inference(factor,[status(thm)],[c36435])).
% 66.33/66.50 cnf(c37147,plain,big_q(skolem0017)|big_p(skolem0018)|big_q(skolem0019(skolem0017)),inference(factor,[status(thm)],[c36819])).
% 66.33/66.50 cnf(c37386,plain,big_q(skolem0017)|big_p(skolem0018)|~big_p(X4226)|big_p(skolem0004)|big_p(X4227)|big_q(skolem0010)|big_q(X4228),inference(resolution,[status(thm)],[c37147, c144])).
% 66.33/66.50 cnf(c39030,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0004)|big_p(X4230)|big_q(skolem0010)|big_q(X4229),inference(resolution,[status(thm)],[c37386, c36180])).
% 66.33/66.50 cnf(c39091,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0004)|big_p(X4237)|big_q(skolem0010),inference(factor,[status(thm)],[c39030])).
% 66.33/66.50 cnf(c39396,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0004)|big_q(skolem0010),inference(factor,[status(thm)],[c39091])).
% 66.33/66.50 cnf(c39670,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0004)|~big_p(X4267)|big_p(X4266)|big_q(X4265)|big_q(X4264),inference(resolution,[status(thm)],[c39396, c141])).
% 66.33/66.50 cnf(c39787,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0004)|big_p(X4270)|big_q(X4269)|big_q(X4268),inference(resolution,[status(thm)],[c39670, c36180])).
% 66.33/66.50 cnf(c39850,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0004)|big_p(X4272)|big_q(X4271),inference(factor,[status(thm)],[c39787])).
% 66.33/66.50 cnf(c40231,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0004)|big_p(X4278),inference(factor,[status(thm)],[c39850])).
% 66.33/66.50 cnf(c40502,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(skolem0004),inference(factor,[status(thm)],[c40231])).
% 66.33/66.50 cnf(c37398,plain,big_q(skolem0017)|big_p(skolem0018)|~big_p(skolem0004)|big_p(X4324)|big_p(X4323)|big_q(skolem0010)|big_q(X4325),inference(resolution,[status(thm)],[c37147, c138])).
% 66.33/66.50 cnf(c40806,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(X4326)|big_p(X4328)|big_q(skolem0010)|big_q(X4327),inference(resolution,[status(thm)],[c37398, c40502])).
% 66.33/66.50 cnf(c40816,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(X4329)|big_p(X4330)|big_q(skolem0010),inference(factor,[status(thm)],[c40806])).
% 66.33/66.50 cnf(c41194,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(X4336)|big_q(skolem0010),inference(factor,[status(thm)],[c40816])).
% 66.33/66.50 cnf(c41461,plain,big_q(skolem0017)|big_p(skolem0018)|big_q(skolem0010),inference(factor,[status(thm)],[c41194])).
% 66.33/66.50 cnf(c41693,plain,big_q(skolem0017)|big_p(skolem0018)|~big_p(skolem0004)|big_p(X4401)|big_p(X4402)|big_q(X4399)|big_q(X4400),inference(resolution,[status(thm)],[c41461, c136])).
% 66.33/66.50 cnf(c41809,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(X4404)|big_p(X4405)|big_q(X4406)|big_q(X4403),inference(resolution,[status(thm)],[c41693, c40502])).
% 66.33/66.50 cnf(c41819,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(X4407)|big_p(X4409)|big_q(X4408),inference(factor,[status(thm)],[c41809])).
% 66.33/66.50 cnf(c42275,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(X4411)|big_p(X4410),inference(factor,[status(thm)],[c41819])).
% 66.33/66.50 cnf(c42619,plain,big_q(skolem0017)|big_p(skolem0018)|big_p(X4412),inference(factor,[status(thm)],[c42275])).
% 66.33/66.50 cnf(c42854,plain,big_q(skolem0017)|big_p(skolem0018),inference(factor,[status(thm)],[c42619])).
% 66.33/66.50 cnf(c121,negated_conjecture,big_q(skolem0017)|big_p(X740)|~big_p(skolem0018)|big_p(X737)|big_q(X741)|big_q(skolem0019(X741))|~big_p(X738)|big_q(X739),inference(split_conjunct,[status(thm)],[c6])).
% 66.33/66.50 cnf(c1045,plain,big_q(skolem0017)|big_p(X744)|~big_p(skolem0018)|big_p(X743)|big_q(X745)|big_q(skolem0019(X745))|big_q(X742),inference(factor,[status(thm)],[c121])).
% 66.33/66.50 cnf(c43035,plain,big_q(skolem0017)|big_p(X4472)|big_p(X4473)|big_q(X4474)|big_q(skolem0019(X4474))|big_q(X4471),inference(resolution,[status(thm)],[c42854, c1045])).
% 66.33/66.50 cnf(c43057,plain,big_q(skolem0017)|big_p(X4477)|big_p(X4476)|big_q(X4475)|big_q(skolem0019(X4475)),inference(factor,[status(thm)],[c43035])).
% 66.33/66.50 cnf(c43502,plain,big_q(skolem0017)|big_p(X4484)|big_q(X4485)|big_q(skolem0019(X4485)),inference(factor,[status(thm)],[c43057])).
% 66.33/66.50 cnf(c43838,plain,big_q(skolem0017)|big_p(X4486)|big_q(skolem0019(skolem0017)),inference(factor,[status(thm)],[c43502])).
% 66.33/66.50 cnf(c44205,plain,big_q(skolem0017)|big_p(X4584)|~big_p(X4582)|big_p(skolem0004)|big_p(X4583)|big_q(skolem0010)|big_q(X4585),inference(resolution,[status(thm)],[c43838, c144])).
% 66.33/66.50 cnf(c44254,plain,big_q(skolem0017)|big_p(X4588)|big_p(skolem0004)|big_p(X4586)|big_q(skolem0010)|big_q(X4587),inference(resolution,[status(thm)],[c44205, c42854])).
% 66.33/66.51 cnf(c44305,plain,big_q(skolem0017)|big_p(X4589)|big_p(skolem0004)|big_p(X4590)|big_q(skolem0010),inference(factor,[status(thm)],[c44254])).
% 66.33/66.51 cnf(c44668,plain,big_q(skolem0017)|big_p(skolem0004)|big_p(X4591)|big_q(skolem0010),inference(factor,[status(thm)],[c44305])).
% 66.33/66.51 cnf(c44925,plain,big_q(skolem0017)|big_p(skolem0004)|big_q(skolem0010),inference(factor,[status(thm)],[c44668])).
% 66.33/66.51 cnf(c45153,plain,big_q(skolem0017)|big_p(skolem0004)|~big_p(X4636)|big_p(X4635)|big_q(X4634)|big_q(X4633),inference(resolution,[status(thm)],[c44925, c141])).
% 66.33/66.51 cnf(c45285,plain,big_q(skolem0017)|big_p(skolem0004)|big_p(X4639)|big_q(X4637)|big_q(X4638),inference(resolution,[status(thm)],[c45153, c42854])).
% 66.33/66.51 cnf(c45337,plain,big_q(skolem0017)|big_p(skolem0004)|big_p(X4640)|big_q(X4641),inference(factor,[status(thm)],[c45285])).
% 66.33/66.51 cnf(c45670,plain,big_q(skolem0017)|big_p(skolem0004)|big_p(X4642),inference(factor,[status(thm)],[c45337])).
% 66.33/66.51 cnf(c45899,plain,big_q(skolem0017)|big_p(skolem0004),inference(factor,[status(thm)],[c45670])).
% 66.33/66.51 cnf(c44217,plain,big_q(skolem0017)|big_p(X5072)|~big_p(skolem0004)|big_p(X5071)|big_p(X5070)|big_q(skolem0010)|big_q(X5073),inference(resolution,[status(thm)],[c43838, c138])).
% 66.33/66.51 cnf(c51607,plain,big_q(skolem0017)|big_p(X5075)|big_p(X5076)|big_p(X5077)|big_q(skolem0010)|big_q(X5074),inference(resolution,[status(thm)],[c44217, c45899])).
% 66.33/66.51 cnf(c51608,plain,big_q(skolem0017)|big_p(X5079)|big_p(X5078)|big_p(X5080)|big_q(skolem0010),inference(factor,[status(thm)],[c51607])).
% 66.33/66.51 cnf(c52007,plain,big_q(skolem0017)|big_p(X5087)|big_p(X5088)|big_q(skolem0010),inference(factor,[status(thm)],[c51608])).
% 66.33/66.51 cnf(c52334,plain,big_q(skolem0017)|big_p(X5089)|big_q(skolem0010),inference(factor,[status(thm)],[c52007])).
% 66.33/66.51 cnf(c52561,plain,big_p(X5125)|big_q(skolem0010)|~big_p(skolem0004)|big_p(X5124)|big_p(X5123)|big_q(X5126),inference(resolution,[status(thm)],[c52334, c138])).
% 66.33/66.51 cnf(c45099,plain,big_p(skolem0004)|big_q(skolem0010)|~big_p(X4601)|big_p(X4602)|big_q(X4603),inference(resolution,[status(thm)],[c44925, c144])).
% 66.33/66.51 cnf(c537,plain,big_p(X589)|big_p(skolem0001(X589))|big_q(skolem0003)|big_q(skolem0007(skolem0003))|big_p(skolem0009),inference(factor,[status(thm)],[c386])).
% 66.33/66.51 cnf(c835,plain,big_p(X1039)|big_p(skolem0001(X1039))|big_q(skolem0003)|big_p(skolem0009)|~big_p(X1036)|big_p(skolem0004)|big_p(X1037)|big_q(skolem0010)|big_q(X1038),inference(resolution,[status(thm)],[c537, c144])).
% 66.33/66.51 cnf(c5031,plain,big_p(skolem0009)|big_q(skolem0003)|big_q(skolem0024)|big_p(skolem0004)|big_q(skolem0010)|big_p(X1707)|big_p(skolem0001(X1707))|big_p(X1706)|big_q(X1708),inference(resolution,[status(thm)],[c4782, c835])).
% 66.33/66.51 cnf(c6155,plain,big_p(skolem0009)|big_q(skolem0003)|big_q(skolem0024)|big_p(skolem0004)|big_q(skolem0010)|big_p(X1710)|big_p(skolem0001(X1710))|big_q(X1709),inference(factor,[status(thm)],[c5031])).
% 66.33/66.51 cnf(c6522,plain,big_p(skolem0009)|big_q(skolem0003)|big_q(skolem0024)|big_p(skolem0004)|big_q(skolem0010)|big_p(X1719)|big_p(skolem0001(X1719)),inference(factor,[status(thm)],[c6155])).
% 66.33/66.51 cnf(c6818,plain,big_p(skolem0009)|big_q(skolem0003)|big_q(skolem0024)|big_p(skolem0004)|big_q(skolem0010)|big_p(skolem0001(skolem0004)),inference(factor,[status(thm)],[c6522])).
% 66.33/66.51 cnf(c7028,plain,big_p(skolem0009)|big_q(skolem0024)|big_p(skolem0004)|big_q(skolem0010)|big_p(skolem0001(skolem0004))|~big_p(X1750)|big_p(X1751)|big_q(X1752),inference(resolution,[status(thm)],[c6818, c144])).
% 66.33/66.51 cnf(c16553,plain,big_p(skolem0009)|big_q(skolem0024)|big_p(skolem0004)|big_q(skolem0010)|big_p(skolem0001(skolem0004))|big_p(X2581)|big_q(X2580),inference(resolution,[status(thm)],[c15495, c7028])).
% 66.33/66.51 cnf(c17814,plain,big_p(skolem0009)|big_q(skolem0024)|big_p(skolem0004)|big_q(skolem0010)|big_p(skolem0001(skolem0004))|big_q(X2589),inference(factor,[status(thm)],[c16553])).
% 66.33/66.51 cnf(c18135,plain,big_p(skolem0009)|big_q(skolem0024)|big_p(skolem0004)|big_q(skolem0010)|big_p(skolem0001(skolem0004)),inference(factor,[status(thm)],[c17814])).
% 66.33/66.51 cnf(c18438,plain,big_p(skolem0009)|big_q(skolem0024)|big_p(skolem0004)|big_p(skolem0001(skolem0004))|~big_p(X2769)|big_p(X2768)|big_q(X2767)|big_q(X2766),inference(resolution,[status(thm)],[c18135, c141])).
% 66.33/66.51 cnf(c22911,plain,big_p(skolem0009)|big_q(skolem0024)|big_p(skolem0004)|big_p(skolem0001(skolem0004))|big_p(X3023)|big_q(X3024)|big_q(X3025),inference(resolution,[status(thm)],[c22659, c18438])).
% 66.33/66.51 cnf(c24487,plain,big_p(skolem0009)|big_q(skolem0024)|big_p(skolem0004)|big_p(skolem0001(skolem0004))|big_q(X3026)|big_q(X3027),inference(factor,[status(thm)],[c22911])).
% 66.33/66.51 cnf(c24883,plain,big_p(skolem0009)|big_q(skolem0024)|big_p(skolem0004)|big_p(skolem0001(skolem0004))|big_q(X3034),inference(factor,[status(thm)],[c24487])).
% 66.33/66.51 cnf(c25198,plain,big_p(skolem0009)|big_q(skolem0024)|big_p(skolem0004)|big_p(skolem0001(skolem0004)),inference(factor,[status(thm)],[c24883])).
% 66.33/66.51 cnf(c45212,plain,big_p(skolem0004)|big_q(skolem0010)|big_p(X4719)|big_q(X4718)|big_p(skolem0009)|big_q(skolem0024),inference(resolution,[status(thm)],[c45099, c25198])).
% 66.33/66.51 cnf(c46865,plain,big_p(skolem0004)|big_q(skolem0010)|big_q(X4720)|big_p(skolem0009)|big_q(skolem0024),inference(factor,[status(thm)],[c45212])).
% 66.33/66.51 cnf(c47146,plain,big_p(skolem0004)|big_q(skolem0010)|big_p(skolem0009)|big_q(skolem0024),inference(factor,[status(thm)],[c46865])).
% 66.33/66.51 cnf(c47395,plain,big_p(skolem0004)|big_q(skolem0010)|big_q(skolem0024)|big_p(X4722)|big_q(X4721),inference(resolution,[status(thm)],[c47146, c45099])).
% 66.33/66.51 cnf(c47435,plain,big_p(skolem0004)|big_q(skolem0010)|big_q(skolem0024)|big_q(X4730),inference(factor,[status(thm)],[c47395])).
% 66.33/66.51 cnf(c47760,plain,big_p(skolem0004)|big_q(skolem0010)|big_q(skolem0024),inference(factor,[status(thm)],[c47435])).
% 66.33/66.51 cnf(c47972,plain,big_p(skolem0004)|big_q(skolem0024)|~big_p(X4746)|big_p(X4745)|big_q(X4744)|big_q(X4743),inference(resolution,[status(thm)],[c47760, c141])).
% 66.33/66.51 cnf(c48056,plain,big_p(skolem0004)|big_q(skolem0024)|big_p(X4809)|big_q(X4810)|big_q(X4808)|big_p(skolem0009),inference(resolution,[status(thm)],[c47972, c25198])).
% 66.33/66.51 cnf(c49009,plain,big_p(skolem0004)|big_q(skolem0024)|big_q(X4811)|big_q(X4812)|big_p(skolem0009),inference(factor,[status(thm)],[c48056])).
% 66.33/66.51 cnf(c49363,plain,big_p(skolem0004)|big_q(skolem0024)|big_q(X4813)|big_p(skolem0009),inference(factor,[status(thm)],[c49009])).
% 66.33/66.51 cnf(c49630,plain,big_p(skolem0004)|big_q(skolem0024)|big_p(skolem0009),inference(factor,[status(thm)],[c49363])).
% 66.33/66.51 cnf(c49848,plain,big_p(skolem0004)|big_q(skolem0024)|big_p(X4822)|big_q(X4823)|big_q(X4821),inference(resolution,[status(thm)],[c49630, c47972])).
% 66.33/66.51 cnf(c49871,plain,big_p(skolem0004)|big_q(skolem0024)|big_q(X4824)|big_q(X4825),inference(factor,[status(thm)],[c49848])).
% 66.33/66.51 cnf(c50208,plain,big_p(skolem0004)|big_q(skolem0024)|big_q(X4826),inference(factor,[status(thm)],[c49871])).
% 66.33/66.51 cnf(c50460,plain,big_p(skolem0004)|big_q(skolem0024),inference(factor,[status(thm)],[c50208])).
% 66.33/66.51 cnf(c52782,plain,big_p(X5137)|big_q(skolem0010)|big_p(X5139)|big_p(X5140)|big_q(X5138)|big_q(skolem0024),inference(resolution,[status(thm)],[c52561, c50460])).
% 66.33/66.51 cnf(c52787,plain,big_p(X5143)|big_q(skolem0010)|big_p(X5142)|big_q(X5141)|big_q(skolem0024),inference(factor,[status(thm)],[c52782])).
% 66.33/66.51 cnf(c53172,plain,big_p(X5144)|big_q(skolem0010)|big_q(X5145)|big_q(skolem0024),inference(factor,[status(thm)],[c52787])).
% 66.33/66.51 cnf(c53478,plain,big_p(X5146)|big_q(skolem0010)|big_q(skolem0024),inference(factor,[status(thm)],[c53172])).
% 66.33/66.51 cnf(c53793,plain,big_p(X5481)|big_q(skolem0024)|~big_p(skolem0004)|big_p(X5483)|big_p(X5482)|big_q(X5484)|big_q(X5485),inference(resolution,[status(thm)],[c53478, c136])).
% 66.33/66.51 cnf(c56061,plain,big_p(X5488)|big_q(skolem0024)|big_p(X5487)|big_p(X5489)|big_q(X5486)|big_q(X5490),inference(resolution,[status(thm)],[c53793, c50460])).
% 66.33/66.51 cnf(c56067,plain,big_p(X5498)|big_q(skolem0024)|big_p(X5499)|big_q(X5496)|big_q(X5497),inference(factor,[status(thm)],[c56061])).
% 66.33/66.51 cnf(c56478,plain,big_p(X5500)|big_q(skolem0024)|big_q(X5501)|big_q(X5502),inference(factor,[status(thm)],[c56067])).
% 66.33/66.51 cnf(c56814,plain,big_p(X5503)|big_q(skolem0024)|big_q(X5504),inference(factor,[status(thm)],[c56478])).
% 66.33/66.51 cnf(c57075,plain,big_p(X5505)|big_q(skolem0024),inference(factor,[status(thm)],[c56814])).
% 66.33/66.51 cnf(c57306,plain,big_p(X6249)|big_p(X6246)|big_p(skolem0013(X6246))|big_p(X6248)|big_p(skolem0023)|big_q(X6247)|big_q(X6250),inference(resolution,[status(thm)],[c57075, c196])).
% 66.33/66.51 cnf(c57508,plain,big_p(X6257)|big_p(skolem0013(X6257))|big_p(X6258)|big_p(skolem0023)|big_q(X6259)|big_q(X6260),inference(factor,[status(thm)],[c57306])).
% 66.33/66.51 cnf(c57899,plain,big_p(X6261)|big_p(skolem0013(X6261))|big_p(skolem0023)|big_q(X6262)|big_q(X6263),inference(factor,[status(thm)],[c57508])).
% 66.33/66.51 cnf(c58225,plain,big_p(X6265)|big_p(skolem0013(X6265))|big_p(skolem0023)|big_q(X6264),inference(factor,[status(thm)],[c57899])).
% 66.33/66.51 cnf(c58484,plain,big_p(skolem0023)|big_p(skolem0013(skolem0023))|big_q(X6266),inference(factor,[status(thm)],[c58225])).
% 66.33/66.51 cnf(c58676,plain,big_p(skolem0023)|big_q(X6324)|big_p(skolem0004)|big_q(skolem0010)|big_p(X6325)|big_q(X6323),inference(resolution,[status(thm)],[c58484, c45099])).
% 66.33/66.51 cnf(c58775,plain,big_p(skolem0023)|big_q(X6326)|big_p(skolem0004)|big_q(skolem0010)|big_q(X6327),inference(factor,[status(thm)],[c58676])).
% 66.33/66.51 cnf(c59062,plain,big_p(skolem0023)|big_q(skolem0010)|big_p(skolem0004)|big_q(X6328),inference(factor,[status(thm)],[c58775])).
% 66.33/66.51 cnf(c59287,plain,big_p(skolem0023)|big_q(skolem0010)|big_p(skolem0004),inference(factor,[status(thm)],[c59062])).
% 66.33/66.51 cnf(c59427,plain,big_q(skolem0010)|big_p(skolem0004)|big_p(X6335)|big_q(X6334),inference(resolution,[status(thm)],[c59287, c45099])).
% 66.33/66.51 cnf(c59483,plain,big_q(skolem0010)|big_p(skolem0004)|big_p(X6336),inference(factor,[status(thm)],[c59427])).
% 66.33/66.51 cnf(c59670,plain,big_q(skolem0010)|big_p(skolem0004),inference(factor,[status(thm)],[c59483])).
% 66.33/66.51 cnf(c59803,plain,big_q(skolem0010)|big_p(X6351)|big_p(X6353)|big_p(X6354)|big_q(X6352),inference(resolution,[status(thm)],[c59670, c52561])).
% 66.33/66.51 cnf(c59834,plain,big_q(skolem0010)|big_p(X6355)|big_p(X6357)|big_p(X6356),inference(factor,[status(thm)],[c59803])).
% 66.33/66.51 cnf(c60087,plain,big_q(skolem0010)|big_p(X6364)|big_p(X6365),inference(factor,[status(thm)],[c59834])).
% 66.33/66.51 cnf(c60266,plain,big_q(skolem0010)|big_p(X6366),inference(factor,[status(thm)],[c60087])).
% 66.33/66.51 cnf(c60394,plain,big_p(X6487)|~big_p(skolem0004)|big_p(X6488)|big_p(X6486)|big_q(X6489)|big_q(X6490),inference(resolution,[status(thm)],[c60266, c136])).
% 66.33/66.51 cnf(c59779,plain,big_p(skolem0004)|~big_p(X6350)|big_p(X6349)|big_q(X6348)|big_q(X6347),inference(resolution,[status(thm)],[c59670, c141])).
% 66.33/66.51 cnf(c59832,plain,big_p(skolem0004)|big_p(X6545)|big_q(X6547)|big_q(X6546)|big_p(skolem0023)|big_q(X6544),inference(resolution,[status(thm)],[c59779, c58484])).
% 66.33/66.51 cnf(c60459,plain,big_p(skolem0004)|big_q(X6550)|big_q(X6549)|big_p(skolem0023)|big_q(X6548),inference(factor,[status(thm)],[c59832])).
% 66.33/66.51 cnf(c60711,plain,big_p(skolem0004)|big_q(X6551)|big_p(skolem0023)|big_q(X6552),inference(factor,[status(thm)],[c60459])).
% 66.33/66.51 cnf(c60917,plain,big_p(skolem0004)|big_q(X6553)|big_p(skolem0023),inference(factor,[status(thm)],[c60711])).
% 66.33/66.51 cnf(c61135,plain,big_p(skolem0004)|big_q(X6567)|big_p(X6565)|big_q(X6568)|big_q(X6566),inference(resolution,[status(thm)],[c60917, c59779])).
% 66.33/66.51 cnf(c61138,plain,big_p(skolem0004)|big_q(X6569)|big_q(X6571)|big_q(X6570),inference(factor,[status(thm)],[c61135])).
% 66.33/66.51 cnf(c61381,plain,big_p(skolem0004)|big_q(X6572)|big_q(X6573),inference(factor,[status(thm)],[c61138])).
% 66.33/66.51 cnf(c61573,plain,big_p(skolem0004)|big_q(X6580),inference(factor,[status(thm)],[c61381])).
% 66.33/66.51 cnf(c61708,plain,big_q(X6623)|big_p(X6625)|big_p(X6622)|big_p(X6626)|big_q(X6621)|big_q(X6624),inference(resolution,[status(thm)],[c61573, c60394])).
% 66.33/66.51 cnf(c61767,plain,big_q(X6628)|big_p(X6630)|big_p(X6631)|big_p(X6627)|big_q(X6629),inference(factor,[status(thm)],[c61708])).
% 66.33/66.51 cnf(c61983,plain,big_q(X6634)|big_p(X6635)|big_p(X6632)|big_p(X6633),inference(factor,[status(thm)],[c61767])).
% 66.33/66.51 cnf(c62146,plain,big_q(X6642)|big_p(X6641)|big_p(X6643),inference(factor,[status(thm)],[c61983])).
% 66.33/66.51 cnf(c62262,plain,big_q(X6645)|big_p(X6644),inference(factor,[status(thm)],[c62146])).
% 66.33/66.51 cnf(c39,negated_conjecture,~big_p(skolem0004)|big_p(X215)|~big_q(X218)|big_p(X217)|~big_q(X216)|~big_q(skolem0007(X216))|~big_p(X219)|~big_q(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 66.33/66.51 cnf(c154,plain,~big_p(skolem0004)|big_p(X221)|~big_q(skolem0007(X222))|big_p(X220)|~big_q(X222)|~big_p(X223)|~big_q(skolem0008),inference(factor,[status(thm)],[c39])).
% 66.33/66.51 cnf(c62315,plain,big_p(X7297)|~big_p(skolem0004)|big_p(X7295)|big_p(X7296)|~big_q(X7299)|~big_p(X7298)|~big_q(skolem0008),inference(resolution,[status(thm)],[c62262, c154])).
% 66.33/66.51 cnf(c62346,plain,big_p(X7306)|~big_p(skolem0004)|big_p(X7304)|big_p(X7305)|~big_q(skolem0008)|~big_p(X7307),inference(factor,[status(thm)],[c62315])).
% 66.33/66.51 cnf(c62348,plain,big_p(X7309)|~big_p(skolem0004)|big_p(X7310)|big_p(X7308)|~big_q(skolem0008),inference(factor,[status(thm)],[c62346])).
% 66.33/66.51 cnf(c62350,plain,big_p(X7311)|~big_p(skolem0004)|big_p(X7313)|big_p(X7314)|big_p(X7312),inference(resolution,[status(thm)],[c62348, c62262])).
% 66.33/66.51 cnf(c55,negated_conjecture,~big_p(X308)|big_p(skolem0004)|~big_q(X311)|big_p(X310)|~big_q(X309)|~big_q(skolem0007(X309))|~big_p(X312)|~big_q(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 66.33/66.51 cnf(c167,plain,~big_p(X314)|big_p(skolem0004)|~big_q(skolem0007(X313))|big_p(X315)|~big_q(X313)|~big_p(X316)|~big_q(skolem0008),inference(factor,[status(thm)],[c55])).
% 66.33/66.51 cnf(c61722,plain,big_p(skolem0004)|~big_p(X6817)|big_p(X6815)|~big_q(X6816)|~big_p(X6814)|~big_q(skolem0008),inference(resolution,[status(thm)],[c61573, c167])).
% 66.33/66.51 cnf(c62340,plain,big_p(skolem0004)|~big_p(X6819)|big_p(X6820)|~big_q(skolem0008)|~big_p(X6818),inference(factor,[status(thm)],[c61722])).
% 66.33/66.51 cnf(c62342,plain,big_p(skolem0004)|~big_p(X6827)|big_p(X6826)|~big_q(skolem0008),inference(factor,[status(thm)],[c62340])).
% 66.33/66.51 cnf(c62344,plain,big_p(skolem0004)|~big_p(X6830)|big_p(X6828)|big_p(X6829),inference(resolution,[status(thm)],[c62342, c62262])).
% 66.33/66.51 cnf(c88,negated_conjecture,big_p(X862)|big_p(skolem0013(X862))|~big_q(X860)|big_p(X861)|~big_q(X859)|~big_q(skolem0019(X859))|~big_q(skolem0020)|big_p(skolem0021),inference(split_conjunct,[status(thm)],[c6])).
% 66.33/66.51 cnf(c1176,plain,big_p(X864)|big_p(skolem0013(X864))|~big_q(skolem0019(X863))|big_p(X865)|~big_q(X863)|~big_q(skolem0020)|big_p(skolem0021),inference(factor,[status(thm)],[c88])).
% 66.33/66.51 cnf(c62323,plain,big_p(X8783)|big_p(X8784)|big_p(skolem0013(X8784))|big_p(X8782)|~big_q(X8785)|~big_q(skolem0020)|big_p(skolem0021),inference(resolution,[status(thm)],[c62262, c1176])).
% 66.33/66.51 cnf(c62366,plain,big_p(X8786)|big_p(X8788)|big_p(skolem0013(X8788))|big_p(X8787)|~big_q(skolem0020)|big_p(skolem0021),inference(factor,[status(thm)],[c62323])).
% 66.33/66.51 cnf(c62368,plain,big_p(X8797)|big_p(X8795)|big_p(skolem0013(X8795))|big_p(X8798)|big_p(skolem0021)|big_p(X8796),inference(resolution,[status(thm)],[c62366, c62262])).
% 66.33/66.51 cnf(c62369,plain,big_p(X8801)|big_p(skolem0013(X8801))|big_p(X8800)|big_p(skolem0021)|big_p(X8799),inference(factor,[status(thm)],[c62368])).
% 66.33/66.51 cnf(c62423,plain,big_p(X8802)|big_p(skolem0013(X8802))|big_p(skolem0021)|big_p(X8803),inference(factor,[status(thm)],[c62369])).
% 66.33/66.51 cnf(c62464,plain,big_p(X8804)|big_p(skolem0013(X8804))|big_p(skolem0021),inference(factor,[status(thm)],[c62423])).
% 66.33/66.51 cnf(c62490,plain,big_p(skolem0021)|big_p(skolem0013(skolem0021)),inference(factor,[status(thm)],[c62464])).
% 66.33/66.51 cnf(c62507,plain,big_p(skolem0021)|big_p(skolem0004)|big_p(X8813)|big_p(X8814),inference(resolution,[status(thm)],[c62490, c62344])).
% 66.33/66.51 cnf(c62510,plain,big_p(skolem0021)|big_p(skolem0004)|big_p(X8815),inference(factor,[status(thm)],[c62507])).
% 66.33/66.51 cnf(c62536,plain,big_p(skolem0021)|big_p(skolem0004),inference(factor,[status(thm)],[c62510])).
% 66.33/66.51 cnf(c62550,plain,big_p(skolem0004)|big_p(X8822)|big_p(X8823),inference(resolution,[status(thm)],[c62536, c62344])).
% 66.33/66.51 cnf(c62553,plain,big_p(skolem0004)|big_p(X8824),inference(factor,[status(thm)],[c62550])).
% 66.33/66.51 cnf(c62573,plain,big_p(skolem0004),inference(factor,[status(thm)],[c62553])).
% 66.33/66.51 cnf(c62583,plain,big_p(X8840)|big_p(X8841)|big_p(X8839)|big_p(X8842),inference(resolution,[status(thm)],[c62573, c62350])).
% 66.33/66.51 cnf(c62584,plain,big_p(X8845)|big_p(X8843)|big_p(X8844),inference(factor,[status(thm)],[c62583])).
% 66.33/66.51 cnf(c62614,plain,big_p(X8846)|big_p(X8847),inference(factor,[status(thm)],[c62584])).
% 66.33/66.51 cnf(c62632,plain,big_p(X8848),inference(factor,[status(thm)],[c62614])).
% 66.33/66.51 cnf(c11,negated_conjecture,~big_p(X131)|~big_p(skolem0001(X131))|~big_q(X129)|~big_p(skolem0002)|~big_q(skolem0010)|big_q(X132)|~big_p(X128)|big_q(X130),inference(split_conjunct,[status(thm)],[c6])).
% 66.33/66.51 cnf(c145,plain,~big_p(X137)|~big_p(skolem0001(X137))|~big_q(X140)|~big_p(skolem0002)|~big_q(skolem0010)|big_q(X138)|big_q(X139),inference(factor,[status(thm)],[c11])).
% 66.33/66.51 cnf(c62643,plain,~big_p(X9055)|~big_q(X9054)|~big_p(skolem0002)|~big_q(skolem0010)|big_q(X9057)|big_q(X9056),inference(resolution,[status(thm)],[c62632, c145])).
% 66.33/66.51 cnf(c62647,plain,~big_p(X9063)|~big_q(skolem0010)|~big_p(skolem0002)|big_q(X9062)|big_q(X9061),inference(factor,[status(thm)],[c62643])).
% 66.33/66.51 cnf(c62649,plain,~big_p(X9064)|~big_q(skolem0010)|big_q(X9065)|big_q(X9066),inference(resolution,[status(thm)],[c62647, c62632])).
% 66.33/66.51 cnf(c13,negated_conjecture,~big_p(X148)|~big_p(skolem0001(X148))|~big_q(X146)|~big_p(skolem0002)|~big_q(X144)|big_q(skolem0010)|~big_p(X145)|big_q(X147),inference(split_conjunct,[status(thm)],[c6])).
% 66.33/66.51 cnf(c147,plain,~big_p(X152)|~big_p(skolem0001(X152))|~big_q(X149)|~big_p(skolem0002)|~big_q(X151)|big_q(skolem0010)|big_q(X150),inference(factor,[status(thm)],[c13])).
% 66.33/66.51 cnf(c60431,plain,big_q(skolem0010)|~big_p(X6767)|~big_q(X6766)|~big_p(skolem0002)|~big_q(X6768)|big_q(X6765),inference(resolution,[status(thm)],[c60266, c147])).
% 66.33/66.51 cnf(c62334,plain,big_q(skolem0010)|~big_p(X6769)|~big_q(X6770)|~big_p(skolem0002)|big_q(X6771),inference(factor,[status(thm)],[c60431])).
% 66.33/66.51 cnf(c62336,plain,big_q(skolem0010)|~big_p(skolem0002)|~big_q(X6773)|big_q(X6772),inference(factor,[status(thm)],[c62334])).
% 66.33/66.51 cnf(c81,negated_conjecture,~big_p(X836)|~big_p(skolem0013(X836))|~big_p(skolem0014)|big_q(skolem0015)|big_q(X834)|big_q(skolem0019(X834))|~big_p(X837)|big_q(X835),inference(split_conjunct,[status(thm)],[c6])).
% 66.33/66.51 cnf(c1157,plain,~big_p(X838)|~big_p(skolem0013(X838))|~big_p(skolem0014)|big_q(skolem0015)|big_q(X840)|big_q(skolem0019(X840))|big_q(X839),inference(factor,[status(thm)],[c81])).
% 66.33/66.51 cnf(c62644,plain,~big_p(X9110)|~big_p(skolem0014)|big_q(skolem0015)|big_q(X9111)|big_q(skolem0019(X9111))|big_q(X9109),inference(resolution,[status(thm)],[c62632, c1157])).
% 66.33/66.51 cnf(c62651,plain,~big_p(X9114)|big_q(skolem0015)|big_q(X9113)|big_q(skolem0019(X9113))|big_q(X9112),inference(resolution,[status(thm)],[c62644, c62632])).
% 66.33/66.51 cnf(c62652,plain,big_q(skolem0015)|big_q(X9116)|big_q(skolem0019(X9116))|big_q(X9115),inference(resolution,[status(thm)],[c62651, c62632])).
% 66.33/66.51 cnf(c62654,plain,big_q(skolem0015)|big_q(X9121)|big_q(skolem0019(X9121)),inference(factor,[status(thm)],[c62652])).
% 66.33/66.51 cnf(c62674,plain,big_q(skolem0015)|big_q(skolem0019(skolem0015)),inference(factor,[status(thm)],[c62654])).
% 66.33/66.51 cnf(c62689,plain,big_q(skolem0015)|big_q(skolem0010)|~big_p(skolem0002)|big_q(X9128),inference(resolution,[status(thm)],[c62674, c62336])).
% 66.33/66.51 cnf(c62691,plain,big_q(skolem0015)|big_q(skolem0010)|big_q(X9129),inference(resolution,[status(thm)],[c62689, c62632])).
% 66.33/66.51 cnf(c62692,plain,big_q(skolem0015)|big_q(skolem0010),inference(factor,[status(thm)],[c62691])).
% 66.33/66.51 cnf(c62705,plain,big_q(skolem0010)|~big_p(skolem0002)|big_q(X9130),inference(resolution,[status(thm)],[c62692, c62336])).
% 66.33/66.51 cnf(c62710,plain,big_q(skolem0010)|big_q(X9134),inference(resolution,[status(thm)],[c62705, c62632])).
% 66.33/66.51 cnf(c62711,plain,big_q(skolem0010),inference(factor,[status(thm)],[c62710])).
% 66.33/66.51 cnf(c62717,plain,~big_p(X9136)|big_q(X9135)|big_q(X9137),inference(resolution,[status(thm)],[c62711, c62649])).
% 66.33/66.51 cnf(c62718,plain,big_q(X9139)|big_q(X9138),inference(resolution,[status(thm)],[c62717, c62632])).
% 66.33/66.51 cnf(c62719,plain,big_q(X9140),inference(factor,[status(thm)],[c62718])).
% 66.33/66.51 cnf(c7,negated_conjecture,~big_p(X83)|~big_p(skolem0001(X83))|~big_q(X82)|~big_p(skolem0002)|~big_q(X80)|~big_q(skolem0007(X80))|~big_p(X81)|~big_q(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 66.33/66.51 cnf(c139,plain,~big_p(X124)|~big_p(skolem0001(X124))|~big_q(skolem0007(X122))|~big_p(skolem0002)|~big_q(X122)|~big_p(X123)|~big_q(skolem0008),inference(factor,[status(thm)],[c7])).
% 66.33/66.51 cnf(c62722,plain,~big_p(X9266)|~big_p(skolem0001(X9266))|~big_p(skolem0002)|~big_q(X9265)|~big_p(X9267)|~big_q(skolem0008),inference(resolution,[status(thm)],[c62719, c139])).
% 66.33/66.51 cnf(c62724,plain,~big_p(X9274)|~big_p(skolem0002)|~big_q(X9273)|~big_p(X9275)|~big_q(skolem0008),inference(resolution,[status(thm)],[c62722, c62632])).
% 66.33/66.51 cnf(c62726,plain,~big_p(X9278)|~big_p(skolem0002)|~big_q(X9277)|~big_p(X9276),inference(resolution,[status(thm)],[c62724, c62719])).
% 66.33/66.51 cnf(c62727,plain,~big_p(X9279)|~big_p(skolem0002)|~big_q(X9280),inference(factor,[status(thm)],[c62726])).
% 66.33/66.51 cnf(c62730,plain,~big_p(X9281)|~big_p(skolem0002),inference(resolution,[status(thm)],[c62727, c62719])).
% 66.33/66.51 cnf(c62732,plain,~big_p(X9282),inference(resolution,[status(thm)],[c62730, c62632])).
% 66.33/66.51 cnf(c62733,plain,$false,inference(resolution,[status(thm)],[c62732, c62632])).
% 66.33/66.51 % SZS output end CNFRefutation
% 66.33/66.51
% 66.33/66.51 % Initial clauses : 128
% 66.33/66.51 % Processed clauses : 731
% 66.33/66.51 % Factors computed : 1051
% 66.33/66.51 % Resolvents computed: 61548
% 66.33/66.51 % Tautologies deleted: 215
% 66.33/66.51 % Forward subsumed : 1952
% 66.33/66.51 % Backward subsumed : 728
% 66.33/66.51 % -------- CPU Time ---------
% 66.33/66.51 % User time : 65.892 s
% 66.33/66.51 % System time : 0.263 s
% 66.33/66.51 % Total time : 66.155 s
%------------------------------------------------------------------------------