%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : TOP053-1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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 : Sun Sep 27 09:53:08 AM UTC 2026
% Result : Unsatisfiable 0.22s 5.70s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 97
% Number of leaves : 19
% Syntax : Number of formulae : 313 ( 313 unt; 0 def)
% Number of atoms : 313 ( 312 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 53 ( 53 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 15 con; 0-14 aty)
% Number of variables : 65 ( 0 sgn 6 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(involutory_quandle,axiom,
! [VAR_0] : product(VAR_0,VAR_0) = VAR_0,
file('theBenchmark.p',involutory_quandle) ).
cnf(c_1,plain,
product(A,A) = A,
inference(clausify,[status(thm)],[involutory_quandle]) ).
fof(involutory_quandle_01,axiom,
! [VAR_0,VAR_1] : product(product(VAR_0,VAR_1),VAR_1) = VAR_0,
file('theBenchmark.p',involutory_quandle_01) ).
cnf(c_2,plain,
product(product(A,B),B) = A,
inference(clausify,[status(thm)],[involutory_quandle_01]) ).
fof(involutory_quandle_02,axiom,
! [VAR_0,VAR_1,VAR_2] : product(product(VAR_0,VAR_1),VAR_2) = product(product(VAR_0,VAR_2),product(VAR_1,VAR_2)),
file('theBenchmark.p',involutory_quandle_02) ).
cnf(c_3,plain,
product(product(A,B),C) = product(product(A,C),product(B,C)),
inference(clausify,[status(thm)],[involutory_quandle_02]) ).
cnf(c_4,plain,
product(product(A,B),product(C,B)) = product(product(A,C),B),
inference(copy,[status(thm)],[c_3]) ).
fof(knot,axiom,
product(a1,a2) = a3,
file('theBenchmark.p',knot) ).
cnf(c_5,plain,
product(a1,a2) = a3,
inference(clausify,[status(thm)],[knot]) ).
fof(knot_03,axiom,
product(a3,a4) = a5,
file('theBenchmark.p',knot_03) ).
cnf(c_6,plain,
product(a3,a4) = a5,
inference(clausify,[status(thm)],[knot_03]) ).
fof(knot_04,axiom,
product(a5,a6) = a7,
file('theBenchmark.p',knot_04) ).
cnf(c_7,plain,
product(a5,a6) = a7,
inference(clausify,[status(thm)],[knot_04]) ).
fof(knot_05,axiom,
product(a7,a3) = a8,
file('theBenchmark.p',knot_05) ).
cnf(c_8,plain,
product(a7,a3) = a8,
inference(clausify,[status(thm)],[knot_05]) ).
fof(knot_06,axiom,
product(a8,a2) = a9,
file('theBenchmark.p',knot_06) ).
cnf(c_9,plain,
product(a8,a2) = a9,
inference(clausify,[status(thm)],[knot_06]) ).
fof(knot_07,axiom,
product(a9,a1) = a10,
file('theBenchmark.p',knot_07) ).
cnf(c_10,plain,
product(a9,a1) = a10,
inference(clausify,[status(thm)],[knot_07]) ).
fof(knot_08,axiom,
product(a10,a11) = a12,
file('theBenchmark.p',knot_08) ).
cnf(c_11,plain,
product(a10,a11) = a12,
inference(clausify,[status(thm)],[knot_08]) ).
fof(knot_09,axiom,
product(a12,a3) = a13,
file('theBenchmark.p',knot_09) ).
cnf(c_12,plain,
product(a12,a3) = a13,
inference(clausify,[status(thm)],[knot_09]) ).
fof(knot_10,axiom,
product(a13,a8) = a6,
file('theBenchmark.p',knot_10) ).
cnf(c_13,plain,
product(a13,a8) = a6,
inference(clausify,[status(thm)],[knot_10]) ).
fof(knot_11,axiom,
product(a6,a7) = a2,
file('theBenchmark.p',knot_11) ).
cnf(c_14,plain,
product(a6,a7) = a2,
inference(clausify,[status(thm)],[knot_11]) ).
fof(knot_12,axiom,
product(a2,a12) = a14,
file('theBenchmark.p',knot_12) ).
cnf(c_15,plain,
product(a2,a12) = a14,
inference(clausify,[status(thm)],[knot_12]) ).
fof(knot_13,axiom,
product(a14,a3) = a15,
file('theBenchmark.p',knot_13) ).
cnf(c_16,plain,
product(a14,a3) = a15,
inference(clausify,[status(thm)],[knot_13]) ).
fof(knot_14,axiom,
product(a15,a8) = a4,
file('theBenchmark.p',knot_14) ).
cnf(c_17,plain,
product(a15,a8) = a4,
inference(clausify,[status(thm)],[knot_14]) ).
fof(knot_15,axiom,
product(a4,a7) = a11,
file('theBenchmark.p',knot_15) ).
cnf(c_18,plain,
product(a4,a7) = a11,
inference(clausify,[status(thm)],[knot_15]) ).
fof(knot_16,axiom,
product(a11,a10) = a1,
file('theBenchmark.p',knot_16) ).
cnf(c_19,plain,
product(a11,a10) = a1,
inference(clausify,[status(thm)],[knot_16]) ).
fof(goal,axiom,
tuple(a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14) != tuple(a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15),
file('theBenchmark.p',goal) ).
cnf(c_20,plain,
tuple(a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14) != tuple(a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15),
inference(clausify,[status(thm)],[goal]) ).
cnf(c_1383,plain,
product(A,product(B,A)) = product(product(A,B),A),
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_21,plain,
product(product(A,B),A) = product(A,product(B,A)),
inference(copy,[status(thm)],[c_1383]) ).
cnf(c_1384,plain,
product(A,product(B,C)) = product(product(product(A,C),B),C),
inference(paramod,[status(thm)],[c_2,c_4]) ).
cnf(c_22,plain,
product(product(product(A,B),C),B) = product(A,product(C,B)),
inference(copy,[status(thm)],[c_1384]) ).
cnf(c_1385,plain,
product(product(A,B),C) = product(product(A,product(C,B)),B),
inference(paramod,[status(thm)],[c_2,c_4]) ).
cnf(c_23,plain,
product(product(A,product(B,C)),C) = product(product(A,C),B),
inference(copy,[status(thm)],[c_1385]) ).
cnf(c_26,plain,
product(a3,a2) = a1,
inference(paramod,[status(thm)],[c_5,c_2]) ).
cnf(c_1386,plain,
product(a3,product(A,a2)) = product(product(a1,A),a2),
inference(paramod,[status(thm)],[c_5,c_4]) ).
cnf(c_27,plain,
product(product(a1,A),a2) = product(a3,product(A,a2)),
inference(copy,[status(thm)],[c_1386]) ).
cnf(c_1387,plain,
product(product(A,a2),a3) = product(product(A,a1),a2),
inference(paramod,[status(thm)],[c_5,c_4]) ).
cnf(c_28,plain,
product(product(A,a1),a2) = product(product(A,a2),a3),
inference(copy,[status(thm)],[c_1387]) ).
cnf(c_29,plain,
product(a5,a4) = a3,
inference(paramod,[status(thm)],[c_6,c_2]) ).
cnf(c_32,plain,
product(a7,a6) = a5,
inference(paramod,[status(thm)],[c_7,c_2]) ).
cnf(c_1388,plain,
product(a7,product(A,a6)) = product(product(a5,A),a6),
inference(paramod,[status(thm)],[c_7,c_4]) ).
cnf(c_33,plain,
product(product(a5,A),a6) = product(a7,product(A,a6)),
inference(copy,[status(thm)],[c_1388]) ).
cnf(c_1389,plain,
product(product(A,a6),a7) = product(product(A,a5),a6),
inference(paramod,[status(thm)],[c_7,c_4]) ).
cnf(c_34,plain,
product(product(A,a5),a6) = product(product(A,a6),a7),
inference(copy,[status(thm)],[c_1389]) ).
cnf(c_35,plain,
product(a8,a3) = a7,
inference(paramod,[status(thm)],[c_8,c_2]) ).
cnf(c_1390,plain,
product(a8,product(A,a3)) = product(product(a7,A),a3),
inference(paramod,[status(thm)],[c_8,c_4]) ).
cnf(c_36,plain,
product(product(a7,A),a3) = product(a8,product(A,a3)),
inference(copy,[status(thm)],[c_1390]) ).
cnf(c_1391,plain,
product(product(A,a3),a8) = product(product(A,a7),a3),
inference(paramod,[status(thm)],[c_8,c_4]) ).
cnf(c_37,plain,
product(product(A,a7),a3) = product(product(A,a3),a8),
inference(copy,[status(thm)],[c_1391]) ).
cnf(c_38,plain,
product(a9,a2) = a8,
inference(paramod,[status(thm)],[c_9,c_2]) ).
cnf(c_1392,plain,
product(a9,product(A,a2)) = product(product(a8,A),a2),
inference(paramod,[status(thm)],[c_9,c_4]) ).
cnf(c_39,plain,
product(product(a8,A),a2) = product(a9,product(A,a2)),
inference(copy,[status(thm)],[c_1392]) ).
cnf(c_41,plain,
product(a10,a1) = a9,
inference(paramod,[status(thm)],[c_10,c_2]) ).
cnf(c_44,plain,
product(a12,a11) = a10,
inference(paramod,[status(thm)],[c_11,c_2]) ).
cnf(c_47,plain,
product(a13,a3) = a12,
inference(paramod,[status(thm)],[c_12,c_2]) ).
cnf(c_53,plain,
product(a2,a7) = a6,
inference(paramod,[status(thm)],[c_14,c_2]) ).
cnf(c_1393,plain,
product(product(A,a7),a2) = product(product(A,a6),a7),
inference(paramod,[status(thm)],[c_14,c_4]) ).
cnf(c_55,plain,
product(product(A,a6),a7) = product(product(A,a7),a2),
inference(copy,[status(thm)],[c_1393]) ).
cnf(c_56,plain,
product(product(A,a5),a6) = product(product(A,a7),a2),
inference(paramod,[status(thm)],[c_55,c_34]) ).
cnf(c_57,plain,
product(a14,a12) = a2,
inference(paramod,[status(thm)],[c_15,c_2]) ).
cnf(c_66,plain,
product(a11,a7) = a4,
inference(paramod,[status(thm)],[c_18,c_2]) ).
cnf(c_69,plain,
product(a1,a10) = a11,
inference(paramod,[status(thm)],[c_19,c_2]) ).
cnf(c_1394,plain,
product(product(A,a10),a1) = product(product(A,a11),a10),
inference(paramod,[status(thm)],[c_19,c_4]) ).
cnf(c_71,plain,
product(product(A,a11),a10) = product(product(A,a10),a1),
inference(copy,[status(thm)],[c_1394]) ).
cnf(c_1395,plain,
product(a5,a3) = product(a3,product(a4,a3)),
inference(paramod,[status(thm)],[c_6,c_21]) ).
cnf(c_77,plain,
product(a3,product(a4,a3)) = product(a5,a3),
inference(copy,[status(thm)],[c_1395]) ).
cnf(c_1396,plain,
product(a14,a2) = product(a2,product(a12,a2)),
inference(paramod,[status(thm)],[c_15,c_21]) ).
cnf(c_88,plain,
product(a2,product(a12,a2)) = product(a14,a2),
inference(copy,[status(thm)],[c_1396]) ).
cnf(c_1397,plain,
product(a3,a5) = product(a5,product(a4,a5)),
inference(paramod,[status(thm)],[c_29,c_21]) ).
cnf(c_99,plain,
product(a5,product(a4,a5)) = product(a3,a5),
inference(copy,[status(thm)],[c_1397]) ).
cnf(c_1398,plain,
product(product(A,a1),a9) = product(product(A,a10),a1),
inference(paramod,[status(thm)],[c_41,c_4]) ).
cnf(c_109,plain,
product(product(A,a10),a1) = product(product(A,a1),a9),
inference(copy,[status(thm)],[c_1398]) ).
cnf(c_1399,plain,
product(a9,a10) = product(a10,product(a1,a10)),
inference(paramod,[status(thm)],[c_41,c_21]) ).
cnf(c_1400,plain,
product(a9,a10) = product(a10,a11),
inference(paramod,[status(thm)],[c_69,c_1399]) ).
cnf(c_110,plain,
product(a9,a10) = a12,
inference(paramod,[status(thm)],[c_11,c_1400]) ).
cnf(c_112,plain,
product(product(A,a11),a10) = product(product(A,a1),a9),
inference(paramod,[status(thm)],[c_109,c_71]) ).
cnf(c_120,plain,
product(product(a6,A),a8) = product(a13,product(A,a8)),
inference(paramod,[status(thm)],[c_13,c_22]) ).
cnf(c_124,plain,
product(product(a4,A),a8) = product(a15,product(A,a8)),
inference(paramod,[status(thm)],[c_17,c_22]) ).
cnf(c_1401,plain,
product(product(product(a12,a2),a2),product(a12,a2)) = product(product(a12,a2),product(a14,a2)),
inference(paramod,[status(thm)],[c_88,c_21]) ).
cnf(c_1402,plain,
product(a12,product(a12,a2)) = product(product(a12,a2),product(a14,a2)),
inference(paramod,[status(thm)],[c_2,c_1401]) ).
cnf(c_1403,plain,
product(a12,product(a12,a2)) = product(product(a12,a14),a2),
inference(paramod,[status(thm)],[c_4,c_1402]) ).
cnf(c_377,plain,
product(product(a12,a14),a2) = product(a12,product(a12,a2)),
inference(copy,[status(thm)],[c_1403]) ).
cnf(c_1404,plain,
product(a11,a2) = product(a3,product(a10,a2)),
inference(paramod,[status(thm)],[c_69,c_27]) ).
cnf(c_395,plain,
product(a3,product(a10,a2)) = product(a11,a2),
inference(copy,[status(thm)],[c_1404]) ).
cnf(c_1405,plain,
product(a10,a2) = product(product(a9,a2),a3),
inference(paramod,[status(thm)],[c_10,c_28]) ).
cnf(c_1406,plain,
product(a10,a2) = product(a8,a3),
inference(paramod,[status(thm)],[c_38,c_1405]) ).
cnf(c_457,plain,
product(a10,a2) = a7,
inference(paramod,[status(thm)],[c_35,c_1406]) ).
cnf(c_1407,plain,
product(a3,a7) = product(a11,a2),
inference(paramod,[status(thm)],[c_457,c_395]) ).
cnf(c_466,plain,
product(a11,a2) = product(a3,a7),
inference(copy,[status(thm)],[c_1407]) ).
cnf(c_467,plain,
product(a7,a2) = a10,
inference(paramod,[status(thm)],[c_457,c_2]) ).
cnf(c_1408,plain,
product(a7,product(A,a2)) = product(product(a10,A),a2),
inference(paramod,[status(thm)],[c_457,c_4]) ).
cnf(c_468,plain,
product(product(a10,A),a2) = product(a7,product(A,a2)),
inference(copy,[status(thm)],[c_1408]) ).
cnf(c_472,plain,
product(product(A,a7),a2) = product(product(A,a2),a10),
inference(paramod,[status(thm)],[c_457,c_23]) ).
cnf(c_493,plain,
product(product(A,a5),a6) = product(product(A,a2),a10),
inference(paramod,[status(thm)],[c_472,c_56]) ).
cnf(c_507,plain,
product(product(A,product(a3,a7)),a2) = product(product(A,a2),a11),
inference(paramod,[status(thm)],[c_466,c_23]) ).
cnf(c_1409,plain,
product(product(a3,a5),a6) = product(a7,product(product(a4,a5),a6)),
inference(paramod,[status(thm)],[c_99,c_33]) ).
cnf(c_1410,plain,
product(product(a3,a2),a10) = product(a7,product(product(a4,a5),a6)),
inference(paramod,[status(thm)],[c_493,c_1409]) ).
cnf(c_1411,plain,
product(a1,a10) = product(a7,product(product(a4,a5),a6)),
inference(paramod,[status(thm)],[c_26,c_1410]) ).
cnf(c_1412,plain,
a11 = product(a7,product(product(a4,a5),a6)),
inference(paramod,[status(thm)],[c_69,c_1411]) ).
cnf(c_1413,plain,
a11 = product(a7,product(product(a4,a2),a10)),
inference(paramod,[status(thm)],[c_493,c_1412]) ).
cnf(c_670,plain,
product(a7,product(product(a4,a2),a10)) = a11,
inference(copy,[status(thm)],[c_1413]) ).
cnf(c_1414,plain,
product(a5,a3) = product(a8,product(a6,a3)),
inference(paramod,[status(thm)],[c_32,c_36]) ).
cnf(c_733,plain,
product(a8,product(a6,a3)) = product(a5,a3),
inference(copy,[status(thm)],[c_1414]) ).
cnf(c_1415,plain,
product(product(a7,a1),a2) = product(a8,product(a2,a3)),
inference(paramod,[status(thm)],[c_36,c_28]) ).
cnf(c_1416,plain,
product(product(a7,a2),a3) = product(a8,product(a2,a3)),
inference(paramod,[status(thm)],[c_28,c_1415]) ).
cnf(c_1417,plain,
product(a10,a3) = product(a8,product(a2,a3)),
inference(paramod,[status(thm)],[c_467,c_1416]) ).
cnf(c_739,plain,
product(a8,product(a2,a3)) = product(a10,a3),
inference(copy,[status(thm)],[c_1417]) ).
cnf(c_1418,plain,
product(a2,a3) = product(product(a6,a3),a8),
inference(paramod,[status(thm)],[c_14,c_37]) ).
cnf(c_1419,plain,
product(a2,a3) = product(a13,product(a3,a8)),
inference(paramod,[status(thm)],[c_120,c_1418]) ).
cnf(c_801,plain,
product(a13,product(a3,a8)) = product(a2,a3),
inference(copy,[status(thm)],[c_1419]) ).
cnf(c_1420,plain,
product(a11,a3) = product(product(a4,a3),a8),
inference(paramod,[status(thm)],[c_18,c_37]) ).
cnf(c_1421,plain,
product(a11,a3) = product(a15,product(a3,a8)),
inference(paramod,[status(thm)],[c_124,c_1420]) ).
cnf(c_802,plain,
product(a15,product(a3,a8)) = product(a11,a3),
inference(copy,[status(thm)],[c_1421]) ).
cnf(c_822,plain,
product(product(a2,a3),product(a3,a8)) = a13,
inference(paramod,[status(thm)],[c_801,c_2]) ).
cnf(c_834,plain,
product(product(a11,a3),product(a3,a8)) = a15,
inference(paramod,[status(thm)],[c_802,c_2]) ).
cnf(c_1422,plain,
product(product(a5,a3),a2) = product(a9,product(product(a6,a3),a2)),
inference(paramod,[status(thm)],[c_733,c_39]) ).
cnf(c_876,plain,
product(a9,product(product(a6,a3),a2)) = product(product(a5,a3),a2),
inference(copy,[status(thm)],[c_1422]) ).
cnf(c_1423,plain,
product(product(a10,a3),a2) = product(a9,product(product(a2,a3),a2)),
inference(paramod,[status(thm)],[c_739,c_39]) ).
cnf(c_1424,plain,
product(a7,product(a3,a2)) = product(a9,product(product(a2,a3),a2)),
inference(paramod,[status(thm)],[c_468,c_1423]) ).
cnf(c_1425,plain,
product(a7,a1) = product(a9,product(product(a2,a3),a2)),
inference(paramod,[status(thm)],[c_26,c_1424]) ).
cnf(c_1426,plain,
product(a7,a1) = product(a9,product(a2,product(a3,a2))),
inference(paramod,[status(thm)],[c_21,c_1425]) ).
cnf(c_1427,plain,
product(a7,a1) = product(a9,product(a2,a1)),
inference(paramod,[status(thm)],[c_26,c_1426]) ).
cnf(c_877,plain,
product(a9,product(a2,a1)) = product(a7,a1),
inference(copy,[status(thm)],[c_1427]) ).
cnf(c_1428,plain,
product(product(a7,a1),a9) = product(a9,product(product(a2,a1),a9)),
inference(paramod,[status(thm)],[c_877,c_21]) ).
cnf(c_884,plain,
product(a9,product(product(a2,a1),a9)) = product(product(a7,a1),a9),
inference(copy,[status(thm)],[c_1428]) ).
cnf(c_1429,plain,
product(a13,a3) = product(a2,product(product(a3,a8),a3)),
inference(paramod,[status(thm)],[c_822,c_22]) ).
cnf(c_1430,plain,
a12 = product(a2,product(product(a3,a8),a3)),
inference(paramod,[status(thm)],[c_47,c_1429]) ).
cnf(c_1431,plain,
a12 = product(a2,product(a3,product(a8,a3))),
inference(paramod,[status(thm)],[c_21,c_1430]) ).
cnf(c_1432,plain,
a12 = product(a2,product(a3,a7)),
inference(paramod,[status(thm)],[c_35,c_1431]) ).
cnf(c_891,plain,
product(a2,product(a3,a7)) = a12,
inference(copy,[status(thm)],[c_1432]) ).
cnf(c_896,plain,
product(a12,product(a3,a7)) = a2,
inference(paramod,[status(thm)],[c_891,c_2]) ).
cnf(c_1433,plain,
product(a12,a2) = product(a2,product(product(a3,a7),a2)),
inference(paramod,[status(thm)],[c_891,c_21]) ).
cnf(c_1434,plain,
product(a12,a2) = product(a2,product(product(a3,a2),a10)),
inference(paramod,[status(thm)],[c_472,c_1433]) ).
cnf(c_1435,plain,
product(a12,a2) = product(a2,product(a1,a10)),
inference(paramod,[status(thm)],[c_26,c_1434]) ).
cnf(c_899,plain,
product(a12,a2) = product(a2,a11),
inference(paramod,[status(thm)],[c_69,c_1435]) ).
cnf(c_1436,plain,
product(product(product(a3,a7),a2),product(a3,a7)) = product(product(a3,a7),a12),
inference(paramod,[status(thm)],[c_891,c_21]) ).
cnf(c_1437,plain,
product(product(product(a3,a2),a10),product(a3,a7)) = product(product(a3,a7),a12),
inference(paramod,[status(thm)],[c_472,c_1436]) ).
cnf(c_1438,plain,
product(product(a1,a10),product(a3,a7)) = product(product(a3,a7),a12),
inference(paramod,[status(thm)],[c_26,c_1437]) ).
cnf(c_1439,plain,
product(a11,product(a3,a7)) = product(product(a3,a7),a12),
inference(paramod,[status(thm)],[c_69,c_1438]) ).
cnf(c_900,plain,
product(product(a3,a7),a12) = product(a11,product(a3,a7)),
inference(copy,[status(thm)],[c_1439]) ).
cnf(c_1440,plain,
product(product(product(A,product(a3,a7)),a2),product(a3,a7)) = product(A,a12),
inference(paramod,[status(thm)],[c_891,c_22]) ).
cnf(c_902,plain,
product(product(product(A,a2),a11),product(a3,a7)) = product(A,a12),
inference(paramod,[status(thm)],[c_507,c_1440]) ).
cnf(c_1441,plain,
product(a12,a7) = product(product(a2,a7),a3),
inference(paramod,[status(thm)],[c_891,c_23]) ).
cnf(c_1442,plain,
product(a12,a7) = product(a6,a3),
inference(paramod,[status(thm)],[c_53,c_1441]) ).
cnf(c_904,plain,
product(a6,a3) = product(a12,a7),
inference(copy,[status(thm)],[c_1442]) ).
cnf(c_915,plain,
product(product(a12,a14),a2) = product(a12,product(a2,a11)),
inference(paramod,[status(thm)],[c_899,c_377]) ).
cnf(c_917,plain,
product(a2,product(a2,a11)) = product(a14,a2),
inference(paramod,[status(thm)],[c_899,c_88]) ).
cnf(c_1443,plain,
product(a9,product(product(a12,a7),a2)) = product(product(a5,a3),a2),
inference(paramod,[status(thm)],[c_904,c_876]) ).
cnf(c_1444,plain,
product(a9,product(product(a12,a2),a10)) = product(product(a5,a3),a2),
inference(paramod,[status(thm)],[c_472,c_1443]) ).
cnf(c_1445,plain,
product(a9,product(product(a2,a11),a10)) = product(product(a5,a3),a2),
inference(paramod,[status(thm)],[c_899,c_1444]) ).
cnf(c_1446,plain,
product(a9,product(product(a2,a1),a9)) = product(product(a5,a3),a2),
inference(paramod,[status(thm)],[c_112,c_1445]) ).
cnf(c_1447,plain,
product(product(a7,a1),a9) = product(product(a5,a3),a2),
inference(paramod,[status(thm)],[c_884,c_1446]) ).
cnf(c_918,plain,
product(product(a5,a3),a2) = product(product(a7,a1),a9),
inference(copy,[status(thm)],[c_1447]) ).
cnf(c_1448,plain,
product(a2,a12) = product(a12,product(product(a3,a7),a12)),
inference(paramod,[status(thm)],[c_896,c_21]) ).
cnf(c_1449,plain,
a14 = product(a12,product(product(a3,a7),a12)),
inference(paramod,[status(thm)],[c_15,c_1448]) ).
cnf(c_1450,plain,
a14 = product(a12,product(a11,product(a3,a7))),
inference(paramod,[status(thm)],[c_900,c_1449]) ).
cnf(c_969,plain,
product(a12,product(a11,product(a3,a7))) = a14,
inference(copy,[status(thm)],[c_1450]) ).
cnf(c_1451,plain,
product(product(product(a2,a11),a2),a11) = product(a14,a2),
inference(paramod,[status(thm)],[c_917,c_22]) ).
cnf(c_1452,plain,
product(product(a2,product(a11,a2)),a11) = product(a14,a2),
inference(paramod,[status(thm)],[c_21,c_1451]) ).
cnf(c_1453,plain,
product(product(a2,product(a3,a7)),a11) = product(a14,a2),
inference(paramod,[status(thm)],[c_466,c_1452]) ).
cnf(c_1454,plain,
product(a12,a11) = product(a14,a2),
inference(paramod,[status(thm)],[c_891,c_1453]) ).
cnf(c_1455,plain,
a10 = product(a14,a2),
inference(paramod,[status(thm)],[c_44,c_1454]) ).
cnf(c_977,plain,
product(a14,a2) = a10,
inference(copy,[status(thm)],[c_1455]) ).
cnf(c_988,plain,
product(a2,product(a2,a11)) = a10,
inference(paramod,[status(thm)],[c_977,c_917]) ).
cnf(c_1456,plain,
product(a10,a2) = a14,
inference(paramod,[status(thm)],[c_977,c_2]) ).
cnf(c_1457,plain,
a7 = a14,
inference(paramod,[status(thm)],[c_457,c_1456]) ).
cnf(c_990,plain,
a14 = a7,
inference(copy,[status(thm)],[c_1457]) ).
cnf(c_991,plain,
product(a12,product(a11,product(a3,a7))) = a7,
inference(paramod,[status(thm)],[c_990,c_969]) ).
cnf(c_1458,plain,
product(product(a12,a7),a2) = product(a12,product(a2,a11)),
inference(paramod,[status(thm)],[c_990,c_915]) ).
cnf(c_1459,plain,
product(product(a12,a2),a10) = product(a12,product(a2,a11)),
inference(paramod,[status(thm)],[c_472,c_1458]) ).
cnf(c_1460,plain,
product(product(a2,a11),a10) = product(a12,product(a2,a11)),
inference(paramod,[status(thm)],[c_899,c_1459]) ).
cnf(c_993,plain,
product(product(a2,a1),a9) = product(a12,product(a2,a11)),
inference(paramod,[status(thm)],[c_112,c_1460]) ).
cnf(c_1044,plain,
product(a7,a12) = a2,
inference(paramod,[status(thm)],[c_990,c_57]) ).
cnf(c_1461,plain,
tuple(a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a7) != tuple(a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15),
inference(paramod,[status(thm)],[c_990,c_20]) ).
cnf(c_1045,plain,
tuple(a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a7) != tuple(a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a7,a15),
inference(paramod,[status(thm)],[c_990,c_1461]) ).
cnf(c_1462,plain,
product(a7,a3) = a15,
inference(paramod,[status(thm)],[c_990,c_16]) ).
cnf(c_1463,plain,
a8 = a15,
inference(paramod,[status(thm)],[c_8,c_1462]) ).
cnf(c_1046,plain,
a15 = a8,
inference(copy,[status(thm)],[c_1463]) ).
cnf(c_1048,plain,
product(a9,product(a12,product(a2,a11))) = product(product(a7,a1),a9),
inference(paramod,[status(thm)],[c_993,c_884]) ).
cnf(c_1060,plain,
tuple(a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a7) != tuple(a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a7,a8),
inference(paramod,[status(thm)],[c_1046,c_1045]) ).
cnf(c_1073,plain,
product(product(a11,a3),product(a3,a8)) = a8,
inference(paramod,[status(thm)],[c_1046,c_834]) ).
cnf(c_1464,plain,
product(a8,a8) = a4,
inference(paramod,[status(thm)],[c_1046,c_17]) ).
cnf(c_1465,plain,
a8 = a4,
inference(paramod,[status(thm)],[c_1,c_1464]) ).
cnf(c_1090,plain,
a4 = a8,
inference(copy,[status(thm)],[c_1465]) ).
cnf(c_1466,plain,
product(a3,product(a8,a3)) = product(a5,a3),
inference(paramod,[status(thm)],[c_1090,c_77]) ).
cnf(c_1467,plain,
product(a3,a7) = product(a5,a3),
inference(paramod,[status(thm)],[c_35,c_1466]) ).
cnf(c_1100,plain,
product(a5,a3) = product(a3,a7),
inference(copy,[status(thm)],[c_1467]) ).
cnf(c_1468,plain,
product(a7,product(product(a8,a2),a10)) = a11,
inference(paramod,[status(thm)],[c_1090,c_670]) ).
cnf(c_1469,plain,
product(a7,product(a9,a10)) = a11,
inference(paramod,[status(thm)],[c_9,c_1468]) ).
cnf(c_1470,plain,
product(a7,a12) = a11,
inference(paramod,[status(thm)],[c_110,c_1469]) ).
cnf(c_1471,plain,
a2 = a11,
inference(paramod,[status(thm)],[c_1044,c_1470]) ).
cnf(c_1101,plain,
a11 = a2,
inference(copy,[status(thm)],[c_1471]) ).
cnf(c_1472,plain,
product(product(a2,a3),product(a3,a8)) = a8,
inference(paramod,[status(thm)],[c_1101,c_1073]) ).
cnf(c_1102,plain,
a13 = a8,
inference(paramod,[status(thm)],[c_822,c_1472]) ).
cnf(c_1473,plain,
tuple(a1,a2,a3,a8,a5,a6,a7,a8,a9,a10,a11,a12,a13,a7) != tuple(a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a7,a8),
inference(paramod,[status(thm)],[c_1090,c_1060]) ).
cnf(c_1474,plain,
tuple(a1,a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a13,a7) != tuple(a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a7,a8),
inference(paramod,[status(thm)],[c_1101,c_1473]) ).
cnf(c_1475,plain,
tuple(a1,a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7) != tuple(a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a7,a8),
inference(paramod,[status(thm)],[c_1102,c_1474]) ).
cnf(c_1476,plain,
tuple(a1,a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a11,a12,a13,a7,a8),
inference(paramod,[status(thm)],[c_1090,c_1475]) ).
cnf(c_1477,plain,
tuple(a1,a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a13,a7,a8),
inference(paramod,[status(thm)],[c_1101,c_1476]) ).
cnf(c_1105,plain,
tuple(a1,a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1102,c_1477]) ).
cnf(c_1478,plain,
product(a2,a7) = a4,
inference(paramod,[status(thm)],[c_1101,c_66]) ).
cnf(c_1479,plain,
a6 = a4,
inference(paramod,[status(thm)],[c_53,c_1478]) ).
cnf(c_1190,plain,
a6 = a8,
inference(paramod,[status(thm)],[c_1090,c_1479]) ).
cnf(c_1480,plain,
product(product(a3,a7),a2) = product(product(a7,a1),a9),
inference(paramod,[status(thm)],[c_1100,c_918]) ).
cnf(c_1481,plain,
product(product(a3,a2),a10) = product(product(a7,a1),a9),
inference(paramod,[status(thm)],[c_472,c_1480]) ).
cnf(c_1482,plain,
product(a1,a10) = product(product(a7,a1),a9),
inference(paramod,[status(thm)],[c_26,c_1481]) ).
cnf(c_1483,plain,
a11 = product(product(a7,a1),a9),
inference(paramod,[status(thm)],[c_69,c_1482]) ).
cnf(c_1484,plain,
a2 = product(product(a7,a1),a9),
inference(paramod,[status(thm)],[c_1101,c_1483]) ).
cnf(c_1202,plain,
product(product(a7,a1),a9) = a2,
inference(copy,[status(thm)],[c_1484]) ).
cnf(c_1485,plain,
product(a9,product(a12,product(a2,a2))) = product(product(a7,a1),a9),
inference(paramod,[status(thm)],[c_1101,c_1048]) ).
cnf(c_1486,plain,
product(a9,product(a12,a2)) = product(product(a7,a1),a9),
inference(paramod,[status(thm)],[c_1,c_1485]) ).
cnf(c_1487,plain,
product(a9,product(a2,a11)) = product(product(a7,a1),a9),
inference(paramod,[status(thm)],[c_899,c_1486]) ).
cnf(c_1488,plain,
product(a9,product(a2,a2)) = product(product(a7,a1),a9),
inference(paramod,[status(thm)],[c_1101,c_1487]) ).
cnf(c_1489,plain,
product(a9,a2) = product(product(a7,a1),a9),
inference(paramod,[status(thm)],[c_1,c_1488]) ).
cnf(c_1490,plain,
a8 = product(product(a7,a1),a9),
inference(paramod,[status(thm)],[c_38,c_1489]) ).
cnf(c_1226,plain,
a8 = a2,
inference(paramod,[status(thm)],[c_1202,c_1490]) ).
cnf(c_1491,plain,
product(a12,product(a2,product(a3,a7))) = a7,
inference(paramod,[status(thm)],[c_1101,c_991]) ).
cnf(c_1492,plain,
product(a12,a12) = a7,
inference(paramod,[status(thm)],[c_891,c_1491]) ).
cnf(c_1228,plain,
a12 = a7,
inference(paramod,[status(thm)],[c_1,c_1492]) ).
cnf(c_1493,plain,
product(a2,product(a2,a2)) = a10,
inference(paramod,[status(thm)],[c_1101,c_988]) ).
cnf(c_1494,plain,
product(a2,a2) = a10,
inference(paramod,[status(thm)],[c_1,c_1493]) ).
cnf(c_1495,plain,
a2 = a10,
inference(paramod,[status(thm)],[c_1,c_1494]) ).
cnf(c_1230,plain,
a10 = a2,
inference(copy,[status(thm)],[c_1495]) ).
cnf(c_1496,plain,
product(product(product(A,a2),a2),product(a3,a7)) = product(A,a12),
inference(paramod,[status(thm)],[c_1101,c_902]) ).
cnf(c_1497,plain,
product(A,product(a3,a7)) = product(A,a12),
inference(paramod,[status(thm)],[c_2,c_1496]) ).
cnf(c_1239,plain,
product(A,product(a3,a7)) = product(A,a7),
inference(paramod,[status(thm)],[c_1228,c_1497]) ).
cnf(c_1498,plain,
product(product(a3,a7),a7) = product(a11,product(a3,a7)),
inference(paramod,[status(thm)],[c_1228,c_900]) ).
cnf(c_1499,plain,
a3 = product(a11,product(a3,a7)),
inference(paramod,[status(thm)],[c_2,c_1498]) ).
cnf(c_1500,plain,
a3 = product(a2,product(a3,a7)),
inference(paramod,[status(thm)],[c_1101,c_1499]) ).
cnf(c_1501,plain,
a3 = product(a2,a7),
inference(paramod,[status(thm)],[c_1239,c_1500]) ).
cnf(c_1502,plain,
a3 = a6,
inference(paramod,[status(thm)],[c_53,c_1501]) ).
cnf(c_1503,plain,
a3 = a8,
inference(paramod,[status(thm)],[c_1190,c_1502]) ).
cnf(c_1504,plain,
a3 = a2,
inference(paramod,[status(thm)],[c_1226,c_1503]) ).
cnf(c_1240,plain,
a2 = a3,
inference(copy,[status(thm)],[c_1504]) ).
cnf(c_1505,plain,
product(a2,a10) = a1,
inference(paramod,[status(thm)],[c_1101,c_19]) ).
cnf(c_1506,plain,
product(a3,a10) = a1,
inference(paramod,[status(thm)],[c_1240,c_1505]) ).
cnf(c_1507,plain,
product(a3,a2) = a1,
inference(paramod,[status(thm)],[c_1230,c_1506]) ).
cnf(c_1508,plain,
product(a3,a3) = a1,
inference(paramod,[status(thm)],[c_1240,c_1507]) ).
cnf(c_1509,plain,
a3 = a1,
inference(paramod,[status(thm)],[c_1,c_1508]) ).
cnf(c_1339,plain,
a1 = a3,
inference(copy,[status(thm)],[c_1509]) ).
cnf(c_1510,plain,
product(a2,a11) = a12,
inference(paramod,[status(thm)],[c_1230,c_11]) ).
cnf(c_1511,plain,
product(a3,a11) = a12,
inference(paramod,[status(thm)],[c_1240,c_1510]) ).
cnf(c_1512,plain,
product(a3,a2) = a12,
inference(paramod,[status(thm)],[c_1101,c_1511]) ).
cnf(c_1513,plain,
product(a3,a3) = a12,
inference(paramod,[status(thm)],[c_1240,c_1512]) ).
cnf(c_1514,plain,
a3 = a12,
inference(paramod,[status(thm)],[c_1,c_1513]) ).
cnf(c_1515,plain,
a3 = a7,
inference(paramod,[status(thm)],[c_1228,c_1514]) ).
cnf(c_1340,plain,
a7 = a3,
inference(copy,[status(thm)],[c_1515]) ).
cnf(c_1516,plain,
tuple(a3,a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1339,c_1105]) ).
cnf(c_1517,plain,
tuple(a3,a3,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1240,c_1516]) ).
cnf(c_1518,plain,
tuple(a3,a3,a3,a2,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1226,c_1517]) ).
cnf(c_1519,plain,
tuple(a3,a3,a3,a3,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1240,c_1518]) ).
cnf(c_1520,plain,
tuple(a3,a3,a3,a3,a5,a8,a7,a8,a9,a10,a2,a12,a8,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1190,c_1519]) ).
cnf(c_1521,plain,
tuple(a3,a3,a3,a3,a5,a2,a7,a8,a9,a10,a2,a12,a8,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1226,c_1520]) ).
cnf(c_1522,plain,
tuple(a3,a3,a3,a3,a5,a3,a7,a8,a9,a10,a2,a12,a8,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1240,c_1521]) ).
cnf(c_1523,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a8,a9,a10,a2,a12,a8,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1340,c_1522]) ).
cnf(c_1524,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a2,a9,a10,a2,a12,a8,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1226,c_1523]) ).
cnf(c_1525,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a10,a2,a12,a8,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1240,c_1524]) ).
cnf(c_1526,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a2,a2,a12,a8,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1230,c_1525]) ).
cnf(c_1527,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a2,a12,a8,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1240,c_1526]) ).
cnf(c_1528,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a12,a8,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1240,c_1527]) ).
cnf(c_1529,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a7,a8,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1228,c_1528]) ).
cnf(c_1530,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a8,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1340,c_1529]) ).
cnf(c_1531,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a2,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1226,c_1530]) ).
cnf(c_1532,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a7) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1240,c_1531]) ).
cnf(c_1533,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a2,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1340,c_1532]) ).
cnf(c_1534,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a3,a3,a8,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1240,c_1533]) ).
cnf(c_1535,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a3,a3,a2,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1226,c_1534]) ).
cnf(c_1536,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a5,a6,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1240,c_1535]) ).
cnf(c_1537,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a5,a8,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1190,c_1536]) ).
cnf(c_1538,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a5,a2,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1226,c_1537]) ).
cnf(c_1539,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a5,a3,a7,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1240,c_1538]) ).
cnf(c_1540,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a5,a3,a3,a8,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1340,c_1539]) ).
cnf(c_1541,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a5,a3,a3,a2,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1226,c_1540]) ).
cnf(c_1542,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a5,a3,a3,a3,a9,a10,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1240,c_1541]) ).
cnf(c_1543,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a5,a3,a3,a3,a9,a2,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1230,c_1542]) ).
cnf(c_1544,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a5,a3,a3,a3,a9,a3,a2,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1240,c_1543]) ).
cnf(c_1545,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a12,a8,a7,a8),
inference(paramod,[status(thm)],[c_1240,c_1544]) ).
cnf(c_1546,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a7,a8,a7,a8),
inference(paramod,[status(thm)],[c_1228,c_1545]) ).
cnf(c_1547,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a8,a7,a8),
inference(paramod,[status(thm)],[c_1340,c_1546]) ).
cnf(c_1548,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a2,a7,a8),
inference(paramod,[status(thm)],[c_1226,c_1547]) ).
cnf(c_1549,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a7,a8),
inference(paramod,[status(thm)],[c_1240,c_1548]) ).
cnf(c_1550,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3,a8),
inference(paramod,[status(thm)],[c_1340,c_1549]) ).
cnf(c_1551,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3,a2),
inference(paramod,[status(thm)],[c_1226,c_1550]) ).
cnf(c_1552,plain,
tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3,a3),
inference(paramod,[status(thm)],[c_1240,c_1551]) ).
cnf(c_1352,plain,
tuple(a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3),
inference(copy,[status(thm)],[c_1552]) ).
cnf(c_1553,plain,
product(a3,a6) = a5,
inference(paramod,[status(thm)],[c_1340,c_32]) ).
cnf(c_1554,plain,
product(a3,a8) = a5,
inference(paramod,[status(thm)],[c_1190,c_1553]) ).
cnf(c_1555,plain,
product(a3,a2) = a5,
inference(paramod,[status(thm)],[c_1226,c_1554]) ).
cnf(c_1556,plain,
product(a3,a3) = a5,
inference(paramod,[status(thm)],[c_1240,c_1555]) ).
cnf(c_1557,plain,
a3 = a5,
inference(paramod,[status(thm)],[c_1,c_1556]) ).
cnf(c_1370,plain,
a5 = a3,
inference(copy,[status(thm)],[c_1557]) ).
cnf(c_1558,plain,
product(a2,a2) = a9,
inference(paramod,[status(thm)],[c_1226,c_9]) ).
cnf(c_1559,plain,
product(a3,a2) = a9,
inference(paramod,[status(thm)],[c_1240,c_1558]) ).
cnf(c_1560,plain,
product(a3,a3) = a9,
inference(paramod,[status(thm)],[c_1240,c_1559]) ).
cnf(c_1561,plain,
a3 = a9,
inference(paramod,[status(thm)],[c_1,c_1560]) ).
cnf(c_1376,plain,
a9 = a3,
inference(copy,[status(thm)],[c_1561]) ).
cnf(c_1562,plain,
tuple(a3,a3,a3,a3,a3,a3,a3,a9,a3,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3),
inference(paramod,[status(thm)],[c_1370,c_1352]) ).
cnf(c_1563,plain,
tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a3,a5,a3,a3,a3,a9,a3,a3,a3,a3,a3),
inference(paramod,[status(thm)],[c_1376,c_1562]) ).
cnf(c_1564,plain,
tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a3,a3,a3,a3,a3,a9,a3,a3,a3,a3,a3),
inference(paramod,[status(thm)],[c_1370,c_1563]) ).
cnf(c_1565,plain,
tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3) != tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3),
inference(paramod,[status(thm)],[c_1376,c_1564]) ).
cnf(c_1382,plain,
$false,
inference(copy,[status(thm)],[c_1565]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP053-1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/5.44 % Computer : n005.cluster.edu
% 0.17/5.44 % Model : x86_64 x86_64
% 0.17/5.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.44 % Memory : 8046.5625MB
% 0.17/5.44 % OS : Linux 6.8.0-71-generic
% 0.17/5.44 % CPULimit : 300
% 0.17/5.44 % WCLimit : 300
% 0.17/5.44 % DateTime : Sat Sep 26 20:50:38 UTC 2026
% 0.17/5.44 % CPUTime :
% 0.17/5.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/5.45 % Process 3064371 was started by sandbox2 on n005,
% 0.17/5.45 % Sat Sep 26 20:50:38 2026
% 0.17/5.45 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/5.45
% 0.17/5.45 % From the command line: assign(max_seconds, 300).
% 0.22/5.70
% 0.22/5.70 % SZS status Unsatisfiable for theBenchmark
% 0.22/5.70
% 0.22/5.70 % Proof 1 at 0.17 (+ 0.06) seconds.
% 0.22/5.70 % Length of proof is 111.
% 0.22/5.70 % Level of proof is 19.
% 0.22/5.70 % Maximum clause weight is 41.000.
% 0.22/5.70 % Given clauses 114.
% 0.22/5.70
% 0.22/5.70 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------