LisaST---0.9.UNS-CRf.s

%------------------------------------------------------------------------------
% File     : LisaST---0.9
% Problem  : GRP129-3.004 : TPTP v9.3.1. Released v1.2.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : casc-portfolio.sh -t 300 /export/starexec/sandbox/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 07:23:00 AM UTC 2026

% Result   : Unsatisfiable 49.51s 8.01s
% Output   : CNFRefutation 49.51s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)

% Comments : 
%------------------------------------------------------------------------------
cnf(e_0_then_e_1,axiom,
    next('e$u0','e$u1') ).

cnf(e_2_then_e_3,axiom,
    next('e$u2','e$u3') ).

cnf(e_3_then_e_4,axiom,
    next('e$u3','e$u4') ).

cnf(e_1_greater_e_0,axiom,
    greater('e$u1','e$u0') ).

cnf(e_2_greater_e_0,axiom,
    greater('e$u2','e$u0') ).

cnf(e_3_greater_e_0,axiom,
    greater('e$u3','e$u0') ).

cnf(e_2_greater_e_1,axiom,
    greater('e$u2','e$u1') ).

cnf(e_3_greater_e_1,axiom,
    greater('e$u3','e$u1') ).

cnf(e_3_greater_e_2,axiom,
    greater('e$u3','e$u2') ).

cnf(e_4_greater_e_2,axiom,
    greater('e$u4','e$u2') ).

cnf(cycle2,axiom,
    ( cycle(X0,'e$u3')
    | cycle(X0,'e$u2')
    | cycle(X0,'e$u1')
    | cycle(X0,'e$u0')
    | ~ 'group$uelement'(X0) ) ).

cnf(cycle3,axiom,
    cycle('e$u4','e$u0') ).

cnf(cycle4,axiom,
    ( equalish(X1,X4)
    | ~ next(X3,X4)
    | ~ greater(X1,'e$u0')
    | ~ next(X0,X2)
    | ~ cycle(X2,X3)
    | ~ cycle(X0,X1) ) ).

cnf(cycle5,axiom,
    ( ~ greater(X1,X4)
    | ~ greater(X2,X0)
    | ~ next(X2,X3)
    | ~ cycle(X3,X4)
    | ~ cycle(X2,'e$u0')
    | ~ cycle(X0,X1) ) ).

cnf(cycle6,axiom,
    ( ~ greater(X1,X0)
    | ~ product(X0,'e$u1',X1)
    | ~ cycle(X0,'e$u0') ) ).

cnf(cycle7,axiom,
    ( equalish(X2,X3)
    | ~ next(X0,X3)
    | ~ greater(X1,'e$u0')
    | ~ product(X0,'e$u1',X2)
    | ~ cycle(X0,X1) ) ).

cnf(element_1,axiom,
    'group$uelement'('e$u1') ).

cnf(element_2,axiom,
    'group$uelement'('e$u2') ).

cnf(element_3,axiom,
    'group$uelement'('e$u3') ).

cnf(element_4,axiom,
    'group$uelement'('e$u4') ).

cnf(e_1_is_not_e_2,axiom,
    ~ equalish('e$u1','e$u2') ).

cnf(e_1_is_not_e_3,axiom,
    ~ equalish('e$u1','e$u3') ).

cnf(e_1_is_not_e_4,axiom,
    ~ equalish('e$u1','e$u4') ).

cnf(e_2_is_not_e_1,axiom,
    ~ equalish('e$u2','e$u1') ).

cnf(e_2_is_not_e_3,axiom,
    ~ equalish('e$u2','e$u3') ).

cnf(e_2_is_not_e_4,axiom,
    ~ equalish('e$u2','e$u4') ).

cnf(e_3_is_not_e_1,axiom,
    ~ equalish('e$u3','e$u1') ).

cnf(e_3_is_not_e_2,axiom,
    ~ equalish('e$u3','e$u2') ).

cnf(e_3_is_not_e_4,axiom,
    ~ equalish('e$u3','e$u4') ).

cnf(e_4_is_not_e_1,axiom,
    ~ equalish('e$u4','e$u1') ).

cnf(e_4_is_not_e_3,axiom,
    ~ equalish('e$u4','e$u3') ).

cnf(product_total_function1,axiom,
    ( product(X0,X1,'e$u4')
    | product(X0,X1,'e$u3')
    | product(X0,X1,'e$u2')
    | product(X0,X1,'e$u1')
    | ~ 'group$uelement'(X1)
    | ~ 'group$uelement'(X0) ) ).

cnf(product_total_function2,axiom,
    ( equalish(X2,X3)
    | ~ product(X0,X1,X3)
    | ~ product(X0,X1,X2) ) ).

cnf(product_right_cancellation,axiom,
    ( equalish(X1,X3)
    | ~ product(X0,X3,X2)
    | ~ product(X0,X1,X2) ) ).

cnf(product_left_cancellation,axiom,
    ( equalish(X0,X3)
    | ~ product(X3,X1,X2)
    | ~ product(X0,X1,X2) ) ).

cnf(qg3,negated_conjecture,
    ( product(X2,X0,X3)
    | ~ product(X1,X2,X3)
    | ~ product(X0,X1,X2) ) ).

cnf(c0,plain,
    next('e$u0','e$u1'),
    inference(clausification,[status(esa)],[e_0_then_e_1]) ).

cnf(c2,plain,
    next('e$u2','e$u3'),
    inference(clausification,[status(esa)],[e_2_then_e_3]) ).

cnf(c3,plain,
    next('e$u3','e$u4'),
    inference(clausification,[status(esa)],[e_3_then_e_4]) ).

cnf(c4,plain,
    greater('e$u1','e$u0'),
    inference(clausification,[status(esa)],[e_1_greater_e_0]) ).

cnf(c5,plain,
    greater('e$u2','e$u0'),
    inference(clausification,[status(esa)],[e_2_greater_e_0]) ).

cnf(c6,plain,
    greater('e$u3','e$u0'),
    inference(clausification,[status(esa)],[e_3_greater_e_0]) ).

cnf(c8,plain,
    greater('e$u2','e$u1'),
    inference(clausification,[status(esa)],[e_2_greater_e_1]) ).

cnf(c9,plain,
    greater('e$u3','e$u1'),
    inference(clausification,[status(esa)],[e_3_greater_e_1]) ).

cnf(c11,plain,
    greater('e$u3','e$u2'),
    inference(clausification,[status(esa)],[e_3_greater_e_2]) ).

cnf(c12,plain,
    greater('e$u4','e$u2'),
    inference(clausification,[status(esa)],[e_4_greater_e_2]) ).

cnf(c15,plain,
    ( ~ 'group$uelement'(X0)
    | cycle(X0,'e$u2')
    | cycle(X0,'e$u0')
    | cycle(X0,'e$u3')
    | cycle(X0,'e$u1') ),
    inference(clausification,[status(esa)],[cycle2]) ).

cnf(c16,plain,
    cycle('e$u4','e$u0'),
    inference(clausification,[status(esa)],[cycle3]) ).

cnf(c17,plain,
    ( ~ next(X1,X3)
    | ~ next(X4,X0)
    | ~ cycle(X4,X2)
    | ~ greater(X2,'e$u0')
    | equalish(X2,X3)
    | ~ cycle(X0,X1) ),
    inference(clausification,[status(esa)],[cycle4]) ).

cnf(c18,plain,
    ( ~ greater(X2,X3)
    | ~ next(X2,X4)
    | ~ cycle(X4,X1)
    | ~ cycle(X3,X0)
    | ~ cycle(X2,'e$u0')
    | ~ greater(X0,X1) ),
    inference(clausification,[status(esa)],[cycle5]) ).

cnf(c19,plain,
    ( ~ greater(X1,X0)
    | ~ cycle(X0,'e$u0')
    | ~ product(X0,'e$u1',X1) ),
    inference(clausification,[status(esa)],[cycle6]) ).

cnf(c20,plain,
    ( ~ greater(X2,'e$u0')
    | ~ product(X0,'e$u1',X3)
    | equalish(X3,X1)
    | ~ cycle(X0,X2)
    | ~ next(X0,X1) ),
    inference(clausification,[status(esa)],[cycle7]) ).

cnf(c21,plain,
    'group$uelement'('e$u1'),
    inference(clausification,[status(esa)],[element_1]) ).

cnf(c22,plain,
    'group$uelement'('e$u2'),
    inference(clausification,[status(esa)],[element_2]) ).

cnf(c23,plain,
    'group$uelement'('e$u3'),
    inference(clausification,[status(esa)],[element_3]) ).

cnf(c24,plain,
    'group$uelement'('e$u4'),
    inference(clausification,[status(esa)],[element_4]) ).

cnf(c25,plain,
    ~ equalish('e$u1','e$u2'),
    inference(clausification,[status(esa)],[e_1_is_not_e_2]) ).

cnf(c26,plain,
    ~ equalish('e$u1','e$u3'),
    inference(clausification,[status(esa)],[e_1_is_not_e_3]) ).

cnf(c27,plain,
    ~ equalish('e$u1','e$u4'),
    inference(clausification,[status(esa)],[e_1_is_not_e_4]) ).

cnf(c28,plain,
    ~ equalish('e$u2','e$u1'),
    inference(clausification,[status(esa)],[e_2_is_not_e_1]) ).

cnf(c29,plain,
    ~ equalish('e$u2','e$u3'),
    inference(clausification,[status(esa)],[e_2_is_not_e_3]) ).

cnf(c30,plain,
    ~ equalish('e$u2','e$u4'),
    inference(clausification,[status(esa)],[e_2_is_not_e_4]) ).

cnf(c31,plain,
    ~ equalish('e$u3','e$u1'),
    inference(clausification,[status(esa)],[e_3_is_not_e_1]) ).

cnf(c32,plain,
    ~ equalish('e$u3','e$u2'),
    inference(clausification,[status(esa)],[e_3_is_not_e_2]) ).

cnf(c33,plain,
    ~ equalish('e$u3','e$u4'),
    inference(clausification,[status(esa)],[e_3_is_not_e_4]) ).

cnf(c34,plain,
    ~ equalish('e$u4','e$u1'),
    inference(clausification,[status(esa)],[e_4_is_not_e_1]) ).

cnf(c36,plain,
    ~ equalish('e$u4','e$u3'),
    inference(clausification,[status(esa)],[e_4_is_not_e_3]) ).

cnf(c37,plain,
    ( product(X0,X1,'e$u3')
    | ~ 'group$uelement'(X1)
    | ~ 'group$uelement'(X0)
    | product(X0,X1,'e$u4')
    | product(X0,X1,'e$u1')
    | product(X0,X1,'e$u2') ),
    inference(clausification,[status(esa)],[product_total_function1]) ).

cnf(c38,plain,
    ( equalish(X3,X2)
    | ~ product(X0,X1,X3)
    | ~ product(X0,X1,X2) ),
    inference(clausification,[status(esa)],[product_total_function2]) ).

cnf(c39,plain,
    ( equalish(X3,X1)
    | ~ product(X0,X3,X2)
    | ~ product(X0,X1,X2) ),
    inference(clausification,[status(esa)],[product_right_cancellation]) ).

cnf(c40,plain,
    ( equalish(X3,X0)
    | ~ product(X3,X1,X2)
    | ~ product(X0,X1,X2) ),
    inference(clausification,[status(esa)],[product_left_cancellation]) ).

cnf(c41,plain,
    ( product(X1,X3,X2)
    | ~ product(X3,X0,X1)
    | ~ product(X0,X1,X2) ),
    inference(clausification,[status(esa)],[qg3]) ).

cnf(d0,plain,
    ( product('e$u3',X0,'e$u4')
    | product('e$u3',X0,'e$u3')
    | product('e$u3',X0,'e$u2')
    | product('e$u3',X0,'e$u1')
    | ~ 'group$uelement'(X0) ),
    inference(resolution,[status(thm)],[c37,c23]) ).

cnf(d1,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u3','e$u1','e$u1') ),
    inference(resolution,[status(thm)],[d0,c21]) ).

cnf(d2,plain,
    ( ~ product('e$u3','e$u1',X1)
    | equalish(X1,'e$u4')
    | ~ cycle('e$u3',X0)
    | ~ greater(X0,'e$u0') ),
    inference(resolution,[status(thm)],[c20,c3]) ).

cnf(d3,plain,
    ( ~ product('e$u3','e$u1',X0)
    | equalish(X0,'e$u4')
    | ~ cycle('e$u3','e$u1') ),
    inference(resolution,[status(thm)],[d2,c4]) ).

cnf(d4,plain,
    ( cycle('e$u3','e$u3')
    | cycle('e$u3','e$u2')
    | cycle('e$u3','e$u1')
    | cycle('e$u3','e$u0') ),
    inference(resolution,[status(thm)],[c15,c23]) ).

cnf(d5,plain,
    ( equalish(X2,'e$u1')
    | ~ cycle(X0,X2)
    | ~ cycle(X1,'e$u0')
    | ~ greater(X2,'e$u0')
    | ~ next(X0,X1) ),
    inference(resolution,[status(thm)],[c17,c0]) ).

cnf(d6,plain,
    ( equalish(X0,'e$u1')
    | ~ cycle('e$u3',X0)
    | ~ cycle('e$u4','e$u0')
    | ~ greater(X0,'e$u0') ),
    inference(resolution,[status(thm)],[d5,c3]) ).

cnf(d7,plain,
    ( equalish(X0,'e$u1')
    | ~ cycle('e$u3',X0)
    | ~ greater(X0,'e$u0') ),
    inference(resolution,[status(thm)],[c16,d6]) ).

cnf(d8,plain,
    ( equalish('e$u2','e$u1')
    | ~ cycle('e$u3','e$u2') ),
    inference(resolution,[status(thm)],[d7,c5]) ).

cnf(d9,plain,
    ~ cycle('e$u3','e$u2'),
    inference(resolution,[status(thm)],[c28,d8]) ).

cnf(d10,plain,
    ( cycle('e$u3','e$u3')
    | cycle('e$u3','e$u1')
    | cycle('e$u3','e$u0') ),
    inference(resolution,[status(thm)],[d9,d4]) ).

cnf(d11,plain,
    ( equalish('e$u3','e$u1')
    | ~ cycle('e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d7,c6]) ).

cnf(d12,plain,
    ~ cycle('e$u3','e$u3'),
    inference(resolution,[status(thm)],[c31,d11]) ).

cnf(d13,plain,
    ( cycle('e$u3','e$u1')
    | cycle('e$u3','e$u0') ),
    inference(resolution,[status(thm)],[d12,d10]) ).

cnf(d14,plain,
    ( ~ cycle('e$u3','e$u0')
    | ~ cycle(X2,X0)
    | ~ cycle('e$u4',X1)
    | ~ greater('e$u3',X2)
    | ~ greater(X0,X1) ),
    inference(resolution,[status(thm)],[c18,c3]) ).

cnf(d15,plain,
    ( ~ cycle('e$u4','e$u0')
    | ~ cycle('e$u3','e$u0')
    | ~ cycle(X0,'e$u3')
    | ~ greater('e$u3',X0) ),
    inference(resolution,[status(thm)],[d14,c6]) ).

cnf(d16,plain,
    ( ~ cycle('e$u3','e$u0')
    | ~ cycle(X0,'e$u3')
    | ~ greater('e$u3',X0) ),
    inference(resolution,[status(thm)],[c16,d15]) ).

cnf(d17,plain,
    ( ~ cycle('e$u3','e$u0')
    | ~ cycle('e$u1','e$u3') ),
    inference(resolution,[status(thm)],[d16,c9]) ).

cnf(d18,plain,
    ( ~ cycle('e$u4','e$u0')
    | ~ cycle('e$u3','e$u0')
    | ~ cycle(X0,'e$u2')
    | ~ greater('e$u3',X0) ),
    inference(resolution,[status(thm)],[d14,c5]) ).

cnf(d19,plain,
    ( ~ cycle('e$u3','e$u0')
    | ~ cycle(X0,'e$u2')
    | ~ greater('e$u3',X0) ),
    inference(resolution,[status(thm)],[c16,d18]) ).

cnf(d20,plain,
    ( ~ cycle('e$u3','e$u0')
    | ~ cycle('e$u1','e$u2') ),
    inference(resolution,[status(thm)],[d19,c9]) ).

cnf(d21,plain,
    ( ~ cycle('e$u4','e$u0')
    | ~ cycle('e$u3','e$u0')
    | ~ cycle(X0,'e$u1')
    | ~ greater('e$u3',X0) ),
    inference(resolution,[status(thm)],[d14,c4]) ).

cnf(d22,plain,
    ( ~ cycle('e$u3','e$u0')
    | ~ cycle(X0,'e$u1')
    | ~ greater('e$u3',X0) ),
    inference(resolution,[status(thm)],[c16,d21]) ).

cnf(d23,plain,
    ( ~ cycle('e$u3','e$u0')
    | ~ cycle('e$u1','e$u1') ),
    inference(resolution,[status(thm)],[d22,c9]) ).

cnf(d24,plain,
    ( cycle('e$u1','e$u3')
    | cycle('e$u1','e$u2')
    | cycle('e$u1','e$u1')
    | cycle('e$u1','e$u0') ),
    inference(resolution,[status(thm)],[c15,c21]) ).

cnf(d25,plain,
    ( ~ product('e$u1','e$u1','e$u2')
    | ~ cycle('e$u1','e$u0') ),
    inference(resolution,[status(thm)],[c19,c8]) ).

cnf(d26,plain,
    ( cycle('e$u1','e$u3')
    | cycle('e$u1','e$u2')
    | cycle('e$u1','e$u1')
    | ~ product('e$u1','e$u1','e$u2') ),
    inference(resolution,[status(thm)],[d25,d24]) ).

cnf(d27,plain,
    ( product('e$u1',X0,'e$u4')
    | product('e$u1',X0,'e$u3')
    | product('e$u1',X0,'e$u2')
    | product('e$u1',X0,'e$u1')
    | ~ 'group$uelement'(X0) ),
    inference(resolution,[status(thm)],[c37,c21]) ).

cnf(d28,plain,
    ( product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3')
    | product('e$u1','e$u1','e$u2')
    | product('e$u1','e$u1','e$u1') ),
    inference(resolution,[status(thm)],[d27,c21]) ).

cnf(d29,plain,
    ( ~ product(X0,'e$u1','e$u1')
    | equalish(X0,'e$u1')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3')
    | product('e$u1','e$u1','e$u2') ),
    inference(resolution,[status(thm)],[d28,c40]) ).

cnf(d30,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3')
    | product('e$u1','e$u1','e$u2')
    | equalish('e$u3','e$u1') ),
    inference(resolution,[status(thm)],[d29,d1]) ).

cnf(d31,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3')
    | product('e$u1','e$u1','e$u2') ),
    inference(resolution,[status(thm)],[c31,d30]) ).

cnf(d32,plain,
    ( cycle('e$u1','e$u3')
    | cycle('e$u1','e$u2')
    | cycle('e$u1','e$u1')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[d31,d26]) ).

cnf(d33,plain,
    ( ~ cycle('e$u3','e$u0')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3')
    | cycle('e$u1','e$u3')
    | cycle('e$u1','e$u2') ),
    inference(resolution,[status(thm)],[d32,d23]) ).

cnf(d34,plain,
    ( cycle('e$u3','e$u1')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3')
    | cycle('e$u1','e$u3')
    | cycle('e$u1','e$u2') ),
    inference(resolution,[status(thm)],[d33,d13]) ).

cnf(d35,plain,
    ( ~ cycle('e$u3','e$u0')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3')
    | cycle('e$u3','e$u1')
    | cycle('e$u1','e$u3') ),
    inference(resolution,[status(thm)],[d34,d20]) ).

cnf(d36,plain,
    ( cycle('e$u3','e$u1')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3')
    | cycle('e$u3','e$u1')
    | cycle('e$u1','e$u3') ),
    inference(resolution,[status(thm)],[d35,d13]) ).

cnf(d37,plain,
    ( ~ cycle('e$u3','e$u0')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3')
    | cycle('e$u3','e$u1') ),
    inference(resolution,[status(thm)],[d36,d17]) ).

cnf(d38,plain,
    ( cycle('e$u3','e$u1')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3')
    | cycle('e$u3','e$u1') ),
    inference(resolution,[status(thm)],[d37,d13]) ).

cnf(d39,plain,
    ( ~ product('e$u3','e$u1',X0)
    | equalish(X0,'e$u4')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[d38,d3]) ).

cnf(d40,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3')
    | equalish('e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d39,d1]) ).

cnf(d41,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[c27,d40]) ).

cnf(d42,plain,
    ( ~ product(X0,'e$u1','e$u1')
    | product('e$u1',X0,'e$u3')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d41,c41]) ).

cnf(d43,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d42,d1]) ).

cnf(d44,plain,
    ( ~ product('e$u1',X0,'e$u4')
    | equalish(X0,'e$u1')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d43,c39]) ).

cnf(d45,plain,
    ( ~ product('e$u1',X0,'e$u3')
    | equalish(X0,'e$u1')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d41,c39]) ).

cnf(d46,plain,
    ( ~ product(X0,'e$u1','e$u1')
    | product('e$u1',X0,'e$u4')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d43,c41]) ).

cnf(d47,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u3','e$u3')
    | product('e$u1','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d46,d1]) ).

cnf(d48,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4')
    | equalish('e$u3','e$u1')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d47,d45]) ).

cnf(d49,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u3','e$u4')
    | product('e$u1','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[c31,d48]) ).

cnf(d50,plain,
    ( ~ product(X0,'e$u1','e$u1')
    | product('e$u1',X0,'e$u4')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d49,c41]) ).

cnf(d51,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u3','e$u4')
    | product('e$u1','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d50,d1]) ).

cnf(d52,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u3','e$u3')
    | equalish('e$u3','e$u1')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2') ),
    inference(resolution,[status(thm)],[d51,d44]) ).

cnf(d53,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u1','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[c31,d52]) ).

cnf(d54,plain,
    ( ~ product('e$u1','e$u3',X0)
    | equalish(X0,'e$u4')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2') ),
    inference(resolution,[status(thm)],[d51,c38]) ).

cnf(d55,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2')
    | equalish('e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d54,d53]) ).

cnf(d56,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u2') ),
    inference(resolution,[status(thm)],[c33,d55]) ).

cnf(d57,plain,
    ( equalish(X0,'e$u1')
    | ~ cycle('e$u2',X0)
    | ~ cycle('e$u3','e$u0')
    | ~ greater(X0,'e$u0') ),
    inference(resolution,[status(thm)],[d5,c2]) ).

cnf(d58,plain,
    ( equalish('e$u3','e$u1')
    | ~ cycle('e$u3','e$u0')
    | ~ cycle('e$u2','e$u3') ),
    inference(resolution,[status(thm)],[d57,c6]) ).

cnf(d59,plain,
    ( ~ cycle('e$u3','e$u0')
    | ~ cycle('e$u2','e$u3') ),
    inference(resolution,[status(thm)],[c31,d58]) ).

cnf(d60,plain,
    ( equalish('e$u2','e$u1')
    | ~ cycle('e$u3','e$u0')
    | ~ cycle('e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d57,c5]) ).

cnf(d61,plain,
    ( ~ cycle('e$u3','e$u0')
    | ~ cycle('e$u2','e$u2') ),
    inference(resolution,[status(thm)],[c28,d60]) ).

cnf(d62,plain,
    ( ~ cycle('e$u3','e$u0')
    | ~ cycle('e$u2','e$u1') ),
    inference(resolution,[status(thm)],[d22,c11]) ).

cnf(d63,plain,
    ( ~ product('e$u2','e$u1','e$u4')
    | ~ cycle('e$u2','e$u0') ),
    inference(resolution,[status(thm)],[c19,c12]) ).

cnf(d64,plain,
    ( cycle('e$u2','e$u3')
    | cycle('e$u2','e$u2')
    | cycle('e$u2','e$u1')
    | cycle('e$u2','e$u0') ),
    inference(resolution,[status(thm)],[c15,c22]) ).

cnf(d65,plain,
    ( ~ product('e$u2','e$u1','e$u4')
    | cycle('e$u2','e$u3')
    | cycle('e$u2','e$u2')
    | cycle('e$u2','e$u1') ),
    inference(resolution,[status(thm)],[d64,d63]) ).

cnf(d66,plain,
    ( ~ product('e$u2','e$u1','e$u3')
    | ~ cycle('e$u2','e$u0') ),
    inference(resolution,[status(thm)],[c19,c11]) ).

cnf(d67,plain,
    ( cycle('e$u2','e$u3')
    | cycle('e$u2','e$u2')
    | cycle('e$u2','e$u1')
    | ~ product('e$u2','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[d66,d64]) ).

cnf(d68,plain,
    ( ~ product(X0,'e$u1','e$u2')
    | equalish(X0,'e$u3')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[d56,c40]) ).

cnf(d69,plain,
    ( product('e$u2',X0,'e$u4')
    | product('e$u2',X0,'e$u3')
    | product('e$u2',X0,'e$u2')
    | product('e$u2',X0,'e$u1')
    | ~ 'group$uelement'(X0) ),
    inference(resolution,[status(thm)],[c37,c22]) ).

cnf(d70,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u2','e$u1','e$u1') ),
    inference(resolution,[status(thm)],[d69,c21]) ).

cnf(d71,plain,
    ( ~ product(X0,'e$u1','e$u1')
    | equalish(X0,'e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2') ),
    inference(resolution,[status(thm)],[d70,c40]) ).

cnf(d72,plain,
    ( product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3')
    | product('e$u1','e$u1','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | equalish('e$u1','e$u2') ),
    inference(resolution,[status(thm)],[d71,d28]) ).

cnf(d73,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3')
    | product('e$u1','e$u1','e$u2') ),
    inference(resolution,[status(thm)],[c25,d72]) ).

cnf(d74,plain,
    ( product('e$u1','e$u2','e$u4')
    | product('e$u1','e$u2','e$u3')
    | product('e$u1','e$u2','e$u2')
    | product('e$u1','e$u2','e$u1') ),
    inference(resolution,[status(thm)],[d27,c22]) ).

cnf(d75,plain,
    ( ~ product('e$u1',X0,'e$u1')
    | equalish(X0,'e$u2')
    | product('e$u1','e$u2','e$u4')
    | product('e$u1','e$u2','e$u3')
    | product('e$u1','e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d74,c39]) ).

cnf(d76,plain,
    ( ~ product(X0,'e$u2','e$u1')
    | product('e$u1',X0,'e$u1')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2') ),
    inference(resolution,[status(thm)],[d70,c41]) ).

cnf(d77,plain,
    ( product('e$u1','e$u2','e$u4')
    | product('e$u1','e$u2','e$u3')
    | product('e$u1','e$u2','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u1','e$u1') ),
    inference(resolution,[status(thm)],[d76,d74]) ).

cnf(d78,plain,
    ( product('e$u1','e$u2','e$u4')
    | product('e$u1','e$u2','e$u3')
    | product('e$u1','e$u2','e$u2')
    | equalish('e$u1','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u4')
    | product('e$u1','e$u2','e$u3')
    | product('e$u1','e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d77,d75]) ).

cnf(d79,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u4')
    | product('e$u1','e$u2','e$u3')
    | product('e$u1','e$u2','e$u2') ),
    inference(resolution,[status(thm)],[c25,d78]) ).

cnf(d80,plain,
    ( ~ product(X0,'e$u1','e$u2')
    | product('e$u2',X0,'e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u4')
    | product('e$u1','e$u2','e$u3') ),
    inference(resolution,[status(thm)],[d79,c41]) ).

cnf(d81,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u4')
    | product('e$u1','e$u2','e$u3') ),
    inference(resolution,[status(thm)],[d80,d73]) ).

cnf(d82,plain,
    ( ~ product(X0,'e$u1','e$u1')
    | product('e$u1',X0,'e$u3')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u4')
    | product('e$u1','e$u2','e$u3')
    | product('e$u1','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d81,c41]) ).

cnf(d83,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u4')
    | product('e$u1','e$u2','e$u3')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u2','e$u3') ),
    inference(resolution,[status(thm)],[d82,d70]) ).

cnf(d84,plain,
    ( ~ product(X0,'e$u1','e$u1')
    | product('e$u1',X0,'e$u4')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u4')
    | product('e$u1','e$u2','e$u3') ),
    inference(resolution,[status(thm)],[d83,c41]) ).

cnf(d85,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u4')
    | product('e$u1','e$u2','e$u3')
    | product('e$u1','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d84,d70]) ).

cnf(d86,plain,
    ( ~ product('e$u1',X0,'e$u3')
    | equalish(X0,'e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d85,c39]) ).

cnf(d87,plain,
    ( ~ product(X0,'e$u1','e$u2')
    | product('e$u2',X0,'e$u3')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d85,c41]) ).

cnf(d88,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u2','e$u1','e$u3')
    | product('e$u1','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d87,d73]) ).

cnf(d89,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u4')
    | equalish('e$u1','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u4')
    | product('e$u1','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d88,d86]) ).

cnf(d90,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u4')
    | product('e$u1','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[c25,d89]) ).

cnf(d91,plain,
    ( ~ product(X0,'e$u1','e$u1')
    | product('e$u1',X0,'e$u4')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d90,c41]) ).

cnf(d92,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u4')
    | product('e$u1','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d91,d70]) ).

cnf(d93,plain,
    ( ~ product('e$u1','e$u2',X0)
    | equalish(X0,'e$u4')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2') ),
    inference(resolution,[status(thm)],[d92,c38]) ).

cnf(d94,plain,
    ( ~ product(X0,'e$u1','e$u1')
    | product('e$u1',X0,'e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[d73,c41]) ).

cnf(d95,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3')
    | product('e$u1','e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d94,d70]) ).

cnf(d96,plain,
    ( ~ product(X0,'e$u1','e$u1')
    | product('e$u1',X0,'e$u3')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u2')
    | product('e$u1','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d95,c41]) ).

cnf(d97,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u2')
    | product('e$u1','e$u1','e$u4')
    | product('e$u1','e$u2','e$u3') ),
    inference(resolution,[status(thm)],[d96,d70]) ).

cnf(d98,plain,
    ( ~ product('e$u1',X0,'e$u4')
    | equalish(X0,'e$u1')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u3')
    | product('e$u1','e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d97,c39]) ).

cnf(d99,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u3')
    | product('e$u1','e$u2','e$u2')
    | equalish('e$u2','e$u1')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2') ),
    inference(resolution,[status(thm)],[d92,d98]) ).

cnf(d100,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u3')
    | product('e$u1','e$u2','e$u2') ),
    inference(resolution,[status(thm)],[c28,d99]) ).

cnf(d101,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | equalish('e$u2','e$u4')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u3') ),
    inference(resolution,[status(thm)],[d100,d93]) ).

cnf(d102,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | product('e$u1','e$u2','e$u3') ),
    inference(resolution,[status(thm)],[c30,d101]) ).

cnf(d103,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2')
    | equalish('e$u3','e$u4')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2') ),
    inference(resolution,[status(thm)],[d102,d93]) ).

cnf(d104,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u2','e$u1','e$u2') ),
    inference(resolution,[status(thm)],[c33,d103]) ).

cnf(d105,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | equalish('e$u2','e$u3')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[d104,d68]) ).

cnf(d106,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[c29,d105]) ).

cnf(d107,plain,
    ( cycle('e$u2','e$u3')
    | cycle('e$u2','e$u2')
    | cycle('e$u2','e$u1')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u2','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d106,d67]) ).

cnf(d108,plain,
    ( ~ cycle('e$u3','e$u0')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u2','e$u1','e$u4')
    | cycle('e$u2','e$u3')
    | cycle('e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d107,d62]) ).

cnf(d109,plain,
    ( cycle('e$u3','e$u1')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u2','e$u1','e$u4')
    | cycle('e$u2','e$u3')
    | cycle('e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d108,d13]) ).

cnf(d110,plain,
    ( ~ cycle('e$u3','e$u0')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u2','e$u1','e$u4')
    | cycle('e$u3','e$u1')
    | cycle('e$u2','e$u3') ),
    inference(resolution,[status(thm)],[d109,d61]) ).

cnf(d111,plain,
    ( cycle('e$u3','e$u1')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u2','e$u1','e$u4')
    | cycle('e$u3','e$u1')
    | cycle('e$u2','e$u3') ),
    inference(resolution,[status(thm)],[d110,d13]) ).

cnf(d112,plain,
    ( ~ cycle('e$u3','e$u0')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u2','e$u1','e$u4')
    | cycle('e$u3','e$u1') ),
    inference(resolution,[status(thm)],[d111,d59]) ).

cnf(d113,plain,
    ( cycle('e$u3','e$u1')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u2','e$u1','e$u4')
    | cycle('e$u3','e$u1') ),
    inference(resolution,[status(thm)],[d112,d13]) ).

cnf(d114,plain,
    ( ~ product('e$u3','e$u1',X0)
    | equalish(X0,'e$u4')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u2','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d113,d3]) ).

cnf(d115,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u2','e$u1','e$u4')
    | equalish('e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d114,d56]) ).

cnf(d116,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u2','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[c30,d115]) ).

cnf(d117,plain,
    ( cycle('e$u2','e$u3')
    | cycle('e$u2','e$u2')
    | cycle('e$u2','e$u1')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[d116,d65]) ).

cnf(d118,plain,
    ( ~ cycle('e$u3','e$u0')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | cycle('e$u2','e$u3')
    | cycle('e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d117,d62]) ).

cnf(d119,plain,
    ( cycle('e$u3','e$u1')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | cycle('e$u2','e$u3')
    | cycle('e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d118,d13]) ).

cnf(d120,plain,
    ( ~ cycle('e$u3','e$u0')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | cycle('e$u3','e$u1')
    | cycle('e$u2','e$u3') ),
    inference(resolution,[status(thm)],[d119,d61]) ).

cnf(d121,plain,
    ( cycle('e$u3','e$u1')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | cycle('e$u3','e$u1')
    | cycle('e$u2','e$u3') ),
    inference(resolution,[status(thm)],[d120,d13]) ).

cnf(d122,plain,
    ( ~ cycle('e$u3','e$u0')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | cycle('e$u3','e$u1') ),
    inference(resolution,[status(thm)],[d121,d59]) ).

cnf(d123,plain,
    ( cycle('e$u3','e$u1')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | cycle('e$u3','e$u1') ),
    inference(resolution,[status(thm)],[d122,d13]) ).

cnf(d124,plain,
    ( ~ product('e$u3','e$u1',X0)
    | equalish(X0,'e$u4')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[d123,d3]) ).

cnf(d125,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3')
    | equalish('e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d124,d56]) ).

cnf(d126,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[c30,d125]) ).

cnf(d127,plain,
    ( ~ product('e$u3','e$u1',X0)
    | equalish(X0,'e$u3')
    | product('e$u3','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d126,c38]) ).

cnf(d128,plain,
    ( product('e$u4',X0,'e$u4')
    | product('e$u4',X0,'e$u3')
    | product('e$u4',X0,'e$u2')
    | product('e$u4',X0,'e$u1')
    | ~ 'group$uelement'(X0) ),
    inference(resolution,[status(thm)],[c37,c24]) ).

cnf(d129,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u3','e$u2')
    | product('e$u4','e$u3','e$u1') ),
    inference(resolution,[status(thm)],[d128,c23]) ).

cnf(d130,plain,
    ( ~ product(X0,'e$u4','e$u3')
    | product('e$u3',X0,'e$u1')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u3','e$u2') ),
    inference(resolution,[status(thm)],[d129,c41]) ).

cnf(d131,plain,
    ( ~ product(X0,'e$u3','e$u1')
    | product('e$u1',X0,'e$u3')
    | product('e$u3','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d126,c41]) ).

cnf(d132,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u3','e$u2')
    | product('e$u3','e$u1','e$u4')
    | product('e$u1','e$u4','e$u3') ),
    inference(resolution,[status(thm)],[d131,d129]) ).

cnf(d133,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u3','e$u2')
    | product('e$u3','e$u1','e$u1')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u3','e$u2')
    | product('e$u3','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d132,d130]) ).

cnf(d134,plain,
    ( product('e$u3','e$u1','e$u4')
    | equalish('e$u1','e$u3')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u3','e$u2')
    | product('e$u3','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d133,d127]) ).

cnf(d135,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u3','e$u2')
    | product('e$u3','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[c26,d134]) ).

cnf(d136,plain,
    ( ~ product(X0,'e$u3','e$u1')
    | product('e$u1',X0,'e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u3','e$u2') ),
    inference(resolution,[status(thm)],[d135,c41]) ).

cnf(d137,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u3','e$u2')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u3','e$u2')
    | product('e$u1','e$u4','e$u4') ),
    inference(resolution,[status(thm)],[d136,d129]) ).

cnf(d138,plain,
    ( ~ product(X0,'e$u1','e$u4')
    | product('e$u4',X0,'e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u3','e$u2') ),
    inference(resolution,[status(thm)],[d137,c41]) ).

cnf(d139,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u3','e$u2')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u3','e$u2')
    | product('e$u4','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d138,d135]) ).

cnf(d140,plain,
    ( ~ product('e$u4',X0,'e$u2')
    | equalish(X0,'e$u3')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d139,c39]) ).

cnf(d141,plain,
    ( ~ product(X0,'e$u1','e$u3')
    | equalish(X0,'e$u3')
    | product('e$u3','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d126,c40]) ).

cnf(d142,plain,
    ( ~ product('e$u2','e$u1',X0)
    | equalish(X0,'e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[d104,c38]) ).

cnf(d143,plain,
    ( product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | product('e$u4','e$u2','e$u1') ),
    inference(resolution,[status(thm)],[d128,c22]) ).

cnf(d144,plain,
    ( ~ product(X0,'e$u4','e$u2')
    | product('e$u2',X0,'e$u1')
    | product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d143,c41]) ).

cnf(d145,plain,
    ( ~ product(X0,'e$u2','e$u1')
    | product('e$u1',X0,'e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[d104,c41]) ).

cnf(d146,plain,
    ( product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u1','e$u4','e$u2') ),
    inference(resolution,[status(thm)],[d145,d143]) ).

cnf(d147,plain,
    ( product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | product('e$u2','e$u1','e$u1')
    | product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[d146,d144]) ).

cnf(d148,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | equalish('e$u1','e$u2')
    | product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[d147,d142]) ).

cnf(d149,plain,
    ( product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[c25,d148]) ).

cnf(d150,plain,
    ( product('e$u3','e$u1','e$u4')
    | equalish('e$u2','e$u3')
    | product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | product('e$u2','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d149,d141]) ).

cnf(d151,plain,
    ( product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | product('e$u3','e$u1','e$u4')
    | product('e$u2','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[c29,d150]) ).

cnf(d152,plain,
    ( ~ product(X0,'e$u2','e$u1')
    | product('e$u1',X0,'e$u4')
    | product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | product('e$u3','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d151,c41]) ).

cnf(d153,plain,
    ( product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | product('e$u3','e$u1','e$u4')
    | product('e$u1','e$u4','e$u4') ),
    inference(resolution,[status(thm)],[d152,d143]) ).

cnf(d154,plain,
    ( ~ product(X0,'e$u1','e$u4')
    | product('e$u4',X0,'e$u4')
    | product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | product('e$u3','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d153,c41]) ).

cnf(d155,plain,
    ( product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | product('e$u3','e$u1','e$u4')
    | product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | product('e$u4','e$u2','e$u4')
    | product('e$u3','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d154,d151]) ).

cnf(d156,plain,
    ( ~ product(X0,'e$u1','e$u4')
    | equalish(X0,'e$u3')
    | product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d155,c40]) ).

cnf(d157,plain,
    ( ~ product(X0,'e$u2','e$u1')
    | product('e$u1',X0,'e$u3')
    | product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | product('e$u2','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d149,c41]) ).

cnf(d158,plain,
    ( product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u1','e$u4','e$u3') ),
    inference(resolution,[status(thm)],[d157,d143]) ).

cnf(d159,plain,
    ( ~ product(X0,'e$u1','e$u4')
    | product('e$u4',X0,'e$u3')
    | product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | product('e$u2','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d158,c41]) ).

cnf(d160,plain,
    ( product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | product('e$u4','e$u3','e$u3')
    | product('e$u2','e$u1','e$u4')
    | product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d155,d159]) ).

cnf(d161,plain,
    ( product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2')
    | equalish('e$u2','e$u3')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d160,d156]) ).

cnf(d162,plain,
    ( product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3')
    | product('e$u4','e$u2','e$u2') ),
    inference(resolution,[status(thm)],[c29,d161]) ).

cnf(d163,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | equalish('e$u2','e$u3')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3') ),
    inference(resolution,[status(thm)],[d162,d140]) ).

cnf(d164,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u2','e$u3') ),
    inference(resolution,[status(thm)],[c29,d163]) ).

cnf(d165,plain,
    ( ~ product(X0,'e$u2','e$u3')
    | equalish(X0,'e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d164,c40]) ).

cnf(d166,plain,
    ( ~ product(X0,'e$u4','e$u2')
    | product('e$u2',X0,'e$u3')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d164,c41]) ).

cnf(d167,plain,
    ( product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | product('e$u3','e$u2','e$u1') ),
    inference(resolution,[status(thm)],[d0,c22]) ).

cnf(d168,plain,
    ( ~ product(X0,'e$u3','e$u2')
    | product('e$u2',X0,'e$u1')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d167,c41]) ).

cnf(d169,plain,
    ( product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | product('e$u1','e$u3','e$u2') ),
    inference(resolution,[status(thm)],[d145,d167]) ).

cnf(d170,plain,
    ( product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | product('e$u2','e$u1','e$u1')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[d169,d168]) ).

cnf(d171,plain,
    ( product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3')
    | equalish('e$u1','e$u2')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[d170,d142]) ).

cnf(d172,plain,
    ( product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u2','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[c25,d171]) ).

cnf(d173,plain,
    ( ~ product(X0,'e$u2','e$u1')
    | product('e$u1',X0,'e$u3')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | product('e$u2','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d172,c41]) ).

cnf(d174,plain,
    ( product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u1','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d173,d167]) ).

cnf(d175,plain,
    ( ~ product(X0,'e$u1','e$u3')
    | product('e$u3',X0,'e$u3')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | product('e$u2','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d174,c41]) ).

cnf(d176,plain,
    ( product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | product('e$u2','e$u1','e$u4')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | product('e$u3','e$u2','e$u3')
    | product('e$u2','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d175,d172]) ).

cnf(d177,plain,
    ( ~ product(X0,'e$u1','e$u4')
    | equalish(X0,'e$u2')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d176,c40]) ).

cnf(d178,plain,
    ( cycle('e$u2','e$u3')
    | cycle('e$u2','e$u2')
    | cycle('e$u2','e$u1')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d176,d65]) ).

cnf(d179,plain,
    ( ~ cycle('e$u3','e$u0')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | cycle('e$u2','e$u3')
    | cycle('e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d178,d62]) ).

cnf(d180,plain,
    ( cycle('e$u3','e$u1')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | cycle('e$u2','e$u3')
    | cycle('e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d179,d13]) ).

cnf(d181,plain,
    ( ~ cycle('e$u3','e$u0')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | cycle('e$u3','e$u1')
    | cycle('e$u2','e$u3') ),
    inference(resolution,[status(thm)],[d180,d61]) ).

cnf(d182,plain,
    ( cycle('e$u3','e$u1')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | cycle('e$u3','e$u1')
    | cycle('e$u2','e$u3') ),
    inference(resolution,[status(thm)],[d181,d13]) ).

cnf(d183,plain,
    ( ~ cycle('e$u3','e$u0')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | cycle('e$u3','e$u1') ),
    inference(resolution,[status(thm)],[d182,d59]) ).

cnf(d184,plain,
    ( cycle('e$u3','e$u1')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | cycle('e$u3','e$u1') ),
    inference(resolution,[status(thm)],[d183,d13]) ).

cnf(d185,plain,
    ( ~ product('e$u3','e$u1',X0)
    | equalish(X0,'e$u4')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d184,d3]) ).

cnf(d186,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | equalish('e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d185,d126]) ).

cnf(d187,plain,
    ( product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | product('e$u3','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[c33,d186]) ).

cnf(d188,plain,
    ( product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2')
    | equalish('e$u3','e$u2')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2') ),
    inference(resolution,[status(thm)],[d187,d177]) ).

cnf(d189,plain,
    ( product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u3','e$u2','e$u2') ),
    inference(resolution,[status(thm)],[c32,d188]) ).

cnf(d190,plain,
    ( ~ product(X0,'e$u3','e$u2')
    | product('e$u2',X0,'e$u2')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3') ),
    inference(resolution,[status(thm)],[d189,c41]) ).

cnf(d191,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u2','e$u4','e$u2') ),
    inference(resolution,[status(thm)],[d190,d139]) ).

cnf(d192,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u2','e$u4')
    | product('e$u2','e$u2','e$u3')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3') ),
    inference(resolution,[status(thm)],[d191,d166]) ).

cnf(d193,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u2','e$u4')
    | equalish('e$u2','e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u2','e$u4')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3') ),
    inference(resolution,[status(thm)],[d192,d165]) ).

cnf(d194,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u2','e$u4')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3') ),
    inference(resolution,[status(thm)],[c30,d193]) ).

cnf(d195,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u2','e$u4')
    | equalish('e$u3','e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u2','e$u4')
    | product('e$u3','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d194,d165]) ).

cnf(d196,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u2','e$u4')
    | product('e$u3','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[c33,d195]) ).

cnf(d197,plain,
    ( ~ product(X0,'e$u3','e$u2')
    | product('e$u2',X0,'e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d196,c41]) ).

cnf(d198,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u2','e$u4')
    | product('e$u2','e$u4','e$u4') ),
    inference(resolution,[status(thm)],[d197,d139]) ).

cnf(d199,plain,
    ( ~ product(X0,'e$u2','e$u4')
    | product('e$u4',X0,'e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d198,c41]) ).

cnf(d200,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u2','e$u4')
    | product('e$u4','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d199,d196]) ).

cnf(d201,plain,
    ( ~ product(X0,'e$u2','e$u4')
    | equalish(X0,'e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d200,c40]) ).

cnf(d202,plain,
    ( ~ product(X0,'e$u4','e$u2')
    | product('e$u2',X0,'e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d200,c41]) ).

cnf(d203,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u2','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d202,d191]) ).

cnf(d204,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | equalish('e$u2','e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3') ),
    inference(resolution,[status(thm)],[d203,d201]) ).

cnf(d205,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3') ),
    inference(resolution,[status(thm)],[c30,d204]) ).

cnf(d206,plain,
    ( ~ product('e$u3','e$u2',X0)
    | equalish(X0,'e$u3')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d205,c38]) ).

cnf(d207,plain,
    ( ~ product(X0,'e$u4','e$u3')
    | product('e$u3',X0,'e$u2')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d139,c41]) ).

cnf(d208,plain,
    ( ~ product(X0,'e$u3','e$u2')
    | product('e$u2',X0,'e$u3')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d205,c41]) ).

cnf(d209,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4')
    | product('e$u2','e$u4','e$u3') ),
    inference(resolution,[status(thm)],[d208,d139]) ).

cnf(d210,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u3','e$u2','e$u2')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d209,d207]) ).

cnf(d211,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4')
    | equalish('e$u2','e$u3')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d210,d206]) ).

cnf(d212,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[c29,d211]) ).

cnf(d213,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3')
    | equalish('e$u3','e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d212,d201]) ).

cnf(d214,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[c33,d213]) ).

cnf(d215,plain,
    ( ~ product('e$u4','e$u3',X0)
    | equalish(X0,'e$u3')
    | product('e$u4','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d214,c38]) ).

cnf(d216,plain,
    ( ~ product(X0,'e$u3','e$u3')
    | equalish(X0,'e$u4')
    | product('e$u4','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d214,c40]) ).

cnf(d217,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u3','e$u2')
    | product('e$u3','e$u3','e$u1') ),
    inference(resolution,[status(thm)],[d0,c23]) ).

cnf(d218,plain,
    ( ~ product('e$u3',X0,'e$u1')
    | equalish(X0,'e$u3')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u3','e$u2') ),
    inference(resolution,[status(thm)],[d217,c39]) ).

cnf(d219,plain,
    ( ~ product(X0,'e$u3','e$u3')
    | product('e$u3',X0,'e$u1')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u3','e$u2') ),
    inference(resolution,[status(thm)],[d217,c41]) ).

cnf(d220,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u3','e$u2')
    | product('e$u3','e$u4','e$u1')
    | product('e$u4','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d214,d219]) ).

cnf(d221,plain,
    ( ~ product(X0,'e$u3','e$u3')
    | product('e$u3',X0,'e$u2')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u1')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d220,c41]) ).

cnf(d222,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u1')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u4','e$u2') ),
    inference(resolution,[status(thm)],[d221,d214]) ).

cnf(d223,plain,
    ( product('e$u4','e$u3','e$u4')
    | equalish('e$u3','e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u4','e$u1')
    | product('e$u3','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d222,d216]) ).

cnf(d224,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u4','e$u1')
    | product('e$u3','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[c33,d223]) ).

cnf(d225,plain,
    ( ~ product('e$u3','e$u3',X0)
    | equalish(X0,'e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u4','e$u1') ),
    inference(resolution,[status(thm)],[d224,c38]) ).

cnf(d226,plain,
    ( ~ product('e$u3',X0,'e$u4')
    | equalish(X0,'e$u3')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u4','e$u1') ),
    inference(resolution,[status(thm)],[d224,c39]) ).

cnf(d227,plain,
    ( product('e$u1','e$u3','e$u4')
    | product('e$u1','e$u3','e$u3')
    | product('e$u1','e$u3','e$u2')
    | product('e$u1','e$u3','e$u1') ),
    inference(resolution,[status(thm)],[d27,c23]) ).

cnf(d228,plain,
    ( product('e$u1','e$u3','e$u4')
    | product('e$u1','e$u3','e$u3')
    | product('e$u1','e$u3','e$u2')
    | product('e$u3','e$u1','e$u4')
    | product('e$u1','e$u1','e$u3') ),
    inference(resolution,[status(thm)],[d131,d227]) ).

cnf(d229,plain,
    ( product('e$u3','e$u1','e$u4')
    | equalish('e$u1','e$u3')
    | product('e$u3','e$u1','e$u4')
    | product('e$u1','e$u3','e$u4')
    | product('e$u1','e$u3','e$u3')
    | product('e$u1','e$u3','e$u2') ),
    inference(resolution,[status(thm)],[d228,d141]) ).

cnf(d230,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u1','e$u3','e$u4')
    | product('e$u1','e$u3','e$u3')
    | product('e$u1','e$u3','e$u2') ),
    inference(resolution,[status(thm)],[c26,d229]) ).

cnf(d231,plain,
    ( ~ product(X0,'e$u1','e$u3')
    | product('e$u3',X0,'e$u2')
    | product('e$u3','e$u1','e$u4')
    | product('e$u1','e$u3','e$u4')
    | product('e$u1','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d230,c41]) ).

cnf(d232,plain,
    ( product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u1','e$u4')
    | product('e$u3','e$u3','e$u2')
    | product('e$u1','e$u3','e$u4')
    | product('e$u1','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d231,d126]) ).

cnf(d233,plain,
    ( ~ product(X0,'e$u3','e$u3')
    | equalish(X0,'e$u1')
    | product('e$u3','e$u3','e$u2')
    | product('e$u3','e$u1','e$u4')
    | product('e$u1','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d232,c40]) ).

cnf(d234,plain,
    ( product('e$u3','e$u3','e$u2')
    | product('e$u3','e$u1','e$u4')
    | product('e$u1','e$u3','e$u4')
    | equalish('e$u4','e$u1')
    | product('e$u4','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d214,d233]) ).

cnf(d235,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u3','e$u2')
    | product('e$u3','e$u1','e$u4')
    | product('e$u1','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[c34,d234]) ).

cnf(d236,plain,
    ( ~ product(X0,'e$u3','e$u4')
    | equalish(X0,'e$u1')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u3','e$u2')
    | product('e$u3','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d235,c40]) ).

cnf(d237,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u3','e$u2')
    | product('e$u3','e$u1','e$u4')
    | equalish('e$u3','e$u1')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u4','e$u1') ),
    inference(resolution,[status(thm)],[d224,d236]) ).

cnf(d238,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u4','e$u1')
    | product('e$u3','e$u3','e$u2')
    | product('e$u3','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[c31,d237]) ).

cnf(d239,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u4','e$u1')
    | equalish('e$u1','e$u3')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u4','e$u1')
    | product('e$u3','e$u3','e$u2') ),
    inference(resolution,[status(thm)],[d238,d226]) ).

cnf(d240,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u4','e$u1')
    | product('e$u3','e$u3','e$u2') ),
    inference(resolution,[status(thm)],[c26,d239]) ).

cnf(d241,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u4','e$u1')
    | equalish('e$u2','e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u4','e$u1') ),
    inference(resolution,[status(thm)],[d240,d225]) ).

cnf(d242,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u4','e$u1') ),
    inference(resolution,[status(thm)],[c30,d241]) ).

cnf(d243,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u3','e$u2')
    | equalish('e$u4','e$u3')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2') ),
    inference(resolution,[status(thm)],[d242,d218]) ).

cnf(d244,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u3','e$u2') ),
    inference(resolution,[status(thm)],[c36,d243]) ).

cnf(d245,plain,
    ( ~ product(X0,'e$u3','e$u3')
    | product('e$u3',X0,'e$u2')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d244,c41]) ).

cnf(d246,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u4','e$u2') ),
    inference(resolution,[status(thm)],[d245,d214]) ).

cnf(d247,plain,
    ( product('e$u4','e$u3','e$u4')
    | equalish('e$u3','e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d246,d216]) ).

cnf(d248,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[c33,d247]) ).

cnf(d249,plain,
    ( ~ product('e$u3','e$u3',X0)
    | equalish(X0,'e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2') ),
    inference(resolution,[status(thm)],[d248,c38]) ).

cnf(d250,plain,
    ( ~ product('e$u3',X0,'e$u4')
    | equalish(X0,'e$u3')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2') ),
    inference(resolution,[status(thm)],[d248,c39]) ).

cnf(d251,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u3','e$u2')
    | product('e$u3','e$u1','e$u4')
    | equalish('e$u3','e$u1')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2') ),
    inference(resolution,[status(thm)],[d248,d236]) ).

cnf(d252,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u3','e$u2')
    | product('e$u3','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[c31,d251]) ).

cnf(d253,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | equalish('e$u1','e$u3')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u3','e$u2') ),
    inference(resolution,[status(thm)],[d252,d250]) ).

cnf(d254,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u3','e$u2') ),
    inference(resolution,[status(thm)],[c26,d253]) ).

cnf(d255,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2')
    | equalish('e$u2','e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2') ),
    inference(resolution,[status(thm)],[d254,d249]) ).

cnf(d256,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u2') ),
    inference(resolution,[status(thm)],[c30,d255]) ).

cnf(d257,plain,
    ( ~ product('e$u3','e$u4',X0)
    | equalish(X0,'e$u2')
    | product('e$u4','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d256,c38]) ).

cnf(d258,plain,
    ( ~ product(X0,'e$u3','e$u4')
    | product('e$u4',X0,'e$u2')
    | product('e$u4','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d256,c41]) ).

cnf(d259,plain,
    ( ~ product('e$u3',X0,'e$u2')
    | equalish(X0,'e$u3')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u1')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d220,c39]) ).

cnf(d260,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u1')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | equalish('e$u4','e$u3')
    | product('e$u4','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d256,d259]) ).

cnf(d261,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u1')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[c36,d260]) ).

cnf(d262,plain,
    ( product('e$u4','e$u3','e$u4')
    | equalish('e$u3','e$u4')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u1')
    | product('e$u3','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d261,d216]) ).

cnf(d263,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u1')
    | product('e$u3','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[c33,d262]) ).

cnf(d264,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u2')
    | product('e$u4','e$u3','e$u4')
    | product('e$u3','e$u4','e$u1') ),
    inference(resolution,[status(thm)],[d263,d258]) ).

cnf(d265,plain,
    ( product('e$u4','e$u3','e$u4')
    | equalish('e$u1','e$u2')
    | product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u2') ),
    inference(resolution,[status(thm)],[d264,d257]) ).

cnf(d266,plain,
    ( product('e$u4','e$u3','e$u4')
    | product('e$u4','e$u3','e$u2') ),
    inference(resolution,[status(thm)],[c25,d265]) ).

cnf(d267,plain,
    ( product('e$u4','e$u3','e$u4')
    | equalish('e$u2','e$u3')
    | product('e$u4','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d266,d215]) ).

cnf(d268,plain,
    product('e$u4','e$u3','e$u4'),
    inference(resolution,[status(thm)],[c29,d267]) ).

cnf(d269,plain,
    ( ~ product('e$u4','e$u3',X0)
    | equalish(X0,'e$u4') ),
    inference(resolution,[status(thm)],[d268,c38]) ).

cnf(d270,plain,
    ( ~ product(X0,'e$u3','e$u4')
    | equalish(X0,'e$u4') ),
    inference(resolution,[status(thm)],[d268,c40]) ).

cnf(d271,plain,
    ( ~ product(X0,'e$u4','e$u3')
    | product('e$u3',X0,'e$u4') ),
    inference(resolution,[status(thm)],[d268,c41]) ).

cnf(d272,plain,
    ( product('e$u3','e$u4','e$u4')
    | product('e$u3','e$u4','e$u3')
    | product('e$u3','e$u4','e$u2')
    | product('e$u3','e$u4','e$u1') ),
    inference(resolution,[status(thm)],[d0,c24]) ).

cnf(d273,plain,
    ( ~ product(X0,'e$u3','e$u4')
    | product('e$u4',X0,'e$u1')
    | product('e$u3','e$u4','e$u4')
    | product('e$u3','e$u4','e$u3')
    | product('e$u3','e$u4','e$u2') ),
    inference(resolution,[status(thm)],[d272,c41]) ).

cnf(d274,plain,
    ( product('e$u4','e$u4','e$u1')
    | product('e$u3','e$u4','e$u4')
    | product('e$u3','e$u4','e$u3')
    | product('e$u3','e$u4','e$u2') ),
    inference(resolution,[status(thm)],[d268,d273]) ).

cnf(d275,plain,
    ( ~ product(X0,'e$u3','e$u4')
    | product('e$u4',X0,'e$u2')
    | product('e$u4','e$u4','e$u1')
    | product('e$u3','e$u4','e$u4')
    | product('e$u3','e$u4','e$u3') ),
    inference(resolution,[status(thm)],[d274,c41]) ).

cnf(d276,plain,
    ( product('e$u4','e$u4','e$u1')
    | product('e$u4','e$u4','e$u2')
    | product('e$u3','e$u4','e$u4')
    | product('e$u3','e$u4','e$u3') ),
    inference(resolution,[status(thm)],[d275,d268]) ).

cnf(d277,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u4','e$u4','e$u2')
    | product('e$u4','e$u4','e$u1')
    | product('e$u3','e$u4','e$u4') ),
    inference(resolution,[status(thm)],[d276,d271]) ).

cnf(d278,plain,
    ( equalish('e$u3','e$u4')
    | product('e$u4','e$u4','e$u2')
    | product('e$u4','e$u4','e$u1')
    | product('e$u3','e$u4','e$u4') ),
    inference(resolution,[status(thm)],[d277,d270]) ).

cnf(d279,plain,
    ( product('e$u4','e$u4','e$u2')
    | product('e$u4','e$u4','e$u1')
    | product('e$u3','e$u4','e$u4') ),
    inference(resolution,[status(thm)],[c33,d278]) ).

cnf(d280,plain,
    ( ~ product('e$u3',X0,'e$u4')
    | equalish(X0,'e$u4')
    | product('e$u4','e$u4','e$u2')
    | product('e$u4','e$u4','e$u1') ),
    inference(resolution,[status(thm)],[d279,c39]) ).

cnf(d281,plain,
    ( ~ product('e$u3',X0,'e$u3')
    | equalish(X0,'e$u1')
    | product('e$u3','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d126,c39]) ).

cnf(d282,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u3','e$u2')
    | product('e$u3','e$u1','e$u4')
    | product('e$u1','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d131,d217]) ).

cnf(d283,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u3','e$u2')
    | product('e$u3','e$u1','e$u1')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u3','e$u2')
    | product('e$u3','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d282,d219]) ).

cnf(d284,plain,
    ( product('e$u3','e$u1','e$u4')
    | equalish('e$u1','e$u3')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u3','e$u2')
    | product('e$u3','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[d283,d127]) ).

cnf(d285,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u3','e$u2')
    | product('e$u3','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[c26,d284]) ).

cnf(d286,plain,
    ( ~ product(X0,'e$u3','e$u1')
    | product('e$u1',X0,'e$u4')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u3','e$u2') ),
    inference(resolution,[status(thm)],[d285,c41]) ).

cnf(d287,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u3','e$u2')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u3','e$u2')
    | product('e$u1','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d286,d217]) ).

cnf(d288,plain,
    ( ~ product(X0,'e$u3','e$u4')
    | equalish(X0,'e$u1')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u3','e$u2') ),
    inference(resolution,[status(thm)],[d287,c40]) ).

cnf(d289,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u3','e$u2')
    | equalish('e$u4','e$u1') ),
    inference(resolution,[status(thm)],[d268,d288]) ).

cnf(d290,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u3','e$u2') ),
    inference(resolution,[status(thm)],[c34,d289]) ).

cnf(d291,plain,
    ( ~ product('e$u3',X0,'e$u2')
    | equalish(X0,'e$u2')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3') ),
    inference(resolution,[status(thm)],[d189,c39]) ).

cnf(d292,plain,
    ( product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3')
    | equalish('e$u3','e$u2')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d290,d291]) ).

cnf(d293,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4')
    | product('e$u3','e$u2','e$u3') ),
    inference(resolution,[status(thm)],[c32,d292]) ).

cnf(d294,plain,
    ( ~ product('e$u3','e$u2',X0)
    | equalish(X0,'e$u3')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d293,c38]) ).

cnf(d295,plain,
    ( ~ product(X0,'e$u3','e$u3')
    | product('e$u3',X0,'e$u2')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d290,c41]) ).

cnf(d296,plain,
    ( ~ product(X0,'e$u3','e$u2')
    | product('e$u2',X0,'e$u3')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d293,c41]) ).

cnf(d297,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4')
    | product('e$u2','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d296,d290]) ).

cnf(d298,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u2','e$u2')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d297,d295]) ).

cnf(d299,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4')
    | equalish('e$u2','e$u3')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[d298,d294]) ).

cnf(d300,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u2','e$u4') ),
    inference(resolution,[status(thm)],[c29,d299]) ).

cnf(d301,plain,
    ( ~ product(X0,'e$u3','e$u2')
    | product('e$u2',X0,'e$u4')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d300,c41]) ).

cnf(d302,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3')
    | product('e$u2','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d301,d290]) ).

cnf(d303,plain,
    ( equalish('e$u2','e$u4')
    | product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[d302,d270]) ).

cnf(d304,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u3','e$u3') ),
    inference(resolution,[status(thm)],[c30,d303]) ).

cnf(d305,plain,
    ( product('e$u3','e$u1','e$u4')
    | equalish('e$u3','e$u1')
    | product('e$u3','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d304,d281]) ).

cnf(d306,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u3','e$u1','e$u4') ),
    inference(resolution,[status(thm)],[c31,d305]) ).

cnf(d307,plain,
    ( product('e$u4','e$u4','e$u2')
    | product('e$u4','e$u4','e$u1')
    | equalish('e$u1','e$u4')
    | product('e$u3','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[d306,d280]) ).

cnf(d308,plain,
    ( product('e$u4','e$u4','e$u2')
    | product('e$u4','e$u4','e$u1')
    | product('e$u3','e$u3','e$u4') ),
    inference(resolution,[status(thm)],[c27,d307]) ).

cnf(d309,plain,
    ( product('e$u4','e$u4','e$u2')
    | product('e$u4','e$u4','e$u1')
    | equalish('e$u3','e$u4')
    | product('e$u4','e$u4','e$u2')
    | product('e$u4','e$u4','e$u1') ),
    inference(resolution,[status(thm)],[d308,d280]) ).

cnf(d310,plain,
    ( product('e$u4','e$u4','e$u2')
    | product('e$u4','e$u4','e$u1') ),
    inference(resolution,[status(thm)],[c33,d309]) ).

cnf(d311,plain,
    ( ~ product(X0,'e$u4','e$u4')
    | product('e$u4',X0,'e$u1')
    | product('e$u4','e$u4','e$u2') ),
    inference(resolution,[status(thm)],[d310,c41]) ).

cnf(d312,plain,
    ( ~ product(X0,'e$u4','e$u1')
    | equalish(X0,'e$u3')
    | product('e$u3','e$u4','e$u4')
    | product('e$u3','e$u4','e$u3')
    | product('e$u3','e$u4','e$u2') ),
    inference(resolution,[status(thm)],[d272,c40]) ).

cnf(d313,plain,
    ( product('e$u3','e$u4','e$u4')
    | product('e$u3','e$u4','e$u3')
    | product('e$u3','e$u4','e$u2')
    | equalish('e$u4','e$u3')
    | product('e$u4','e$u4','e$u2') ),
    inference(resolution,[status(thm)],[d310,d312]) ).

cnf(d314,plain,
    ( product('e$u4','e$u4','e$u2')
    | product('e$u3','e$u4','e$u4')
    | product('e$u3','e$u4','e$u3')
    | product('e$u3','e$u4','e$u2') ),
    inference(resolution,[status(thm)],[c36,d313]) ).

cnf(d315,plain,
    ( ~ product(X0,'e$u3','e$u4')
    | product('e$u4',X0,'e$u2')
    | product('e$u4','e$u4','e$u2')
    | product('e$u3','e$u4','e$u4')
    | product('e$u3','e$u4','e$u3') ),
    inference(resolution,[status(thm)],[d314,c41]) ).

cnf(d316,plain,
    ( product('e$u4','e$u4','e$u2')
    | product('e$u4','e$u4','e$u2')
    | product('e$u3','e$u4','e$u4')
    | product('e$u3','e$u4','e$u3') ),
    inference(resolution,[status(thm)],[d315,d268]) ).

cnf(d317,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u4','e$u4','e$u2')
    | product('e$u3','e$u4','e$u4') ),
    inference(resolution,[status(thm)],[d316,d271]) ).

cnf(d318,plain,
    ( equalish('e$u3','e$u4')
    | product('e$u4','e$u4','e$u2')
    | product('e$u3','e$u4','e$u4') ),
    inference(resolution,[status(thm)],[d317,d270]) ).

cnf(d319,plain,
    ( product('e$u4','e$u4','e$u2')
    | product('e$u3','e$u4','e$u4') ),
    inference(resolution,[status(thm)],[c33,d318]) ).

cnf(d320,plain,
    ( product('e$u4','e$u4','e$u2')
    | product('e$u4','e$u3','e$u1')
    | product('e$u4','e$u4','e$u2') ),
    inference(resolution,[status(thm)],[d319,d311]) ).

cnf(d321,plain,
    ( equalish('e$u1','e$u4')
    | product('e$u4','e$u4','e$u2') ),
    inference(resolution,[status(thm)],[d320,d269]) ).

cnf(d322,plain,
    product('e$u4','e$u4','e$u2'),
    inference(resolution,[status(thm)],[c27,d321]) ).

cnf(d323,plain,
    ( ~ product('e$u4','e$u4',X0)
    | equalish(X0,'e$u2') ),
    inference(resolution,[status(thm)],[d322,c38]) ).

cnf(d324,plain,
    ( ~ product(X0,'e$u4','e$u4')
    | product('e$u4',X0,'e$u2') ),
    inference(resolution,[status(thm)],[d322,c41]) ).

cnf(d325,plain,
    ( ~ product(X0,'e$u4','e$u2')
    | equalish(X0,'e$u3')
    | product('e$u4','e$u4','e$u1')
    | product('e$u3','e$u4','e$u4')
    | product('e$u3','e$u4','e$u3') ),
    inference(resolution,[status(thm)],[d274,c40]) ).

cnf(d326,plain,
    ( product('e$u4','e$u4','e$u1')
    | product('e$u3','e$u4','e$u4')
    | product('e$u3','e$u4','e$u3')
    | equalish('e$u4','e$u3') ),
    inference(resolution,[status(thm)],[d322,d325]) ).

cnf(d327,plain,
    ( product('e$u4','e$u4','e$u1')
    | product('e$u3','e$u4','e$u4')
    | product('e$u3','e$u4','e$u3') ),
    inference(resolution,[status(thm)],[c36,d326]) ).

cnf(d328,plain,
    ( product('e$u3','e$u3','e$u4')
    | product('e$u4','e$u4','e$u1')
    | product('e$u3','e$u4','e$u4') ),
    inference(resolution,[status(thm)],[d327,d271]) ).

cnf(d329,plain,
    ( equalish('e$u3','e$u4')
    | product('e$u4','e$u4','e$u1')
    | product('e$u3','e$u4','e$u4') ),
    inference(resolution,[status(thm)],[d328,d270]) ).

cnf(d330,plain,
    ( product('e$u4','e$u4','e$u1')
    | product('e$u3','e$u4','e$u4') ),
    inference(resolution,[status(thm)],[c33,d329]) ).

cnf(d331,plain,
    ( product('e$u4','e$u3','e$u2')
    | product('e$u4','e$u4','e$u1') ),
    inference(resolution,[status(thm)],[d330,d324]) ).

cnf(d332,plain,
    ( equalish('e$u2','e$u4')
    | product('e$u4','e$u4','e$u1') ),
    inference(resolution,[status(thm)],[d331,d269]) ).

cnf(d333,plain,
    product('e$u4','e$u4','e$u1'),
    inference(resolution,[status(thm)],[c30,d332]) ).

cnf(d334,plain,
    equalish('e$u1','e$u2'),
    inference(resolution,[status(thm)],[d333,d323]) ).

cnf(d335,plain,
    $false,
    inference(resolution,[status(thm)],[c25,d334]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP129-3.004 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.04  % Command  : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35  % Computer : n005.cluster.edu
% 0.09/0.35  % Model    : x86_64 x86_64
% 0.09/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35  % Memory   : 8046.5625MB
% 0.09/0.35  % OS       : Linux 6.8.0-71-generic
% 0.09/0.35  % CPULimit : 300
% 0.09/0.35  % WCLimit  : 300
% 0.09/0.35  % DateTime : Fri Sep 25 14:28:18 UTC 2026
% 0.09/0.36  % CPUTime  : 
% 0.09/0.36  Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 49.51/8.01  % SZS status Unsatisfiable for theBenchmark.p
% 49.51/8.01  % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------