%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT077-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 : n004.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:19 PM UTC 2026
% Result : Unsatisfiable 141.66s 20.92s
% Output : CNFRefutation 141.66s
% 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(t305318,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)],[t305318]) ).
cnf(t305319,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)],[t305319]) ).
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(t305320,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)],[t305320]) ).
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(t305321,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)],[t305321]) ).
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(t305322,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(t305323,plain,
f(X1,X2) = f(f(X3,f(X1,X2)),f(f(X1,X2),f(X1,X2))),
inference(step,[status(thm)],[t305322,t932]) ).
cnf(t1074,plain,
f(f(X1,f(X2,X3)),f(f(X2,X3),f(X2,X3))) = f(X2,X3),
inference(orient,[status(thm)],[t305323]) ).
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(t305324,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)],[t305324]) ).
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(t305333,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(t305334,plain,
f(f(f(f(f(X1,X2),X1),X1),X2),f(X1,X2)) = X2,
inference(step,[status(thm)],[t305333,t1212]) ).
cnf(t1464,plain,
f(f(f(f(f(X1,X2),X1),X1),X2),f(X1,X2)) = X2,
inference(orient,[status(thm)],[t305334]) ).
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(t305335,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(t305336,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)],[t305335,t1464]) ).
cnf(t305337,plain,
X2 = f(f(X3,X2),f(X2,X2)),
inference(step,[status(thm)],[t305336,t1464]) ).
cnf(t1516,plain,
f(f(X1,X2),f(X2,X2)) = X2,
inference(orient,[status(thm)],[t305337]) ).
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(t305338,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)],[t305338]) ).
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(t305339,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)],[t305339]) ).
cnf(t305340,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)],[t305340]) ).
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(t305348,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)],[t305348]) ).
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(t305344,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)],[t305344]) ).
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(t305345,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(t305346,plain,
f(X1,f(X1,X1)) = f(f(X1,X1),f(f(X1,X1),f(X1,f(X1,X1)))),
inference(step,[status(thm)],[t305345,t1597]) ).
cnf(t305347,plain,
f(X1,f(X1,X1)) = f(f(X1,X1),X1),
inference(step,[status(thm)],[t305346,t1847]) ).
cnf(t1878,plain,
f(f(X1,X1),X1) = f(X1,f(X1,X1)),
inference(orient,[status(thm)],[t305347]) ).
cnf(t305371,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)],[t305371]) ).
cnf(t1584,plain,
X1 = f(f(f(X1,X1),X1),f(X1,f(f(X1,X1),X2))),
inference(cp,[status(thm)],[t420,t1572]) ).
cnf(t305354,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)],[t305354]) ).
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(t305349,plain,
f(X1,X2) = f(f(X2,f(X1,X2)),f(f(X2,X2),f(X1,X2))),
inference(step,[status(thm)],[t2009,t1768]) ).
cnf(t305350,plain,
f(X1,X2) = f(f(X2,f(X1,X2)),X2),
inference(step,[status(thm)],[t305349,t1993]) ).
cnf(t2076,plain,
f(f(X1,f(X2,X1)),X1) = f(X2,X1),
inference(orient,[status(thm)],[t305350]) ).
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(t305351,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)],[t305351]) ).
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(t305356,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)],[t305356]) ).
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(t305379,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)],[t305379]) ).
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(t305380,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)],[t305380]) ).
cnf(t5240,plain,
f(f(X1,X1),f(X1,X1)) = f(f(X1,X1),f(X1,X2)),
inference(cp,[status(thm)],[t5232,t1993]) ).
cnf(t305381,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)],[t305381]) ).
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(t305574,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(t305575,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)],[t305574,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)],[t305575]) ).
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(t305576,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(t305363,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)],[t305363]) ).
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(t305418,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)],[t305418]) ).
cnf(t305577,plain,
f(X1,X2) = f(X2,f(f(X1,X2),f(X2,X1))),
inference(step,[status(thm)],[t305576,t6317]) ).
cnf(t33986,plain,
f(X1,f(f(X2,X1),f(X1,X2))) = f(X2,X1),
inference(orient,[status(thm)],[t305577]) ).
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(t305352,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)],[t305352]) ).
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(t305353,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)],[t305353]) ).
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(t305396,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(t305383,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)],[t305383]) ).
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(t305382,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)],[t305382]) ).
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(t305397,plain,
X1 = f(f(X1,X2),f(X1,f(X1,X2))),
inference(step,[status(thm)],[t305396,t5627]) ).
cnf(t5662,plain,
f(f(X1,X2),f(X1,f(X1,X2))) = X1,
inference(orient,[status(thm)],[t305397]) ).
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(t305359,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)],[t305359]) ).
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(t305364,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)],[t305364]) ).
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(t305372,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(t305367,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(t305368,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)],[t305367,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)],[t305368]) ).
cnf(t305373,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)],[t305372,t4098]) ).
cnf(t305374,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)],[t305373,t3772]) ).
cnf(t305375,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)],[t305374,t1287]) ).
cnf(t305376,plain,
f(X1,X1) = f(f(f(f(X2,X1),f(X2,X1)),f(X2,X1)),X1),
inference(step,[status(thm)],[t305375,t1212]) ).
cnf(t305377,plain,
f(X1,X1) = f(f(f(X2,X1),f(f(X2,X1),f(X2,X1))),X1),
inference(step,[status(thm)],[t305376,t1878]) ).
cnf(t4877,plain,
f(f(f(X1,X2),f(f(X1,X2),f(X1,X2))),X2) = f(X2,X2),
inference(orient,[status(thm)],[t305377]) ).
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(t305429,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(t305430,plain,
f(f(X1,X2),f(X1,X2)) = f(f(X2,f(X2,X2)),f(X1,X2)),
inference(step,[status(thm)],[t305429,t1948]) ).
cnf(t7368,plain,
f(f(X1,X2),f(X1,X2)) = f(f(X2,f(X2,X2)),f(X1,X2)),
inference(orient,[status(thm)],[t305430]) ).
cnf(t305431,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)],[t305431]) ).
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(t305432,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)],[t305432]) ).
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(t305437,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)],[t305437]) ).
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(t305449,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(t305357,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)],[t305357]) ).
cnf(t305450,plain,
X1 = f(f(X1,X1),f(X3,f(f(X1,X2),f(X1,X2)))),
inference(step,[status(thm)],[t305449,t2498]) ).
cnf(t9911,plain,
f(f(X1,X1),f(X2,f(f(X1,X3),f(X1,X3)))) = X1,
inference(orient,[status(thm)],[t305450]) ).
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(t305454,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)],[t305454]) ).
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(t305579,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)],[t305579]) ).
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(t305580,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(t305581,plain,
f(f(X1,X2),f(X2,X1)) = f(f(X2,X1),f(X2,X1)),
inference(step,[status(thm)],[t305580,t33986]) ).
cnf(t34750,plain,
f(f(X1,X2),f(X2,X1)) = f(f(X2,X1),f(X2,X1)),
inference(orient,[status(thm)],[t305581]) ).
cnf(t305582,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(t305583,plain,
f(X1,X2) = f(X2,X1),
inference(step,[status(thm)],[t305582,t1911]) ).
cnf(t35219,plain,
f(X1,X2) = f(X2,X1),
inference(orient,[status(thm)],[t305583]) ).
cnf(t305605,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(t305606,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)],[t305605,t35219]) ).
cnf(t305607,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)],[t305606,t35219]) ).
cnf(t305608,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)],[t305607,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)],[t305608]) ).
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(t305390,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)],[t305390]) ).
cnf(t305617,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(t305618,plain,
f(X2,f(X1,f(f(X3,f(f(f(X1,X1),X2),X3)),X2))) = f(X2,X2),
inference(step,[status(thm)],[t305617,t35219]) ).
cnf(t305619,plain,
f(X2,f(X1,f(X2,f(X3,f(f(f(X1,X1),X2),X3))))) = f(X2,X2),
inference(step,[status(thm)],[t305618,t35219]) ).
cnf(t305620,plain,
f(X2,f(X1,f(X2,f(X3,f(X3,f(f(X1,X1),X2)))))) = f(X2,X2),
inference(step,[status(thm)],[t305619,t35219]) ).
cnf(t305621,plain,
f(X2,f(X1,f(X2,f(X3,f(X3,f(X2,f(X1,X1))))))) = f(X2,X2),
inference(step,[status(thm)],[t305620,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)],[t305621]) ).
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(t305387,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)],[t305387]) ).
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(t305400,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(t305401,plain,
f(X1,X1) = f(X1,f(f(X1,f(X2,X1)),f(X2,X2))),
inference(step,[status(thm)],[t305400,t1993]) ).
cnf(t5896,plain,
f(X1,f(f(X1,f(X2,X1)),f(X2,X2))) = f(X1,X1),
inference(orient,[status(thm)],[t305401]) ).
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(t305433,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(t305434,plain,
X1 = f(f(X3,f(f(X1,X2),f(X1,X2))),f(X1,X1)),
inference(step,[status(thm)],[t305433,t2498]) ).
cnf(t8104,plain,
f(f(X1,f(f(X2,X3),f(X2,X3))),f(X2,X2)) = X2,
inference(orient,[status(thm)],[t305434]) ).
cnf(t305325,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)],[t305325]) ).
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(t305504,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)],[t305504]) ).
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(t305543,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)],[t305543]) ).
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(t305545,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(t305546,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)],[t305545,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(t305435,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)],[t305435]) ).
cnf(t305389,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)],[t305389]) ).
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(t305438,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(t305439,plain,
f(X2,f(X2,X2)) = f(f(X1,X2),f(f(X1,X2),f(X1,X2))),
inference(step,[status(thm)],[t305438,t1516]) ).
cnf(t8824,plain,
f(f(X1,X2),f(f(X1,X2),f(X1,X2))) = f(X2,f(X2,X2)),
inference(orient,[status(thm)],[t305439]) ).
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(t305441,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(t305442,plain,
f(X2,f(X2,X2)) = f(f(X1,X1),X1),
inference(step,[status(thm)],[t305441,t5080]) ).
cnf(t305443,plain,
f(X2,f(X2,X2)) = f(X1,f(X1,X1)),
inference(step,[status(thm)],[t305442,t5580]) ).
cnf(t8971,plain,
f(X1,f(X1,X1)) = f(X2,f(X2,X2)),
inference(orient,[status(thm)],[t305443]) ).
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(t305547,plain,
X1 = f(f(X1,X1),f(X2,f(f(X1,X3),f(X1,X4)))),
inference(step,[status(thm)],[t305546,t10343]) ).
cnf(t25119,plain,
f(f(X1,X1),f(X2,f(f(X1,X3),f(X1,X4)))) = X1,
inference(orient,[status(thm)],[t305547]) ).
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(t305369,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)],[t305369]) ).
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(t305512,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(t305378,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)],[t305378]) ).
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(t305436,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)],[t305436]) ).
cnf(t305513,plain,
X1 = f(f(f(f(X1,X2),f(X1,X2)),X3),f(X1,X1)),
inference(step,[status(thm)],[t305512,t8484]) ).
cnf(t18547,plain,
f(f(f(f(X1,X2),f(X1,X2)),X3),f(X1,X1)) = X1,
inference(orient,[status(thm)],[t305513]) ).
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(t305514,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(t305515,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)],[t305514,t5580]) ).
cnf(t305516,plain,
X1 = f(f(X1,X1),f(f(f(X1,X2),f(X1,X2)),X3)),
inference(step,[status(thm)],[t305515,t10343]) ).
cnf(t18713,plain,
f(f(X1,X1),f(f(f(X1,X2),f(X1,X2)),X3)) = X1,
inference(orient,[status(thm)],[t305516]) ).
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(t305520,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)],[t305520]) ).
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(t305524,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)],[t305524]) ).
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(t305508,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)],[t305508]) ).
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(t305525,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)],[t305525]) ).
cnf(t35323,plain,
f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,X2)) = X2,
inference(rw,[status(thm)],[t21096]) ).
cnf(t305589,plain,
f(f(X2,X2),f(f(f(X1,X2),f(X2,X3)),X4)) = X2,
inference(step,[status(thm)],[t35323,t35219]) ).
cnf(t305590,plain,
f(f(X2,X2),f(X4,f(f(X1,X2),f(X2,X3)))) = X2,
inference(step,[status(thm)],[t305589,t35219]) ).
cnf(t35623,plain,
f(f(X1,X1),f(X2,f(f(X3,X1),f(X1,X4)))) = X1,
inference(orient,[status(thm)],[t305590]) ).
cnf(t35706,plain,
f(X1,X2) = f(f(f(X1,X2),f(X1,X2)),X2),
inference(cp,[status(thm)],[t25119,t35623]) ).
cnf(t305596,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)],[t305596]) ).
cnf(t305622,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(t305623,plain,
f(f(X1,X2),f(X2,f(X3,f(X3,f(X1,X2))))) = X2,
inference(step,[status(thm)],[t305622,t1516]) ).
cnf(t36557,plain,
f(f(X1,X2),f(X2,f(X3,f(X3,f(X1,X2))))) = X2,
inference(orient,[status(thm)],[t305623]) ).
cnf(t36589,plain,
X1 = f(f(X1,X2),f(X1,f(X3,f(X3,f(X2,X1))))),
inference(cp,[status(thm)],[t36557,t35219]) ).
cnf(t305627,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)],[t305627]) ).
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(t305631,plain,
f(X1,X2) = f(f(f(X1,X2),X1),f(f(X1,X3),f(X1,X2))),
inference(step,[status(thm)],[t36600,t35219]) ).
cnf(t305632,plain,
f(X1,X2) = f(f(X1,f(X1,X2)),f(f(X1,X3),f(X1,X2))),
inference(step,[status(thm)],[t305631,t35219]) ).
cnf(t305633,plain,
f(X1,X2) = f(f(X1,f(X1,X2)),f(f(X1,X2),f(X1,X3))),
inference(step,[status(thm)],[t305632,t35219]) ).
cnf(t37132,plain,
f(f(X1,f(X1,X2)),f(f(X1,X2),f(X1,X3))) = f(X1,X2),
inference(orient,[status(thm)],[t305633]) ).
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(t305634,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(t305635,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)],[t305634,t35219]) ).
cnf(t305636,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)],[t305635,t35219]) ).
cnf(t305637,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)],[t305636,t35219]) ).
cnf(t305638,plain,
X1 = f(f(X1,f(X1,X2)),f(f(X4,f(X1,X2)),X1)),
inference(step,[status(thm)],[t305637,t36936]) ).
cnf(t305639,plain,
X1 = f(f(X1,f(X1,X2)),f(X1,f(X4,f(X1,X2)))),
inference(step,[status(thm)],[t305638,t35219]) ).
cnf(t37305,plain,
f(f(X1,f(X1,X2)),f(X1,f(X3,f(X1,X2)))) = X1,
inference(orient,[status(thm)],[t305639]) ).
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(t305714,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)],[t305714]) ).
cnf(t42576,plain,
f(X1,X2) = f(f(f(X1,X2),f(X2,X3)),X1),
inference(cp,[status(thm)],[t36936,t42257]) ).
cnf(t305715,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)],[t305715]) ).
cnf(t42691,plain,
f(X1,f(X2,X3)) = f(X1,f(f(X1,f(X2,X3)),X2)),
inference(cp,[status(thm)],[t42603,t36936]) ).
cnf(t305716,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)],[t305716]) ).
cnf(t5837,plain,
f(f(f(X1,f(f(X2,X2),X1)),X2),X1) = f(f(f(X1,X1),f(f(f(X1,f(f(X2,X2),X1)),X2),X1)),f(f(X1,f(f(X2,X2),X1)),X2)),
inference(cp,[status(thm)],[t5739,t5823]) ).
cnf(t305402,plain,
f(X1,X1) = f(f(f(X1,X1),f(f(f(X1,f(f(X2,X2),X1)),X2),X1)),f(f(X1,f(f(X2,X2),X1)),X2)),
inference(step,[status(thm)],[t5837,t5823]) ).
cnf(t305403,plain,
f(X1,X1) = f(X1,f(f(X1,f(f(X2,X2),X1)),X2)),
inference(step,[status(thm)],[t305402,t1993]) ).
cnf(t5969,plain,
f(X1,f(f(X1,f(f(X2,X2),X1)),X2)) = f(X1,X1),
inference(orient,[status(thm)],[t305403]) ).
cnf(t35362,plain,
f(X1,f(f(X1,f(f(X2,X2),X1)),X2)) = f(X1,X1),
inference(rw,[status(thm)],[t5969]) ).
cnf(t305586,plain,
f(X1,f(X2,f(X1,f(f(X2,X2),X1)))) = f(X1,X1),
inference(step,[status(thm)],[t35362,t35219]) ).
cnf(t305587,plain,
f(X1,f(X2,f(X1,f(X1,f(X2,X2))))) = f(X1,X1),
inference(step,[status(thm)],[t305586,t35219]) ).
cnf(t35524,plain,
f(X1,f(X2,f(X1,f(X1,f(X2,X2))))) = f(X1,X1),
inference(orient,[status(thm)],[t305587]) ).
cnf(t42815,plain,
f(X1,f(X2,f(X2,f(X1,X1)))) = f(X1,f(X2,X2)),
inference(cp,[status(thm)],[t42808,t35524]) ).
cnf(t43146,plain,
f(X1,f(X2,f(X2,f(X1,X1)))) = f(X1,f(X2,X2)),
inference(orient,[status(thm)],[t42815]) ).
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(t305456,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)],[t305456]) ).
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(t305793,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(t305794,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)],[t305793,t35219]) ).
cnf(t305795,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)],[t305794,t5662]) ).
cnf(t305796,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)],[t305795,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)],[t305796]) ).
cnf(t54828,plain,
f(f(X1,f(X2,X3)),f(f(X2,X2),f(X2,X2))) = f(f(X1,f(X2,X3)),f(f(X2,X2),f(X1,f(X2,X2)))),
inference(cp,[status(thm)],[t43146,t54532]) ).
cnf(t305906,plain,
f(f(X1,f(X2,X3)),X2) = f(f(X1,f(X2,X3)),f(f(X2,X2),f(X1,f(X2,X2)))),
inference(step,[status(thm)],[t54828,t1516]) ).
cnf(t305907,plain,
f(X2,f(X1,f(X2,X3))) = f(f(X1,f(X2,X3)),f(f(X2,X2),f(X1,f(X2,X2)))),
inference(step,[status(thm)],[t305906,t35219]) ).
cnf(t87842,plain,
f(f(X1,f(X2,X3)),f(f(X2,X2),f(X1,f(X2,X2)))) = f(X2,f(X1,f(X2,X3))),
inference(orient,[status(thm)],[t305907]) ).
cnf(t35290,plain,
f(X1,f(f(X1,f(X2,X2)),f(f(X2,X3),X1))) = f(f(X2,X3),X1),
inference(rw,[status(thm)],[t34360]) ).
cnf(t305599,plain,
f(X1,f(f(X1,f(X2,X2)),f(X1,f(X2,X3)))) = f(f(X2,X3),X1),
inference(step,[status(thm)],[t35290,t35219]) ).
cnf(t305600,plain,
f(X1,f(f(X1,f(X2,X2)),f(X1,f(X2,X3)))) = f(X1,f(X2,X3)),
inference(step,[status(thm)],[t305599,t35219]) ).
cnf(t35931,plain,
f(X1,f(f(X1,f(X2,X2)),f(X1,f(X2,X3)))) = f(X1,f(X2,X3)),
inference(orient,[status(thm)],[t305600]) ).
cnf(t35971,plain,
f(X1,f(X2,f(f(X3,X2),f(X3,X2)))) = f(X1,f(f(X1,f(X2,X2)),f(X1,f(X3,X2)))),
inference(cp,[status(thm)],[t35931,t35785]) ).
cnf(t36068,plain,
f(X1,f(f(X1,f(X2,X3)),f(X1,f(X3,X3)))) = f(X1,f(X2,X3)),
inference(orient,[status(thm)],[t35971]) ).
cnf(t37354,plain,
X1 = f(f(X1,f(X1,f(X2,X2))),f(X1,f(X3,X2))),
inference(cp,[status(thm)],[t37305,t36068]) ).
cnf(t305640,plain,
X1 = f(f(X1,f(X3,X2)),f(X1,f(X1,f(X2,X2)))),
inference(step,[status(thm)],[t37354,t35219]) ).
cnf(t305641,plain,
X1 = f(f(X1,f(X2,X3)),f(X1,f(X1,f(X2,X2)))),
inference(step,[status(thm)],[t305640,t35219]) ).
cnf(t37646,plain,
f(f(X1,f(X2,X3)),f(X1,f(X1,f(X2,X2)))) = X1,
inference(orient,[status(thm)],[t305641]) ).
cnf(t54537,plain,
f(X1,f(f(X2,f(X2,f(X2,X2))),f(X2,f(X2,f(X2,X2))))) = f(X2,f(f(X1,f(f(X2,f(X2,f(X2,X2))),X3)),f(X1,f(f(X2,f(X2,f(X2,X2))),X3)))),
inference(cp,[status(thm)],[t54532,t37646]) ).
cnf(t305969,plain,
f(X1,X2) = f(X2,f(f(X1,f(f(X2,f(X2,f(X2,X2))),X3)),f(X1,f(f(X2,f(X2,f(X2,X2))),X3)))),
inference(step,[status(thm)],[t54537,t37646]) ).
cnf(t35226,plain,
f(X1,f(X2,f(X2,X2))) = f(X1,X1),
inference(cp,[status(thm)],[t35219,t8484]) ).
cnf(t35373,plain,
f(X1,f(X2,f(X2,X2))) = f(X1,X1),
inference(orient,[status(thm)],[t35226]) ).
cnf(t305970,plain,
f(X1,X2) = f(X2,f(f(X1,f(f(X2,f(X2,f(X2,X2))),X3)),f(c,f(c,c)))),
inference(step,[status(thm)],[t305969,t35373]) ).
cnf(t305971,plain,
f(X1,X2) = f(X2,f(f(c,f(c,c)),f(X1,f(f(X2,f(X2,f(X2,X2))),X3)))),
inference(step,[status(thm)],[t305970,t35219]) ).
cnf(t305972,plain,
f(X1,X2) = f(X2,f(f(c,f(c,c)),f(X1,f(X3,f(X2,f(X2,f(X2,X2))))))),
inference(step,[status(thm)],[t305971,t35219]) ).
cnf(t305973,plain,
f(X1,X2) = f(X2,f(f(c,f(c,c)),f(X1,f(X3,f(X2,X2))))),
inference(step,[status(thm)],[t305972,t2041]) ).
cnf(t107337,plain,
f(X1,f(f(c,f(c,c)),f(X2,f(X3,f(X1,X1))))) = f(X2,X1),
inference(orient,[status(thm)],[t305973]) ).
cnf(t107431,plain,
f(X1,X2) = f(X2,f(f(X3,f(X3,X3)),f(X1,f(X4,f(X2,X2))))),
inference(cp,[status(thm)],[t107337,t8971]) ).
cnf(t121194,plain,
f(X1,f(f(X2,f(X2,X2)),f(X3,f(X4,f(X1,X1))))) = f(X3,X1),
inference(orient,[status(thm)],[t107431]) ).
cnf(t43167,plain,
f(f(f(X1,X2),f(X1,X3)),f(f(X1,X1),f(X1,X1))) = f(f(f(X1,X2),f(X1,X3)),f(f(X1,X1),X1)),
inference(cp,[status(thm)],[t43146,t25119]) ).
cnf(t305755,plain,
f(f(f(X1,X1),f(X1,X1)),f(f(X1,X2),f(X1,X3))) = f(f(f(X1,X2),f(X1,X3)),f(f(X1,X1),X1)),
inference(step,[status(thm)],[t43167,t35219]) ).
cnf(t305756,plain,
f(X1,f(f(X1,X2),f(X1,X3))) = f(f(f(X1,X2),f(X1,X3)),f(f(X1,X1),X1)),
inference(step,[status(thm)],[t305755,t1516]) ).
cnf(t305757,plain,
f(X1,f(f(X1,X2),f(X1,X3))) = f(f(f(X1,X1),X1),f(f(X1,X2),f(X1,X3))),
inference(step,[status(thm)],[t305756,t35219]) ).
cnf(t305758,plain,
f(X1,f(f(X1,X2),f(X1,X3))) = f(f(X1,f(X1,X1)),f(f(X1,X2),f(X1,X3))),
inference(step,[status(thm)],[t305757,t1878]) ).
cnf(t49805,plain,
f(f(X1,f(X1,X1)),f(f(X1,X2),f(X1,X3))) = f(X1,f(f(X1,X2),f(X1,X3))),
inference(orient,[status(thm)],[t305758]) ).
cnf(t121234,plain,
f(f(X1,X2),X3) = f(X3,f(X1,f(f(X1,X2),f(X1,f(X3,X3))))),
inference(cp,[status(thm)],[t121194,t49805]) ).
cnf(t306042,plain,
f(X3,f(X1,X2)) = f(X3,f(X1,f(f(X1,X2),f(X1,f(X3,X3))))),
inference(step,[status(thm)],[t121234,t35219]) ).
cnf(t122556,plain,
f(X1,f(X2,f(f(X2,X3),f(X2,f(X1,X1))))) = f(X1,f(X2,X3)),
inference(orient,[status(thm)],[t306042]) ).
cnf(t37674,plain,
X1 = f(f(X1,f(X2,X3)),f(X1,f(X1,f(X3,X3)))),
inference(cp,[status(thm)],[t37646,t35785]) ).
cnf(t38271,plain,
f(f(X1,f(X2,X3)),f(X1,f(X1,f(X3,X3)))) = X1,
inference(orient,[status(thm)],[t37674]) ).
cnf(t54843,plain,
X1 = f(f(X1,f(X2,f(X3,X3))),f(X1,f(X1,f(f(f(X2,f(X3,X4)),f(X2,f(X3,X4))),f(f(X2,f(X3,X4)),f(X2,f(X3,X4))))))),
inference(cp,[status(thm)],[t38271,t54532]) ).
cnf(t305849,plain,
X1 = f(f(X1,f(X2,f(X3,X3))),f(X1,f(X1,f(X2,f(X3,X4))))),
inference(step,[status(thm)],[t54843,t932]) ).
cnf(t66766,plain,
f(f(X1,f(X2,f(X3,X3))),f(X1,f(X1,f(X2,f(X3,X4))))) = X1,
inference(orient,[status(thm)],[t305849]) ).
cnf(t67028,plain,
X1 = f(f(X1,f(f(X2,X2),f(X3,X3))),f(X1,f(X1,X2))),
inference(cp,[status(thm)],[t66766,t25119]) ).
cnf(t305853,plain,
X1 = f(f(X1,f(X1,X2)),f(X1,f(f(X2,X2),f(X3,X3)))),
inference(step,[status(thm)],[t67028,t35219]) ).
cnf(t67837,plain,
f(f(X1,f(X1,X2)),f(X1,f(f(X2,X2),f(X3,X3)))) = X1,
inference(orient,[status(thm)],[t305853]) ).
cnf(t44098,plain,
f(X1,f(X2,f(f(X3,X2),f(X3,X2)))) = f(X1,f(f(X1,f(X3,X2)),f(X4,f(f(f(X3,X2),f(X3,X2)),f(f(X3,X2),f(X3,X2)))))),
inference(cp,[status(thm)],[t44035,t35785]) ).
cnf(t305719,plain,
f(X1,f(X3,X2)) = f(X1,f(f(X1,f(X3,X2)),f(X4,f(f(f(X3,X2),f(X3,X2)),f(f(X3,X2),f(X3,X2)))))),
inference(step,[status(thm)],[t44098,t35785]) ).
cnf(t305720,plain,
f(X1,f(X2,X3)) = f(X1,f(f(X1,f(X3,X2)),f(X4,f(f(f(X3,X2),f(X3,X2)),f(f(X3,X2),f(X3,X2)))))),
inference(step,[status(thm)],[t305719,t35219]) ).
cnf(t305721,plain,
f(X1,f(X2,X3)) = f(X1,f(f(X1,f(X2,X3)),f(X4,f(f(f(X3,X2),f(X3,X2)),f(f(X3,X2),f(X3,X2)))))),
inference(step,[status(thm)],[t305720,t35219]) ).
cnf(t305722,plain,
f(X1,f(X2,X3)) = f(X1,f(f(X1,f(X2,X3)),f(X4,f(X3,X2)))),
inference(step,[status(thm)],[t305721,t932]) ).
cnf(t305723,plain,
f(X1,f(X2,X3)) = f(X1,f(f(X1,f(X2,X3)),f(X4,f(X2,X3)))),
inference(step,[status(thm)],[t305722,t35219]) ).
cnf(t44679,plain,
f(X1,f(f(X1,f(X2,X3)),f(X4,f(X2,X3)))) = f(X1,f(X2,X3)),
inference(orient,[status(thm)],[t305723]) ).
cnf(t68067,plain,
X1 = f(f(X1,f(X1,X2)),f(X1,f(f(X2,X2),f(X3,X4)))),
inference(cp,[status(thm)],[t67837,t44679]) ).
cnf(t68981,plain,
f(f(X1,f(X1,X2)),f(X1,f(f(X2,X2),f(X3,X4)))) = X1,
inference(orient,[status(thm)],[t68067]) ).
cnf(t42633,plain,
f(f(X1,f(X2,X3)),f(X1,f(X1,f(X2,X2)))) = f(f(X1,f(X2,X3)),f(X1,f(f(X1,f(X1,f(X2,X2))),X4))),
inference(cp,[status(thm)],[t42603,t37646]) ).
cnf(t305814,plain,
X1 = f(f(X1,f(X2,X3)),f(X1,f(f(X1,f(X1,f(X2,X2))),X4))),
inference(step,[status(thm)],[t42633,t37646]) ).
cnf(t305815,plain,
X1 = f(f(X1,f(X2,X3)),f(X1,f(X4,f(X1,f(X1,f(X2,X2)))))),
inference(step,[status(thm)],[t305814,t35219]) ).
cnf(t58336,plain,
f(f(X1,f(X2,X3)),f(X1,f(X4,f(X1,f(X1,f(X2,X2)))))) = X1,
inference(orient,[status(thm)],[t305815]) ).
cnf(t69263,plain,
X1 = f(f(X1,f(X1,f(X2,f(X3,f(X2,f(X2,f(X3,X3))))))),f(X1,f(X2,f(X4,Y4)))),
inference(cp,[status(thm)],[t68981,t58336]) ).
cnf(t305854,plain,
X1 = f(f(X1,f(X1,f(X2,X2))),f(X1,f(X2,f(X4,Y4)))),
inference(step,[status(thm)],[t69263,t35524]) ).
cnf(t69694,plain,
f(f(X1,f(X1,f(X2,X2))),f(X1,f(X2,f(X3,X4)))) = X1,
inference(orient,[status(thm)],[t305854]) ).
cnf(t122816,plain,
f(f(X1,f(X1,f(X1,X1))),f(X2,X3)) = f(f(X1,f(X1,f(X1,X1))),f(X2,f(f(X2,X3),f(X2,X1)))),
inference(cp,[status(thm)],[t122556,t69694]) ).
cnf(t306049,plain,
f(f(X2,X3),f(X1,f(X1,f(X1,X1)))) = f(f(X1,f(X1,f(X1,X1))),f(X2,f(f(X2,X3),f(X2,X1)))),
inference(step,[status(thm)],[t122816,t35219]) ).
cnf(t306050,plain,
f(f(X2,X3),f(X1,X1)) = f(f(X1,f(X1,f(X1,X1))),f(X2,f(f(X2,X3),f(X2,X1)))),
inference(step,[status(thm)],[t306049,t2041]) ).
cnf(t306051,plain,
f(f(X1,X1),f(X2,X3)) = f(f(X1,f(X1,f(X1,X1))),f(X2,f(f(X2,X3),f(X2,X1)))),
inference(step,[status(thm)],[t306050,t35219]) ).
cnf(t306052,plain,
f(f(X1,X1),f(X2,X3)) = f(f(X1,X1),f(X2,f(f(X2,X3),f(X2,X1)))),
inference(step,[status(thm)],[t306051,t2041]) ).
cnf(t306053,plain,
f(f(X1,X1),f(X2,X3)) = f(f(X1,X1),f(X2,f(f(X2,X1),f(X2,X3)))),
inference(step,[status(thm)],[t306052,t35219]) ).
cnf(t306054,plain,
f(f(X1,X1),f(X2,X3)) = f(f(X1,X1),f(X2,f(f(X1,X2),f(X2,X3)))),
inference(step,[status(thm)],[t306053,t35219]) ).
cnf(t124655,plain,
f(f(X1,X1),f(X2,f(f(X1,X2),f(X2,X3)))) = f(f(X1,X1),f(X2,X3)),
inference(orient,[status(thm)],[t306054]) ).
cnf(t8424,plain,
f(X1,f(X2,X2)) = f(f(X2,X3),f(f(X1,f(X2,X2)),f(f(X1,f(X2,X2)),f(f(X2,X3),f(X2,X3))))),
inference(cp,[status(thm)],[t5662,t8343]) ).
cnf(t305455,plain,
f(X1,f(X2,X2)) = f(f(X2,X3),f(f(X1,f(X2,X2)),f(X2,X3))),
inference(step,[status(thm)],[t8424,t8343]) ).
cnf(t10770,plain,
f(f(X1,X2),f(f(X3,f(X1,X1)),f(X1,X2))) = f(X3,f(X1,X1)),
inference(orient,[status(thm)],[t305455]) ).
cnf(t10907,plain,
f(f(X1,X2),f(f(X3,f(X1,X1)),f(X1,X2))) = f(f(X1,X2),f(f(X1,X2),f(X3,f(X1,X1)))),
inference(cp,[status(thm)],[t5427,t10770]) ).
cnf(t305466,plain,
f(X3,f(X1,X1)) = f(f(X1,X2),f(f(X1,X2),f(X3,f(X1,X1)))),
inference(step,[status(thm)],[t10907,t10770]) ).
cnf(t12047,plain,
f(f(X1,X2),f(f(X1,X2),f(X3,f(X1,X1)))) = f(X3,f(X1,X1)),
inference(orient,[status(thm)],[t305466]) ).
cnf(t42695,plain,
f(X1,f(X2,X3)) = f(X1,f(f(X1,f(X2,X3)),f(X4,f(X2,X2)))),
inference(cp,[status(thm)],[t42603,t12047]) ).
cnf(t44307,plain,
f(X1,f(f(X1,f(X2,X3)),f(X4,f(X2,X2)))) = f(X1,f(X2,X3)),
inference(orient,[status(thm)],[t42695]) ).
cnf(t70286,plain,
f(X1,f(X2,f(X3,X4))) = f(X1,f(f(X1,f(X2,f(X3,X4))),f(Y4,f(Y4,f(f(X1,f(X1,f(X2,X2))),f(X1,f(X2,f(X3,X4)))))))),
inference(cp,[status(thm)],[t36557,t69694]) ).
cnf(t305919,plain,
f(X1,f(X2,f(X3,X4))) = f(X1,f(f(X1,f(X2,f(X3,X4))),f(Y4,f(Y4,X1)))),
inference(step,[status(thm)],[t70286,t69694]) ).
cnf(t305920,plain,
f(X1,f(X2,f(X3,X4))) = f(X1,f(f(X1,f(X2,f(X3,X4))),f(Y4,f(X1,Y4)))),
inference(step,[status(thm)],[t305919,t35219]) ).
cnf(t305921,plain,
f(X1,f(X2,f(X3,X4))) = f(X1,f(f(Y4,f(X1,Y4)),f(X1,f(X2,f(X3,X4))))),
inference(step,[status(thm)],[t305920,t35219]) ).
cnf(t90119,plain,
f(X1,f(f(X2,f(X1,X2)),f(X1,f(X3,f(X4,Y4))))) = f(X1,f(X3,f(X4,Y4))),
inference(orient,[status(thm)],[t305921]) ).
cnf(t35358,plain,
f(X1,f(f(X1,f(X2,X1)),f(X2,X2))) = f(X1,X1),
inference(rw,[status(thm)],[t5896]) ).
cnf(t305584,plain,
f(X1,f(f(X2,X2),f(X1,f(X2,X1)))) = f(X1,X1),
inference(step,[status(thm)],[t35358,t35219]) ).
cnf(t305585,plain,
f(X1,f(f(X2,X2),f(X1,f(X1,X2)))) = f(X1,X1),
inference(step,[status(thm)],[t305584,t35219]) ).
cnf(t35476,plain,
f(X1,f(f(X2,X2),f(X1,f(X1,X2)))) = f(X1,X1),
inference(orient,[status(thm)],[t305585]) ).
cnf(t42819,plain,
f(f(X1,X1),f(X2,f(X2,X1))) = f(f(X1,X1),f(X2,X2)),
inference(cp,[status(thm)],[t42808,t35476]) ).
cnf(t305718,plain,
f(f(X1,X1),f(X2,f(X1,X2))) = f(f(X1,X1),f(X2,X2)),
inference(step,[status(thm)],[t42819,t35219]) ).
cnf(t43251,plain,
f(f(X1,X1),f(X2,f(X1,X2))) = f(f(X1,X1),f(X2,X2)),
inference(orient,[status(thm)],[t305718]) ).
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(t306371,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(t306372,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)],[t306371,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)],[t306372]) ).
cnf(t223108,plain,
f(f(f(f(X1,X2),f(X1,X2)),f(f(X1,X2),f(X1,X2))),f(X3,X3)) = f(f(X1,f(f(X1,X2),f(X1,X2))),f(X3,f(f(f(X1,X2),f(X1,X2)),X3))),
inference(cp,[status(thm)],[t43251,t221829]) ).
cnf(t306374,plain,
f(f(X3,X3),f(f(f(X1,X2),f(X1,X2)),f(f(X1,X2),f(X1,X2)))) = f(f(X1,f(f(X1,X2),f(X1,X2))),f(X3,f(f(f(X1,X2),f(X1,X2)),X3))),
inference(step,[status(thm)],[t223108,t35219]) ).
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(t306373,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)],[t306373]) ).
cnf(t306375,plain,
f(f(X1,X2),f(f(f(X3,X3),f(X1,X2)),f(f(X3,X3),f(X1,X2)))) = f(f(X1,f(f(X1,X2),f(X1,X2))),f(X3,f(f(f(X1,X2),f(X1,X2)),X3))),
inference(step,[status(thm)],[t306374,t223696]) ).
cnf(t37307,plain,
X1 = f(f(X1,X2),f(X1,f(X3,f(X1,f(X1,X2))))),
inference(cp,[status(thm)],[t37305,t5427]) ).
cnf(t37497,plain,
f(f(X1,X2),f(X1,f(X3,f(X1,f(X1,X2))))) = X1,
inference(orient,[status(thm)],[t37307]) ).
cnf(t42648,plain,
f(f(X1,X2),f(X1,f(X3,f(X1,f(X1,X2))))) = f(f(X1,X2),f(X1,f(f(X1,f(X3,f(X1,f(X1,X2)))),X4))),
inference(cp,[status(thm)],[t42603,t37497]) ).
cnf(t305839,plain,
X1 = f(f(X1,X2),f(X1,f(f(X1,f(X3,f(X1,f(X1,X2)))),X4))),
inference(step,[status(thm)],[t42648,t37497]) ).
cnf(t305840,plain,
X1 = f(f(X1,X2),f(X1,f(X4,f(X1,f(X3,f(X1,f(X1,X2))))))),
inference(step,[status(thm)],[t305839,t35219]) ).
cnf(t65142,plain,
f(f(X1,X2),f(X1,f(X3,f(X1,f(X4,f(X1,f(X1,X2))))))) = X1,
inference(orient,[status(thm)],[t305840]) ).
cnf(t65526,plain,
f(X1,f(X2,f(X1,f(X3,f(X1,f(X1,f(X2,X2))))))) = f(X1,X1),
inference(cp,[status(thm)],[t35931,t65142]) ).
cnf(t65621,plain,
f(X1,f(X2,f(X1,f(X3,f(X1,f(X1,f(X2,X2))))))) = f(X1,X1),
inference(orient,[status(thm)],[t65526]) ).
cnf(t65687,plain,
f(X1,f(X2,f(X3,f(X2,f(X2,f(X1,X1)))))) = f(f(X2,X2),f(f(X1,f(X2,f(X3,f(X2,f(X2,f(X1,X1)))))),f(X1,f(X2,f(X3,f(X2,f(X2,f(X1,X1)))))))),
inference(cp,[status(thm)],[t1516,t65621]) ).
cnf(t305841,plain,
f(X1,f(X2,f(X3,f(X2,f(X2,f(X1,X1)))))) = f(X1,f(X2,X2)),
inference(step,[status(thm)],[t65687,t54532]) ).
cnf(t65808,plain,
f(X1,f(X2,f(X3,f(X2,f(X2,f(X1,X1)))))) = f(X1,f(X2,X2)),
inference(orient,[status(thm)],[t305841]) ).
cnf(t65882,plain,
f(f(X1,f(X2,f(X1,f(X1,f(X2,X2))))),f(X3,X3)) = f(f(X1,f(X2,f(X1,f(X1,f(X2,X2))))),f(X3,f(X4,f(X3,f(X3,X1))))),
inference(cp,[status(thm)],[t65808,t58336]) ).
cnf(t305842,plain,
f(f(X3,X3),f(X1,f(X2,f(X1,f(X1,f(X2,X2)))))) = f(f(X1,f(X2,f(X1,f(X1,f(X2,X2))))),f(X3,f(X4,f(X3,f(X3,X1))))),
inference(step,[status(thm)],[t65882,t35219]) ).
cnf(t305843,plain,
f(f(X3,X3),f(X1,X1)) = f(f(X1,f(X2,f(X1,f(X1,f(X2,X2))))),f(X3,f(X4,f(X3,f(X3,X1))))),
inference(step,[status(thm)],[t305842,t35524]) ).
cnf(t305844,plain,
f(f(X1,X1),f(X3,X3)) = f(f(X1,f(X2,f(X1,f(X1,f(X2,X2))))),f(X3,f(X4,f(X3,f(X3,X1))))),
inference(step,[status(thm)],[t305843,t35219]) ).
cnf(t305845,plain,
f(f(X1,X1),f(X3,X3)) = f(f(X3,f(X4,f(X3,f(X3,X1)))),f(X1,f(X2,f(X1,f(X1,f(X2,X2)))))),
inference(step,[status(thm)],[t305844,t35219]) ).
cnf(t305846,plain,
f(f(X1,X1),f(X3,X3)) = f(f(X3,f(X4,f(X3,f(X1,X3)))),f(X1,f(X2,f(X1,f(X1,f(X2,X2)))))),
inference(step,[status(thm)],[t305845,t35219]) ).
cnf(t305847,plain,
f(f(X1,X1),f(X3,X3)) = f(f(X3,f(X4,f(X3,f(X1,X3)))),f(X1,X1)),
inference(step,[status(thm)],[t305846,t35524]) ).
cnf(t305848,plain,
f(f(X1,X1),f(X3,X3)) = f(f(X1,X1),f(X3,f(X4,f(X3,f(X1,X3))))),
inference(step,[status(thm)],[t305847,t35219]) ).
cnf(t65999,plain,
f(f(X1,X1),f(X2,f(X3,f(X2,f(X1,X2))))) = f(f(X1,X1),f(X2,X2)),
inference(orient,[status(thm)],[t305848]) ).
cnf(t25199,plain,
f(X1,X2) = f(f(f(X1,X2),f(X1,X2)),f(X3,f(X1,f(f(X1,X2),X4)))),
inference(cp,[status(thm)],[t25119,t5662]) ).
cnf(t305927,plain,
f(X1,X2) = f(f(f(X1,X2),f(X1,X2)),f(X3,f(X1,f(X4,f(X1,X2))))),
inference(step,[status(thm)],[t25199,t35219]) ).
cnf(t92380,plain,
f(f(f(X1,X2),f(X1,X2)),f(X3,f(X1,f(X4,f(X1,X2))))) = f(X1,X2),
inference(orient,[status(thm)],[t305927]) ).
cnf(t93312,plain,
f(f(X1,X1),f(f(X2,f(X1,X3)),f(X2,f(X1,X3)))) = f(f(X1,X1),f(f(X2,f(X1,X3)),f(X1,X3))),
inference(cp,[status(thm)],[t65999,t92380]) ).
cnf(t305928,plain,
f(X2,f(X1,X1)) = f(f(X1,X1),f(f(X2,f(X1,X3)),f(X1,X3))),
inference(step,[status(thm)],[t93312,t54532]) ).
cnf(t305929,plain,
f(X2,f(X1,X1)) = f(f(X1,X1),f(f(X1,X3),f(X2,f(X1,X3)))),
inference(step,[status(thm)],[t305928,t35219]) ).
cnf(t93419,plain,
f(f(X1,X1),f(f(X1,X2),f(X3,f(X1,X2)))) = f(X3,f(X1,X1)),
inference(orient,[status(thm)],[t305929]) ).
cnf(t93424,plain,
f(X1,f(f(X2,f(X2,f(X2,X2))),f(X2,f(X2,f(X2,X2))))) = f(X2,f(f(f(X2,f(X2,f(X2,X2))),X3),f(X1,f(f(X2,f(X2,f(X2,X2))),X3)))),
inference(cp,[status(thm)],[t93419,t69694]) ).
cnf(t305930,plain,
f(X1,X2) = f(X2,f(f(f(X2,f(X2,f(X2,X2))),X3),f(X1,f(f(X2,f(X2,f(X2,X2))),X3)))),
inference(step,[status(thm)],[t93424,t37646]) ).
cnf(t305931,plain,
f(X1,X2) = f(X2,f(f(X3,f(X2,f(X2,f(X2,X2)))),f(X1,f(f(X2,f(X2,f(X2,X2))),X3)))),
inference(step,[status(thm)],[t305930,t35219]) ).
cnf(t305932,plain,
f(X1,X2) = f(X2,f(f(X3,f(X2,X2)),f(X1,f(f(X2,f(X2,f(X2,X2))),X3)))),
inference(step,[status(thm)],[t305931,t2041]) ).
cnf(t305933,plain,
f(X1,X2) = f(X2,f(f(X3,f(X2,X2)),f(X1,f(X3,f(X2,f(X2,f(X2,X2))))))),
inference(step,[status(thm)],[t305932,t35219]) ).
cnf(t305934,plain,
f(X1,X2) = f(X2,f(f(X3,f(X2,X2)),f(X1,f(X3,f(X2,X2))))),
inference(step,[status(thm)],[t305933,t2041]) ).
cnf(t94068,plain,
f(X1,f(f(X2,f(X1,X1)),f(X3,f(X2,f(X1,X1))))) = f(X3,X1),
inference(orient,[status(thm)],[t305934]) ).
cnf(t94138,plain,
f(X1,f(f(X2,X3),f(X3,X4))) = f(f(f(X2,X3),f(X3,X4)),f(X3,f(X1,f(f(X3,X3),f(f(f(X2,X3),f(X3,X4)),f(f(X2,X3),f(X3,X4))))))),
inference(cp,[status(thm)],[t94068,t35623]) ).
cnf(t305939,plain,
f(X1,f(f(X2,X3),f(X3,X4))) = f(f(f(X2,X3),f(X3,X4)),f(X3,f(X1,f(f(X2,X3),f(X3,X3))))),
inference(step,[status(thm)],[t94138,t54532]) ).
cnf(t305940,plain,
f(X1,f(f(X2,X3),f(X3,X4))) = f(f(f(X2,X3),f(X3,X4)),f(X3,f(X1,X3))),
inference(step,[status(thm)],[t305939,t1516]) ).
cnf(t305941,plain,
f(X1,f(f(X2,X3),f(X3,X4))) = f(f(X3,f(X1,X3)),f(f(X2,X3),f(X3,X4))),
inference(step,[status(thm)],[t305940,t35219]) ).
cnf(t96077,plain,
f(f(X1,f(X2,X1)),f(f(X3,X1),f(X1,X4))) = f(X2,f(f(X3,X1),f(X1,X4))),
inference(orient,[status(thm)],[t305941]) ).
cnf(t121228,plain,
f(f(X1,X2),X3) = f(X3,f(X2,f(f(X1,X2),f(X2,f(X3,X3))))),
inference(cp,[status(thm)],[t121194,t96077]) ).
cnf(t306041,plain,
f(X3,f(X1,X2)) = f(X3,f(X2,f(f(X1,X2),f(X2,f(X3,X3))))),
inference(step,[status(thm)],[t121228,t35219]) ).
cnf(t122017,plain,
f(X1,f(X2,f(f(X3,X2),f(X2,f(X1,X1))))) = f(X1,f(X3,X2)),
inference(orient,[status(thm)],[t306041]) ).
cnf(t122310,plain,
f(f(X1,f(X1,f(X1,X1))),f(X2,X3)) = f(f(X1,f(X1,f(X1,X1))),f(X3,f(f(X2,X3),f(X3,X1)))),
inference(cp,[status(thm)],[t122017,t69694]) ).
cnf(t306043,plain,
f(f(X2,X3),f(X1,f(X1,f(X1,X1)))) = f(f(X1,f(X1,f(X1,X1))),f(X3,f(f(X2,X3),f(X3,X1)))),
inference(step,[status(thm)],[t122310,t35219]) ).
cnf(t306044,plain,
f(f(X2,X3),f(X1,X1)) = f(f(X1,f(X1,f(X1,X1))),f(X3,f(f(X2,X3),f(X3,X1)))),
inference(step,[status(thm)],[t306043,t2041]) ).
cnf(t306045,plain,
f(f(X1,X1),f(X2,X3)) = f(f(X1,f(X1,f(X1,X1))),f(X3,f(f(X2,X3),f(X3,X1)))),
inference(step,[status(thm)],[t306044,t35219]) ).
cnf(t306046,plain,
f(f(X1,X1),f(X2,X3)) = f(f(X1,X1),f(X3,f(f(X2,X3),f(X3,X1)))),
inference(step,[status(thm)],[t306045,t2041]) ).
cnf(t306047,plain,
f(f(X1,X1),f(X2,X3)) = f(f(X1,X1),f(X3,f(f(X2,X3),f(X1,X3)))),
inference(step,[status(thm)],[t306046,t35219]) ).
cnf(t306048,plain,
f(f(X1,X1),f(X2,X3)) = f(f(X1,X1),f(X3,f(f(X1,X3),f(X2,X3)))),
inference(step,[status(thm)],[t306047,t35219]) ).
cnf(t123039,plain,
f(f(X1,X1),f(X2,f(f(X1,X2),f(X3,X2)))) = f(f(X1,X1),f(X3,X2)),
inference(orient,[status(thm)],[t306048]) ).
cnf(t42647,plain,
f(f(X1,X2),f(X1,f(X3,f(X3,f(X1,X2))))) = f(f(X1,X2),f(X1,f(f(X1,f(X3,f(X3,f(X1,X2)))),X4))),
inference(cp,[status(thm)],[t42603,t36936]) ).
cnf(t305822,plain,
X1 = f(f(X1,X2),f(X1,f(f(X1,f(X3,f(X3,f(X1,X2)))),X4))),
inference(step,[status(thm)],[t42647,t36936]) ).
cnf(t305823,plain,
X1 = f(f(X1,X2),f(X1,f(X4,f(X1,f(X3,f(X3,f(X1,X2))))))),
inference(step,[status(thm)],[t305822,t35219]) ).
cnf(t60406,plain,
f(f(X1,X2),f(X1,f(X3,f(X1,f(X4,f(X4,f(X1,X2))))))) = X1,
inference(orient,[status(thm)],[t305823]) ).
cnf(t60519,plain,
f(X1,X2) = f(f(f(X1,X2),f(X2,X3)),f(f(X1,X2),f(X4,X1))),
inference(cp,[status(thm)],[t60406,t42257]) ).
cnf(t305824,plain,
f(X1,X2) = f(f(f(X1,X2),f(X2,X3)),f(f(X1,X2),f(X1,X4))),
inference(step,[status(thm)],[t60519,t35219]) ).
cnf(t305825,plain,
f(X1,X2) = f(f(f(X1,X2),f(X1,X4)),f(f(X1,X2),f(X2,X3))),
inference(step,[status(thm)],[t305824,t35219]) ).
cnf(t60900,plain,
f(f(f(X1,X2),f(X1,X3)),f(f(X1,X2),f(X2,X4))) = f(X1,X2),
inference(orient,[status(thm)],[t305825]) ).
cnf(t61097,plain,
f(X1,X2) = f(f(f(X1,X2),f(X1,X3)),X2),
inference(cp,[status(thm)],[t60900,t1516]) ).
cnf(t305826,plain,
f(X1,X2) = f(X2,f(f(X1,X2),f(X1,X3))),
inference(step,[status(thm)],[t61097,t35219]) ).
cnf(t61574,plain,
f(X1,f(f(X2,X1),f(X2,X3))) = f(X2,X1),
inference(orient,[status(thm)],[t305826]) ).
cnf(t305384,plain,
f(f(X1,X2),f(X2,f(X1,X2))) = X2,
inference(step,[status(thm)],[t2135,t5580]) ).
cnf(t5615,plain,
f(f(X1,X2),f(X2,f(X1,X2))) = X2,
inference(rw,[status(thm)],[t305384]) ).
cnf(t5718,plain,
f(f(X1,X2),f(X2,f(X1,X2))) = X2,
inference(orient,[status(thm)],[t5615]) ).
cnf(t35698,plain,
f(X1,f(f(X2,X3),f(X3,X4))) = f(X3,f(f(X1,f(f(X2,X3),f(X3,X4))),f(f(X3,X3),f(X1,f(f(X2,X3),f(X3,X4)))))),
inference(cp,[status(thm)],[t5718,t35623]) ).
cnf(t305753,plain,
f(X1,f(f(X2,X3),f(X3,X4))) = f(X3,f(f(X1,f(f(X2,X3),f(X3,X4))),X3)),
inference(step,[status(thm)],[t35698,t35623]) ).
cnf(t305754,plain,
f(X1,f(f(X2,X3),f(X3,X4))) = f(X3,f(X3,f(X1,f(f(X2,X3),f(X3,X4))))),
inference(step,[status(thm)],[t305753,t35219]) ).
cnf(t49500,plain,
f(X1,f(X1,f(X2,f(f(X3,X1),f(X1,X4))))) = f(X2,f(f(X3,X1),f(X1,X4))),
inference(orient,[status(thm)],[t305754]) ).
cnf(t61718,plain,
f(X1,X2) = f(X2,f(f(X1,X2),f(X3,f(f(X4,X1),f(X1,Y4))))),
inference(cp,[status(thm)],[t61574,t49500]) ).
cnf(t305836,plain,
f(X1,X2) = f(X2,f(f(X1,X2),f(X3,f(f(X1,Y4),f(X4,X1))))),
inference(step,[status(thm)],[t61718,t35219]) ).
cnf(t305837,plain,
f(X1,X2) = f(X2,f(f(X1,X2),f(X3,f(f(X1,Y4),f(X1,X4))))),
inference(step,[status(thm)],[t305836,t35219]) ).
cnf(t305838,plain,
f(X1,X2) = f(X2,f(f(X1,X2),f(X3,f(f(X1,X4),f(X1,Y4))))),
inference(step,[status(thm)],[t305837,t35219]) ).
cnf(t64024,plain,
f(X1,f(f(X2,X1),f(X3,f(f(X2,X4),f(X2,Y4))))) = f(X2,X1),
inference(orient,[status(thm)],[t305838]) ).
cnf(t123044,plain,
f(f(X1,X1),f(f(X2,X3),f(X2,f(X1,X1)))) = f(X2,f(X1,X1)),
inference(cp,[status(thm)],[t123039,t64024]) ).
cnf(t123714,plain,
f(f(X1,X1),f(f(X2,X3),f(X2,f(X1,X1)))) = f(X2,f(X1,X1)),
inference(orient,[status(thm)],[t123044]) ).
cnf(t42693,plain,
f(X1,f(X2,X3)) = f(X1,f(f(X1,f(X2,X3)),X3)),
inference(cp,[status(thm)],[t42603,t36557]) ).
cnf(t305717,plain,
f(X1,f(X2,X3)) = f(X1,f(X3,f(X1,f(X2,X3)))),
inference(step,[status(thm)],[t42693,t35219]) ).
cnf(t42961,plain,
f(X1,f(X2,f(X1,f(X3,X2)))) = f(X1,f(X3,X2)),
inference(orient,[status(thm)],[t305717]) ).
cnf(t43044,plain,
f(X1,f(f(X2,X2),f(X3,f(f(X2,X4),f(X2,Y4))))) = f(X1,f(f(X3,f(f(X2,X4),f(X2,Y4))),f(X1,X2))),
inference(cp,[status(thm)],[t42961,t25119]) ).
cnf(t305745,plain,
f(X1,X2) = f(X1,f(f(X3,f(f(X2,X4),f(X2,Y4))),f(X1,X2))),
inference(step,[status(thm)],[t43044,t25119]) ).
cnf(t305746,plain,
f(X1,X2) = f(X1,f(f(X1,X2),f(X3,f(f(X2,X4),f(X2,Y4))))),
inference(step,[status(thm)],[t305745,t35219]) ).
cnf(t48354,plain,
f(X1,f(f(X1,X2),f(X3,f(f(X2,X4),f(X2,Y4))))) = f(X1,X2),
inference(orient,[status(thm)],[t305746]) ).
cnf(t48659,plain,
f(f(f(X1,X2),f(X1,X3)),f(f(X4,X1),f(X4,X1))) = f(f(f(X1,X2),f(X1,X3)),f(f(X4,X1),f(X4,f(X4,X1)))),
inference(cp,[status(thm)],[t44534,t48354]) ).
cnf(t306181,plain,
f(f(f(X1,X2),f(X1,X3)),f(f(X1,X4),f(X4,X1))) = f(f(f(X1,X2),f(X1,X3)),f(f(X4,X1),f(X4,f(X4,X1)))),
inference(step,[status(thm)],[t48659,t35219]) ).
cnf(t306182,plain,
f(f(f(X1,X2),f(X1,X3)),f(f(X1,X4),f(X1,X4))) = f(f(f(X1,X2),f(X1,X3)),f(f(X4,X1),f(X4,f(X4,X1)))),
inference(step,[status(thm)],[t306181,t35219]) ).
cnf(t306183,plain,
f(f(f(X1,X2),f(X1,X3)),f(f(X1,X4),f(X1,X4))) = f(f(f(X1,X2),f(X1,X3)),X4),
inference(step,[status(thm)],[t306182,t5662]) ).
cnf(t306184,plain,
f(f(f(X1,X2),f(X1,X3)),f(f(X1,X4),f(X1,X4))) = f(X4,f(f(X1,X2),f(X1,X3))),
inference(step,[status(thm)],[t306183,t35219]) ).
cnf(t165297,plain,
f(f(f(X1,X2),f(X1,X3)),f(f(X1,X4),f(X1,X4))) = f(X4,f(f(X1,X2),f(X1,X3))),
inference(orient,[status(thm)],[t306184]) ).
cnf(t166492,plain,
f(X1,f(f(f(X2,X3),f(X2,X3)),f(f(X2,X3),f(X2,X3)))) = f(f(X3,f(f(X2,X3),f(X2,X3))),f(f(X1,X4),f(X1,f(f(f(X2,X3),f(X2,X3)),f(f(X2,X3),f(X2,X3)))))),
inference(cp,[status(thm)],[t123714,t165297]) ).
cnf(t306190,plain,
f(X1,f(X3,f(f(X2,X3),f(X2,X3)))) = f(f(X3,f(f(X2,X3),f(X2,X3))),f(f(X1,X4),f(X1,f(f(f(X2,X3),f(X2,X3)),f(f(X2,X3),f(X2,X3)))))),
inference(step,[status(thm)],[t166492,t165297]) ).
cnf(t306191,plain,
f(X1,f(X2,X3)) = f(f(X3,f(f(X2,X3),f(X2,X3))),f(f(X1,X4),f(X1,f(f(f(X2,X3),f(X2,X3)),f(f(X2,X3),f(X2,X3)))))),
inference(step,[status(thm)],[t306190,t61574]) ).
cnf(t306192,plain,
f(X1,f(X2,X3)) = f(f(X2,X3),f(f(X1,X4),f(X1,f(f(f(X2,X3),f(X2,X3)),f(f(X2,X3),f(X2,X3)))))),
inference(step,[status(thm)],[t306191,t61574]) ).
cnf(t306193,plain,
f(X1,f(X2,X3)) = f(f(X2,X3),f(f(X1,X4),f(X1,f(X3,f(f(X2,X3),f(X2,X3)))))),
inference(step,[status(thm)],[t306192,t165297]) ).
cnf(t306194,plain,
f(X1,f(X2,X3)) = f(f(X2,X3),f(f(X1,X4),f(X1,f(X2,X3)))),
inference(step,[status(thm)],[t306193,t61574]) ).
cnf(t167628,plain,
f(f(X1,X2),f(f(X3,X4),f(X3,f(X1,X2)))) = f(X3,f(X1,X2)),
inference(orient,[status(thm)],[t306194]) ).
cnf(t306376,plain,
f(f(X3,X3),f(X1,X2)) = f(f(X1,f(f(X1,X2),f(X1,X2))),f(X3,f(f(f(X1,X2),f(X1,X2)),X3))),
inference(step,[status(thm)],[t306375,t167628]) ).
cnf(t306377,plain,
f(f(X1,X2),f(X3,X3)) = f(f(X1,f(f(X1,X2),f(X1,X2))),f(X3,f(f(f(X1,X2),f(X1,X2)),X3))),
inference(step,[status(thm)],[t306376,t35219]) ).
cnf(t306378,plain,
f(f(X1,X2),f(X3,X3)) = f(f(X1,X2),f(X3,f(f(f(X1,X2),f(X1,X2)),X3))),
inference(step,[status(thm)],[t306377,t1911]) ).
cnf(t306379,plain,
f(f(X1,X2),f(X3,X3)) = f(f(X1,X2),f(X3,f(X3,f(f(X1,X2),f(X1,X2))))),
inference(step,[status(thm)],[t306378,t35219]) ).
cnf(t306380,plain,
f(f(X1,X2),f(X3,X3)) = f(f(X1,X2),f(X3,f(X1,f(f(X3,X2),f(X3,X2))))),
inference(step,[status(thm)],[t306379,t223696]) ).
cnf(t306381,plain,
f(f(X1,X2),f(X3,X3)) = f(f(X1,X2),f(X3,f(X1,f(f(X2,X3),f(X3,X2))))),
inference(step,[status(thm)],[t306380,t35219]) ).
cnf(t306382,plain,
f(f(X1,X2),f(X3,X3)) = f(f(X1,X2),f(X3,f(X1,f(f(X2,X3),f(X2,X3))))),
inference(step,[status(thm)],[t306381,t35219]) ).
cnf(t224909,plain,
f(f(X1,X2),f(X3,f(X1,f(f(X2,X3),f(X2,X3))))) = f(f(X1,X2),f(X3,X3)),
inference(orient,[status(thm)],[t306382]) ).
cnf(t225300,plain,
f(f(f(X1,f(X2,X3)),X2),f(X3,X3)) = f(f(f(X1,f(X2,X3)),X2),f(X3,f(X2,X3))),
inference(cp,[status(thm)],[t224909,t1516]) ).
cnf(t306425,plain,
f(f(X3,X3),f(f(X1,f(X2,X3)),X2)) = f(f(f(X1,f(X2,X3)),X2),f(X3,f(X2,X3))),
inference(step,[status(thm)],[t225300,t35219]) ).
cnf(t306426,plain,
f(f(X3,X3),f(X2,f(X1,f(X2,X3)))) = f(f(f(X1,f(X2,X3)),X2),f(X3,f(X2,X3))),
inference(step,[status(thm)],[t306425,t35219]) ).
cnf(t306427,plain,
f(f(X3,X3),f(X2,f(X1,f(X2,X3)))) = f(f(X3,f(X2,X3)),f(f(X1,f(X2,X3)),X2)),
inference(step,[status(thm)],[t306426,t35219]) ).
cnf(t306428,plain,
f(f(X3,X3),f(X2,f(X1,f(X2,X3)))) = f(f(X3,f(X2,X3)),f(X2,f(X1,f(X2,X3)))),
inference(step,[status(thm)],[t306427,t35219]) ).
cnf(t238726,plain,
f(f(X1,f(X2,X1)),f(X2,f(X3,f(X2,X1)))) = f(f(X1,X1),f(X2,f(X3,f(X2,X1)))),
inference(orient,[status(thm)],[t306428]) ).
cnf(t240216,plain,
f(X1,f(X2,f(X1,X3))) = f(X1,f(f(X3,X3),f(X1,f(X2,f(X1,X3))))),
inference(cp,[status(thm)],[t90119,t238726]) ).
cnf(t240354,plain,
f(X1,f(f(X2,X2),f(X1,f(X3,f(X1,X2))))) = f(X1,f(X3,f(X1,X2))),
inference(orient,[status(thm)],[t240216]) ).
cnf(t241167,plain,
f(X1,f(f(X2,X2),f(X1,f(X3,f(X1,X2))))) = f(X1,f(f(X1,f(X3,f(X1,X2))),f(X4,f(f(X2,X2),f(X2,X2))))),
inference(cp,[status(thm)],[t44307,t240354]) ).
cnf(t306440,plain,
f(X1,f(X3,f(X1,X2))) = f(X1,f(f(X1,f(X3,f(X1,X2))),f(X4,f(f(X2,X2),f(X2,X2))))),
inference(step,[status(thm)],[t241167,t240354]) ).
cnf(t306441,plain,
f(X1,f(X3,f(X1,X2))) = f(X1,f(f(X1,f(X3,f(X1,X2))),f(X2,f(f(X4,X2),f(X4,X2))))),
inference(step,[status(thm)],[t306440,t223696]) ).
cnf(t306442,plain,
f(X1,f(X3,f(X1,X2))) = f(X1,f(f(X1,f(X3,f(X1,X2))),f(X4,X2))),
inference(step,[status(thm)],[t306441,t61574]) ).
cnf(t306443,plain,
f(X1,f(X3,f(X1,X2))) = f(X1,f(f(X1,f(X3,f(X1,X2))),f(X2,X4))),
inference(step,[status(thm)],[t306442,t35219]) ).
cnf(t306444,plain,
f(X1,f(X3,f(X1,X2))) = f(X1,f(f(X2,X4),f(X1,f(X3,f(X1,X2))))),
inference(step,[status(thm)],[t306443,t35219]) ).
cnf(t242958,plain,
f(X1,f(f(X2,X3),f(X1,f(X4,f(X1,X2))))) = f(X1,f(X4,f(X1,X2))),
inference(orient,[status(thm)],[t306444]) ).
cnf(t243141,plain,
f(X1,f(X2,f(X1,f(X3,X3)))) = f(X1,f(X3,f(X1,f(X2,f(X1,f(X3,X3)))))),
inference(cp,[status(thm)],[t242958,t25119]) ).
cnf(t247733,plain,
f(X1,f(X2,f(X1,f(X3,f(X1,f(X2,X2)))))) = f(X1,f(X3,f(X1,f(X2,X2)))),
inference(orient,[status(thm)],[t243141]) ).
cnf(t247747,plain,
f(X1,f(f(X1,X2),f(X1,f(X3,X3)))) = f(X1,f(X3,f(X1,X2))),
inference(cp,[status(thm)],[t247733,t122556]) ).
cnf(t248905,plain,
f(X1,f(f(X1,X2),f(X1,f(X3,X3)))) = f(X1,f(X3,f(X1,X2))),
inference(orient,[status(thm)],[t247747]) ).
cnf(t249155,plain,
f(f(X1,X2),f(X3,f(f(X1,X2),f(X2,f(X4,f(X4,f(X1,X2))))))) = f(f(X1,X2),f(X2,f(f(X1,X2),f(X3,X3)))),
inference(cp,[status(thm)],[t248905,t36557]) ).
cnf(t306472,plain,
f(f(X1,X2),f(X3,X2)) = f(f(X1,X2),f(X2,f(f(X1,X2),f(X3,X3)))),
inference(step,[status(thm)],[t249155,t36557]) ).
cnf(t306473,plain,
f(f(X1,X2),f(X2,X3)) = f(f(X1,X2),f(X2,f(f(X1,X2),f(X3,X3)))),
inference(step,[status(thm)],[t306472,t35219]) ).
cnf(t256150,plain,
f(f(X1,X2),f(X2,f(f(X1,X2),f(X3,X3)))) = f(f(X1,X2),f(X2,X3)),
inference(orient,[status(thm)],[t306473]) ).
cnf(t256934,plain,
f(f(X1,X1),f(X2,f(f(X1,X2),f(X3,X3)))) = f(f(X1,X1),f(X2,f(f(X1,X2),f(X2,X3)))),
inference(cp,[status(thm)],[t124655,t256150]) ).
cnf(t306488,plain,
f(f(X1,X1),f(X2,f(f(X1,X2),f(X3,X3)))) = f(f(X1,X1),f(X2,X3)),
inference(step,[status(thm)],[t256934,t124655]) ).
cnf(t260212,plain,
f(f(X1,X1),f(X2,f(f(X1,X2),f(X3,X3)))) = f(f(X1,X1),f(X2,X3)),
inference(orient,[status(thm)],[t306488]) ).
cnf(t260246,plain,
f(f(f(X1,f(X1,f(X1,X1))),f(X1,f(X1,f(X1,X1)))),f(X2,X3)) = f(X1,f(X2,f(f(f(X1,f(X1,f(X1,X1))),X2),f(X3,X3)))),
inference(cp,[status(thm)],[t260212,t69694]) ).
cnf(t306490,plain,
f(f(X2,X3),f(f(X1,f(X1,f(X1,X1))),f(X1,f(X1,f(X1,X1))))) = f(X1,f(X2,f(f(f(X1,f(X1,f(X1,X1))),X2),f(X3,X3)))),
inference(step,[status(thm)],[t260246,t35219]) ).
cnf(t306491,plain,
f(f(X2,X3),X1) = f(X1,f(X2,f(f(f(X1,f(X1,f(X1,X1))),X2),f(X3,X3)))),
inference(step,[status(thm)],[t306490,t37646]) ).
cnf(t306492,plain,
f(X1,f(X2,X3)) = f(X1,f(X2,f(f(f(X1,f(X1,f(X1,X1))),X2),f(X3,X3)))),
inference(step,[status(thm)],[t306491,t35219]) ).
cnf(t306493,plain,
f(X1,f(X2,X3)) = f(X1,f(X2,f(f(X3,X3),f(f(X1,f(X1,f(X1,X1))),X2)))),
inference(step,[status(thm)],[t306492,t35219]) ).
cnf(t306494,plain,
f(X1,f(X2,X3)) = f(X1,f(X2,f(f(X3,X3),f(X2,f(X1,f(X1,f(X1,X1))))))),
inference(step,[status(thm)],[t306493,t35219]) ).
cnf(t306495,plain,
f(X1,f(X2,X3)) = f(X1,f(X2,f(f(X3,X3),f(X2,f(X1,X1))))),
inference(step,[status(thm)],[t306494,t2041]) ).
cnf(t260996,plain,
f(X1,f(X2,f(f(X3,X3),f(X2,f(X1,X1))))) = f(X1,f(X2,X3)),
inference(orient,[status(thm)],[t306495]) ).
cnf(t261496,plain,
f(X1,f(X2,f(X1,f(f(X3,X3),f(X1,f(X2,X2)))))) = f(f(X2,f(X1,X3)),f(f(X1,X1),f(X2,f(X1,X1)))),
inference(cp,[status(thm)],[t87842,t260996]) ).
cnf(t306496,plain,
f(X1,f(f(X3,X3),f(X1,f(X2,X2)))) = f(f(X2,f(X1,X3)),f(f(X1,X1),f(X2,f(X1,X1)))),
inference(step,[status(thm)],[t261496,t247733]) ).
cnf(t306497,plain,
f(X1,f(f(X3,X3),f(X1,f(X2,X2)))) = f(X1,f(X2,f(X1,X3))),
inference(step,[status(thm)],[t306496,t87842]) ).
cnf(t261778,plain,
f(X1,f(f(X2,X2),f(X1,f(X3,X3)))) = f(X1,f(X3,f(X1,X2))),
inference(orient,[status(thm)],[t306497]) ).
cnf(t261906,plain,
f(X1,f(X2,f(X1,f(X3,f(X3,f(X3,X3)))))) = f(X1,f(X3,f(X1,f(X2,X2)))),
inference(cp,[status(thm)],[t261778,t69694]) ).
cnf(t306590,plain,
f(X1,f(X2,f(X1,f(X3,X3)))) = f(X1,f(X3,f(X1,f(X2,X2)))),
inference(step,[status(thm)],[t261906,t2041]) ).
cnf(t304535,plain,
f(X1,f(X2,f(X1,f(X3,X3)))) = f(X1,f(X3,f(X1,f(X2,X2)))),
inference(orient,[status(thm)],[t306590]) ).
cnf(goal_0,negated_conjecture,
f(a,f(c,f(a,f(b,b)))) != f(a,f(b,f(a,f(c,c)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
f(a,f(c,f(a,f(b,b)))) != f(a,f(c,f(a,f(b,b)))),
inference(rw,[status(thm)],[goal_0,t304535]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT077-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.38 % Computer : n004.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Wed Sep 23 20:10:51 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 141.66/20.92 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 141.66/20.92 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------