%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : TOP049-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 : n009.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:05 AM UTC 2026
% Result : Unsatisfiable 1.74s 0.67s
% Output : CNFRefutation 1.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 82
% Number of leaves : 14
% Syntax : Number of formulae : 351 ( 351 unt; 0 def)
% Number of atoms : 351 ( 350 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 24 ( 24 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-9 aty)
% Number of variables : 165 ( 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,
a1 = product(a9,a7),
file('theBenchmark.p',knot) ).
cnf(c_5,plain,
a1 = product(a9,a7),
inference(clausify,[status(thm)],[knot]) ).
cnf(c_6,plain,
product(a9,a7) = a1,
inference(copy,[status(thm)],[c_5]) ).
fof(knot_03,axiom,
a3 = product(a1,a2),
file('theBenchmark.p',knot_03) ).
cnf(c_7,plain,
a3 = product(a1,a2),
inference(clausify,[status(thm)],[knot_03]) ).
cnf(c_8,plain,
product(a1,a2) = a3,
inference(copy,[status(thm)],[c_7]) ).
fof(knot_04,axiom,
a2 = product(a3,a4),
file('theBenchmark.p',knot_04) ).
cnf(c_9,plain,
a2 = product(a3,a4),
inference(clausify,[status(thm)],[knot_04]) ).
cnf(c_10,plain,
product(a3,a4) = a2,
inference(copy,[status(thm)],[c_9]) ).
fof(knot_05,axiom,
a5 = product(a2,a10),
file('theBenchmark.p',knot_05) ).
cnf(c_11,plain,
a5 = product(a2,a10),
inference(clausify,[status(thm)],[knot_05]) ).
cnf(c_12,plain,
product(a2,a10) = a5,
inference(copy,[status(thm)],[c_11]) ).
fof(knot_06,axiom,
a6 = product(a5,a4),
file('theBenchmark.p',knot_06) ).
cnf(c_13,plain,
a6 = product(a5,a4),
inference(clausify,[status(thm)],[knot_06]) ).
cnf(c_14,plain,
product(a5,a4) = a6,
inference(copy,[status(thm)],[c_13]) ).
fof(knot_07,axiom,
a7 = product(a6,a1),
file('theBenchmark.p',knot_07) ).
cnf(c_15,plain,
a7 = product(a6,a1),
inference(clausify,[status(thm)],[knot_07]) ).
cnf(c_16,plain,
product(a6,a1) = a7,
inference(copy,[status(thm)],[c_15]) ).
fof(knot_08,axiom,
a8 = product(a7,a4),
file('theBenchmark.p',knot_08) ).
cnf(c_17,plain,
a8 = product(a7,a4),
inference(clausify,[status(thm)],[knot_08]) ).
cnf(c_18,plain,
product(a7,a4) = a8,
inference(copy,[status(thm)],[c_17]) ).
fof(knot_09,axiom,
a10 = product(a8,a9),
file('theBenchmark.p',knot_09) ).
cnf(c_19,plain,
a10 = product(a8,a9),
inference(clausify,[status(thm)],[knot_09]) ).
cnf(c_20,plain,
product(a8,a9) = a10,
inference(copy,[status(thm)],[c_19]) ).
fof(knot_10,axiom,
a4 = product(a10,a3),
file('theBenchmark.p',knot_10) ).
cnf(c_21,plain,
a4 = product(a10,a3),
inference(clausify,[status(thm)],[knot_10]) ).
cnf(c_22,plain,
product(a10,a3) = a4,
inference(copy,[status(thm)],[c_21]) ).
fof(knot_11,axiom,
a9 = product(a4,a8),
file('theBenchmark.p',knot_11) ).
cnf(c_23,plain,
a9 = product(a4,a8),
inference(clausify,[status(thm)],[knot_11]) ).
cnf(c_24,plain,
product(a4,a8) = a9,
inference(copy,[status(thm)],[c_23]) ).
fof(goal,axiom,
tuple(a1,a9,a8,a6,a7,a2,a3,a4,a5) != tuple(a2,a10,a9,a7,a8,a3,a4,a5,a6),
file('theBenchmark.p',goal) ).
cnf(c_25,plain,
tuple(a1,a9,a8,a6,a7,a2,a3,a4,a5) != tuple(a2,a10,a9,a7,a8,a3,a4,a5,a6),
inference(clausify,[status(thm)],[goal]) ).
cnf(c_26,plain,
tuple(a2,a10,a9,a7,a8,a3,a4,a5,a6) != tuple(a1,a9,a8,a6,a7,a2,a3,a4,a5),
inference(copy,[status(thm)],[c_25]) ).
cnf(c_865,plain,
product(A,product(B,A)) = product(product(A,B),A),
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_27,plain,
product(product(A,B),A) = product(A,product(B,A)),
inference(copy,[status(thm)],[c_865]) ).
cnf(c_866,plain,
product(A,product(B,C)) = product(product(product(A,C),B),C),
inference(paramod,[status(thm)],[c_2,c_4]) ).
cnf(c_28,plain,
product(product(product(A,B),C),B) = product(A,product(C,B)),
inference(copy,[status(thm)],[c_866]) ).
cnf(c_867,plain,
product(product(A,B),C) = product(product(A,product(C,B)),B),
inference(paramod,[status(thm)],[c_2,c_4]) ).
cnf(c_29,plain,
product(product(A,product(B,C)),C) = product(product(A,C),B),
inference(copy,[status(thm)],[c_867]) ).
cnf(c_30,plain,
product(product(product(A,B),C),product(D,product(B,C))) = product(product(product(A,C),D),product(B,C)),
inference(paramod,[status(thm)],[c_4,c_4]) ).
cnf(c_31,plain,
product(product(A,product(B,C)),product(product(D,B),C)) = product(product(A,product(D,C)),product(B,C)),
inference(paramod,[status(thm)],[c_4,c_4]) ).
cnf(c_35,plain,
product(a3,a2) = a1,
inference(paramod,[status(thm)],[c_8,c_2]) ).
cnf(c_868,plain,
product(a3,product(A,a2)) = product(product(a1,A),a2),
inference(paramod,[status(thm)],[c_8,c_4]) ).
cnf(c_36,plain,
product(product(a1,A),a2) = product(a3,product(A,a2)),
inference(copy,[status(thm)],[c_868]) ).
cnf(c_37,plain,
product(product(A,a2),a3) = product(product(A,a1),a2),
inference(paramod,[status(thm)],[c_8,c_4]) ).
cnf(c_38,plain,
product(a2,a4) = a3,
inference(paramod,[status(thm)],[c_10,c_2]) ).
cnf(c_869,plain,
product(a2,product(A,a4)) = product(product(a3,A),a4),
inference(paramod,[status(thm)],[c_10,c_4]) ).
cnf(c_39,plain,
product(product(a3,A),a4) = product(a2,product(A,a4)),
inference(copy,[status(thm)],[c_869]) ).
cnf(c_870,plain,
product(product(A,a4),a2) = product(product(A,a3),a4),
inference(paramod,[status(thm)],[c_10,c_4]) ).
cnf(c_40,plain,
product(product(A,a3),a4) = product(product(A,a4),a2),
inference(copy,[status(thm)],[c_870]) ).
cnf(c_47,plain,
product(a7,a1) = a6,
inference(paramod,[status(thm)],[c_16,c_2]) ).
cnf(c_871,plain,
product(product(A,a1),a7) = product(product(A,a6),a1),
inference(paramod,[status(thm)],[c_16,c_4]) ).
cnf(c_49,plain,
product(product(A,a6),a1) = product(product(A,a1),a7),
inference(copy,[status(thm)],[c_871]) ).
cnf(c_50,plain,
product(a8,a4) = a7,
inference(paramod,[status(thm)],[c_18,c_2]) ).
cnf(c_872,plain,
product(product(A,a4),a8) = product(product(A,a7),a4),
inference(paramod,[status(thm)],[c_18,c_4]) ).
cnf(c_52,plain,
product(product(A,a7),a4) = product(product(A,a4),a8),
inference(copy,[status(thm)],[c_872]) ).
cnf(c_53,plain,
product(a10,a9) = a8,
inference(paramod,[status(thm)],[c_20,c_2]) ).
cnf(c_55,plain,
product(product(A,a9),a10) = product(product(A,a8),a9),
inference(paramod,[status(thm)],[c_20,c_4]) ).
cnf(c_56,plain,
product(a4,a3) = a10,
inference(paramod,[status(thm)],[c_22,c_2]) ).
cnf(c_873,plain,
product(product(A,a3),a4) = product(product(A,a10),a3),
inference(paramod,[status(thm)],[c_22,c_4]) ).
cnf(c_874,plain,
product(product(A,a4),a2) = product(product(A,a10),a3),
inference(paramod,[status(thm)],[c_40,c_873]) ).
cnf(c_58,plain,
product(product(A,a10),a3) = product(product(A,a4),a2),
inference(copy,[status(thm)],[c_874]) ).
cnf(c_59,plain,
product(a9,a8) = a4,
inference(paramod,[status(thm)],[c_24,c_2]) ).
cnf(c_61,plain,
product(product(A,a8),a9) = product(product(A,a4),a8),
inference(paramod,[status(thm)],[c_24,c_4]) ).
cnf(c_62,plain,
product(product(A,a9),a10) = product(product(A,a4),a8),
inference(paramod,[status(thm)],[c_61,c_55]) ).
cnf(c_875,plain,
product(a1,a9) = product(a9,product(a7,a9)),
inference(paramod,[status(thm)],[c_6,c_27]) ).
cnf(c_67,plain,
product(a9,product(a7,a9)) = product(a1,a9),
inference(copy,[status(thm)],[c_875]) ).
cnf(c_876,plain,
product(a2,a3) = product(a3,product(a4,a3)),
inference(paramod,[status(thm)],[c_10,c_27]) ).
cnf(c_877,plain,
product(a2,a3) = product(a3,a10),
inference(paramod,[status(thm)],[c_56,c_876]) ).
cnf(c_69,plain,
product(a3,a10) = product(a2,a3),
inference(copy,[status(thm)],[c_877]) ).
cnf(c_878,plain,
product(product(a4,a3),a4) = product(a4,a2),
inference(paramod,[status(thm)],[c_10,c_27]) ).
cnf(c_70,plain,
product(a10,a4) = product(a4,a2),
inference(paramod,[status(thm)],[c_56,c_878]) ).
cnf(c_879,plain,
product(a8,a7) = product(a7,product(a4,a7)),
inference(paramod,[status(thm)],[c_18,c_27]) ).
cnf(c_74,plain,
product(a7,product(a4,a7)) = product(a8,a7),
inference(copy,[status(thm)],[c_879]) ).
cnf(c_880,plain,
product(a10,a8) = product(a8,product(a9,a8)),
inference(paramod,[status(thm)],[c_20,c_27]) ).
cnf(c_881,plain,
product(a10,a8) = product(a8,a4),
inference(paramod,[status(thm)],[c_59,c_880]) ).
cnf(c_75,plain,
product(a10,a8) = a7,
inference(paramod,[status(thm)],[c_50,c_881]) ).
cnf(c_882,plain,
product(product(a9,a8),a9) = product(a9,a10),
inference(paramod,[status(thm)],[c_20,c_27]) ).
cnf(c_883,plain,
product(a4,a9) = product(a9,a10),
inference(paramod,[status(thm)],[c_59,c_882]) ).
cnf(c_76,plain,
product(a9,a10) = product(a4,a9),
inference(copy,[status(thm)],[c_883]) ).
cnf(c_884,plain,
product(a4,a10) = product(a10,product(a3,a10)),
inference(paramod,[status(thm)],[c_22,c_27]) ).
cnf(c_885,plain,
product(a4,a10) = product(a10,product(a2,a3)),
inference(paramod,[status(thm)],[c_69,c_884]) ).
cnf(c_77,plain,
product(a10,product(a2,a3)) = product(a4,a10),
inference(copy,[status(thm)],[c_885]) ).
cnf(c_886,plain,
product(a9,a4) = product(a4,product(a8,a4)),
inference(paramod,[status(thm)],[c_24,c_27]) ).
cnf(c_78,plain,
product(a9,a4) = product(a4,a7),
inference(paramod,[status(thm)],[c_50,c_886]) ).
cnf(c_887,plain,
product(product(a8,a4),a8) = product(a8,a9),
inference(paramod,[status(thm)],[c_24,c_27]) ).
cnf(c_888,plain,
product(a7,a8) = product(a8,a9),
inference(paramod,[status(thm)],[c_50,c_887]) ).
cnf(c_79,plain,
product(a7,a8) = a10,
inference(paramod,[status(thm)],[c_20,c_888]) ).
cnf(c_889,plain,
product(a1,a3) = product(a3,product(a2,a3)),
inference(paramod,[status(thm)],[c_35,c_27]) ).
cnf(c_87,plain,
product(a3,product(a2,a3)) = product(a1,a3),
inference(copy,[status(thm)],[c_889]) ).
cnf(c_890,plain,
product(a3,a2) = product(a2,product(a4,a2)),
inference(paramod,[status(thm)],[c_38,c_27]) ).
cnf(c_891,plain,
a1 = product(a2,product(a4,a2)),
inference(paramod,[status(thm)],[c_35,c_890]) ).
cnf(c_90,plain,
product(a2,product(a4,a2)) = a1,
inference(copy,[status(thm)],[c_891]) ).
cnf(c_892,plain,
product(product(A,a1),a6) = product(product(A,a7),a1),
inference(paramod,[status(thm)],[c_47,c_4]) ).
cnf(c_98,plain,
product(product(A,a7),a1) = product(product(A,a1),a6),
inference(copy,[status(thm)],[c_892]) ).
cnf(c_893,plain,
product(product(A,a4),a7) = product(product(A,a8),a4),
inference(paramod,[status(thm)],[c_50,c_4]) ).
cnf(c_115,plain,
product(product(A,a8),a4) = product(product(A,a4),a7),
inference(copy,[status(thm)],[c_893]) ).
cnf(c_116,plain,
product(product(A,a9),a8) = product(product(A,a10),a9),
inference(paramod,[status(thm)],[c_53,c_4]) ).
cnf(c_894,plain,
product(a8,a10) = product(a10,product(a9,a10)),
inference(paramod,[status(thm)],[c_53,c_27]) ).
cnf(c_895,plain,
product(a8,a10) = product(a10,product(a4,a9)),
inference(paramod,[status(thm)],[c_76,c_894]) ).
cnf(c_117,plain,
product(a10,product(a4,a9)) = product(a8,a10),
inference(copy,[status(thm)],[c_895]) ).
cnf(c_118,plain,
product(product(A,a3),a10) = product(product(A,a4),a3),
inference(paramod,[status(thm)],[c_56,c_4]) ).
cnf(c_896,plain,
product(product(A,a8),a4) = product(product(A,a9),a8),
inference(paramod,[status(thm)],[c_59,c_4]) ).
cnf(c_897,plain,
product(product(A,a4),a7) = product(product(A,a9),a8),
inference(paramod,[status(thm)],[c_115,c_896]) ).
cnf(c_898,plain,
product(product(A,a4),a7) = product(product(A,a10),a9),
inference(paramod,[status(thm)],[c_116,c_897]) ).
cnf(c_120,plain,
product(product(A,a10),a9) = product(product(A,a4),a7),
inference(copy,[status(thm)],[c_898]) ).
cnf(c_123,plain,
product(product(A,a8),a7) = product(product(A,a10),a8),
inference(paramod,[status(thm)],[c_75,c_4]) ).
cnf(c_899,plain,
product(a7,a10) = product(a10,product(a8,a10)),
inference(paramod,[status(thm)],[c_75,c_27]) ).
cnf(c_124,plain,
product(a10,product(a8,a10)) = product(a7,a10),
inference(copy,[status(thm)],[c_899]) ).
cnf(c_900,plain,
product(a10,a7) = product(a7,product(a8,a7)),
inference(paramod,[status(thm)],[c_79,c_27]) ).
cnf(c_127,plain,
product(a7,product(a8,a7)) = product(a10,a7),
inference(copy,[status(thm)],[c_900]) ).
cnf(c_131,plain,
product(product(a2,a3),product(A,a10)) = product(product(a3,A),a10),
inference(paramod,[status(thm)],[c_69,c_4]) ).
cnf(c_901,plain,
product(product(A,a10),product(a2,a3)) = product(product(A,a3),a10),
inference(paramod,[status(thm)],[c_69,c_4]) ).
cnf(c_132,plain,
product(product(A,a10),product(a2,a3)) = product(product(A,a4),a3),
inference(paramod,[status(thm)],[c_118,c_901]) ).
cnf(c_133,plain,
product(product(product(a2,a3),A),a10) = product(a3,product(A,a10)),
inference(paramod,[status(thm)],[c_69,c_28]) ).
cnf(c_902,plain,
product(product(A,product(a2,a3)),a10) = product(product(A,a10),a3),
inference(paramod,[status(thm)],[c_69,c_29]) ).
cnf(c_135,plain,
product(product(A,product(a2,a3)),a10) = product(product(A,a4),a2),
inference(paramod,[status(thm)],[c_58,c_902]) ).
cnf(c_903,plain,
product(product(A,a10),product(a4,a9)) = product(product(A,a9),a10),
inference(paramod,[status(thm)],[c_76,c_4]) ).
cnf(c_142,plain,
product(product(A,a10),product(a4,a9)) = product(product(A,a4),a8),
inference(paramod,[status(thm)],[c_62,c_903]) ).
cnf(c_143,plain,
product(product(product(a4,a9),A),a10) = product(a9,product(A,a10)),
inference(paramod,[status(thm)],[c_76,c_28]) ).
cnf(c_904,plain,
product(product(A,product(a4,a9)),a10) = product(product(A,a10),a9),
inference(paramod,[status(thm)],[c_76,c_29]) ).
cnf(c_145,plain,
product(product(A,product(a4,a9)),a10) = product(product(A,a4),a7),
inference(paramod,[status(thm)],[c_120,c_904]) ).
cnf(c_905,plain,
product(product(product(A,a8),a9),product(B,a10)) = product(product(product(A,a9),B),product(a8,a9)),
inference(paramod,[status(thm)],[c_20,c_30]) ).
cnf(c_906,plain,
product(product(product(A,a4),a8),product(B,a10)) = product(product(product(A,a9),B),product(a8,a9)),
inference(paramod,[status(thm)],[c_61,c_905]) ).
cnf(c_172,plain,
product(product(product(A,a4),a8),product(B,a10)) = product(product(product(A,a9),B),a10),
inference(paramod,[status(thm)],[c_20,c_906]) ).
cnf(c_907,plain,
product(product(product(A,a4),a3),product(B,a10)) = product(product(product(A,a3),B),product(a4,a3)),
inference(paramod,[status(thm)],[c_56,c_30]) ).
cnf(c_189,plain,
product(product(product(A,a4),a3),product(B,a10)) = product(product(product(A,a3),B),a10),
inference(paramod,[status(thm)],[c_56,c_907]) ).
cnf(c_208,plain,
product(a1,product(a4,a2)) = a2,
inference(paramod,[status(thm)],[c_90,c_2]) ).
cnf(c_908,plain,
product(product(product(a4,a2),a2),product(a4,a2)) = product(product(a4,a2),a1),
inference(paramod,[status(thm)],[c_90,c_27]) ).
cnf(c_909,plain,
product(a4,product(a4,a2)) = product(product(a4,a2),a1),
inference(paramod,[status(thm)],[c_2,c_908]) ).
cnf(c_211,plain,
product(product(a4,a2),a1) = product(a4,product(a4,a2)),
inference(copy,[status(thm)],[c_909]) ).
cnf(c_910,plain,
product(product(product(A,a4),a2),a1) = product(product(product(A,a2),a2),product(a4,a2)),
inference(paramod,[status(thm)],[c_90,c_30]) ).
cnf(c_217,plain,
product(product(product(A,a4),a2),a1) = product(A,product(a4,a2)),
inference(paramod,[status(thm)],[c_2,c_910]) ).
cnf(c_911,plain,
product(a2,a1) = product(a1,product(product(a4,a2),a1)),
inference(paramod,[status(thm)],[c_208,c_27]) ).
cnf(c_912,plain,
product(a2,a1) = product(a1,product(a4,product(a4,a2))),
inference(paramod,[status(thm)],[c_211,c_911]) ).
cnf(c_218,plain,
product(a1,product(a4,product(a4,a2))) = product(a2,a1),
inference(copy,[status(thm)],[c_912]) ).
cnf(c_913,plain,
product(product(A,a10),product(product(B,a8),a9)) = product(product(A,product(B,a9)),product(a8,a9)),
inference(paramod,[status(thm)],[c_20,c_31]) ).
cnf(c_914,plain,
product(product(A,a10),product(product(B,a4),a8)) = product(product(A,product(B,a9)),product(a8,a9)),
inference(paramod,[status(thm)],[c_61,c_913]) ).
cnf(c_260,plain,
product(product(A,a10),product(product(B,a4),a8)) = product(product(A,product(B,a9)),a10),
inference(paramod,[status(thm)],[c_20,c_914]) ).
cnf(c_915,plain,
product(product(A,a10),product(product(B,a4),a3)) = product(product(A,product(B,a3)),product(a4,a3)),
inference(paramod,[status(thm)],[c_56,c_31]) ).
cnf(c_278,plain,
product(product(A,a10),product(product(B,a4),a3)) = product(product(A,product(B,a3)),a10),
inference(paramod,[status(thm)],[c_56,c_915]) ).
cnf(c_916,plain,
product(product(product(a4,a7),a7),product(a4,a7)) = product(product(a4,a7),product(a8,a7)),
inference(paramod,[status(thm)],[c_74,c_27]) ).
cnf(c_917,plain,
product(a4,product(a4,a7)) = product(product(a4,a7),product(a8,a7)),
inference(paramod,[status(thm)],[c_2,c_916]) ).
cnf(c_918,plain,
product(a4,product(a4,a7)) = product(product(a4,a8),a7),
inference(paramod,[status(thm)],[c_4,c_917]) ).
cnf(c_919,plain,
product(a4,product(a4,a7)) = product(a9,a7),
inference(paramod,[status(thm)],[c_24,c_918]) ).
cnf(c_324,plain,
product(a4,product(a4,a7)) = a1,
inference(paramod,[status(thm)],[c_6,c_919]) ).
cnf(c_920,plain,
product(product(product(A,a4),a7),product(a8,a7)) = product(product(product(A,a7),a7),product(a4,a7)),
inference(paramod,[status(thm)],[c_74,c_30]) ).
cnf(c_921,plain,
product(product(product(A,a4),a8),a7) = product(product(product(A,a7),a7),product(a4,a7)),
inference(paramod,[status(thm)],[c_4,c_920]) ).
cnf(c_922,plain,
product(product(product(A,a4),a10),a8) = product(product(product(A,a7),a7),product(a4,a7)),
inference(paramod,[status(thm)],[c_123,c_921]) ).
cnf(c_328,plain,
product(product(product(A,a4),a10),a8) = product(A,product(a4,a7)),
inference(paramod,[status(thm)],[c_2,c_922]) ).
cnf(c_331,plain,
product(a1,product(a4,a7)) = a4,
inference(paramod,[status(thm)],[c_324,c_2]) ).
cnf(c_923,plain,
product(a1,a4) = product(a4,product(product(a4,a7),a4)),
inference(paramod,[status(thm)],[c_324,c_27]) ).
cnf(c_924,plain,
product(a1,a4) = product(a4,product(a4,product(a7,a4))),
inference(paramod,[status(thm)],[c_27,c_923]) ).
cnf(c_925,plain,
product(a1,a4) = product(a4,product(a4,a8)),
inference(paramod,[status(thm)],[c_18,c_924]) ).
cnf(c_334,plain,
product(a1,a4) = product(a4,a9),
inference(paramod,[status(thm)],[c_24,c_925]) ).
cnf(c_926,plain,
product(product(product(A,a4),a7),a4) = product(product(product(A,a7),a1),product(a4,a7)),
inference(paramod,[status(thm)],[c_331,c_30]) ).
cnf(c_927,plain,
product(product(product(A,a4),a4),a8) = product(product(product(A,a7),a1),product(a4,a7)),
inference(paramod,[status(thm)],[c_52,c_926]) ).
cnf(c_928,plain,
product(A,a8) = product(product(product(A,a7),a1),product(a4,a7)),
inference(paramod,[status(thm)],[c_2,c_927]) ).
cnf(c_929,plain,
product(A,a8) = product(product(product(A,a1),a6),product(a4,a7)),
inference(paramod,[status(thm)],[c_98,c_928]) ).
cnf(c_356,plain,
product(product(product(A,a1),a6),product(a4,a7)) = product(A,a8),
inference(copy,[status(thm)],[c_929]) ).
cnf(c_930,plain,
product(product(product(a2,a3),a10),product(a2,a3)) = product(product(a2,a3),product(a4,a10)),
inference(paramod,[status(thm)],[c_77,c_27]) ).
cnf(c_931,plain,
product(product(product(a2,a4),a3),product(a2,a3)) = product(product(a2,a3),product(a4,a10)),
inference(paramod,[status(thm)],[c_118,c_930]) ).
cnf(c_932,plain,
product(product(a3,a3),product(a2,a3)) = product(product(a2,a3),product(a4,a10)),
inference(paramod,[status(thm)],[c_38,c_931]) ).
cnf(c_933,plain,
product(a3,product(a2,a3)) = product(product(a2,a3),product(a4,a10)),
inference(paramod,[status(thm)],[c_1,c_932]) ).
cnf(c_934,plain,
product(a1,a3) = product(product(a2,a3),product(a4,a10)),
inference(paramod,[status(thm)],[c_87,c_933]) ).
cnf(c_935,plain,
product(a1,a3) = product(product(a3,a4),a10),
inference(paramod,[status(thm)],[c_131,c_934]) ).
cnf(c_936,plain,
product(a1,a3) = product(a2,a10),
inference(paramod,[status(thm)],[c_10,c_935]) ).
cnf(c_361,plain,
product(a1,a3) = a5,
inference(paramod,[status(thm)],[c_12,c_936]) ).
cnf(c_937,plain,
product(product(product(A,product(a2,a3)),a10),product(a2,a3)) = product(A,product(a4,a10)),
inference(paramod,[status(thm)],[c_77,c_28]) ).
cnf(c_363,plain,
product(product(product(A,a4),a2),product(a2,a3)) = product(A,product(a4,a10)),
inference(paramod,[status(thm)],[c_135,c_937]) ).
cnf(c_372,plain,
product(a3,product(a2,a3)) = a5,
inference(paramod,[status(thm)],[c_361,c_87]) ).
cnf(c_396,plain,
product(a5,product(a2,a3)) = a3,
inference(paramod,[status(thm)],[c_372,c_2]) ).
cnf(c_437,plain,
product(product(a4,a9),a2) = product(a3,product(a4,a2)),
inference(paramod,[status(thm)],[c_334,c_36]) ).
cnf(c_938,plain,
product(product(product(a10,a9),a4),a9) = product(a8,a10),
inference(paramod,[status(thm)],[c_117,c_28]) ).
cnf(c_939,plain,
product(product(a8,a4),a9) = product(a8,a10),
inference(paramod,[status(thm)],[c_53,c_938]) ).
cnf(c_940,plain,
product(a7,a9) = product(a8,a10),
inference(paramod,[status(thm)],[c_50,c_939]) ).
cnf(c_461,plain,
product(a8,a10) = product(a7,a9),
inference(copy,[status(thm)],[c_940]) ).
cnf(c_471,plain,
product(a10,product(a7,a9)) = product(a7,a10),
inference(paramod,[status(thm)],[c_461,c_124]) ).
cnf(c_472,plain,
product(a10,product(a4,a9)) = product(a7,a9),
inference(paramod,[status(thm)],[c_461,c_117]) ).
cnf(c_477,plain,
product(product(A,product(a7,a9)),a10) = product(product(A,a10),a8),
inference(paramod,[status(thm)],[c_461,c_29]) ).
cnf(c_941,plain,
product(product(product(a8,a7),a7),product(a8,a7)) = product(product(a8,a7),product(a10,a7)),
inference(paramod,[status(thm)],[c_127,c_27]) ).
cnf(c_942,plain,
product(a8,product(a8,a7)) = product(product(a8,a7),product(a10,a7)),
inference(paramod,[status(thm)],[c_2,c_941]) ).
cnf(c_943,plain,
product(a8,product(a8,a7)) = product(product(a8,a10),a7),
inference(paramod,[status(thm)],[c_4,c_942]) ).
cnf(c_944,plain,
product(a8,product(a8,a7)) = product(product(a7,a9),a7),
inference(paramod,[status(thm)],[c_461,c_943]) ).
cnf(c_945,plain,
product(a8,product(a8,a7)) = product(a7,product(a9,a7)),
inference(paramod,[status(thm)],[c_27,c_944]) ).
cnf(c_946,plain,
product(a8,product(a8,a7)) = product(a7,a1),
inference(paramod,[status(thm)],[c_6,c_945]) ).
cnf(c_483,plain,
product(a8,product(a8,a7)) = a6,
inference(paramod,[status(thm)],[c_47,c_946]) ).
cnf(c_490,plain,
product(a6,product(a8,a7)) = a8,
inference(paramod,[status(thm)],[c_483,c_2]) ).
cnf(c_510,plain,
product(product(product(A,a3),a1),a2) = product(A,product(a2,a3)),
inference(paramod,[status(thm)],[c_37,c_28]) ).
cnf(c_947,plain,
product(a1,a4) = product(a2,product(a2,a4)),
inference(paramod,[status(thm)],[c_35,c_39]) ).
cnf(c_948,plain,
product(a4,a9) = product(a2,product(a2,a4)),
inference(paramod,[status(thm)],[c_334,c_947]) ).
cnf(c_949,plain,
product(a4,a9) = product(a2,a3),
inference(paramod,[status(thm)],[c_38,c_948]) ).
cnf(c_585,plain,
product(a2,a3) = product(a4,a9),
inference(copy,[status(thm)],[c_949]) ).
cnf(c_950,plain,
product(a5,a4) = product(a2,product(product(a2,a3),a4)),
inference(paramod,[status(thm)],[c_372,c_39]) ).
cnf(c_951,plain,
a6 = product(a2,product(product(a2,a3),a4)),
inference(paramod,[status(thm)],[c_14,c_950]) ).
cnf(c_952,plain,
a6 = product(a2,product(product(a4,a9),a4)),
inference(paramod,[status(thm)],[c_585,c_951]) ).
cnf(c_953,plain,
a6 = product(a2,product(a4,product(a9,a4))),
inference(paramod,[status(thm)],[c_27,c_952]) ).
cnf(c_954,plain,
a6 = product(a2,product(a4,product(a4,a7))),
inference(paramod,[status(thm)],[c_78,c_953]) ).
cnf(c_955,plain,
a6 = product(a2,a1),
inference(paramod,[status(thm)],[c_324,c_954]) ).
cnf(c_589,plain,
product(a2,a1) = a6,
inference(copy,[status(thm)],[c_955]) ).
cnf(c_592,plain,
product(product(product(A,a3),a1),a2) = product(A,product(a4,a9)),
inference(paramod,[status(thm)],[c_585,c_510]) ).
cnf(c_607,plain,
product(a5,product(a4,a9)) = a3,
inference(paramod,[status(thm)],[c_585,c_396]) ).
cnf(c_608,plain,
product(a3,product(a4,a9)) = a5,
inference(paramod,[status(thm)],[c_585,c_372]) ).
cnf(c_615,plain,
product(product(product(A,a4),a2),product(a4,a9)) = product(A,product(a4,a10)),
inference(paramod,[status(thm)],[c_585,c_363]) ).
cnf(c_956,plain,
product(product(A,product(a4,a9)),a10) = product(product(A,a4),a2),
inference(paramod,[status(thm)],[c_585,c_135]) ).
cnf(c_624,plain,
product(product(A,a4),a7) = product(product(A,a4),a2),
inference(paramod,[status(thm)],[c_145,c_956]) ).
cnf(c_957,plain,
product(product(product(a4,a9),A),a10) = product(a3,product(A,a10)),
inference(paramod,[status(thm)],[c_585,c_133]) ).
cnf(c_626,plain,
product(a9,product(A,a10)) = product(a3,product(A,a10)),
inference(paramod,[status(thm)],[c_143,c_957]) ).
cnf(c_958,plain,
product(product(A,a10),product(a4,a9)) = product(product(A,a4),a3),
inference(paramod,[status(thm)],[c_585,c_132]) ).
cnf(c_627,plain,
product(product(A,a4),a8) = product(product(A,a4),a3),
inference(paramod,[status(thm)],[c_142,c_958]) ).
cnf(c_959,plain,
product(a10,product(a4,a9)) = product(a4,a10),
inference(paramod,[status(thm)],[c_585,c_77]) ).
cnf(c_629,plain,
product(a7,a9) = product(a4,a10),
inference(paramod,[status(thm)],[c_472,c_959]) ).
cnf(c_637,plain,
product(a1,product(a4,product(a4,a2))) = a6,
inference(paramod,[status(thm)],[c_589,c_218]) ).
cnf(c_654,plain,
product(product(A,product(a4,a9)),a10) = product(product(A,a4),a2),
inference(paramod,[status(thm)],[c_624,c_145]) ).
cnf(c_658,plain,
product(product(product(a4,a9),A),a10) = product(a3,product(A,a10)),
inference(paramod,[status(thm)],[c_626,c_143]) ).
cnf(c_960,plain,
product(product(A,a10),product(product(B,a4),a3)) = product(product(A,product(B,a9)),a10),
inference(paramod,[status(thm)],[c_627,c_260]) ).
cnf(c_961,plain,
product(product(A,product(B,a3)),a10) = product(product(A,product(B,a9)),a10),
inference(paramod,[status(thm)],[c_278,c_960]) ).
cnf(c_665,plain,
product(product(A,product(B,a9)),a10) = product(product(A,product(B,a3)),a10),
inference(copy,[status(thm)],[c_961]) ).
cnf(c_962,plain,
product(product(product(A,a4),a3),product(B,a10)) = product(product(product(A,a9),B),a10),
inference(paramod,[status(thm)],[c_627,c_172]) ).
cnf(c_963,plain,
product(product(product(A,a3),B),a10) = product(product(product(A,a9),B),a10),
inference(paramod,[status(thm)],[c_189,c_962]) ).
cnf(c_667,plain,
product(product(product(A,a9),B),a10) = product(product(product(A,a3),B),a10),
inference(copy,[status(thm)],[c_963]) ).
cnf(c_964,plain,
product(product(A,product(a4,a10)),a10) = product(product(A,a10),a8),
inference(paramod,[status(thm)],[c_629,c_477]) ).
cnf(c_965,plain,
product(product(A,a10),a4) = product(product(A,a10),a8),
inference(paramod,[status(thm)],[c_29,c_964]) ).
cnf(c_690,plain,
product(product(A,a10),a8) = product(product(A,a10),a4),
inference(copy,[status(thm)],[c_965]) ).
cnf(c_695,plain,
product(a10,product(a4,a9)) = product(a4,a10),
inference(paramod,[status(thm)],[c_629,c_472]) ).
cnf(c_696,plain,
product(a10,product(a4,a10)) = product(a7,a10),
inference(paramod,[status(thm)],[c_629,c_471]) ).
cnf(c_966,plain,
product(a9,product(a4,a10)) = product(a1,a9),
inference(paramod,[status(thm)],[c_629,c_67]) ).
cnf(c_717,plain,
product(a3,product(a4,a10)) = product(a1,a9),
inference(paramod,[status(thm)],[c_626,c_966]) ).
cnf(c_967,plain,
product(product(A,product(a4,a3)),a10) = product(product(A,a4),a2),
inference(paramod,[status(thm)],[c_665,c_654]) ).
cnf(c_968,plain,
product(product(A,a10),a10) = product(product(A,a4),a2),
inference(paramod,[status(thm)],[c_56,c_967]) ).
cnf(c_969,plain,
A = product(product(A,a4),a2),
inference(paramod,[status(thm)],[c_2,c_968]) ).
cnf(c_746,plain,
product(product(A,a4),a2) = A,
inference(copy,[status(thm)],[c_969]) ).
cnf(c_970,plain,
product(product(product(a4,a3),A),a10) = product(a3,product(A,a10)),
inference(paramod,[status(thm)],[c_667,c_658]) ).
cnf(c_971,plain,
product(product(a10,A),a10) = product(a3,product(A,a10)),
inference(paramod,[status(thm)],[c_56,c_970]) ).
cnf(c_972,plain,
product(a10,product(A,a10)) = product(a3,product(A,a10)),
inference(paramod,[status(thm)],[c_27,c_971]) ).
cnf(c_747,plain,
product(a3,product(A,a10)) = product(a10,product(A,a10)),
inference(copy,[status(thm)],[c_972]) ).
cnf(c_973,plain,
product(product(product(A,a4),a10),a4) = product(A,product(a4,a7)),
inference(paramod,[status(thm)],[c_690,c_328]) ).
cnf(c_974,plain,
product(A,product(a10,a4)) = product(A,product(a4,a7)),
inference(paramod,[status(thm)],[c_28,c_973]) ).
cnf(c_975,plain,
product(A,product(a4,a2)) = product(A,product(a4,a7)),
inference(paramod,[status(thm)],[c_70,c_974]) ).
cnf(c_754,plain,
product(A,product(a4,a7)) = product(A,product(a4,a2)),
inference(copy,[status(thm)],[c_975]) ).
cnf(c_780,plain,
product(A,product(a4,a9)) = product(A,product(a4,a10)),
inference(paramod,[status(thm)],[c_746,c_615]) ).
cnf(c_976,plain,
product(A,a1) = product(A,product(a4,a2)),
inference(paramod,[status(thm)],[c_746,c_217]) ).
cnf(c_783,plain,
product(A,product(a4,a2)) = product(A,a1),
inference(copy,[status(thm)],[c_976]) ).
cnf(c_786,plain,
product(product(A,a3),a4) = A,
inference(paramod,[status(thm)],[c_746,c_40]) ).
cnf(c_977,plain,
product(a10,product(a4,a10)) = product(a1,a9),
inference(paramod,[status(thm)],[c_747,c_717]) ).
cnf(c_787,plain,
product(a7,a10) = product(a1,a9),
inference(paramod,[status(thm)],[c_696,c_977]) ).
cnf(c_978,plain,
product(product(product(A,a1),a6),product(a4,a2)) = product(A,a8),
inference(paramod,[status(thm)],[c_754,c_356]) ).
cnf(c_979,plain,
product(product(product(A,a1),a6),a1) = product(A,a8),
inference(paramod,[status(thm)],[c_783,c_978]) ).
cnf(c_980,plain,
product(product(product(A,a1),a1),a7) = product(A,a8),
inference(paramod,[status(thm)],[c_49,c_979]) ).
cnf(c_981,plain,
product(A,a7) = product(A,a8),
inference(paramod,[status(thm)],[c_2,c_980]) ).
cnf(c_796,plain,
product(A,a8) = product(A,a7),
inference(copy,[status(thm)],[c_981]) ).
cnf(c_982,plain,
product(a1,product(a4,a2)) = a4,
inference(paramod,[status(thm)],[c_754,c_331]) ).
cnf(c_983,plain,
product(a1,a1) = a4,
inference(paramod,[status(thm)],[c_783,c_982]) ).
cnf(c_804,plain,
a1 = a4,
inference(paramod,[status(thm)],[c_1,c_983]) ).
cnf(c_984,plain,
product(a10,product(a4,a10)) = product(a4,a10),
inference(paramod,[status(thm)],[c_780,c_695]) ).
cnf(c_985,plain,
product(a7,a10) = product(a4,a10),
inference(paramod,[status(thm)],[c_696,c_984]) ).
cnf(c_986,plain,
product(a1,a9) = product(a4,a10),
inference(paramod,[status(thm)],[c_787,c_985]) ).
cnf(c_813,plain,
product(a4,a9) = product(a4,a10),
inference(paramod,[status(thm)],[c_804,c_986]) ).
cnf(c_987,plain,
product(a3,product(a4,a10)) = a5,
inference(paramod,[status(thm)],[c_813,c_608]) ).
cnf(c_988,plain,
product(a10,product(a4,a10)) = a5,
inference(paramod,[status(thm)],[c_747,c_987]) ).
cnf(c_989,plain,
product(a7,a10) = a5,
inference(paramod,[status(thm)],[c_696,c_988]) ).
cnf(c_990,plain,
product(a1,a9) = a5,
inference(paramod,[status(thm)],[c_787,c_989]) ).
cnf(c_991,plain,
product(a4,a9) = a5,
inference(paramod,[status(thm)],[c_804,c_990]) ).
cnf(c_820,plain,
product(a4,a10) = a5,
inference(paramod,[status(thm)],[c_813,c_991]) ).
cnf(c_992,plain,
product(a5,product(a4,a10)) = a3,
inference(paramod,[status(thm)],[c_813,c_607]) ).
cnf(c_993,plain,
product(a5,a5) = a3,
inference(paramod,[status(thm)],[c_820,c_992]) ).
cnf(c_821,plain,
a5 = a3,
inference(paramod,[status(thm)],[c_1,c_993]) ).
cnf(c_994,plain,
product(product(product(A,a3),a4),a2) = product(A,product(a4,a9)),
inference(paramod,[status(thm)],[c_804,c_592]) ).
cnf(c_995,plain,
product(A,a2) = product(A,product(a4,a9)),
inference(paramod,[status(thm)],[c_786,c_994]) ).
cnf(c_996,plain,
product(A,a2) = product(A,product(a4,a10)),
inference(paramod,[status(thm)],[c_813,c_995]) ).
cnf(c_997,plain,
product(A,a2) = product(A,a5),
inference(paramod,[status(thm)],[c_820,c_996]) ).
cnf(c_998,plain,
product(A,a2) = product(A,a3),
inference(paramod,[status(thm)],[c_821,c_997]) ).
cnf(c_823,plain,
product(A,a3) = product(A,a2),
inference(copy,[status(thm)],[c_998]) ).
cnf(c_999,plain,
product(a4,product(a4,product(a4,a2))) = a6,
inference(paramod,[status(thm)],[c_804,c_637]) ).
cnf(c_1000,plain,
product(a4,product(a4,a1)) = a6,
inference(paramod,[status(thm)],[c_783,c_999]) ).
cnf(c_1001,plain,
product(a4,product(a4,a4)) = a6,
inference(paramod,[status(thm)],[c_804,c_1000]) ).
cnf(c_1002,plain,
product(a4,a4) = a6,
inference(paramod,[status(thm)],[c_1,c_1001]) ).
cnf(c_1003,plain,
a4 = a6,
inference(paramod,[status(thm)],[c_1,c_1002]) ).
cnf(c_834,plain,
a6 = a4,
inference(copy,[status(thm)],[c_1003]) ).
cnf(c_1004,plain,
product(product(a4,a10),a2) = product(a3,product(a4,a2)),
inference(paramod,[status(thm)],[c_813,c_437]) ).
cnf(c_1005,plain,
product(a5,a2) = product(a3,product(a4,a2)),
inference(paramod,[status(thm)],[c_820,c_1004]) ).
cnf(c_1006,plain,
product(a3,a2) = product(a3,product(a4,a2)),
inference(paramod,[status(thm)],[c_821,c_1005]) ).
cnf(c_1007,plain,
a1 = product(a3,product(a4,a2)),
inference(paramod,[status(thm)],[c_35,c_1006]) ).
cnf(c_1008,plain,
a4 = product(a3,product(a4,a2)),
inference(paramod,[status(thm)],[c_804,c_1007]) ).
cnf(c_1009,plain,
a4 = product(a3,a1),
inference(paramod,[status(thm)],[c_783,c_1008]) ).
cnf(c_1010,plain,
a4 = product(a3,a4),
inference(paramod,[status(thm)],[c_804,c_1009]) ).
cnf(c_1011,plain,
a4 = a2,
inference(paramod,[status(thm)],[c_10,c_1010]) ).
cnf(c_835,plain,
a2 = a4,
inference(copy,[status(thm)],[c_1011]) ).
cnf(c_1012,plain,
product(a10,a5) = product(a7,a10),
inference(paramod,[status(thm)],[c_820,c_696]) ).
cnf(c_1013,plain,
product(a10,a3) = product(a7,a10),
inference(paramod,[status(thm)],[c_821,c_1012]) ).
cnf(c_1014,plain,
product(a10,a2) = product(a7,a10),
inference(paramod,[status(thm)],[c_823,c_1013]) ).
cnf(c_1015,plain,
product(a10,a4) = product(a7,a10),
inference(paramod,[status(thm)],[c_835,c_1014]) ).
cnf(c_1016,plain,
product(a4,a2) = product(a7,a10),
inference(paramod,[status(thm)],[c_70,c_1015]) ).
cnf(c_1017,plain,
product(a4,a4) = product(a7,a10),
inference(paramod,[status(thm)],[c_835,c_1016]) ).
cnf(c_1018,plain,
a4 = product(a7,a10),
inference(paramod,[status(thm)],[c_1,c_1017]) ).
cnf(c_1019,plain,
a4 = product(a1,a9),
inference(paramod,[status(thm)],[c_787,c_1018]) ).
cnf(c_1020,plain,
a4 = product(a4,a9),
inference(paramod,[status(thm)],[c_804,c_1019]) ).
cnf(c_1021,plain,
a4 = product(a4,a10),
inference(paramod,[status(thm)],[c_813,c_1020]) ).
cnf(c_1022,plain,
a4 = a5,
inference(paramod,[status(thm)],[c_820,c_1021]) ).
cnf(c_1023,plain,
a4 = a3,
inference(paramod,[status(thm)],[c_821,c_1022]) ).
cnf(c_840,plain,
a3 = a4,
inference(copy,[status(thm)],[c_1023]) ).
cnf(c_1024,plain,
product(a7,a7) = a10,
inference(paramod,[status(thm)],[c_796,c_79]) ).
cnf(c_853,plain,
a7 = a10,
inference(paramod,[status(thm)],[c_1,c_1024]) ).
cnf(c_1025,plain,
product(a4,a7) = a9,
inference(paramod,[status(thm)],[c_796,c_24]) ).
cnf(c_1026,plain,
product(a4,a10) = a9,
inference(paramod,[status(thm)],[c_853,c_1025]) ).
cnf(c_1027,plain,
a5 = a9,
inference(paramod,[status(thm)],[c_820,c_1026]) ).
cnf(c_1028,plain,
a3 = a9,
inference(paramod,[status(thm)],[c_821,c_1027]) ).
cnf(c_1029,plain,
a4 = a9,
inference(paramod,[status(thm)],[c_840,c_1028]) ).
cnf(c_855,plain,
a9 = a4,
inference(copy,[status(thm)],[c_1029]) ).
cnf(c_1030,plain,
product(a10,a10) = product(a1,a9),
inference(paramod,[status(thm)],[c_853,c_787]) ).
cnf(c_1031,plain,
a10 = product(a1,a9),
inference(paramod,[status(thm)],[c_1,c_1030]) ).
cnf(c_1032,plain,
a10 = product(a4,a9),
inference(paramod,[status(thm)],[c_804,c_1031]) ).
cnf(c_1033,plain,
a10 = product(a4,a4),
inference(paramod,[status(thm)],[c_855,c_1032]) ).
cnf(c_857,plain,
a10 = a4,
inference(paramod,[status(thm)],[c_1,c_1033]) ).
cnf(c_1034,plain,
tuple(a4,a10,a9,a7,a8,a3,a4,a5,a6) != tuple(a1,a9,a8,a6,a7,a2,a3,a4,a5),
inference(paramod,[status(thm)],[c_835,c_26]) ).
cnf(c_1035,plain,
tuple(a4,a4,a9,a7,a8,a3,a4,a5,a6) != tuple(a1,a9,a8,a6,a7,a2,a3,a4,a5),
inference(paramod,[status(thm)],[c_857,c_1034]) ).
cnf(c_1036,plain,
tuple(a4,a4,a4,a7,a8,a3,a4,a5,a6) != tuple(a1,a9,a8,a6,a7,a2,a3,a4,a5),
inference(paramod,[status(thm)],[c_855,c_1035]) ).
cnf(c_1037,plain,
tuple(a4,a4,a4,a10,a8,a3,a4,a5,a6) != tuple(a1,a9,a8,a6,a7,a2,a3,a4,a5),
inference(paramod,[status(thm)],[c_853,c_1036]) ).
cnf(c_1038,plain,
tuple(a4,a4,a4,a4,a8,a3,a4,a5,a6) != tuple(a1,a9,a8,a6,a7,a2,a3,a4,a5),
inference(paramod,[status(thm)],[c_857,c_1037]) ).
cnf(c_1039,plain,
tuple(a4,a4,a4,a4,a8,a4,a4,a5,a6) != tuple(a1,a9,a8,a6,a7,a2,a3,a4,a5),
inference(paramod,[status(thm)],[c_840,c_1038]) ).
cnf(c_1040,plain,
tuple(a4,a4,a4,a4,a8,a4,a4,a3,a6) != tuple(a1,a9,a8,a6,a7,a2,a3,a4,a5),
inference(paramod,[status(thm)],[c_821,c_1039]) ).
cnf(c_1041,plain,
tuple(a4,a4,a4,a4,a8,a4,a4,a4,a6) != tuple(a1,a9,a8,a6,a7,a2,a3,a4,a5),
inference(paramod,[status(thm)],[c_840,c_1040]) ).
cnf(c_1042,plain,
tuple(a4,a4,a4,a4,a8,a4,a4,a4,a4) != tuple(a1,a9,a8,a6,a7,a2,a3,a4,a5),
inference(paramod,[status(thm)],[c_834,c_1041]) ).
cnf(c_1043,plain,
tuple(a4,a4,a4,a4,a8,a4,a4,a4,a4) != tuple(a4,a9,a8,a6,a7,a2,a3,a4,a5),
inference(paramod,[status(thm)],[c_804,c_1042]) ).
cnf(c_1044,plain,
tuple(a4,a4,a4,a4,a8,a4,a4,a4,a4) != tuple(a4,a4,a8,a6,a7,a2,a3,a4,a5),
inference(paramod,[status(thm)],[c_855,c_1043]) ).
cnf(c_1045,plain,
tuple(a4,a4,a4,a4,a8,a4,a4,a4,a4) != tuple(a4,a4,a8,a4,a7,a2,a3,a4,a5),
inference(paramod,[status(thm)],[c_834,c_1044]) ).
cnf(c_1046,plain,
tuple(a4,a4,a4,a4,a8,a4,a4,a4,a4) != tuple(a4,a4,a8,a4,a10,a2,a3,a4,a5),
inference(paramod,[status(thm)],[c_853,c_1045]) ).
cnf(c_1047,plain,
tuple(a4,a4,a4,a4,a8,a4,a4,a4,a4) != tuple(a4,a4,a8,a4,a4,a2,a3,a4,a5),
inference(paramod,[status(thm)],[c_857,c_1046]) ).
cnf(c_1048,plain,
tuple(a4,a4,a4,a4,a8,a4,a4,a4,a4) != tuple(a4,a4,a8,a4,a4,a4,a3,a4,a5),
inference(paramod,[status(thm)],[c_835,c_1047]) ).
cnf(c_1049,plain,
tuple(a4,a4,a4,a4,a8,a4,a4,a4,a4) != tuple(a4,a4,a8,a4,a4,a4,a4,a4,a5),
inference(paramod,[status(thm)],[c_840,c_1048]) ).
cnf(c_1050,plain,
tuple(a4,a4,a4,a4,a8,a4,a4,a4,a4) != tuple(a4,a4,a8,a4,a4,a4,a4,a4,a3),
inference(paramod,[status(thm)],[c_821,c_1049]) ).
cnf(c_1051,plain,
tuple(a4,a4,a4,a4,a8,a4,a4,a4,a4) != tuple(a4,a4,a8,a4,a4,a4,a4,a4,a4),
inference(paramod,[status(thm)],[c_840,c_1050]) ).
cnf(c_858,plain,
tuple(a4,a4,a8,a4,a4,a4,a4,a4,a4) != tuple(a4,a4,a4,a4,a8,a4,a4,a4,a4),
inference(copy,[status(thm)],[c_1051]) ).
cnf(c_1052,plain,
product(a4,product(a8,a7)) = a8,
inference(paramod,[status(thm)],[c_834,c_490]) ).
cnf(c_1053,plain,
product(a4,product(a8,a10)) = a8,
inference(paramod,[status(thm)],[c_853,c_1052]) ).
cnf(c_1054,plain,
product(a4,product(a8,a4)) = a8,
inference(paramod,[status(thm)],[c_857,c_1053]) ).
cnf(c_1055,plain,
product(a4,a7) = a8,
inference(paramod,[status(thm)],[c_50,c_1054]) ).
cnf(c_1056,plain,
product(a4,a10) = a8,
inference(paramod,[status(thm)],[c_853,c_1055]) ).
cnf(c_1057,plain,
product(a4,a4) = a8,
inference(paramod,[status(thm)],[c_857,c_1056]) ).
cnf(c_1058,plain,
a4 = a8,
inference(paramod,[status(thm)],[c_1,c_1057]) ).
cnf(c_861,plain,
a8 = a4,
inference(copy,[status(thm)],[c_1058]) ).
cnf(c_1059,plain,
tuple(a4,a4,a4,a4,a4,a4,a4,a4,a4) != tuple(a4,a4,a4,a4,a8,a4,a4,a4,a4),
inference(paramod,[status(thm)],[c_861,c_858]) ).
cnf(c_1060,plain,
tuple(a4,a4,a4,a4,a4,a4,a4,a4,a4) != tuple(a4,a4,a4,a4,a4,a4,a4,a4,a4),
inference(paramod,[status(thm)],[c_861,c_1059]) ).
cnf(c_864,plain,
$false,
inference(copy,[status(thm)],[c_1060]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP049-1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.38 % Computer : n009.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sat Sep 26 20:49:30 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.39 % Process 1104835 was started by sandbox2 on n009,
% 0.12/0.39 % Sat Sep 26 20:49:30 2026
% 0.12/0.39 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.39
% 0.12/0.39 % From the command line: assign(max_seconds, 300).
% 1.74/0.67
% 1.74/0.67 % SZS status Unsatisfiable for theBenchmark
% 1.74/0.67
% 1.74/0.67 % Proof 1 at 0.17 (+ 0.09) seconds.
% 1.74/0.67 % Length of proof is 141.
% 1.74/0.67 % Level of proof is 20.
% 1.74/0.67 % Maximum clause weight is 76.000.
% 1.74/0.67 % Given clauses 71.
% 1.74/0.67
% 1.74/0.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------