%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL095-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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 : Mon Sep 7 12:57:50 PM UTC 2026
% Result : Unsatisfiable 127.55s 127.85s
% Output : CNFRefutation 127.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 3
% Syntax : Number of clauses : 89 ( 56 unt; 0 nHn; 5 RR)
% Number of literals : 123 ( 0 equ; 35 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 401 ( 259 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_ic_5,negated_conjecture,
~ is_a_theorem(implies(a,implies(implies(a,b),b))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_ic_5) ).
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X3,X2))
| ~ is_a_theorem(X3)
| is_a_theorem(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condensed_detachment) ).
cnf(ic_JLukasiewicz_5,axiom,
is_a_theorem(implies(implies(implies(X7,X5),implies(X8,X6)),implies(implies(X6,X7),implies(X4,implies(X8,X7))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ic_JLukasiewicz_5) ).
cnf(c0,plain,
( ~ is_a_theorem(implies(implies(X9,X12),implies(X11,X10)))
| is_a_theorem(implies(implies(X10,X9),implies(X13,implies(X11,X9)))) ),
inference(resolution,[status(thm)],[ic_JLukasiewicz_5,condensed_detachment]) ).
cnf(c1,plain,
is_a_theorem(implies(implies(implies(X19,implies(X15,X14)),implies(X14,X17)),implies(X18,implies(implies(X16,X14),implies(X14,X17))))),
inference(resolution,[status(thm)],[c0,ic_JLukasiewicz_5]) ).
cnf(c2,plain,
( ~ is_a_theorem(implies(implies(X23,implies(X20,X24)),implies(X24,X21)))
| is_a_theorem(implies(X22,implies(implies(X25,X24),implies(X24,X21)))) ),
inference(resolution,[status(thm)],[c1,condensed_detachment]) ).
cnf(c4,plain,
is_a_theorem(implies(X27,implies(implies(X28,X26),implies(X26,implies(implies(X30,X29),implies(X29,X26)))))),
inference(resolution,[status(thm)],[c2,c1]) ).
cnf(c6,plain,
( ~ is_a_theorem(X34)
| is_a_theorem(implies(implies(X31,X33),implies(X33,implies(implies(X35,X32),implies(X32,X33))))) ),
inference(resolution,[status(thm)],[c4,condensed_detachment]) ).
cnf(c8,plain,
is_a_theorem(implies(implies(X36,X39),implies(X39,implies(implies(X37,X38),implies(X38,X39))))),
inference(resolution,[status(thm)],[c6,ic_JLukasiewicz_5]) ).
cnf(c12,plain,
is_a_theorem(implies(implies(implies(implies(X60,X59),implies(X59,X61)),X63),implies(X62,implies(X61,X63)))),
inference(resolution,[status(thm)],[c8,c0]) ).
cnf(c23,plain,
is_a_theorem(implies(X67,implies(implies(X68,X64),implies(X64,implies(X66,implies(X65,X64)))))),
inference(resolution,[status(thm)],[c12,c2]) ).
cnf(c25,plain,
( ~ is_a_theorem(X72)
| is_a_theorem(implies(implies(X70,X73),implies(X73,implies(X69,implies(X71,X73))))) ),
inference(resolution,[status(thm)],[c23,condensed_detachment]) ).
cnf(c29,plain,
is_a_theorem(implies(implies(X74,X75),implies(X75,implies(X77,implies(X76,X75))))),
inference(resolution,[status(thm)],[c25,ic_JLukasiewicz_5]) ).
cnf(c37,plain,
is_a_theorem(implies(implies(implies(X116,implies(X114,X115)),X118),implies(X117,implies(X115,X118)))),
inference(resolution,[status(thm)],[c29,c0]) ).
cnf(c54,plain,
( ~ is_a_theorem(implies(implies(X120,implies(X121,X122)),X123))
| is_a_theorem(implies(X119,implies(X122,X123))) ),
inference(resolution,[status(thm)],[c37,condensed_detachment]) ).
cnf(c59,plain,
is_a_theorem(implies(X204,implies(X201,implies(implies(X201,X200),implies(X203,implies(X202,X200)))))),
inference(resolution,[status(thm)],[c54,ic_JLukasiewicz_5]) ).
cnf(c105,plain,
( ~ is_a_theorem(X235)
| is_a_theorem(implies(X234,implies(implies(X234,X238),implies(X237,implies(X236,X238))))) ),
inference(resolution,[status(thm)],[c59,condensed_detachment]) ).
cnf(c124,plain,
is_a_theorem(implies(X241,implies(implies(X241,X242),implies(X240,implies(X239,X242))))),
inference(resolution,[status(thm)],[c105,c29]) ).
cnf(c139,plain,
( ~ is_a_theorem(X312)
| is_a_theorem(implies(implies(X312,X314),implies(X315,implies(X313,X314)))) ),
inference(resolution,[status(thm)],[c124,condensed_detachment]) ).
cnf(c64,plain,
is_a_theorem(implies(X128,implies(X124,implies(X125,implies(X127,implies(X126,X124)))))),
inference(resolution,[status(thm)],[c54,c37]) ).
cnf(c70,plain,
is_a_theorem(implies(implies(implies(X505,implies(X509,implies(X506,X507))),X510),implies(X508,implies(X507,X510)))),
inference(resolution,[status(thm)],[c64,c0]) ).
cnf(c274,plain,
is_a_theorem(implies(implies(implies(implies(implies(X4816,implies(X4811,implies(X4813,X4815))),X4818),implies(X4810,implies(X4815,X4818))),X4814),implies(X4812,implies(X4817,X4814)))),
inference(resolution,[status(thm)],[c70,c139]) ).
cnf(c160,plain,
is_a_theorem(implies(implies(implies(X2543,implies(X2542,implies(implies(X2542,X2548),implies(X2547,implies(X2545,X2548))))),X2544),implies(X2541,implies(X2546,X2544)))),
inference(resolution,[status(thm)],[c139,c59]) ).
cnf(c35,plain,
( ~ is_a_theorem(implies(X111,X113))
| is_a_theorem(implies(X113,implies(X112,implies(X110,X113)))) ),
inference(resolution,[status(thm)],[c29,condensed_detachment]) ).
cnf(c50,plain,
is_a_theorem(implies(implies(X343,implies(X341,X344)),implies(X342,implies(X340,implies(X343,implies(X341,X344)))))),
inference(resolution,[status(thm)],[c35,c12]) ).
cnf(c180,plain,
is_a_theorem(implies(X350,implies(X345,implies(X348,implies(X349,implies(X346,implies(X347,X345))))))),
inference(resolution,[status(thm)],[c50,c54]) ).
cnf(c188,plain,
( ~ is_a_theorem(X354)
| is_a_theorem(implies(X353,implies(X351,implies(X356,implies(X352,implies(X355,X353)))))) ),
inference(resolution,[status(thm)],[c180,condensed_detachment]) ).
cnf(c195,plain,
is_a_theorem(implies(X360,implies(X359,implies(X358,implies(X361,implies(X357,X360)))))),
inference(resolution,[status(thm)],[c188,c29]) ).
cnf(c212,plain,
( ~ is_a_theorem(X456)
| is_a_theorem(implies(X458,implies(X454,implies(X455,implies(X457,X456))))) ),
inference(resolution,[status(thm)],[c195,condensed_detachment]) ).
cnf(c235,plain,
is_a_theorem(implies(X4098,implies(X4102,implies(X4095,implies(X4103,implies(X4100,implies(implies(X4097,X4101),implies(X4101,implies(X4096,implies(X4099,X4101)))))))))),
inference(resolution,[status(thm)],[c212,c23]) ).
cnf(c3,plain,
is_a_theorem(implies(implies(implies(implies(X54,X53),implies(X53,X49)),implies(X51,implies(X48,X53))),implies(X52,implies(X50,implies(X51,implies(X48,X53)))))),
inference(resolution,[status(thm)],[c1,c0]) ).
cnf(c15,plain,
is_a_theorem(implies(implies(implies(X193,implies(X192,implies(X191,X190))),implies(implies(X187,X190),implies(X190,X194))),implies(X189,implies(X188,implies(implies(X187,X190),implies(X190,X194)))))),
inference(resolution,[status(thm)],[c3,c0]) ).
cnf(c99,plain,
( ~ is_a_theorem(implies(implies(X1586,implies(X1585,implies(X1581,X1584))),implies(implies(X1587,X1584),implies(X1584,X1583))))
| is_a_theorem(implies(X1588,implies(X1582,implies(implies(X1587,X1584),implies(X1584,X1583))))) ),
inference(resolution,[status(thm)],[c15,condensed_detachment]) ).
cnf(c889,plain,
is_a_theorem(implies(X1637,implies(X1636,implies(implies(implies(X1639,X1638),X1638),implies(X1638,implies(X1635,X1638)))))),
inference(resolution,[status(thm)],[c99,ic_JLukasiewicz_5]) ).
cnf(c926,plain,
( ~ is_a_theorem(X1685)
| is_a_theorem(implies(X1686,implies(implies(implies(X1682,X1684),X1684),implies(X1684,implies(X1683,X1684))))) ),
inference(resolution,[status(thm)],[c889,condensed_detachment]) ).
cnf(c937,plain,
is_a_theorem(implies(X1687,implies(implies(implies(X1689,X1688),X1688),implies(X1688,implies(X1690,X1688))))),
inference(resolution,[status(thm)],[c926,c29]) ).
cnf(c990,plain,
( ~ is_a_theorem(X1949)
| is_a_theorem(implies(implies(implies(X1951,X1952),X1952),implies(X1952,implies(X1950,X1952)))) ),
inference(resolution,[status(thm)],[c937,condensed_detachment]) ).
cnf(c1065,plain,
is_a_theorem(implies(implies(implies(X1953,X1954),X1954),implies(X1954,implies(X1955,X1954)))),
inference(resolution,[status(thm)],[c990,c29]) ).
cnf(c1127,plain,
is_a_theorem(implies(implies(implies(X2241,X2239),implies(X2242,X2239)),implies(X2240,implies(X2239,implies(X2242,X2239))))),
inference(resolution,[status(thm)],[c1065,c0]) ).
cnf(c24,plain,
is_a_theorem(implies(implies(implies(X397,X400),implies(implies(X402,X399),implies(X399,X397))),implies(X401,implies(X398,implies(implies(X402,X399),implies(X399,X397)))))),
inference(resolution,[status(thm)],[c12,c0]) ).
cnf(c219,plain,
( ~ is_a_theorem(implies(implies(X3637,X3638),implies(implies(X3633,X3635),implies(X3635,X3637))))
| is_a_theorem(implies(X3634,implies(X3636,implies(implies(X3633,X3635),implies(X3635,X3637))))) ),
inference(resolution,[status(thm)],[c24,condensed_detachment]) ).
cnf(c2004,plain,
is_a_theorem(implies(X3641,implies(X3642,implies(implies(X3643,X3639),implies(X3639,implies(X3640,X3639)))))),
inference(resolution,[status(thm)],[c219,c1127]) ).
cnf(c2041,plain,
( ~ is_a_theorem(X3652)
| is_a_theorem(implies(X3649,implies(implies(X3651,X3650),implies(X3650,implies(X3648,X3650))))) ),
inference(resolution,[status(thm)],[c2004,condensed_detachment]) ).
cnf(c2056,plain,
is_a_theorem(implies(X3654,implies(implies(X3655,X3656),implies(X3656,implies(X3653,X3656))))),
inference(resolution,[status(thm)],[c2041,c15]) ).
cnf(c2141,plain,
( ~ is_a_theorem(X4104)
| is_a_theorem(implies(implies(X4105,X4106),implies(X4106,implies(X4107,X4106)))) ),
inference(resolution,[status(thm)],[c2056,condensed_detachment]) ).
cnf(c2399,plain,
is_a_theorem(implies(implies(X4109,X4110),implies(X4110,implies(X4108,X4110)))),
inference(resolution,[status(thm)],[c2141,c235]) ).
cnf(c2490,plain,
( ~ is_a_theorem(implies(X4515,X4514))
| is_a_theorem(implies(X4514,implies(X4516,X4514))) ),
inference(resolution,[status(thm)],[c2399,condensed_detachment]) ).
cnf(c2686,plain,
is_a_theorem(implies(implies(X5468,implies(X5467,X5470)),implies(X5469,implies(X5468,implies(X5467,X5470))))),
inference(resolution,[status(thm)],[c2490,c160]) ).
cnf(c3590,plain,
is_a_theorem(implies(implies(implies(X6074,implies(X6070,X6071)),X6074),implies(X6073,implies(X6072,X6074)))),
inference(resolution,[status(thm)],[c2686,c0]) ).
cnf(c4056,plain,
( ~ is_a_theorem(implies(implies(X6210,implies(X6208,X6207)),X6210))
| is_a_theorem(implies(X6209,implies(X6211,X6210))) ),
inference(resolution,[status(thm)],[c3590,condensed_detachment]) ).
cnf(c4235,plain,
is_a_theorem(implies(X6216,implies(X6212,implies(X6215,implies(X6213,implies(X6214,X6213)))))),
inference(resolution,[status(thm)],[c4056,c70]) ).
cnf(c4300,plain,
( ~ is_a_theorem(X6224)
| is_a_theorem(implies(X6225,implies(X6222,implies(X6223,implies(X6226,X6223))))) ),
inference(resolution,[status(thm)],[c4235,condensed_detachment]) ).
cnf(c4314,plain,
is_a_theorem(implies(X6238,implies(X6240,implies(X6239,implies(X6237,X6239))))),
inference(resolution,[status(thm)],[c4300,c274]) ).
cnf(c4448,plain,
( ~ is_a_theorem(X6940)
| is_a_theorem(implies(X6939,implies(X6942,implies(X6941,X6942)))) ),
inference(resolution,[status(thm)],[c4314,condensed_detachment]) ).
cnf(c4792,plain,
is_a_theorem(implies(X6954,implies(X6953,implies(X6952,X6953)))),
inference(resolution,[status(thm)],[c4448,c274]) ).
cnf(c4962,plain,
( ~ is_a_theorem(X7576)
| is_a_theorem(implies(X7577,implies(X7578,X7577))) ),
inference(resolution,[status(thm)],[c4792,condensed_detachment]) ).
cnf(c5210,plain,
is_a_theorem(implies(X7591,implies(X7590,X7591))),
inference(resolution,[status(thm)],[c4962,c274]) ).
cnf(c5386,plain,
( ~ is_a_theorem(X8178)
| is_a_theorem(implies(X8177,X8178)) ),
inference(resolution,[status(thm)],[c5210,condensed_detachment]) ).
cnf(c5392,plain,
is_a_theorem(implies(X8448,implies(X8446,implies(implies(X8445,X8447),implies(X8447,X8447))))),
inference(resolution,[status(thm)],[c5210,c219]) ).
cnf(c6124,plain,
( ~ is_a_theorem(X8500)
| is_a_theorem(implies(X8498,implies(implies(X8501,X8499),implies(X8499,X8499)))) ),
inference(resolution,[status(thm)],[c5392,condensed_detachment]) ).
cnf(c6150,plain,
is_a_theorem(implies(X8503,implies(implies(X8504,X8502),implies(X8502,X8502)))),
inference(resolution,[status(thm)],[c6124,c274]) ).
cnf(c6334,plain,
( ~ is_a_theorem(X9296)
| is_a_theorem(implies(implies(X9298,X9297),implies(X9297,X9297))) ),
inference(resolution,[status(thm)],[c6150,condensed_detachment]) ).
cnf(c6873,plain,
is_a_theorem(implies(implies(X9299,X9300),implies(X9300,X9300))),
inference(resolution,[status(thm)],[c6334,c274]) ).
cnf(c7063,plain,
( ~ is_a_theorem(implies(X9975,X9976))
| is_a_theorem(implies(X9976,X9976)) ),
inference(resolution,[status(thm)],[c6873,condensed_detachment]) ).
cnf(c7442,plain,
is_a_theorem(implies(implies(X9986,X9987),implies(X9986,X9987))),
inference(resolution,[status(thm)],[c7063,c5210]) ).
cnf(c7468,plain,
is_a_theorem(implies(implies(X10078,X10076),implies(X10077,implies(X10076,X10076)))),
inference(resolution,[status(thm)],[c7442,c0]) ).
cnf(c7537,plain,
is_a_theorem(implies(implies(implies(X13541,X13541),X13542),implies(X13543,implies(X13540,X13542)))),
inference(resolution,[status(thm)],[c7468,c0]) ).
cnf(c9919,plain,
is_a_theorem(implies(X16035,implies(implies(implies(X16039,X16039),X16038),implies(X16036,implies(X16037,X16038))))),
inference(resolution,[status(thm)],[c7537,c5386]) ).
cnf(c7,plain,
is_a_theorem(implies(implies(implies(X106,implies(implies(X108,X105),implies(X105,X106))),X109),implies(X107,implies(implies(X104,X106),X109)))),
inference(resolution,[status(thm)],[c4,c0]) ).
cnf(c42,plain,
( ~ is_a_theorem(implies(implies(X715,implies(implies(X713,X714),implies(X714,X715))),X711))
| is_a_theorem(implies(X710,implies(implies(X712,X715),X711))) ),
inference(resolution,[status(thm)],[c7,condensed_detachment]) ).
cnf(c402,plain,
is_a_theorem(implies(X6945,implies(implies(X6950,X6943),implies(X6951,implies(X6949,implies(X6948,implies(X6944,implies(X6943,implies(implies(X6947,X6946),implies(X6946,X6943)))))))))),
inference(resolution,[status(thm)],[c42,c195]) ).
cnf(c143,plain,
is_a_theorem(implies(implies(implies(X1537,implies(X1535,X1536)),X1540),implies(X1539,implies(implies(implies(X1540,X1538),X1536),X1540)))),
inference(resolution,[status(thm)],[c124,c0]) ).
cnf(c5398,plain,
is_a_theorem(implies(implies(implies(X8464,X8463),X8464),implies(X8465,implies(X8462,X8464)))),
inference(resolution,[status(thm)],[c5210,c0]) ).
cnf(c6143,plain,
( ~ is_a_theorem(implies(implies(X12960,X12962),X12960))
| is_a_theorem(implies(X12959,implies(X12961,X12960))) ),
inference(resolution,[status(thm)],[c5398,condensed_detachment]) ).
cnf(c9551,plain,
is_a_theorem(implies(X15846,implies(X15847,implies(X15845,implies(implies(implies(X15849,X15848),X15849),X15849))))),
inference(resolution,[status(thm)],[c6143,c143]) ).
cnf(c11463,plain,
( ~ is_a_theorem(X20800)
| is_a_theorem(implies(X20799,implies(X20801,implies(implies(implies(X20798,X20802),X20798),X20798)))) ),
inference(resolution,[status(thm)],[c9551,condensed_detachment]) ).
cnf(c15064,plain,
is_a_theorem(implies(X20805,implies(X20803,implies(implies(implies(X20804,X20806),X20804),X20804)))),
inference(resolution,[status(thm)],[c11463,c402]) ).
cnf(c15414,plain,
( ~ is_a_theorem(X22675)
| is_a_theorem(implies(X22677,implies(implies(implies(X22676,X22678),X22676),X22676))) ),
inference(resolution,[status(thm)],[c15064,condensed_detachment]) ).
cnf(c15706,plain,
is_a_theorem(implies(X22681,implies(implies(implies(X22680,X22679),X22680),X22680))),
inference(resolution,[status(thm)],[c15414,c402]) ).
cnf(c16066,plain,
( ~ is_a_theorem(X24314)
| is_a_theorem(implies(implies(implies(X24313,X24315),X24313),X24313)) ),
inference(resolution,[status(thm)],[c15706,condensed_detachment]) ).
cnf(c17199,plain,
is_a_theorem(implies(implies(implies(X24316,X24317),X24316),X24316)),
inference(resolution,[status(thm)],[c16066,c9919]) ).
cnf(c17568,plain,
( ~ is_a_theorem(implies(implies(X25691,X25692),X25691))
| is_a_theorem(X25691) ),
inference(resolution,[status(thm)],[c17199,condensed_detachment]) ).
cnf(c110,plain,
is_a_theorem(implies(implies(implies(implies(X1442,X1447),implies(X1446,implies(X1443,X1447))),X1445),implies(X1444,implies(X1442,X1445)))),
inference(resolution,[status(thm)],[c59,c0]) ).
cnf(c4192,plain,
is_a_theorem(implies(X14275,implies(X14271,implies(implies(X14272,X14274),implies(X14272,implies(X14273,X14274)))))),
inference(resolution,[status(thm)],[c4056,c110]) ).
cnf(c10661,plain,
( ~ is_a_theorem(X16150)
| is_a_theorem(implies(X16148,implies(implies(X16152,X16151),implies(X16152,implies(X16149,X16151))))) ),
inference(resolution,[status(thm)],[c4192,condensed_detachment]) ).
cnf(c11498,plain,
is_a_theorem(implies(X16153,implies(implies(X16156,X16155),implies(X16156,implies(X16154,X16155))))),
inference(resolution,[status(thm)],[c10661,c274]) ).
cnf(c11794,plain,
is_a_theorem(implies(implies(implies(X56383,implies(X56384,X56381)),X56385),implies(X56382,implies(implies(X56383,X56381),X56385)))),
inference(resolution,[status(thm)],[c11498,c0]) ).
cnf(c54002,plain,
is_a_theorem(implies(X56387,implies(implies(X56387,X56386),X56386))),
inference(resolution,[status(thm)],[c11794,c17568]) ).
cnf(c54048,plain,
$false,
inference(resolution,[status(thm)],[c54002,prove_ic_5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL095-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.35 % Computer : n009.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 5 23:35:21 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.41 (re.compile("\."), Token.FullStop),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.41 (re.compile("\("), Token.OpenPar),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.41 (re.compile("\)"), Token.ClosePar),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.41 (re.compile("\["), Token.OpenSquare),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("~\|"), Token.Nor),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("\|"), Token.Or),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.41 (re.compile("\?"), Token.Existential),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.41 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.41 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.21/0.48 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.48 """
% 0.21/0.48 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.48 """
% 0.31/0.57 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.31/0.57 """
% 127.55/127.85 % Version: 1.5
% 127.55/127.85 % SZS status Unsatisfiable
% 127.55/127.85 % SZS output start CNFRefutation
% See solution above
% 127.55/127.85
% 127.55/127.85 % Initial clauses : 3
% 127.55/127.85 % Processed clauses : 836
% 127.55/127.85 % Factors computed : 0
% 127.55/127.85 % Resolvents computed: 54082
% 127.55/127.85 % Tautologies deleted: 2
% 127.55/127.85 % Forward subsumed : 10421
% 127.55/127.85 % Backward subsumed : 192
% 127.55/127.85 % -------- CPU Time ---------
% 127.55/127.85 % User time : 127.332 s
% 127.55/127.85 % System time : 0.167 s
% 127.55/127.85 % Total time : 127.499 s
%------------------------------------------------------------------------------