%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : TOP051-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 : n001.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.67s 0.52s
% Output : CNFRefutation 0.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 76
% Number of leaves : 14
% Syntax : Number of formulae : 299 ( 299 unt; 0 def)
% Number of atoms : 299 ( 298 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 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-10 aty)
% Number of variables : 139 ( 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,a6) = a2,
file('theBenchmark.p',knot) ).
cnf(c_5,plain,
product(a1,a6) = a2,
inference(clausify,[status(thm)],[knot]) ).
fof(knot_03,axiom,
product(a2,a7) = a3,
file('theBenchmark.p',knot_03) ).
cnf(c_6,plain,
product(a2,a7) = a3,
inference(clausify,[status(thm)],[knot_03]) ).
fof(knot_04,axiom,
product(a3,a1) = a4,
file('theBenchmark.p',knot_04) ).
cnf(c_7,plain,
product(a3,a1) = a4,
inference(clausify,[status(thm)],[knot_04]) ).
fof(knot_05,axiom,
product(a4,a10) = a5,
file('theBenchmark.p',knot_05) ).
cnf(c_8,plain,
product(a4,a10) = a5,
inference(clausify,[status(thm)],[knot_05]) ).
fof(knot_06,axiom,
product(a5,a9) = a6,
file('theBenchmark.p',knot_06) ).
cnf(c_9,plain,
product(a5,a9) = a6,
inference(clausify,[status(thm)],[knot_06]) ).
fof(knot_07,axiom,
product(a6,a2) = a7,
file('theBenchmark.p',knot_07) ).
cnf(c_10,plain,
product(a6,a2) = a7,
inference(clausify,[status(thm)],[knot_07]) ).
fof(knot_08,axiom,
product(a7,a3) = a8,
file('theBenchmark.p',knot_08) ).
cnf(c_11,plain,
product(a7,a3) = a8,
inference(clausify,[status(thm)],[knot_08]) ).
fof(knot_09,axiom,
product(a8,a6) = a9,
file('theBenchmark.p',knot_09) ).
cnf(c_12,plain,
product(a8,a6) = a9,
inference(clausify,[status(thm)],[knot_09]) ).
fof(knot_10,axiom,
product(a9,a4) = a10,
file('theBenchmark.p',knot_10) ).
cnf(c_13,plain,
product(a9,a4) = a10,
inference(clausify,[status(thm)],[knot_10]) ).
fof(knot_11,axiom,
product(a10,a5) = a11,
file('theBenchmark.p',knot_11) ).
cnf(c_14,plain,
product(a10,a5) = a11,
inference(clausify,[status(thm)],[knot_11]) ).
fof(goal,axiom,
tuple(a1,a6,a5,a2,a7,a3,a4,a9,a10,a8) != tuple(a2,a7,a6,a3,a8,a4,a5,a10,a11,a9),
file('theBenchmark.p',goal) ).
cnf(c_15,plain,
tuple(a1,a6,a5,a2,a7,a3,a4,a9,a10,a8) != tuple(a2,a7,a6,a3,a8,a4,a5,a10,a11,a9),
inference(clausify,[status(thm)],[goal]) ).
cnf(c_686,plain,
product(A,product(B,A)) = product(product(A,B),A),
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_16,plain,
product(product(A,B),A) = product(A,product(B,A)),
inference(copy,[status(thm)],[c_686]) ).
cnf(c_687,plain,
product(A,product(B,C)) = product(product(product(A,C),B),C),
inference(paramod,[status(thm)],[c_2,c_4]) ).
cnf(c_17,plain,
product(product(product(A,B),C),B) = product(A,product(C,B)),
inference(copy,[status(thm)],[c_687]) ).
cnf(c_688,plain,
product(product(A,B),C) = product(product(A,product(C,B)),B),
inference(paramod,[status(thm)],[c_2,c_4]) ).
cnf(c_18,plain,
product(product(A,product(B,C)),C) = product(product(A,C),B),
inference(copy,[status(thm)],[c_688]) ).
cnf(c_19,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_21,plain,
product(a2,a6) = a1,
inference(paramod,[status(thm)],[c_5,c_2]) ).
cnf(c_689,plain,
product(a2,product(A,a6)) = product(product(a1,A),a6),
inference(paramod,[status(thm)],[c_5,c_4]) ).
cnf(c_22,plain,
product(product(a1,A),a6) = product(a2,product(A,a6)),
inference(copy,[status(thm)],[c_689]) ).
cnf(c_690,plain,
product(product(A,a6),a2) = product(product(A,a1),a6),
inference(paramod,[status(thm)],[c_5,c_4]) ).
cnf(c_23,plain,
product(product(A,a1),a6) = product(product(A,a6),a2),
inference(copy,[status(thm)],[c_690]) ).
cnf(c_24,plain,
product(a3,a7) = a2,
inference(paramod,[status(thm)],[c_6,c_2]) ).
cnf(c_691,plain,
product(a3,product(A,a7)) = product(product(a2,A),a7),
inference(paramod,[status(thm)],[c_6,c_4]) ).
cnf(c_25,plain,
product(product(a2,A),a7) = product(a3,product(A,a7)),
inference(copy,[status(thm)],[c_691]) ).
cnf(c_26,plain,
product(product(A,a7),a3) = product(product(A,a2),a7),
inference(paramod,[status(thm)],[c_6,c_4]) ).
cnf(c_35,plain,
product(product(A,a9),a6) = product(product(A,a5),a9),
inference(paramod,[status(thm)],[c_9,c_4]) ).
cnf(c_36,plain,
product(a7,a2) = a6,
inference(paramod,[status(thm)],[c_10,c_2]) ).
cnf(c_38,plain,
product(product(A,a2),a7) = product(product(A,a6),a2),
inference(paramod,[status(thm)],[c_10,c_4]) ).
cnf(c_39,plain,
product(product(A,a7),a3) = product(product(A,a6),a2),
inference(paramod,[status(thm)],[c_38,c_26]) ).
cnf(c_40,plain,
product(a8,a3) = a7,
inference(paramod,[status(thm)],[c_11,c_2]) ).
cnf(c_692,plain,
product(product(A,a3),a8) = product(product(A,a7),a3),
inference(paramod,[status(thm)],[c_11,c_4]) ).
cnf(c_42,plain,
product(product(A,a3),a8) = product(product(A,a6),a2),
inference(paramod,[status(thm)],[c_39,c_692]) ).
cnf(c_43,plain,
product(a9,a6) = a8,
inference(paramod,[status(thm)],[c_12,c_2]) ).
cnf(c_693,plain,
product(product(A,a6),a9) = product(product(A,a8),a6),
inference(paramod,[status(thm)],[c_12,c_4]) ).
cnf(c_45,plain,
product(product(A,a8),a6) = product(product(A,a6),a9),
inference(copy,[status(thm)],[c_693]) ).
cnf(c_46,plain,
product(a10,a4) = a9,
inference(paramod,[status(thm)],[c_13,c_2]) ).
cnf(c_694,plain,
product(a2,a1) = product(a1,product(a6,a1)),
inference(paramod,[status(thm)],[c_5,c_16]) ).
cnf(c_56,plain,
product(a1,product(a6,a1)) = product(a2,a1),
inference(copy,[status(thm)],[c_694]) ).
cnf(c_695,plain,
product(a3,a2) = product(a2,product(a7,a2)),
inference(paramod,[status(thm)],[c_6,c_16]) ).
cnf(c_696,plain,
product(a3,a2) = product(a2,a6),
inference(paramod,[status(thm)],[c_36,c_695]) ).
cnf(c_57,plain,
product(a3,a2) = a1,
inference(paramod,[status(thm)],[c_21,c_696]) ).
cnf(c_697,plain,
product(product(a7,a2),a7) = product(a7,a3),
inference(paramod,[status(thm)],[c_6,c_16]) ).
cnf(c_698,plain,
product(a6,a7) = product(a7,a3),
inference(paramod,[status(thm)],[c_36,c_697]) ).
cnf(c_58,plain,
product(a6,a7) = a8,
inference(paramod,[status(thm)],[c_11,c_698]) ).
cnf(c_699,plain,
product(product(a10,a4),a10) = product(a10,a5),
inference(paramod,[status(thm)],[c_8,c_16]) ).
cnf(c_700,plain,
product(a9,a10) = product(a10,a5),
inference(paramod,[status(thm)],[c_46,c_699]) ).
cnf(c_61,plain,
product(a9,a10) = a11,
inference(paramod,[status(thm)],[c_14,c_700]) ).
cnf(c_701,plain,
product(a7,a6) = product(a6,product(a2,a6)),
inference(paramod,[status(thm)],[c_10,c_16]) ).
cnf(c_63,plain,
product(a7,a6) = product(a6,a1),
inference(paramod,[status(thm)],[c_21,c_701]) ).
cnf(c_702,plain,
product(product(a2,a6),a2) = product(a2,a7),
inference(paramod,[status(thm)],[c_10,c_16]) ).
cnf(c_703,plain,
product(a1,a2) = product(a2,a7),
inference(paramod,[status(thm)],[c_21,c_702]) ).
cnf(c_64,plain,
product(a1,a2) = a3,
inference(paramod,[status(thm)],[c_6,c_703]) ).
cnf(c_704,plain,
product(product(a3,a7),a3) = product(a3,a8),
inference(paramod,[status(thm)],[c_11,c_16]) ).
cnf(c_705,plain,
product(a2,a3) = product(a3,a8),
inference(paramod,[status(thm)],[c_24,c_704]) ).
cnf(c_66,plain,
product(a3,a8) = product(a2,a3),
inference(copy,[status(thm)],[c_705]) ).
cnf(c_706,plain,
product(a10,a9) = product(a9,product(a4,a9)),
inference(paramod,[status(thm)],[c_13,c_16]) ).
cnf(c_68,plain,
product(a9,product(a4,a9)) = product(a10,a9),
inference(copy,[status(thm)],[c_706]) ).
cnf(c_707,plain,
product(a1,product(A,a6)) = product(product(a2,A),a6),
inference(paramod,[status(thm)],[c_21,c_4]) ).
cnf(c_72,plain,
product(product(a2,A),a6) = product(a1,product(A,a6)),
inference(copy,[status(thm)],[c_707]) ).
cnf(c_708,plain,
product(product(product(A,a3),a8),a3) = product(A,a7),
inference(paramod,[status(thm)],[c_40,c_17]) ).
cnf(c_107,plain,
product(product(product(A,a6),a2),a3) = product(A,a7),
inference(paramod,[status(thm)],[c_42,c_708]) ).
cnf(c_709,plain,
product(product(A,a6),a8) = product(product(A,a9),a6),
inference(paramod,[status(thm)],[c_43,c_4]) ).
cnf(c_710,plain,
product(product(A,a6),a8) = product(product(A,a5),a9),
inference(paramod,[status(thm)],[c_35,c_709]) ).
cnf(c_108,plain,
product(product(A,a5),a9) = product(product(A,a6),a8),
inference(copy,[status(thm)],[c_710]) ).
cnf(c_109,plain,
product(product(A,a9),a6) = product(product(A,a6),a8),
inference(paramod,[status(thm)],[c_108,c_35]) ).
cnf(c_110,plain,
product(product(A,a4),a9) = product(product(A,a10),a4),
inference(paramod,[status(thm)],[c_46,c_4]) ).
cnf(c_711,plain,
product(a8,a6) = product(a6,product(a7,a6)),
inference(paramod,[status(thm)],[c_58,c_16]) ).
cnf(c_712,plain,
a9 = product(a6,product(a7,a6)),
inference(paramod,[status(thm)],[c_12,c_711]) ).
cnf(c_713,plain,
a9 = product(a6,product(a6,a1)),
inference(paramod,[status(thm)],[c_63,c_712]) ).
cnf(c_120,plain,
product(a6,product(a6,a1)) = a9,
inference(copy,[status(thm)],[c_713]) ).
cnf(c_126,plain,
product(product(A,a1),a2) = product(product(A,a2),a3),
inference(paramod,[status(thm)],[c_57,c_18]) ).
cnf(c_714,plain,
product(a3,a1) = product(a1,product(a2,a1)),
inference(paramod,[status(thm)],[c_64,c_16]) ).
cnf(c_715,plain,
a4 = product(a1,product(a2,a1)),
inference(paramod,[status(thm)],[c_7,c_714]) ).
cnf(c_133,plain,
product(a1,product(a2,a1)) = a4,
inference(copy,[status(thm)],[c_715]) ).
cnf(c_220,plain,
product(a9,product(a6,a1)) = a6,
inference(paramod,[status(thm)],[c_120,c_2]) ).
cnf(c_716,plain,
product(product(product(a6,a1),a6),a1) = a9,
inference(paramod,[status(thm)],[c_120,c_17]) ).
cnf(c_717,plain,
product(product(a6,product(a1,a6)),a1) = a9,
inference(paramod,[status(thm)],[c_16,c_716]) ).
cnf(c_718,plain,
product(product(a6,a2),a1) = a9,
inference(paramod,[status(thm)],[c_5,c_717]) ).
cnf(c_226,plain,
product(a7,a1) = a9,
inference(paramod,[status(thm)],[c_10,c_718]) ).
cnf(c_719,plain,
product(a9,a1) = product(product(a6,a1),a6),
inference(paramod,[status(thm)],[c_120,c_18]) ).
cnf(c_720,plain,
product(a9,a1) = product(a6,product(a1,a6)),
inference(paramod,[status(thm)],[c_16,c_719]) ).
cnf(c_721,plain,
product(a9,a1) = product(a6,a2),
inference(paramod,[status(thm)],[c_5,c_720]) ).
cnf(c_228,plain,
product(a9,a1) = a7,
inference(paramod,[status(thm)],[c_10,c_721]) ).
cnf(c_722,plain,
product(product(product(A,a6),a1),a9) = product(product(product(A,a1),a6),product(a6,a1)),
inference(paramod,[status(thm)],[c_120,c_19]) ).
cnf(c_723,plain,
product(product(product(A,a6),a1),a9) = product(product(product(A,a6),a2),product(a6,a1)),
inference(paramod,[status(thm)],[c_23,c_722]) ).
cnf(c_231,plain,
product(product(product(A,a6),a2),product(a6,a1)) = product(product(product(A,a6),a1),a9),
inference(copy,[status(thm)],[c_723]) ).
cnf(c_233,plain,
product(product(A,a1),a9) = product(product(A,a7),a1),
inference(paramod,[status(thm)],[c_226,c_4]) ).
cnf(c_239,plain,
product(product(product(A,a6),a2),product(a6,a1)) = product(product(product(A,a6),a7),a1),
inference(paramod,[status(thm)],[c_233,c_231]) ).
cnf(c_309,plain,
product(a4,product(a2,a1)) = a1,
inference(paramod,[status(thm)],[c_133,c_2]) ).
cnf(c_724,plain,
product(product(product(A,product(a2,a1)),a1),product(a2,a1)) = product(A,a4),
inference(paramod,[status(thm)],[c_133,c_17]) ).
cnf(c_725,plain,
product(product(product(A,a1),a2),product(a2,a1)) = product(A,a4),
inference(paramod,[status(thm)],[c_18,c_724]) ).
cnf(c_314,plain,
product(product(product(A,a2),a3),product(a2,a1)) = product(A,a4),
inference(paramod,[status(thm)],[c_126,c_725]) ).
cnf(c_726,plain,
product(product(A,a4),product(a2,a1)) = product(product(A,product(a2,a1)),a1),
inference(paramod,[status(thm)],[c_133,c_18]) ).
cnf(c_727,plain,
product(product(A,a4),product(a2,a1)) = product(product(A,a1),a2),
inference(paramod,[status(thm)],[c_18,c_726]) ).
cnf(c_315,plain,
product(product(A,a4),product(a2,a1)) = product(product(A,a2),a3),
inference(paramod,[status(thm)],[c_126,c_727]) ).
cnf(c_728,plain,
product(product(product(A,a6),a1),a6) = product(product(product(A,a1),a9),product(a6,a1)),
inference(paramod,[status(thm)],[c_220,c_19]) ).
cnf(c_729,plain,
product(product(product(A,a6),a6),a2) = product(product(product(A,a1),a9),product(a6,a1)),
inference(paramod,[status(thm)],[c_23,c_728]) ).
cnf(c_730,plain,
product(A,a2) = product(product(product(A,a1),a9),product(a6,a1)),
inference(paramod,[status(thm)],[c_2,c_729]) ).
cnf(c_731,plain,
product(A,a2) = product(product(product(A,a7),a1),product(a6,a1)),
inference(paramod,[status(thm)],[c_233,c_730]) ).
cnf(c_732,plain,
product(A,a2) = product(product(product(A,a7),a6),a1),
inference(paramod,[status(thm)],[c_4,c_731]) ).
cnf(c_324,plain,
product(product(product(A,a7),a6),a1) = product(A,a2),
inference(copy,[status(thm)],[c_732]) ).
cnf(c_733,plain,
product(product(a1,a2),a6) = product(a2,a1),
inference(paramod,[status(thm)],[c_21,c_22]) ).
cnf(c_358,plain,
product(a3,a6) = product(a2,a1),
inference(paramod,[status(thm)],[c_64,c_733]) ).
cnf(c_734,plain,
product(a4,a6) = product(a2,product(product(a2,a1),a6)),
inference(paramod,[status(thm)],[c_133,c_22]) ).
cnf(c_735,plain,
product(a4,a6) = product(a2,product(product(a2,a6),a2)),
inference(paramod,[status(thm)],[c_23,c_734]) ).
cnf(c_736,plain,
product(a4,a6) = product(a2,product(a1,a2)),
inference(paramod,[status(thm)],[c_21,c_735]) ).
cnf(c_362,plain,
product(a4,a6) = product(a2,a3),
inference(paramod,[status(thm)],[c_64,c_736]) ).
cnf(c_737,plain,
product(product(A,product(a6,a1)),product(a2,a1)) = product(product(A,a1),product(a6,a1)),
inference(paramod,[status(thm)],[c_56,c_4]) ).
cnf(c_396,plain,
product(product(A,product(a6,a1)),product(a2,a1)) = product(product(A,a6),a1),
inference(paramod,[status(thm)],[c_4,c_737]) ).
cnf(c_738,plain,
product(product(product(A,product(a6,a1)),a1),product(a6,a1)) = product(A,product(a2,a1)),
inference(paramod,[status(thm)],[c_56,c_17]) ).
cnf(c_739,plain,
product(product(product(A,a1),a6),product(a6,a1)) = product(A,product(a2,a1)),
inference(paramod,[status(thm)],[c_18,c_738]) ).
cnf(c_740,plain,
product(product(product(A,a6),a2),product(a6,a1)) = product(A,product(a2,a1)),
inference(paramod,[status(thm)],[c_23,c_739]) ).
cnf(c_397,plain,
product(product(product(A,a6),a7),a1) = product(A,product(a2,a1)),
inference(paramod,[status(thm)],[c_239,c_740]) ).
cnf(c_741,plain,
product(product(product(A,a6),a1),product(a2,a1)) = product(product(product(A,a1),a1),product(a6,a1)),
inference(paramod,[status(thm)],[c_56,c_19]) ).
cnf(c_742,plain,
product(product(product(A,a6),a2),a1) = product(product(product(A,a1),a1),product(a6,a1)),
inference(paramod,[status(thm)],[c_4,c_741]) ).
cnf(c_400,plain,
product(product(product(A,a6),a2),a1) = product(A,product(a6,a1)),
inference(paramod,[status(thm)],[c_2,c_742]) ).
cnf(c_404,plain,
product(product(product(A,a6),a2),product(a6,a1)) = product(A,product(a2,a1)),
inference(paramod,[status(thm)],[c_397,c_239]) ).
cnf(c_743,plain,
product(product(a9,a1),a6) = product(a8,a2),
inference(paramod,[status(thm)],[c_43,c_23]) ).
cnf(c_744,plain,
product(a7,a6) = product(a8,a2),
inference(paramod,[status(thm)],[c_228,c_743]) ).
cnf(c_745,plain,
product(a6,a1) = product(a8,a2),
inference(paramod,[status(thm)],[c_63,c_744]) ).
cnf(c_417,plain,
product(a8,a2) = product(a6,a1),
inference(copy,[status(thm)],[c_745]) ).
cnf(c_422,plain,
product(product(A,a2),product(a6,a1)) = product(product(A,a8),a2),
inference(paramod,[status(thm)],[c_417,c_4]) ).
cnf(c_425,plain,
product(product(A,product(a6,a1)),a2) = product(product(A,a2),a8),
inference(paramod,[status(thm)],[c_417,c_18]) ).
cnf(c_430,plain,
product(product(product(A,a6),a8),a2) = product(A,product(a2,a1)),
inference(paramod,[status(thm)],[c_422,c_404]) ).
cnf(c_746,plain,
product(product(product(a4,a9),a9),product(a4,a9)) = product(product(a4,a9),product(a10,a9)),
inference(paramod,[status(thm)],[c_68,c_16]) ).
cnf(c_747,plain,
product(a4,product(a4,a9)) = product(product(a4,a9),product(a10,a9)),
inference(paramod,[status(thm)],[c_2,c_746]) ).
cnf(c_748,plain,
product(a4,product(a4,a9)) = product(product(a4,a10),a9),
inference(paramod,[status(thm)],[c_4,c_747]) ).
cnf(c_749,plain,
product(a4,product(a4,a9)) = product(a5,a9),
inference(paramod,[status(thm)],[c_8,c_748]) ).
cnf(c_452,plain,
product(a4,product(a4,a9)) = a6,
inference(paramod,[status(thm)],[c_9,c_749]) ).
cnf(c_460,plain,
product(a6,product(a4,a9)) = a4,
inference(paramod,[status(thm)],[c_452,c_2]) ).
cnf(c_750,plain,
product(a1,a7) = product(a3,product(a6,a7)),
inference(paramod,[status(thm)],[c_21,c_25]) ).
cnf(c_751,plain,
product(a1,a7) = product(a3,a8),
inference(paramod,[status(thm)],[c_58,c_750]) ).
cnf(c_497,plain,
product(a1,a7) = product(a2,a3),
inference(paramod,[status(thm)],[c_66,c_751]) ).
cnf(c_752,plain,
product(product(a2,a3),a6) = product(a2,product(a7,a6)),
inference(paramod,[status(thm)],[c_497,c_22]) ).
cnf(c_753,plain,
product(a1,product(a3,a6)) = product(a2,product(a7,a6)),
inference(paramod,[status(thm)],[c_72,c_752]) ).
cnf(c_754,plain,
product(a1,product(a2,a1)) = product(a2,product(a7,a6)),
inference(paramod,[status(thm)],[c_358,c_753]) ).
cnf(c_755,plain,
a4 = product(a2,product(a7,a6)),
inference(paramod,[status(thm)],[c_133,c_754]) ).
cnf(c_756,plain,
a4 = product(a2,product(a6,a1)),
inference(paramod,[status(thm)],[c_63,c_755]) ).
cnf(c_513,plain,
product(a2,product(a6,a1)) = a4,
inference(copy,[status(thm)],[c_756]) ).
cnf(c_757,plain,
product(a4,a6) = product(a6,product(product(a4,a9),a6)),
inference(paramod,[status(thm)],[c_460,c_16]) ).
cnf(c_758,plain,
product(a2,a3) = product(a6,product(product(a4,a9),a6)),
inference(paramod,[status(thm)],[c_362,c_757]) ).
cnf(c_759,plain,
product(a2,a3) = product(a6,product(product(a4,a6),a8)),
inference(paramod,[status(thm)],[c_109,c_758]) ).
cnf(c_760,plain,
product(a2,a3) = product(a6,product(product(a2,a3),a8)),
inference(paramod,[status(thm)],[c_362,c_759]) ).
cnf(c_761,plain,
product(a2,a3) = product(a6,product(product(a2,a6),a2)),
inference(paramod,[status(thm)],[c_42,c_760]) ).
cnf(c_762,plain,
product(a2,a3) = product(a6,product(a1,a2)),
inference(paramod,[status(thm)],[c_21,c_761]) ).
cnf(c_517,plain,
product(a2,a3) = product(a6,a3),
inference(paramod,[status(thm)],[c_64,c_762]) ).
cnf(c_763,plain,
product(product(product(a4,a9),a6),product(a4,a9)) = product(product(a4,a9),a4),
inference(paramod,[status(thm)],[c_460,c_16]) ).
cnf(c_764,plain,
product(product(product(a4,a6),a8),product(a4,a9)) = product(product(a4,a9),a4),
inference(paramod,[status(thm)],[c_109,c_763]) ).
cnf(c_765,plain,
product(product(product(a2,a3),a8),product(a4,a9)) = product(product(a4,a9),a4),
inference(paramod,[status(thm)],[c_362,c_764]) ).
cnf(c_766,plain,
product(product(product(a6,a3),a8),product(a4,a9)) = product(product(a4,a9),a4),
inference(paramod,[status(thm)],[c_517,c_765]) ).
cnf(c_767,plain,
product(product(product(a6,a6),a2),product(a4,a9)) = product(product(a4,a9),a4),
inference(paramod,[status(thm)],[c_42,c_766]) ).
cnf(c_768,plain,
product(product(a6,a2),product(a4,a9)) = product(product(a4,a9),a4),
inference(paramod,[status(thm)],[c_1,c_767]) ).
cnf(c_769,plain,
product(a7,product(a4,a9)) = product(product(a4,a9),a4),
inference(paramod,[status(thm)],[c_10,c_768]) ).
cnf(c_770,plain,
product(a7,product(a4,a9)) = product(a4,product(a9,a4)),
inference(paramod,[status(thm)],[c_16,c_769]) ).
cnf(c_771,plain,
product(a7,product(a4,a9)) = product(a4,a10),
inference(paramod,[status(thm)],[c_13,c_770]) ).
cnf(c_518,plain,
product(a7,product(a4,a9)) = a5,
inference(paramod,[status(thm)],[c_8,c_771]) ).
cnf(c_772,plain,
product(product(product(A,a4),a9),a4) = product(product(product(A,a9),a6),product(a4,a9)),
inference(paramod,[status(thm)],[c_460,c_19]) ).
cnf(c_773,plain,
product(product(product(A,a10),a4),a4) = product(product(product(A,a9),a6),product(a4,a9)),
inference(paramod,[status(thm)],[c_110,c_772]) ).
cnf(c_774,plain,
product(A,a10) = product(product(product(A,a9),a6),product(a4,a9)),
inference(paramod,[status(thm)],[c_2,c_773]) ).
cnf(c_775,plain,
product(A,a10) = product(product(product(A,a6),a8),product(a4,a9)),
inference(paramod,[status(thm)],[c_109,c_774]) ).
cnf(c_521,plain,
product(product(product(A,a6),a8),product(a4,a9)) = product(A,a10),
inference(copy,[status(thm)],[c_775]) ).
cnf(c_546,plain,
product(a4,a6) = product(a6,a3),
inference(paramod,[status(thm)],[c_517,c_362]) ).
cnf(c_776,plain,
product(product(a6,a3),a3) = a2,
inference(paramod,[status(thm)],[c_517,c_2]) ).
cnf(c_777,plain,
a6 = a2,
inference(paramod,[status(thm)],[c_2,c_776]) ).
cnf(c_560,plain,
a2 = a6,
inference(copy,[status(thm)],[c_777]) ).
cnf(c_778,plain,
product(a6,product(a6,a1)) = a4,
inference(paramod,[status(thm)],[c_560,c_513]) ).
cnf(c_567,plain,
a9 = a4,
inference(paramod,[status(thm)],[c_120,c_778]) ).
cnf(c_779,plain,
product(product(product(A,a6),a8),a6) = product(A,product(a2,a1)),
inference(paramod,[status(thm)],[c_560,c_430]) ).
cnf(c_780,plain,
product(product(product(A,a6),a6),a9) = product(A,product(a2,a1)),
inference(paramod,[status(thm)],[c_45,c_779]) ).
cnf(c_781,plain,
product(A,a9) = product(A,product(a2,a1)),
inference(paramod,[status(thm)],[c_2,c_780]) ).
cnf(c_782,plain,
product(A,a4) = product(A,product(a2,a1)),
inference(paramod,[status(thm)],[c_567,c_781]) ).
cnf(c_783,plain,
product(A,a4) = product(A,product(a6,a1)),
inference(paramod,[status(thm)],[c_560,c_782]) ).
cnf(c_575,plain,
product(A,product(a6,a1)) = product(A,a4),
inference(copy,[status(thm)],[c_783]) ).
cnf(c_784,plain,
product(product(A,a4),a2) = product(product(A,a2),a8),
inference(paramod,[status(thm)],[c_575,c_425]) ).
cnf(c_785,plain,
product(product(A,a4),a6) = product(product(A,a2),a8),
inference(paramod,[status(thm)],[c_560,c_784]) ).
cnf(c_578,plain,
product(product(A,a4),a6) = product(product(A,a6),a8),
inference(paramod,[status(thm)],[c_560,c_785]) ).
cnf(c_786,plain,
product(a8,a6) = product(a6,a1),
inference(paramod,[status(thm)],[c_560,c_417]) ).
cnf(c_787,plain,
a9 = product(a6,a1),
inference(paramod,[status(thm)],[c_12,c_786]) ).
cnf(c_788,plain,
a4 = product(a6,a1),
inference(paramod,[status(thm)],[c_567,c_787]) ).
cnf(c_585,plain,
product(a6,a1) = a4,
inference(copy,[status(thm)],[c_788]) ).
cnf(c_789,plain,
product(product(product(A,a6),a6),a1) = product(A,product(a6,a1)),
inference(paramod,[status(thm)],[c_560,c_400]) ).
cnf(c_790,plain,
product(A,a1) = product(A,product(a6,a1)),
inference(paramod,[status(thm)],[c_2,c_789]) ).
cnf(c_591,plain,
product(A,a1) = product(A,a4),
inference(paramod,[status(thm)],[c_585,c_790]) ).
cnf(c_791,plain,
product(product(A,product(a6,a4)),product(a2,a1)) = product(product(A,a6),a1),
inference(paramod,[status(thm)],[c_591,c_396]) ).
cnf(c_792,plain,
product(product(A,product(a6,a4)),product(a6,a1)) = product(product(A,a6),a1),
inference(paramod,[status(thm)],[c_560,c_791]) ).
cnf(c_793,plain,
product(product(A,product(a6,a4)),product(a6,a4)) = product(product(A,a6),a1),
inference(paramod,[status(thm)],[c_591,c_792]) ).
cnf(c_794,plain,
A = product(product(A,a6),a1),
inference(paramod,[status(thm)],[c_2,c_793]) ).
cnf(c_795,plain,
A = product(product(A,a6),a4),
inference(paramod,[status(thm)],[c_591,c_794]) ).
cnf(c_595,plain,
product(product(A,a6),a4) = A,
inference(copy,[status(thm)],[c_795]) ).
cnf(c_796,plain,
product(product(product(A,a7),a6),a4) = product(A,a2),
inference(paramod,[status(thm)],[c_591,c_324]) ).
cnf(c_797,plain,
product(A,a7) = product(A,a2),
inference(paramod,[status(thm)],[c_595,c_796]) ).
cnf(c_615,plain,
product(A,a7) = product(A,a6),
inference(paramod,[status(thm)],[c_560,c_797]) ).
cnf(c_798,plain,
product(product(A,a4),product(a6,a1)) = product(product(A,a2),a3),
inference(paramod,[status(thm)],[c_560,c_315]) ).
cnf(c_799,plain,
product(product(A,a4),product(a6,a4)) = product(product(A,a2),a3),
inference(paramod,[status(thm)],[c_591,c_798]) ).
cnf(c_800,plain,
product(product(A,a6),a4) = product(product(A,a2),a3),
inference(paramod,[status(thm)],[c_4,c_799]) ).
cnf(c_801,plain,
A = product(product(A,a2),a3),
inference(paramod,[status(thm)],[c_595,c_800]) ).
cnf(c_802,plain,
A = product(product(A,a6),a3),
inference(paramod,[status(thm)],[c_560,c_801]) ).
cnf(c_621,plain,
product(product(A,a6),a3) = A,
inference(copy,[status(thm)],[c_802]) ).
cnf(c_803,plain,
product(product(product(A,a6),a3),product(a2,a1)) = product(A,a4),
inference(paramod,[status(thm)],[c_560,c_314]) ).
cnf(c_804,plain,
product(A,product(a2,a1)) = product(A,a4),
inference(paramod,[status(thm)],[c_621,c_803]) ).
cnf(c_805,plain,
product(A,product(a6,a1)) = product(A,a4),
inference(paramod,[status(thm)],[c_560,c_804]) ).
cnf(c_622,plain,
product(A,product(a6,a4)) = product(A,a4),
inference(paramod,[status(thm)],[c_591,c_805]) ).
cnf(c_806,plain,
product(a4,product(a6,a1)) = a1,
inference(paramod,[status(thm)],[c_560,c_309]) ).
cnf(c_807,plain,
product(a4,product(a6,a4)) = a1,
inference(paramod,[status(thm)],[c_591,c_806]) ).
cnf(c_808,plain,
product(a4,a4) = a1,
inference(paramod,[status(thm)],[c_622,c_807]) ).
cnf(c_809,plain,
a4 = a1,
inference(paramod,[status(thm)],[c_1,c_808]) ).
cnf(c_625,plain,
a1 = a4,
inference(copy,[status(thm)],[c_809]) ).
cnf(c_810,plain,
product(product(A,a4),a2) = product(product(A,a2),a3),
inference(paramod,[status(thm)],[c_625,c_126]) ).
cnf(c_811,plain,
product(product(A,a4),a6) = product(product(A,a2),a3),
inference(paramod,[status(thm)],[c_560,c_810]) ).
cnf(c_812,plain,
product(product(A,a6),a8) = product(product(A,a2),a3),
inference(paramod,[status(thm)],[c_578,c_811]) ).
cnf(c_813,plain,
product(product(A,a6),a8) = product(product(A,a6),a3),
inference(paramod,[status(thm)],[c_560,c_812]) ).
cnf(c_642,plain,
product(product(A,a6),a8) = A,
inference(paramod,[status(thm)],[c_621,c_813]) ).
cnf(c_814,plain,
product(product(product(A,a6),a6),a3) = product(A,a7),
inference(paramod,[status(thm)],[c_560,c_107]) ).
cnf(c_815,plain,
product(A,a3) = product(A,a7),
inference(paramod,[status(thm)],[c_2,c_814]) ).
cnf(c_646,plain,
product(A,a3) = product(A,a6),
inference(paramod,[status(thm)],[c_615,c_815]) ).
cnf(c_816,plain,
product(a4,a2) = a3,
inference(paramod,[status(thm)],[c_625,c_64]) ).
cnf(c_817,plain,
product(a4,a6) = a3,
inference(paramod,[status(thm)],[c_560,c_816]) ).
cnf(c_818,plain,
product(a6,a3) = a3,
inference(paramod,[status(thm)],[c_546,c_817]) ).
cnf(c_819,plain,
product(a6,a6) = a3,
inference(paramod,[status(thm)],[c_646,c_818]) ).
cnf(c_820,plain,
a6 = a3,
inference(paramod,[status(thm)],[c_1,c_819]) ).
cnf(c_648,plain,
a3 = a6,
inference(copy,[status(thm)],[c_820]) ).
cnf(c_821,plain,
product(a6,a2) = a1,
inference(paramod,[status(thm)],[c_648,c_57]) ).
cnf(c_822,plain,
product(a6,a6) = a1,
inference(paramod,[status(thm)],[c_560,c_821]) ).
cnf(c_823,plain,
a6 = a1,
inference(paramod,[status(thm)],[c_1,c_822]) ).
cnf(c_824,plain,
a6 = a4,
inference(paramod,[status(thm)],[c_625,c_823]) ).
cnf(c_649,plain,
a4 = a6,
inference(copy,[status(thm)],[c_824]) ).
cnf(c_825,plain,
tuple(a4,a6,a5,a2,a7,a3,a4,a9,a10,a8) != tuple(a2,a7,a6,a3,a8,a4,a5,a10,a11,a9),
inference(paramod,[status(thm)],[c_625,c_15]) ).
cnf(c_826,plain,
tuple(a6,a6,a5,a2,a7,a3,a4,a9,a10,a8) != tuple(a2,a7,a6,a3,a8,a4,a5,a10,a11,a9),
inference(paramod,[status(thm)],[c_649,c_825]) ).
cnf(c_827,plain,
tuple(a6,a6,a5,a6,a7,a3,a4,a9,a10,a8) != tuple(a2,a7,a6,a3,a8,a4,a5,a10,a11,a9),
inference(paramod,[status(thm)],[c_560,c_826]) ).
cnf(c_828,plain,
tuple(a6,a6,a5,a6,a7,a6,a4,a9,a10,a8) != tuple(a2,a7,a6,a3,a8,a4,a5,a10,a11,a9),
inference(paramod,[status(thm)],[c_648,c_827]) ).
cnf(c_829,plain,
tuple(a6,a6,a5,a6,a7,a6,a6,a9,a10,a8) != tuple(a2,a7,a6,a3,a8,a4,a5,a10,a11,a9),
inference(paramod,[status(thm)],[c_649,c_828]) ).
cnf(c_830,plain,
tuple(a6,a6,a5,a6,a7,a6,a6,a4,a10,a8) != tuple(a2,a7,a6,a3,a8,a4,a5,a10,a11,a9),
inference(paramod,[status(thm)],[c_567,c_829]) ).
cnf(c_831,plain,
tuple(a6,a6,a5,a6,a7,a6,a6,a6,a10,a8) != tuple(a2,a7,a6,a3,a8,a4,a5,a10,a11,a9),
inference(paramod,[status(thm)],[c_649,c_830]) ).
cnf(c_832,plain,
tuple(a6,a6,a5,a6,a7,a6,a6,a6,a10,a8) != tuple(a6,a7,a6,a3,a8,a4,a5,a10,a11,a9),
inference(paramod,[status(thm)],[c_560,c_831]) ).
cnf(c_833,plain,
tuple(a6,a6,a5,a6,a7,a6,a6,a6,a10,a8) != tuple(a6,a7,a6,a6,a8,a4,a5,a10,a11,a9),
inference(paramod,[status(thm)],[c_648,c_832]) ).
cnf(c_834,plain,
tuple(a6,a6,a5,a6,a7,a6,a6,a6,a10,a8) != tuple(a6,a7,a6,a6,a8,a6,a5,a10,a11,a9),
inference(paramod,[status(thm)],[c_649,c_833]) ).
cnf(c_835,plain,
tuple(a6,a6,a5,a6,a7,a6,a6,a6,a10,a8) != tuple(a6,a7,a6,a6,a8,a6,a5,a10,a11,a4),
inference(paramod,[status(thm)],[c_567,c_834]) ).
cnf(c_836,plain,
tuple(a6,a6,a5,a6,a7,a6,a6,a6,a10,a8) != tuple(a6,a7,a6,a6,a8,a6,a5,a10,a11,a6),
inference(paramod,[status(thm)],[c_649,c_835]) ).
cnf(c_651,plain,
tuple(a6,a7,a6,a6,a8,a6,a5,a10,a11,a6) != tuple(a6,a6,a5,a6,a7,a6,a6,a6,a10,a8),
inference(copy,[status(thm)],[c_836]) ).
cnf(c_837,plain,
product(a6,a6) = a7,
inference(paramod,[status(thm)],[c_560,c_10]) ).
cnf(c_838,plain,
a6 = a7,
inference(paramod,[status(thm)],[c_1,c_837]) ).
cnf(c_652,plain,
a7 = a6,
inference(copy,[status(thm)],[c_838]) ).
cnf(c_839,plain,
product(A,product(a4,a9)) = product(A,a10),
inference(paramod,[status(thm)],[c_642,c_521]) ).
cnf(c_840,plain,
product(A,product(a6,a9)) = product(A,a10),
inference(paramod,[status(thm)],[c_649,c_839]) ).
cnf(c_841,plain,
product(A,product(a6,a4)) = product(A,a10),
inference(paramod,[status(thm)],[c_567,c_840]) ).
cnf(c_842,plain,
product(A,product(a6,a6)) = product(A,a10),
inference(paramod,[status(thm)],[c_649,c_841]) ).
cnf(c_843,plain,
product(A,a6) = product(A,a10),
inference(paramod,[status(thm)],[c_1,c_842]) ).
cnf(c_654,plain,
product(A,a10) = product(A,a6),
inference(copy,[status(thm)],[c_843]) ).
cnf(c_844,plain,
product(a6,product(a4,a9)) = a5,
inference(paramod,[status(thm)],[c_652,c_518]) ).
cnf(c_845,plain,
product(a6,product(a6,a9)) = a5,
inference(paramod,[status(thm)],[c_649,c_844]) ).
cnf(c_846,plain,
product(a6,product(a6,a4)) = a5,
inference(paramod,[status(thm)],[c_567,c_845]) ).
cnf(c_847,plain,
product(a6,product(a6,a6)) = a5,
inference(paramod,[status(thm)],[c_649,c_846]) ).
cnf(c_848,plain,
product(a6,a6) = a5,
inference(paramod,[status(thm)],[c_1,c_847]) ).
cnf(c_849,plain,
a6 = a5,
inference(paramod,[status(thm)],[c_1,c_848]) ).
cnf(c_656,plain,
a5 = a6,
inference(copy,[status(thm)],[c_849]) ).
cnf(c_850,plain,
product(a4,a10) = a11,
inference(paramod,[status(thm)],[c_567,c_61]) ).
cnf(c_851,plain,
product(a6,a10) = a11,
inference(paramod,[status(thm)],[c_649,c_850]) ).
cnf(c_852,plain,
product(a6,a6) = a11,
inference(paramod,[status(thm)],[c_654,c_851]) ).
cnf(c_853,plain,
a6 = a11,
inference(paramod,[status(thm)],[c_1,c_852]) ).
cnf(c_678,plain,
a11 = a6,
inference(copy,[status(thm)],[c_853]) ).
cnf(c_854,plain,
product(a4,a6) = a8,
inference(paramod,[status(thm)],[c_567,c_43]) ).
cnf(c_855,plain,
product(a6,a6) = a8,
inference(paramod,[status(thm)],[c_649,c_854]) ).
cnf(c_856,plain,
a6 = a8,
inference(paramod,[status(thm)],[c_1,c_855]) ).
cnf(c_681,plain,
a8 = a6,
inference(copy,[status(thm)],[c_856]) ).
cnf(c_857,plain,
product(a4,a4) = a10,
inference(paramod,[status(thm)],[c_567,c_13]) ).
cnf(c_858,plain,
product(a6,a4) = a10,
inference(paramod,[status(thm)],[c_649,c_857]) ).
cnf(c_859,plain,
product(a6,a6) = a10,
inference(paramod,[status(thm)],[c_649,c_858]) ).
cnf(c_860,plain,
a6 = a10,
inference(paramod,[status(thm)],[c_1,c_859]) ).
cnf(c_682,plain,
a10 = a6,
inference(copy,[status(thm)],[c_860]) ).
cnf(c_861,plain,
tuple(a6,a6,a6,a6,a8,a6,a5,a10,a11,a6) != tuple(a6,a6,a5,a6,a7,a6,a6,a6,a10,a8),
inference(paramod,[status(thm)],[c_652,c_651]) ).
cnf(c_862,plain,
tuple(a6,a6,a6,a6,a6,a6,a5,a10,a11,a6) != tuple(a6,a6,a5,a6,a7,a6,a6,a6,a10,a8),
inference(paramod,[status(thm)],[c_681,c_861]) ).
cnf(c_863,plain,
tuple(a6,a6,a6,a6,a6,a6,a6,a10,a11,a6) != tuple(a6,a6,a5,a6,a7,a6,a6,a6,a10,a8),
inference(paramod,[status(thm)],[c_656,c_862]) ).
cnf(c_864,plain,
tuple(a6,a6,a6,a6,a6,a6,a6,a6,a11,a6) != tuple(a6,a6,a5,a6,a7,a6,a6,a6,a10,a8),
inference(paramod,[status(thm)],[c_682,c_863]) ).
cnf(c_865,plain,
tuple(a6,a6,a6,a6,a6,a6,a6,a6,a6,a6) != tuple(a6,a6,a5,a6,a7,a6,a6,a6,a10,a8),
inference(paramod,[status(thm)],[c_678,c_864]) ).
cnf(c_866,plain,
tuple(a6,a6,a6,a6,a6,a6,a6,a6,a6,a6) != tuple(a6,a6,a6,a6,a7,a6,a6,a6,a10,a8),
inference(paramod,[status(thm)],[c_656,c_865]) ).
cnf(c_867,plain,
tuple(a6,a6,a6,a6,a6,a6,a6,a6,a6,a6) != tuple(a6,a6,a6,a6,a6,a6,a6,a6,a10,a8),
inference(paramod,[status(thm)],[c_652,c_866]) ).
cnf(c_868,plain,
tuple(a6,a6,a6,a6,a6,a6,a6,a6,a6,a6) != tuple(a6,a6,a6,a6,a6,a6,a6,a6,a6,a8),
inference(paramod,[status(thm)],[c_682,c_867]) ).
cnf(c_869,plain,
tuple(a6,a6,a6,a6,a6,a6,a6,a6,a6,a6) != tuple(a6,a6,a6,a6,a6,a6,a6,a6,a6,a6),
inference(paramod,[status(thm)],[c_681,c_868]) ).
cnf(c_685,plain,
$false,
inference(copy,[status(thm)],[c_869]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP051-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.09/0.36 % Computer : n001.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 20:55:58 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 2650938 was started by sandbox2 on n001,
% 0.09/0.37 % Sat Sep 26 20:55:58 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.37
% 0.09/0.37 % From the command line: assign(max_seconds, 300).
% 0.67/0.52
% 0.67/0.52 % SZS status Unsatisfiable for theBenchmark
% 0.67/0.52
% 0.67/0.52 % Proof 1 at 0.10 (+ 0.03) seconds.
% 0.67/0.52 % Length of proof is 101.
% 0.67/0.52 % Level of proof is 19.
% 0.67/0.52 % Maximum clause weight is 76.000.
% 0.67/0.52 % Given clauses 68.
% 0.67/0.52
% 0.67/0.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------