%------------------------------------------------------------------------------ % File : Faust---1.0 % Problem : MSC015-1.010 : TPTP v3.4.2. Released v3.5.0. % Transfm : none % Format : tptp % Command : faust %s % Computer : art01.cs.miami.edu % Model : i686 i686 % CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz % Memory : 1003MB % OS : Linux 2.6.17-1.2142_FC4 % CPULimit : 600s % DateTime : Wed May 6 14:19:32 EDT 2009 % Result : Unsatisfiable 3.8s % Output : Refutation 3.8s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % Proof found in: 3 seconds % START OF PROOF SEQUENCE % cnf(rule9,plain, % % cnf(167721408,derived,(~p(A,s0,s1,s1,s1,s1,s1,s1,s1,s1)|p(A,s1,s0,s0,s0,s0,s0,s0,s0,s0)),inference(rewrite,[status(thm)],[rule9]),[]). % % cnf(rule8,plain, % % cnf(167715744,derived,(~p(A,B,s0,s1,s1,s1,s1,s1,s1,s1)|p(A,B,s1,s0,s0,s0,s0,s0,s0,s0)),inference(rewrite,[status(thm)],[rule8]),[]). % % cnf(rule7,plain, % % cnf(167706048,derived,(~p(A,B,C,s0,s1,s1,s1,s1,s1,s1)|p(A,B,C,s1,s0,s0,s0,s0,s0,s0)),inference(rewrite,[status(thm)],[rule7]),[]). % % cnf(rule6,plain, % % cnf(167700408,derived,(~p(A,B,C,D,s0,s1,s1,s1,s1,s1)|p(A,B,C,D,s1,s0,s0,s0,s0,s0)),inference(rewrite,[status(thm)],[rule6]),[]). % % cnf(rule5,plain, % % cnf(167694792,derived,(~p(A,B,C,D,E,s0,s1,s1,s1,s1)|p(A,B,C,D,E,s1,s0,s0,s0,s0)),inference(rewrite,[status(thm)],[rule5]),[]). % % cnf(rule4,plain, % % cnf(167685056,derived,(~p(A,B,C,D,E,F,s0,s1,s1,s1)|p(A,B,C,D,E,F,s1,s0,s0,s0)),inference(rewrite,[status(thm)],[rule4]),[]). % % cnf(rule3,plain, % % cnf(167679376,derived,(~p(A,B,C,D,E,F,G,s0,s1,s1)|p(A,B,C,D,E,F,G,s1,s0,s0)),inference(rewrite,[status(thm)],[rule3]),[]). % % cnf(rule2,plain, % % cnf(167669600,derived,(~p(A,B,C,D,E,F,G,H,s0,s1)|p(A,B,C,D,E,F,G,H,s1,s0)),inference(rewrite,[status(thm)],[rule2]),[]). % % cnf(rule1,plain, % % cnf(167663384,derived,(~p(A,B,C,D,E,F,G,H,I,s0)|p(A,B,C,D,E,F,G,H,I,s1)),inference(rewrite,[status(thm)],[rule1]),[]). % % cnf(init,plain, % % cnf(167656816,derived,(p(s0,s0,s0,s0,s0,s0,s0,s0,s0,s0)),inference(rewrite,[status(thm)],[init]),[]). % % cnf(175474448,derived,(p(s0,s0,s0,s0,s0,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[167663384,167656816]),[]). % % cnf(175510464,derived,(p(s0,s0,s0,s0,s0,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[167669600,175474448]),[]). % % cnf(175591776,derived,(p(s0,s0,s0,s0,s0,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[175510464,167663384]),[]). % % cnf(175631672,derived,(p(s0,s0,s0,s0,s0,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[167679376,175591776]),[]). % % cnf(175692928,derived,(p(s0,s0,s0,s0,s0,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[175631672,167663384]),[]). % % cnf(175709520,derived,(p(s0,s0,s0,s0,s0,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[175692928,167669600]),[]). % % cnf(175722784,derived,(p(s0,s0,s0,s0,s0,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[175709520,167663384]),[]). % % cnf(175837152,derived,(p(s0,s0,s0,s0,s0,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[167685056,175722784]),[]). % % cnf(175901560,derived,(p(s0,s0,s0,s0,s0,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[175837152,167663384]),[]). % % cnf(175926264,derived,(p(s0,s0,s0,s0,s0,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[175901560,167669600]),[]). % % cnf(175943656,derived,(p(s0,s0,s0,s0,s0,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[175926264,167663384]),[]). % % cnf(175967288,derived,(p(s0,s0,s0,s0,s0,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[175943656,167679376]),[]). % % cnf(175987880,derived,(p(s0,s0,s0,s0,s0,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[175967288,167663384]),[]). % % cnf(176008496,derived,(p(s0,s0,s0,s0,s0,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[175987880,167669600]),[]). % % cnf(176029832,derived,(p(s0,s0,s0,s0,s0,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[176008496,167663384]),[]). % % cnf(176309608,derived,(p(s0,s0,s0,s0,s0,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[167694792,176029832]),[]). % % cnf(176390976,derived,(p(s0,s0,s0,s0,s0,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[176309608,167663384]),[]). % % cnf(176422880,derived,(p(s0,s0,s0,s0,s0,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[176390976,167669600]),[]). % % cnf(176447456,derived,(p(s0,s0,s0,s0,s0,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[176422880,167663384]),[]). % % cnf(176477536,derived,(p(s0,s0,s0,s0,s0,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[176447456,167679376]),[]). % % cnf(176501408,derived,(p(s0,s0,s0,s0,s0,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[176477536,167663384]),[]). % % cnf(176533184,derived,(p(s0,s0,s0,s0,s0,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[176501408,167669600]),[]). % % cnf(176557760,derived,(p(s0,s0,s0,s0,s0,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[176533184,167663384]),[]). % % cnf(176590368,derived,(p(s0,s0,s0,s0,s0,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[176557760,167685056]),[]). % % cnf(176617360,derived,(p(s0,s0,s0,s0,s0,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[176590368,167663384]),[]). % % cnf(176645176,derived,(p(s0,s0,s0,s0,s0,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[176617360,167669600]),[]). % % cnf(176669776,derived,(p(s0,s0,s0,s0,s0,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[176645176,167663384]),[]). % % cnf(176699848,derived,(p(s0,s0,s0,s0,s0,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[176669776,167679376]),[]). % % cnf(176731744,derived,(p(s0,s0,s0,s0,s0,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[176699848,167663384]),[]). % % cnf(176759560,derived,(p(s0,s0,s0,s0,s0,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[176731744,167669600]),[]). % % cnf(176784024,derived,(p(s0,s0,s0,s0,s0,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[176759560,167663384]),[]). % % cnf(177578168,derived,(p(s0,s0,s0,s0,s1,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[167700408,176784024]),[]). % % cnf(177688160,derived,(p(s0,s0,s0,s0,s1,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[177578168,167663384]),[]). % % cnf(177729560,derived,(p(s0,s0,s0,s0,s1,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[177688160,167669600]),[]). % % cnf(176806416,derived,(p(s0,s0,s0,s0,s1,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[177729560,167663384]),[]). % % cnf(177821744,derived,(p(s0,s0,s0,s0,s1,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[176806416,167679376]),[]). % % cnf(177863136,derived,(p(s0,s0,s0,s0,s1,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[177821744,167663384]),[]). % % cnf(177904552,derived,(p(s0,s0,s0,s0,s1,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[177863136,167669600]),[]). % % cnf(177946696,derived,(p(s0,s0,s0,s0,s1,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[177904552,167663384]),[]). % % cnf(177992920,derived,(p(s0,s0,s0,s0,s1,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[177946696,167685056]),[]). % % cnf(178029424,derived,(p(s0,s0,s0,s0,s1,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[177992920,167663384]),[]). % % cnf(178074928,derived,(p(s0,s0,s0,s0,s1,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[178029424,167669600]),[]). % % cnf(178113104,derived,(p(s0,s0,s0,s0,s1,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[178074928,167663384]),[]). % % cnf(178160848,derived,(p(s0,s0,s0,s0,s1,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[178113104,167679376]),[]). % % cnf(178198152,derived,(p(s0,s0,s0,s0,s1,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[178160848,167663384]),[]). % % cnf(178243656,derived,(p(s0,s0,s0,s0,s1,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[178198152,167669600]),[]). % % cnf(178281736,derived,(p(s0,s0,s0,s0,s1,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[178243656,167663384]),[]). % % cnf(178334504,derived,(p(s0,s0,s0,s0,s1,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[178281736,167694792]),[]). % % cnf(178370208,derived,(p(s0,s0,s0,s0,s1,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[178334504,167663384]),[]). % % cnf(178411688,derived,(p(s0,s0,s0,s0,s1,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[178370208,167669600]),[]). % % cnf(178453952,derived,(p(s0,s0,s0,s0,s1,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[178411688,167663384]),[]). % % cnf(178497608,derived,(p(s0,s0,s0,s0,s1,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[178453952,167679376]),[]). % % cnf(178539000,derived,(p(s0,s0,s0,s0,s1,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[178497608,167663384]),[]). % % cnf(178580416,derived,(p(s0,s0,s0,s0,s1,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[178539000,167669600]),[]). % % cnf(178622680,derived,(p(s0,s0,s0,s0,s1,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[178580416,167663384]),[]). % % cnf(178668792,derived,(p(s0,s0,s0,s0,s1,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[178622680,167685056]),[]). % % cnf(178709384,derived,(p(s0,s0,s0,s0,s1,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[178668792,167663384]),[]). % % cnf(178750800,derived,(p(s0,s0,s0,s0,s1,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[178709384,167669600]),[]). % % cnf(178788976,derived,(p(s0,s0,s0,s0,s1,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[178750800,167663384]),[]). % % cnf(178836720,derived,(p(s0,s0,s0,s0,s1,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[178788976,167679376]),[]). % % cnf(178874024,derived,(p(s0,s0,s0,s0,s1,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[178836720,167663384]),[]). % % cnf(178923632,derived,(p(s0,s0,s0,s0,s1,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[178874024,167669600]),[]). % % cnf(178965768,derived,(p(s0,s0,s0,s0,s1,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[178923632,167663384]),[]). % % cnf(181442256,derived,(p(s0,s0,s0,s1,s0,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[167706048,178965768]),[]). % % cnf(181597864,derived,(p(s0,s0,s0,s1,s0,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[181442256,167663384]),[]). % % cnf(181669768,derived,(p(s0,s0,s0,s1,s0,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[181597864,167669600]),[]). % % cnf(181738496,derived,(p(s0,s0,s0,s1,s0,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[181669768,167663384]),[]). % % cnf(181808552,derived,(p(s0,s0,s0,s1,s0,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[181738496,167679376]),[]). % % cnf(181876344,derived,(p(s0,s0,s0,s1,s0,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[181808552,167663384]),[]). % % cnf(181948248,derived,(p(s0,s0,s0,s1,s0,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[181876344,167669600]),[]). % % cnf(182016912,derived,(p(s0,s0,s0,s1,s0,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[181948248,167663384]),[]). % % cnf(182093504,derived,(p(s0,s0,s0,s1,s0,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[182016912,167685056]),[]). % % cnf(182160496,derived,(p(s0,s0,s0,s1,s0,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[182093504,167663384]),[]). % % cnf(182232400,derived,(p(s0,s0,s0,s1,s0,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[182160496,167669600]),[]). % % cnf(182301064,derived,(p(s0,s0,s0,s1,s0,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[182232400,167663384]),[]). % % cnf(182375272,derived,(p(s0,s0,s0,s1,s0,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[182301064,167679376]),[]). % % cnf(182438976,derived,(p(s0,s0,s0,s1,s0,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[182375272,167663384]),[]). % % cnf(182510880,derived,(p(s0,s0,s0,s1,s0,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[182438976,167669600]),[]). % % cnf(182579544,derived,(p(s0,s0,s0,s1,s0,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[182510880,167663384]),[]). % % cnf(179470560,derived,(p(s0,s0,s0,s1,s0,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[182579544,167694792]),[]). % % cnf(182745368,derived,(p(s0,s0,s0,s1,s0,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[179470560,167663384]),[]). % % cnf(182810640,derived,(p(s0,s0,s0,s1,s0,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[182745368,167669600]),[]). % % cnf(182885680,derived,(p(s0,s0,s0,s1,s0,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[182810640,167663384]),[]). % % cnf(182960016,derived,(p(s0,s0,s0,s1,s0,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[182885680,167679376]),[]). % % cnf(183027880,derived,(p(s0,s0,s0,s1,s0,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[182960016,167663384]),[]). % % cnf(183095568,derived,(p(s0,s0,s0,s1,s0,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[183027880,167669600]),[]). % % cnf(183164232,derived,(p(s0,s0,s0,s1,s0,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[183095568,167663384]),[]). % % cnf(183240824,derived,(p(s0,s0,s0,s1,s0,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[183164232,167685056]),[]). % % cnf(183307816,derived,(p(s0,s0,s0,s1,s0,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[183240824,167663384]),[]). % % cnf(183369128,derived,(p(s0,s0,s0,s1,s0,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[183307816,167669600]),[]). % % cnf(183444168,derived,(p(s0,s0,s0,s1,s0,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[183369128,167663384]),[]). % % cnf(183518528,derived,(p(s0,s0,s0,s1,s0,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[183444168,167679376]),[]). % % cnf(183586272,derived,(p(s0,s0,s0,s1,s0,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[183518528,167663384]),[]). % % cnf(183658152,derived,(p(s0,s0,s0,s1,s0,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[183586272,167669600]),[]). % % cnf(183722632,derived,(p(s0,s0,s0,s1,s0,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[183658152,167663384]),[]). % % cnf(183804216,derived,(p(s0,s0,s0,s1,s1,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[183722632,167700408]),[]). % % cnf(183868800,derived,(p(s0,s0,s0,s1,s1,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[183804216,167663384]),[]). % % cnf(183939096,derived,(p(s0,s0,s0,s1,s1,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[183868800,167669600]),[]). % % cnf(184005152,derived,(p(s0,s0,s0,s1,s1,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[183939096,167663384]),[]). % % cnf(184084384,derived,(p(s0,s0,s0,s1,s1,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[184005152,167679376]),[]). % % cnf(184147352,derived,(p(s0,s0,s0,s1,s1,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[184084384,167663384]),[]). % % cnf(184217632,derived,(p(s0,s0,s0,s1,s1,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[184147352,167669600]),[]). % % cnf(184292672,derived,(p(s0,s0,s0,s1,s1,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[184217632,167663384]),[]). % % cnf(184359840,derived,(p(s0,s0,s0,s1,s1,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[184292672,167685056]),[]). % % cnf(184431480,derived,(p(s0,s0,s0,s1,s1,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[184359840,167663384]),[]). % % cnf(184501776,derived,(p(s0,s0,s0,s1,s1,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[184431480,167669600]),[]). % % cnf(184576816,derived,(p(s0,s0,s0,s1,s1,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[184501776,167663384]),[]). % % cnf(184647064,derived,(p(s0,s0,s0,s1,s1,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[184576816,167679376]),[]). % % cnf(184714928,derived,(p(s0,s0,s0,s1,s1,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[184647064,167663384]),[]). % % cnf(184786704,derived,(p(s0,s0,s0,s1,s1,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[184714928,167669600]),[]). % % cnf(184855368,derived,(p(s0,s0,s0,s1,s1,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[184786704,167663384]),[]). % % cnf(184930456,derived,(p(s0,s0,s0,s1,s1,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[184855368,167694792]),[]). % % cnf(184991640,derived,(p(s0,s0,s0,s1,s1,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[184930456,167663384]),[]). % % cnf(185061920,derived,(p(s0,s0,s0,s1,s1,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[184991640,167669600]),[]). % % cnf(185137224,derived,(p(s0,s0,s0,s1,s1,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[185061920,167663384]),[]). % % cnf(185203384,derived,(p(s0,s0,s0,s1,s1,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[185137224,167679376]),[]). % % cnf(185275088,derived,(p(s0,s0,s0,s1,s1,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[185203384,167663384]),[]). % % cnf(185340552,derived,(p(s0,s0,s0,s1,s1,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[185275088,167669600]),[]). % % cnf(185415592,derived,(p(s0,s0,s0,s1,s1,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[185340552,167663384]),[]). % % cnf(185482760,derived,(p(s0,s0,s0,s1,s1,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[185415592,167685056]),[]). % % cnf(185550312,derived,(p(s0,s0,s0,s1,s1,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[185482760,167663384]),[]). % % cnf(185620608,derived,(p(s0,s0,s0,s1,s1,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[185550312,167669600]),[]). % % cnf(185697216,derived,(p(s0,s0,s0,s1,s1,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[185620608,167663384]),[]). % % cnf(185771568,derived,(p(s0,s0,s0,s1,s1,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[185697216,167679376]),[]). % % cnf(185835344,derived,(p(s0,s0,s0,s1,s1,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[185771568,167663384]),[]). % % cnf(185907120,derived,(p(s0,s0,s0,s1,s1,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[185835344,167669600]),[]). % % cnf(185975656,derived,(p(s0,s0,s0,s1,s1,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[185907120,167663384]),[]). % % cnf(194461760,derived,(p(s0,s0,s1,s0,s0,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[167715744,185975656]),[]). % % cnf(194709112,derived,(p(s0,s0,s1,s0,s0,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[194461760,167663384]),[]). % % cnf(194836976,derived,(p(s0,s0,s1,s0,s0,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[194709112,167669600]),[]). % % cnf(194952624,derived,(p(s0,s0,s1,s0,s0,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[194836976,167663384]),[]). % % cnf(195087896,derived,(p(s0,s0,s1,s0,s0,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[194952624,167679376]),[]). % % cnf(195202792,derived,(p(s0,s0,s1,s0,s0,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[195087896,167663384]),[]). % % cnf(195325064,derived,(p(s0,s0,s1,s0,s0,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[195202792,167669600]),[]). % % cnf(195451288,derived,(p(s0,s0,s1,s0,s0,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[195325064,167663384]),[]). % % cnf(195584896,derived,(p(s0,s0,s1,s0,s0,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[195451288,167685056]),[]). % % cnf(195703080,derived,(p(s0,s0,s1,s0,s0,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[195584896,167663384]),[]). % % cnf(195825352,derived,(p(s0,s0,s1,s0,s0,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[195703080,167669600]),[]). % % cnf(195947488,derived,(p(s0,s0,s1,s0,s0,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[195825352,167663384]),[]). % % cnf(196074752,derived,(p(s0,s0,s1,s0,s0,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[195947488,167679376]),[]). % % cnf(196197648,derived,(p(s0,s0,s1,s0,s0,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[196074752,167663384]),[]). % % cnf(196324008,derived,(p(s0,s0,s1,s0,s0,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[196197648,167669600]),[]). % % cnf(196446144,derived,(p(s0,s0,s1,s0,s0,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[196324008,167663384]),[]). % % cnf(196586288,derived,(p(s0,s0,s1,s0,s0,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[196446144,167694792]),[]). % % cnf(196699584,derived,(p(s0,s0,s1,s0,s0,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[196586288,167663384]),[]). % % cnf(196821856,derived,(p(s0,s0,s1,s0,s0,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[196699584,167669600]),[]). % % cnf(196948080,derived,(p(s0,s0,s1,s0,s0,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[196821856,167663384]),[]). % % cnf(197071256,derived,(p(s0,s0,s1,s0,s0,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[196948080,167679376]),[]). % % cnf(197198240,derived,(p(s0,s0,s1,s0,s0,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[197071256,167663384]),[]). % % cnf(197320512,derived,(p(s0,s0,s1,s0,s0,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[197198240,167669600]),[]). % % cnf(197442648,derived,(p(s0,s0,s1,s0,s0,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[197320512,167663384]),[]). % % cnf(197570800,derived,(p(s0,s0,s1,s0,s0,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[197442648,167685056]),[]). % % cnf(197694440,derived,(p(s0,s0,s1,s0,s0,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[197570800,167663384]),[]). % % cnf(197820800,derived,(p(s0,s0,s1,s0,s0,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[197694440,167669600]),[]). % % cnf(197942936,derived,(p(s0,s0,s1,s0,s0,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[197820800,167663384]),[]). % % cnf(198070208,derived,(p(s0,s0,s1,s0,s0,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[197942936,167679376]),[]). % % cnf(198197192,derived,(p(s0,s0,s1,s0,s0,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[198070208,167663384]),[]). % % cnf(198319488,derived,(p(s0,s0,s1,s0,s0,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[198197192,167669600]),[]). % % cnf(198445720,derived,(p(s0,s0,s1,s0,s0,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[198319488,167663384]),[]). % % cnf(198584216,derived,(p(s0,s0,s1,s0,s1,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[198445720,167700408]),[]). % % cnf(198700800,derived,(p(s0,s0,s1,s0,s1,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[198584216,167663384]),[]). % % cnf(198823072,derived,(p(s0,s0,s1,s0,s1,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[198700800,167669600]),[]). % % cnf(198945208,derived,(p(s0,s0,s1,s0,s1,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[198823072,167663384]),[]). % % cnf(199072472,derived,(p(s0,s0,s1,s0,s1,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[198945208,167679376]),[]). % % cnf(199195368,derived,(p(s0,s0,s1,s0,s1,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[199072472,167663384]),[]). % % cnf(199328336,derived,(p(s0,s0,s1,s0,s1,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[199195368,167669600]),[]). % % cnf(199447968,derived,(p(s0,s0,s1,s0,s1,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[199328336,167663384]),[]). % % cnf(199576120,derived,(p(s0,s0,s1,s0,s1,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[199447968,167685056]),[]). % % cnf(199699768,derived,(p(s0,s0,s1,s0,s1,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[199576120,167663384]),[]). % % cnf(199822056,derived,(p(s0,s0,s1,s0,s1,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[199699768,167669600]),[]). % % cnf(199948304,derived,(p(s0,s0,s1,s0,s1,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[199822056,167663384]),[]). % % cnf(200079520,derived,(p(s0,s0,s1,s0,s1,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[199948304,167679376]),[]). % % cnf(200198456,derived,(p(s0,s0,s1,s0,s1,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[200079520,167663384]),[]). % % cnf(200222376,derived,(p(s0,s0,s1,s0,s1,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[200198456,167669600]),[]). % % cnf(200344520,derived,(p(s0,s0,s1,s0,s1,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[200222376,167663384]),[]). % % cnf(200484832,derived,(p(s0,s0,s1,s0,s1,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[200344520,167694792]),[]). % % cnf(200597992,derived,(p(s0,s0,s1,s0,s1,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[200484832,167663384]),[]). % % cnf(200724360,derived,(p(s0,s0,s1,s0,s1,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[200597992,167669600]),[]). % % cnf(200846504,derived,(p(s0,s0,s1,s0,s1,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[200724360,167663384]),[]). % % cnf(200981824,derived,(p(s0,s0,s1,s0,s1,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[200846504,167679376]),[]). % % cnf(201096648,derived,(p(s0,s0,s1,s0,s1,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[200981824,167663384]),[]). % % cnf(201225448,derived,(p(s0,s0,s1,s0,s1,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[201096648,167669600]),[]). % % cnf(201345304,derived,(p(s0,s0,s1,s0,s1,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[201225448,167663384]),[]). % % cnf(201483000,derived,(p(s0,s0,s1,s0,s1,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[201345304,167685056]),[]). % % cnf(201601192,derived,(p(s0,s0,s1,s0,s1,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[201483000,167663384]),[]). % % cnf(201724264,derived,(p(s0,s0,s1,s0,s1,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[201601192,167669600]),[]). % % cnf(201847208,derived,(p(s0,s0,s1,s0,s1,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[201724264,167663384]),[]). % % cnf(201982512,derived,(p(s0,s0,s1,s0,s1,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[201847208,167679376]),[]). % % cnf(202097360,derived,(p(s0,s0,s1,s0,s1,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[201982512,167663384]),[]). % % cnf(202223744,derived,(p(s0,s0,s1,s0,s1,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[202097360,167669600]),[]). % % cnf(202345888,derived,(p(s0,s0,s1,s0,s1,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[202223744,167663384]),[]). % % cnf(202490912,derived,(p(s0,s0,s1,s1,s0,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[202345888,167706048]),[]). % % cnf(202602608,derived,(p(s0,s0,s1,s1,s0,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[202490912,167663384]),[]). % % cnf(202724880,derived,(p(s0,s0,s1,s1,s0,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[202602608,167669600]),[]). % % cnf(202851104,derived,(p(s0,s0,s1,s1,s0,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[202724880,167663384]),[]). % % cnf(202974280,derived,(p(s0,s0,s1,s1,s0,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[202851104,167679376]),[]). % % cnf(203101304,derived,(p(s0,s0,s1,s1,s0,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[202974280,167663384]),[]). % % cnf(203223552,derived,(p(s0,s0,s1,s1,s0,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[203101304,167669600]),[]). % % cnf(203345728,derived,(p(s0,s0,s1,s1,s0,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[203223552,167663384]),[]). % % cnf(203473832,derived,(p(s0,s0,s1,s1,s0,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[203345728,167685056]),[]). % % cnf(203597480,derived,(p(s0,s0,s1,s1,s0,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[203473832,167663384]),[]). % % cnf(203723856,derived,(p(s0,s0,s1,s1,s0,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[203597480,167669600]),[]). % % cnf(203845992,derived,(p(s0,s0,s1,s1,s0,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[203723856,167663384]),[]). % % cnf(203981296,derived,(p(s0,s0,s1,s1,s0,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[203845992,167679376]),[]). % % cnf(204100248,derived,(p(s0,s0,s1,s1,s0,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[203981296,167663384]),[]). % % cnf(204222496,derived,(p(s0,s0,s1,s1,s0,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[204100248,167669600]),[]). % % cnf(204348728,derived,(p(s0,s0,s1,s1,s0,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[204222496,167663384]),[]). % % cnf(204484920,derived,(p(s0,s0,s1,s1,s0,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[204348728,167694792]),[]). % % cnf(204602168,derived,(p(s0,s0,s1,s1,s0,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[204484920,167663384]),[]). % % cnf(204724440,derived,(p(s0,s0,s1,s1,s0,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[204602168,167669600]),[]). % % cnf(204846584,derived,(p(s0,s0,s1,s1,s0,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[204724440,167663384]),[]). % % cnf(204985984,derived,(p(s0,s0,s1,s1,s0,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[204846584,167679376]),[]). % % cnf(205100840,derived,(p(s0,s0,s1,s1,s0,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[204985984,167663384]),[]). % % cnf(205227216,derived,(p(s0,s0,s1,s1,s0,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[205100840,167669600]),[]). % % cnf(205349376,derived,(p(s0,s0,s1,s1,s0,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[205227216,167663384]),[]). % % cnf(205482976,derived,(p(s0,s0,s1,s1,s0,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[205349376,167685056]),[]). % % cnf(205601400,derived,(p(s0,s0,s1,s1,s0,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[205482976,167663384]),[]). % % cnf(205723696,derived,(p(s0,s0,s1,s1,s0,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[205601400,167669600]),[]). % % cnf(205849944,derived,(p(s0,s0,s1,s1,s0,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[205723696,167663384]),[]). % % cnf(205981160,derived,(p(s0,s0,s1,s1,s0,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[205849944,167679376]),[]). % % cnf(206100096,derived,(p(s0,s0,s1,s1,s0,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[205981160,167663384]),[]). % % cnf(206222448,derived,(p(s0,s0,s1,s1,s0,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[206100096,167669600]),[]). % % cnf(206344592,derived,(p(s0,s0,s1,s1,s0,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[206222448,167663384]),[]). % % cnf(206487232,derived,(p(s0,s0,s1,s1,s1,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[206344592,167700408]),[]). % % cnf(206604600,derived,(p(s0,s0,s1,s1,s1,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[206487232,167663384]),[]). % % cnf(206732504,derived,(p(s0,s0,s1,s1,s1,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[206604600,167669600]),[]). % % cnf(206848208,derived,(p(s0,s0,s1,s1,s1,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[206732504,167663384]),[]). % % cnf(206979384,derived,(p(s0,s0,s1,s1,s1,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[206848208,167679376]),[]). % % cnf(207098384,derived,(p(s0,s0,s1,s1,s1,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[206979384,167663384]),[]). % % cnf(207220672,derived,(p(s0,s0,s1,s1,s1,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[207098384,167669600]),[]). % % cnf(207346920,derived,(p(s0,s0,s1,s1,s1,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[207220672,167663384]),[]). % % cnf(207470960,derived,(p(s0,s0,s1,s1,s1,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[207346920,167685056]),[]). % % cnf(207598728,derived,(p(s0,s0,s1,s1,s1,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[207470960,167663384]),[]). % % cnf(207720984,derived,(p(s0,s0,s1,s1,s1,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[207598728,167669600]),[]). % % cnf(207848024,derived,(p(s0,s0,s1,s1,s1,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[207720984,167663384]),[]). % % cnf(207978448,derived,(p(s0,s0,s1,s1,s1,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[207848024,167679376]),[]). % % cnf(208098192,derived,(p(s0,s0,s1,s1,s1,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[207978448,167663384]),[]). % % cnf(208226184,derived,(p(s0,s0,s1,s1,s1,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[208098192,167669600]),[]). % % cnf(208341808,derived,(p(s0,s0,s1,s1,s1,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[208226184,167663384]),[]). % % cnf(208486040,derived,(p(s0,s0,s1,s1,s1,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[208341808,167694792]),[]). % % cnf(208603432,derived,(p(s0,s0,s1,s1,s1,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[208486040,167663384]),[]). % % cnf(208725720,derived,(p(s0,s0,s1,s1,s1,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[208603432,167669600]),[]). % % cnf(208856840,derived,(p(s0,s0,s1,s1,s1,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[208725720,167663384]),[]). % % cnf(208983176,derived,(p(s0,s0,s1,s1,s1,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[208856840,167679376]),[]). % % cnf(209107008,derived,(p(s0,s0,s1,s1,s1,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[208983176,167663384]),[]). % % cnf(209230864,derived,(p(s0,s0,s1,s1,s1,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[209107008,167669600]),[]). % % cnf(209346512,derived,(p(s0,s0,s1,s1,s1,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[209230864,167663384]),[]). % % cnf(209484232,derived,(p(s0,s0,s1,s1,s1,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[209346512,167685056]),[]). % % cnf(209603208,derived,(p(s0,s0,s1,s1,s1,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[209484232,167663384]),[]). % % cnf(209731200,derived,(p(s0,s0,s1,s1,s1,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[209603208,167669600]),[]). % % cnf(209846824,derived,(p(s0,s0,s1,s1,s1,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[209731200,167663384]),[]). % % cnf(209978016,derived,(p(s0,s0,s1,s1,s1,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[209846824,167679376]),[]). % % cnf(210096984,derived,(p(s0,s0,s1,s1,s1,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[209978016,167663384]),[]). % % cnf(210222312,derived,(p(s0,s0,s1,s1,s1,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[210096984,167669600]),[]). % % cnf(210353432,derived,(p(s0,s0,s1,s1,s1,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[210222312,167663384]),[]). % % cnf(241250440,derived,(p(s0,s1,s0,s0,s0,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[167721408,210353432]),[]). % % cnf(241644712,derived,(p(s0,s1,s0,s0,s0,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[241250440,167663384]),[]). % % cnf(241897760,derived,(p(s0,s1,s0,s0,s0,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[241644712,167669600]),[]). % % cnf(242111936,derived,(p(s0,s1,s0,s0,s0,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[241897760,167663384]),[]). % % cnf(242380888,derived,(p(s0,s1,s0,s0,s0,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[242111936,167679376]),[]). % % cnf(242576624,derived,(p(s0,s1,s0,s0,s0,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[242380888,167663384]),[]). % % cnf(242829672,derived,(p(s0,s1,s0,s0,s0,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[242576624,167669600]),[]). % % cnf(243044640,derived,(p(s0,s1,s0,s0,s0,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[242829672,167663384]),[]). % % cnf(243315232,derived,(p(s0,s1,s0,s0,s0,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[243044640,167685056]),[]). % % cnf(243514304,derived,(p(s0,s1,s0,s0,s0,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[243315232,167663384]),[]). % % cnf(243767352,derived,(p(s0,s1,s0,s0,s0,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[243514304,167669600]),[]). % % cnf(243982320,derived,(p(s0,s1,s0,s0,s0,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[243767352,167663384]),[]). % % cnf(244246432,derived,(p(s0,s1,s0,s0,s0,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[243982320,167679376]),[]). % % cnf(244446256,derived,(p(s0,s1,s0,s0,s0,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[244246432,167663384]),[]). % % cnf(244695072,derived,(p(s0,s1,s0,s0,s0,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[244446256,167669600]),[]). % % cnf(244909344,derived,(p(s0,s1,s0,s0,s0,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[244695072,167663384]),[]). % % cnf(245183208,derived,(p(s0,s1,s0,s0,s0,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[244909344,167694792]),[]). % % cnf(245377496,derived,(p(s0,s1,s0,s0,s0,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[245183208,167663384]),[]). % % cnf(245630528,derived,(p(s0,s1,s0,s0,s0,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[245377496,167669600]),[]). % % cnf(245849568,derived,(p(s0,s1,s0,s0,s0,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[245630528,167663384]),[]). % % cnf(246113664,derived,(p(s0,s1,s0,s0,s0,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[245849568,167679376]),[]). % % cnf(246309656,derived,(p(s0,s1,s0,s0,s0,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[246113664,167663384]),[]). % % cnf(246562560,derived,(p(s0,s1,s0,s0,s0,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[246309656,167669600]),[]). % % cnf(246772744,derived,(p(s0,s1,s0,s0,s0,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[246562560,167663384]),[]). % % cnf(247038680,derived,(p(s0,s1,s0,s0,s0,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[246772744,167685056]),[]). % % cnf(247248136,derived,(p(s0,s1,s0,s0,s0,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[247038680,167663384]),[]). % % cnf(247496128,derived,(p(s0,s1,s0,s0,s0,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[247248136,167669600]),[]). % % cnf(247706312,derived,(p(s0,s1,s0,s0,s0,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[247496128,167663384]),[]). % % cnf(247967256,derived,(p(s0,s1,s0,s0,s0,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[247706312,167679376]),[]). % % cnf(248175168,derived,(p(s0,s1,s0,s0,s0,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[247967256,167663384]),[]). % % cnf(248424080,derived,(p(s0,s1,s0,s0,s0,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[248175168,167669600]),[]). % % cnf(248643096,derived,(p(s0,s1,s0,s0,s0,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[248424080,167663384]),[]). % % cnf(248914520,derived,(p(s0,s1,s0,s0,s1,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[248643096,167700408]),[]). % % cnf(249112776,derived,(p(s0,s1,s0,s0,s1,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[248914520,167663384]),[]). % % cnf(249354312,derived,(p(s0,s1,s0,s0,s1,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[249112776,167669600]),[]). % % cnf(249579952,derived,(p(s0,s1,s0,s0,s1,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[249354312,167663384]),[]). % % cnf(249843984,derived,(p(s0,s1,s0,s0,s1,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[249579952,167679376]),[]). % % cnf(250048752,derived,(p(s0,s1,s0,s0,s1,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[249843984,167663384]),[]). % % cnf(250290312,derived,(p(s0,s1,s0,s0,s1,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[250048752,167669600]),[]). % % cnf(250511040,derived,(p(s0,s1,s0,s0,s1,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[250290312,167663384]),[]). % % cnf(250782424,derived,(p(s0,s1,s0,s0,s1,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[250511040,167685056]),[]). % % cnf(250982304,derived,(p(s0,s1,s0,s0,s1,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[250782424,167663384]),[]). % % cnf(251223864,derived,(p(s0,s1,s0,s0,s1,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[250982304,167669600]),[]). % % cnf(251440504,derived,(p(s0,s1,s0,s0,s1,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[251223864,167663384]),[]). % % cnf(251709448,derived,(p(s0,s1,s0,s0,s1,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[251440504,167679376]),[]). % % cnf(251909320,derived,(p(s0,s1,s0,s0,s1,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[251709448,167663384]),[]). % % cnf(252162368,derived,(p(s0,s1,s0,s0,s1,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[251909320,167669600]),[]). % % cnf(252377552,derived,(p(s0,s1,s0,s0,s1,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[252162368,167663384]),[]). % % cnf(252646488,derived,(p(s0,s1,s0,s0,s1,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[252377552,167694792]),[]). % % cnf(252845568,derived,(p(s0,s1,s0,s0,s1,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[252646488,167663384]),[]). % % cnf(253093584,derived,(p(s0,s1,s0,s0,s1,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[252845568,167669600]),[]). % % cnf(253312776,derived,(p(s0,s1,s0,s0,s1,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[253093584,167663384]),[]). % % cnf(253576808,derived,(p(s0,s1,s0,s0,s1,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[253312776,167679376]),[]). % % cnf(253777488,derived,(p(s0,s1,s0,s0,s1,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[253576808,167663384]),[]). % % cnf(254029600,derived,(p(s0,s1,s0,s0,s1,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[253777488,167669600]),[]). % % cnf(254248768,derived,(p(s0,s1,s0,s0,s1,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[254029600,167663384]),[]). % % cnf(254505704,derived,(p(s0,s1,s0,s0,s1,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[254248768,167685056]),[]). % % cnf(254715152,derived,(p(s0,s1,s0,s0,s1,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[254505704,167663384]),[]). % % cnf(254963144,derived,(p(s0,s1,s0,s0,s1,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[254715152,167669600]),[]). % % cnf(255178224,derived,(p(s0,s1,s0,s0,s1,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[254963144,167663384]),[]). % % cnf(255434272,derived,(p(s0,s1,s0,s0,s1,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[255178224,167679376]),[]). % % cnf(255647064,derived,(p(s0,s1,s0,s0,s1,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[255434272,167663384]),[]). % % cnf(255895320,derived,(p(s0,s1,s0,s0,s1,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[255647064,167669600]),[]). % % cnf(256110264,derived,(p(s0,s1,s0,s0,s1,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[255895320,167663384]),[]). % % cnf(256384112,derived,(p(s0,s1,s0,s1,s0,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[256110264,167706048]),[]). % % cnf(256589792,derived,(p(s0,s1,s0,s1,s0,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[256384112,167663384]),[]). % % cnf(256833696,derived,(p(s0,s1,s0,s1,s0,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[256589792,167669600]),[]). % % cnf(257052864,derived,(p(s0,s1,s0,s1,s0,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[256833696,167663384]),[]). % % cnf(257308912,derived,(p(s0,s1,s0,s1,s0,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[257052864,167679376]),[]). % % cnf(257517616,derived,(p(s0,s1,s0,s1,s0,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[257308912,167663384]),[]). % % cnf(257765640,derived,(p(s0,s1,s0,s1,s0,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[257517616,167669600]),[]). % % cnf(257984808,derived,(p(s0,s1,s0,s1,s0,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[257765640,167663384]),[]). % % cnf(258241744,derived,(p(s0,s1,s0,s1,s0,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[257984808,167685056]),[]). % % cnf(258451192,derived,(p(s0,s1,s0,s1,s0,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[258241744,167663384]),[]). % % cnf(258692728,derived,(p(s0,s1,s0,s1,s0,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[258451192,167669600]),[]). % % cnf(258918368,derived,(p(s0,s1,s0,s1,s0,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[258692728,167663384]),[]). % % cnf(259182408,derived,(p(s0,s1,s0,s1,s0,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[258918368,167679376]),[]). % % cnf(259383112,derived,(p(s0,s1,s0,s1,s0,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[259182408,167663384]),[]). % % cnf(259624648,derived,(p(s0,s1,s0,s1,s0,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[259383112,167669600]),[]). % % cnf(259841288,derived,(p(s0,s1,s0,s1,s0,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[259624648,167663384]),[]). % % cnf(260115112,derived,(p(s0,s1,s0,s1,s0,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[259841288,167694792]),[]). % % cnf(260318280,derived,(p(s0,s1,s0,s1,s0,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[260115112,167663384]),[]). % % cnf(260559928,derived,(p(s0,s1,s0,s1,s0,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[260318280,167669600]),[]). % % cnf(260781392,derived,(p(s0,s1,s0,s1,s0,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[260559928,167663384]),[]). % % cnf(261045424,derived,(p(s0,s1,s0,s1,s0,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[260781392,167679376]),[]). % % cnf(261246104,derived,(p(s0,s1,s0,s1,s0,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[261045424,167663384]),[]). % % cnf(261487664,derived,(p(s0,s1,s0,s1,s0,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[261246104,167669600]),[]). % % cnf(261708392,derived,(p(s0,s1,s0,s1,s0,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[261487664,167663384]),[]). % % cnf(261979776,derived,(p(s0,s1,s0,s1,s0,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[261708392,167685056]),[]). % % cnf(262179656,derived,(p(s0,s1,s0,s1,s0,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[261979776,167663384]),[]). % % cnf(262425312,derived,(p(s0,s1,s0,s1,s0,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[262179656,167669600]),[]). % % cnf(262646040,derived,(p(s0,s1,s0,s1,s0,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[262425312,167663384]),[]). % % cnf(262914984,derived,(p(s0,s1,s0,s1,s0,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[262646040,167679376]),[]). % % cnf(263110768,derived,(p(s0,s1,s0,s1,s0,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[262914984,167663384]),[]). % % cnf(263367904,derived,(p(s0,s1,s0,s1,s0,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[263110768,167669600]),[]). % % cnf(263582872,derived,(p(s0,s1,s0,s1,s0,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[263367904,167663384]),[]). % % cnf(263854224,derived,(p(s0,s1,s0,s1,s1,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[263582872,167700408]),[]). % % cnf(264056592,derived,(p(s0,s1,s0,s1,s1,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[263854224,167663384]),[]). % % cnf(264304608,derived,(p(s0,s1,s0,s1,s1,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[264056592,167669600]),[]). % % cnf(264519712,derived,(p(s0,s1,s0,s1,s1,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[264304608,167663384]),[]). % % cnf(264783744,derived,(p(s0,s1,s0,s1,s1,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[264519712,167679376]),[]). % % cnf(264988536,derived,(p(s0,s1,s0,s1,s1,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[264783744,167663384]),[]). % % cnf(265232448,derived,(p(s0,s1,s0,s1,s1,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[264988536,167669600]),[]). % % cnf(265446720,derived,(p(s0,s1,s0,s1,s1,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[265232448,167663384]),[]). % % cnf(265708552,derived,(p(s0,s1,s0,s1,s1,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[265446720,167685056]),[]). % % cnf(265918000,derived,(p(s0,s1,s0,s1,s1,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[265708552,167663384]),[]). % % cnf(266165992,derived,(p(s0,s1,s0,s1,s1,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[265918000,167669600]),[]). % % cnf(266380264,derived,(p(s0,s1,s0,s1,s1,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[266165992,167663384]),[]). % % cnf(266641208,derived,(p(s0,s1,s0,s1,s1,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[266380264,167679376]),[]). % % cnf(266845032,derived,(p(s0,s1,s0,s1,s1,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[266641208,167663384]),[]). % % cnf(267098032,derived,(p(s0,s1,s0,s1,s1,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[266845032,167669600]),[]). % % cnf(267312976,derived,(p(s0,s1,s0,s1,s1,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[267098032,167663384]),[]). % % cnf(267574904,derived,(p(s0,s1,s0,s1,s1,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[267312976,167694792]),[]). % % cnf(267785104,derived,(p(s0,s1,s0,s1,s1,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[267574904,167663384]),[]). % % cnf(268033096,derived,(p(s0,s1,s0,s1,s1,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[267785104,167669600]),[]). % % cnf(268243280,derived,(p(s0,s1,s0,s1,s1,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[268033096,167663384]),[]). % % cnf(268504224,derived,(p(s0,s1,s0,s1,s1,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[268243280,167679376]),[]). % % cnf(268712136,derived,(p(s0,s1,s0,s1,s1,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[268504224,167663384]),[]). % % cnf(268961048,derived,(p(s0,s1,s0,s1,s1,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[268712136,167669600]),[]). % % cnf(269180064,derived,(p(s0,s1,s0,s1,s1,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[268961048,167663384]),[]). % % cnf(269446560,derived,(p(s0,s1,s0,s1,s1,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[269180064,167685056]),[]). % % cnf(269641552,derived,(p(s0,s1,s0,s1,s1,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[269446560,167663384]),[]). % % cnf(269898680,derived,(p(s0,s1,s0,s1,s1,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[269641552,167669600]),[]). % % cnf(270117696,derived,(p(s0,s1,s0,s1,s1,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[269898680,167663384]),[]). % % cnf(270381800,derived,(p(s0,s1,s0,s1,s1,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[270117696,167679376]),[]). % % cnf(201730872,derived,(p(s0,s1,s0,s1,s1,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[270381800,167663384]),[]). % % cnf(270837624,derived,(p(s0,s1,s0,s1,s1,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[201730872,167669600]),[]). % % cnf(271051848,derived,(p(s0,s1,s0,s1,s1,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[270837624,167663384]),[]). % % cnf(271331360,derived,(p(s0,s1,s1,s0,s0,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[271051848,167715744]),[]). % % cnf(271528040,derived,(p(s0,s1,s1,s0,s0,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[271331360,167663384]),[]). % % cnf(271769600,derived,(p(s0,s1,s1,s0,s0,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[271528040,167669600]),[]). % % cnf(271991152,derived,(p(s0,s1,s1,s0,s0,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[271769600,167663384]),[]). % % cnf(272255184,derived,(p(s0,s1,s1,s0,s0,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[271991152,167679376]),[]). % % cnf(272459952,derived,(p(s0,s1,s1,s0,s0,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[272255184,167663384]),[]). % % cnf(272701512,derived,(p(s0,s1,s1,s0,s0,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[272459952,167669600]),[]). % % cnf(272923064,derived,(p(s0,s1,s1,s0,s0,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[272701512,167663384]),[]). % % cnf(273189536,derived,(p(s0,s1,s1,s0,s0,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[272923064,167685056]),[]). % % cnf(273389416,derived,(p(s0,s1,s1,s0,s0,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[273189536,167663384]),[]). % % cnf(273630976,derived,(p(s0,s1,s1,s0,s0,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[273389416,167669600]),[]). % % cnf(273856616,derived,(p(s0,s1,s1,s0,s0,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[273630976,167663384]),[]). % % cnf(274120648,derived,(p(s0,s1,s1,s0,s0,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[273856616,167679376]),[]). % % cnf(274321328,derived,(p(s0,s1,s1,s0,s0,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[274120648,167663384]),[]). % % cnf(274569344,derived,(p(s0,s1,s1,s0,s0,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[274321328,167669600]),[]). % % cnf(274783624,derived,(p(s0,s1,s1,s0,s0,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[274569344,167663384]),[]). % % cnf(275057448,derived,(p(s0,s1,s1,s0,s0,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[274783624,167694792]),[]). % % cnf(275256528,derived,(p(s0,s1,s1,s0,s0,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[275057448,167663384]),[]). % % cnf(275504544,derived,(p(s0,s1,s1,s0,s0,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[275256528,167669600]),[]). % % cnf(275719624,derived,(p(s0,s1,s1,s0,s0,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[275504544,167663384]),[]). % % cnf(275975672,derived,(p(s0,s1,s1,s0,s0,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[275719624,167679376]),[]). % % cnf(276188464,derived,(p(s0,s1,s1,s0,s0,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[275975672,167663384]),[]). % % cnf(276436488,derived,(p(s0,s1,s1,s0,s0,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[276188464,167669600]),[]). % % cnf(276650760,derived,(p(s0,s1,s1,s0,s0,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[276436488,167663384]),[]). % % cnf(276912584,derived,(p(s0,s1,s1,s0,s0,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[276650760,167685056]),[]). % % cnf(277126120,derived,(p(s0,s1,s1,s0,s0,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[276912584,167663384]),[]). % % cnf(277370024,derived,(p(s0,s1,s1,s0,s0,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[277126120,167669600]),[]). % % cnf(277584296,derived,(p(s0,s1,s1,s0,s0,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[277370024,167663384]),[]). % % cnf(277845240,derived,(p(s0,s1,s1,s0,s0,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[277584296,167679376]),[]). % % cnf(278049064,derived,(p(s0,s1,s1,s0,s0,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[277845240,167663384]),[]). % % cnf(278302064,derived,(p(s0,s1,s1,s0,s0,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[278049064,167669600]),[]). % % cnf(278521096,derived,(p(s0,s1,s1,s0,s0,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[278302064,167663384]),[]). % % cnf(278792592,derived,(p(s0,s1,s1,s0,s1,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[278521096,167700408]),[]). % % cnf(278990768,derived,(p(s0,s1,s1,s0,s1,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[278792592,167663384]),[]). % % cnf(279242856,derived,(p(s0,s1,s1,s0,s1,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[278990768,167669600]),[]). % % cnf(279457224,derived,(p(s0,s1,s1,s0,s1,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[279242856,167663384]),[]). % % cnf(279718064,derived,(p(s0,s1,s1,s0,s1,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[279457224,167679376]),[]). % % cnf(279926768,derived,(p(s0,s1,s1,s0,s1,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[279718064,167663384]),[]). % % cnf(280168336,derived,(p(s0,s1,s1,s0,s1,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[279926768,167669600]),[]). % % cnf(280384976,derived,(p(s0,s1,s1,s0,s1,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[280168336,167663384]),[]). % % cnf(280656360,derived,(p(s0,s1,s1,s0,s1,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[280384976,167685056]),[]). % % cnf(280860328,derived,(p(s0,s1,s1,s0,s1,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[280656360,167663384]),[]). % % cnf(281101976,derived,(p(s0,s1,s1,s0,s1,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[280860328,167669600]),[]). % % cnf(281318528,derived,(p(s0,s1,s1,s0,s1,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[281101976,167663384]),[]). % % cnf(281587472,derived,(p(s0,s1,s1,s0,s1,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[281318528,167679376]),[]). % % cnf(281783256,derived,(p(s0,s1,s1,s0,s1,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[281587472,167663384]),[]). % % cnf(282036304,derived,(p(s0,s1,s1,s0,s1,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[281783256,167669600]),[]). % % cnf(282255320,derived,(p(s0,s1,s1,s0,s1,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[282036304,167663384]),[]). % % cnf(282524320,derived,(p(s0,s1,s1,s0,s1,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[282255320,167694792]),[]). % % cnf(282723400,derived,(p(s0,s1,s1,s0,s1,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[282524320,167663384]),[]). % % cnf(282964960,derived,(p(s0,s1,s1,s0,s1,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[282723400,167669600]),[]). % % cnf(283185688,derived,(p(s0,s1,s1,s0,s1,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[282964960,167663384]),[]). % % cnf(283458720,derived,(p(s0,s1,s1,s0,s1,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[283185688,167679376]),[]). % % cnf(283654504,derived,(p(s0,s1,s1,s0,s1,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[283458720,167663384]),[]). % % cnf(283907552,derived,(p(s0,s1,s1,s0,s1,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[283654504,167669600]),[]). % % cnf(284122480,derived,(p(s0,s1,s1,s0,s1,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[283907552,167663384]),[]). % % cnf(284388976,derived,(p(s0,s1,s1,s0,s1,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[284122480,167685056]),[]). % % cnf(284588048,derived,(p(s0,s1,s1,s0,s1,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[284388976,167663384]),[]). % % cnf(284910928,derived,(p(s0,s1,s1,s0,s1,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[284588048,167669600]),[]). % % cnf(285125856,derived,(p(s0,s1,s1,s0,s1,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[284910928,167663384]),[]). % % cnf(285389960,derived,(p(s0,s1,s1,s0,s1,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[285125856,167679376]),[]). % % cnf(285594680,derived,(p(s0,s1,s1,s0,s1,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[285389960,167663384]),[]). % % cnf(285838640,derived,(p(s0,s1,s1,s0,s1,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[285594680,167669600]),[]). % % cnf(286052864,derived,(p(s0,s1,s1,s0,s1,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[285838640,167663384]),[]). % % cnf(286329944,derived,(p(s0,s1,s1,s1,s0,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[286052864,167706048]),[]). % % cnf(286522560,derived,(p(s0,s1,s1,s1,s0,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[286329944,167663384]),[]). % % cnf(286769000,derived,(p(s0,s1,s1,s1,s0,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[286522560,167669600]),[]). % % cnf(286994640,derived,(p(s0,s1,s1,s1,s0,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[286769000,167663384]),[]). % % cnf(287258672,derived,(p(s0,s1,s1,s1,s0,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[286994640,167679376]),[]). % % cnf(287459352,derived,(p(s0,s1,s1,s1,s0,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[287258672,167663384]),[]). % % cnf(287700912,derived,(p(s0,s1,s1,s1,s0,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[287459352,167669600]),[]). % % cnf(287921648,derived,(p(s0,s1,s1,s1,s0,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[287700912,167663384]),[]). % % cnf(288187832,derived,(p(s0,s1,s1,s1,s0,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[287921648,167685056]),[]). % % cnf(288397264,derived,(p(s0,s1,s1,s1,s0,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[288187832,167663384]),[]). % % cnf(288638824,derived,(p(s0,s1,s1,s1,s0,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[288397264,167669600]),[]). % % cnf(288860376,derived,(p(s0,s1,s1,s1,s0,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[288638824,167663384]),[]). % % cnf(289124408,derived,(p(s0,s1,s1,s1,s0,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[288860376,167679376]),[]). % % cnf(289329176,derived,(p(s0,s1,s1,s1,s0,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[289124408,167663384]),[]). % % cnf(289573104,derived,(p(s0,s1,s1,s1,s0,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[289329176,167669600]),[]). % % cnf(289792272,derived,(p(s0,s1,s1,s1,s0,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[289573104,167663384]),[]). % % cnf(290065296,derived,(p(s0,s1,s1,s1,s0,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[289792272,167694792]),[]). % % cnf(290264376,derived,(p(s0,s1,s1,s1,s0,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[290065296,167663384]),[]). % % cnf(290512392,derived,(p(s0,s1,s1,s1,s0,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[290264376,167669600]),[]). % % cnf(290731584,derived,(p(s0,s1,s1,s1,s0,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[290512392,167663384]),[]). % % cnf(290987608,derived,(p(s0,s1,s1,s1,s0,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[290731584,167679376]),[]). % % cnf(291196312,derived,(p(s0,s1,s1,s1,s0,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[290987608,167663384]),[]). % % cnf(291444336,derived,(p(s0,s1,s1,s1,s0,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[291196312,167669600]),[]). % % cnf(291663504,derived,(p(s0,s1,s1,s1,s0,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[291444336,167663384]),[]). % % cnf(291920440,derived,(p(s0,s1,s1,s1,s0,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[291663504,167685056]),[]). % % cnf(292129888,derived,(p(s0,s1,s1,s1,s0,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[291920440,167663384]),[]). % % cnf(292377880,derived,(p(s0,s1,s1,s1,s0,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[292129888,167669600]),[]). % % cnf(292592960,derived,(p(s0,s1,s1,s1,s0,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[292377880,167663384]),[]). % % cnf(292849008,derived,(p(s0,s1,s1,s1,s0,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[292592960,167679376]),[]). % % cnf(293061800,derived,(p(s0,s1,s1,s1,s0,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[292849008,167663384]),[]). % % cnf(293309824,derived,(p(s0,s1,s1,s1,s0,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[293061800,167669600]),[]). % % cnf(293519968,derived,(p(s0,s1,s1,s1,s0,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[293309824,167663384]),[]). % % cnf(293783488,derived,(p(s0,s1,s1,s1,s1,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[293519968,167700408]),[]). % % cnf(293987984,derived,(p(s0,s1,s1,s1,s1,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[293783488,167663384]),[]). % % cnf(294240888,derived,(p(s0,s1,s1,s1,s1,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[293987984,167669600]),[]). % % cnf(294460056,derived,(p(s0,s1,s1,s1,s1,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[294240888,167663384]),[]). % % cnf(294716104,derived,(p(s0,s1,s1,s1,s1,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[294460056,167679376]),[]). % % cnf(294924808,derived,(p(s0,s1,s1,s1,s1,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[294716104,167663384]),[]). % % cnf(295166376,derived,(p(s0,s1,s1,s1,s1,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[294924808,167669600]),[]). % % cnf(295391992,derived,(p(s0,s1,s1,s1,s1,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[295166376,167663384]),[]). % % cnf(295658488,derived,(p(s0,s1,s1,s1,s1,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[295391992,167685056]),[]). % % cnf(295858392,derived,(p(s0,s1,s1,s1,s1,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[295658488,167663384]),[]). % % cnf(296099928,derived,(p(s0,s1,s1,s1,s1,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[295858392,167669600]),[]). % % cnf(296325552,derived,(p(s0,s1,s1,s1,s1,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[296099928,167663384]),[]). % % cnf(296593696,derived,(p(s0,s1,s1,s1,s1,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[296325552,167679376]),[]). % % cnf(296798464,derived,(p(s0,s1,s1,s1,s1,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[296593696,167663384]),[]). % % cnf(297046512,derived,(p(s0,s1,s1,s1,s1,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[296798464,167669600]),[]). % % cnf(297256648,derived,(p(s0,s1,s1,s1,s1,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[297046512,167663384]),[]). % % cnf(297528856,derived,(p(s0,s1,s1,s1,s1,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[297256648,167694792]),[]). % % cnf(297732024,derived,(p(s0,s1,s1,s1,s1,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[297528856,167663384]),[]). % % cnf(297969496,derived,(p(s0,s1,s1,s1,s1,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[297732024,167669600]),[]). % % cnf(298195112,derived,(p(s0,s1,s1,s1,s1,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[297969496,167663384]),[]). % % cnf(298459168,derived,(p(s0,s1,s1,s1,s1,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[298195112,167679376]),[]). % % cnf(298659848,derived,(p(s0,s1,s1,s1,s1,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[298459168,167663384]),[]). % % cnf(298907896,derived,(p(s0,s1,s1,s1,s1,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[298659848,167669600]),[]). % % cnf(299122264,derived,(p(s0,s1,s1,s1,s1,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[298907896,167663384]),[]). % % cnf(299392008,derived,(p(s0,s1,s1,s1,s1,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[299122264,167685056]),[]). % % cnf(299593192,derived,(p(s0,s1,s1,s1,s1,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[299392008,167663384]),[]). % % cnf(299846240,derived,(p(s0,s1,s1,s1,s1,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[299593192,167669600]),[]). % % cnf(300060368,derived,(p(s0,s1,s1,s1,s1,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[299846240,167663384]),[]). % % cnf(300327808,derived,(p(s0,s1,s1,s1,s1,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[300060368,167679376]),[]). % % cnf(300523480,derived,(p(s0,s1,s1,s1,s1,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[300327808,167663384]),[]). % % cnf(300769840,derived,(p(s0,s1,s1,s1,s1,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[300523480,167669600]),[]). % % cnf(300985032,derived,(p(s0,s1,s1,s1,s1,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[300769840,167663384]),[]). % % cnf(rule10,plain, % % cnf(167727040,derived,(~p(s0,s1,s1,s1,s1,s1,s1,s1,s1,s1)|p(s1,s0,s0,s0,s0,s0,s0,s0,s0,s0)),inference(rewrite,[status(thm)],[rule10]),[]). % % cnf(302151512,derived,(p(s1,s0,s0,s0,s0,s0,s0,s0,s0,s1)),inference(forward_subsumption_resolution__resolution,[status(thm)],[300985032,167727040,167663384]),[]). % % cnf(302616400,derived,(p(s1,s0,s0,s0,s0,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[302151512,167669600]),[]). % % cnf(302843608,derived,(p(s1,s0,s0,s0,s0,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[302616400,167663384]),[]). % % cnf(303101264,derived,(p(s1,s0,s0,s0,s0,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[302843608,167679376]),[]). % % cnf(303311568,derived,(p(s1,s0,s0,s0,s0,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[303101264,167663384]),[]). % % cnf(303554736,derived,(p(s1,s0,s0,s0,s0,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[303311568,167669600]),[]). % % cnf(303781928,derived,(p(s1,s0,s0,s0,s0,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[303554736,167663384]),[]). % % cnf(304041272,derived,(p(s1,s0,s0,s0,s0,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[303781928,167685056]),[]). % % cnf(304251520,derived,(p(s1,s0,s0,s0,s0,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[304041272,167663384]),[]). % % cnf(304494656,derived,(p(s1,s0,s0,s0,s0,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[304251520,167669600]),[]). % % cnf(304721872,derived,(p(s1,s0,s0,s0,s0,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[304494656,167663384]),[]). % % cnf(304979520,derived,(p(s1,s0,s0,s0,s0,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[304721872,167679376]),[]). % % cnf(305193912,derived,(p(s1,s0,s0,s0,s0,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[304979520,167663384]),[]). % % cnf(305444040,derived,(p(s1,s0,s0,s0,s0,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[305193912,167669600]),[]). % % cnf(305660720,derived,(p(s1,s0,s0,s0,s0,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[305444040,167663384]),[]). % % cnf(305936280,derived,(p(s1,s0,s0,s0,s0,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[305660720,167694792]),[]). % % cnf(306136048,derived,(p(s1,s0,s0,s0,s0,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[305936280,167663384]),[]). % % cnf(306379216,derived,(p(s1,s0,s0,s0,s0,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[306136048,167669600]),[]). % % cnf(306602424,derived,(p(s1,s0,s0,s0,s0,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[306379216,167663384]),[]). % % cnf(306868000,derived,(p(s1,s0,s0,s0,s0,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[306602424,167679376]),[]). % % cnf(307074448,derived,(p(s1,s0,s0,s0,s0,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[306868000,167663384]),[]). % % cnf(307323976,derived,(p(s1,s0,s0,s0,s0,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[307074448,167669600]),[]). % % cnf(307540680,derived,(p(s1,s0,s0,s0,s0,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[307323976,167663384]),[]). % % cnf(307809552,derived,(p(s1,s0,s0,s0,s0,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[307540680,167685056]),[]). % % cnf(308014400,derived,(p(s1,s0,s0,s0,s0,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[307809552,167663384]),[]). % % cnf(308259840,derived,(p(s1,s0,s0,s0,s0,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[308014400,167669600]),[]). % % cnf(308480632,derived,(p(s1,s0,s0,s0,s0,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[308259840,167663384]),[]). % % cnf(308746800,derived,(p(s1,s0,s0,s0,s0,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[308480632,167679376]),[]). % % cnf(308949104,derived,(p(s1,s0,s0,s0,s0,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[308746800,167663384]),[]). % % cnf(309198656,derived,(p(s1,s0,s0,s0,s0,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[308949104,167669600]),[]). % % cnf(309419448,derived,(p(s1,s0,s0,s0,s0,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[309198656,167663384]),[]). % % cnf(309693248,derived,(p(s1,s0,s0,s0,s1,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[309419448,167700408]),[]). % % cnf(309892280,derived,(p(s1,s0,s0,s0,s1,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[309693248,167663384]),[]). % % cnf(310135440,derived,(p(s1,s0,s0,s0,s1,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[309892280,167669600]),[]). % % cnf(310362736,derived,(p(s1,s0,s0,s0,s1,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[310135440,167663384]),[]). % % cnf(310628312,derived,(p(s1,s0,s0,s0,s1,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[310362736,167679376]),[]). % % cnf(310830672,derived,(p(s1,s0,s0,s0,s1,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[310628312,167663384]),[]). % % cnf(311080200,derived,(p(s1,s0,s0,s0,s1,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[310830672,167669600]),[]). % % cnf(311301048,derived,(p(s1,s0,s0,s0,s1,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[311080200,167663384]),[]). % % cnf(311573952,derived,(p(s1,s0,s0,s0,s1,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[311301048,167685056]),[]). % % cnf(311774712,derived,(p(s1,s0,s0,s0,s1,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[311573952,167663384]),[]). % % cnf(312024240,derived,(p(s1,s0,s0,s0,s1,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[311774712,167669600]),[]). % % cnf(312241000,derived,(p(s1,s0,s0,s0,s1,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[312024240,167663384]),[]). % % cnf(312506600,derived,(p(s1,s0,s0,s0,s1,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[312241000,167679376]),[]). % % cnf(312712992,derived,(p(s1,s0,s0,s0,s1,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[312506600,167663384]),[]). % % cnf(312962544,derived,(p(s1,s0,s0,s0,s1,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[312712992,167669600]),[]). % % cnf(313179248,derived,(p(s1,s0,s0,s0,s1,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[312962544,167663384]),[]). % % cnf(313450560,derived,(p(s1,s0,s0,s0,s1,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[313179248,167694792]),[]). % % cnf(313654608,derived,(p(s1,s0,s0,s0,s1,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[313450560,167663384]),[]). % % cnf(313904136,derived,(p(s1,s0,s0,s0,s1,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[313654608,167669600]),[]). % % cnf(314120896,derived,(p(s1,s0,s0,s0,s1,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[313904136,167663384]),[]). % % cnf(314386496,derived,(p(s1,s0,s0,s0,s1,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[314120896,167679376]),[]). % % cnf(314592888,derived,(p(s1,s0,s0,s0,s1,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[314386496,167663384]),[]). % % cnf(314838344,derived,(p(s1,s0,s0,s0,s1,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[314592888,167669600]),[]). % % cnf(315059136,derived,(p(s1,s0,s0,s0,s1,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[314838344,167663384]),[]). % % cnf(315328000,derived,(p(s1,s0,s0,s0,s1,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[315059136,167685056]),[]). % % cnf(315528760,derived,(p(s1,s0,s0,s0,s1,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[315328000,167663384]),[]). % % cnf(315778288,derived,(p(s1,s0,s0,s0,s1,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[315528760,167669600]),[]). % % cnf(315999080,derived,(p(s1,s0,s0,s0,s1,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[315778288,167663384]),[]). % % cnf(316264736,derived,(p(s1,s0,s0,s0,s1,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[315999080,167679376]),[]). % % cnf(316467000,derived,(p(s1,s0,s0,s0,s1,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[316264736,167663384]),[]). % % cnf(316716592,derived,(p(s1,s0,s0,s0,s1,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[316467000,167669600]),[]). % % cnf(316932464,derived,(p(s1,s0,s0,s0,s1,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[316716592,167663384]),[]). % % cnf(317213576,derived,(p(s1,s0,s0,s1,s0,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[316932464,167706048]),[]). % % cnf(317411880,derived,(p(s1,s0,s0,s1,s0,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[317213576,167663384]),[]). % % cnf(317661472,derived,(p(s1,s0,s0,s1,s0,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[317411880,167669600]),[]). % % cnf(317878232,derived,(p(s1,s0,s0,s1,s0,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[317661472,167663384]),[]). % % cnf(318139888,derived,(p(s1,s0,s0,s1,s0,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[317878232,167679376]),[]). % % cnf(318354320,derived,(p(s1,s0,s0,s1,s0,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[318139888,167663384]),[]). % % cnf(318603888,derived,(p(s1,s0,s0,s1,s0,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[318354320,167669600]),[]). % % cnf(318820648,derived,(p(s1,s0,s0,s1,s0,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[318603888,167663384]),[]). % % cnf(319079904,derived,(p(s1,s0,s0,s1,s0,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[318820648,167685056]),[]). % % cnf(319294296,derived,(p(s1,s0,s0,s1,s0,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[319079904,167663384]),[]). % % cnf(319543824,derived,(p(s1,s0,s0,s1,s0,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[319294296,167669600]),[]). % % cnf(319760584,derived,(p(s1,s0,s0,s1,s0,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[319543824,167663384]),[]). % % cnf(320026184,derived,(p(s1,s0,s0,s1,s0,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[319760584,167679376]),[]). % % cnf(320232592,derived,(p(s1,s0,s0,s1,s0,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[320026184,167663384]),[]). % % cnf(320482144,derived,(p(s1,s0,s0,s1,s0,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[320232592,167669600]),[]). % % cnf(320698824,derived,(p(s1,s0,s0,s1,s0,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[320482144,167663384]),[]). % % cnf(320959040,derived,(p(s1,s0,s0,s1,s0,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[320698824,167694792]),[]). % % cnf(321170072,derived,(p(s1,s0,s0,s1,s0,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[320959040,167663384]),[]). % % cnf(321419624,derived,(p(s1,s0,s0,s1,s0,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[321170072,167669600]),[]). % % cnf(321640472,derived,(p(s1,s0,s0,s1,s0,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[321419624,167663384]),[]). % % cnf(321906072,derived,(p(s1,s0,s0,s1,s0,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[321640472,167679376]),[]). % % cnf(322108392,derived,(p(s1,s0,s0,s1,s0,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[321906072,167663384]),[]). % % cnf(322362016,derived,(p(s1,s0,s0,s1,s0,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[322108392,167669600]),[]). % % cnf(322582784,derived,(p(s1,s0,s0,s1,s0,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[322362016,167663384]),[]). % % cnf(322851672,derived,(p(s1,s0,s0,s1,s0,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[322582784,167685056]),[]). % % cnf(323052432,derived,(p(s1,s0,s0,s1,s0,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[322851672,167663384]),[]). % % cnf(323301960,derived,(p(s1,s0,s0,s1,s0,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[323052432,167669600]),[]). % % cnf(323522728,derived,(p(s1,s0,s0,s1,s0,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[323301960,167663384]),[]). % % cnf(323788408,derived,(p(s1,s0,s0,s1,s0,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[323522728,167679376]),[]). % % cnf(323990672,derived,(p(s1,s0,s0,s1,s0,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[323788408,167663384]),[]). % % cnf(324240264,derived,(p(s1,s0,s0,s1,s0,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[323990672,167669600]),[]). % % cnf(324452048,derived,(p(s1,s0,s0,s1,s0,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[324240264,167663384]),[]). % % cnf(324739016,derived,(p(s1,s0,s0,s1,s1,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[324452048,167700408]),[]). % % cnf(324938048,derived,(p(s1,s0,s0,s1,s1,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[324739016,167663384]),[]). % % cnf(325187576,derived,(p(s1,s0,s0,s1,s1,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[324938048,167669600]),[]). % % cnf(325404336,derived,(p(s1,s0,s0,s1,s1,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[325187576,167663384]),[]). % % cnf(325669936,derived,(p(s1,s0,s0,s1,s1,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[325404336,167679376]),[]). % % cnf(325876344,derived,(p(s1,s0,s0,s1,s1,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[325669936,167663384]),[]). % % cnf(326125872,derived,(p(s1,s0,s0,s1,s1,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[325876344,167669600]),[]). % % cnf(326342552,derived,(p(s1,s0,s0,s1,s1,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[326125872,167663384]),[]). % % cnf(326611440,derived,(p(s1,s0,s0,s1,s1,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[326342552,167685056]),[]). % % cnf(326816288,derived,(p(s1,s0,s0,s1,s1,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[326611440,167663384]),[]). % % cnf(327061728,derived,(p(s1,s0,s0,s1,s1,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[326816288,167669600]),[]). % % cnf(327282496,derived,(p(s1,s0,s0,s1,s1,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[327061728,167663384]),[]). % % cnf(327548176,derived,(p(s1,s0,s0,s1,s1,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[327282496,167679376]),[]). % % cnf(327750440,derived,(p(s1,s0,s0,s1,s1,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[327548176,167663384]),[]). % % cnf(327993576,derived,(p(s1,s0,s0,s1,s1,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[327750440,167669600]),[]). % % cnf(328215904,derived,(p(s1,s0,s0,s1,s1,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[327993576,167663384]),[]). % % cnf(328492120,derived,(p(s1,s0,s0,s1,s1,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[328215904,167694792]),[]). % % cnf(328692080,derived,(p(s1,s0,s0,s1,s1,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[328492120,167663384]),[]). % % cnf(328941608,derived,(p(s1,s0,s0,s1,s1,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[328692080,167669600]),[]). % % cnf(329162400,derived,(p(s1,s0,s0,s1,s1,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[328941608,167663384]),[]). % % cnf(329428056,derived,(p(s1,s0,s0,s1,s1,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[329162400,167679376]),[]). % % cnf(329625440,derived,(p(s1,s0,s0,s1,s1,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[329428056,167663384]),[]). % % cnf(329873472,derived,(p(s1,s0,s0,s1,s1,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[329625440,167669600]),[]). % % cnf(330095800,derived,(p(s1,s0,s0,s1,s1,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[329873472,167663384]),[]). % % cnf(330369576,derived,(p(s1,s0,s0,s1,s1,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[330095800,167685056]),[]). % % cnf(330570256,derived,(p(s1,s0,s0,s1,s1,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[330369576,167663384]),[]). % % cnf(330817512,derived,(p(s1,s0,s0,s1,s1,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[330570256,167669600]),[]). % % cnf(331035752,derived,(p(s1,s0,s0,s1,s1,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[330817512,167663384]),[]). % % cnf(331306296,derived,(p(s1,s0,s0,s1,s1,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[331035752,167679376]),[]). % % cnf(331507768,derived,(p(s1,s0,s0,s1,s1,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[331306296,167663384]),[]). % % cnf(331766392,derived,(p(s1,s0,s0,s1,s1,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[331507768,167669600]),[]). % % cnf(331978136,derived,(p(s1,s0,s0,s1,s1,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[331766392,167663384]),[]). % % cnf(332260048,derived,(p(s1,s0,s1,s0,s0,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[331978136,167715744]),[]). % % cnf(332461616,derived,(p(s1,s0,s1,s0,s0,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[332260048,167663384]),[]). % % cnf(332704776,derived,(p(s1,s0,s1,s0,s0,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[332461616,167669600]),[]). % % cnf(332927984,derived,(p(s1,s0,s1,s0,s0,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[332704776,167663384]),[]). % % cnf(333193560,derived,(p(s1,s0,s1,s0,s0,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[332927984,167679376]),[]). % % cnf(333400008,derived,(p(s1,s0,s1,s0,s0,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[333193560,167663384]),[]). % % cnf(333645448,derived,(p(s1,s0,s1,s0,s0,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[333400008,167669600]),[]). % % cnf(333866296,derived,(p(s1,s0,s1,s0,s0,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[333645448,167663384]),[]). % % cnf(334135112,derived,(p(s1,s0,s1,s0,s0,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[333866296,167685056]),[]). % % cnf(334335872,derived,(p(s1,s0,s1,s0,s0,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[334135112,167663384]),[]). % % cnf(334585400,derived,(p(s1,s0,s1,s0,s0,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[334335872,167669600]),[]). % % cnf(334806248,derived,(p(s1,s0,s1,s0,s0,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[334585400,167663384]),[]). % % cnf(335071848,derived,(p(s1,s0,s1,s0,s0,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[334806248,167679376]),[]). % % cnf(335274152,derived,(p(s1,s0,s1,s0,s0,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[335071848,167663384]),[]). % % cnf(335523704,derived,(p(s1,s0,s1,s0,s0,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[335274152,167669600]),[]). % % cnf(335744496,derived,(p(s1,s0,s1,s0,s0,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[335523704,167663384]),[]). % % cnf(336015808,derived,(p(s1,s0,s1,s0,s0,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[335744496,167694792]),[]). % % cnf(336215768,derived,(p(s1,s0,s1,s0,s0,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[336015808,167663384]),[]). % % cnf(336465296,derived,(p(s1,s0,s1,s0,s0,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[336215768,167669600]),[]). % % cnf(336686144,derived,(p(s1,s0,s1,s0,s0,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[336465296,167663384]),[]). % % cnf(336951744,derived,(p(s1,s0,s1,s0,s0,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[336686144,167679376]),[]). % % cnf(337154048,derived,(p(s1,s0,s1,s0,s0,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[336951744,167663384]),[]). % % cnf(337403600,derived,(p(s1,s0,s1,s0,s0,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[337154048,167669600]),[]). % % cnf(337620304,derived,(p(s1,s0,s1,s0,s0,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[337403600,167663384]),[]). % % cnf(337889168,derived,(p(s1,s0,s1,s0,s0,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[337620304,167685056]),[]). % % cnf(338098104,derived,(p(s1,s0,s1,s0,s0,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[337889168,167663384]),[]). % % cnf(338347632,derived,(p(s1,s0,s1,s0,s0,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[338098104,167669600]),[]). % % cnf(338564336,derived,(p(s1,s0,s1,s0,s0,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[338347632,167663384]),[]). % % cnf(338829992,derived,(p(s1,s0,s1,s0,s0,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[338564336,167679376]),[]). % % cnf(339031464,derived,(p(s1,s0,s1,s0,s0,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[338829992,167663384]),[]). % % cnf(339283680,derived,(p(s1,s0,s1,s0,s0,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[339031464,167669600]),[]). % % cnf(339501832,derived,(p(s1,s0,s1,s0,s0,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[339283680,167663384]),[]). % % cnf(339780496,derived,(p(s1,s0,s1,s0,s1,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[339501832,167700408]),[]). % % cnf(339983672,derived,(p(s1,s0,s1,s0,s1,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[339780496,167663384]),[]). % % cnf(340229176,derived,(p(s1,s0,s1,s0,s1,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[339983672,167669600]),[]). % % cnf(340450024,derived,(p(s1,s0,s1,s0,s1,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[340229176,167663384]),[]). % % cnf(340715624,derived,(p(s1,s0,s1,s0,s1,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[340450024,167679376]),[]). % % cnf(340917928,derived,(p(s1,s0,s1,s0,s1,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[340715624,167663384]),[]). % % cnf(341167480,derived,(p(s1,s0,s1,s0,s1,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[340917928,167669600]),[]). % % cnf(341388272,derived,(p(s1,s0,s1,s0,s1,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[341167480,167663384]),[]). % % cnf(341657136,derived,(p(s1,s0,s1,s0,s1,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[341388272,167685056]),[]). % % cnf(341857896,derived,(p(s1,s0,s1,s0,s1,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[341657136,167663384]),[]). % % cnf(342107424,derived,(p(s1,s0,s1,s0,s1,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[341857896,167669600]),[]). % % cnf(342328192,derived,(p(s1,s0,s1,s0,s1,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[342107424,167663384]),[]). % % cnf(342593872,derived,(p(s1,s0,s1,s0,s1,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[342328192,167679376]),[]). % % cnf(342796136,derived,(p(s1,s0,s1,s0,s1,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[342593872,167663384]),[]). % % cnf(343045728,derived,(p(s1,s0,s1,s0,s1,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[342796136,167669600]),[]). % % cnf(343257512,derived,(p(s1,s0,s1,s0,s1,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[343045728,167663384]),[]). % % cnf(343537824,derived,(p(s1,s0,s1,s0,s1,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[343257512,167694792]),[]). % % cnf(343742848,derived,(p(s1,s0,s1,s0,s1,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[343537824,167663384]),[]). % % cnf(343992376,derived,(p(s1,s0,s1,s0,s1,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[343742848,167669600]),[]). % % cnf(344209056,derived,(p(s1,s0,s1,s0,s1,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[343992376,167663384]),[]). % % cnf(344474736,derived,(p(s1,s0,s1,s0,s1,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[344209056,167679376]),[]). % % cnf(344681088,derived,(p(s1,s0,s1,s0,s1,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[344474736,167663384]),[]). % % cnf(344934768,derived,(p(s1,s0,s1,s0,s1,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[344681088,167669600]),[]). % % cnf(345146552,derived,(p(s1,s0,s1,s0,s1,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[344934768,167663384]),[]). % % cnf(345420336,derived,(p(s1,s0,s1,s0,s1,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[345146552,167685056]),[]). % % cnf(345625128,derived,(p(s1,s0,s1,s0,s1,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[345420336,167663384]),[]). % % cnf(345870632,derived,(p(s1,s0,s1,s0,s1,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[345625128,167669600]),[]). % % cnf(346086504,derived,(p(s1,s0,s1,s0,s1,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[345870632,167663384]),[]). % % cnf(346349048,derived,(p(s1,s0,s1,s0,s1,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[346086504,167679376]),[]). % % cnf(346554472,derived,(p(s1,s0,s1,s0,s1,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[346349048,167663384]),[]). % % cnf(346809072,derived,(p(s1,s0,s1,s0,s1,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[346554472,167669600]),[]). % % cnf(347024832,derived,(p(s1,s0,s1,s0,s1,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[346809072,167663384]),[]). % % cnf(347304408,derived,(p(s1,s0,s1,s1,s0,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[347024832,167706048]),[]). % % cnf(347502640,derived,(p(s1,s0,s1,s1,s0,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[347304408,167663384]),[]). % % cnf(347752168,derived,(p(s1,s0,s1,s1,s0,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[347502640,167669600]),[]). % % cnf(347977112,derived,(p(s1,s0,s1,s1,s0,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[347752168,167663384]),[]). % % cnf(348242712,derived,(p(s1,s0,s1,s1,s0,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[347977112,167679376]),[]). % % cnf(348445032,derived,(p(s1,s0,s1,s1,s0,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[348242712,167663384]),[]). % % cnf(348694560,derived,(p(s1,s0,s1,s1,s0,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[348445032,167669600]),[]). % % cnf(348915328,derived,(p(s1,s0,s1,s1,s0,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[348694560,167663384]),[]). % % cnf(349184216,derived,(p(s1,s0,s1,s1,s0,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[348915328,167685056]),[]). % % cnf(349384976,derived,(p(s1,s0,s1,s1,s0,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[349184216,167663384]),[]). % % cnf(349634504,derived,(p(s1,s0,s1,s1,s0,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[349384976,167669600]),[]). % % cnf(349851184,derived,(p(s1,s0,s1,s1,s0,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[349634504,167663384]),[]). % % cnf(350120920,derived,(p(s1,s0,s1,s1,s0,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[349851184,167679376]),[]). % % cnf(350323224,derived,(p(s1,s0,s1,s1,s0,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[350120920,167663384]),[]). % % cnf(350572816,derived,(p(s1,s0,s1,s1,s0,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[350323224,167669600]),[]). % % cnf(350784600,derived,(p(s1,s0,s1,s1,s0,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[350572816,167663384]),[]). % % cnf(351060824,derived,(p(s1,s0,s1,s1,s0,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[350784600,167694792]),[]). % % cnf(351264840,derived,(p(s1,s0,s1,s1,s0,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[351060824,167663384]),[]). % % cnf(351518496,derived,(p(s1,s0,s1,s1,s0,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[351264840,167669600]),[]). % % cnf(351735176,derived,(p(s1,s0,s1,s1,s0,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[351518496,167663384]),[]). % % cnf(352000816,derived,(p(s1,s0,s1,s1,s0,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[351735176,167679376]),[]). % % cnf(352207208,derived,(p(s1,s0,s1,s1,s0,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[352000816,167663384]),[]). % % cnf(352446256,derived,(p(s1,s0,s1,s1,s0,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[352207208,167669600]),[]). % % cnf(352668576,derived,(p(s1,s0,s1,s1,s0,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[352446256,167663384]),[]). % % cnf(352942352,derived,(p(s1,s0,s1,s1,s0,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[352668576,167685056]),[]). % % cnf(353143056,derived,(p(s1,s0,s1,s1,s0,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[352942352,167663384]),[]). % % cnf(353386192,derived,(p(s1,s0,s1,s1,s0,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[353143056,167669600]),[]). % % cnf(353609056,derived,(p(s1,s0,s1,s1,s0,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[353386192,167663384]),[]). % % cnf(353879600,derived,(p(s1,s0,s1,s1,s0,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[353609056,167679376]),[]). % % cnf(354076968,derived,(p(s1,s0,s1,s1,s0,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[353879600,167663384]),[]). % % cnf(354331600,derived,(p(s1,s0,s1,s1,s0,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[354076968,167669600]),[]). % % cnf(354547320,derived,(p(s1,s0,s1,s1,s0,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[354331600,167663384]),[]). % % cnf(354824344,derived,(p(s1,s0,s1,s1,s1,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[354547320,167700408]),[]). % % cnf(355023472,derived,(p(s1,s0,s1,s1,s1,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[354824344,167663384]),[]). % % cnf(355273024,derived,(p(s1,s0,s1,s1,s1,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[355023472,167669600]),[]). % % cnf(355493872,derived,(p(s1,s0,s1,s1,s1,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[355273024,167663384]),[]). % % cnf(355759448,derived,(p(s1,s0,s1,s1,s1,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[355493872,167679376]),[]). % % cnf(355961808,derived,(p(s1,s0,s1,s1,s1,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[355759448,167663384]),[]). % % cnf(356211336,derived,(p(s1,s0,s1,s1,s1,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[355961808,167669600]),[]). % % cnf(356427224,derived,(p(s1,s0,s1,s1,s1,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[356211336,167663384]),[]). % % cnf(356701008,derived,(p(s1,s0,s1,s1,s1,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[356427224,167685056]),[]). % % cnf(356905856,derived,(p(s1,s0,s1,s1,s1,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[356701008,167663384]),[]). % % cnf(357155384,derived,(p(s1,s0,s1,s1,s1,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[356905856,167669600]),[]). % % cnf(357367176,derived,(p(s1,s0,s1,s1,s1,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[357155384,167663384]),[]). % % cnf(357637744,derived,(p(s1,s0,s1,s1,s1,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[357367176,167679376]),[]). % % cnf(357839216,derived,(p(s1,s0,s1,s1,s1,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[357637744,167663384]),[]). % % cnf(358093832,derived,(p(s1,s0,s1,s1,s1,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[357839216,167669600]),[]). % % cnf(358305464,derived,(p(s1,s0,s1,s1,s1,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[358093832,167663384]),[]). % % cnf(358584160,derived,(p(s1,s0,s1,s1,s1,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[358305464,167694792]),[]). % % cnf(358788184,derived,(p(s1,s0,s1,s1,s1,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[358584160,167663384]),[]). % % cnf(359033640,derived,(p(s1,s0,s1,s1,s1,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[358788184,167669600]),[]). % % cnf(359249520,derived,(p(s1,s0,s1,s1,s1,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[359033640,167663384]),[]). % % cnf(359520088,derived,(p(s1,s0,s1,s1,s1,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[359249520,167679376]),[]). % % cnf(359717472,derived,(p(s1,s0,s1,s1,s1,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[359520088,167663384]),[]). % % cnf(359972088,derived,(p(s1,s0,s1,s1,s1,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[359717472,167669600]),[]). % % cnf(360187808,derived,(p(s1,s0,s1,s1,s1,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[359972088,167663384]),[]). % % cnf(360463088,derived,(p(s1,s0,s1,s1,s1,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[360187808,167685056]),[]). % % cnf(360658872,derived,(p(s1,s0,s1,s1,s1,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[360463088,167663384]),[]). % % cnf(360916584,derived,(p(s1,s0,s1,s1,s1,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[360658872,167669600]),[]). % % cnf(361132304,derived,(p(s1,s0,s1,s1,s1,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[360916584,167663384]),[]). % % cnf(361401352,derived,(p(s1,s0,s1,s1,s1,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[361132304,167679376]),[]). % % cnf(361598624,derived,(p(s1,s0,s1,s1,s1,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[361401352,167663384]),[]). % % cnf(361846384,derived,(p(s1,s0,s1,s1,s1,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[361598624,167669600]),[]). % % cnf(362058224,derived,(p(s1,s0,s1,s1,s1,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[361846384,167663384]),[]). % % cnf(goal,plain, % % cnf(167730904,derived,(~p(s1,s1,s1,s1,s1,s1,s1,s1,s1,s1)),inference(rewrite,[status(thm)],[goal]),[]). % % cnf(175533840,derived,(~p(s1,s1,s1,s1,s1,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[167663384,167730904]),[]). % % cnf(175553048,derived,(~p(s1,s1,s1,s1,s1,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[167669600,175533840]),[]). % % cnf(175612536,derived,(~p(s1,s1,s1,s1,s1,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[175553048,167663384]),[]). % % cnf(175650688,derived,(~p(s1,s1,s1,s1,s1,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[167679376,175612536]),[]). % % cnf(175754040,derived,(~p(s1,s1,s1,s1,s1,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[175650688,167663384]),[]). % % cnf(175777952,derived,(~p(s1,s1,s1,s1,s1,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[175754040,167669600]),[]). % % cnf(175798616,derived,(~p(s1,s1,s1,s1,s1,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[175777952,167663384]),[]). % % cnf(175859416,derived,(~p(s1,s1,s1,s1,s1,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[167685056,175798616]),[]). % % cnf(176068216,derived,(~p(s1,s1,s1,s1,s1,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[175859416,167663384]),[]). % % cnf(176099328,derived,(~p(s1,s1,s1,s1,s1,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[176068216,167669600]),[]). % % cnf(176131288,derived,(~p(s1,s1,s1,s1,s1,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[176099328,167663384]),[]). % % cnf(176168912,derived,(~p(s1,s1,s1,s1,s1,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[176131288,167679376]),[]). % % cnf(176196048,derived,(~p(s1,s1,s1,s1,s1,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[176168912,167663384]),[]). % % cnf(176231168,derived,(~p(s1,s1,s1,s1,s1,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[176196048,167669600]),[]). % % cnf(176259008,derived,(~p(s1,s1,s1,s1,s1,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[176231168,167663384]),[]). % % cnf(176341616,derived,(~p(s1,s1,s1,s1,s1,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[167694792,176259008]),[]). % % cnf(176850400,derived,(~p(s1,s1,s1,s1,s1,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[176341616,167663384]),[]). % % cnf(176895096,derived,(~p(s1,s1,s1,s1,s1,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[176850400,167669600]),[]). % % cnf(176940640,derived,(~p(s1,s1,s1,s1,s1,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[176895096,167663384]),[]). % % cnf(176987792,derived,(~p(s1,s1,s1,s1,s1,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[176940640,167679376]),[]). % % cnf(177032568,derived,(~p(s1,s1,s1,s1,s1,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[176987792,167663384]),[]). % % cnf(177077272,derived,(~p(s1,s1,s1,s1,s1,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[177032568,167669600]),[]). % % cnf(177122920,derived,(~p(s1,s1,s1,s1,s1,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[177077272,167663384]),[]). % % cnf(177172496,derived,(~p(s1,s1,s1,s1,s1,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[177122920,167685056]),[]). % % cnf(177216520,derived,(~p(s1,s1,s1,s1,s1,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[177172496,167663384]),[]). % % cnf(177261152,derived,(~p(s1,s1,s1,s1,s1,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[177216520,167669600]),[]). % % cnf(177306808,derived,(~p(s1,s1,s1,s1,s1,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[177261152,167663384]),[]). % % cnf(177353872,derived,(~p(s1,s1,s1,s1,s1,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[177306808,167679376]),[]). % % cnf(177402704,derived,(~p(s1,s1,s1,s1,s1,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[177353872,167663384]),[]). % % cnf(177447416,derived,(~p(s1,s1,s1,s1,s1,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[177402704,167669600]),[]). % % cnf(177492976,derived,(~p(s1,s1,s1,s1,s1,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[177447416,167663384]),[]). % % cnf(177617312,derived,(~p(s1,s1,s1,s1,s0,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[167700408,177492976]),[]). % % cnf(179069048,derived,(~p(s1,s1,s1,s1,s0,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[177617312,167663384]),[]). % % cnf(179144232,derived,(~p(s1,s1,s1,s1,s0,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[179069048,167669600]),[]). % % cnf(179216280,derived,(~p(s1,s1,s1,s1,s0,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[179144232,167663384]),[]). % % cnf(179293904,derived,(~p(s1,s1,s1,s1,s0,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[179216280,167679376]),[]). % % cnf(179365048,derived,(~p(s1,s1,s1,s1,s0,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[179293904,167663384]),[]). % % cnf(179436160,derived,(~p(s1,s1,s1,s1,s0,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[179365048,167669600]),[]). % % cnf(179520400,derived,(~p(s1,s1,s1,s1,s0,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[179436160,167663384]),[]). % % cnf(179600464,derived,(~p(s1,s1,s1,s1,s0,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[179520400,167685056]),[]). % % cnf(179670808,derived,(~p(s1,s1,s1,s1,s0,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[179600464,167663384]),[]). % % cnf(179746008,derived,(~p(s1,s1,s1,s1,s0,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[179670808,167669600]),[]). % % cnf(179817944,derived,(~p(s1,s1,s1,s1,s0,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[179746008,167663384]),[]). % % cnf(179891480,derived,(~p(s1,s1,s1,s1,s0,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[179817944,167679376]),[]). % % cnf(179962624,derived,(~p(s1,s1,s1,s1,s0,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[179891480,167663384]),[]). % % cnf(180037824,derived,(~p(s1,s1,s1,s1,s0,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[179962624,167669600]),[]). % % cnf(180109880,derived,(~p(s1,s1,s1,s1,s0,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[180037824,167663384]),[]). % % cnf(180192304,derived,(~p(s1,s1,s1,s1,s0,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[180109880,167694792]),[]). % % cnf(180257840,derived,(~p(s1,s1,s1,s1,s0,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[180192304,167663384]),[]). % % cnf(180333024,derived,(~p(s1,s1,s1,s1,s0,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[180257840,167669600]),[]). % % cnf(180404968,derived,(~p(s1,s1,s1,s1,s0,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[180333024,167663384]),[]). % % cnf(180482592,derived,(~p(s1,s1,s1,s1,s0,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[180404968,167679376]),[]). % % cnf(180553736,derived,(~p(s1,s1,s1,s1,s0,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[180482592,167663384]),[]). % % cnf(180628936,derived,(~p(s1,s1,s1,s1,s0,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[180553736,167669600]),[]). % % cnf(180700880,derived,(~p(s1,s1,s1,s1,s0,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[180628936,167663384]),[]). % % cnf(180780952,derived,(~p(s1,s1,s1,s1,s0,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[180700880,167685056]),[]). % % cnf(180851296,derived,(~p(s1,s1,s1,s1,s0,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[180780952,167663384]),[]). % % cnf(180926496,derived,(~p(s1,s1,s1,s1,s0,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[180851296,167669600]),[]). % % cnf(180994352,derived,(~p(s1,s1,s1,s1,s0,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[180926496,167663384]),[]). % % cnf(181071976,derived,(~p(s1,s1,s1,s1,s0,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[180994352,167679376]),[]). % % cnf(181143120,derived,(~p(s1,s1,s1,s1,s0,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[181071976,167663384]),[]). % % cnf(181218336,derived,(~p(s1,s1,s1,s1,s0,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[181143120,167669600]),[]). % % cnf(181294368,derived,(~p(s1,s1,s1,s1,s0,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[181218336,167663384]),[]). % % cnf(181504728,derived,(~p(s1,s1,s1,s0,s1,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[167706048,181294368]),[]). % % cnf(186165520,derived,(~p(s1,s1,s1,s0,s1,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[181504728,167663384]),[]). % % cnf(186296792,derived,(~p(s1,s1,s1,s0,s1,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[186165520,167669600]),[]). % % cnf(186420792,derived,(~p(s1,s1,s1,s0,s1,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[186296792,167663384]),[]). % % cnf(186558600,derived,(~p(s1,s1,s1,s0,s1,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[186420792,167679376]),[]). % % cnf(186681736,derived,(~p(s1,s1,s1,s0,s1,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[186558600,167663384]),[]). % % cnf(186808968,derived,(~p(s1,s1,s1,s0,s1,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[186681736,167669600]),[]). % % cnf(186936952,derived,(~p(s1,s1,s1,s0,s1,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[186808968,167663384]),[]). % % cnf(187069016,derived,(~p(s1,s1,s1,s0,s1,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[186936952,167685056]),[]). % % cnf(187195440,derived,(~p(s1,s1,s1,s0,s1,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[187069016,167663384]),[]). % % cnf(187322672,derived,(~p(s1,s1,s1,s0,s1,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[187195440,167669600]),[]). % % cnf(187450656,derived,(~p(s1,s1,s1,s0,s1,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[187322672,167663384]),[]). % % cnf(187580344,derived,(~p(s1,s1,s1,s0,s1,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[187450656,167679376]),[]). % % cnf(187707568,derived,(~p(s1,s1,s1,s0,s1,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[187580344,167663384]),[]). % % cnf(187834800,derived,(~p(s1,s1,s1,s0,s1,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[187707568,167669600]),[]). % % cnf(187962784,derived,(~p(s1,s1,s1,s0,s1,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[187834800,167663384]),[]). % % cnf(188097288,derived,(~p(s1,s1,s1,s0,s1,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[187962784,167694792]),[]). % % cnf(188218824,derived,(~p(s1,s1,s1,s0,s1,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[188097288,167663384]),[]). % % cnf(188350248,derived,(~p(s1,s1,s1,s0,s1,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[188218824,167669600]),[]). % % cnf(188474048,derived,(~p(s1,s1,s1,s0,s1,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[188350248,167663384]),[]). % % cnf(188607800,derived,(~p(s1,s1,s1,s0,s1,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[188474048,167679376]),[]). % % cnf(188780120,derived,(~p(s1,s1,s1,s0,s1,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[188607800,167663384]),[]). % % cnf(188911440,derived,(~p(s1,s1,s1,s0,s1,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[188780120,167669600]),[]). % % cnf(189035336,derived,(~p(s1,s1,s1,s0,s1,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[188911440,167663384]),[]). % % cnf(189171488,derived,(~p(s1,s1,s1,s0,s1,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[189035336,167685056]),[]). % % cnf(189297912,derived,(~p(s1,s1,s1,s0,s1,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[189171488,167663384]),[]). % % cnf(189429208,derived,(~p(s1,s1,s1,s0,s1,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[189297912,167669600]),[]). % % cnf(189553128,derived,(~p(s1,s1,s1,s0,s1,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[189429208,167663384]),[]). % % cnf(189682816,derived,(~p(s1,s1,s1,s0,s1,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[189553128,167679376]),[]). % % cnf(189810024,derived,(~p(s1,s1,s1,s0,s1,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[189682816,167663384]),[]). % % cnf(189937256,derived,(~p(s1,s1,s1,s0,s1,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[189810024,167669600]),[]). % % cnf(190056464,derived,(~p(s1,s1,s1,s0,s1,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[189937256,167663384]),[]). % % cnf(190202192,derived,(~p(s1,s1,s1,s0,s0,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[190056464,167700408]),[]). % % cnf(190322336,derived,(~p(s1,s1,s1,s0,s0,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[190202192,167663384]),[]). % % cnf(190458456,derived,(~p(s1,s1,s1,s0,s0,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[190322336,167669600]),[]). % % cnf(190577568,derived,(~p(s1,s1,s1,s0,s0,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[190458456,167663384]),[]). % % cnf(190715984,derived,(~p(s1,s1,s1,s0,s0,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[190577568,167679376]),[]). % % cnf(190843376,derived,(~p(s1,s1,s1,s0,s0,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[190715984,167663384]),[]). % % cnf(190960200,derived,(~p(s1,s1,s1,s0,s0,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[190843376,167669600]),[]). % % cnf(191094472,derived,(~p(s1,s1,s1,s0,s0,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[190960200,167663384]),[]). % % cnf(191230640,derived,(~p(s1,s1,s1,s0,s0,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[191094472,167685056]),[]). % % cnf(191344184,derived,(~p(s1,s1,s1,s0,s0,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[191230640,167663384]),[]). % % cnf(191473912,derived,(~p(s1,s1,s1,s0,s0,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[191344184,167669600]),[]). % % cnf(191599408,derived,(~p(s1,s1,s1,s0,s0,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[191473912,167663384]),[]). % % cnf(191742016,derived,(~p(s1,s1,s1,s0,s0,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[191599408,167679376]),[]). % % cnf(191856264,derived,(~p(s1,s1,s1,s0,s0,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[191742016,167663384]),[]). % % cnf(192000560,derived,(~p(s1,s1,s1,s0,s0,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[191856264,167669600]),[]). % % cnf(192115584,derived,(~p(s1,s1,s1,s0,s0,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[192000560,167663384]),[]). % % cnf(192263056,derived,(~p(s1,s1,s1,s0,s0,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[192115584,167694792]),[]). % % cnf(192375736,derived,(~p(s1,s1,s1,s0,s0,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[192263056,167663384]),[]). % % cnf(192501376,derived,(~p(s1,s1,s1,s0,s0,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[192375736,167669600]),[]). % % cnf(192631096,derived,(~p(s1,s1,s1,s0,s0,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[192501376,167663384]),[]). % % cnf(192769616,derived,(~p(s1,s1,s1,s0,s0,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[192631096,167679376]),[]). % % cnf(192887952,derived,(~p(s1,s1,s1,s0,s0,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[192769616,167663384]),[]). % % cnf(193024136,derived,(~p(s1,s1,s1,s0,s0,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[192887952,167669600]),[]). % % cnf(193143248,derived,(~p(s1,s1,s1,s0,s0,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[193024136,167663384]),[]). % % cnf(193284112,derived,(~p(s1,s1,s1,s0,s0,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[193143248,167685056]),[]). % % cnf(193401744,derived,(~p(s1,s1,s1,s0,s0,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[193284112,167663384]),[]). % % cnf(193537864,derived,(~p(s1,s1,s1,s0,s0,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[193401744,167669600]),[]). % % cnf(193656976,derived,(~p(s1,s1,s1,s0,s0,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[193537864,167663384]),[]). % % cnf(193795440,derived,(~p(s1,s1,s1,s0,s0,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[193656976,167679376]),[]). % % cnf(193909760,derived,(~p(s1,s1,s1,s0,s0,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[193795440,167663384]),[]). % % cnf(194049968,derived,(~p(s1,s1,s1,s0,s0,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[193909760,167669600]),[]). % % cnf(194173824,derived,(~p(s1,s1,s1,s0,s0,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[194049968,167663384]),[]). % % cnf(194563560,derived,(~p(s1,s1,s0,s1,s1,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[167715744,194173824]),[]). % % cnf(210702488,derived,(~p(s1,s1,s0,s1,s1,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[194563560,167663384]),[]). % % cnf(210941104,derived,(~p(s1,s1,s0,s1,s1,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[210702488,167669600]),[]). % % cnf(211167600,derived,(~p(s1,s1,s0,s1,s1,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[210941104,167663384]),[]). % % cnf(211417376,derived,(~p(s1,s1,s0,s1,s1,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[211167600,167679376]),[]). % % cnf(211643112,derived,(~p(s1,s1,s0,s1,s1,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[211417376,167663384]),[]). % % cnf(211876040,derived,(~p(s1,s1,s0,s1,s1,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[211643112,167669600]),[]). % % cnf(212112912,derived,(~p(s1,s1,s0,s1,s1,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[211876040,167663384]),[]). % % cnf(212365128,derived,(~p(s1,s1,s0,s1,s1,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[212112912,167685056]),[]). % % cnf(212590064,derived,(~p(s1,s1,s0,s1,s1,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[212365128,167663384]),[]). % % cnf(212822992,derived,(~p(s1,s1,s0,s1,s1,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[212590064,167669600]),[]). % % cnf(213059864,derived,(~p(s1,s1,s0,s1,s1,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[212822992,167663384]),[]). % % cnf(213313840,derived,(~p(s1,s1,s0,s1,s1,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[213059864,167679376]),[]). % % cnf(213548272,derived,(~p(s1,s1,s0,s1,s1,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[213313840,167663384]),[]). % % cnf(213782744,derived,(~p(s1,s1,s0,s1,s1,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[213548272,167669600]),[]). % % cnf(214009400,derived,(~p(s1,s1,s0,s1,s1,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[213782744,167663384]),[]). % % cnf(214263944,derived,(~p(s1,s1,s0,s1,s1,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[214009400,167694792]),[]). % % cnf(214483992,derived,(~p(s1,s1,s0,s1,s1,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[214263944,167663384]),[]). % % cnf(214721008,derived,(~p(s1,s1,s0,s1,s1,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[214483992,167669600]),[]). % % cnf(214966688,derived,(~p(s1,s1,s0,s1,s1,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[214721008,167663384]),[]). % % cnf(215207760,derived,(~p(s1,s1,s0,s1,s1,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[214966688,167679376]),[]). % % cnf(215429320,derived,(~p(s1,s1,s0,s1,s1,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[215207760,167663384]),[]). % % cnf(215666400,derived,(~p(s1,s1,s0,s1,s1,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[215429320,167669600]),[]). % % cnf(215903216,derived,(~p(s1,s1,s0,s1,s1,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[215666400,167663384]),[]). % % cnf(216155456,derived,(~p(s1,s1,s0,s1,s1,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[215903216,167685056]),[]). % % cnf(216376304,derived,(~p(s1,s1,s0,s1,s1,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[216155456,167663384]),[]). % % cnf(216613384,derived,(~p(s1,s1,s0,s1,s1,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[216376304,167669600]),[]). % % cnf(216850200,derived,(~p(s1,s1,s0,s1,s1,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[216613384,167663384]),[]). % % cnf(217099992,derived,(~p(s1,s1,s0,s1,s1,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[216850200,167679376]),[]). % % cnf(217321760,derived,(~p(s1,s1,s0,s1,s1,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[217099992,167663384]),[]). % % cnf(217558712,derived,(~p(s1,s1,s0,s1,s1,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[217321760,167669600]),[]). % % cnf(217804304,derived,(~p(s1,s1,s0,s1,s1,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[217558712,167663384]),[]). % % cnf(218056696,derived,(~p(s1,s1,s0,s1,s0,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[217804304,167700408]),[]). % % cnf(218275944,derived,(~p(s1,s1,s0,s1,s0,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[218056696,167663384]),[]). % % cnf(218512960,derived,(~p(s1,s1,s0,s1,s0,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[218275944,167669600]),[]). % % cnf(218749848,derived,(~p(s1,s1,s0,s1,s0,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[218512960,167663384]),[]). % % cnf(218995656,derived,(~p(s1,s1,s0,s1,s0,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[218749848,167679376]),[]). % % cnf(219221304,derived,(~p(s1,s1,s0,s1,s0,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[218995656,167663384]),[]). % % cnf(219458384,derived,(~p(s1,s1,s0,s1,s0,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[219221304,167669600]),[]). % % cnf(219699296,derived,(~p(s1,s1,s0,s1,s0,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[219458384,167663384]),[]). % % cnf(219947448,derived,(~p(s1,s1,s0,s1,s0,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[219699296,167685056]),[]). % % cnf(220172384,derived,(~p(s1,s1,s0,s1,s0,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[219947448,167663384]),[]). % % cnf(220409464,derived,(~p(s1,s1,s0,s1,s0,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[220172384,167669600]),[]). % % cnf(220655056,derived,(~p(s1,s1,s0,s1,s0,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[220409464,167663384]),[]). % % cnf(220880080,derived,(~p(s1,s1,s0,s1,s0,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[220655056,167679376]),[]). % % cnf(221117832,derived,(~p(s1,s1,s0,s1,s0,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[220880080,167663384]),[]). % % cnf(221354784,derived,(~p(s1,s1,s0,s1,s0,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[221117832,167669600]),[]). % % cnf(221596288,derived,(~p(s1,s1,s0,s1,s0,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[221354784,167663384]),[]). % % cnf(221843064,derived,(~p(s1,s1,s0,s1,s0,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[221596288,167694792]),[]). % % cnf(222067136,derived,(~p(s1,s1,s0,s1,s0,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[221843064,167663384]),[]). % % cnf(222304216,derived,(~p(s1,s1,s0,s1,s0,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[222067136,167669600]),[]). % % cnf(222536944,derived,(~p(s1,s1,s0,s1,s0,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[222304216,167663384]),[]). % % cnf(222774856,derived,(~p(s1,s1,s0,s1,s0,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[222536944,167679376]),[]). % % cnf(223012608,derived,(~p(s1,s1,s0,s1,s0,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[222774856,167663384]),[]). % % cnf(223249560,derived,(~p(s1,s1,s0,s1,s0,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[223012608,167669600]),[]). % % cnf(167661072,derived,(~p(s1,s1,s0,s1,s0,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[223249560,167663384]),[]). % % cnf(223739528,derived,(~p(s1,s1,s0,s1,s0,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[167661072,167685056]),[]). % % cnf(223964584,derived,(~p(s1,s1,s0,s1,s0,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[223739528,167663384]),[]). % % cnf(224212592,derived,(~p(s1,s1,s0,s1,s0,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[223964584,167669600]),[]). % % cnf(224443840,derived,(~p(s1,s1,s0,s1,s0,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[224212592,167663384]),[]). % % cnf(224672960,derived,(~p(s1,s1,s0,s1,s0,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[224443840,167679376]),[]). % % cnf(224919360,derived,(~p(s1,s1,s0,s1,s0,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[224672960,167663384]),[]). % % cnf(225153840,derived,(~p(s1,s1,s0,s1,s0,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[224919360,167669600]),[]). % % cnf(225380376,derived,(~p(s1,s1,s0,s1,s0,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[225153840,167663384]),[]). % % cnf(225639928,derived,(~p(s1,s1,s0,s0,s1,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[225380376,167706048]),[]). % % cnf(225862472,derived,(~p(s1,s1,s0,s0,s1,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[225639928,167663384]),[]). % % cnf(226095392,derived,(~p(s1,s1,s0,s0,s1,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[225862472,167669600]),[]). % % cnf(226341064,derived,(~p(s1,s1,s0,s0,s1,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[226095392,167663384]),[]). % % cnf(226582168,derived,(~p(s1,s1,s0,s0,s1,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[226341064,167679376]),[]). % % cnf(227098176,derived,(~p(s1,s1,s0,s0,s1,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[226582168,167663384]),[]). % % cnf(227332632,derived,(~p(s1,s1,s0,s0,s1,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[227098176,167669600]),[]). % % cnf(227559304,derived,(~p(s1,s1,s0,s0,s1,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[227332632,167663384]),[]). % % cnf(227811408,derived,(~p(s1,s1,s0,s0,s1,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[227559304,167685056]),[]). % % cnf(228041040,derived,(~p(s1,s1,s0,s0,s1,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[227811408,167663384]),[]). % % cnf(228279584,derived,(~p(s1,s1,s0,s0,s1,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[228041040,167669600]),[]). % % cnf(228510352,derived,(~p(s1,s1,s0,s0,s1,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[228279584,167663384]),[]). % % cnf(228764104,derived,(~p(s1,s1,s0,s0,s1,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[228510352,167679376]),[]). % % cnf(228985872,derived,(~p(s1,s1,s0,s0,s1,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[228764104,167663384]),[]). % % cnf(229222792,derived,(~p(s1,s1,s0,s0,s1,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[228985872,167669600]),[]). % % cnf(229468408,derived,(~p(s1,s1,s0,s0,s1,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[229222792,167663384]),[]). % % cnf(229714376,derived,(~p(s1,s1,s0,s0,s1,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[229468408,167694792]),[]). % % cnf(229943144,derived,(~p(s1,s1,s0,s0,s1,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[229714376,167663384]),[]). % % cnf(230181688,derived,(~p(s1,s1,s0,s0,s1,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[229943144,167669600]),[]). % % cnf(230408360,derived,(~p(s1,s1,s0,s0,s1,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[230181688,167663384]),[]). % % cnf(230658024,derived,(~p(s1,s1,s0,s0,s1,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[230408360,167679376]),[]). % % cnf(230879792,derived,(~p(s1,s1,s0,s0,s1,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[230658024,167663384]),[]). % % cnf(231116744,derived,(~p(s1,s1,s0,s0,s1,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[230879792,167669600]),[]). % % cnf(231362336,derived,(~p(s1,s1,s0,s0,s1,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[231116744,167663384]),[]). % % cnf(231605768,derived,(~p(s1,s1,s0,s0,s1,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[231362336,167685056]),[]). % % cnf(231827008,derived,(~p(s1,s1,s0,s0,s1,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[231605768,167663384]),[]). % % cnf(232063960,derived,(~p(s1,s1,s0,s0,s1,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[231827008,167669600]),[]). % % cnf(232309552,derived,(~p(s1,s1,s0,s0,s1,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[232063960,167663384]),[]). % % cnf(232534584,derived,(~p(s1,s1,s0,s0,s1,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[232309552,167679376]),[]). % % cnf(232781008,derived,(~p(s1,s1,s0,s0,s1,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[232534584,167663384]),[]). % % cnf(233019640,derived,(~p(s1,s1,s0,s0,s1,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[232781008,167669600]),[]). % % cnf(233246176,derived,(~p(s1,s1,s0,s0,s1,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[233019640,167663384]),[]). % % cnf(233503288,derived,(~p(s1,s1,s0,s0,s0,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[233246176,167700408]),[]). % % cnf(233735424,derived,(~p(s1,s1,s0,s0,s0,s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[233503288,167663384]),[]). % % cnf(233973968,derived,(~p(s1,s1,s0,s0,s0,s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[233735424,167669600]),[]). % % cnf(234209296,derived,(~p(s1,s1,s0,s0,s0,s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[233973968,167663384]),[]). % % cnf(234446216,derived,(~p(s1,s1,s0,s0,s0,s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[234209296,167679376]),[]). % % cnf(234672072,derived,(~p(s1,s1,s0,s0,s0,s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[234446216,167663384]),[]). % % cnf(234909024,derived,(~p(s1,s1,s0,s0,s0,s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[234672072,167669600]),[]). % % cnf(235150528,derived,(~p(s1,s1,s0,s0,s0,s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[234909024,167663384]),[]). % % cnf(235393968,derived,(~p(s1,s1,s0,s0,s0,s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[235150528,167685056]),[]). % % cnf(235619024,derived,(~p(s1,s1,s0,s0,s0,s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[235393968,167663384]),[]). % % cnf(235855976,derived,(~p(s1,s1,s0,s0,s0,s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[235619024,167669600]),[]). % % cnf(236097480,derived,(~p(s1,s1,s0,s0,s0,s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[235855976,167663384]),[]). % % cnf(236326600,derived,(~p(s1,s1,s0,s0,s0,s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[236097480,167679376]),[]). % % cnf(236573024,derived,(~p(s1,s1,s0,s0,s0,s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[236326600,167663384]),[]). % % cnf(236811592,derived,(~p(s1,s1,s0,s0,s0,s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[236573024,167669600]),[]). % % cnf(237038136,derived,(~p(s1,s1,s0,s0,s0,s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[236811592,167663384]),[]). % % cnf(237292808,derived,(~p(s1,s1,s0,s0,s0,s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[237038136,167694792]),[]). % % cnf(237517064,derived,(~p(s1,s1,s0,s0,s0,s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[237292808,167663384]),[]). % % cnf(237764280,derived,(~p(s1,s1,s0,s0,s0,s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[237517064,167669600]),[]). % % cnf(237986744,derived,(~p(s1,s1,s0,s0,s0,s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[237764280,167663384]),[]). % % cnf(238236544,derived,(~p(s1,s1,s0,s0,s0,s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[237986744,167679376]),[]). % % cnf(238462400,derived,(~p(s1,s1,s0,s0,s0,s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[238236544,167663384]),[]). % % cnf(238695264,derived,(~p(s1,s1,s0,s0,s0,s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[238462400,167669600]),[]). % % cnf(238936160,derived,(~p(s1,s1,s0,s0,s0,s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[238695264,167663384]),[]). % % cnf(239188408,derived,(~p(s1,s1,s0,s0,s0,s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[238936160,167685056]),[]). % % cnf(239413464,derived,(~p(s1,s1,s0,s0,s0,s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[239188408,167663384]),[]). % % cnf(239646328,derived,(~p(s1,s1,s0,s0,s0,s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[239413464,167669600]),[]). % % cnf(239883136,derived,(~p(s1,s1,s0,s0,s0,s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[239646328,167663384]),[]). % % cnf(240121048,derived,(~p(s1,s1,s0,s0,s0,s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[239883136,167679376]),[]). % % cnf(240358648,derived,(~p(s1,s1,s0,s0,s0,s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[240121048,167663384]),[]). % % cnf(240602056,derived,(~p(s1,s1,s0,s0,s0,s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[240358648,167669600]),[]). % % cnf(240837240,derived,(~p(s1,s1,s0,s0,s0,s0,s0,s0,s0,s0)),inference(resolution,[status(thm)],[240602056,167663384]),[]). % % cnf(241448168,derived,(~p(s1,s0,s1,s1,s1,s1,s1,s1,s1,s1)),inference(resolution,[status(thm)],[167721408,240837240]),[]). % % cnf(contradiction,derived,$false,inference(resolution,[status(thm)],[362058224,241448168]),[]). % % END OF PROOF SEQUENCE % %------------------------------------------------------------------------------