FindProof---0.1.UNS-CRf.s

%------------------------------------------------------------------------------
% File     : FindProof---0.1
% Problem  : TOP050-1 : TPTP v9.3.1. Released v8.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300

% Computer : n019.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 03:54:47 PM UTC 2026

% Result   : Unsatisfiable 27.35s 3.94s
% Output   : CNFRefutation 27.35s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :  131
%            Number of leaves      :   35
% Syntax   : Number of clauses     :  577 ( 577 unt;   0 nHn; 531 RR)
%            Number of literals    :  577 ( 576 equ;  61 neg)
%            Maximal clause size   :    1 (   1 avg)
%            Maximal term depth    :   32 (   7 avg)
%            Number of predicates  :    2 (   0 usr;   1 prp; 0-2 aty)
%            Number of functors    :   35 (  35 usr;  33 con; 0-2 aty)
%            Number of variables   :   56 (   0 sgn)

% Comments : 
%------------------------------------------------------------------------------
cnf(t32,axiom,
    product(product(X1,X2),X2) = X1,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t128,plain,
    product(product(X1,X2),X2) = X1,
    inference(orient,[status(thm)],[t32]) ).

cnf(t33,axiom,
    product(product(X1,X2),product(X3,X2)) = product(product(X1,X3),X2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t170,plain,
    product(product(X1,X2),product(X3,X2)) = product(product(X1,X3),X2),
    inference(orient,[status(thm)],[t33]) ).

cnf(t0,axiom,
    product(X1,X1) = X1,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t96,plain,
    product(X1,X1) = X1,
    inference(orient,[status(thm)],[t0]) ).

cnf(t171,plain,
    product(product(X1,X2),X1) = product(X1,product(X2,X1)),
    inference(cp,[status(thm)],[t170,t96]) ).

cnf(t326,plain,
    product(product(X1,X2),X1) = product(X1,product(X2,X1)),
    inference(orient,[status(thm)],[t171]) ).

cnf(t12,axiom,
    product(a2,a25) = a3,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t108,plain,
    product(a2,a25) = a3,
    inference(orient,[status(thm)],[t12]) ).

cnf(t140,plain,
    a2 = product(a3,a25),
    inference(cp,[status(thm)],[t128,t108]) ).

cnf(t263,plain,
    product(a3,a25) = a2,
    inference(orient,[status(thm)],[t140]) ).

cnf(t371,plain,
    product(a3,product(a25,a3)) = product(a2,a3),
    inference(cp,[status(thm)],[t326,t263]) ).

cnf(t17,axiom,
    product(a24,a3) = a25,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t113,plain,
    product(a24,a3) = a25,
    inference(orient,[status(thm)],[t17]) ).

cnf(t145,plain,
    a24 = product(a25,a3),
    inference(cp,[status(thm)],[t128,t113]) ).

cnf(t278,plain,
    product(a25,a3) = a24,
    inference(orient,[status(thm)],[t145]) ).

cnf(t4840,plain,
    product(a3,a24) = product(a2,a3),
    inference(step,[status(thm)],[t371,t278]) ).

cnf(t419,plain,
    product(a2,a3) = product(a3,a24),
    inference(orient,[status(thm)],[t4840]) ).

cnf(t2936,plain,
    product(a31,a3) = a24,
    inference(rw,[status(thm)],[t278]) ).

cnf(t25,axiom,
    product(a31,a3) = a32,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t121,plain,
    product(a31,a3) = a32,
    inference(orient,[status(thm)],[t25]) ).

cnf(t5743,plain,
    a32 = a24,
    inference(step,[status(thm)],[t2936,t121]) ).

cnf(t3201,plain,
    a24 = a32,
    inference(orient,[status(thm)],[t5743]) ).

cnf(t5744,plain,
    product(a2,a3) = product(a3,a32),
    inference(step,[status(thm)],[t419,t3201]) ).

cnf(t3203,plain,
    product(a2,a3) = product(a3,a32),
    inference(orient,[status(thm)],[t5744]) ).

cnf(t3370,plain,
    product(a2,a32) = product(a3,a32),
    inference(rw,[status(thm)],[t3203]) ).

cnf(t23,axiom,
    product(a3,a29) = a4,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t119,plain,
    product(a3,a29) = a4,
    inference(orient,[status(thm)],[t23]) ).

cnf(t349,plain,
    product(a3,product(a29,a3)) = product(a4,a3),
    inference(cp,[status(thm)],[t326,t119]) ).

cnf(t21,axiom,
    product(a28,a3) = a29,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t117,plain,
    product(a28,a3) = a29,
    inference(orient,[status(thm)],[t21]) ).

cnf(t149,plain,
    a28 = product(a29,a3),
    inference(cp,[status(thm)],[t128,t117]) ).

cnf(t291,plain,
    product(a29,a3) = a28,
    inference(orient,[status(thm)],[t149]) ).

cnf(t4834,plain,
    product(a3,a28) = product(a4,a3),
    inference(step,[status(thm)],[t349,t291]) ).

cnf(t406,plain,
    product(a3,a28) = product(a4,a3),
    inference(orient,[status(thm)],[t4834]) ).

cnf(t22,axiom,
    product(a29,a1) = a30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t118,plain,
    product(a29,a1) = a30,
    inference(orient,[status(thm)],[t22]) ).

cnf(t3036,plain,
    product(a29,a3) = a30,
    inference(rw,[status(thm)],[t118]) ).

cnf(t5763,plain,
    a28 = a30,
    inference(step,[status(thm)],[t3036,t291]) ).

cnf(t3244,plain,
    a28 = a30,
    inference(orient,[status(thm)],[t5763]) ).

cnf(t5766,plain,
    product(a3,a30) = product(a4,a3),
    inference(step,[status(thm)],[t406,t3244]) ).

cnf(t3248,plain,
    product(a3,a30) = product(a4,a3),
    inference(rw,[status(thm)],[t5766]) ).

cnf(t26,axiom,
    product(a32,a21) = a1,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t122,plain,
    product(a32,a21) = a1,
    inference(orient,[status(thm)],[t26]) ).

cnf(t194,plain,
    product(product(a2,X1),a25) = product(a3,product(X1,a25)),
    inference(cp,[status(thm)],[t170,t108]) ).

cnf(t596,plain,
    product(product(a2,X1),a25) = product(a3,product(X1,a25)),
    inference(orient,[status(thm)],[t194]) ).

cnf(t1,axiom,
    product(a1,a31) = a2,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t97,plain,
    product(a1,a31) = a2,
    inference(orient,[status(thm)],[t1]) ).

cnf(t129,plain,
    a1 = product(a2,a31),
    inference(cp,[status(thm)],[t128,t97]) ).

cnf(t162,plain,
    product(a2,a31) = a1,
    inference(orient,[status(thm)],[t129]) ).

cnf(t597,plain,
    product(a3,product(a31,a25)) = product(a1,a25),
    inference(cp,[status(thm)],[t596,t162]) ).

cnf(t1935,plain,
    product(a3,product(a31,a25)) = product(a1,a25),
    inference(orient,[status(thm)],[t597]) ).

cnf(t2918,plain,
    product(a3,a25) = product(a1,a25),
    inference(rw,[status(thm)],[t1935]) ).

cnf(t195,plain,
    product(product(X1,a2),a25) = product(product(X1,a25),a3),
    inference(cp,[status(thm)],[t170,t108]) ).

cnf(t604,plain,
    product(product(X1,a2),a25) = product(product(X1,a25),a3),
    inference(orient,[status(thm)],[t195]) ).

cnf(t280,plain,
    product(product(X1,a25),a3) = product(product(X1,a3),a24),
    inference(cp,[status(thm)],[t170,t278]) ).

cnf(t1214,plain,
    product(product(X1,a25),a3) = product(product(X1,a3),a24),
    inference(orient,[status(thm)],[t280]) ).

cnf(t4937,plain,
    product(product(X1,a2),a25) = product(product(X1,a3),a24),
    inference(step,[status(thm)],[t604,t1214]) ).

cnf(t1215,plain,
    product(product(X1,a2),a25) = product(product(X1,a3),a24),
    inference(orient,[status(thm)],[t4937]) ).

cnf(t173,plain,
    product(product(X1,a1),a31) = product(product(X1,a31),a2),
    inference(cp,[status(thm)],[t170,t97]) ).

cnf(t449,plain,
    product(product(X1,a1),a31) = product(product(X1,a31),a2),
    inference(orient,[status(thm)],[t173]) ).

cnf(t451,plain,
    product(product(a29,a31),a2) = product(a30,a31),
    inference(cp,[status(thm)],[t449,t118]) ).

cnf(t24,axiom,
    product(a30,a23) = a31,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t120,plain,
    product(a30,a23) = a31,
    inference(orient,[status(thm)],[t24]) ).

cnf(t152,plain,
    a30 = product(a31,a23),
    inference(cp,[status(thm)],[t128,t120]) ).

cnf(t300,plain,
    product(a31,a23) = a30,
    inference(orient,[status(thm)],[t152]) ).

cnf(t383,plain,
    product(a31,product(a23,a31)) = product(a30,a31),
    inference(cp,[status(thm)],[t326,t300]) ).

cnf(t15,axiom,
    product(a22,a31) = a23,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t111,plain,
    product(a22,a31) = a23,
    inference(orient,[status(thm)],[t15]) ).

cnf(t143,plain,
    a22 = product(a23,a31),
    inference(cp,[status(thm)],[t128,t111]) ).

cnf(t272,plain,
    product(a23,a31) = a22,
    inference(orient,[status(thm)],[t143]) ).

cnf(t4844,plain,
    product(a31,a22) = product(a30,a31),
    inference(step,[status(thm)],[t383,t272]) ).

cnf(t435,plain,
    product(a30,a31) = product(a31,a22),
    inference(orient,[status(thm)],[t4844]) ).

cnf(t5113,plain,
    product(product(a29,a31),a2) = product(a31,a22),
    inference(step,[status(thm)],[t451,t435]) ).

cnf(t1811,plain,
    product(product(a29,a31),a2) = product(a31,a22),
    inference(orient,[status(thm)],[t5113]) ).

cnf(t1815,plain,
    product(product(product(a29,a31),a3),a24) = product(product(a31,a22),a25),
    inference(cp,[status(thm)],[t1215,t1811]) ).

cnf(t292,plain,
    product(product(a29,X1),a3) = product(a28,product(X1,a3)),
    inference(cp,[status(thm)],[t170,t291]) ).

cnf(t1295,plain,
    product(product(a29,X1),a3) = product(a28,product(X1,a3)),
    inference(orient,[status(thm)],[t292]) ).

cnf(t5610,plain,
    product(product(a28,product(a31,a3)),a24) = product(product(a31,a22),a25),
    inference(step,[status(thm)],[t1815,t1295]) ).

cnf(t5611,plain,
    product(product(a28,a32),a24) = product(product(a31,a22),a25),
    inference(step,[status(thm)],[t5610,t121]) ).

cnf(t16,axiom,
    product(a23,a21) = a24,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t112,plain,
    product(a23,a21) = a24,
    inference(orient,[status(thm)],[t16]) ).

cnf(t203,plain,
    product(product(X1,a23),a21) = product(product(X1,a21),a24),
    inference(cp,[status(thm)],[t170,t112]) ).

cnf(t657,plain,
    product(product(X1,a21),a24) = product(product(X1,a23),a21),
    inference(orient,[status(thm)],[t203]) ).

cnf(t20,axiom,
    product(a27,a21) = a28,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t116,plain,
    product(a27,a21) = a28,
    inference(orient,[status(thm)],[t20]) ).

cnf(t210,plain,
    product(product(a27,X1),a21) = product(a28,product(X1,a21)),
    inference(cp,[status(thm)],[t170,t116]) ).

cnf(t714,plain,
    product(product(a27,X1),a21) = product(a28,product(X1,a21)),
    inference(orient,[status(thm)],[t210]) ).

cnf(t19,axiom,
    product(a26,a1) = a27,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t115,plain,
    product(a26,a1) = a27,
    inference(orient,[status(thm)],[t19]) ).

cnf(t147,plain,
    a26 = product(a27,a1),
    inference(cp,[status(thm)],[t128,t115]) ).

cnf(t285,plain,
    product(a27,a1) = a26,
    inference(orient,[status(thm)],[t147]) ).

cnf(t715,plain,
    product(a28,product(a1,a21)) = product(a26,a21),
    inference(cp,[status(thm)],[t714,t285]) ).

cnf(t154,plain,
    a32 = product(a1,a21),
    inference(cp,[status(thm)],[t128,t122]) ).

cnf(t306,plain,
    product(a1,a21) = a32,
    inference(orient,[status(thm)],[t154]) ).

cnf(t4868,plain,
    product(a28,a32) = product(a26,a21),
    inference(step,[status(thm)],[t715,t306]) ).

cnf(t722,plain,
    product(a26,a21) = product(a28,a32),
    inference(orient,[status(thm)],[t4868]) ).

cnf(t728,plain,
    product(product(a26,a23),a21) = product(product(a28,a32),a24),
    inference(cp,[status(thm)],[t657,t722]) ).

cnf(t18,axiom,
    product(a25,a23) = a26,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t114,plain,
    product(a25,a23) = a26,
    inference(orient,[status(thm)],[t18]) ).

cnf(t146,plain,
    a25 = product(a26,a23),
    inference(cp,[status(thm)],[t128,t114]) ).

cnf(t281,plain,
    product(a26,a23) = a25,
    inference(orient,[status(thm)],[t146]) ).

cnf(t5300,plain,
    product(a25,a21) = product(product(a28,a32),a24),
    inference(step,[status(thm)],[t728,t281]) ).

cnf(t2013,plain,
    product(product(a28,a32),a24) = product(a25,a21),
    inference(orient,[status(thm)],[t5300]) ).

cnf(t5612,plain,
    product(a25,a21) = product(product(a31,a22),a25),
    inference(step,[status(thm)],[t5611,t2013]) ).

cnf(t14,axiom,
    product(a21,a25) = a22,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t110,plain,
    product(a21,a25) = a22,
    inference(orient,[status(thm)],[t14]) ).

cnf(t142,plain,
    a21 = product(a22,a25),
    inference(cp,[status(thm)],[t128,t110]) ).

cnf(t269,plain,
    product(a22,a25) = a21,
    inference(orient,[status(thm)],[t142]) ).

cnf(t271,plain,
    product(product(X1,a22),a25) = product(product(X1,a25),a21),
    inference(cp,[status(thm)],[t170,t269]) ).

cnf(t1160,plain,
    product(product(X1,a22),a25) = product(product(X1,a25),a21),
    inference(orient,[status(thm)],[t271]) ).

cnf(t5613,plain,
    product(a25,a21) = product(product(a31,a25),a21),
    inference(step,[status(thm)],[t5612,t1160]) ).

cnf(t2908,plain,
    product(product(a31,a25),a21) = product(a25,a21),
    inference(orient,[status(thm)],[t5613]) ).

cnf(t2909,plain,
    product(a31,a25) = product(product(a25,a21),a21),
    inference(cp,[status(thm)],[t128,t2908]) ).

cnf(t5614,plain,
    product(a31,a25) = a25,
    inference(step,[status(thm)],[t2909,t128]) ).

cnf(t2917,plain,
    product(a31,a25) = a25,
    inference(orient,[status(thm)],[t5614]) ).

cnf(t2921,plain,
    a31 = product(a25,a25),
    inference(cp,[status(thm)],[t128,t2917]) ).

cnf(t5616,plain,
    a31 = a25,
    inference(step,[status(thm)],[t2921,t96]) ).

cnf(t2928,plain,
    a25 = a31,
    inference(orient,[status(thm)],[t5616]) ).

cnf(t5657,plain,
    product(a3,a31) = product(a1,a25),
    inference(step,[status(thm)],[t2918,t2928]) ).

cnf(t5658,plain,
    product(a3,a31) = product(a1,a31),
    inference(step,[status(thm)],[t5657,t2928]) ).

cnf(t5659,plain,
    product(a3,a31) = a2,
    inference(step,[status(thm)],[t5658,t97]) ).

cnf(t3017,plain,
    product(a3,a31) = a2,
    inference(orient,[status(thm)],[t5659]) ).

cnf(t3029,plain,
    a3 = product(a2,a31),
    inference(cp,[status(thm)],[t128,t3017]) ).

cnf(t5669,plain,
    a3 = a1,
    inference(step,[status(thm)],[t3029,t162]) ).

cnf(t3033,plain,
    a1 = a3,
    inference(orient,[status(thm)],[t5669]) ).

cnf(t5671,plain,
    product(a32,a21) = a3,
    inference(step,[status(thm)],[t122,t3033]) ).

cnf(t3037,plain,
    product(a32,a21) = a3,
    inference(orient,[status(thm)],[t5671]) ).

cnf(t270,plain,
    product(product(a22,X1),a25) = product(a21,product(X1,a25)),
    inference(cp,[status(thm)],[t170,t269]) ).

cnf(t1153,plain,
    product(product(a22,X1),a25) = product(a21,product(X1,a25)),
    inference(orient,[status(thm)],[t270]) ).

cnf(t1154,plain,
    product(a21,product(a31,a25)) = product(a23,a25),
    inference(cp,[status(thm)],[t1153,t111]) ).

cnf(t2384,plain,
    product(a21,product(a31,a25)) = product(a23,a25),
    inference(orient,[status(thm)],[t1154]) ).

cnf(t2919,plain,
    product(a21,a25) = product(a23,a25),
    inference(rw,[status(thm)],[t2384]) ).

cnf(t5706,plain,
    product(a21,a31) = product(a23,a25),
    inference(step,[status(thm)],[t2919,t2928]) ).

cnf(t5707,plain,
    product(a21,a31) = product(a23,a31),
    inference(step,[status(thm)],[t5706,t2928]) ).

cnf(t5708,plain,
    product(a21,a31) = a22,
    inference(step,[status(thm)],[t5707,t272]) ).

cnf(t3106,plain,
    product(a21,a31) = a22,
    inference(orient,[status(thm)],[t5708]) ).

cnf(t3110,plain,
    a21 = product(a22,a31),
    inference(cp,[status(thm)],[t128,t3106]) ).

cnf(t5710,plain,
    a21 = a23,
    inference(step,[status(thm)],[t3110,t111]) ).

cnf(t3113,plain,
    a21 = a23,
    inference(orient,[status(thm)],[t5710]) ).

cnf(t5714,plain,
    product(a32,a23) = a3,
    inference(step,[status(thm)],[t3037,t3113]) ).

cnf(t3118,plain,
    product(a32,a23) = a3,
    inference(rw,[status(thm)],[t5714]) ).

cnf(t273,plain,
    product(product(a23,X1),a31) = product(a22,product(X1,a31)),
    inference(cp,[status(thm)],[t170,t272]) ).

cnf(t1165,plain,
    product(product(a23,X1),a31) = product(a22,product(X1,a31)),
    inference(orient,[status(thm)],[t273]) ).

cnf(t1166,plain,
    product(a22,product(a21,a31)) = product(a24,a31),
    inference(cp,[status(thm)],[t1165,t112]) ).

cnf(t2394,plain,
    product(a22,product(a21,a31)) = product(a24,a31),
    inference(orient,[status(thm)],[t1166]) ).

cnf(t3108,plain,
    product(a22,a22) = product(a24,a31),
    inference(rw,[status(thm)],[t2394]) ).

cnf(t5802,plain,
    a22 = product(a24,a31),
    inference(step,[status(thm)],[t3108,t96]) ).

cnf(t5803,plain,
    a22 = product(a32,a31),
    inference(step,[status(thm)],[t5802,t3201]) ).

cnf(t3302,plain,
    product(a32,a31) = a22,
    inference(orient,[status(thm)],[t5803]) ).

cnf(t3309,plain,
    a32 = product(a22,a31),
    inference(cp,[status(thm)],[t128,t3302]) ).

cnf(t5810,plain,
    a32 = a23,
    inference(step,[status(thm)],[t3309,t111]) ).

cnf(t3314,plain,
    a23 = a32,
    inference(orient,[status(thm)],[t5810]) ).

cnf(t5844,plain,
    product(a32,a32) = a3,
    inference(step,[status(thm)],[t3118,t3314]) ).

cnf(t5845,plain,
    a32 = a3,
    inference(step,[status(thm)],[t5844,t96]) ).

cnf(t3360,plain,
    a3 = a32,
    inference(orient,[status(thm)],[t5845]) ).

cnf(t5944,plain,
    product(a32,a30) = product(a4,a3),
    inference(step,[status(thm)],[t3248,t3360]) ).

cnf(t5670,plain,
    product(a26,a3) = a27,
    inference(step,[status(thm)],[t115,t3033]) ).

cnf(t3035,plain,
    product(a26,a3) = a27,
    inference(rw,[status(thm)],[t5670]) ).

cnf(t2933,plain,
    product(a31,a23) = a26,
    inference(rw,[status(thm)],[t114]) ).

cnf(t5738,plain,
    a30 = a26,
    inference(step,[status(thm)],[t2933,t300]) ).

cnf(t3182,plain,
    a26 = a30,
    inference(orient,[status(thm)],[t5738]) ).

cnf(t5760,plain,
    product(a30,a3) = a27,
    inference(step,[status(thm)],[t3035,t3182]) ).

cnf(t3233,plain,
    product(a30,a3) = a27,
    inference(orient,[status(thm)],[t5760]) ).

cnf(t3236,plain,
    a30 = product(a27,a3),
    inference(cp,[status(thm)],[t128,t3233]) ).

cnf(t150,plain,
    a29 = product(a30,a1),
    inference(cp,[status(thm)],[t128,t118]) ).

cnf(t294,plain,
    product(a30,a1) = a29,
    inference(orient,[status(thm)],[t150]) ).

cnf(t5677,plain,
    product(a30,a3) = a29,
    inference(step,[status(thm)],[t294,t3033]) ).

cnf(t3043,plain,
    product(a30,a3) = a29,
    inference(rw,[status(thm)],[t5677]) ).

cnf(t5792,plain,
    a27 = a29,
    inference(step,[status(thm)],[t3043,t3233]) ).

cnf(t3277,plain,
    a27 = a29,
    inference(orient,[status(thm)],[t5792]) ).

cnf(t5621,plain,
    product(a26,a23) = a31,
    inference(step,[status(thm)],[t281,t2928]) ).

cnf(t2937,plain,
    product(a26,a23) = a31,
    inference(orient,[status(thm)],[t5621]) ).

cnf(t3183,plain,
    product(a30,a23) = a31,
    inference(rw,[status(thm)],[t2937]) ).

cnf(t5888,plain,
    product(a30,a32) = a31,
    inference(step,[status(thm)],[t3183,t3314]) ).

cnf(t148,plain,
    a27 = product(a28,a21),
    inference(cp,[status(thm)],[t128,t116]) ).

cnf(t288,plain,
    product(a28,a21) = a27,
    inference(orient,[status(thm)],[t148]) ).

cnf(t5717,plain,
    product(a28,a23) = a27,
    inference(step,[status(thm)],[t288,t3113]) ).

cnf(t3121,plain,
    product(a28,a23) = a27,
    inference(rw,[status(thm)],[t5717]) ).

cnf(t5884,plain,
    product(a30,a23) = a27,
    inference(step,[status(thm)],[t3121,t3244]) ).

cnf(t5885,plain,
    product(a30,a32) = a27,
    inference(step,[status(thm)],[t5884,t3314]) ).

cnf(t5886,plain,
    product(a30,a32) = a29,
    inference(step,[status(thm)],[t5885,t3277]) ).

cnf(t3414,plain,
    product(a30,a32) = a29,
    inference(orient,[status(thm)],[t5886]) ).

cnf(t5889,plain,
    a29 = a31,
    inference(step,[status(thm)],[t5888,t3414]) ).

cnf(t3419,plain,
    a29 = a31,
    inference(orient,[status(thm)],[t5889]) ).

cnf(t5899,plain,
    a27 = a31,
    inference(step,[status(thm)],[t3277,t3419]) ).

cnf(t3441,plain,
    a27 = a31,
    inference(orient,[status(thm)],[t5899]) ).

cnf(t5618,plain,
    product(a24,a3) = a31,
    inference(step,[status(thm)],[t113,t2928]) ).

cnf(t2931,plain,
    product(a24,a3) = a31,
    inference(orient,[status(thm)],[t5618]) ).

cnf(t3202,plain,
    product(a32,a3) = a31,
    inference(rw,[status(thm)],[t2931]) ).

cnf(t5905,plain,
    product(a32,a32) = a31,
    inference(step,[status(thm)],[t3202,t3360]) ).

cnf(t5906,plain,
    a32 = a31,
    inference(step,[status(thm)],[t5905,t96]) ).

cnf(t3449,plain,
    a31 = a32,
    inference(orient,[status(thm)],[t5906]) ).

cnf(t5919,plain,
    a27 = a32,
    inference(step,[status(thm)],[t3441,t3449]) ).

cnf(t3468,plain,
    a27 = a32,
    inference(orient,[status(thm)],[t5919]) ).

cnf(t5932,plain,
    a30 = product(a32,a3),
    inference(step,[status(thm)],[t3236,t3468]) ).

cnf(t5933,plain,
    a30 = product(a32,a32),
    inference(step,[status(thm)],[t5932,t3360]) ).

cnf(t5934,plain,
    a30 = a32,
    inference(step,[status(thm)],[t5933,t96]) ).

cnf(t3478,plain,
    a30 = a32,
    inference(orient,[status(thm)],[t5934]) ).

cnf(t5945,plain,
    product(a32,a32) = product(a4,a3),
    inference(step,[status(thm)],[t5944,t3478]) ).

cnf(t5946,plain,
    a32 = product(a4,a3),
    inference(step,[status(thm)],[t5945,t96]) ).

cnf(t5947,plain,
    a32 = product(a4,a32),
    inference(step,[status(thm)],[t5946,t3360]) ).

cnf(t3488,plain,
    product(a4,a32) = a32,
    inference(orient,[status(thm)],[t5947]) ).

cnf(t3489,plain,
    a4 = product(a32,a32),
    inference(cp,[status(thm)],[t128,t3488]) ).

cnf(t5948,plain,
    a4 = a32,
    inference(step,[status(thm)],[t3489,t96]) ).

cnf(t3494,plain,
    a32 = a4,
    inference(orient,[status(thm)],[t5948]) ).

cnf(t6006,plain,
    product(a2,a4) = product(a3,a32),
    inference(step,[status(thm)],[t3370,t3494]) ).

cnf(t5966,plain,
    a3 = a4,
    inference(step,[status(thm)],[t3360,t3494]) ).

cnf(t3512,plain,
    a3 = a4,
    inference(orient,[status(thm)],[t5966]) ).

cnf(t6007,plain,
    product(a2,a4) = product(a4,a32),
    inference(step,[status(thm)],[t6006,t3512]) ).

cnf(t6008,plain,
    product(a2,a4) = product(a4,a4),
    inference(step,[status(thm)],[t6007,t3494]) ).

cnf(t6009,plain,
    product(a2,a4) = a4,
    inference(step,[status(thm)],[t6008,t96]) ).

cnf(t3534,plain,
    product(a2,a4) = a4,
    inference(orient,[status(thm)],[t6009]) ).

cnf(t3535,plain,
    a2 = product(a4,a4),
    inference(cp,[status(thm)],[t128,t3534]) ).

cnf(t6010,plain,
    a2 = a4,
    inference(step,[status(thm)],[t3535,t96]) ).

cnf(t3540,plain,
    a2 = a4,
    inference(orient,[status(thm)],[t6010]) ).

cnf(t11,axiom,
    product(a19,a11) = a20,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t107,plain,
    product(a19,a11) = a20,
    inference(orient,[status(thm)],[t11]) ).

cnf(t13,axiom,
    product(a20,a29) = a21,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t109,plain,
    product(a20,a29) = a21,
    inference(orient,[status(thm)],[t13]) ).

cnf(t141,plain,
    a20 = product(a21,a29),
    inference(cp,[status(thm)],[t128,t109]) ).

cnf(t266,plain,
    product(a21,a29) = a20,
    inference(orient,[status(thm)],[t141]) ).

cnf(t268,plain,
    product(product(X1,a21),a29) = product(product(X1,a29),a20),
    inference(cp,[status(thm)],[t170,t266]) ).

cnf(t1138,plain,
    product(product(X1,a21),a29) = product(product(X1,a29),a20),
    inference(orient,[status(thm)],[t268]) ).

cnf(t1141,plain,
    product(product(a32,a29),a20) = product(a1,a29),
    inference(cp,[status(thm)],[t1138,t122]) ).

cnf(t2364,plain,
    product(product(a32,a29),a20) = product(a1,a29),
    inference(orient,[status(thm)],[t1141]) ).

cnf(t3087,plain,
    product(product(a32,a29),a20) = product(a3,a29),
    inference(orient,[status(thm)],[t2364]) ).

cnf(t5868,plain,
    product(product(a32,a29),a20) = product(a32,a29),
    inference(step,[status(thm)],[t3087,t3360]) ).

cnf(t3392,plain,
    product(product(a32,a29),a20) = product(a32,a29),
    inference(orient,[status(thm)],[t5868]) ).

cnf(t3408,plain,
    product(a20,a20) = product(a32,a29),
    inference(rw,[status(thm)],[t3392]) ).

cnf(t6016,plain,
    a20 = product(a32,a29),
    inference(step,[status(thm)],[t3408,t96]) ).

cnf(t6017,plain,
    a20 = product(a4,a29),
    inference(step,[status(thm)],[t6016,t3494]) ).

cnf(t5923,plain,
    a29 = a32,
    inference(step,[status(thm)],[t3419,t3449]) ).

cnf(t3473,plain,
    a29 = a32,
    inference(orient,[status(thm)],[t5923]) ).

cnf(t5969,plain,
    a29 = a4,
    inference(step,[status(thm)],[t3473,t3494]) ).

cnf(t3515,plain,
    a29 = a4,
    inference(orient,[status(thm)],[t5969]) ).

cnf(t6018,plain,
    a20 = product(a4,a4),
    inference(step,[status(thm)],[t6017,t3515]) ).

cnf(t6019,plain,
    a20 = a4,
    inference(step,[status(thm)],[t6018,t96]) ).

cnf(t3547,plain,
    a20 = a4,
    inference(orient,[status(thm)],[t6019]) ).

cnf(t6020,plain,
    product(a19,a11) = a4,
    inference(step,[status(thm)],[t107,t3547]) ).

cnf(t3548,plain,
    product(a19,a11) = a4,
    inference(orient,[status(thm)],[t6020]) ).

cnf(t3607,plain,
    product(a5,a11) = a4,
    inference(rw,[status(thm)],[t3548]) ).

cnf(t4,axiom,
    product(a12,a19) = a13,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t100,plain,
    product(a12,a19) = a13,
    inference(orient,[status(thm)],[t4]) ).

cnf(t3603,plain,
    product(a12,a5) = a13,
    inference(rw,[status(thm)],[t100]) ).

cnf(t3,axiom,
    product(a11,a5) = a12,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t99,plain,
    product(a11,a5) = a12,
    inference(orient,[status(thm)],[t3]) ).

cnf(t131,plain,
    a11 = product(a12,a5),
    inference(cp,[status(thm)],[t128,t99]) ).

cnf(t164,plain,
    product(a12,a5) = a11,
    inference(orient,[status(thm)],[t131]) ).

cnf(t6120,plain,
    a11 = a13,
    inference(step,[status(thm)],[t3603,t164]) ).

cnf(t3889,plain,
    a11 = a13,
    inference(orient,[status(thm)],[t6120]) ).

cnf(t6188,plain,
    product(a5,a13) = a4,
    inference(step,[status(thm)],[t3607,t3889]) ).

cnf(t3995,plain,
    product(a5,a13) = a4,
    inference(orient,[status(thm)],[t6188]) ).

cnf(t2,axiom,
    product(a10,a7) = a11,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t98,plain,
    product(a10,a7) = a11,
    inference(orient,[status(thm)],[t2]) ).

cnf(t6121,plain,
    product(a10,a7) = a13,
    inference(step,[status(thm)],[t98,t3889]) ).

cnf(t3890,plain,
    product(a10,a7) = a13,
    inference(orient,[status(thm)],[t6121]) ).

cnf(t4011,plain,
    product(a10,a9) = a13,
    inference(rw,[status(thm)],[t3890]) ).

cnf(t176,plain,
    product(product(a11,X1),a5) = product(a12,product(X1,a5)),
    inference(cp,[status(thm)],[t170,t99]) ).

cnf(t472,plain,
    product(product(a11,X1),a5) = product(a12,product(X1,a5)),
    inference(orient,[status(thm)],[t176]) ).

cnf(t130,plain,
    a10 = product(a11,a7),
    inference(cp,[status(thm)],[t128,t98]) ).

cnf(t163,plain,
    product(a11,a7) = a10,
    inference(orient,[status(thm)],[t130]) ).

cnf(t473,plain,
    product(a12,product(a7,a5)) = product(a10,a5),
    inference(cp,[status(thm)],[t472,t163]) ).

cnf(t1844,plain,
    product(a12,product(a7,a5)) = product(a10,a5),
    inference(orient,[status(thm)],[t473]) ).

cnf(t4002,plain,
    product(a12,a8) = product(a10,a5),
    inference(rw,[status(thm)],[t1844]) ).

cnf(t29,axiom,
    product(a7,a19) = a8,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t125,plain,
    product(a7,a19) = a8,
    inference(orient,[status(thm)],[t29]) ).

cnf(t229,plain,
    product(product(X1,a7),a19) = product(product(X1,a19),a8),
    inference(cp,[status(thm)],[t170,t125]) ).

cnf(t895,plain,
    product(product(X1,a19),a8) = product(product(X1,a7),a19),
    inference(orient,[status(thm)],[t229]) ).

cnf(t132,plain,
    a12 = product(a13,a19),
    inference(cp,[status(thm)],[t128,t100]) ).

cnf(t165,plain,
    product(a13,a19) = a12,
    inference(orient,[status(thm)],[t132]) ).

cnf(t897,plain,
    product(product(a13,a7),a19) = product(a12,a8),
    inference(cp,[status(thm)],[t895,t165]) ).

cnf(t5,axiom,
    product(a13,a7) = a14,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t101,plain,
    product(a13,a7) = a14,
    inference(orient,[status(thm)],[t5]) ).

cnf(t4887,plain,
    product(a14,a19) = product(a12,a8),
    inference(step,[status(thm)],[t897,t101]) ).

cnf(t909,plain,
    product(a12,a8) = product(a14,a19),
    inference(orient,[status(thm)],[t4887]) ).

cnf(t139,plain,
    a19 = product(a20,a11),
    inference(cp,[status(thm)],[t128,t107]) ).

cnf(t260,plain,
    product(a20,a11) = a19,
    inference(orient,[status(thm)],[t139]) ).

cnf(t3550,plain,
    product(a4,a11) = a19,
    inference(rw,[status(thm)],[t260]) ).

cnf(t27,axiom,
    product(a4,a11) = a5,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t123,plain,
    product(a4,a11) = a5,
    inference(orient,[status(thm)],[t27]) ).

cnf(t6091,plain,
    a5 = a19,
    inference(step,[status(thm)],[t3550,t123]) ).

cnf(t3602,plain,
    a19 = a5,
    inference(orient,[status(thm)],[t6091]) ).

cnf(t6099,plain,
    product(a12,a8) = product(a14,a5),
    inference(step,[status(thm)],[t909,t3602]) ).

cnf(t3623,plain,
    product(a12,a8) = product(a14,a5),
    inference(orient,[status(thm)],[t6099]) ).

cnf(t4331,plain,
    product(a12,a8) = product(a17,a5),
    inference(orient,[status(thm)],[t3623]) ).

cnf(t6242,plain,
    product(a17,a5) = product(a10,a5),
    inference(step,[status(thm)],[t4002,t4331]) ).

cnf(t8,axiom,
    product(a16,a19) = a17,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t104,plain,
    product(a16,a19) = a17,
    inference(orient,[status(thm)],[t8]) ).

cnf(t136,plain,
    a16 = product(a17,a19),
    inference(cp,[status(thm)],[t128,t104]) ).

cnf(t169,plain,
    product(a17,a19) = a16,
    inference(orient,[status(thm)],[t136]) ).

cnf(t6096,plain,
    product(a17,a5) = a16,
    inference(step,[status(thm)],[t169,t3602]) ).

cnf(t3610,plain,
    product(a17,a5) = a16,
    inference(rw,[status(thm)],[t6096]) ).

cnf(t4038,plain,
    product(a17,a5) = a16,
    inference(orient,[status(thm)],[t3610]) ).

cnf(t6243,plain,
    a16 = product(a10,a5),
    inference(step,[status(thm)],[t6242,t4038]) ).

cnf(t4360,plain,
    product(a10,a5) = a16,
    inference(orient,[status(thm)],[t6243]) ).

cnf(t4361,plain,
    a10 = product(a16,a5),
    inference(cp,[status(thm)],[t128,t4360]) ).

cnf(t7,axiom,
    product(a15,a5) = a16,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t103,plain,
    product(a15,a5) = a16,
    inference(orient,[status(thm)],[t7]) ).

cnf(t135,plain,
    a15 = product(a16,a5),
    inference(cp,[status(thm)],[t128,t103]) ).

cnf(t168,plain,
    product(a16,a5) = a15,
    inference(orient,[status(thm)],[t135]) ).

cnf(t3604,plain,
    product(a16,a5) = a17,
    inference(rw,[status(thm)],[t104]) ).

cnf(t6156,plain,
    a15 = a17,
    inference(step,[status(thm)],[t3604,t168]) ).

cnf(t3937,plain,
    a15 = a17,
    inference(orient,[status(thm)],[t6156]) ).

cnf(t6162,plain,
    product(a16,a5) = a17,
    inference(step,[status(thm)],[t168,t3937]) ).

cnf(t3944,plain,
    product(a16,a5) = a17,
    inference(orient,[status(thm)],[t6162]) ).

cnf(t6244,plain,
    a10 = a17,
    inference(step,[status(thm)],[t4361,t3944]) ).

cnf(t4373,plain,
    a10 = a17,
    inference(orient,[status(thm)],[t6244]) ).

cnf(t6253,plain,
    product(a17,a9) = a13,
    inference(step,[status(thm)],[t4011,t4373]) ).

cnf(t9,axiom,
    product(a17,a9) = a18,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t105,plain,
    product(a17,a9) = a18,
    inference(orient,[status(thm)],[t9]) ).

cnf(t28,axiom,
    product(a5,a15) = a6,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t124,plain,
    product(a5,a15) = a6,
    inference(orient,[status(thm)],[t28]) ).

cnf(t6161,plain,
    product(a5,a17) = a6,
    inference(step,[status(thm)],[t124,t3937]) ).

cnf(t3942,plain,
    product(a5,a17) = a6,
    inference(rw,[status(thm)],[t6161]) ).

cnf(t10,axiom,
    product(a18,a15) = a19,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t106,plain,
    product(a18,a15) = a19,
    inference(orient,[status(thm)],[t10]) ).

cnf(t138,plain,
    a18 = product(a19,a15),
    inference(cp,[status(thm)],[t128,t106]) ).

cnf(t257,plain,
    product(a19,a15) = a18,
    inference(orient,[status(thm)],[t138]) ).

cnf(t3611,plain,
    product(a5,a15) = a18,
    inference(rw,[status(thm)],[t257]) ).

cnf(t6198,plain,
    product(a5,a17) = a18,
    inference(step,[status(thm)],[t3611,t3937]) ).

cnf(t4044,plain,
    product(a5,a17) = a18,
    inference(orient,[status(thm)],[t6198]) ).

cnf(t6213,plain,
    a18 = a6,
    inference(step,[status(thm)],[t3942,t4044]) ).

cnf(t4299,plain,
    a18 = a6,
    inference(orient,[status(thm)],[t6213]) ).

cnf(t6214,plain,
    product(a17,a9) = a6,
    inference(step,[status(thm)],[t105,t4299]) ).

cnf(t4300,plain,
    product(a17,a9) = a6,
    inference(orient,[status(thm)],[t6214]) ).

cnf(t6254,plain,
    a6 = a13,
    inference(step,[status(thm)],[t6253,t4300]) ).

cnf(t4389,plain,
    a13 = a6,
    inference(orient,[status(thm)],[t6254]) ).

cnf(t6266,plain,
    product(a5,a6) = a4,
    inference(step,[status(thm)],[t3995,t4389]) ).

cnf(t4401,plain,
    product(a5,a6) = a4,
    inference(rw,[status(thm)],[t6266]) ).

cnf(t6,axiom,
    product(a14,a17) = a15,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t102,plain,
    product(a14,a17) = a15,
    inference(orient,[status(thm)],[t6]) ).

cnf(t134,plain,
    a14 = product(a15,a17),
    inference(cp,[status(thm)],[t128,t102]) ).

cnf(t167,plain,
    product(a15,a17) = a14,
    inference(orient,[status(thm)],[t134]) ).

cnf(t247,plain,
    product(product(X1,a15),a17) = product(product(X1,a17),a14),
    inference(cp,[status(thm)],[t170,t167]) ).

cnf(t1020,plain,
    product(product(X1,a15),a17) = product(product(X1,a17),a14),
    inference(orient,[status(thm)],[t247]) ).

cnf(t1021,plain,
    product(product(a18,a17),a14) = product(a19,a17),
    inference(cp,[status(thm)],[t1020,t106]) ).

cnf(t2214,plain,
    product(product(a18,a17),a14) = product(a19,a17),
    inference(orient,[status(thm)],[t1021]) ).

cnf(t6113,plain,
    product(product(a18,a17),a14) = product(a5,a17),
    inference(step,[status(thm)],[t2214,t3602]) ).

cnf(t3666,plain,
    product(product(a18,a17),a14) = product(a5,a17),
    inference(orient,[status(thm)],[t6113]) ).

cnf(t6201,plain,
    product(product(a18,a17),a14) = a18,
    inference(step,[status(thm)],[t3666,t4044]) ).

cnf(t4047,plain,
    product(product(a18,a17),a14) = a18,
    inference(orient,[status(thm)],[t6201]) ).

cnf(t6092,plain,
    product(a18,a15) = a5,
    inference(step,[status(thm)],[t106,t3602]) ).

cnf(t3605,plain,
    product(a18,a15) = a5,
    inference(orient,[status(thm)],[t6092]) ).

cnf(t6160,plain,
    product(a18,a17) = a5,
    inference(step,[status(thm)],[t3605,t3937]) ).

cnf(t3941,plain,
    product(a18,a17) = a5,
    inference(rw,[status(thm)],[t6160]) ).

cnf(t4290,plain,
    product(a18,a17) = a5,
    inference(orient,[status(thm)],[t3941]) ).

cnf(t6212,plain,
    product(a5,a14) = a18,
    inference(step,[status(thm)],[t4047,t4290]) ).

cnf(t4294,plain,
    product(a5,a14) = a18,
    inference(rw,[status(thm)],[t6212]) ).

cnf(t3943,plain,
    product(a17,a17) = a14,
    inference(rw,[status(thm)],[t167]) ).

cnf(t6238,plain,
    a17 = a14,
    inference(step,[status(thm)],[t3943,t96]) ).

cnf(t4327,plain,
    a14 = a17,
    inference(orient,[status(thm)],[t6238]) ).

cnf(t358,plain,
    product(product(X1,X2),product(X2,product(X1,X2))) = product(X1,product(X1,X2)),
    inference(cp,[status(thm)],[t326,t128]) ).

cnf(t4582,plain,
    product(product(X1,X2),product(X2,product(X1,X2))) = product(X1,product(X1,X2)),
    inference(orient,[status(thm)],[t358]) ).

cnf(t30,axiom,
    product(a8,a5) = a9,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t126,plain,
    product(a8,a5) = a9,
    inference(orient,[status(thm)],[t30]) ).

cnf(t158,plain,
    a8 = product(a9,a5),
    inference(cp,[status(thm)],[t128,t126]) ).

cnf(t319,plain,
    product(a9,a5) = a8,
    inference(orient,[status(thm)],[t158]) ).

cnf(t321,plain,
    product(product(X1,a9),a5) = product(product(X1,a5),a8),
    inference(cp,[status(thm)],[t170,t319]) ).

cnf(t1531,plain,
    product(product(X1,a5),a8) = product(product(X1,a9),a5),
    inference(orient,[status(thm)],[t321]) ).

cnf(t4043,plain,
    product(product(a17,a9),a5) = product(a16,a8),
    inference(cp,[status(thm)],[t1531,t4038]) ).

cnf(t6283,plain,
    product(a6,a5) = product(a16,a8),
    inference(step,[status(thm)],[t4043,t4300]) ).

cnf(t320,plain,
    product(product(a9,X1),a5) = product(a8,product(X1,a5)),
    inference(cp,[status(thm)],[t170,t319]) ).

cnf(t1523,plain,
    product(product(a9,X1),a5) = product(a8,product(X1,a5)),
    inference(orient,[status(thm)],[t320]) ).

cnf(t31,axiom,
    product(a9,a17) = a10,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t127,plain,
    product(a9,a17) = a10,
    inference(orient,[status(thm)],[t31]) ).

cnf(t1524,plain,
    product(a8,product(a17,a5)) = product(a10,a5),
    inference(cp,[status(thm)],[t1523,t127]) ).

cnf(t2816,plain,
    product(a8,product(a17,a5)) = product(a10,a5),
    inference(orient,[status(thm)],[t1524]) ).

cnf(t6197,plain,
    product(a8,a16) = product(a10,a5),
    inference(step,[status(thm)],[t2816,t4038]) ).

cnf(t4040,plain,
    product(a8,a16) = product(a10,a5),
    inference(rw,[status(thm)],[t6197]) ).

cnf(t6274,plain,
    product(a8,a16) = product(a17,a5),
    inference(step,[status(thm)],[t4040,t4373]) ).

cnf(t6275,plain,
    product(a8,a16) = a16,
    inference(step,[status(thm)],[t6274,t4038]) ).

cnf(t4517,plain,
    product(a8,a16) = a16,
    inference(orient,[status(thm)],[t6275]) ).

cnf(t4518,plain,
    a8 = product(a16,a16),
    inference(cp,[status(thm)],[t128,t4517]) ).

cnf(t6276,plain,
    a8 = a16,
    inference(step,[status(thm)],[t4518,t96]) ).

cnf(t4528,plain,
    a16 = a8,
    inference(orient,[status(thm)],[t6276]) ).

cnf(t6284,plain,
    product(a6,a5) = product(a8,a8),
    inference(step,[status(thm)],[t6283,t4528]) ).

cnf(t6285,plain,
    product(a6,a5) = a8,
    inference(step,[status(thm)],[t6284,t96]) ).

cnf(t4540,plain,
    product(a6,a5) = a8,
    inference(orient,[status(thm)],[t6285]) ).

cnf(t4541,plain,
    a6 = product(a8,a5),
    inference(cp,[status(thm)],[t128,t4540]) ).

cnf(t6286,plain,
    a6 = a9,
    inference(step,[status(thm)],[t4541,t126]) ).

cnf(t4552,plain,
    a6 = a9,
    inference(orient,[status(thm)],[t6286]) ).

cnf(t6287,plain,
    product(a17,a9) = a9,
    inference(step,[status(thm)],[t4300,t4552]) ).

cnf(t4553,plain,
    product(a17,a9) = a9,
    inference(orient,[status(thm)],[t6287]) ).

cnf(t4583,plain,
    product(a17,product(a17,a9)) = product(product(a17,a9),product(a9,a9)),
    inference(cp,[status(thm)],[t4582,t4553]) ).

cnf(t6307,plain,
    product(a17,a9) = product(product(a17,a9),product(a9,a9)),
    inference(step,[status(thm)],[t4583,t4553]) ).

cnf(t6308,plain,
    a9 = product(product(a17,a9),product(a9,a9)),
    inference(step,[status(thm)],[t6307,t4553]) ).

cnf(t6309,plain,
    a9 = product(product(a17,a9),a9),
    inference(step,[status(thm)],[t6308,t170]) ).

cnf(t6310,plain,
    a9 = a17,
    inference(step,[status(thm)],[t6309,t128]) ).

cnf(t4620,plain,
    a17 = a9,
    inference(orient,[status(thm)],[t6310]) ).

cnf(t6315,plain,
    a14 = a9,
    inference(step,[status(thm)],[t4327,t4620]) ).

cnf(t4634,plain,
    a14 = a9,
    inference(orient,[status(thm)],[t6315]) ).

cnf(t6341,plain,
    product(a5,a9) = a18,
    inference(step,[status(thm)],[t4294,t4634]) ).

cnf(t6303,plain,
    a18 = a9,
    inference(step,[status(thm)],[t4299,t4552]) ).

cnf(t4575,plain,
    a18 = a9,
    inference(orient,[status(thm)],[t6303]) ).

cnf(t6342,plain,
    product(a5,a9) = a9,
    inference(step,[status(thm)],[t6341,t4575]) ).

cnf(t4676,plain,
    product(a5,a9) = a9,
    inference(orient,[status(thm)],[t6342]) ).

cnf(t4678,plain,
    a5 = product(a9,a9),
    inference(cp,[status(thm)],[t128,t4676]) ).

cnf(t6345,plain,
    a5 = a9,
    inference(step,[status(thm)],[t4678,t96]) ).

cnf(t4717,plain,
    a5 = a9,
    inference(orient,[status(thm)],[t6345]) ).

cnf(t6363,plain,
    product(a9,a6) = a4,
    inference(step,[status(thm)],[t4401,t4717]) ).

cnf(t6364,plain,
    product(a9,a9) = a4,
    inference(step,[status(thm)],[t6363,t4552]) ).

cnf(t6365,plain,
    a9 = a4,
    inference(step,[status(thm)],[t6364,t96]) ).

cnf(t4769,plain,
    a4 = a9,
    inference(orient,[status(thm)],[t6365]) ).

cnf(t6402,plain,
    a2 = a9,
    inference(step,[status(thm)],[t3540,t4769]) ).

cnf(t4806,plain,
    a2 = a9,
    inference(orient,[status(thm)],[t6402]) ).

cnf(t5971,plain,
    a31 = a4,
    inference(step,[status(thm)],[t3449,t3494]) ).

cnf(t3517,plain,
    a31 = a4,
    inference(orient,[status(thm)],[t5971]) ).

cnf(t6388,plain,
    a31 = a9,
    inference(step,[status(thm)],[t3517,t4769]) ).

cnf(t4792,plain,
    a31 = a9,
    inference(orient,[status(thm)],[t6388]) ).

cnf(t6392,plain,
    a32 = a9,
    inference(step,[status(thm)],[t3494,t4769]) ).

cnf(t4796,plain,
    a32 = a9,
    inference(orient,[status(thm)],[t6392]) ).

cnf(t6384,plain,
    a3 = a9,
    inference(step,[status(thm)],[t3512,t4769]) ).

cnf(t4788,plain,
    a3 = a9,
    inference(orient,[status(thm)],[t6384]) ).

cnf(t5914,plain,
    a25 = a32,
    inference(step,[status(thm)],[t2928,t3449]) ).

cnf(t3463,plain,
    a25 = a32,
    inference(orient,[status(thm)],[t5914]) ).

cnf(t5950,plain,
    a25 = a4,
    inference(step,[status(thm)],[t3463,t3494]) ).

cnf(t3496,plain,
    a25 = a4,
    inference(orient,[status(thm)],[t5950]) ).

cnf(t6368,plain,
    a25 = a9,
    inference(step,[status(thm)],[t3496,t4769]) ).

cnf(t4772,plain,
    a25 = a9,
    inference(orient,[status(thm)],[t6368]) ).

cnf(t5937,plain,
    a26 = a32,
    inference(step,[status(thm)],[t3182,t3478]) ).

cnf(t3481,plain,
    a26 = a32,
    inference(orient,[status(thm)],[t5937]) ).

cnf(t5956,plain,
    a26 = a4,
    inference(step,[status(thm)],[t3481,t3494]) ).

cnf(t3502,plain,
    a26 = a4,
    inference(orient,[status(thm)],[t5956]) ).

cnf(t6374,plain,
    a26 = a9,
    inference(step,[status(thm)],[t3502,t4769]) ).

cnf(t4778,plain,
    a26 = a9,
    inference(orient,[status(thm)],[t6374]) ).

cnf(t6386,plain,
    a29 = a9,
    inference(step,[status(thm)],[t3515,t4769]) ).

cnf(t4790,plain,
    a29 = a9,
    inference(orient,[status(thm)],[t6386]) ).

cnf(t5975,plain,
    a30 = a4,
    inference(step,[status(thm)],[t3478,t3494]) ).

cnf(t3521,plain,
    a30 = a4,
    inference(orient,[status(thm)],[t5975]) ).

cnf(t6390,plain,
    a30 = a9,
    inference(step,[status(thm)],[t3521,t4769]) ).

cnf(t4794,plain,
    a30 = a9,
    inference(orient,[status(thm)],[t6390]) ).

cnf(t6264,plain,
    a11 = a6,
    inference(step,[status(thm)],[t3889,t4389]) ).

cnf(t4399,plain,
    a11 = a6,
    inference(orient,[status(thm)],[t6264]) ).

cnf(t6299,plain,
    a11 = a9,
    inference(step,[status(thm)],[t4399,t4552]) ).

cnf(t4571,plain,
    a11 = a9,
    inference(orient,[status(thm)],[t6299]) ).

cnf(t6095,plain,
    product(a13,a5) = a12,
    inference(step,[status(thm)],[t165,t3602]) ).

cnf(t3609,plain,
    product(a13,a5) = a12,
    inference(rw,[status(thm)],[t6095]) ).

cnf(t4033,plain,
    product(a13,a5) = a12,
    inference(orient,[status(thm)],[t3609]) ).

cnf(t6267,plain,
    product(a6,a5) = a12,
    inference(step,[status(thm)],[t4033,t4389]) ).

cnf(t4402,plain,
    product(a6,a5) = a12,
    inference(rw,[status(thm)],[t6267]) ).

cnf(t6421,plain,
    product(a9,a5) = a12,
    inference(step,[status(thm)],[t4402,t4552]) ).

cnf(t6422,plain,
    product(a9,a9) = a12,
    inference(step,[status(thm)],[t6421,t4717]) ).

cnf(t6423,plain,
    a9 = a12,
    inference(step,[status(thm)],[t6422,t96]) ).

cnf(t4825,plain,
    a12 = a9,
    inference(orient,[status(thm)],[t6423]) ).

cnf(t6312,plain,
    a15 = a9,
    inference(step,[status(thm)],[t3937,t4620]) ).

cnf(t4630,plain,
    a15 = a9,
    inference(orient,[status(thm)],[t6312]) ).

cnf(t232,plain,
    product(product(a9,X1),a17) = product(a10,product(X1,a17)),
    inference(cp,[status(thm)],[t170,t127]) ).

cnf(t934,plain,
    product(product(a9,X1),a17) = product(a10,product(X1,a17)),
    inference(orient,[status(thm)],[t232]) ).

cnf(t935,plain,
    product(a10,product(a5,a17)) = product(a8,a17),
    inference(cp,[status(thm)],[t934,t319]) ).

cnf(t2142,plain,
    product(a10,product(a5,a17)) = product(a8,a17),
    inference(orient,[status(thm)],[t935]) ).

cnf(t6199,plain,
    product(a10,a18) = product(a8,a17),
    inference(step,[status(thm)],[t2142,t4044]) ).

cnf(t4045,plain,
    product(a10,a18) = product(a8,a17),
    inference(rw,[status(thm)],[t6199]) ).

cnf(t6319,plain,
    a10 = a9,
    inference(step,[status(thm)],[t4373,t4620]) ).

cnf(t4638,plain,
    a10 = a9,
    inference(orient,[status(thm)],[t6319]) ).

cnf(t6321,plain,
    product(a9,a18) = product(a8,a17),
    inference(step,[status(thm)],[t4045,t4638]) ).

cnf(t6322,plain,
    product(a9,a9) = product(a8,a17),
    inference(step,[status(thm)],[t6321,t4575]) ).

cnf(t6323,plain,
    a9 = product(a8,a17),
    inference(step,[status(thm)],[t6322,t96]) ).

cnf(t6324,plain,
    a9 = product(a8,a9),
    inference(step,[status(thm)],[t6323,t4620]) ).

cnf(t4640,plain,
    product(a8,a9) = a9,
    inference(orient,[status(thm)],[t6324]) ).

cnf(t4643,plain,
    a8 = product(a9,a9),
    inference(cp,[status(thm)],[t128,t4640]) ).

cnf(t6327,plain,
    a8 = a9,
    inference(step,[status(thm)],[t4643,t96]) ).

cnf(t4654,plain,
    a8 = a9,
    inference(orient,[status(thm)],[t6327]) ).

cnf(t6338,plain,
    a16 = a9,
    inference(step,[status(thm)],[t4528,t4654]) ).

cnf(t4671,plain,
    a16 = a9,
    inference(orient,[status(thm)],[t6338]) ).

cnf(t6094,plain,
    product(a7,a5) = a8,
    inference(step,[status(thm)],[t125,t3602]) ).

cnf(t3608,plain,
    product(a7,a5) = a8,
    inference(rw,[status(thm)],[t6094]) ).

cnf(t4001,plain,
    product(a7,a5) = a8,
    inference(orient,[status(thm)],[t3608]) ).

cnf(t4003,plain,
    a7 = product(a8,a5),
    inference(cp,[status(thm)],[t128,t4001]) ).

cnf(t6189,plain,
    a7 = a9,
    inference(step,[status(thm)],[t4003,t126]) ).

cnf(t4010,plain,
    a7 = a9,
    inference(orient,[status(thm)],[t6189]) ).

cnf(t6352,plain,
    a19 = a9,
    inference(step,[status(thm)],[t3602,t4717]) ).

cnf(t4731,plain,
    a19 = a9,
    inference(orient,[status(thm)],[t6352]) ).

cnf(t6406,plain,
    a20 = a9,
    inference(step,[status(thm)],[t3547,t4769]) ).

cnf(t4810,plain,
    a20 = a9,
    inference(orient,[status(thm)],[t6406]) ).

cnf(t6305,plain,
    a13 = a9,
    inference(step,[status(thm)],[t4389,t4552]) ).

cnf(t4578,plain,
    a13 = a9,
    inference(orient,[status(thm)],[t6305]) ).

cnf(t5838,plain,
    a21 = a32,
    inference(step,[status(thm)],[t3113,t3314]) ).

cnf(t3351,plain,
    a21 = a32,
    inference(orient,[status(thm)],[t5838]) ).

cnf(t5954,plain,
    a21 = a4,
    inference(step,[status(thm)],[t3351,t3494]) ).

cnf(t3500,plain,
    a21 = a4,
    inference(orient,[status(thm)],[t5954]) ).

cnf(t6372,plain,
    a21 = a9,
    inference(step,[status(thm)],[t3500,t4769]) ).

cnf(t4776,plain,
    a21 = a9,
    inference(orient,[status(thm)],[t6372]) ).

cnf(t3320,plain,
    product(a32,a31) = a22,
    inference(rw,[status(thm)],[t272]) ).

cnf(t5989,plain,
    product(a4,a31) = a22,
    inference(step,[status(thm)],[t3320,t3494]) ).

cnf(t5990,plain,
    product(a4,a4) = a22,
    inference(step,[status(thm)],[t5989,t3517]) ).

cnf(t5991,plain,
    a4 = a22,
    inference(step,[status(thm)],[t5990,t96]) ).

cnf(t3528,plain,
    a22 = a4,
    inference(orient,[status(thm)],[t5991]) ).

cnf(t6397,plain,
    a22 = a9,
    inference(step,[status(thm)],[t3528,t4769]) ).

cnf(t4801,plain,
    a22 = a9,
    inference(orient,[status(thm)],[t6397]) ).

cnf(t5964,plain,
    a23 = a4,
    inference(step,[status(thm)],[t3314,t3494]) ).

cnf(t3510,plain,
    a23 = a4,
    inference(orient,[status(thm)],[t5964]) ).

cnf(t6382,plain,
    a23 = a9,
    inference(step,[status(thm)],[t3510,t4769]) ).

cnf(t4786,plain,
    a23 = a9,
    inference(orient,[status(thm)],[t6382]) ).

cnf(t5958,plain,
    a24 = a4,
    inference(step,[status(thm)],[t3201,t3494]) ).

cnf(t3504,plain,
    a24 = a4,
    inference(orient,[status(thm)],[t5958]) ).

cnf(t6376,plain,
    a24 = a9,
    inference(step,[status(thm)],[t3504,t4769]) ).

cnf(t4780,plain,
    a24 = a9,
    inference(orient,[status(thm)],[t6376]) ).

cnf(t5962,plain,
    a27 = a4,
    inference(step,[status(thm)],[t3468,t3494]) ).

cnf(t3508,plain,
    a27 = a4,
    inference(orient,[status(thm)],[t5962]) ).

cnf(t6380,plain,
    a27 = a9,
    inference(step,[status(thm)],[t3508,t4769]) ).

cnf(t4784,plain,
    a27 = a9,
    inference(orient,[status(thm)],[t6380]) ).

cnf(t5939,plain,
    a28 = a32,
    inference(step,[status(thm)],[t3244,t3478]) ).

cnf(t3483,plain,
    a28 = a32,
    inference(orient,[status(thm)],[t5939]) ).

cnf(t5960,plain,
    a28 = a4,
    inference(step,[status(thm)],[t3483,t3494]) ).

cnf(t3506,plain,
    a28 = a4,
    inference(orient,[status(thm)],[t5960]) ).

cnf(t6378,plain,
    a28 = a9,
    inference(step,[status(thm)],[t3506,t4769]) ).

cnf(t4782,plain,
    a28 = a9,
    inference(orient,[status(thm)],[t6378]) ).

cnf(t5873,plain,
    a1 = a32,
    inference(step,[status(thm)],[t3033,t3360]) ).

cnf(t3402,plain,
    a1 = a32,
    inference(orient,[status(thm)],[t5873]) ).

cnf(t5952,plain,
    a1 = a4,
    inference(step,[status(thm)],[t3402,t3494]) ).

cnf(t3498,plain,
    a1 = a4,
    inference(orient,[status(thm)],[t5952]) ).

cnf(t6370,plain,
    a1 = a9,
    inference(step,[status(thm)],[t3498,t4769]) ).

cnf(t4774,plain,
    a1 = a9,
    inference(orient,[status(thm)],[t6370]) ).

cnf(goal_0,negated_conjecture,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a2),a31),a32),a3),a25),a26),a4),a29),a30),a5),a11),a12),a6),a15),a16),a7),a8),a19),a20),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(g0_0,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a31),a32),a3),a25),a26),a4),a29),a30),a5),a11),a12),a6),a15),a16),a7),a8),a19),a20),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[goal_0,t4806]) ).

cnf(g0_1,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a32),a3),a25),a26),a4),a29),a30),a5),a11),a12),a6),a15),a16),a7),a8),a19),a20),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_0,t4792]) ).

cnf(g0_2,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a3),a25),a26),a4),a29),a30),a5),a11),a12),a6),a15),a16),a7),a8),a19),a20),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_1,t4796]) ).

cnf(g0_3,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a25),a26),a4),a29),a30),a5),a11),a12),a6),a15),a16),a7),a8),a19),a20),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_2,t4788]) ).

cnf(g0_4,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a26),a4),a29),a30),a5),a11),a12),a6),a15),a16),a7),a8),a19),a20),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_3,t4772]) ).

cnf(g0_5,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a4),a29),a30),a5),a11),a12),a6),a15),a16),a7),a8),a19),a20),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_4,t4778]) ).

cnf(g0_6,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a29),a30),a5),a11),a12),a6),a15),a16),a7),a8),a19),a20),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_5,t4769]) ).

cnf(g0_7,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a30),a5),a11),a12),a6),a15),a16),a7),a8),a19),a20),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_6,t4790]) ).

cnf(g0_8,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a5),a11),a12),a6),a15),a16),a7),a8),a19),a20),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_7,t4794]) ).

cnf(g0_9,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a11),a12),a6),a15),a16),a7),a8),a19),a20),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_8,t4717]) ).

cnf(g0_10,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a12),a6),a15),a16),a7),a8),a19),a20),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_9,t4571]) ).

cnf(g0_11,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a6),a15),a16),a7),a8),a19),a20),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_10,t4825]) ).

cnf(g0_12,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a15),a16),a7),a8),a19),a20),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_11,t4552]) ).

cnf(g0_13,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a16),a7),a8),a19),a20),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_12,t4630]) ).

cnf(g0_14,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a7),a8),a19),a20),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_13,t4671]) ).

cnf(g0_15,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a8),a19),a20),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_14,t4010]) ).

cnf(g0_16,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a19),a20),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_15,t4654]) ).

cnf(g0_17,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a20),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_16,t4731]) ).

cnf(g0_18,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a10),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_17,t4810]) ).

cnf(g0_19,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a17),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_18,t4638]) ).

cnf(g0_20,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a18),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_19,t4620]) ).

cnf(g0_21,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a13),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_20,t4575]) ).

cnf(g0_22,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a14),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_21,t4578]) ).

cnf(g0_23,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a21),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_22,t4634]) ).

cnf(g0_24,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a22),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_23,t4776]) ).

cnf(g0_25,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a23),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_24,t4801]) ).

cnf(g0_26,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a24),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_25,t4786]) ).

cnf(g0_27,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a27),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_26,t4780]) ).

cnf(g0_28,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a28) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_27,t4784]) ).

cnf(g0_29,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_28,t4782]) ).

cnf(g0_30,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a30),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_29,t4774]) ).

cnf(g0_31,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a31),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_30,t4794]) ).

cnf(g0_32,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a2),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_31,t4792]) ).

cnf(g0_33,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a24),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_32,t4806]) ).

cnf(g0_34,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a25),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_33,t4780]) ).

cnf(g0_35,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a3),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_34,t4772]) ).

cnf(g0_36,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a28),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_35,t4788]) ).

cnf(g0_37,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a29),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_36,t4782]) ).

cnf(g0_38,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a4),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_37,t4790]) ).

cnf(g0_39,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a10),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_38,t4769]) ).

cnf(g0_40,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a11),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_39,t4638]) ).

cnf(g0_41,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a5),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_40,t4571]) ).

cnf(g0_42,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a14),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_41,t4717]) ).

cnf(g0_43,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a15),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_42,t4634]) ).

cnf(g0_44,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a6),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_43,t4630]) ).

cnf(g0_45,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a7),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_44,t4552]) ).

cnf(g0_46,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a18),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_45,t4010]) ).

cnf(g0_47,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a19),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_46,t4575]) ).

cnf(g0_48,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a8),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_47,t4731]) ).

cnf(g0_49,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a16),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_48,t4654]) ).

cnf(g0_50,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a17),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_49,t4671]) ).

cnf(g0_51,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a12),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_50,t4620]) ).

cnf(g0_52,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a13),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_51,t4825]) ).

cnf(g0_53,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a20),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_52,t4578]) ).

cnf(g0_54,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a21),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_53,t4810]) ).

cnf(g0_55,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a22),a23),a26),a27),
    inference(rw,[status(thm)],[g0_54,t4776]) ).

cnf(g0_56,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a23),a26),a27),
    inference(rw,[status(thm)],[g0_55,t4801]) ).

cnf(g0_57,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a26),a27),
    inference(rw,[status(thm)],[g0_56,t4786]) ).

cnf(g0_58,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a27),
    inference(rw,[status(thm)],[g0_57,t4778]) ).

cnf(g0_59,plain,
    ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),
    inference(rw,[status(thm)],[g0_58,t4784]) ).

cnf(contradiction_0,plain,
    $false,
    inference(trivial_inequality_removal,[status(thm)],[g0_59]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : TOP050-1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04  % Command  : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35  % Computer : n019.cluster.edu
% 0.09/0.35  % Model    : x86_64 x86_64
% 0.09/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35  % Memory   : 8046.5625MB
% 0.09/0.35  % OS       : Linux 6.8.0-71-generic
% 0.09/0.35  % CPULimit : 300
% 0.09/0.35  % WCLimit  : 300
% 0.09/0.35  % DateTime : Fri Sep 25 04:20:03 UTC 2026
% 0.09/0.36  % CPUTime  : 
% 0.09/0.36  Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 27.35/3.94  % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.35/3.94  % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------