%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : PUZ054-10 : TPTP v8.1.0. Released v7.5.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n023.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Mon Jul 18 18:27:25 EDT 2022
% Result : Satisfiable 0.18s 0.46s
% Output : Saturation 0.18s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 483)
% Comments :
%------------------------------------------------------------------------------
cnf(792,plain,
equal(ifeq(p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[492,4]),
[iquote('0:SpR:492.0,4.0')] ).
cnf(73,plain,
equal(ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(s(n0))))),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[53,3]),
[iquote('0:SpR:53.0,3.0')] ).
cnf(802,plain,
equal(ifeq(p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[797,4]),
[iquote('0:SpR:797.0,4.0')] ).
cnf(85,plain,
equal(ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(n0)))),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[76,3]),
[iquote('0:SpR:76.0,3.0')] ).
cnf(487,plain,
equal(ifeq(p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[246,4]),
[iquote('0:SpR:246.0,4.0')] ).
cnf(97,plain,
equal(ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(n0))),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[88,3]),
[iquote('0:SpR:88.0,3.0')] ).
cnf(109,plain,
equal(ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(n0)),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[100,3]),
[iquote('0:SpR:100.0,3.0')] ).
cnf(122,plain,
equal(ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),n0),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[112,3]),
[iquote('0:SpR:112.0,3.0')] ).
cnf(797,plain,
equal(p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,788]),
[iquote('0:Rew:1.0,788.0')] ).
cnf(50,plain,
equal(ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(s(s(n0)))))),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[41,3]),
[iquote('0:SpR:41.0,3.0')] ).
cnf(492,plain,
equal(p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,483]),
[iquote('0:Rew:1.0,483.0')] ).
cnf(777,plain,
equal(p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,768]),
[iquote('0:Rew:1.0,768.0')] ).
cnf(757,plain,
equal(p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,748]),
[iquote('0:Rew:1.0,748.0')] ).
cnf(745,plain,
equal(p(n0,s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,736]),
[iquote('0:Rew:1.0,736.0')] ).
cnf(435,plain,
equal(p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,426]),
[iquote('0:Rew:1.0,426.0')] ).
cnf(731,plain,
equal(p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,722]),
[iquote('0:Rew:1.0,722.0')] ).
cnf(699,plain,
equal(p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(n0))))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,690]),
[iquote('0:Rew:1.0,690.0')] ).
cnf(713,plain,
equal(p(n0,s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,704]),
[iquote('0:Rew:1.0,704.0')] ).
cnf(687,plain,
equal(p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(n0))))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,678]),
[iquote('0:Rew:1.0,678.0')] ).
cnf(386,plain,
equal(p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0)))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,377]),
[iquote('0:Rew:1.0,377.0')] ).
cnf(673,plain,
equal(p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(n0)))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,664]),
[iquote('0:Rew:1.0,664.0')] ).
cnf(641,plain,
equal(p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(n0))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,632]),
[iquote('0:Rew:1.0,632.0')] ).
cnf(653,plain,
equal(p(n0,s(s(s(s(s(s(s(s(s(s(n0))))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,646]),
[iquote('0:Rew:1.0,646.0')] ).
cnf(629,plain,
equal(p(s(s(n0)),s(s(s(s(s(s(s(s(s(n0)))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,620]),
[iquote('0:Rew:1.0,620.0')] ).
cnf(55,plain,
equal(p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(n0)))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,46]),
[iquote('0:Rew:1.0,46.0')] ).
cnf(617,plain,
equal(p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(n0))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,608]),
[iquote('0:Rew:1.0,608.0')] ).
cnf(603,plain,
equal(p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0)))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,594]),
[iquote('0:Rew:1.0,594.0')] ).
cnf(78,plain,
equal(p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(n0))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,69]),
[iquote('0:Rew:1.0,69.0')] ).
cnf(582,plain,
equal(p(n0,s(s(s(s(s(s(s(s(s(n0)))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,575]),
[iquote('0:Rew:1.0,575.0')] ).
cnf(241,plain,
equal(ifeq(p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[67,4]),
[iquote('0:SpR:67.0,4.0')] ).
cnf(570,plain,
equal(p(s(s(n0)),s(s(s(s(s(s(s(s(n0))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,563]),
[iquote('0:Rew:1.0,563.0')] ).
cnf(560,plain,
equal(p(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0)))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,551]),
[iquote('0:Rew:1.0,551.0')] ).
cnf(546,plain,
equal(p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(n0))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,537]),
[iquote('0:Rew:1.0,537.0')] ).
cnf(90,plain,
equal(p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(n0)))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,81]),
[iquote('0:Rew:1.0,81.0')] ).
cnf(38,plain,
equal(ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(s(s(s(n0))))))),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[29,3]),
[iquote('0:SpR:29.0,3.0')] ).
cnf(525,plain,
equal(p(n0,s(s(s(s(s(s(s(s(n0))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,518]),
[iquote('0:Rew:1.0,518.0')] ).
cnf(513,plain,
equal(p(s(s(n0)),s(s(s(s(s(s(s(n0)))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,506]),
[iquote('0:Rew:1.0,506.0')] ).
cnf(501,plain,
equal(p(s(s(s(s(n0)))),s(s(s(s(s(s(n0))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,494]),
[iquote('0:Rew:1.0,494.0')] ).
cnf(478,plain,
equal(p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(n0)))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,469]),
[iquote('0:Rew:1.0,469.0')] ).
cnf(246,plain,
equal(p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,237]),
[iquote('0:Rew:1.0,237.0')] ).
cnf(102,plain,
equal(p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(n0))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,93]),
[iquote('0:Rew:1.0,93.0')] ).
cnf(458,plain,
equal(p(n0,s(s(s(s(s(s(s(n0)))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,451]),
[iquote('0:Rew:1.0,451.0')] ).
cnf(446,plain,
equal(p(s(s(n0)),s(s(s(s(s(s(n0))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,439]),
[iquote('0:Rew:1.0,439.0')] ).
cnf(421,plain,
equal(p(s(s(s(s(n0)))),s(s(s(s(s(n0)))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,414]),
[iquote('0:Rew:1.0,414.0')] ).
cnf(203,plain,
equal(p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(n0))))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,194]),
[iquote('0:Rew:1.0,194.0')] ).
cnf(407,plain,
equal(p(s(s(s(s(s(s(n0)))))),s(s(s(s(n0))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,400]),
[iquote('0:Rew:1.0,400.0')] ).
cnf(114,plain,
equal(p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(n0)))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,105]),
[iquote('0:Rew:1.0,105.0')] ).
cnf(125,plain,
equal(p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),n0),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,120]),
[iquote('0:Rew:1.0,120.0')] ).
cnf(372,plain,
equal(p(s(s(s(s(s(s(s(s(n0)))))))),n0),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,367]),
[iquote('0:Rew:1.0,367.0')] ).
cnf(43,plain,
equal(p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(n0))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,34]),
[iquote('0:Rew:1.0,34.0')] ).
cnf(136,plain,
equal(p(s(s(s(s(s(s(s(s(n0)))))))),s(n0)),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,130]),
[iquote('0:Rew:1.0,130.0')] ).
cnf(356,plain,
equal(p(s(s(s(s(s(s(n0)))))),n0),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,351]),
[iquote('0:Rew:1.0,351.0')] ).
cnf(343,plain,
equal(p(s(s(s(s(s(s(n0)))))),s(n0)),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,337]),
[iquote('0:Rew:1.0,337.0')] ).
cnf(149,plain,
equal(p(s(s(s(s(s(s(n0)))))),s(s(n0))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,143]),
[iquote('0:Rew:1.0,143.0')] ).
cnf(63,plain,
equal(ifeq(p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[21,4]),
[iquote('0:SpR:21.0,4.0')] ).
cnf(325,plain,
equal(p(s(s(s(s(n0)))),n0),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,320]),
[iquote('0:Rew:1.0,320.0')] ).
cnf(313,plain,
equal(p(s(s(s(s(n0)))),s(n0)),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,307]),
[iquote('0:Rew:1.0,307.0')] ).
cnf(299,plain,
equal(p(s(s(s(s(n0)))),s(s(n0))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,293]),
[iquote('0:Rew:1.0,293.0')] ).
cnf(160,plain,
equal(p(s(s(s(s(n0)))),s(s(s(n0)))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,154]),
[iquote('0:Rew:1.0,154.0')] ).
cnf(26,plain,
equal(ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(s(s(s(s(n0)))))))),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[19,3]),
[iquote('0:SpR:19.0,3.0')] ).
cnf(281,plain,
equal(p(s(s(n0)),n0),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,276]),
[iquote('0:Rew:1.0,276.0')] ).
cnf(269,plain,
equal(p(s(s(n0)),s(n0)),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,263]),
[iquote('0:Rew:1.0,263.0')] ).
cnf(256,plain,
equal(p(s(s(n0)),s(s(n0))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,250]),
[iquote('0:Rew:1.0,250.0')] ).
cnf(231,plain,
equal(p(s(s(n0)),s(s(s(n0)))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,225]),
[iquote('0:Rew:1.0,225.0')] ).
cnf(67,plain,
equal(p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,58]),
[iquote('0:Rew:1.0,58.0')] ).
cnf(172,plain,
equal(p(s(s(n0)),s(s(s(s(n0))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,166]),
[iquote('0:Rew:1.0,166.0')] ).
cnf(217,plain,
equal(p(n0,s(n0)),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,215]),
[iquote('0:Rew:1.0,215.0')] ).
cnf(211,plain,
equal(p(n0,s(s(n0))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,209]),
[iquote('0:Rew:1.0,209.0')] ).
cnf(192,plain,
equal(p(n0,s(s(s(n0)))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,190]),
[iquote('0:Rew:1.0,190.0')] ).
cnf(31,plain,
equal(p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(s(n0)))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,22]),
[iquote('0:Rew:1.0,22.0')] ).
cnf(185,plain,
equal(p(n0,s(s(s(s(n0))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,183]),
[iquote('0:Rew:1.0,183.0')] ).
cnf(179,plain,
equal(p(n0,s(s(s(s(s(n0)))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,177]),
[iquote('0:Rew:1.0,177.0')] ).
cnf(171,plain,
equal(p(n0,s(s(s(s(s(s(n0))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,164]),
[iquote('0:Rew:1.0,164.0')] ).
cnf(159,plain,
equal(p(s(s(n0)),s(s(s(s(s(n0)))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,152]),
[iquote('0:Rew:1.0,152.0')] ).
cnf(16,plain,
equal(ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(s(s(s(s(s(n0))))))))),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[2,3]),
[iquote('0:SpR:2.0,3.0')] ).
cnf(148,plain,
equal(p(s(s(s(s(n0)))),s(s(s(s(n0))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,141]),
[iquote('0:Rew:1.0,141.0')] ).
cnf(135,plain,
equal(p(s(s(s(s(s(s(n0)))))),s(s(s(n0)))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,128]),
[iquote('0:Rew:1.0,128.0')] ).
cnf(124,plain,
equal(p(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,118]),
[iquote('0:Rew:1.0,118.0')] ).
cnf(112,plain,
equal(p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(n0)),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,111]),
[iquote('0:Rew:1.0,111.0')] ).
cnf(17,plain,
equal(ifeq(p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(s(n0))))))))))),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[2,4]),
[iquote('0:SpR:2.0,4.0')] ).
cnf(100,plain,
equal(p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(n0))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,99]),
[iquote('0:Rew:1.0,99.0')] ).
cnf(88,plain,
equal(p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(n0)))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,87]),
[iquote('0:Rew:1.0,87.0')] ).
cnf(76,plain,
equal(p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(n0))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,75]),
[iquote('0:Rew:1.0,75.0')] ).
cnf(53,plain,
equal(p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(n0)))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,52]),
[iquote('0:Rew:1.0,52.0')] ).
cnf(21,plain,
equal(p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(s(s(n0))))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,12]),
[iquote('0:Rew:1.0,12.0')] ).
cnf(41,plain,
equal(p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(n0))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,40]),
[iquote('0:Rew:1.0,40.0')] ).
cnf(29,plain,
equal(p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0)))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,28]),
[iquote('0:Rew:1.0,28.0')] ).
cnf(19,plain,
equal(p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(n0))))))))),true__dfg),
inference(rew,[status(thm),theory(equality)],[1,18]),
[iquote('0:Rew:1.0,18.0')] ).
cnf(2,axiom,
equal(p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(n0)))))))))),true__dfg),
file('PUZ054-10.p',unknown),
[] ).
cnf(4,axiom,
equal(ifeq(p(u,s(s(v))),true__dfg,p(u,s(v)),true__dfg),true__dfg),
file('PUZ054-10.p',unknown),
[] ).
cnf(5,axiom,
equal(ifeq(p(s(u),s(v)),true__dfg,p(s(u),v),true__dfg),true__dfg),
file('PUZ054-10.p',unknown),
[] ).
cnf(3,axiom,
equal(ifeq(p(s(s(u)),v),true__dfg,p(u,s(v)),true__dfg),true__dfg),
file('PUZ054-10.p',unknown),
[] ).
cnf(1,axiom,
equal(ifeq(u,u,v,w),v),
file('PUZ054-10.p',unknown),
[] ).
cnf(6,axiom,
~ equal(p(s(n0),n0),true__dfg),
file('PUZ054-10.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : PUZ054-10 : TPTP v8.1.0. Released v7.5.0.
% 0.11/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n023.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Sun May 29 03:02:27 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.18/0.46
% 0.18/0.46 SPASS V 3.9
% 0.18/0.46 SPASS beiseite: Completion found.
% 0.18/0.46 % SZS status CounterSatisfiable
% 0.18/0.46 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.46 SPASS derived 506 clauses, backtracked 0 clauses, performed 0 splits and kept 130 clauses.
% 0.18/0.46 SPASS allocated 63590 KBytes.
% 0.18/0.46 SPASS spent 0:00:00.13 on the problem.
% 0.18/0.46 0:00:00.04 for the input.
% 0.18/0.46 0:00:00.00 for the FLOTTER CNF translation.
% 0.18/0.46 0:00:00.01 for inferences.
% 0.18/0.46 0:00:00.00 for the backtracking.
% 0.18/0.46 0:00:00.05 for the reduction.
% 0.18/0.46
% 0.18/0.46
% 0.18/0.46 The saturated set of worked-off clauses is :
% 0.18/0.46 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------