%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT076-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:55:09 PM UTC 2026
% Result : Unsatisfiable 87.42s 13.19s
% Output : CNFRefutation 87.42s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
f(f(f(f(X1,X2),f(X3,X2)),X4),f(X2,f(f(f(f(f(f(X1,X1),X2),X3),X3),X2),X1))) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t1,plain,
f(f(f(f(X1,X2),f(X3,X2)),X4),f(X2,f(f(f(f(f(f(X1,X1),X2),X3),X3),X2),X1))) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t2,plain,
f(X1,X2) = f(X2,f(f(X1,X2),f(f(f(f(f(f(f(X3,X2),f(X3,X2)),f(X1,X2)),X4),X4),f(X1,X2)),f(X3,X2)))),
inference(cp,[status(thm)],[t1,t1]) ).
cnf(t9,plain,
f(X1,f(f(X2,X1),f(f(f(f(f(f(f(X3,X1),f(X3,X1)),f(X2,X1)),X4),X4),f(X2,X1)),f(X3,X1)))) = f(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t17,plain,
X1 = f(f(X2,f(f(X3,X1),f(X4,X1))),f(X1,f(f(f(f(f(f(X3,X3),X1),X4),X4),X1),X3))),
inference(cp,[status(thm)],[t1,t9]) ).
cnf(t29,plain,
f(f(X1,f(f(X2,X3),f(X4,X3))),f(X3,f(f(f(f(f(f(X2,X2),X3),X4),X4),X3),X2))) = X3,
inference(orient,[status(thm)],[t17]) ).
cnf(t41,plain,
f(X1,X2) = f(X2,f(f(X1,X2),f(f(f(f(f(f(X3,X3),f(X1,X2)),f(X4,X2)),f(X4,X2)),f(X1,X2)),X3))),
inference(cp,[status(thm)],[t1,t29]) ).
cnf(t63,plain,
f(X1,f(f(X2,X1),f(f(f(f(f(f(X3,X3),f(X2,X1)),f(X4,X1)),f(X4,X1)),f(X2,X1)),X3))) = f(X2,X1),
inference(orient,[status(thm)],[t41]) ).
cnf(t67,plain,
f(f(X1,X2),f(X3,X2)) = f(f(X3,X2),f(f(f(X1,X2),f(X3,X2)),X2)),
inference(cp,[status(thm)],[t63,t29]) ).
cnf(t106,plain,
f(f(X1,X2),f(f(f(X3,X2),f(X1,X2)),X2)) = f(f(X3,X2),f(X1,X2)),
inference(orient,[status(thm)],[t67]) ).
cnf(t127,plain,
f(X1,X2) = f(f(f(f(X2,f(X1,X2)),f(X2,f(X1,X2))),X3),f(f(f(f(f(X2,X2),f(X1,X2)),X2),X2),f(X1,X2))),
inference(cp,[status(thm)],[t1,t106]) ).
cnf(t204,plain,
f(f(f(f(X1,f(X2,X1)),f(X1,f(X2,X1))),X3),f(f(f(f(f(X1,X1),f(X2,X1)),X1),X1),f(X2,X1))) = f(X2,X1),
inference(orient,[status(thm)],[t127]) ).
cnf(t260,plain,
X1 = f(f(X2,X1),f(X1,f(f(f(f(f(f(f(f(f(X1,X1),f(X2,X1)),X1),f(f(f(X1,X1),f(X2,X1)),X1)),X1),X2),X2),X1),f(f(f(X1,X1),f(X2,X1)),X1)))),
inference(cp,[status(thm)],[t29,t204]) ).
cnf(t121,plain,
f(f(X1,X2),f(f(f(X3,X2),f(X1,X2)),X2)) = f(f(f(f(X3,X2),f(X1,X2)),X2),f(f(f(X3,X2),f(X1,X2)),X2)),
inference(cp,[status(thm)],[t106,t106]) ).
cnf(t224909,plain,
f(f(X3,X2),f(X1,X2)) = f(f(f(f(X3,X2),f(X1,X2)),X2),f(f(f(X3,X2),f(X1,X2)),X2)),
inference(step,[status(thm)],[t121,t106]) ).
cnf(t149,plain,
f(f(f(f(X1,X2),f(X3,X2)),X2),f(f(f(X1,X2),f(X3,X2)),X2)) = f(f(X1,X2),f(X3,X2)),
inference(orient,[status(thm)],[t224909]) ).
cnf(t224910,plain,
X1 = f(f(X2,X1),f(X1,f(f(f(f(f(f(f(X1,X1),f(X2,X1)),X1),X2),X2),X1),f(f(f(X1,X1),f(X2,X1)),X1)))),
inference(step,[status(thm)],[t260,t149]) ).
cnf(t346,plain,
f(f(X1,X2),f(X2,f(f(f(f(f(f(f(X2,X2),f(X1,X2)),X2),X1),X1),X2),f(f(f(X2,X2),f(X1,X2)),X2)))) = X2,
inference(orient,[status(thm)],[t224910]) ).
cnf(t395,plain,
X1 = f(f(X2,X1),f(X1,f(f(f(f(f(f(X3,X3),X1),X2),X2),X1),X3))),
inference(cp,[status(thm)],[t1,t346]) ).
cnf(t420,plain,
f(f(X1,X2),f(X2,f(f(f(f(f(f(X3,X3),X2),X1),X1),X2),X3))) = X2,
inference(orient,[status(thm)],[t395]) ).
cnf(t431,plain,
f(f(X1,X2),f(X3,X2)) = f(f(X4,f(f(X1,X2),f(X3,X2))),f(f(f(X1,X2),f(X3,X2)),X2)),
inference(cp,[status(thm)],[t420,t29]) ).
cnf(t498,plain,
f(f(X1,f(f(X2,X3),f(X4,X3))),f(f(f(X2,X3),f(X4,X3)),X3)) = f(f(X2,X3),f(X4,X3)),
inference(orient,[status(thm)],[t431]) ).
cnf(t386,plain,
f(X1,X2) = f(f(X2,f(X1,X2)),f(f(f(f(f(X2,X2),f(X1,X2)),X2),X2),f(X1,X2))),
inference(cp,[status(thm)],[t204,t346]) ).
cnf(t720,plain,
f(f(X1,f(X2,X1)),f(f(f(f(f(X1,X1),f(X2,X1)),X1),X1),f(X2,X1))) = f(X2,X1),
inference(orient,[status(thm)],[t386]) ).
cnf(t760,plain,
f(f(X1,f(X2,X1)),f(f(f(f(f(X1,X1),f(X2,X1)),X1),X1),f(X2,X1))) = f(f(f(f(f(f(X1,X1),f(X2,X1)),X1),X1),f(X2,X1)),f(f(X2,X1),f(X2,X1))),
inference(cp,[status(thm)],[t106,t720]) ).
cnf(t224911,plain,
f(X2,X1) = f(f(f(f(f(f(X1,X1),f(X2,X1)),X1),X1),f(X2,X1)),f(f(X2,X1),f(X2,X1))),
inference(step,[status(thm)],[t760,t720]) ).
cnf(t817,plain,
f(f(f(f(f(f(X1,X1),f(X2,X1)),X1),X1),f(X2,X1)),f(f(X2,X1),f(X2,X1))) = f(X2,X1),
inference(orient,[status(thm)],[t224911]) ).
cnf(t874,plain,
f(f(f(f(f(f(X1,X1),f(X2,X1)),X1),X1),f(X2,X1)),f(f(X2,X1),f(X2,X1))) = f(f(f(X2,X1),f(X2,X1)),f(f(X2,X1),f(X2,X1))),
inference(cp,[status(thm)],[t106,t817]) ).
cnf(t224912,plain,
f(X2,X1) = f(f(f(X2,X1),f(X2,X1)),f(f(X2,X1),f(X2,X1))),
inference(step,[status(thm)],[t874,t817]) ).
cnf(t932,plain,
f(f(f(X1,X2),f(X1,X2)),f(f(X1,X2),f(X1,X2))) = f(X1,X2),
inference(orient,[status(thm)],[t224912]) ).
cnf(t1003,plain,
f(f(f(X1,X2),f(X1,X2)),f(f(X1,X2),f(X1,X2))) = f(f(X3,f(X1,X2)),f(f(f(f(X1,X2),f(X1,X2)),f(f(X1,X2),f(X1,X2))),f(X1,X2))),
inference(cp,[status(thm)],[t498,t932]) ).
cnf(t224913,plain,
f(X1,X2) = f(f(X3,f(X1,X2)),f(f(f(f(X1,X2),f(X1,X2)),f(f(X1,X2),f(X1,X2))),f(X1,X2))),
inference(step,[status(thm)],[t1003,t932]) ).
cnf(t224914,plain,
f(X1,X2) = f(f(X3,f(X1,X2)),f(f(X1,X2),f(X1,X2))),
inference(step,[status(thm)],[t224913,t932]) ).
cnf(t1074,plain,
f(f(X1,f(X2,X3)),f(f(X2,X3),f(X2,X3))) = f(X2,X3),
inference(orient,[status(thm)],[t224914]) ).
cnf(t1179,plain,
f(X1,X2) = f(X2,f(f(X1,X2),f(X1,X2))),
inference(cp,[status(thm)],[t63,t1074]) ).
cnf(t1212,plain,
f(X1,f(f(X2,X1),f(X2,X1))) = f(X2,X1),
inference(orient,[status(thm)],[t1179]) ).
cnf(t1213,plain,
f(f(f(X1,X2),f(X3,X2)),X2) = f(X2,f(f(X1,X2),f(X3,X2))),
inference(cp,[status(thm)],[t1212,t149]) ).
cnf(t1287,plain,
f(f(f(X1,X2),f(X3,X2)),X2) = f(X2,f(f(X1,X2),f(X3,X2))),
inference(orient,[status(thm)],[t1213]) ).
cnf(t224915,plain,
f(f(X1,X2),f(X2,f(f(X3,X2),f(X1,X2)))) = f(f(X3,X2),f(X1,X2)),
inference(step,[status(thm)],[t106,t1287]) ).
cnf(t1334,plain,
f(f(X1,X2),f(X2,f(f(X3,X2),f(X1,X2)))) = f(f(X3,X2),f(X1,X2)),
inference(rw,[status(thm)],[t224915]) ).
cnf(t1399,plain,
f(f(X1,X2),f(X2,f(f(X3,X2),f(X1,X2)))) = f(f(X3,X2),f(X1,X2)),
inference(orient,[status(thm)],[t1334]) ).
cnf(t35289,plain,
f(f(X1,X2),f(X2,f(f(X3,X2),f(X1,X2)))) = f(f(X3,X2),f(X1,X2)),
inference(rw,[status(thm)],[t1399]) ).
cnf(t1400,plain,
f(f(f(f(f(f(f(X1,X2),f(X1,X2)),X2),X1),X1),X2),f(X1,X2)) = X2,
inference(cp,[status(thm)],[t1399,t420]) ).
cnf(t224924,plain,
f(f(f(f(f(X2,f(f(X1,X2),f(X1,X2))),X1),X1),X2),f(X1,X2)) = X2,
inference(step,[status(thm)],[t1400,t1287]) ).
cnf(t224925,plain,
f(f(f(f(f(X1,X2),X1),X1),X2),f(X1,X2)) = X2,
inference(step,[status(thm)],[t224924,t1212]) ).
cnf(t1464,plain,
f(f(f(f(f(X1,X2),X1),X1),X2),f(X1,X2)) = X2,
inference(orient,[status(thm)],[t224925]) ).
cnf(t1485,plain,
f(f(f(f(f(X1,X2),X1),X1),X2),f(X1,X2)) = f(f(X3,X2),f(f(f(f(f(f(X1,X2),X1),X1),X2),f(X1,X2)),f(f(f(f(f(X1,X2),X1),X1),X2),f(X1,X2)))),
inference(cp,[status(thm)],[t1074,t1464]) ).
cnf(t224926,plain,
X2 = f(f(X3,X2),f(f(f(f(f(f(X1,X2),X1),X1),X2),f(X1,X2)),f(f(f(f(f(X1,X2),X1),X1),X2),f(X1,X2)))),
inference(step,[status(thm)],[t1485,t1464]) ).
cnf(t224927,plain,
X2 = f(f(X3,X2),f(X2,f(f(f(f(f(X1,X2),X1),X1),X2),f(X1,X2)))),
inference(step,[status(thm)],[t224926,t1464]) ).
cnf(t224928,plain,
X2 = f(f(X3,X2),f(X2,X2)),
inference(step,[status(thm)],[t224927,t1464]) ).
cnf(t1516,plain,
f(f(X1,X2),f(X2,X2)) = X2,
inference(orient,[status(thm)],[t224928]) ).
cnf(t1523,plain,
f(X1,X1) = f(f(X2,f(X1,X1)),X1),
inference(cp,[status(thm)],[t1516,t1516]) ).
cnf(t1572,plain,
f(f(X1,f(X2,X2)),X2) = f(X2,X2),
inference(orient,[status(thm)],[t1523]) ).
cnf(t1575,plain,
X1 = f(f(X1,X1),f(f(X1,X1),X1)),
inference(cp,[status(thm)],[t1464,t1572]) ).
cnf(t1630,plain,
f(f(X1,X1),f(f(X1,X1),X1)) = X1,
inference(orient,[status(thm)],[t1575]) ).
cnf(t1638,plain,
X1 = f(f(X1,X2),f(X1,f(f(f(f(f(f(X1,X1),X1),f(X1,X1)),f(X1,X1)),X1),X1))),
inference(cp,[status(thm)],[t1,t1630]) ).
cnf(t224929,plain,
X1 = f(f(X1,X2),f(X1,f(f(X1,X1),X1))),
inference(step,[status(thm)],[t1638,t1572]) ).
cnf(t1661,plain,
f(f(X1,X2),f(X1,f(f(X1,X1),X1))) = X1,
inference(orient,[status(thm)],[t224929]) ).
cnf(t1675,plain,
f(X1,f(f(X1,X1),X1)) = f(X1,f(f(X1,f(f(X1,X1),X1)),f(X1,f(f(X1,X1),X1)))),
inference(cp,[status(thm)],[t1516,t1661]) ).
cnf(t224930,plain,
f(X1,f(f(X1,X1),X1)) = f(X1,X1),
inference(step,[status(thm)],[t1675,t1661]) ).
cnf(t1731,plain,
f(X1,f(f(X1,X1),X1)) = f(X1,X1),
inference(orient,[status(thm)],[t224930]) ).
cnf(t224931,plain,
f(f(X1,X2),f(X1,X1)) = X1,
inference(step,[status(thm)],[t1661,t1731]) ).
cnf(t1767,plain,
f(f(X1,X2),f(X1,X1)) = X1,
inference(rw,[status(thm)],[t224931]) ).
cnf(t1768,plain,
f(f(X1,X2),f(X1,X1)) = X1,
inference(orient,[status(thm)],[t1767]) ).
cnf(t1771,plain,
f(X1,X1) = f(f(f(X1,X1),X2),X1),
inference(cp,[status(thm)],[t1768,t1516]) ).
cnf(t1823,plain,
f(f(f(X1,X1),X2),X1) = f(X1,X1),
inference(orient,[status(thm)],[t1771]) ).
cnf(t1824,plain,
f(X1,X1) = f(X1,f(f(X1,X1),f(X2,X1))),
inference(cp,[status(thm)],[t1823,t1287]) ).
cnf(t1948,plain,
f(X1,f(f(X1,X1),f(X2,X1))) = f(X1,X1),
inference(orient,[status(thm)],[t1824]) ).
cnf(t1963,plain,
f(f(X1,X1),f(X2,X1)) = f(f(X2,X1),f(X1,X1)),
inference(cp,[status(thm)],[t1399,t1948]) ).
cnf(t224939,plain,
f(f(X1,X1),f(X2,X1)) = X1,
inference(step,[status(thm)],[t1963,t1516]) ).
cnf(t1993,plain,
f(f(X1,X1),f(X2,X1)) = X1,
inference(orient,[status(thm)],[t224939]) ).
cnf(t3,plain,
f(f(f(f(f(f(X1,X1),X2),X3),X3),X2),X1) = f(f(X2,X4),f(f(f(f(f(f(f(X1,X1),X2),X3),X3),X2),X1),f(f(f(f(f(f(f(f(X1,X2),f(X3,X2)),f(f(X1,X2),f(X3,X2))),f(f(f(f(f(f(X1,X1),X2),X3),X3),X2),X1)),X2),X2),f(f(f(f(f(f(X1,X1),X2),X3),X3),X2),X1)),f(f(X1,X2),f(X3,X2))))),
inference(cp,[status(thm)],[t1,t1]) ).
cnf(t2796,plain,
f(f(X1,X2),f(f(f(f(f(f(f(X3,X3),X1),X4),X4),X1),X3),f(f(f(f(f(f(f(f(X3,X1),f(X4,X1)),f(f(X3,X1),f(X4,X1))),f(f(f(f(f(f(X3,X3),X1),X4),X4),X1),X3)),X1),X1),f(f(f(f(f(f(X3,X3),X1),X4),X4),X1),X3)),f(f(X3,X1),f(X4,X1))))) = f(f(f(f(f(f(X3,X3),X1),X4),X4),X1),X3),
inference(orient,[status(thm)],[t3]) ).
cnf(t3289,plain,
f(X1,X1) = f(f(f(f(f(f(f(X2,X2),X1),X3),X3),X1),X2),X1),
inference(cp,[status(thm)],[t1823,t2796]) ).
cnf(t4547,plain,
f(f(f(f(f(f(f(X1,X1),X2),X3),X3),X2),X1),X2) = f(X2,X2),
inference(orient,[status(thm)],[t3289]) ).
cnf(t4562,plain,
f(X1,X1) = f(f(f(f(f(X2,X2),X2),X1),X2),X1),
inference(cp,[status(thm)],[t4547,t1823]) ).
cnf(t1732,plain,
f(f(X1,X1),f(X1,X1)) = f(f(X1,X1),f(X1,f(X1,X1))),
inference(cp,[status(thm)],[t1731,t1516]) ).
cnf(t224935,plain,
X1 = f(f(X1,X1),f(X1,f(X1,X1))),
inference(step,[status(thm)],[t1732,t1516]) ).
cnf(t1847,plain,
f(f(X1,X1),f(X1,f(X1,X1))) = X1,
inference(orient,[status(thm)],[t224935]) ).
cnf(t1854,plain,
f(X1,f(X1,X1)) = f(f(f(f(X1,f(X1,X1)),f(X1,X1)),f(X1,f(X1,X1))),f(f(X1,X1),f(X1,f(X1,X1)))),
inference(cp,[status(thm)],[t1464,t1847]) ).
cnf(t224936,plain,
f(X1,f(X1,X1)) = f(f(X1,f(X1,f(X1,X1))),f(f(X1,X1),f(X1,f(X1,X1)))),
inference(step,[status(thm)],[t1854,t1768]) ).
cnf(t1532,plain,
f(X1,X1) = f(X1,f(X1,f(X1,X1))),
inference(cp,[status(thm)],[t1464,t1516]) ).
cnf(t1597,plain,
f(X1,f(X1,f(X1,X1))) = f(X1,X1),
inference(orient,[status(thm)],[t1532]) ).
cnf(t224937,plain,
f(X1,f(X1,X1)) = f(f(X1,X1),f(f(X1,X1),f(X1,f(X1,X1)))),
inference(step,[status(thm)],[t224936,t1597]) ).
cnf(t224938,plain,
f(X1,f(X1,X1)) = f(f(X1,X1),X1),
inference(step,[status(thm)],[t224937,t1847]) ).
cnf(t1878,plain,
f(f(X1,X1),X1) = f(X1,f(X1,X1)),
inference(orient,[status(thm)],[t224938]) ).
cnf(t224962,plain,
f(X1,X1) = f(f(f(f(X2,f(X2,X2)),X1),X2),X1),
inference(step,[status(thm)],[t4562,t1878]) ).
cnf(t4724,plain,
f(f(f(f(X1,f(X1,X1)),X2),X1),X2) = f(X2,X2),
inference(orient,[status(thm)],[t224962]) ).
cnf(t1584,plain,
X1 = f(f(f(X1,X1),X1),f(X1,f(f(X1,X1),X2))),
inference(cp,[status(thm)],[t420,t1572]) ).
cnf(t224945,plain,
X1 = f(f(X1,f(X1,X1)),f(X1,f(f(X1,X1),X2))),
inference(step,[status(thm)],[t1584,t1878]) ).
cnf(t2289,plain,
f(f(X1,f(X1,X1)),f(X1,f(f(X1,X1),X2))) = X1,
inference(orient,[status(thm)],[t224945]) ).
cnf(t4732,plain,
f(f(X1,f(f(X1,X1),X2)),f(X1,f(f(X1,X1),X2))) = f(f(X1,X1),f(X1,f(f(X1,X1),X2))),
inference(cp,[status(thm)],[t4724,t2289]) ).
cnf(t2009,plain,
f(X1,X2) = f(f(f(f(X2,f(X2,X2)),f(X2,X2)),f(X1,X2)),f(f(X2,X2),f(X1,X2))),
inference(cp,[status(thm)],[t1464,t1993]) ).
cnf(t224940,plain,
f(X1,X2) = f(f(X2,f(X1,X2)),f(f(X2,X2),f(X1,X2))),
inference(step,[status(thm)],[t2009,t1768]) ).
cnf(t224941,plain,
f(X1,X2) = f(f(X2,f(X1,X2)),X2),
inference(step,[status(thm)],[t224940,t1993]) ).
cnf(t2076,plain,
f(f(X1,f(X2,X1)),X1) = f(X2,X1),
inference(orient,[status(thm)],[t224941]) ).
cnf(t2080,plain,
f(f(X1,X1),f(X2,X1)) = f(f(f(X2,X1),X1),f(X2,X1)),
inference(cp,[status(thm)],[t2076,t1993]) ).
cnf(t224942,plain,
X1 = f(f(f(X2,X1),X1),f(X2,X1)),
inference(step,[status(thm)],[t2080,t1993]) ).
cnf(t2098,plain,
f(f(f(X1,X2),X2),f(X1,X2)) = X2,
inference(orient,[status(thm)],[t224942]) ).
cnf(t2304,plain,
f(X1,f(f(X1,X1),X2)) = f(f(X1,f(X1,f(f(X1,X1),X2))),f(f(X1,f(X1,X1)),f(X1,f(f(X1,X1),X2)))),
inference(cp,[status(thm)],[t2098,t2289]) ).
cnf(t224947,plain,
f(X1,f(f(X1,X1),X2)) = f(f(X1,f(X1,f(f(X1,X1),X2))),X1),
inference(step,[status(thm)],[t2304,t2289]) ).
cnf(t2454,plain,
f(f(X1,f(X1,f(f(X1,X1),X2))),X1) = f(X1,f(f(X1,X1),X2)),
inference(orient,[status(thm)],[t224947]) ).
cnf(t2462,plain,
X1 = f(f(X1,X1),f(X1,f(f(X1,X1),X2))),
inference(cp,[status(thm)],[t1993,t2454]) ).
cnf(t2549,plain,
f(f(X1,X1),f(X1,f(f(X1,X1),X2))) = X1,
inference(orient,[status(thm)],[t2462]) ).
cnf(t224970,plain,
f(f(X1,f(f(X1,X1),X2)),f(X1,f(f(X1,X1),X2))) = X1,
inference(step,[status(thm)],[t4732,t2549]) ).
cnf(t5080,plain,
f(f(X1,f(f(X1,X1),X2)),f(X1,f(f(X1,X1),X2))) = X1,
inference(orient,[status(thm)],[t224970]) ).
cnf(t5107,plain,
f(X1,f(f(X1,X1),X2)) = f(f(f(X1,f(f(X1,X1),X2)),f(X1,f(f(X1,X1),X2))),X1),
inference(cp,[status(thm)],[t1993,t5080]) ).
cnf(t224971,plain,
f(X1,f(f(X1,X1),X2)) = f(X1,X1),
inference(step,[status(thm)],[t5107,t5080]) ).
cnf(t5232,plain,
f(X1,f(f(X1,X1),X2)) = f(X1,X1),
inference(orient,[status(thm)],[t224971]) ).
cnf(t5240,plain,
f(f(X1,X1),f(X1,X1)) = f(f(X1,X1),f(X1,X2)),
inference(cp,[status(thm)],[t5232,t1993]) ).
cnf(t224972,plain,
X1 = f(f(X1,X1),f(X1,X2)),
inference(step,[status(thm)],[t5240,t1516]) ).
cnf(t5330,plain,
f(f(X1,X1),f(X1,X2)) = X1,
inference(orient,[status(thm)],[t224972]) ).
cnf(t5355,plain,
f(f(X1,f(X2,X3)),f(f(X2,X2),f(X2,X3))) = f(X2,f(f(X2,X3),f(f(X1,f(X2,X3)),f(f(X2,X2),f(X2,X3))))),
inference(cp,[status(thm)],[t1399,t5330]) ).
cnf(t225165,plain,
f(f(X1,f(X2,X3)),X2) = f(X2,f(f(X2,X3),f(f(X1,f(X2,X3)),f(f(X2,X2),f(X2,X3))))),
inference(step,[status(thm)],[t5355,t5330]) ).
cnf(t225166,plain,
f(f(X1,f(X2,X3)),X2) = f(X2,f(f(X2,X3),f(f(X1,f(X2,X3)),X2))),
inference(step,[status(thm)],[t225165,t5330]) ).
cnf(t33580,plain,
f(X1,f(f(X1,X2),f(f(X3,f(X1,X2)),X1))) = f(f(X3,f(X1,X2)),X1),
inference(orient,[status(thm)],[t225166]) ).
cnf(t33741,plain,
f(f(f(X1,X1),f(X2,X1)),X2) = f(X2,f(f(X2,X1),f(X1,X2))),
inference(cp,[status(thm)],[t33580,t1993]) ).
cnf(t225167,plain,
f(X1,X2) = f(X2,f(f(X2,X1),f(X1,X2))),
inference(step,[status(thm)],[t33741,t1993]) ).
cnf(t1488,plain,
f(f(X1,X2),f(f(f(f(f(f(X1,X2),X1),X1),X2),f(X1,X2)),f(X3,f(X1,X2)))) = f(f(X2,f(X3,f(X1,X2))),f(X1,X2)),
inference(cp,[status(thm)],[t1287,t1464]) ).
cnf(t224954,plain,
f(f(X1,X2),f(X2,f(X3,f(X1,X2)))) = f(f(X2,f(X3,f(X1,X2))),f(X1,X2)),
inference(step,[status(thm)],[t1488,t1464]) ).
cnf(t3646,plain,
f(f(X1,f(X2,f(X3,X1))),f(X3,X1)) = f(f(X3,X1),f(X1,f(X2,f(X3,X1)))),
inference(orient,[status(thm)],[t224954]) ).
cnf(t5366,plain,
f(f(X1,X2),f(X2,f(f(X1,X1),f(X1,X2)))) = f(f(X2,X1),f(X1,X2)),
inference(cp,[status(thm)],[t3646,t5330]) ).
cnf(t225009,plain,
f(f(X1,X2),f(X2,X1)) = f(f(X2,X1),f(X1,X2)),
inference(step,[status(thm)],[t5366,t5330]) ).
cnf(t6317,plain,
f(f(X1,X2),f(X2,X1)) = f(f(X2,X1),f(X1,X2)),
inference(orient,[status(thm)],[t225009]) ).
cnf(t225168,plain,
f(X1,X2) = f(X2,f(f(X1,X2),f(X2,X1))),
inference(step,[status(thm)],[t225167,t6317]) ).
cnf(t33986,plain,
f(X1,f(f(X2,X1),f(X1,X2))) = f(X2,X1),
inference(orient,[status(thm)],[t225168]) ).
cnf(t35215,plain,
f(X1,f(f(X2,X1),f(X1,X2))) = f(X2,X1),
inference(rw,[status(thm)],[t33986]) ).
cnf(t2117,plain,
X1 = f(f(f(X1,f(X2,X1)),X1),f(f(X2,X1),X1)),
inference(cp,[status(thm)],[t1464,t2098]) ).
cnf(t224943,plain,
X1 = f(f(X2,X1),f(f(X2,X1),X1)),
inference(step,[status(thm)],[t2117,t2076]) ).
cnf(t2135,plain,
f(f(X1,X2),f(f(X1,X2),X2)) = X2,
inference(orient,[status(thm)],[t224943]) ).
cnf(t2139,plain,
f(X1,X2) = f(X2,f(f(f(X2,X2),f(X1,X2)),f(X1,X2))),
inference(cp,[status(thm)],[t2135,t1993]) ).
cnf(t224944,plain,
f(X1,X2) = f(X2,f(X2,f(X1,X2))),
inference(step,[status(thm)],[t2139,t1993]) ).
cnf(t2193,plain,
f(X1,f(X1,f(X2,X1))) = f(X2,X1),
inference(orient,[status(thm)],[t224944]) ).
cnf(t5349,plain,
f(f(X1,X1),f(X1,X2)) = f(f(X1,X2),f(f(X1,X2),X1)),
inference(cp,[status(thm)],[t2193,t5330]) ).
cnf(t224987,plain,
X1 = f(f(X1,X2),f(f(X1,X2),X1)),
inference(step,[status(thm)],[t5349,t5330]) ).
cnf(t5352,plain,
f(X1,X2) = f(f(X1,f(X1,X2)),f(f(X1,X1),f(X1,X2))),
inference(cp,[status(thm)],[t2098,t5330]) ).
cnf(t224974,plain,
f(X1,X2) = f(f(X1,f(X1,X2)),X1),
inference(step,[status(thm)],[t5352,t5330]) ).
cnf(t5498,plain,
f(f(X1,f(X1,X2)),X1) = f(X1,X2),
inference(orient,[status(thm)],[t224974]) ).
cnf(t5350,plain,
f(X1,X2) = f(X1,f(f(f(X1,X1),f(X1,X2)),f(X1,X2))),
inference(cp,[status(thm)],[t2135,t5330]) ).
cnf(t224973,plain,
f(X1,X2) = f(X1,f(X1,f(X1,X2))),
inference(step,[status(thm)],[t5350,t5330]) ).
cnf(t5427,plain,
f(X1,f(X1,f(X1,X2))) = f(X1,X2),
inference(orient,[status(thm)],[t224973]) ).
cnf(t5500,plain,
f(X1,f(X1,X2)) = f(f(X1,X2),X1),
inference(cp,[status(thm)],[t5498,t5427]) ).
cnf(t5627,plain,
f(f(X1,X2),X1) = f(X1,f(X1,X2)),
inference(orient,[status(thm)],[t5500]) ).
cnf(t224988,plain,
X1 = f(f(X1,X2),f(X1,f(X1,X2))),
inference(step,[status(thm)],[t224987,t5627]) ).
cnf(t5662,plain,
f(f(X1,X2),f(X1,f(X1,X2))) = X1,
inference(orient,[status(thm)],[t224988]) ).
cnf(t1558,plain,
X1 = f(f(X2,f(f(f(X1,X1),X1),f(X3,X1))),f(X1,X1)),
inference(cp,[status(thm)],[t29,t1516]) ).
cnf(t224950,plain,
X1 = f(f(X2,f(f(X1,f(X1,X1)),f(X3,X1))),f(X1,X1)),
inference(step,[status(thm)],[t1558,t1878]) ).
cnf(t2724,plain,
f(f(X1,f(f(X2,f(X2,X2)),f(X3,X2))),f(X2,X2)) = X2,
inference(orient,[status(thm)],[t224950]) ).
cnf(t7551,plain,
f(f(X1,f(f(X2,f(X2,X2)),f(X3,X2))),f(X2,X2)) = X2,
inference(rw,[status(thm)],[t2724]) ).
cnf(t1489,plain,
f(f(X1,X2),f(f(X3,f(X1,X2)),f(f(f(f(f(X1,X2),X1),X1),X2),f(X1,X2)))) = f(f(f(X3,f(X1,X2)),X2),f(X1,X2)),
inference(cp,[status(thm)],[t1287,t1464]) ).
cnf(t224955,plain,
f(f(X1,X2),f(f(X3,f(X1,X2)),X2)) = f(f(f(X3,f(X1,X2)),X2),f(X1,X2)),
inference(step,[status(thm)],[t1489,t1464]) ).
cnf(t3772,plain,
f(f(f(X1,f(X2,X3)),X3),f(X2,X3)) = f(f(X2,X3),f(f(X1,f(X2,X3)),X3)),
inference(orient,[status(thm)],[t224955]) ).
cnf(t4553,plain,
f(X1,X1) = f(f(f(X2,X1),f(f(f(f(f(f(X2,X1),f(X2,X1)),X1),f(X2,X1)),f(X2,X1)),X1)),X1),
inference(cp,[status(thm)],[t4547,t3772]) ).
cnf(t224963,plain,
f(X1,X1) = f(X1,f(f(X2,X1),f(f(f(f(f(f(X2,X1),f(X2,X1)),X1),f(X2,X1)),f(X2,X1)),X1))),
inference(step,[status(thm)],[t4553,t1287]) ).
cnf(t1493,plain,
f(f(X1,f(X2,X3)),f(f(f(f(f(X2,X3),X2),X2),X3),f(X2,X3))) = f(X3,f(f(X2,X3),f(f(X1,f(X2,X3)),f(f(f(f(f(X2,X3),X2),X2),X3),f(X2,X3))))),
inference(cp,[status(thm)],[t1399,t1464]) ).
cnf(t224958,plain,
f(f(X1,f(X2,X3)),X3) = f(X3,f(f(X2,X3),f(f(X1,f(X2,X3)),f(f(f(f(f(X2,X3),X2),X2),X3),f(X2,X3))))),
inference(step,[status(thm)],[t1493,t1464]) ).
cnf(t224959,plain,
f(f(X1,f(X2,X3)),X3) = f(X3,f(f(X2,X3),f(f(X1,f(X2,X3)),X3))),
inference(step,[status(thm)],[t224958,t1464]) ).
cnf(t4098,plain,
f(X1,f(f(X2,X1),f(f(X3,f(X2,X1)),X1))) = f(f(X3,f(X2,X1)),X1),
inference(orient,[status(thm)],[t224959]) ).
cnf(t224964,plain,
f(X1,X1) = f(f(f(f(f(f(X2,X1),f(X2,X1)),X1),f(X2,X1)),f(X2,X1)),X1),
inference(step,[status(thm)],[t224963,t4098]) ).
cnf(t224965,plain,
f(X1,X1) = f(f(f(f(X2,X1),f(f(f(X2,X1),f(X2,X1)),X1)),f(X2,X1)),X1),
inference(step,[status(thm)],[t224964,t3772]) ).
cnf(t224966,plain,
f(X1,X1) = f(f(f(f(X2,X1),f(X1,f(f(X2,X1),f(X2,X1)))),f(X2,X1)),X1),
inference(step,[status(thm)],[t224965,t1287]) ).
cnf(t224967,plain,
f(X1,X1) = f(f(f(f(X2,X1),f(X2,X1)),f(X2,X1)),X1),
inference(step,[status(thm)],[t224966,t1212]) ).
cnf(t224968,plain,
f(X1,X1) = f(f(f(X2,X1),f(f(X2,X1),f(X2,X1))),X1),
inference(step,[status(thm)],[t224967,t1878]) ).
cnf(t4877,plain,
f(f(f(X1,X2),f(f(X1,X2),f(X1,X2))),X2) = f(X2,X2),
inference(orient,[status(thm)],[t224968]) ).
cnf(t4895,plain,
f(f(X1,X2),f(X1,X2)) = f(f(X2,f(f(f(X2,X2),f(X1,X2)),f(f(X2,X2),f(X1,X2)))),f(X1,X2)),
inference(cp,[status(thm)],[t4877,t1993]) ).
cnf(t225020,plain,
f(f(X1,X2),f(X1,X2)) = f(f(X2,f(X2,f(f(X2,X2),f(X1,X2)))),f(X1,X2)),
inference(step,[status(thm)],[t4895,t1993]) ).
cnf(t225021,plain,
f(f(X1,X2),f(X1,X2)) = f(f(X2,f(X2,X2)),f(X1,X2)),
inference(step,[status(thm)],[t225020,t1948]) ).
cnf(t7368,plain,
f(f(X1,X2),f(X1,X2)) = f(f(X2,f(X2,X2)),f(X1,X2)),
inference(orient,[status(thm)],[t225021]) ).
cnf(t225022,plain,
f(f(X1,f(f(X3,X2),f(X3,X2))),f(X2,X2)) = X2,
inference(step,[status(thm)],[t7551,t7368]) ).
cnf(t7553,plain,
f(f(X1,f(f(X2,X3),f(X2,X3))),f(X3,X3)) = X3,
inference(orient,[status(thm)],[t225022]) ).
cnf(t7584,plain,
f(X1,X2) = f(f(X3,f(X2,f(f(X2,X2),f(X1,X2)))),f(f(X1,X2),f(X1,X2))),
inference(cp,[status(thm)],[t7553,t1993]) ).
cnf(t225023,plain,
f(X1,X2) = f(f(X3,f(X2,X2)),f(f(X1,X2),f(X1,X2))),
inference(step,[status(thm)],[t7584,t1948]) ).
cnf(t7964,plain,
f(f(X1,f(X2,X2)),f(f(X3,X2),f(X3,X2))) = f(X3,X2),
inference(orient,[status(thm)],[t225023]) ).
cnf(t8051,plain,
f(X1,f(X2,X2)) = f(f(X3,X2),f(f(X1,f(X2,X2)),f(f(X1,f(X2,X2)),f(f(X3,X2),f(X3,X2))))),
inference(cp,[status(thm)],[t5662,t7964]) ).
cnf(t225028,plain,
f(X1,f(X2,X2)) = f(f(X3,X2),f(f(X1,f(X2,X2)),f(X3,X2))),
inference(step,[status(thm)],[t8051,t7964]) ).
cnf(t8659,plain,
f(f(X1,X2),f(f(X3,f(X2,X2)),f(X1,X2))) = f(X3,f(X2,X2)),
inference(orient,[status(thm)],[t225028]) ).
cnf(t8753,plain,
f(X1,X2) = f(f(f(X1,X2),f(X1,X2)),f(X3,f(X2,X2))),
inference(cp,[status(thm)],[t5330,t8659]) ).
cnf(t9317,plain,
f(f(f(X1,X2),f(X1,X2)),f(X3,f(X2,X2))) = f(X1,X2),
inference(orient,[status(thm)],[t8753]) ).
cnf(t9342,plain,
f(f(X1,X1),f(X1,X2)) = f(f(X1,f(f(X1,X1),f(X1,X2))),f(X3,f(f(X1,X2),f(X1,X2)))),
inference(cp,[status(thm)],[t9317,t5330]) ).
cnf(t225040,plain,
X1 = f(f(X1,f(f(X1,X1),f(X1,X2))),f(X3,f(f(X1,X2),f(X1,X2)))),
inference(step,[status(thm)],[t9342,t5330]) ).
cnf(t1994,plain,
f(X1,X1) = f(X1,f(X2,f(X1,X1))),
inference(cp,[status(thm)],[t1993,t1768]) ).
cnf(t2041,plain,
f(X1,f(X2,f(X1,X1))) = f(X1,X1),
inference(orient,[status(thm)],[t1994]) ).
cnf(t2469,plain,
f(X1,X1) = f(X1,f(f(X1,X1),f(f(f(X1,X1),f(X1,X1)),X2))),
inference(cp,[status(thm)],[t2041,t2454]) ).
cnf(t224948,plain,
f(X1,X1) = f(X1,f(f(X1,X1),f(X1,X2))),
inference(step,[status(thm)],[t2469,t1516]) ).
cnf(t2498,plain,
f(X1,f(f(X1,X1),f(X1,X2))) = f(X1,X1),
inference(orient,[status(thm)],[t224948]) ).
cnf(t225041,plain,
X1 = f(f(X1,X1),f(X3,f(f(X1,X2),f(X1,X2)))),
inference(step,[status(thm)],[t225040,t2498]) ).
cnf(t9911,plain,
f(f(X1,X1),f(X2,f(f(X1,X3),f(X1,X3)))) = X1,
inference(orient,[status(thm)],[t225041]) ).
cnf(t9945,plain,
f(X1,X2) = f(f(f(X1,X2),f(X1,X2)),f(X3,f(X1,f(f(X1,X2),f(X1,X1))))),
inference(cp,[status(thm)],[t9911,t1768]) ).
cnf(t225045,plain,
f(X1,X2) = f(f(f(X1,X2),f(X1,X2)),f(X3,f(X1,X1))),
inference(step,[status(thm)],[t9945,t2041]) ).
cnf(t10619,plain,
f(f(f(X1,X2),f(X1,X2)),f(X3,f(X1,X1))) = f(X1,X2),
inference(orient,[status(thm)],[t225045]) ).
cnf(t33733,plain,
f(f(f(f(X1,X2),f(X1,X2)),f(X3,f(X1,X1))),X3) = f(X3,f(f(X3,f(X1,X1)),f(f(X1,X2),X3))),
inference(cp,[status(thm)],[t33580,t10619]) ).
cnf(t225170,plain,
f(f(X1,X2),X3) = f(X3,f(f(X3,f(X1,X1)),f(f(X1,X2),X3))),
inference(step,[status(thm)],[t33733,t10619]) ).
cnf(t34360,plain,
f(X1,f(f(X1,f(X2,X2)),f(f(X2,X3),X1))) = f(f(X2,X3),X1),
inference(orient,[status(thm)],[t225170]) ).
cnf(t34494,plain,
f(f(X1,X2),f(X2,X1)) = f(f(X2,X1),f(f(f(X2,X1),f(X1,X1)),f(f(X2,X1),f(X1,X2)))),
inference(cp,[status(thm)],[t34360,t6317]) ).
cnf(t225171,plain,
f(f(X1,X2),f(X2,X1)) = f(f(X2,X1),f(X1,f(f(X2,X1),f(X1,X2)))),
inference(step,[status(thm)],[t34494,t1516]) ).
cnf(t225172,plain,
f(f(X1,X2),f(X2,X1)) = f(f(X2,X1),f(X2,X1)),
inference(step,[status(thm)],[t225171,t33986]) ).
cnf(t34750,plain,
f(f(X1,X2),f(X2,X1)) = f(f(X2,X1),f(X2,X1)),
inference(orient,[status(thm)],[t225172]) ).
cnf(t225173,plain,
f(X1,f(f(X1,X2),f(X1,X2))) = f(X2,X1),
inference(step,[status(thm)],[t35215,t34750]) ).
cnf(t1772,plain,
f(X1,X2) = f(X1,f(f(X1,X2),f(X1,X2))),
inference(cp,[status(thm)],[t1768,t1768]) ).
cnf(t1911,plain,
f(X1,f(f(X1,X2),f(X1,X2))) = f(X1,X2),
inference(orient,[status(thm)],[t1772]) ).
cnf(t225174,plain,
f(X1,X2) = f(X2,X1),
inference(step,[status(thm)],[t225173,t1911]) ).
cnf(t35219,plain,
f(X1,X2) = f(X2,X1),
inference(orient,[status(thm)],[t225174]) ).
cnf(t225196,plain,
f(f(X1,X2),f(X2,f(f(X1,X2),f(X3,X2)))) = f(f(X3,X2),f(X1,X2)),
inference(step,[status(thm)],[t35289,t35219]) ).
cnf(t225197,plain,
f(f(X1,X2),f(X2,f(f(X1,X2),f(X2,X3)))) = f(f(X3,X2),f(X1,X2)),
inference(step,[status(thm)],[t225196,t35219]) ).
cnf(t225198,plain,
f(f(X1,X2),f(X2,f(f(X1,X2),f(X2,X3)))) = f(f(X1,X2),f(X3,X2)),
inference(step,[status(thm)],[t225197,t35219]) ).
cnf(t225199,plain,
f(f(X1,X2),f(X2,f(f(X1,X2),f(X2,X3)))) = f(f(X1,X2),f(X2,X3)),
inference(step,[status(thm)],[t225198,t35219]) ).
cnf(t36150,plain,
f(f(X1,X2),f(X2,f(f(X1,X2),f(X2,X3)))) = f(f(X1,X2),f(X2,X3)),
inference(orient,[status(thm)],[t225199]) ).
cnf(t5499,plain,
f(X1,f(X2,X1)) = f(f(X2,X1),X1),
inference(cp,[status(thm)],[t5498,t2193]) ).
cnf(t5580,plain,
f(f(X1,X2),X2) = f(X2,f(X1,X2)),
inference(orient,[status(thm)],[t5499]) ).
cnf(t224981,plain,
f(f(f(f(X3,f(f(f(X1,X1),X2),X3)),X2),X1),X2) = f(X2,X2),
inference(step,[status(thm)],[t4547,t5580]) ).
cnf(t5620,plain,
f(f(f(f(X3,f(f(f(X1,X1),X2),X3)),X2),X1),X2) = f(X2,X2),
inference(rw,[status(thm)],[t224981]) ).
cnf(t225208,plain,
f(X2,f(f(f(X3,f(f(f(X1,X1),X2),X3)),X2),X1)) = f(X2,X2),
inference(step,[status(thm)],[t5620,t35219]) ).
cnf(t225209,plain,
f(X2,f(X1,f(f(X3,f(f(f(X1,X1),X2),X3)),X2))) = f(X2,X2),
inference(step,[status(thm)],[t225208,t35219]) ).
cnf(t225210,plain,
f(X2,f(X1,f(X2,f(X3,f(f(f(X1,X1),X2),X3))))) = f(X2,X2),
inference(step,[status(thm)],[t225209,t35219]) ).
cnf(t225211,plain,
f(X2,f(X1,f(X2,f(X3,f(X3,f(f(X1,X1),X2)))))) = f(X2,X2),
inference(step,[status(thm)],[t225210,t35219]) ).
cnf(t225212,plain,
f(X2,f(X1,f(X2,f(X3,f(X3,f(X2,f(X1,X1))))))) = f(X2,X2),
inference(step,[status(thm)],[t225211,t35219]) ).
cnf(t36475,plain,
f(X1,f(X2,f(X1,f(X3,f(X3,f(X1,f(X2,X2))))))) = f(X1,X1),
inference(orient,[status(thm)],[t225212]) ).
cnf(t36547,plain,
f(f(X1,X2),f(X2,f(X3,f(X3,f(X2,f(f(X1,X2),f(X1,X2))))))) = f(f(X1,X2),f(X2,X2)),
inference(cp,[status(thm)],[t36150,t36475]) ).
cnf(t5345,plain,
f(X1,X2) = f(f(f(X1,X2),f(X1,X2)),X1),
inference(cp,[status(thm)],[t5330,t1768]) ).
cnf(t5739,plain,
f(f(f(X1,X2),f(X1,X2)),X1) = f(X1,X2),
inference(orient,[status(thm)],[t5345]) ).
cnf(t4559,plain,
f(X1,X1) = f(f(f(f(f(X2,X2),X1),X1),X2),X1),
inference(cp,[status(thm)],[t4547,t1768]) ).
cnf(t4659,plain,
f(f(f(f(f(X1,X1),X2),X2),X1),X2) = f(X2,X2),
inference(orient,[status(thm)],[t4559]) ).
cnf(t4682,plain,
f(X1,X1) = f(f(f(f(X2,X1),X1),f(X2,X2)),X1),
inference(cp,[status(thm)],[t4659,t1993]) ).
cnf(t4790,plain,
f(f(f(f(X1,X2),X2),f(X1,X1)),X2) = f(X2,X2),
inference(orient,[status(thm)],[t4682]) ).
cnf(t224978,plain,
f(f(f(X2,f(X1,X2)),f(X1,X1)),X2) = f(X2,X2),
inference(step,[status(thm)],[t4790,t5580]) ).
cnf(t5617,plain,
f(f(f(X2,f(X1,X2)),f(X1,X1)),X2) = f(X2,X2),
inference(rw,[status(thm)],[t224978]) ).
cnf(t5778,plain,
f(f(f(X1,f(X2,X1)),f(X2,X2)),X1) = f(X1,X1),
inference(orient,[status(thm)],[t5617]) ).
cnf(t5816,plain,
f(f(f(X1,f(X2,X1)),f(X2,X2)),X1) = f(f(f(X1,X1),f(f(f(X1,f(X2,X1)),f(X2,X2)),X1)),f(f(X1,f(X2,X1)),f(X2,X2))),
inference(cp,[status(thm)],[t5739,t5778]) ).
cnf(t224991,plain,
f(X1,X1) = f(f(f(X1,X1),f(f(f(X1,f(X2,X1)),f(X2,X2)),X1)),f(f(X1,f(X2,X1)),f(X2,X2))),
inference(step,[status(thm)],[t5816,t5778]) ).
cnf(t224992,plain,
f(X1,X1) = f(X1,f(f(X1,f(X2,X1)),f(X2,X2))),
inference(step,[status(thm)],[t224991,t1993]) ).
cnf(t5896,plain,
f(X1,f(f(X1,f(X2,X1)),f(X2,X2))) = f(X1,X1),
inference(orient,[status(thm)],[t224992]) ).
cnf(t8000,plain,
f(f(X1,X1),f(X1,X2)) = f(f(X3,f(f(X1,X2),f(X1,X2))),f(X1,f(f(X1,X1),f(X1,X2)))),
inference(cp,[status(thm)],[t7964,t5330]) ).
cnf(t225024,plain,
X1 = f(f(X3,f(f(X1,X2),f(X1,X2))),f(X1,f(f(X1,X1),f(X1,X2)))),
inference(step,[status(thm)],[t8000,t5330]) ).
cnf(t225025,plain,
X1 = f(f(X3,f(f(X1,X2),f(X1,X2))),f(X1,X1)),
inference(step,[status(thm)],[t225024,t2498]) ).
cnf(t8104,plain,
f(f(X1,f(f(X2,X3),f(X2,X3))),f(X2,X2)) = X2,
inference(orient,[status(thm)],[t225025]) ).
cnf(t224916,plain,
f(f(X1,f(f(X2,X3),f(X4,X3))),f(X3,f(f(X2,X3),f(X4,X3)))) = f(f(X2,X3),f(X4,X3)),
inference(step,[status(thm)],[t498,t1287]) ).
cnf(t1335,plain,
f(f(X1,f(f(X2,X3),f(X4,X3))),f(X3,f(f(X2,X3),f(X4,X3)))) = f(f(X2,X3),f(X4,X3)),
inference(rw,[status(thm)],[t224916]) ).
cnf(t7671,plain,
f(f(X1,f(f(X2,X3),f(X4,X3))),f(X3,f(f(X2,X3),f(X4,X3)))) = f(f(X2,X3),f(X4,X3)),
inference(orient,[status(thm)],[t1335]) ).
cnf(t8112,plain,
X1 = f(f(X2,f(f(X3,X1),f(X4,X1))),f(X1,X1)),
inference(cp,[status(thm)],[t8104,t7671]) ).
cnf(t8202,plain,
f(f(X1,f(f(X2,X3),f(X4,X3))),f(X3,X3)) = X3,
inference(orient,[status(thm)],[t8112]) ).
cnf(t8246,plain,
X1 = f(f(X2,f(f(X1,f(X3,X1)),f(X4,X1))),f(X1,X1)),
inference(cp,[status(thm)],[t8202,t5580]) ).
cnf(t17156,plain,
f(f(X1,f(f(X2,f(X3,X2)),f(X4,X2))),f(X2,X2)) = X2,
inference(orient,[status(thm)],[t8246]) ).
cnf(t17226,plain,
X1 = f(f(X2,f(f(X1,f(X1,f(X1,X3))),f(X4,X1))),f(X1,X1)),
inference(cp,[status(thm)],[t17156,t5627]) ).
cnf(t225095,plain,
X1 = f(f(X2,f(f(X1,X3),f(X4,X1))),f(X1,X1)),
inference(step,[status(thm)],[t17226,t5427]) ).
cnf(t17387,plain,
f(f(X1,f(f(X2,X3),f(X4,X2))),f(X2,X2)) = X2,
inference(orient,[status(thm)],[t225095]) ).
cnf(t17504,plain,
X1 = f(f(X2,f(f(X1,X3),f(X1,f(X4,X1)))),f(X1,X1)),
inference(cp,[status(thm)],[t17387,t5580]) ).
cnf(t24364,plain,
f(f(X1,f(f(X2,X3),f(X2,f(X4,X2)))),f(X2,X2)) = X2,
inference(orient,[status(thm)],[t17504]) ).
cnf(t24514,plain,
X1 = f(f(X2,f(f(X1,X3),f(X1,f(X1,f(X1,X4))))),f(X1,X1)),
inference(cp,[status(thm)],[t24364,t5627]) ).
cnf(t225134,plain,
X1 = f(f(X2,f(f(X1,X3),f(X1,X4))),f(X1,X1)),
inference(step,[status(thm)],[t24514,t5427]) ).
cnf(t24654,plain,
f(f(X1,f(f(X2,X3),f(X2,X4))),f(X2,X2)) = X2,
inference(orient,[status(thm)],[t225134]) ).
cnf(t24885,plain,
f(f(X1,X1),f(X1,X1)) = f(f(X1,X1),f(f(f(X1,X1),X1),f(f(X2,f(f(X1,X3),f(X1,X4))),f(X2,f(f(X1,X3),f(X1,X4)))))),
inference(cp,[status(thm)],[t5896,t24654]) ).
cnf(t225136,plain,
X1 = f(f(X1,X1),f(f(f(X1,X1),X1),f(f(X2,f(f(X1,X3),f(X1,X4))),f(X2,f(f(X1,X3),f(X1,X4)))))),
inference(step,[status(thm)],[t24885,t1516]) ).
cnf(t225137,plain,
X1 = f(f(X1,X1),f(f(X1,f(X1,X1)),f(f(X2,f(f(X1,X3),f(X1,X4))),f(X2,f(f(X1,X3),f(X1,X4)))))),
inference(step,[status(thm)],[t225136,t5580]) ).
cnf(t8128,plain,
f(X1,X2) = f(f(X3,f(X1,f(f(X1,X2),f(X1,X1)))),f(f(X1,X2),f(X1,X2))),
inference(cp,[status(thm)],[t8104,t1768]) ).
cnf(t225026,plain,
f(X1,X2) = f(f(X3,f(X1,X1)),f(f(X1,X2),f(X1,X2))),
inference(step,[status(thm)],[t8128,t2041]) ).
cnf(t8343,plain,
f(f(X1,f(X2,X2)),f(f(X2,X3),f(X2,X3))) = f(X2,X3),
inference(orient,[status(thm)],[t225026]) ).
cnf(t224980,plain,
f(f(f(X2,f(f(X1,X1),X2)),X1),X2) = f(X2,X2),
inference(step,[status(thm)],[t4659,t5580]) ).
cnf(t5619,plain,
f(f(f(X2,f(f(X1,X1),X2)),X1),X2) = f(X2,X2),
inference(rw,[status(thm)],[t224980]) ).
cnf(t5823,plain,
f(f(f(X1,f(f(X2,X2),X1)),X2),X1) = f(X1,X1),
inference(orient,[status(thm)],[t5619]) ).
cnf(t8695,plain,
f(f(f(X1,X2),f(f(f(X2,X2),f(X2,X2)),f(X1,X2))),f(X2,X2)) = f(f(X1,X2),f(f(X1,X2),f(X1,X2))),
inference(cp,[status(thm)],[t8659,t5823]) ).
cnf(t225029,plain,
f(f(f(X2,X2),f(X2,X2)),f(X2,X2)) = f(f(X1,X2),f(f(X1,X2),f(X1,X2))),
inference(step,[status(thm)],[t8695,t8659]) ).
cnf(t225030,plain,
f(X2,f(X2,X2)) = f(f(X1,X2),f(f(X1,X2),f(X1,X2))),
inference(step,[status(thm)],[t225029,t1516]) ).
cnf(t8824,plain,
f(f(X1,X2),f(f(X1,X2),f(X1,X2))) = f(X2,f(X2,X2)),
inference(orient,[status(thm)],[t225030]) ).
cnf(t8827,plain,
f(f(f(X1,X1),X2),f(f(f(X1,X1),X2),f(f(X1,X1),X2))) = f(f(X1,X1),f(f(X1,f(f(X1,X1),X2)),f(X1,f(f(X1,X1),X2)))),
inference(cp,[status(thm)],[t8824,t5232]) ).
cnf(t225032,plain,
f(X2,f(X2,X2)) = f(f(X1,X1),f(f(X1,f(f(X1,X1),X2)),f(X1,f(f(X1,X1),X2)))),
inference(step,[status(thm)],[t8827,t8824]) ).
cnf(t225033,plain,
f(X2,f(X2,X2)) = f(f(X1,X1),X1),
inference(step,[status(thm)],[t225032,t5080]) ).
cnf(t225034,plain,
f(X2,f(X2,X2)) = f(X1,f(X1,X1)),
inference(step,[status(thm)],[t225033,t5580]) ).
cnf(t8971,plain,
f(X1,f(X1,X1)) = f(X2,f(X2,X2)),
inference(orient,[status(thm)],[t225034]) ).
cnf(t8991,plain,
f(X1,X2) = f(f(X3,f(X3,X3)),f(f(X1,X2),f(X1,X2))),
inference(cp,[status(thm)],[t8343,t8971]) ).
cnf(t10343,plain,
f(f(X1,f(X1,X1)),f(f(X2,X3),f(X2,X3))) = f(X2,X3),
inference(orient,[status(thm)],[t8991]) ).
cnf(t225138,plain,
X1 = f(f(X1,X1),f(X2,f(f(X1,X3),f(X1,X4)))),
inference(step,[status(thm)],[t225137,t10343]) ).
cnf(t25119,plain,
f(f(X1,X1),f(X2,f(f(X1,X3),f(X1,X4)))) = X1,
inference(orient,[status(thm)],[t225138]) ).
cnf(t1579,plain,
f(X1,X1) = f(f(f(f(X1,f(X1,X1)),f(X2,f(X1,X1))),X3),f(f(X1,X1),f(X1,X1))),
inference(cp,[status(thm)],[t1,t1572]) ).
cnf(t224960,plain,
f(X1,X1) = f(f(f(f(X1,f(X1,X1)),f(X2,f(X1,X1))),X3),X1),
inference(step,[status(thm)],[t1579,t1516]) ).
cnf(t4397,plain,
f(f(f(f(X1,f(X1,X1)),f(X2,f(X1,X1))),X3),X1) = f(X1,X1),
inference(orient,[status(thm)],[t224960]) ).
cnf(t10763,plain,
f(f(X1,X1),f(X1,X1)) = f(f(f(f(f(X1,X1),f(f(X1,X1),f(X1,X1))),f(X1,X2)),X3),f(X1,X1)),
inference(cp,[status(thm)],[t4397,t10619]) ).
cnf(t225103,plain,
X1 = f(f(f(f(f(X1,X1),f(f(X1,X1),f(X1,X1))),f(X1,X2)),X3),f(X1,X1)),
inference(step,[status(thm)],[t10763,t1516]) ).
cnf(t4750,plain,
f(X1,X1) = f(f(f(f(f(X2,X2),X2),X1),f(X2,X2)),X1),
inference(cp,[status(thm)],[t4724,t1993]) ).
cnf(t224969,plain,
f(X1,X1) = f(f(f(f(X2,f(X2,X2)),X1),f(X2,X2)),X1),
inference(step,[status(thm)],[t4750,t1878]) ).
cnf(t5006,plain,
f(f(f(f(X1,f(X1,X1)),X2),f(X1,X1)),X2) = f(X2,X2),
inference(orient,[status(thm)],[t224969]) ).
cnf(t8469,plain,
f(X1,X1) = f(f(f(f(X2,f(X2,X2)),X1),f(f(X2,f(X2,X2)),f(X2,f(X2,X2)))),X1),
inference(cp,[status(thm)],[t5006,t8343]) ).
cnf(t225027,plain,
f(X1,X1) = f(f(X2,f(X2,X2)),X1),
inference(step,[status(thm)],[t8469,t1768]) ).
cnf(t8484,plain,
f(X1,X1) = f(f(X2,f(X2,X2)),X1),
inference(orient,[status(thm)],[t225027]) ).
cnf(t225104,plain,
X1 = f(f(f(f(X1,X2),f(X1,X2)),X3),f(X1,X1)),
inference(step,[status(thm)],[t225103,t8484]) ).
cnf(t18547,plain,
f(f(f(f(X1,X2),f(X1,X2)),X3),f(X1,X1)) = X1,
inference(orient,[status(thm)],[t225104]) ).
cnf(t18703,plain,
f(f(X1,X1),f(X1,X1)) = f(f(X1,X1),f(f(f(X1,X1),X1),f(f(f(f(X1,X2),f(X1,X2)),X3),f(f(f(X1,X2),f(X1,X2)),X3)))),
inference(cp,[status(thm)],[t5896,t18547]) ).
cnf(t225105,plain,
X1 = f(f(X1,X1),f(f(f(X1,X1),X1),f(f(f(f(X1,X2),f(X1,X2)),X3),f(f(f(X1,X2),f(X1,X2)),X3)))),
inference(step,[status(thm)],[t18703,t1516]) ).
cnf(t225106,plain,
X1 = f(f(X1,X1),f(f(X1,f(X1,X1)),f(f(f(f(X1,X2),f(X1,X2)),X3),f(f(f(X1,X2),f(X1,X2)),X3)))),
inference(step,[status(thm)],[t225105,t5580]) ).
cnf(t225107,plain,
X1 = f(f(X1,X1),f(f(f(X1,X2),f(X1,X2)),X3)),
inference(step,[status(thm)],[t225106,t10343]) ).
cnf(t18713,plain,
f(f(X1,X1),f(f(f(X1,X2),f(X1,X2)),X3)) = X1,
inference(orient,[status(thm)],[t225107]) ).
cnf(t18757,plain,
f(X1,X2) = f(f(f(X1,X2),f(X1,X2)),f(f(X1,f(f(X1,X2),f(X1,X1))),X3)),
inference(cp,[status(thm)],[t18713,t1768]) ).
cnf(t225111,plain,
f(X1,X2) = f(f(f(X1,X2),f(X1,X2)),f(f(X1,X1),X3)),
inference(step,[status(thm)],[t18757,t2041]) ).
cnf(t19645,plain,
f(f(f(X1,X2),f(X1,X2)),f(f(X1,X1),X3)) = f(X1,X2),
inference(orient,[status(thm)],[t225111]) ).
cnf(t19890,plain,
f(f(f(f(X1,X2),f(X1,X2)),f(f(X1,X1),X3)),X3) = f(X3,f(f(f(X1,X1),X3),f(f(X1,X2),X3))),
inference(cp,[status(thm)],[t4098,t19645]) ).
cnf(t225115,plain,
f(f(X1,X2),X3) = f(X3,f(f(f(X1,X1),X3),f(f(X1,X2),X3))),
inference(step,[status(thm)],[t19890,t19645]) ).
cnf(t20826,plain,
f(X1,f(f(f(X2,X2),X1),f(f(X2,X3),X1))) = f(f(X2,X3),X1),
inference(orient,[status(thm)],[t225115]) ).
cnf(t8279,plain,
X1 = f(f(X2,f(f(X3,X1),f(X1,f(X4,X1)))),f(X1,X1)),
inference(cp,[status(thm)],[t8202,t5580]) ).
cnf(t17850,plain,
f(f(X1,f(f(X2,X3),f(X3,f(X4,X3)))),f(X3,X3)) = X3,
inference(orient,[status(thm)],[t8279]) ).
cnf(t17981,plain,
X1 = f(f(X2,f(f(X3,X1),f(X1,f(X1,f(X1,X4))))),f(X1,X1)),
inference(cp,[status(thm)],[t17850,t5627]) ).
cnf(t225099,plain,
X1 = f(f(X2,f(f(X3,X1),f(X1,X4))),f(X1,X1)),
inference(step,[status(thm)],[t17981,t5427]) ).
cnf(t18084,plain,
f(f(X1,f(f(X2,X3),f(X3,X4))),f(X3,X3)) = X3,
inference(orient,[status(thm)],[t225099]) ).
cnf(t20853,plain,
f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,X2)) = f(f(X2,X2),f(X2,f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,X2)))),
inference(cp,[status(thm)],[t20826,t18084]) ).
cnf(t225116,plain,
f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,X2)) = X2,
inference(step,[status(thm)],[t20853,t5330]) ).
cnf(t21096,plain,
f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,X2)) = X2,
inference(orient,[status(thm)],[t225116]) ).
cnf(t35323,plain,
f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,X2)) = X2,
inference(rw,[status(thm)],[t21096]) ).
cnf(t225180,plain,
f(f(X2,X2),f(f(f(X1,X2),f(X2,X3)),X4)) = X2,
inference(step,[status(thm)],[t35323,t35219]) ).
cnf(t225181,plain,
f(f(X2,X2),f(X4,f(f(X1,X2),f(X2,X3)))) = X2,
inference(step,[status(thm)],[t225180,t35219]) ).
cnf(t35623,plain,
f(f(X1,X1),f(X2,f(f(X3,X1),f(X1,X4)))) = X1,
inference(orient,[status(thm)],[t225181]) ).
cnf(t35706,plain,
f(X1,X2) = f(f(f(X1,X2),f(X1,X2)),X2),
inference(cp,[status(thm)],[t25119,t35623]) ).
cnf(t225187,plain,
f(X1,X2) = f(X2,f(f(X1,X2),f(X1,X2))),
inference(step,[status(thm)],[t35706,t35219]) ).
cnf(t35785,plain,
f(X1,f(f(X2,X1),f(X2,X1))) = f(X2,X1),
inference(orient,[status(thm)],[t225187]) ).
cnf(t225213,plain,
f(f(X1,X2),f(X2,f(X3,f(X3,f(X1,X2))))) = f(f(X1,X2),f(X2,X2)),
inference(step,[status(thm)],[t36547,t35785]) ).
cnf(t225214,plain,
f(f(X1,X2),f(X2,f(X3,f(X3,f(X1,X2))))) = X2,
inference(step,[status(thm)],[t225213,t1516]) ).
cnf(t36557,plain,
f(f(X1,X2),f(X2,f(X3,f(X3,f(X1,X2))))) = X2,
inference(orient,[status(thm)],[t225214]) ).
cnf(t36589,plain,
X1 = f(f(X1,X2),f(X1,f(X3,f(X3,f(X2,X1))))),
inference(cp,[status(thm)],[t36557,t35219]) ).
cnf(t225218,plain,
X1 = f(f(X1,X2),f(X1,f(X3,f(X3,f(X1,X2))))),
inference(step,[status(thm)],[t36589,t35219]) ).
cnf(t36936,plain,
f(f(X1,X2),f(X1,f(X3,f(X3,f(X1,X2))))) = X1,
inference(orient,[status(thm)],[t225218]) ).
cnf(t36600,plain,
f(X1,X2) = f(f(f(X1,X3),f(X1,X2)),f(f(X1,X2),X1)),
inference(cp,[status(thm)],[t36557,t25119]) ).
cnf(t225222,plain,
f(X1,X2) = f(f(f(X1,X2),X1),f(f(X1,X3),f(X1,X2))),
inference(step,[status(thm)],[t36600,t35219]) ).
cnf(t225223,plain,
f(X1,X2) = f(f(X1,f(X1,X2)),f(f(X1,X3),f(X1,X2))),
inference(step,[status(thm)],[t225222,t35219]) ).
cnf(t225224,plain,
f(X1,X2) = f(f(X1,f(X1,X2)),f(f(X1,X2),f(X1,X3))),
inference(step,[status(thm)],[t225223,t35219]) ).
cnf(t37132,plain,
f(f(X1,f(X1,X2)),f(f(X1,X2),f(X1,X3))) = f(X1,X2),
inference(orient,[status(thm)],[t225224]) ).
cnf(t37162,plain,
f(f(X1,X2),f(X1,f(X3,f(X3,f(X1,X2))))) = f(f(f(X1,X2),X1),f(f(f(X1,X2),f(X1,f(X3,f(X3,f(X1,X2))))),f(f(X1,X2),X4))),
inference(cp,[status(thm)],[t37132,t36936]) ).
cnf(t225225,plain,
X1 = f(f(f(X1,X2),X1),f(f(f(X1,X2),f(X1,f(X3,f(X3,f(X1,X2))))),f(f(X1,X2),X4))),
inference(step,[status(thm)],[t37162,t36936]) ).
cnf(t225226,plain,
X1 = f(f(X1,f(X1,X2)),f(f(f(X1,X2),f(X1,f(X3,f(X3,f(X1,X2))))),f(f(X1,X2),X4))),
inference(step,[status(thm)],[t225225,t35219]) ).
cnf(t225227,plain,
X1 = f(f(X1,f(X1,X2)),f(f(f(X1,X2),X4),f(f(X1,X2),f(X1,f(X3,f(X3,f(X1,X2))))))),
inference(step,[status(thm)],[t225226,t35219]) ).
cnf(t225228,plain,
X1 = f(f(X1,f(X1,X2)),f(f(X4,f(X1,X2)),f(f(X1,X2),f(X1,f(X3,f(X3,f(X1,X2))))))),
inference(step,[status(thm)],[t225227,t35219]) ).
cnf(t225229,plain,
X1 = f(f(X1,f(X1,X2)),f(f(X4,f(X1,X2)),X1)),
inference(step,[status(thm)],[t225228,t36936]) ).
cnf(t225230,plain,
X1 = f(f(X1,f(X1,X2)),f(X1,f(X4,f(X1,X2)))),
inference(step,[status(thm)],[t225229,t35219]) ).
cnf(t37305,plain,
f(f(X1,f(X1,X2)),f(X1,f(X3,f(X1,X2)))) = X1,
inference(orient,[status(thm)],[t225230]) ).
cnf(t37385,plain,
X1 = f(f(X1,f(X1,f(f(X2,X3),f(X3,X4)))),f(X1,X3)),
inference(cp,[status(thm)],[t37305,t35623]) ).
cnf(t225305,plain,
X1 = f(f(X1,X3),f(X1,f(X1,f(f(X2,X3),f(X3,X4))))),
inference(step,[status(thm)],[t37385,t35219]) ).
cnf(t42257,plain,
f(f(X1,X2),f(X1,f(X1,f(f(X3,X2),f(X2,X4))))) = X1,
inference(orient,[status(thm)],[t225305]) ).
cnf(t42576,plain,
f(X1,X2) = f(f(f(X1,X2),f(X2,X3)),X1),
inference(cp,[status(thm)],[t36936,t42257]) ).
cnf(t225306,plain,
f(X1,X2) = f(X1,f(f(X1,X2),f(X2,X3))),
inference(step,[status(thm)],[t42576,t35219]) ).
cnf(t42603,plain,
f(X1,f(f(X1,X2),f(X2,X3))) = f(X1,X2),
inference(orient,[status(thm)],[t225306]) ).
cnf(t42691,plain,
f(X1,f(X2,X3)) = f(X1,f(f(X1,f(X2,X3)),X2)),
inference(cp,[status(thm)],[t42603,t36936]) ).
cnf(t225307,plain,
f(X1,f(X2,X3)) = f(X1,f(X2,f(X1,f(X2,X3)))),
inference(step,[status(thm)],[t42691,t35219]) ).
cnf(t42808,plain,
f(X1,f(X2,f(X1,f(X2,X3)))) = f(X1,f(X2,X3)),
inference(orient,[status(thm)],[t225307]) ).
cnf(t42816,plain,
f(X1,f(X2,f(X3,f(X3,f(X2,f(X1,X1)))))) = f(X1,f(X2,X2)),
inference(cp,[status(thm)],[t42808,t36475]) ).
cnf(t44534,plain,
f(X1,f(X2,f(X3,f(X3,f(X2,f(X1,X1)))))) = f(X1,f(X2,X2)),
inference(orient,[status(thm)],[t42816]) ).
cnf(t8769,plain,
f(f(X1,X2),f(f(X3,f(X2,X2)),f(X1,X2))) = f(f(X1,X2),f(f(X1,X2),f(X3,f(X2,X2)))),
inference(cp,[status(thm)],[t5427,t8659]) ).
cnf(t225047,plain,
f(X3,f(X2,X2)) = f(f(X1,X2),f(f(X1,X2),f(X3,f(X2,X2)))),
inference(step,[status(thm)],[t8769,t8659]) ).
cnf(t10965,plain,
f(f(X1,X2),f(f(X1,X2),f(X3,f(X2,X2)))) = f(X3,f(X2,X2)),
inference(orient,[status(thm)],[t225047]) ).
cnf(t42694,plain,
f(X1,f(X2,X3)) = f(X1,f(f(X1,f(X2,X3)),f(X4,f(X3,X3)))),
inference(cp,[status(thm)],[t42603,t10965]) ).
cnf(t44035,plain,
f(X1,f(f(X1,f(X2,X3)),f(X4,f(X3,X3)))) = f(X1,f(X2,X3)),
inference(orient,[status(thm)],[t42694]) ).
cnf(t44548,plain,
f(f(X1,X1),f(f(X2,f(X3,X1)),f(X2,f(X3,X1)))) = f(f(X1,X1),f(f(X2,f(X3,X1)),f(X2,f(X2,f(X3,X1))))),
inference(cp,[status(thm)],[t44534,t44035]) ).
cnf(t225384,plain,
f(f(X1,X1),f(f(X2,f(X1,X3)),f(X2,f(X3,X1)))) = f(f(X1,X1),f(f(X2,f(X3,X1)),f(X2,f(X2,f(X3,X1))))),
inference(step,[status(thm)],[t44548,t35219]) ).
cnf(t225385,plain,
f(f(X1,X1),f(f(X2,f(X1,X3)),f(X2,f(X1,X3)))) = f(f(X1,X1),f(f(X2,f(X3,X1)),f(X2,f(X2,f(X3,X1))))),
inference(step,[status(thm)],[t225384,t35219]) ).
cnf(t225386,plain,
f(f(X1,X1),f(f(X2,f(X1,X3)),f(X2,f(X1,X3)))) = f(f(X1,X1),X2),
inference(step,[status(thm)],[t225385,t5662]) ).
cnf(t225387,plain,
f(f(X1,X1),f(f(X2,f(X1,X3)),f(X2,f(X1,X3)))) = f(X2,f(X1,X1)),
inference(step,[status(thm)],[t225386,t35219]) ).
cnf(t54532,plain,
f(f(X1,X1),f(f(X2,f(X1,X3)),f(X2,f(X1,X3)))) = f(X2,f(X1,X1)),
inference(orient,[status(thm)],[t225387]) ).
cnf(t54636,plain,
f(X1,f(f(X2,X3),f(X2,X3))) = f(f(f(X2,X3),f(X2,X3)),f(f(X1,X3),f(X1,f(f(X2,X3),f(X3,f(X4,f(X4,f(X2,X3)))))))),
inference(cp,[status(thm)],[t54532,t36557]) ).
cnf(t225962,plain,
f(X1,f(f(X2,X3),f(X2,X3))) = f(f(f(X2,X3),f(X2,X3)),f(f(X1,X3),f(X1,X3))),
inference(step,[status(thm)],[t54636,t36557]) ).
cnf(t225963,plain,
f(X1,f(f(X2,X3),f(X2,X3))) = f(f(f(X1,X3),f(X1,X3)),f(f(X2,X3),f(X2,X3))),
inference(step,[status(thm)],[t225962,t35219]) ).
cnf(t221829,plain,
f(f(f(X1,X2),f(X1,X2)),f(f(X3,X2),f(X3,X2))) = f(X1,f(f(X3,X2),f(X3,X2))),
inference(orient,[status(thm)],[t225963]) ).
cnf(t221841,plain,
f(X1,f(f(X2,X3),f(X2,X3))) = f(f(f(X2,X3),f(X2,X3)),f(f(X1,X3),f(X1,X3))),
inference(cp,[status(thm)],[t221829,t35219]) ).
cnf(t225964,plain,
f(X1,f(f(X2,X3),f(X2,X3))) = f(X2,f(f(X1,X3),f(X1,X3))),
inference(step,[status(thm)],[t221841,t221829]) ).
cnf(t223696,plain,
f(X1,f(f(X2,X3),f(X2,X3))) = f(X2,f(f(X1,X3),f(X1,X3))),
inference(orient,[status(thm)],[t225964]) ).
cnf(goal_0,negated_conjecture,
f(c,f(f(b,a),f(b,a))) != f(a,f(f(b,c),f(b,c))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
f(c,f(f(b,a),f(b,a))) != f(b,f(f(a,c),f(a,c))),
inference(rw,[status(thm)],[goal_0,t223696]) ).
cnf(g0_1,plain,
f(c,f(f(b,a),f(b,a))) != f(b,f(f(c,a),f(a,c))),
inference(rw,[status(thm)],[g0_0,t35219]) ).
cnf(g0_2,plain,
f(c,f(f(b,a),f(b,a))) != f(b,f(f(c,a),f(c,a))),
inference(rw,[status(thm)],[g0_1,t35219]) ).
cnf(g0_3,plain,
f(c,f(f(b,a),f(b,a))) != f(c,f(f(b,a),f(b,a))),
inference(rw,[status(thm)],[g0_2,t223696]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT076-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.42 % Computer : n014.cluster.edu
% 0.09/0.42 % Model : x86_64 x86_64
% 0.09/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.42 % Memory : 8046.5625MB
% 0.09/0.42 % OS : Linux 6.8.0-71-generic
% 0.09/0.43 % CPULimit : 300
% 0.09/0.43 % WCLimit : 300
% 0.09/0.43 % DateTime : Wed Sep 23 20:11:03 UTC 2026
% 0.09/0.43 % CPUTime :
% 0.09/0.43 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 87.42/13.19 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 87.42/13.19 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------