%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT070-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 : n020.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:07 PM UTC 2026
% Result : Unsatisfiable 57.10s 12.90s
% Output : CNFRefutation 57.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 119
% Number of leaves : 2
% Syntax : Number of clauses : 260 ( 260 unt; 0 nHn; 6 RR)
% Number of literals : 260 ( 259 equ; 5 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% Number of variables : 734 ( 152 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(X2,f(f(X1,X1),X1)),X3))) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t1,plain,
f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(X2,f(f(X1,X1),X1)),X3))) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t2,plain,
f(X1,X2) = f(X1,f(f(X1,X2),f(f(f(X1,X2),f(f(f(X3,X1),f(X3,X1)),f(X3,X1))),X4))),
inference(cp,[status(thm)],[t1,t1]) ).
cnf(t7,plain,
f(X1,f(f(X1,X2),f(f(f(X1,X2),f(f(f(X3,X1),f(X3,X1)),f(X3,X1))),X4))) = f(X1,X2),
inference(orient,[status(thm)],[t2]) ).
cnf(t9,plain,
f(f(X1,X2),f(X2,X3)) = f(f(X1,X2),f(f(f(X1,X2),f(X2,X3)),X2)),
inference(cp,[status(thm)],[t7,t1]) ).
cnf(t24,plain,
f(f(X1,X2),f(f(f(X1,X2),f(X2,X3)),X2)) = f(f(X1,X2),f(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t27,plain,
f(f(f(f(X1,X2),f(X2,X3)),X2),f(X2,f(f(X2,f(f(X1,X1),X1)),X3))) = f(f(f(f(X1,X2),f(X2,X3)),X2),f(X2,X2)),
inference(cp,[status(thm)],[t24,t1]) ).
cnf(t132109,plain,
X2 = f(f(f(f(X1,X2),f(X2,X3)),X2),f(X2,X2)),
inference(step,[status(thm)],[t27,t1]) ).
cnf(t43,plain,
f(f(f(f(X1,X2),f(X2,X3)),X2),f(X2,X2)) = X2,
inference(orient,[status(thm)],[t132109]) ).
cnf(t44,plain,
X1 = f(f(X1,X1),f(X1,X1)),
inference(cp,[status(thm)],[t43,t1]) ).
cnf(t64,plain,
f(f(X1,X1),f(X1,X1)) = X1,
inference(orient,[status(thm)],[t44]) ).
cnf(t72,plain,
X1 = f(f(X1,X2),f(X1,f(f(X1,f(f(X1,X1),X1)),X1))),
inference(cp,[status(thm)],[t1,t64]) ).
cnf(t123,plain,
f(f(X1,X2),f(X1,f(f(X1,f(f(X1,X1),X1)),X1))) = X1,
inference(orient,[status(thm)],[t72]) ).
cnf(t151,plain,
f(X1,X2) = f(X1,f(f(X1,X2),f(X1,X2))),
inference(cp,[status(thm)],[t7,t123]) ).
cnf(t157,plain,
f(X1,f(f(X1,X2),f(X1,X2))) = f(X1,X2),
inference(orient,[status(thm)],[t151]) ).
cnf(t161,plain,
f(f(X1,X2),f(X1,f(f(X1,f(f(X1,X1),X1)),X1))) = f(f(X1,X2),f(X1,f(f(X1,X2),f(X1,f(f(X1,f(f(X1,X1),X1)),X1))))),
inference(cp,[status(thm)],[t157,t123]) ).
cnf(t132112,plain,
X1 = f(f(X1,X2),f(X1,f(f(X1,X2),f(X1,f(f(X1,f(f(X1,X1),X1)),X1))))),
inference(step,[status(thm)],[t161,t123]) ).
cnf(t132113,plain,
X1 = f(f(X1,X2),f(X1,X1)),
inference(step,[status(thm)],[t132112,t123]) ).
cnf(t175,plain,
f(f(X1,X2),f(X1,X1)) = X1,
inference(orient,[status(thm)],[t132113]) ).
cnf(t180,plain,
f(X1,X1) = f(f(f(X1,X1),X2),X1),
inference(cp,[status(thm)],[t175,t175]) ).
cnf(t199,plain,
f(f(f(X1,X1),X2),X1) = f(X1,X1),
inference(orient,[status(thm)],[t180]) ).
cnf(t201,plain,
f(f(f(f(X1,X1),X2),X1),f(X1,X3)) = f(f(X1,X1),f(f(f(f(f(X1,X1),X2),X1),f(X1,X3)),X1)),
inference(cp,[status(thm)],[t24,t199]) ).
cnf(t132114,plain,
f(f(X1,X1),f(X1,X3)) = f(f(X1,X1),f(f(f(f(f(X1,X1),X2),X1),f(X1,X3)),X1)),
inference(step,[status(thm)],[t201,t199]) ).
cnf(t132115,plain,
f(f(X1,X1),f(X1,X3)) = f(f(X1,X1),f(f(f(X1,X1),f(X1,X3)),X1)),
inference(step,[status(thm)],[t132114,t199]) ).
cnf(t132116,plain,
f(f(X1,X1),f(X1,X3)) = f(f(X1,X1),f(X1,X1)),
inference(step,[status(thm)],[t132115,t199]) ).
cnf(t132117,plain,
f(f(X1,X1),f(X1,X3)) = X1,
inference(step,[status(thm)],[t132116,t175]) ).
cnf(t219,plain,
f(f(X1,X1),f(X1,X2)) = X1,
inference(orient,[status(thm)],[t132117]) ).
cnf(t229,plain,
f(f(f(X1,X1),f(X1,X2)),f(f(X1,X2),X3)) = f(X1,f(f(f(f(X1,X1),f(X1,X2)),f(f(X1,X2),X3)),f(X1,X2))),
inference(cp,[status(thm)],[t24,t219]) ).
cnf(t132133,plain,
f(X1,f(f(X1,X2),X3)) = f(X1,f(f(f(f(X1,X1),f(X1,X2)),f(f(X1,X2),X3)),f(X1,X2))),
inference(step,[status(thm)],[t229,t219]) ).
cnf(t132134,plain,
f(X1,f(f(X1,X2),X3)) = f(X1,f(f(X1,f(f(X1,X2),X3)),f(X1,X2))),
inference(step,[status(thm)],[t132133,t219]) ).
cnf(t871,plain,
f(X1,f(f(X1,f(f(X1,X2),X3)),f(X1,X2))) = f(X1,f(f(X1,X2),X3)),
inference(orient,[status(thm)],[t132134]) ).
cnf(t52791,plain,
f(X1,f(f(X1,f(f(X1,X2),X3)),f(X1,X2))) = f(X1,f(f(X1,X2),X3)),
inference(rw,[status(thm)],[t871]) ).
cnf(t227,plain,
f(X1,X2) = f(f(f(X1,X2),f(X1,X2)),X1),
inference(cp,[status(thm)],[t219,t175]) ).
cnf(t255,plain,
f(f(f(X1,X2),f(X1,X2)),X1) = f(X1,X2),
inference(orient,[status(thm)],[t227]) ).
cnf(t264,plain,
f(f(f(f(X1,X2),f(X1,X2)),X1),f(X1,X3)) = f(f(X1,X2),f(f(f(f(f(X1,X2),f(X1,X2)),X1),f(X1,X3)),X1)),
inference(cp,[status(thm)],[t24,t255]) ).
cnf(t132135,plain,
f(f(X1,X2),f(X1,X3)) = f(f(X1,X2),f(f(f(f(f(X1,X2),f(X1,X2)),X1),f(X1,X3)),X1)),
inference(step,[status(thm)],[t264,t255]) ).
cnf(t132136,plain,
f(f(X1,X2),f(X1,X3)) = f(f(X1,X2),f(f(f(X1,X2),f(X1,X3)),X1)),
inference(step,[status(thm)],[t132135,t255]) ).
cnf(t904,plain,
f(f(X1,X2),f(f(f(X1,X2),f(X1,X3)),X1)) = f(f(X1,X2),f(X1,X3)),
inference(orient,[status(thm)],[t132136]) ).
cnf(t935,plain,
f(f(f(X1,X2),X3),f(f(X1,X2),f(X1,X1))) = f(f(f(X1,X2),X3),f(f(f(f(X1,X2),X3),X1),f(X1,X2))),
inference(cp,[status(thm)],[t904,t175]) ).
cnf(t132151,plain,
f(f(f(X1,X2),X3),X1) = f(f(f(X1,X2),X3),f(f(f(f(X1,X2),X3),X1),f(X1,X2))),
inference(step,[status(thm)],[t935,t175]) ).
cnf(t1871,plain,
f(f(f(X1,X2),X3),f(f(f(f(X1,X2),X3),X1),f(X1,X2))) = f(f(f(X1,X2),X3),X1),
inference(orient,[status(thm)],[t132151]) ).
cnf(t709,plain,
f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(X2,f(f(X1,X1),X1)),X3))) = X2,
inference(rw,[status(thm)],[t1]) ).
cnf(t186,plain,
X1 = f(f(X2,X1),f(X1,f(f(X1,f(f(X2,X2),X2)),X3))),
inference(cp,[status(thm)],[t1,t175]) ).
cnf(t379,plain,
f(f(X1,X2),f(X2,f(f(X2,f(f(X1,X1),X1)),X3))) = X2,
inference(orient,[status(thm)],[t186]) ).
cnf(t404,plain,
f(f(X1,X2),f(X2,f(f(X2,f(f(X1,X1),X1)),X3))) = f(f(X2,f(f(X1,X2),f(X2,f(f(X2,f(f(X1,X1),X1)),X3)))),f(X1,X2)),
inference(cp,[status(thm)],[t255,t379]) ).
cnf(t132125,plain,
X2 = f(f(X2,f(f(X1,X2),f(X2,f(f(X2,f(f(X1,X1),X1)),X3)))),f(X1,X2)),
inference(step,[status(thm)],[t404,t379]) ).
cnf(t132126,plain,
X2 = f(f(X2,X2),f(X1,X2)),
inference(step,[status(thm)],[t132125,t379]) ).
cnf(t463,plain,
f(f(X1,X1),f(X2,X1)) = X1,
inference(orient,[status(thm)],[t132126]) ).
cnf(t472,plain,
f(f(f(X1,X1),f(X2,X1)),f(f(X2,X1),X3)) = f(X1,f(f(f(f(X1,X1),f(X2,X1)),f(f(X2,X1),X3)),f(X2,X1))),
inference(cp,[status(thm)],[t24,t463]) ).
cnf(t132137,plain,
f(X1,f(f(X2,X1),X3)) = f(X1,f(f(f(f(X1,X1),f(X2,X1)),f(f(X2,X1),X3)),f(X2,X1))),
inference(step,[status(thm)],[t472,t463]) ).
cnf(t132138,plain,
f(X1,f(f(X2,X1),X3)) = f(X1,f(f(X1,f(f(X2,X1),X3)),f(X2,X1))),
inference(step,[status(thm)],[t132137,t463]) ).
cnf(t950,plain,
f(X1,f(f(X1,f(f(X2,X1),X3)),f(X2,X1))) = f(X1,f(f(X2,X1),X3)),
inference(orient,[status(thm)],[t132138]) ).
cnf(t952,plain,
f(X1,f(f(X2,X1),f(X2,X2))) = f(X1,f(f(X1,X2),f(X2,X1))),
inference(cp,[status(thm)],[t950,t175]) ).
cnf(t132139,plain,
f(X1,X2) = f(X1,f(f(X1,X2),f(X2,X1))),
inference(step,[status(thm)],[t952,t175]) ).
cnf(t985,plain,
f(X1,f(f(X1,X2),f(X2,X1))) = f(X1,X2),
inference(orient,[status(thm)],[t132139]) ).
cnf(t401,plain,
f(X1,X2) = f(X2,f(f(X1,X2),f(X1,X2))),
inference(cp,[status(thm)],[t175,t379]) ).
cnf(t520,plain,
f(X1,f(f(X2,X1),f(X2,X1))) = f(X2,X1),
inference(orient,[status(thm)],[t401]) ).
cnf(t388,plain,
X1 = f(f(X2,X1),f(X1,f(f(X2,X2),X2))),
inference(cp,[status(thm)],[t379,t7]) ).
cnf(t556,plain,
f(f(X1,X2),f(X2,f(f(X1,X1),X1))) = X2,
inference(orient,[status(thm)],[t388]) ).
cnf(t560,plain,
f(X1,X2) = f(X1,f(f(X1,X2),f(f(f(X1,X1),f(X1,X1)),f(X1,X1)))),
inference(cp,[status(thm)],[t556,t219]) ).
cnf(t391,plain,
X1 = f(f(X2,X1),f(X1,X1)),
inference(cp,[status(thm)],[t379,t175]) ).
cnf(t431,plain,
f(f(X1,X2),f(X2,X2)) = X2,
inference(orient,[status(thm)],[t391]) ).
cnf(t132128,plain,
f(X1,X2) = f(X1,f(f(X1,X2),f(X1,f(X1,X1)))),
inference(step,[status(thm)],[t560,t431]) ).
cnf(t590,plain,
f(X1,f(f(X1,X2),f(X1,f(X1,X1)))) = f(X1,X2),
inference(orient,[status(thm)],[t132128]) ).
cnf(t608,plain,
X1 = f(f(f(f(X2,X1),f(X1,f(X1,f(X1,X1)))),X3),f(X1,f(f(X2,X2),X2))),
inference(cp,[status(thm)],[t1,t590]) ).
cnf(t464,plain,
f(X1,X1) = f(X1,f(X2,f(X1,X1))),
inference(cp,[status(thm)],[t463,t219]) ).
cnf(t505,plain,
f(X1,f(X2,f(X1,X1))) = f(X1,X1),
inference(orient,[status(thm)],[t464]) ).
cnf(t132129,plain,
X1 = f(f(f(f(X2,X1),f(X1,X1)),X3),f(X1,f(f(X2,X2),X2))),
inference(step,[status(thm)],[t608,t505]) ).
cnf(t132130,plain,
X1 = f(f(X1,X3),f(X1,f(f(X2,X2),X2))),
inference(step,[status(thm)],[t132129,t431]) ).
cnf(t615,plain,
f(f(X1,X2),f(X1,f(f(X3,X3),X3))) = X1,
inference(orient,[status(thm)],[t132130]) ).
cnf(t634,plain,
f(X1,f(f(X2,X2),X2)) = f(X1,X1),
inference(cp,[status(thm)],[t157,t615]) ).
cnf(t665,plain,
f(X1,f(f(X2,X2),X2)) = f(X1,X1),
inference(orient,[status(thm)],[t634]) ).
cnf(t674,plain,
f(X1,f(f(X2,X2),X2)) = f(f(f(X2,X2),X2),f(f(X1,X1),f(X1,f(f(X2,X2),X2)))),
inference(cp,[status(thm)],[t520,t665]) ).
cnf(t132131,plain,
f(X1,X1) = f(f(f(X2,X2),X2),f(f(X1,X1),f(X1,f(f(X2,X2),X2)))),
inference(step,[status(thm)],[t674,t665]) ).
cnf(t132132,plain,
f(X1,X1) = f(f(f(X2,X2),X2),X1),
inference(step,[status(thm)],[t132131,t219]) ).
cnf(t758,plain,
f(X1,X1) = f(f(f(X2,X2),X2),X1),
inference(orient,[status(thm)],[t132132]) ).
cnf(t986,plain,
f(f(X1,X1),X1) = f(f(X1,X1),f(f(X1,f(X1,X1)),f(X1,f(X1,X1)))),
inference(cp,[status(thm)],[t985,t758]) ).
cnf(t132140,plain,
f(f(X1,X1),X1) = f(X1,f(X1,X1)),
inference(step,[status(thm)],[t986,t520]) ).
cnf(t1004,plain,
f(f(X1,X1),X1) = f(X1,f(X1,X1)),
inference(orient,[status(thm)],[t132140]) ).
cnf(t132152,plain,
f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(X2,f(X1,f(X1,X1))),X3))) = X2,
inference(step,[status(thm)],[t709,t1004]) ).
cnf(t666,plain,
f(X1,X1) = f(X1,f(X2,f(X2,X2))),
inference(cp,[status(thm)],[t665,t219]) ).
cnf(t712,plain,
f(X1,X1) = f(X1,f(X2,f(X2,X2))),
inference(orient,[status(thm)],[t666]) ).
cnf(t132153,plain,
f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(X2,X2),X3))) = X2,
inference(step,[status(thm)],[t132152,t712]) ).
cnf(t181,plain,
f(f(f(X1,X2),f(X1,X1)),f(f(X1,X1),X3)) = f(X1,f(f(f(f(X1,X2),f(X1,X1)),f(f(X1,X1),X3)),f(X1,X1))),
inference(cp,[status(thm)],[t24,t175]) ).
cnf(t132118,plain,
f(X1,f(f(X1,X1),X3)) = f(X1,f(f(f(f(X1,X2),f(X1,X1)),f(f(X1,X1),X3)),f(X1,X1))),
inference(step,[status(thm)],[t181,t175]) ).
cnf(t132119,plain,
f(X1,f(f(X1,X1),X3)) = f(X1,f(f(X1,f(f(X1,X1),X3)),f(X1,X1))),
inference(step,[status(thm)],[t132118,t175]) ).
cnf(t132120,plain,
f(X1,f(f(X1,X1),X3)) = f(X1,X1),
inference(step,[status(thm)],[t132119,t175]) ).
cnf(t243,plain,
f(X1,f(f(X1,X1),X2)) = f(X1,X1),
inference(orient,[status(thm)],[t132120]) ).
cnf(t132154,plain,
f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,X2)) = X2,
inference(step,[status(thm)],[t132153,t243]) ).
cnf(t2002,plain,
f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,X2)) = X2,
inference(orient,[status(thm)],[t132154]) ).
cnf(t2028,plain,
f(X1,X2) = f(f(f(X1,f(f(X1,X2),X3)),X4),f(f(X1,X2),f(X1,X2))),
inference(cp,[status(thm)],[t2002,t219]) ).
cnf(t25151,plain,
f(f(f(X1,f(f(X1,X2),X3)),X4),f(f(X1,X2),f(X1,X2))) = f(X1,X2),
inference(orient,[status(thm)],[t2028]) ).
cnf(t2003,plain,
X1 = f(f(X2,f(f(X3,X1),f(X1,X4))),f(X1,X1)),
inference(cp,[status(thm)],[t2002,t520]) ).
cnf(t2090,plain,
f(f(X1,f(f(X2,X3),f(X3,X4))),f(X3,X3)) = X3,
inference(orient,[status(thm)],[t2003]) ).
cnf(t2116,plain,
X1 = f(f(X2,f(f(X1,X3),f(X1,X4))),f(X1,X1)),
inference(cp,[status(thm)],[t2090,t255]) ).
cnf(t2780,plain,
f(f(X1,f(f(X2,X3),f(X2,X4))),f(X2,X2)) = X2,
inference(orient,[status(thm)],[t2116]) ).
cnf(t2820,plain,
f(f(X1,X1),f(X2,f(f(X1,X3),f(X1,X4)))) = f(f(X1,X1),f(f(f(X1,X1),f(X2,f(f(X1,X3),f(X1,X4)))),X1)),
inference(cp,[status(thm)],[t985,t2780]) ).
cnf(t132159,plain,
f(f(X1,X1),f(X2,f(f(X1,X3),f(X1,X4)))) = X1,
inference(step,[status(thm)],[t2820,t463]) ).
cnf(t3452,plain,
f(f(X1,X1),f(X2,f(f(X1,X3),f(X1,X4)))) = X1,
inference(orient,[status(thm)],[t132159]) ).
cnf(t3453,plain,
f(X1,X1) = f(X1,f(X2,f(f(f(X1,X1),X3),f(f(X1,X1),X4)))),
inference(cp,[status(thm)],[t3452,t219]) ).
cnf(t12734,plain,
f(X1,f(X2,f(f(f(X1,X1),X3),f(f(X1,X1),X4)))) = f(X1,X1),
inference(orient,[status(thm)],[t3453]) ).
cnf(t25173,plain,
f(X1,X2) = f(f(f(X1,X1),X3),f(f(X1,X2),f(X1,X2))),
inference(cp,[status(thm)],[t25151,t12734]) ).
cnf(t26000,plain,
f(f(f(X1,X1),X2),f(f(X1,X3),f(X1,X3))) = f(X1,X3),
inference(orient,[status(thm)],[t25173]) ).
cnf(t26036,plain,
f(X1,X2) = f(f(X3,f(X1,X1)),f(f(X1,X2),f(X1,X2))),
inference(cp,[status(thm)],[t26000,t520]) ).
cnf(t26493,plain,
f(f(X1,f(X2,X2)),f(f(X2,X3),f(X2,X3))) = f(X2,X3),
inference(orient,[status(thm)],[t26036]) ).
cnf(t26542,plain,
f(X1,f(f(X2,X1),f(X2,X1))) = f(f(X3,f(X1,X1)),f(f(X2,X1),f(X1,f(f(X2,X1),f(X2,X1))))),
inference(cp,[status(thm)],[t26493,t520]) ).
cnf(t132278,plain,
f(X2,X1) = f(f(X3,f(X1,X1)),f(f(X2,X1),f(X1,f(f(X2,X1),f(X2,X1))))),
inference(step,[status(thm)],[t26542,t520]) ).
cnf(t132279,plain,
f(X2,X1) = f(f(X3,f(X1,X1)),f(f(X2,X1),f(X2,X1))),
inference(step,[status(thm)],[t132278,t505]) ).
cnf(t27363,plain,
f(f(X1,f(X2,X2)),f(f(X3,X2),f(X3,X2))) = f(X3,X2),
inference(orient,[status(thm)],[t132279]) ).
cnf(t27681,plain,
f(f(f(X1,f(X2,X2)),f(f(X3,X2),f(X3,X2))),X1) = f(f(X3,X2),f(f(f(f(X1,f(X2,X2)),f(f(X3,X2),f(X3,X2))),X1),f(X1,f(X2,X2)))),
inference(cp,[status(thm)],[t1871,t27363]) ).
cnf(t132302,plain,
f(f(X3,X2),X1) = f(f(X3,X2),f(f(f(f(X1,f(X2,X2)),f(f(X3,X2),f(X3,X2))),X1),f(X1,f(X2,X2)))),
inference(step,[status(thm)],[t27681,t27363]) ).
cnf(t132303,plain,
f(f(X3,X2),X1) = f(f(X3,X2),f(f(f(X3,X2),X1),f(X1,f(X2,X2)))),
inference(step,[status(thm)],[t132302,t27363]) ).
cnf(t37266,plain,
f(f(X1,X2),f(f(f(X1,X2),X3),f(X3,f(X2,X2)))) = f(f(X1,X2),X3),
inference(orient,[status(thm)],[t132303]) ).
cnf(t49911,plain,
f(X1,f(f(X2,X1),f(X2,X1))) = f(X2,X1),
inference(rw,[status(thm)],[t520]) ).
cnf(t2029,plain,
f(X1,X2) = f(f(f(X2,f(f(X1,X2),X3)),X4),f(f(X1,X2),f(X1,X2))),
inference(cp,[status(thm)],[t2002,t463]) ).
cnf(t48013,plain,
f(f(f(X1,f(f(X2,X1),X3)),X4),f(f(X2,X1),f(X2,X1))) = f(X2,X1),
inference(orient,[status(thm)],[t2029]) ).
cnf(t48036,plain,
f(X1,X2) = f(f(f(X2,X1),X3),f(f(X1,X2),f(X1,X2))),
inference(cp,[status(thm)],[t48013,t175]) ).
cnf(t48700,plain,
f(f(f(X1,X2),X3),f(f(X2,X1),f(X2,X1))) = f(X2,X1),
inference(orient,[status(thm)],[t48036]) ).
cnf(t49071,plain,
f(f(X1,X2),f(X1,X2)) = f(f(X1,X2),f(X2,X1)),
inference(cp,[status(thm)],[t243,t48700]) ).
cnf(t49266,plain,
f(f(X1,X2),f(X1,X2)) = f(f(X1,X2),f(X2,X1)),
inference(orient,[status(thm)],[t49071]) ).
cnf(t132343,plain,
f(X1,f(f(X2,X1),f(X1,X2))) = f(X2,X1),
inference(step,[status(thm)],[t49911,t49266]) ).
cnf(t49913,plain,
f(X1,f(f(X2,X1),f(X1,X2))) = f(X2,X1),
inference(orient,[status(thm)],[t132343]) ).
cnf(t49983,plain,
f(f(X1,X2),f(X2,X1)) = f(f(X2,X1),f(f(f(X1,X2),f(X1,X2)),f(f(X2,X1),f(X1,X2)))),
inference(cp,[status(thm)],[t49913,t49266]) ).
cnf(t132352,plain,
f(f(X1,X2),f(X1,X2)) = f(f(X2,X1),f(f(f(X1,X2),f(X1,X2)),f(f(X2,X1),f(X1,X2)))),
inference(step,[status(thm)],[t49983,t49266]) ).
cnf(t132353,plain,
f(f(X1,X2),f(X1,X2)) = f(f(X2,X1),f(X1,X2)),
inference(step,[status(thm)],[t132352,t463]) ).
cnf(t51683,plain,
f(f(X1,X2),f(X1,X2)) = f(f(X2,X1),f(X1,X2)),
inference(orient,[status(thm)],[t132353]) ).
cnf(t52208,plain,
f(f(X1,X1),X2) = f(f(X1,X1),f(f(X2,f(X1,X1)),f(X2,f(X1,X1)))),
inference(cp,[status(thm)],[t37266,t51683]) ).
cnf(t26048,plain,
f(X1,f(f(X2,X1),f(X2,X1))) = f(f(f(X1,X1),X3),f(f(X2,X1),f(X1,f(f(X2,X1),f(X2,X1))))),
inference(cp,[status(thm)],[t26000,t520]) ).
cnf(t132275,plain,
f(X2,X1) = f(f(f(X1,X1),X3),f(f(X2,X1),f(X1,f(f(X2,X1),f(X2,X1))))),
inference(step,[status(thm)],[t26048,t520]) ).
cnf(t132276,plain,
f(X2,X1) = f(f(f(X1,X1),X3),f(f(X2,X1),f(X2,X1))),
inference(step,[status(thm)],[t132275,t505]) ).
cnf(t26755,plain,
f(f(f(X1,X1),X2),f(f(X3,X1),f(X3,X1))) = f(X3,X1),
inference(orient,[status(thm)],[t132276]) ).
cnf(t26984,plain,
f(X1,f(X2,X2)) = f(f(X3,X2),f(f(X1,f(X2,X2)),f(X1,f(X2,X2)))),
inference(cp,[status(thm)],[t26755,t26755]) ).
cnf(t35802,plain,
f(f(X1,X2),f(f(X3,f(X2,X2)),f(X3,f(X2,X2)))) = f(X3,f(X2,X2)),
inference(orient,[status(thm)],[t26984]) ).
cnf(t132354,plain,
f(f(X1,X1),X2) = f(X2,f(X1,X1)),
inference(step,[status(thm)],[t52208,t35802]) ).
cnf(t52317,plain,
f(f(X1,X1),X2) = f(X2,f(X1,X1)),
inference(orient,[status(thm)],[t132354]) ).
cnf(t52326,plain,
f(X1,f(f(X2,X2),f(X2,X2))) = f(X2,X1),
inference(cp,[status(thm)],[t52317,t219]) ).
cnf(t132355,plain,
f(X1,X2) = f(X2,X1),
inference(step,[status(thm)],[t52326,t431]) ).
cnf(t52706,plain,
f(X1,X2) = f(X2,X1),
inference(orient,[status(thm)],[t132355]) ).
cnf(t132373,plain,
f(X1,f(f(X1,X2),f(X1,f(f(X1,X2),X3)))) = f(X1,f(f(X1,X2),X3)),
inference(step,[status(thm)],[t52791,t52706]) ).
cnf(t132374,plain,
f(X1,f(f(X1,X2),f(X1,f(X3,f(X1,X2))))) = f(X1,f(f(X1,X2),X3)),
inference(step,[status(thm)],[t132373,t52706]) ).
cnf(t132375,plain,
f(X1,f(f(X1,X2),f(X1,f(X3,f(X1,X2))))) = f(X1,f(X3,f(X1,X2))),
inference(step,[status(thm)],[t132374,t52706]) ).
cnf(t53750,plain,
f(X1,f(f(X1,X2),f(X1,f(X3,f(X1,X2))))) = f(X1,f(X3,f(X1,X2))),
inference(orient,[status(thm)],[t132375]) ).
cnf(t3475,plain,
f(X1,X2) = f(f(f(X1,X2),f(X1,X2)),f(X3,f(X2,f(f(X1,X2),X4)))),
inference(cp,[status(thm)],[t3452,t431]) ).
cnf(t132407,plain,
f(X1,X2) = f(f(f(X1,X2),f(X1,X2)),f(X3,f(X2,f(X4,f(X1,X2))))),
inference(step,[status(thm)],[t3475,t52706]) ).
cnf(t55426,plain,
f(f(f(X1,X2),f(X1,X2)),f(X3,f(X2,f(X4,f(X1,X2))))) = f(X1,X2),
inference(orient,[status(thm)],[t132407]) ).
cnf(t55716,plain,
f(X1,f(f(f(X2,X3),f(X2,X3)),f(X1,f(X3,f(X4,f(X2,X3)))))) = f(X1,f(f(X1,f(X3,f(X4,f(X2,X3)))),f(X1,f(X2,X3)))),
inference(cp,[status(thm)],[t53750,t55426]) ).
cnf(t132488,plain,
f(X1,f(X2,X3)) = f(X1,f(f(X1,f(X3,f(X4,f(X2,X3)))),f(X1,f(X2,X3)))),
inference(step,[status(thm)],[t55716,t55426]) ).
cnf(t132489,plain,
f(X1,f(X2,X3)) = f(X1,f(f(X1,f(X2,X3)),f(X1,f(X3,f(X4,f(X2,X3)))))),
inference(step,[status(thm)],[t132488,t52706]) ).
cnf(t63398,plain,
f(X1,f(f(X1,f(X2,X3)),f(X1,f(X3,f(X4,f(X2,X3)))))) = f(X1,f(X2,X3)),
inference(orient,[status(thm)],[t132489]) ).
cnf(t63399,plain,
f(X1,f(X2,X3)) = f(X1,f(X3,f(X1,f(X2,X3)))),
inference(cp,[status(thm)],[t63398,t53750]) ).
cnf(t63783,plain,
f(X1,f(X2,f(X1,f(X3,X2)))) = f(X1,f(X3,X2)),
inference(orient,[status(thm)],[t63399]) ).
cnf(t63869,plain,
f(X1,f(f(X2,X2),f(X2,X3))) = f(X1,f(f(X2,X3),f(X1,X2))),
inference(cp,[status(thm)],[t63783,t219]) ).
cnf(t132490,plain,
f(X1,X2) = f(X1,f(f(X2,X3),f(X1,X2))),
inference(step,[status(thm)],[t63869,t219]) ).
cnf(t132491,plain,
f(X1,X2) = f(X1,f(f(X1,X2),f(X2,X3))),
inference(step,[status(thm)],[t132490,t52706]) ).
cnf(t63970,plain,
f(X1,f(f(X1,X2),f(X2,X3))) = f(X1,X2),
inference(orient,[status(thm)],[t132491]) ).
cnf(t26983,plain,
f(f(X1,X1),X2) = f(f(f(f(X1,X1),X2),f(f(X1,X1),X2)),f(X3,X1)),
inference(cp,[status(thm)],[t219,t26755]) ).
cnf(t793,plain,
f(X1,X1) = f(f(X2,f(X2,X2)),X1),
inference(cp,[status(thm)],[t758,t219]) ).
cnf(t811,plain,
f(X1,X1) = f(f(X2,f(X2,X2)),X1),
inference(orient,[status(thm)],[t793]) ).
cnf(t132299,plain,
f(f(X1,X1),X2) = f(f(f(c,f(c,c)),f(f(X1,X1),X2)),f(X3,X1)),
inference(step,[status(thm)],[t26983,t811]) ).
cnf(t35341,plain,
f(f(f(c,f(c,c)),f(f(X1,X1),X2)),f(X3,X1)) = f(f(X1,X1),X2),
inference(orient,[status(thm)],[t132299]) ).
cnf(t745,plain,
f(X1,f(X1,X1)) = f(f(f(X1,f(X1,X1)),f(X1,f(X1,X1))),f(X2,X2)),
inference(cp,[status(thm)],[t463,t712]) ).
cnf(t1249,plain,
f(f(f(X1,f(X1,X1)),f(X1,f(X1,X1))),f(X2,X2)) = f(X1,f(X1,X1)),
inference(orient,[status(thm)],[t745]) ).
cnf(t1250,plain,
f(X1,f(X1,X1)) = f(X2,f(f(X1,f(X1,X1)),f(X1,f(X1,X1)))),
inference(cp,[status(thm)],[t1249,t520]) ).
cnf(t1315,plain,
f(X1,f(f(X2,f(X2,X2)),f(X2,f(X2,X2)))) = f(X2,f(X2,X2)),
inference(orient,[status(thm)],[t1250]) ).
cnf(t1316,plain,
f(X1,f(X1,X1)) = f(X2,f(X2,X2)),
inference(cp,[status(thm)],[t1315,t1249]) ).
cnf(t1377,plain,
f(X1,f(X1,X1)) = f(X2,f(X2,X2)),
inference(orient,[status(thm)],[t1316]) ).
cnf(t35382,plain,
f(f(X1,X1),X2) = f(f(f(X3,f(X3,X3)),f(f(X1,X1),X2)),f(X4,X1)),
inference(cp,[status(thm)],[t35341,t1377]) ).
cnf(t44516,plain,
f(f(f(X1,f(X1,X1)),f(f(X2,X2),X3)),f(X4,X2)) = f(f(X2,X2),X3),
inference(orient,[status(thm)],[t35382]) ).
cnf(t52654,plain,
f(f(f(X1,f(X1,X1)),f(f(X2,X2),X3)),f(X4,X2)) = f(f(X2,X2),X3),
inference(rw,[status(thm)],[t44516]) ).
cnf(t132376,plain,
f(f(X4,X2),f(f(X1,f(X1,X1)),f(f(X2,X2),X3))) = f(f(X2,X2),X3),
inference(step,[status(thm)],[t52654,t52706]) ).
cnf(t132377,plain,
f(f(X2,X4),f(f(X1,f(X1,X1)),f(f(X2,X2),X3))) = f(f(X2,X2),X3),
inference(step,[status(thm)],[t132376,t52706]) ).
cnf(t132378,plain,
f(f(X2,X4),f(f(X1,f(X1,X1)),f(X3,f(X2,X2)))) = f(f(X2,X2),X3),
inference(step,[status(thm)],[t132377,t52317]) ).
cnf(t132379,plain,
f(f(X2,X4),f(f(X1,f(X1,X1)),f(X3,f(X2,X2)))) = f(X3,f(X2,X2)),
inference(step,[status(thm)],[t132378,t52317]) ).
cnf(t53979,plain,
f(f(X1,X2),f(f(X3,f(X3,X3)),f(X4,f(X1,X1)))) = f(X4,f(X1,X1)),
inference(orient,[status(thm)],[t132379]) ).
cnf(t64077,plain,
f(X1,f(X2,X3)) = f(X1,f(f(X1,f(X2,X3)),f(X4,f(X2,X2)))),
inference(cp,[status(thm)],[t63970,t53979]) ).
cnf(t64348,plain,
f(X1,f(f(X1,f(X2,X3)),f(X4,f(X2,X2)))) = f(X1,f(X2,X3)),
inference(orient,[status(thm)],[t64077]) ).
cnf(t64361,plain,
f(X1,f(X2,X3)) = f(X1,f(f(X1,f(X2,X3)),X2)),
inference(cp,[status(thm)],[t64348,t63970]) ).
cnf(t132494,plain,
f(X1,f(X2,X3)) = f(X1,f(X2,f(X1,f(X2,X3)))),
inference(step,[status(thm)],[t64361,t52706]) ).
cnf(t64591,plain,
f(X1,f(X2,f(X1,f(X2,X3)))) = f(X1,f(X2,X3)),
inference(orient,[status(thm)],[t132494]) ).
cnf(t929,plain,
f(f(X1,X2),f(X1,f(f(X3,X1),f(X3,X1)))) = f(f(X1,X2),f(f(f(X1,X2),f(X3,X1)),X1)),
inference(cp,[status(thm)],[t904,t520]) ).
cnf(t132145,plain,
f(f(X1,X2),f(X3,X1)) = f(f(X1,X2),f(f(f(X1,X2),f(X3,X1)),X1)),
inference(step,[status(thm)],[t929,t520]) ).
cnf(t1114,plain,
f(f(X1,X2),f(f(f(X1,X2),f(X3,X1)),X1)) = f(f(X1,X2),f(X3,X1)),
inference(orient,[status(thm)],[t132145]) ).
cnf(t52788,plain,
f(f(X1,X2),f(f(f(X1,X2),f(X3,X1)),X1)) = f(f(X1,X2),f(X3,X1)),
inference(rw,[status(thm)],[t1114]) ).
cnf(t132370,plain,
f(f(X1,X2),f(X1,f(f(X1,X2),f(X3,X1)))) = f(f(X1,X2),f(X3,X1)),
inference(step,[status(thm)],[t52788,t52706]) ).
cnf(t132371,plain,
f(f(X1,X2),f(X1,f(f(X1,X2),f(X1,X3)))) = f(f(X1,X2),f(X3,X1)),
inference(step,[status(thm)],[t132370,t52706]) ).
cnf(t132372,plain,
f(f(X1,X2),f(X1,f(f(X1,X2),f(X1,X3)))) = f(f(X1,X2),f(X1,X3)),
inference(step,[status(thm)],[t132371,t52706]) ).
cnf(t53669,plain,
f(f(X1,X2),f(X1,f(f(X1,X2),f(X1,X3)))) = f(f(X1,X2),f(X1,X3)),
inference(orient,[status(thm)],[t132372]) ).
cnf(t2839,plain,
f(X1,f(f(X1,f(f(X2,X3),f(X2,X4))),f(X2,X2))) = f(X1,f(f(X1,X2),f(X1,f(f(X2,X3),f(X2,X4))))),
inference(cp,[status(thm)],[t871,t2780]) ).
cnf(t132192,plain,
f(X1,X2) = f(X1,f(f(X1,X2),f(X1,f(f(X2,X3),f(X2,X4))))),
inference(step,[status(thm)],[t2839,t2780]) ).
cnf(t7777,plain,
f(X1,f(f(X1,X2),f(X1,f(f(X2,X3),f(X2,X4))))) = f(X1,X2),
inference(orient,[status(thm)],[t132192]) ).
cnf(t53688,plain,
f(f(X1,X2),f(X1,f(f(X2,X3),f(X2,X4)))) = f(f(X1,X2),f(X1,X2)),
inference(cp,[status(thm)],[t53669,t7777]) ).
cnf(t53827,plain,
f(f(X1,X2),f(X1,f(f(X2,X3),f(X2,X4)))) = f(f(X1,X2),f(X1,X2)),
inference(orient,[status(thm)],[t53688]) ).
cnf(t27601,plain,
f(f(f(X1,X2),f(X1,X2)),f(X3,f(X2,X2))) = f(f(f(X1,X2),f(X1,X2)),f(f(f(f(X1,X2),f(X1,X2)),f(X3,f(X2,X2))),f(X1,X2))),
inference(cp,[status(thm)],[t985,t27363]) ).
cnf(t132284,plain,
f(f(f(X1,X2),f(X1,X2)),f(X3,f(X2,X2))) = f(X1,X2),
inference(step,[status(thm)],[t27601,t463]) ).
cnf(t28716,plain,
f(f(f(X1,X2),f(X1,X2)),f(X3,f(X2,X2))) = f(X1,X2),
inference(orient,[status(thm)],[t132284]) ).
cnf(t52640,plain,
f(f(f(X1,X2),f(X1,X2)),f(X3,f(X2,X2))) = f(X1,X2),
inference(rw,[status(thm)],[t28716]) ).
cnf(t132361,plain,
f(f(X3,f(X2,X2)),f(f(X1,X2),f(X1,X2))) = f(X1,X2),
inference(step,[status(thm)],[t52640,t52317]) ).
cnf(t53202,plain,
f(f(X1,f(X2,X2)),f(f(X3,X2),f(X3,X2))) = f(X3,X2),
inference(orient,[status(thm)],[t132361]) ).
cnf(t53871,plain,
f(f(f(X1,f(X2,X2)),X3),f(f(X1,f(X2,X2)),X3)) = f(f(f(X1,f(X2,X2)),X3),f(X3,X2)),
inference(cp,[status(thm)],[t53827,t53202]) ).
cnf(t132575,plain,
f(f(X3,f(X1,f(X2,X2))),f(f(X1,f(X2,X2)),X3)) = f(f(f(X1,f(X2,X2)),X3),f(X3,X2)),
inference(step,[status(thm)],[t53871,t51683]) ).
cnf(t132576,plain,
f(f(X3,f(X1,f(X2,X2))),f(X3,f(X1,f(X2,X2)))) = f(f(f(X1,f(X2,X2)),X3),f(X3,X2)),
inference(step,[status(thm)],[t132575,t49266]) ).
cnf(t52717,plain,
f(X1,f(X2,f(X2,X2))) = f(X1,X1),
inference(cp,[status(thm)],[t52706,t811]) ).
cnf(t52821,plain,
f(X1,f(X2,f(X2,X2))) = f(X1,X1),
inference(orient,[status(thm)],[t52717]) ).
cnf(t132577,plain,
f(f(X3,f(X1,f(X2,X2))),f(c,f(c,c))) = f(f(f(X1,f(X2,X2)),X3),f(X3,X2)),
inference(step,[status(thm)],[t132576,t52821]) ).
cnf(t132578,plain,
f(f(c,f(c,c)),f(X3,f(X1,f(X2,X2)))) = f(f(f(X1,f(X2,X2)),X3),f(X3,X2)),
inference(step,[status(thm)],[t132577,t52706]) ).
cnf(t132579,plain,
f(f(c,f(c,c)),f(X3,f(X1,f(X2,X2)))) = f(f(X3,X2),f(f(X1,f(X2,X2)),X3)),
inference(step,[status(thm)],[t132578,t52706]) ).
cnf(t132580,plain,
f(f(c,f(c,c)),f(X3,f(X1,f(X2,X2)))) = f(f(X2,X3),f(f(X1,f(X2,X2)),X3)),
inference(step,[status(thm)],[t132579,t52706]) ).
cnf(t132581,plain,
f(f(c,f(c,c)),f(X3,f(X1,f(X2,X2)))) = f(f(X2,X3),f(X3,f(X1,f(X2,X2)))),
inference(step,[status(thm)],[t132580,t52706]) ).
cnf(t77038,plain,
f(f(c,f(c,c)),f(X1,f(X2,f(X3,X3)))) = f(f(X3,X1),f(X1,f(X2,f(X3,X3)))),
inference(orient,[status(thm)],[t132581]) ).
cnf(t2123,plain,
X1 = f(f(X2,f(f(X3,X1),f(X4,X1))),f(X1,X1)),
inference(cp,[status(thm)],[t2090,t520]) ).
cnf(t2861,plain,
f(f(X1,f(f(X2,X3),f(X4,X3))),f(X3,X3)) = X3,
inference(orient,[status(thm)],[t2123]) ).
cnf(t52671,plain,
f(f(X1,f(f(X2,X3),f(X4,X3))),f(X3,X3)) = X3,
inference(rw,[status(thm)],[t2861]) ).
cnf(t132359,plain,
f(f(X3,X3),f(X1,f(f(X2,X3),f(X4,X3)))) = X3,
inference(step,[status(thm)],[t52671,t52317]) ).
cnf(t132360,plain,
f(f(X3,X3),f(X1,f(f(X2,X3),f(X3,X4)))) = X3,
inference(step,[status(thm)],[t132359,t52706]) ).
cnf(t53091,plain,
f(f(X1,X1),f(X2,f(f(X3,X1),f(X1,X4)))) = X1,
inference(orient,[status(thm)],[t132360]) ).
cnf(t53174,plain,
f(f(f(X1,X2),f(X2,X3)),f(f(X1,X2),f(X2,X3))) = f(f(f(X1,X2),f(X2,X3)),X2),
inference(cp,[status(thm)],[t505,t53091]) ).
cnf(t132485,plain,
f(f(f(X1,X2),f(X2,X3)),f(c,f(c,c))) = f(f(f(X1,X2),f(X2,X3)),X2),
inference(step,[status(thm)],[t53174,t52821]) ).
cnf(t132486,plain,
f(f(c,f(c,c)),f(f(X1,X2),f(X2,X3))) = f(f(f(X1,X2),f(X2,X3)),X2),
inference(step,[status(thm)],[t132485,t52706]) ).
cnf(t132487,plain,
f(f(c,f(c,c)),f(f(X1,X2),f(X2,X3))) = f(X2,f(f(X1,X2),f(X2,X3))),
inference(step,[status(thm)],[t132486,t52706]) ).
cnf(t62832,plain,
f(f(c,f(c,c)),f(f(X1,X2),f(X2,X3))) = f(X2,f(f(X1,X2),f(X2,X3))),
inference(orient,[status(thm)],[t132487]) ).
cnf(t77043,plain,
f(f(X1,f(X2,X3)),f(f(X2,X3),f(X3,f(X1,X1)))) = f(X3,f(f(X2,X3),f(X3,f(X1,X1)))),
inference(cp,[status(thm)],[t77038,t62832]) ).
cnf(t101296,plain,
f(f(X1,f(X2,X3)),f(f(X2,X3),f(X3,f(X1,X1)))) = f(X3,f(f(X2,X3),f(X3,f(X1,X1)))),
inference(orient,[status(thm)],[t77043]) ).
cnf(t101852,plain,
f(X1,f(X2,X3)) = f(X1,f(X3,f(f(X2,X3),f(X3,f(X1,X1))))),
inference(cp,[status(thm)],[t63970,t101296]) ).
cnf(t102135,plain,
f(X1,f(X2,f(f(X3,X2),f(X2,f(X1,X1))))) = f(X1,f(X3,X2)),
inference(orient,[status(thm)],[t101852]) ).
cnf(t102398,plain,
f(f(X1,X1),f(X2,X3)) = f(f(X1,X1),f(X3,f(f(X2,X3),f(X3,X1)))),
inference(cp,[status(thm)],[t102135,t219]) ).
cnf(t132691,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)],[t102398,t52706]) ).
cnf(t132692,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)],[t132691,t52706]) ).
cnf(t102595,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)],[t132692]) ).
cnf(t102861,plain,
f(f(X1,X1),f(f(X2,X2),f(X2,X3))) = f(f(X1,X1),f(f(X2,X3),f(f(X1,f(X2,X3)),X2))),
inference(cp,[status(thm)],[t102595,t219]) ).
cnf(t132698,plain,
f(f(X1,X1),X2) = f(f(X1,X1),f(f(X2,X3),f(f(X1,f(X2,X3)),X2))),
inference(step,[status(thm)],[t102861,t219]) ).
cnf(t132699,plain,
f(X2,f(X1,X1)) = f(f(X1,X1),f(f(X2,X3),f(f(X1,f(X2,X3)),X2))),
inference(step,[status(thm)],[t132698,t52317]) ).
cnf(t132700,plain,
f(X2,f(X1,X1)) = f(f(X1,X1),f(f(X2,X3),f(X2,f(X1,f(X2,X3))))),
inference(step,[status(thm)],[t132699,t52706]) ).
cnf(t104109,plain,
f(f(X1,X1),f(f(X2,X3),f(X2,f(X1,f(X2,X3))))) = f(X2,f(X1,X1)),
inference(orient,[status(thm)],[t132700]) ).
cnf(t104660,plain,
f(f(X1,X1),f(f(X2,X3),f(X2,f(X1,f(X2,X3))))) = f(f(X1,X1),f(f(X2,X3),f(X2,f(X1,X1)))),
inference(cp,[status(thm)],[t64591,t104109]) ).
cnf(t132701,plain,
f(X2,f(X1,X1)) = f(f(X1,X1),f(f(X2,X3),f(X2,f(X1,X1)))),
inference(step,[status(thm)],[t104660,t104109]) ).
cnf(t104805,plain,
f(f(X1,X1),f(f(X2,X3),f(X2,f(X1,X1)))) = f(X2,f(X1,X1)),
inference(orient,[status(thm)],[t132701]) ).
cnf(t77382,plain,
f(f(c,f(c,c)),f(X1,f(f(X1,f(X2,X3)),f(f(X2,X2),f(X2,X2))))) = f(f(f(X2,X2),X1),f(X1,f(X2,X3))),
inference(cp,[status(thm)],[t77038,t64348]) ).
cnf(t132586,plain,
f(f(c,f(c,c)),f(X1,f(X2,X3))) = f(f(f(X2,X2),X1),f(X1,f(X2,X3))),
inference(step,[status(thm)],[t77382,t64348]) ).
cnf(t132587,plain,
f(f(X1,f(X2,X3)),f(X1,f(X2,X3))) = f(f(f(X2,X2),X1),f(X1,f(X2,X3))),
inference(step,[status(thm)],[t132586,t811]) ).
cnf(t132588,plain,
f(f(X1,f(X2,X3)),f(X1,f(X2,X3))) = f(f(X1,f(X2,X3)),f(f(X2,X2),X1)),
inference(step,[status(thm)],[t132587,t52706]) ).
cnf(t132589,plain,
f(f(X1,f(X2,X3)),f(X1,f(X2,X3))) = f(f(X1,f(X2,X3)),f(X1,f(X2,X2))),
inference(step,[status(thm)],[t132588,t52317]) ).
cnf(t132590,plain,
f(f(X1,f(X2,X3)),f(X1,f(X2,X3))) = f(f(X1,f(X2,X2)),f(X1,f(X2,X3))),
inference(step,[status(thm)],[t132589,t52706]) ).
cnf(t78596,plain,
f(f(X1,f(X2,X3)),f(X1,f(X2,X3))) = f(f(X1,f(X2,X2)),f(X1,f(X2,X3))),
inference(orient,[status(thm)],[t132590]) ).
cnf(t78747,plain,
f(f(X1,f(f(X2,X3),f(X2,X3))),f(X1,f(f(X2,X3),f(X3,X3)))) = f(f(X1,X3),f(X1,f(f(X2,X3),f(X3,X3)))),
inference(cp,[status(thm)],[t78596,t431]) ).
cnf(t132597,plain,
f(f(X1,f(f(X2,X3),f(X2,X3))),f(X1,X3)) = f(f(X1,X3),f(X1,f(f(X2,X3),f(X3,X3)))),
inference(step,[status(thm)],[t78747,t431]) ).
cnf(t132598,plain,
f(f(X1,X3),f(X1,f(f(X2,X3),f(X2,X3)))) = f(f(X1,X3),f(X1,f(f(X2,X3),f(X3,X3)))),
inference(step,[status(thm)],[t132597,t52706]) ).
cnf(t132599,plain,
f(f(X1,X3),f(X1,f(f(X2,X3),f(X2,X3)))) = f(f(X1,X3),f(X1,X3)),
inference(step,[status(thm)],[t132598,t431]) ).
cnf(t80490,plain,
f(f(X1,X2),f(X1,f(f(X3,X2),f(X3,X2)))) = f(f(X1,X2),f(X1,X2)),
inference(orient,[status(thm)],[t132599]) ).
cnf(t104826,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)],[t104805,t80490]) ).
cnf(t132769,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)],[t104826,t52317]) ).
cnf(t124134,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)],[t132769]) ).
cnf(t124145,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)],[t124134,t52706]) ).
cnf(t132793,plain,
f(X1,f(f(X2,X3),f(X2,X3))) = f(X2,f(f(X1,X3),f(X1,X3))),
inference(step,[status(thm)],[t124145,t124134]) ).
cnf(t131343,plain,
f(X1,f(f(X2,X3),f(X2,X3))) = f(X2,f(f(X1,X3),f(X1,X3))),
inference(orient,[status(thm)],[t132793]) ).
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,t131343]) ).
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,t51683]) ).
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,t52706]) ).
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,t131343]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT070-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/5.39 % Computer : n020.cluster.edu
% 0.11/5.39 % Model : x86_64 x86_64
% 0.11/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.39 % Memory : 8046.5625MB
% 0.11/5.39 % OS : Linux 6.8.0-71-generic
% 0.11/5.39 % CPULimit : 300
% 0.11/5.39 % WCLimit : 300
% 0.11/5.39 % DateTime : Wed Sep 23 20:10:25 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.11/5.39 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 57.10/12.90 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 57.10/12.90 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------