%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ046-1 : TPTP v8.1.2. Released v2.5.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:37:42 EDT 2024
% Result : Satisfiable 0.49s 0.68s
% Output : Saturation 0.49s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(b_up,axiom,
( ~ state(bb(s(X476),X480),X471,X481,X472,X474,X475,X479,X477,X473,X478,e1(X476,X480),e2(X476,s(X480)))
| state(bb(X476,X480),X471,X481,X472,X474,X475,X479,X477,X473,X478,e1(s(s(X476)),X480),e2(s(s(X476)),s(X480))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',b_up) ).
cnf(b_down,axiom,
( ~ state(bb(X465,X469),X460,X470,X461,X463,X464,X468,X466,X462,X467,e1(s(s(X465)),X469),e2(s(s(X465)),s(X469)))
| state(bb(s(X465),X469),X460,X470,X461,X463,X464,X468,X466,X462,X467,e1(X465,X469),e2(X465,s(X469))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',b_down) ).
cnf(b_left,axiom,
( ~ state(bb(X454,s(X458)),X449,X459,X450,X452,X453,X457,X455,X451,X456,e1(X454,X458),e2(s(X454),X458))
| state(bb(X454,X458),X449,X459,X450,X452,X453,X457,X455,X451,X456,e1(X454,s(s(X458))),e2(s(X454),s(s(X458)))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',b_left) ).
cnf(b_right,axiom,
( ~ state(bb(X443,X447),X438,X448,X439,X441,X442,X446,X444,X440,X445,e1(X443,s(s(X447))),e2(s(X443),s(s(X447))))
| state(bb(X443,s(X447)),X438,X448,X439,X441,X442,X446,X444,X440,X445,e1(X443,X447),e2(s(X443),X447)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',b_right) ).
cnf(h_up,axiom,
( ~ state(X433,X427,X437,X428,X430,h(s(X431),X436),X435,X432,X429,X434,e1(X431,X436),e2(X431,s(X436)))
| state(X433,X427,X437,X428,X430,h(X431,X436),X435,X432,X429,X434,e1(s(X431),X436),e2(s(X431),s(X436))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',h_up) ).
cnf(h_down,axiom,
( ~ state(X422,X416,X426,X417,X419,h(X420,X425),X424,X421,X418,X423,e1(s(X420),X425),e2(s(X420),s(X425)))
| state(X422,X416,X426,X417,X419,h(s(X420),X425),X424,X421,X418,X423,e1(X420,X425),e2(X420,s(X425))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',h_down) ).
cnf(v4_left,axiom,
( ~ state(X411,X405,X415,X406,v4(X409,s(X414)),X408,X413,X410,X407,X412,e1(X409,X414),e2(s(X409),X414))
| state(X411,X405,X415,X406,v4(X409,X414),X408,X413,X410,X407,X412,e1(X409,s(X414)),e2(s(X409),s(X414))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',v4_left) ).
cnf(v4_right,axiom,
( ~ state(X400,X394,X404,X395,v4(X398,X403),X397,X402,X399,X396,X401,e1(X398,s(X403)),e2(s(X398),s(X403)))
| state(X400,X394,X404,X395,v4(X398,s(X403)),X397,X402,X399,X396,X401,e1(X398,X403),e2(s(X398),X403)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',v4_right) ).
cnf(v3_left,axiom,
( ~ state(X389,X383,X393,v3(X387,s(X392)),X385,X386,X391,X388,X384,X390,e1(X387,X392),e2(s(X387),X392))
| state(X389,X383,X393,v3(X387,X392),X385,X386,X391,X388,X384,X390,e1(X387,s(X392)),e2(s(X387),s(X392))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',v3_left) ).
cnf(v3_right,axiom,
( ~ state(X378,X372,X382,v3(X376,X381),X374,X375,X380,X377,X373,X379,e1(X376,s(X381)),e2(s(X376),s(X381)))
| state(X378,X372,X382,v3(X376,s(X381)),X374,X375,X380,X377,X373,X379,e1(X376,X381),e2(s(X376),X381)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',v3_right) ).
cnf(v2_left,axiom,
( ~ state(X368,X361,v2(X366,s(X370)),X362,X364,X365,X369,X367,X363,X371,e1(X366,X370),e2(s(X366),X370))
| state(X368,X361,v2(X366,X370),X362,X364,X365,X369,X367,X363,X371,e1(X366,s(X370)),e2(s(X366),s(X370))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',v2_left) ).
cnf(v2_right,axiom,
( ~ state(X357,X350,v2(X355,X359),X351,X353,X354,X358,X356,X352,X360,e1(X355,s(X359)),e2(s(X355),s(X359)))
| state(X357,X350,v2(X355,s(X359)),X351,X353,X354,X358,X356,X352,X360,e1(X355,X359),e2(s(X355),X359)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',v2_right) ).
cnf(h_left,axiom,
( ~ state(X344,X338,X349,X339,X341,h(X342,s(X348)),X347,X343,X340,X345,e1(X342,X348),X346)
| state(X344,X338,X349,X339,X341,h(X342,X348),X347,X343,X340,X345,e1(X342,s(s(X348))),X346) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',h_left) ).
cnf(h_right,axiom,
( ~ state(X332,X326,X337,X327,X329,h(X330,X336),X335,X331,X328,X333,e1(X330,s(s(X336))),X334)
| state(X332,X326,X337,X327,X329,h(X330,s(X336)),X335,X331,X328,X333,e1(X330,X336),X334) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',h_right) ).
cnf(v4_up,axiom,
( ~ state(X320,X314,X325,X315,v4(s(X318),X324),X317,X323,X319,X316,X321,e1(X318,X324),X322)
| state(X320,X314,X325,X315,v4(X318,X324),X317,X323,X319,X316,X321,e1(s(s(X318)),X324),X322) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',v4_up) ).
cnf(v4_down,axiom,
( ~ state(X308,X302,X313,X303,v4(X306,X312),X305,X311,X307,X304,X309,e1(s(s(X306)),X312),X310)
| state(X308,X302,X313,X303,v4(s(X306),X312),X305,X311,X307,X304,X309,e1(X306,X312),X310) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',v4_down) ).
cnf(v3_up,axiom,
( ~ state(X296,X290,X301,v3(s(X294),X300),X292,X293,X299,X295,X291,X297,e1(X294,X300),X298)
| state(X296,X290,X301,v3(X294,X300),X292,X293,X299,X295,X291,X297,e1(s(s(X294)),X300),X298) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',v3_up) ).
cnf(v1_left,axiom,
( ~ state(X285,v1(X283,s(X288)),X289,X279,X281,X282,X287,X284,X280,X286,e1(X283,X288),e2(s(X283),X288))
| state(X285,v1(X283,X288),X289,X279,X281,X282,X287,X284,X280,X286,e1(X283,s(X288)),e2(s(X283),s(X288))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',v1_left) ).
cnf(v3_down,axiom,
( ~ state(X273,X267,X278,v3(X271,X277),X269,X270,X276,X272,X268,X274,e1(s(s(X271)),X277),X275)
| state(X273,X267,X278,v3(s(X271),X277),X269,X270,X276,X272,X268,X274,e1(X271,X277),X275) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',v3_down) ).
cnf(v2_up,axiom,
( ~ state(X262,X255,v2(s(X260),X265),X256,X258,X259,X264,X261,X257,X266,e1(X260,X265),X263)
| state(X262,X255,v2(X260,X265),X256,X258,X259,X264,X261,X257,X266,e1(s(s(X260)),X265),X263) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',v2_up) ).
cnf(v2_down,axiom,
( ~ state(X250,X243,v2(X248,X253),X244,X246,X247,X252,X249,X245,X254,e1(s(s(X248)),X253),X251)
| state(X250,X243,v2(s(X248),X253),X244,X246,X247,X252,X249,X245,X254,e1(X248,X253),X251) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',v2_down) ).
cnf(v1_up,axiom,
( ~ state(X237,v1(s(X235),X241),X242,X231,X233,X234,X240,X236,X232,X238,e1(X235,X241),X239)
| state(X237,v1(X235,X241),X242,X231,X233,X234,X240,X236,X232,X238,e1(s(s(X235)),X241),X239) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',v1_up) ).
cnf(v1_down,axiom,
( ~ state(X225,v1(X223,X229),X230,X219,X221,X222,X228,X224,X220,X226,e1(s(s(X223)),X229),X227)
| state(X225,v1(s(X223),X229),X230,X219,X221,X222,X228,X224,X220,X226,e1(X223,X229),X227) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',v1_down) ).
cnf(v1_right,axiom,
( ~ state(X214,v1(X212,X217),X218,X208,X210,X211,X216,X213,X209,X215,e1(X212,s(X217)),e2(s(X212),s(X217)))
| state(X214,v1(X212,s(X217)),X218,X208,X210,X211,X216,X213,X209,X215,e1(X212,X217),e2(s(X212),X217)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',v1_right) ).
cnf(s4_up,axiom,
( ~ state(X203,X196,X207,X197,X199,X200,X205,X201,X198,s4(s(X202),X206),e1(X202,X206),X204)
| state(X203,X196,X207,X197,X199,X200,X205,X201,X198,s4(X202,X206),e1(s(X202),X206),X204) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',s4_up) ).
cnf(s4_down,axiom,
( ~ state(X191,X184,X195,X185,X187,X188,X193,X189,X186,s4(X190,X194),e1(s(X190),X194),X192)
| state(X191,X184,X195,X185,X187,X188,X193,X189,X186,s4(s(X190),X194),e1(X190,X194),X192) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',s4_down) ).
cnf(s4_left,axiom,
( ~ state(X179,X172,X183,X173,X175,X176,X181,X177,X174,s4(X178,s(X182)),e1(X178,X182),X180)
| state(X179,X172,X183,X173,X175,X176,X181,X177,X174,s4(X178,X182),e1(X178,s(X182)),X180) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',s4_left) ).
cnf(s4_right,axiom,
( ~ state(X167,X160,X171,X161,X163,X164,X169,X165,X162,s4(X166,X170),e1(X166,s(X170)),X168)
| state(X167,X160,X171,X161,X163,X164,X169,X165,X162,s4(X166,s(X170)),e1(X166,X170),X168) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',s4_right) ).
cnf(s3_up,axiom,
( ~ state(X154,X148,X159,X149,X150,X151,X157,X152,s3(s(X153),X158),X155,e1(X153,X158),X156)
| state(X154,X148,X159,X149,X150,X151,X157,X152,s3(X153,X158),X155,e1(s(X153),X158),X156) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',s3_up) ).
cnf(s3_down,axiom,
( ~ state(X142,X136,X147,X137,X138,X139,X145,X140,s3(X141,X146),X143,e1(s(X141),X146),X144)
| state(X142,X136,X147,X137,X138,X139,X145,X140,s3(s(X141),X146),X143,e1(X141,X146),X144) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',s3_down) ).
cnf(s3_left,axiom,
( ~ state(X130,X124,X135,X125,X126,X127,X133,X128,s3(X129,s(X134)),X131,e1(X129,X134),X132)
| state(X130,X124,X135,X125,X126,X127,X133,X128,s3(X129,X134),X131,e1(X129,s(X134)),X132) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',s3_left) ).
cnf(s3_right,axiom,
( ~ state(X118,X112,X123,X113,X114,X115,X121,X116,s3(X117,X122),X119,e1(X117,s(X122)),X120)
| state(X118,X112,X123,X113,X114,X115,X121,X116,s3(X117,s(X122)),X119,e1(X117,X122),X120) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',s3_right) ).
cnf(s2_up,axiom,
( ~ state(X106,X100,X111,X101,X103,X104,X109,s2(s(X105),X110),X102,X107,e1(X105,X110),X108)
| state(X106,X100,X111,X101,X103,X104,X109,s2(X105,X110),X102,X107,e1(s(X105),X110),X108) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',s2_up) ).
cnf(s2_down,axiom,
( ~ state(X94,X88,X99,X89,X91,X92,X97,s2(X93,X98),X90,X95,e1(s(X93),X98),X96)
| state(X94,X88,X99,X89,X91,X92,X97,s2(s(X93),X98),X90,X95,e1(X93,X98),X96) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',s2_down) ).
cnf(s2_left,axiom,
( ~ state(X82,X76,X87,X77,X79,X80,X85,s2(X81,s(X86)),X78,X83,e1(X81,X86),X84)
| state(X82,X76,X87,X77,X79,X80,X85,s2(X81,X86),X78,X83,e1(X81,s(X86)),X84) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',s2_left) ).
cnf(s2_right,axiom,
( ~ state(X70,X64,X75,X65,X67,X68,X73,s2(X69,X74),X66,X71,e1(X69,s(X74)),X72)
| state(X70,X64,X75,X65,X67,X68,X73,s2(X69,s(X74)),X66,X71,e1(X69,X74),X72) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',s2_right) ).
cnf(s1_up,axiom,
( ~ state(X59,X52,X63,X53,X55,X56,s1(s(X57),X62),X58,X54,X60,e1(X57,X62),X61)
| state(X59,X52,X63,X53,X55,X56,s1(X57,X62),X58,X54,X60,e1(s(X57),X62),X61) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',s1_up) ).
cnf(s1_down,axiom,
( ~ state(X47,X40,X51,X41,X43,X44,s1(X45,X50),X46,X42,X48,e1(s(X45),X50),X49)
| state(X47,X40,X51,X41,X43,X44,s1(s(X45),X50),X46,X42,X48,e1(X45,X50),X49) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',s1_down) ).
cnf(s1_left,axiom,
( ~ state(X35,X28,X39,X29,X31,X32,s1(X33,s(X38)),X34,X30,X36,e1(X33,X38),X37)
| state(X35,X28,X39,X29,X31,X32,s1(X33,X38),X34,X30,X36,e1(X33,s(X38)),X37) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',s1_left) ).
cnf(s1_right,axiom,
( ~ state(X23,X16,X27,X17,X19,X20,s1(X21,X26),X22,X18,X24,e1(X21,s(X26)),X25)
| state(X23,X16,X27,X17,X19,X20,s1(X21,s(X26)),X22,X18,X24,e1(X21,X26),X25) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',s1_right) ).
cnf(swap_blanks,axiom,
( ~ state(X11,X2,X15,X3,X6,X7,X13,X8,X4,X12,e1(X9,X14),e2(X5,X10))
| state(X11,X2,X15,X3,X6,X7,X13,X8,X4,X12,e1(X5,X10),e2(X9,X14)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ004-0.ax',swap_blanks) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : PUZ046-1 : TPTP v8.1.2. Released v2.5.0.
% 0.13/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n004.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 20:40:08 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.49/0.68 % Version: 1.5
% 0.49/0.68 % SZS status Satisfiable
% 0.49/0.68 % SZS output start Saturation
% See solution above
% 0.49/0.68
% 0.49/0.68 % Initial clauses : 41
% 0.49/0.68 % Processed clauses : 41
% 0.49/0.68 % Factors computed : 0
% 0.49/0.68 % Resolvents computed: 0
% 0.49/0.68 % Tautologies deleted: 0
% 0.49/0.68 % Forward subsumed : 0
% 0.49/0.68 % Backward subsumed : 0
% 0.49/0.68 % -------- CPU Time ---------
% 0.49/0.68 % User time : 0.310 s
% 0.49/0.68 % System time : 0.012 s
% 0.49/0.68 % Total time : 0.322 s
%------------------------------------------------------------------------------