%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : ALG216+2 : TPTP v5.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art02.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Sat Dec 25 04:21:02 EST 2010
% Result : Theorem 9.06s
% Output : CNFRefutation 9.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 10
% Syntax : Number of formulae : 165 ( 28 unt; 0 def)
% Number of atoms : 1947 ( 66 equ)
% Maximal formula atoms : 44 ( 11 avg)
% Number of connectives : 2672 ( 890 ~;1533 |; 209 &)
% ( 1 <=>; 39 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 12 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-3 aty)
% Number of variables : 121 ( 0 sgn 92 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(159,axiom,
! [X1] :
( l2_struct_0(X1)
=> l1_struct_0(X1) ),
file('/tmp/tmpsY844r/sel_ALG216+2.p_1',dt_l2_struct_0) ).
fof(303,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v4_group_1(X1)
& v6_vectsp_1(X1)
& v7_vectsp_1(X1)
& v8_vectsp_1(X1)
& l3_vectsp_1(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v3_rlvect_1(X2)
& v4_rlvect_1(X2)
& v5_rlvect_1(X2)
& v6_rlvect_1(X2)
& v5_vectsp_2(X2,X1)
& l1_vectsp_2(X2,X1) )
=> ! [X3] :
( m1_rmod_2(X3,X1,X2)
=> r1_rlvect_1(X3,k1_rlvect_1(X2)) ) ) ),
file('/tmp/tmpsY844r/sel_ALG216+2.p_1',t25_rmod_2) ).
fof(400,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v4_group_1(X1)
& v6_vectsp_1(X1)
& v7_vectsp_1(X1)
& v8_vectsp_1(X1)
& l3_vectsp_1(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v3_rlvect_1(X2)
& v4_rlvect_1(X2)
& v5_rlvect_1(X2)
& v6_rlvect_1(X2)
& v5_vectsp_2(X2,X1)
& l1_vectsp_2(X2,X1) )
=> m1_rmod_2(X2,X1,X2) ) ),
file('/tmp/tmpsY844r/sel_ALG216+2.p_1',t32_rmod_2) ).
fof(449,axiom,
! [X1] :
( l3_vectsp_1(X1)
=> ( l1_rlvect_1(X1)
& l2_vectsp_1(X1) ) ),
file('/tmp/tmpsY844r/sel_ALG216+2.p_1',dt_l3_vectsp_1) ).
fof(1037,axiom,
! [X1] :
( l1_rlvect_1(X1)
=> l2_struct_0(X1) ),
file('/tmp/tmpsY844r/sel_ALG216+2.p_1',dt_l1_rlvect_1) ).
fof(1376,axiom,
! [X1] :
( l1_struct_0(X1)
=> ! [X2] :
( l1_vectsp_2(X2,X1)
=> l1_rlvect_1(X2) ) ),
file('/tmp/tmpsY844r/sel_ALG216+2.p_1',dt_l1_vectsp_2) ).
fof(1460,axiom,
! [X1,X2] :
( r2_hidden(X1,X2)
=> m1_subset_1(X1,X2) ),
file('/tmp/tmpsY844r/sel_ALG216+2.p_1',t1_subset) ).
fof(1467,axiom,
! [X1] :
( l1_struct_0(X1)
=> ! [X2] :
( r1_rlvect_1(X1,X2)
<=> r2_hidden(X2,u1_struct_0(X1)) ) ),
file('/tmp/tmpsY844r/sel_ALG216+2.p_1',d1_rlvect_1) ).
fof(1772,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v4_group_1(X1)
& v6_vectsp_1(X1)
& v7_vectsp_1(X1)
& v8_vectsp_1(X1)
& l3_vectsp_1(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v3_rlvect_1(X2)
& v4_rlvect_1(X2)
& v5_rlvect_1(X2)
& v6_rlvect_1(X2)
& v5_vectsp_2(X2,X1)
& l1_vectsp_2(X2,X1) )
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X2))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X2))
=> ( v1_rmod_5(k8_rlvect_2(X2,X3,X4),X1,X2)
=> ( k1_rlvect_1(X1) = k2_group_1(X1)
| ( X3 != k1_rlvect_1(X2)
& X4 != k1_rlvect_1(X2) ) ) ) ) ) ) ),
file('/tmp/tmpsY844r/sel_ALG216+2.p_1',t5_rmod_5) ).
fof(1774,conjecture,
! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v4_group_1(X1)
& v6_vectsp_1(X1)
& v7_vectsp_1(X1)
& v8_vectsp_1(X1)
& l3_vectsp_1(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v3_rlvect_1(X2)
& v4_rlvect_1(X2)
& v5_rlvect_1(X2)
& v6_rlvect_1(X2)
& v5_vectsp_2(X2,X1)
& l1_vectsp_2(X2,X1) )
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X2))
=> ( k1_rlvect_1(X1) != k2_group_1(X1)
=> ( ~ v1_rmod_5(k8_rlvect_2(X2,X3,k1_rlvect_1(X2)),X1,X2)
& ~ v1_rmod_5(k8_rlvect_2(X2,k1_rlvect_1(X2),X3),X1,X2) ) ) ) ) ),
file('/tmp/tmpsY844r/sel_ALG216+2.p_1',t6_rmod_5) ).
fof(1777,negated_conjecture,
~ ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v4_group_1(X1)
& v6_vectsp_1(X1)
& v7_vectsp_1(X1)
& v8_vectsp_1(X1)
& l3_vectsp_1(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v3_rlvect_1(X2)
& v4_rlvect_1(X2)
& v5_rlvect_1(X2)
& v6_rlvect_1(X2)
& v5_vectsp_2(X2,X1)
& l1_vectsp_2(X2,X1) )
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X2))
=> ( k1_rlvect_1(X1) != k2_group_1(X1)
=> ( ~ v1_rmod_5(k8_rlvect_2(X2,X3,k1_rlvect_1(X2)),X1,X2)
& ~ v1_rmod_5(k8_rlvect_2(X2,k1_rlvect_1(X2),X3),X1,X2) ) ) ) ) ),
inference(assume_negation,[status(cth)],[1774]) ).
fof(1861,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v4_group_1(X1)
& v6_vectsp_1(X1)
& v7_vectsp_1(X1)
& v8_vectsp_1(X1)
& l3_vectsp_1(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v3_rlvect_1(X2)
& v4_rlvect_1(X2)
& v5_rlvect_1(X2)
& v6_rlvect_1(X2)
& v5_vectsp_2(X2,X1)
& l1_vectsp_2(X2,X1) )
=> ! [X3] :
( m1_rmod_2(X3,X1,X2)
=> r1_rlvect_1(X3,k1_rlvect_1(X2)) ) ) ),
inference(fof_simplification,[status(thm)],[303,theory(equality)]) ).
fof(1897,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v4_group_1(X1)
& v6_vectsp_1(X1)
& v7_vectsp_1(X1)
& v8_vectsp_1(X1)
& l3_vectsp_1(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v3_rlvect_1(X2)
& v4_rlvect_1(X2)
& v5_rlvect_1(X2)
& v6_rlvect_1(X2)
& v5_vectsp_2(X2,X1)
& l1_vectsp_2(X2,X1) )
=> m1_rmod_2(X2,X1,X2) ) ),
inference(fof_simplification,[status(thm)],[400,theory(equality)]) ).
fof(2260,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v4_group_1(X1)
& v6_vectsp_1(X1)
& v7_vectsp_1(X1)
& v8_vectsp_1(X1)
& l3_vectsp_1(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v3_rlvect_1(X2)
& v4_rlvect_1(X2)
& v5_rlvect_1(X2)
& v6_rlvect_1(X2)
& v5_vectsp_2(X2,X1)
& l1_vectsp_2(X2,X1) )
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X2))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X2))
=> ( v1_rmod_5(k8_rlvect_2(X2,X3,X4),X1,X2)
=> ( k1_rlvect_1(X1) = k2_group_1(X1)
| ( X3 != k1_rlvect_1(X2)
& X4 != k1_rlvect_1(X2) ) ) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[1772,theory(equality)]) ).
fof(2262,negated_conjecture,
~ ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v4_group_1(X1)
& v6_vectsp_1(X1)
& v7_vectsp_1(X1)
& v8_vectsp_1(X1)
& l3_vectsp_1(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v3_rlvect_1(X2)
& v4_rlvect_1(X2)
& v5_rlvect_1(X2)
& v6_rlvect_1(X2)
& v5_vectsp_2(X2,X1)
& l1_vectsp_2(X2,X1) )
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X2))
=> ( k1_rlvect_1(X1) != k2_group_1(X1)
=> ( ~ v1_rmod_5(k8_rlvect_2(X2,X3,k1_rlvect_1(X2)),X1,X2)
& ~ v1_rmod_5(k8_rlvect_2(X2,k1_rlvect_1(X2),X3),X1,X2) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[1777,theory(equality)]) ).
fof(2780,plain,
! [X1] :
( ~ l2_struct_0(X1)
| l1_struct_0(X1) ),
inference(fof_nnf,[status(thm)],[159]) ).
fof(2781,plain,
! [X2] :
( ~ l2_struct_0(X2)
| l1_struct_0(X2) ),
inference(variable_rename,[status(thm)],[2780]) ).
cnf(2782,plain,
( l1_struct_0(X1)
| ~ l2_struct_0(X1) ),
inference(split_conjunct,[status(thm)],[2781]) ).
fof(3231,plain,
! [X1] :
( v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ! [X2] :
( v3_struct_0(X2)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X2)
| ~ v5_vectsp_2(X2,X1)
| ~ l1_vectsp_2(X2,X1)
| ! [X3] :
( ~ m1_rmod_2(X3,X1,X2)
| r1_rlvect_1(X3,k1_rlvect_1(X2)) ) ) ),
inference(fof_nnf,[status(thm)],[1861]) ).
fof(3232,plain,
! [X4] :
( v3_struct_0(X4)
| ~ v3_rlvect_1(X4)
| ~ v4_rlvect_1(X4)
| ~ v5_rlvect_1(X4)
| ~ v6_rlvect_1(X4)
| ~ v4_group_1(X4)
| ~ v6_vectsp_1(X4)
| ~ v7_vectsp_1(X4)
| ~ v8_vectsp_1(X4)
| ~ l3_vectsp_1(X4)
| ! [X5] :
( v3_struct_0(X5)
| ~ v3_rlvect_1(X5)
| ~ v4_rlvect_1(X5)
| ~ v5_rlvect_1(X5)
| ~ v6_rlvect_1(X5)
| ~ v5_vectsp_2(X5,X4)
| ~ l1_vectsp_2(X5,X4)
| ! [X6] :
( ~ m1_rmod_2(X6,X4,X5)
| r1_rlvect_1(X6,k1_rlvect_1(X5)) ) ) ),
inference(variable_rename,[status(thm)],[3231]) ).
fof(3233,plain,
! [X4,X5,X6] :
( ~ m1_rmod_2(X6,X4,X5)
| r1_rlvect_1(X6,k1_rlvect_1(X5))
| v3_struct_0(X5)
| ~ v3_rlvect_1(X5)
| ~ v4_rlvect_1(X5)
| ~ v5_rlvect_1(X5)
| ~ v6_rlvect_1(X5)
| ~ v5_vectsp_2(X5,X4)
| ~ l1_vectsp_2(X5,X4)
| v3_struct_0(X4)
| ~ v3_rlvect_1(X4)
| ~ v4_rlvect_1(X4)
| ~ v5_rlvect_1(X4)
| ~ v6_rlvect_1(X4)
| ~ v4_group_1(X4)
| ~ v6_vectsp_1(X4)
| ~ v7_vectsp_1(X4)
| ~ v8_vectsp_1(X4)
| ~ l3_vectsp_1(X4) ),
inference(shift_quantors,[status(thm)],[3232]) ).
cnf(3234,plain,
( v3_struct_0(X1)
| v3_struct_0(X2)
| r1_rlvect_1(X3,k1_rlvect_1(X2))
| ~ l3_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v4_group_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v3_rlvect_1(X1)
| ~ l1_vectsp_2(X2,X1)
| ~ v5_vectsp_2(X2,X1)
| ~ v6_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v3_rlvect_1(X2)
| ~ m1_rmod_2(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[3233]) ).
fof(3626,plain,
! [X1] :
( v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ! [X2] :
( v3_struct_0(X2)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X2)
| ~ v5_vectsp_2(X2,X1)
| ~ l1_vectsp_2(X2,X1)
| m1_rmod_2(X2,X1,X2) ) ),
inference(fof_nnf,[status(thm)],[1897]) ).
fof(3627,plain,
! [X3] :
( v3_struct_0(X3)
| ~ v3_rlvect_1(X3)
| ~ v4_rlvect_1(X3)
| ~ v5_rlvect_1(X3)
| ~ v6_rlvect_1(X3)
| ~ v4_group_1(X3)
| ~ v6_vectsp_1(X3)
| ~ v7_vectsp_1(X3)
| ~ v8_vectsp_1(X3)
| ~ l3_vectsp_1(X3)
| ! [X4] :
( v3_struct_0(X4)
| ~ v3_rlvect_1(X4)
| ~ v4_rlvect_1(X4)
| ~ v5_rlvect_1(X4)
| ~ v6_rlvect_1(X4)
| ~ v5_vectsp_2(X4,X3)
| ~ l1_vectsp_2(X4,X3)
| m1_rmod_2(X4,X3,X4) ) ),
inference(variable_rename,[status(thm)],[3626]) ).
fof(3628,plain,
! [X3,X4] :
( v3_struct_0(X4)
| ~ v3_rlvect_1(X4)
| ~ v4_rlvect_1(X4)
| ~ v5_rlvect_1(X4)
| ~ v6_rlvect_1(X4)
| ~ v5_vectsp_2(X4,X3)
| ~ l1_vectsp_2(X4,X3)
| m1_rmod_2(X4,X3,X4)
| v3_struct_0(X3)
| ~ v3_rlvect_1(X3)
| ~ v4_rlvect_1(X3)
| ~ v5_rlvect_1(X3)
| ~ v6_rlvect_1(X3)
| ~ v4_group_1(X3)
| ~ v6_vectsp_1(X3)
| ~ v7_vectsp_1(X3)
| ~ v8_vectsp_1(X3)
| ~ l3_vectsp_1(X3) ),
inference(shift_quantors,[status(thm)],[3627]) ).
cnf(3629,plain,
( v3_struct_0(X1)
| m1_rmod_2(X2,X1,X2)
| v3_struct_0(X2)
| ~ l3_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v4_group_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v3_rlvect_1(X1)
| ~ l1_vectsp_2(X2,X1)
| ~ v5_vectsp_2(X2,X1)
| ~ v6_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v3_rlvect_1(X2) ),
inference(split_conjunct,[status(thm)],[3628]) ).
fof(3793,plain,
! [X1] :
( ~ l3_vectsp_1(X1)
| ( l1_rlvect_1(X1)
& l2_vectsp_1(X1) ) ),
inference(fof_nnf,[status(thm)],[449]) ).
fof(3794,plain,
! [X2] :
( ~ l3_vectsp_1(X2)
| ( l1_rlvect_1(X2)
& l2_vectsp_1(X2) ) ),
inference(variable_rename,[status(thm)],[3793]) ).
fof(3795,plain,
! [X2] :
( ( l1_rlvect_1(X2)
| ~ l3_vectsp_1(X2) )
& ( l2_vectsp_1(X2)
| ~ l3_vectsp_1(X2) ) ),
inference(distribute,[status(thm)],[3794]) ).
cnf(3797,plain,
( l1_rlvect_1(X1)
| ~ l3_vectsp_1(X1) ),
inference(split_conjunct,[status(thm)],[3795]) ).
fof(5595,plain,
! [X1] :
( ~ l1_rlvect_1(X1)
| l2_struct_0(X1) ),
inference(fof_nnf,[status(thm)],[1037]) ).
fof(5596,plain,
! [X2] :
( ~ l1_rlvect_1(X2)
| l2_struct_0(X2) ),
inference(variable_rename,[status(thm)],[5595]) ).
cnf(5597,plain,
( l2_struct_0(X1)
| ~ l1_rlvect_1(X1) ),
inference(split_conjunct,[status(thm)],[5596]) ).
fof(6685,plain,
! [X1] :
( ~ l1_struct_0(X1)
| ! [X2] :
( ~ l1_vectsp_2(X2,X1)
| l1_rlvect_1(X2) ) ),
inference(fof_nnf,[status(thm)],[1376]) ).
fof(6686,plain,
! [X3] :
( ~ l1_struct_0(X3)
| ! [X4] :
( ~ l1_vectsp_2(X4,X3)
| l1_rlvect_1(X4) ) ),
inference(variable_rename,[status(thm)],[6685]) ).
fof(6687,plain,
! [X3,X4] :
( ~ l1_vectsp_2(X4,X3)
| l1_rlvect_1(X4)
| ~ l1_struct_0(X3) ),
inference(shift_quantors,[status(thm)],[6686]) ).
cnf(6688,plain,
( l1_rlvect_1(X2)
| ~ l1_struct_0(X1)
| ~ l1_vectsp_2(X2,X1) ),
inference(split_conjunct,[status(thm)],[6687]) ).
fof(6921,plain,
! [X1,X2] :
( ~ r2_hidden(X1,X2)
| m1_subset_1(X1,X2) ),
inference(fof_nnf,[status(thm)],[1460]) ).
fof(6922,plain,
! [X3,X4] :
( ~ r2_hidden(X3,X4)
| m1_subset_1(X3,X4) ),
inference(variable_rename,[status(thm)],[6921]) ).
cnf(6923,plain,
( m1_subset_1(X1,X2)
| ~ r2_hidden(X1,X2) ),
inference(split_conjunct,[status(thm)],[6922]) ).
fof(6944,plain,
! [X1] :
( ~ l1_struct_0(X1)
| ! [X2] :
( ( ~ r1_rlvect_1(X1,X2)
| r2_hidden(X2,u1_struct_0(X1)) )
& ( ~ r2_hidden(X2,u1_struct_0(X1))
| r1_rlvect_1(X1,X2) ) ) ),
inference(fof_nnf,[status(thm)],[1467]) ).
fof(6945,plain,
! [X3] :
( ~ l1_struct_0(X3)
| ! [X4] :
( ( ~ r1_rlvect_1(X3,X4)
| r2_hidden(X4,u1_struct_0(X3)) )
& ( ~ r2_hidden(X4,u1_struct_0(X3))
| r1_rlvect_1(X3,X4) ) ) ),
inference(variable_rename,[status(thm)],[6944]) ).
fof(6946,plain,
! [X3,X4] :
( ( ( ~ r1_rlvect_1(X3,X4)
| r2_hidden(X4,u1_struct_0(X3)) )
& ( ~ r2_hidden(X4,u1_struct_0(X3))
| r1_rlvect_1(X3,X4) ) )
| ~ l1_struct_0(X3) ),
inference(shift_quantors,[status(thm)],[6945]) ).
fof(6947,plain,
! [X3,X4] :
( ( ~ r1_rlvect_1(X3,X4)
| r2_hidden(X4,u1_struct_0(X3))
| ~ l1_struct_0(X3) )
& ( ~ r2_hidden(X4,u1_struct_0(X3))
| r1_rlvect_1(X3,X4)
| ~ l1_struct_0(X3) ) ),
inference(distribute,[status(thm)],[6946]) ).
cnf(6949,plain,
( r2_hidden(X2,u1_struct_0(X1))
| ~ l1_struct_0(X1)
| ~ r1_rlvect_1(X1,X2) ),
inference(split_conjunct,[status(thm)],[6947]) ).
fof(7896,plain,
! [X1] :
( v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ! [X2] :
( v3_struct_0(X2)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X2)
| ~ v5_vectsp_2(X2,X1)
| ~ l1_vectsp_2(X2,X1)
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X2))
| ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(X2))
| ~ v1_rmod_5(k8_rlvect_2(X2,X3,X4),X1,X2)
| k1_rlvect_1(X1) = k2_group_1(X1)
| ( X3 != k1_rlvect_1(X2)
& X4 != k1_rlvect_1(X2) ) ) ) ) ),
inference(fof_nnf,[status(thm)],[2260]) ).
fof(7897,plain,
! [X5] :
( v3_struct_0(X5)
| ~ v3_rlvect_1(X5)
| ~ v4_rlvect_1(X5)
| ~ v5_rlvect_1(X5)
| ~ v6_rlvect_1(X5)
| ~ v4_group_1(X5)
| ~ v6_vectsp_1(X5)
| ~ v7_vectsp_1(X5)
| ~ v8_vectsp_1(X5)
| ~ l3_vectsp_1(X5)
| ! [X6] :
( v3_struct_0(X6)
| ~ v3_rlvect_1(X6)
| ~ v4_rlvect_1(X6)
| ~ v5_rlvect_1(X6)
| ~ v6_rlvect_1(X6)
| ~ v5_vectsp_2(X6,X5)
| ~ l1_vectsp_2(X6,X5)
| ! [X7] :
( ~ m1_subset_1(X7,u1_struct_0(X6))
| ! [X8] :
( ~ m1_subset_1(X8,u1_struct_0(X6))
| ~ v1_rmod_5(k8_rlvect_2(X6,X7,X8),X5,X6)
| k1_rlvect_1(X5) = k2_group_1(X5)
| ( X7 != k1_rlvect_1(X6)
& X8 != k1_rlvect_1(X6) ) ) ) ) ),
inference(variable_rename,[status(thm)],[7896]) ).
fof(7898,plain,
! [X5,X6,X7,X8] :
( ~ m1_subset_1(X8,u1_struct_0(X6))
| ~ v1_rmod_5(k8_rlvect_2(X6,X7,X8),X5,X6)
| k1_rlvect_1(X5) = k2_group_1(X5)
| ( X7 != k1_rlvect_1(X6)
& X8 != k1_rlvect_1(X6) )
| ~ m1_subset_1(X7,u1_struct_0(X6))
| v3_struct_0(X6)
| ~ v3_rlvect_1(X6)
| ~ v4_rlvect_1(X6)
| ~ v5_rlvect_1(X6)
| ~ v6_rlvect_1(X6)
| ~ v5_vectsp_2(X6,X5)
| ~ l1_vectsp_2(X6,X5)
| v3_struct_0(X5)
| ~ v3_rlvect_1(X5)
| ~ v4_rlvect_1(X5)
| ~ v5_rlvect_1(X5)
| ~ v6_rlvect_1(X5)
| ~ v4_group_1(X5)
| ~ v6_vectsp_1(X5)
| ~ v7_vectsp_1(X5)
| ~ v8_vectsp_1(X5)
| ~ l3_vectsp_1(X5) ),
inference(shift_quantors,[status(thm)],[7897]) ).
fof(7899,plain,
! [X5,X6,X7,X8] :
( ( X7 != k1_rlvect_1(X6)
| k1_rlvect_1(X5) = k2_group_1(X5)
| ~ v1_rmod_5(k8_rlvect_2(X6,X7,X8),X5,X6)
| ~ m1_subset_1(X8,u1_struct_0(X6))
| ~ m1_subset_1(X7,u1_struct_0(X6))
| v3_struct_0(X6)
| ~ v3_rlvect_1(X6)
| ~ v4_rlvect_1(X6)
| ~ v5_rlvect_1(X6)
| ~ v6_rlvect_1(X6)
| ~ v5_vectsp_2(X6,X5)
| ~ l1_vectsp_2(X6,X5)
| v3_struct_0(X5)
| ~ v3_rlvect_1(X5)
| ~ v4_rlvect_1(X5)
| ~ v5_rlvect_1(X5)
| ~ v6_rlvect_1(X5)
| ~ v4_group_1(X5)
| ~ v6_vectsp_1(X5)
| ~ v7_vectsp_1(X5)
| ~ v8_vectsp_1(X5)
| ~ l3_vectsp_1(X5) )
& ( X8 != k1_rlvect_1(X6)
| k1_rlvect_1(X5) = k2_group_1(X5)
| ~ v1_rmod_5(k8_rlvect_2(X6,X7,X8),X5,X6)
| ~ m1_subset_1(X8,u1_struct_0(X6))
| ~ m1_subset_1(X7,u1_struct_0(X6))
| v3_struct_0(X6)
| ~ v3_rlvect_1(X6)
| ~ v4_rlvect_1(X6)
| ~ v5_rlvect_1(X6)
| ~ v6_rlvect_1(X6)
| ~ v5_vectsp_2(X6,X5)
| ~ l1_vectsp_2(X6,X5)
| v3_struct_0(X5)
| ~ v3_rlvect_1(X5)
| ~ v4_rlvect_1(X5)
| ~ v5_rlvect_1(X5)
| ~ v6_rlvect_1(X5)
| ~ v4_group_1(X5)
| ~ v6_vectsp_1(X5)
| ~ v7_vectsp_1(X5)
| ~ v8_vectsp_1(X5)
| ~ l3_vectsp_1(X5) ) ),
inference(distribute,[status(thm)],[7898]) ).
cnf(7900,plain,
( v3_struct_0(X1)
| v3_struct_0(X2)
| k1_rlvect_1(X1) = k2_group_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v4_group_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v3_rlvect_1(X1)
| ~ l1_vectsp_2(X2,X1)
| ~ v5_vectsp_2(X2,X1)
| ~ v6_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v3_rlvect_1(X2)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ m1_subset_1(X4,u1_struct_0(X2))
| ~ v1_rmod_5(k8_rlvect_2(X2,X3,X4),X1,X2)
| X4 != k1_rlvect_1(X2) ),
inference(split_conjunct,[status(thm)],[7899]) ).
cnf(7901,plain,
( v3_struct_0(X1)
| v3_struct_0(X2)
| k1_rlvect_1(X1) = k2_group_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v4_group_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v3_rlvect_1(X1)
| ~ l1_vectsp_2(X2,X1)
| ~ v5_vectsp_2(X2,X1)
| ~ v6_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v3_rlvect_1(X2)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ m1_subset_1(X4,u1_struct_0(X2))
| ~ v1_rmod_5(k8_rlvect_2(X2,X3,X4),X1,X2)
| X3 != k1_rlvect_1(X2) ),
inference(split_conjunct,[status(thm)],[7899]) ).
fof(7906,negated_conjecture,
? [X1] :
( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v4_group_1(X1)
& v6_vectsp_1(X1)
& v7_vectsp_1(X1)
& v8_vectsp_1(X1)
& l3_vectsp_1(X1)
& ? [X2] :
( ~ v3_struct_0(X2)
& v3_rlvect_1(X2)
& v4_rlvect_1(X2)
& v5_rlvect_1(X2)
& v6_rlvect_1(X2)
& v5_vectsp_2(X2,X1)
& l1_vectsp_2(X2,X1)
& ? [X3] :
( m1_subset_1(X3,u1_struct_0(X2))
& k1_rlvect_1(X1) != k2_group_1(X1)
& ( v1_rmod_5(k8_rlvect_2(X2,X3,k1_rlvect_1(X2)),X1,X2)
| v1_rmod_5(k8_rlvect_2(X2,k1_rlvect_1(X2),X3),X1,X2) ) ) ) ),
inference(fof_nnf,[status(thm)],[2262]) ).
fof(7907,negated_conjecture,
? [X4] :
( ~ v3_struct_0(X4)
& v3_rlvect_1(X4)
& v4_rlvect_1(X4)
& v5_rlvect_1(X4)
& v6_rlvect_1(X4)
& v4_group_1(X4)
& v6_vectsp_1(X4)
& v7_vectsp_1(X4)
& v8_vectsp_1(X4)
& l3_vectsp_1(X4)
& ? [X5] :
( ~ v3_struct_0(X5)
& v3_rlvect_1(X5)
& v4_rlvect_1(X5)
& v5_rlvect_1(X5)
& v6_rlvect_1(X5)
& v5_vectsp_2(X5,X4)
& l1_vectsp_2(X5,X4)
& ? [X6] :
( m1_subset_1(X6,u1_struct_0(X5))
& k1_rlvect_1(X4) != k2_group_1(X4)
& ( v1_rmod_5(k8_rlvect_2(X5,X6,k1_rlvect_1(X5)),X4,X5)
| v1_rmod_5(k8_rlvect_2(X5,k1_rlvect_1(X5),X6),X4,X5) ) ) ) ),
inference(variable_rename,[status(thm)],[7906]) ).
fof(7908,negated_conjecture,
( ~ v3_struct_0(esk293_0)
& v3_rlvect_1(esk293_0)
& v4_rlvect_1(esk293_0)
& v5_rlvect_1(esk293_0)
& v6_rlvect_1(esk293_0)
& v4_group_1(esk293_0)
& v6_vectsp_1(esk293_0)
& v7_vectsp_1(esk293_0)
& v8_vectsp_1(esk293_0)
& l3_vectsp_1(esk293_0)
& ~ v3_struct_0(esk294_0)
& v3_rlvect_1(esk294_0)
& v4_rlvect_1(esk294_0)
& v5_rlvect_1(esk294_0)
& v6_rlvect_1(esk294_0)
& v5_vectsp_2(esk294_0,esk293_0)
& l1_vectsp_2(esk294_0,esk293_0)
& m1_subset_1(esk295_0,u1_struct_0(esk294_0))
& k1_rlvect_1(esk293_0) != k2_group_1(esk293_0)
& ( v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,k1_rlvect_1(esk294_0),esk295_0),esk293_0,esk294_0) ) ),
inference(skolemize,[status(esa)],[7907]) ).
cnf(7909,negated_conjecture,
( v1_rmod_5(k8_rlvect_2(esk294_0,k1_rlvect_1(esk294_0),esk295_0),esk293_0,esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0) ),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(7910,negated_conjecture,
k1_rlvect_1(esk293_0) != k2_group_1(esk293_0),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(7911,negated_conjecture,
m1_subset_1(esk295_0,u1_struct_0(esk294_0)),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(7912,negated_conjecture,
l1_vectsp_2(esk294_0,esk293_0),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(7913,negated_conjecture,
v5_vectsp_2(esk294_0,esk293_0),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(7914,negated_conjecture,
v6_rlvect_1(esk294_0),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(7915,negated_conjecture,
v5_rlvect_1(esk294_0),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(7916,negated_conjecture,
v4_rlvect_1(esk294_0),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(7917,negated_conjecture,
v3_rlvect_1(esk294_0),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(7918,negated_conjecture,
~ v3_struct_0(esk294_0),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(7919,negated_conjecture,
l3_vectsp_1(esk293_0),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(7920,negated_conjecture,
v8_vectsp_1(esk293_0),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(7921,negated_conjecture,
v7_vectsp_1(esk293_0),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(7922,negated_conjecture,
v6_vectsp_1(esk293_0),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(7923,negated_conjecture,
v4_group_1(esk293_0),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(7924,negated_conjecture,
v6_rlvect_1(esk293_0),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(7925,negated_conjecture,
v5_rlvect_1(esk293_0),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(7926,negated_conjecture,
v4_rlvect_1(esk293_0),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(7927,negated_conjecture,
v3_rlvect_1(esk293_0),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(7928,negated_conjecture,
~ v3_struct_0(esk293_0),
inference(split_conjunct,[status(thm)],[7908]) ).
cnf(8396,plain,
( l1_struct_0(X1)
| ~ l1_rlvect_1(X1) ),
inference(spm,[status(thm)],[2782,5597,theory(equality)]) ).
cnf(8503,negated_conjecture,
( l1_rlvect_1(esk294_0)
| ~ l1_struct_0(esk293_0) ),
inference(spm,[status(thm)],[6688,7912,theory(equality)]) ).
cnf(32907,negated_conjecture,
( m1_rmod_2(esk294_0,esk293_0,esk294_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| ~ l3_vectsp_1(esk293_0)
| ~ v8_vectsp_1(esk293_0)
| ~ v7_vectsp_1(esk293_0)
| ~ v6_vectsp_1(esk293_0)
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(spm,[status(thm)],[3629,7913,theory(equality)]) ).
cnf(32909,negated_conjecture,
( m1_rmod_2(esk294_0,esk293_0,esk294_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| ~ v8_vectsp_1(esk293_0)
| ~ v7_vectsp_1(esk293_0)
| ~ v6_vectsp_1(esk293_0)
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[32907,7919,theory(equality)]) ).
cnf(32910,negated_conjecture,
( m1_rmod_2(esk294_0,esk293_0,esk294_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| ~ v7_vectsp_1(esk293_0)
| ~ v6_vectsp_1(esk293_0)
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[32909,7920,theory(equality)]) ).
cnf(32911,negated_conjecture,
( m1_rmod_2(esk294_0,esk293_0,esk294_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| ~ v6_vectsp_1(esk293_0)
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[32910,7921,theory(equality)]) ).
cnf(32912,negated_conjecture,
( m1_rmod_2(esk294_0,esk293_0,esk294_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[32911,7922,theory(equality)]) ).
cnf(32913,negated_conjecture,
( m1_rmod_2(esk294_0,esk293_0,esk294_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[32912,7923,theory(equality)]) ).
cnf(32914,negated_conjecture,
( m1_rmod_2(esk294_0,esk293_0,esk294_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[32913,7912,theory(equality)]) ).
cnf(32915,negated_conjecture,
( m1_rmod_2(esk294_0,esk293_0,esk294_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[32914,7914,theory(equality)]) ).
cnf(32916,negated_conjecture,
( m1_rmod_2(esk294_0,esk293_0,esk294_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[32915,7924,theory(equality)]) ).
cnf(32917,negated_conjecture,
( m1_rmod_2(esk294_0,esk293_0,esk294_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[32916,7915,theory(equality)]) ).
cnf(32918,negated_conjecture,
( m1_rmod_2(esk294_0,esk293_0,esk294_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[32917,7925,theory(equality)]) ).
cnf(32919,negated_conjecture,
( m1_rmod_2(esk294_0,esk293_0,esk294_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[32918,7916,theory(equality)]) ).
cnf(32920,negated_conjecture,
( m1_rmod_2(esk294_0,esk293_0,esk294_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[32919,7926,theory(equality)]) ).
cnf(32921,negated_conjecture,
( m1_rmod_2(esk294_0,esk293_0,esk294_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[32920,7917,theory(equality)]) ).
cnf(32922,negated_conjecture,
( m1_rmod_2(esk294_0,esk293_0,esk294_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[32921,7927,theory(equality)]) ).
cnf(32923,negated_conjecture,
( m1_rmod_2(esk294_0,esk293_0,esk294_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0) ),
inference(cn,[status(thm)],[32922,theory(equality)]) ).
cnf(32924,negated_conjecture,
( m1_rmod_2(esk294_0,esk293_0,esk294_0)
| v3_struct_0(esk294_0) ),
inference(sr,[status(thm)],[32923,7928,theory(equality)]) ).
cnf(32925,negated_conjecture,
m1_rmod_2(esk294_0,esk293_0,esk294_0),
inference(sr,[status(thm)],[32924,7918,theory(equality)]) ).
cnf(41386,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| ~ v5_vectsp_2(esk294_0,esk293_0)
| ~ l3_vectsp_1(esk293_0)
| ~ v8_vectsp_1(esk293_0)
| ~ v7_vectsp_1(esk293_0)
| ~ v6_vectsp_1(esk293_0)
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ m1_subset_1(esk295_0,u1_struct_0(esk294_0))
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(spm,[status(thm)],[7901,7909,theory(equality)]) ).
cnf(41393,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| $false
| ~ l3_vectsp_1(esk293_0)
| ~ v8_vectsp_1(esk293_0)
| ~ v7_vectsp_1(esk293_0)
| ~ v6_vectsp_1(esk293_0)
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ m1_subset_1(esk295_0,u1_struct_0(esk294_0))
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[41386,7913,theory(equality)]) ).
cnf(41394,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| $false
| $false
| ~ v8_vectsp_1(esk293_0)
| ~ v7_vectsp_1(esk293_0)
| ~ v6_vectsp_1(esk293_0)
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ m1_subset_1(esk295_0,u1_struct_0(esk294_0))
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[41393,7919,theory(equality)]) ).
cnf(41395,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| $false
| $false
| $false
| ~ v7_vectsp_1(esk293_0)
| ~ v6_vectsp_1(esk293_0)
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ m1_subset_1(esk295_0,u1_struct_0(esk294_0))
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[41394,7920,theory(equality)]) ).
cnf(41396,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| $false
| $false
| $false
| $false
| ~ v6_vectsp_1(esk293_0)
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ m1_subset_1(esk295_0,u1_struct_0(esk294_0))
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[41395,7921,theory(equality)]) ).
cnf(41397,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| $false
| $false
| $false
| $false
| $false
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ m1_subset_1(esk295_0,u1_struct_0(esk294_0))
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[41396,7922,theory(equality)]) ).
cnf(41398,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ m1_subset_1(esk295_0,u1_struct_0(esk294_0))
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[41397,7923,theory(equality)]) ).
cnf(41399,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(esk295_0,u1_struct_0(esk294_0))
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[41398,7912,theory(equality)]) ).
cnf(41400,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[41399,7911,theory(equality)]) ).
cnf(41401,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| $false
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[41400,7914,theory(equality)]) ).
cnf(41402,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| $false
| $false
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[41401,7924,theory(equality)]) ).
cnf(41403,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| $false
| $false
| $false
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[41402,7915,theory(equality)]) ).
cnf(41404,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| $false
| $false
| $false
| $false
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[41403,7925,theory(equality)]) ).
cnf(41405,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| $false
| $false
| $false
| $false
| $false
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[41404,7916,theory(equality)]) ).
cnf(41406,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[41405,7926,theory(equality)]) ).
cnf(41407,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[41406,7917,theory(equality)]) ).
cnf(41408,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[41407,7927,theory(equality)]) ).
cnf(41409,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0)) ),
inference(cn,[status(thm)],[41408,theory(equality)]) ).
cnf(41410,negated_conjecture,
( v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0)) ),
inference(sr,[status(thm)],[41409,7910,theory(equality)]) ).
cnf(41411,negated_conjecture,
( v3_struct_0(esk294_0)
| v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0)) ),
inference(sr,[status(thm)],[41410,7928,theory(equality)]) ).
cnf(41412,negated_conjecture,
( v1_rmod_5(k8_rlvect_2(esk294_0,esk295_0,k1_rlvect_1(esk294_0)),esk293_0,esk294_0)
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0)) ),
inference(sr,[status(thm)],[41411,7918,theory(equality)]) ).
cnf(51943,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| ~ v5_vectsp_2(esk294_0,esk293_0)
| ~ l3_vectsp_1(esk293_0)
| ~ v8_vectsp_1(esk293_0)
| ~ v7_vectsp_1(esk293_0)
| ~ v6_vectsp_1(esk293_0)
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ m1_subset_1(esk295_0,u1_struct_0(esk294_0))
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(spm,[status(thm)],[7900,41412,theory(equality)]) ).
cnf(51968,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| ~ l3_vectsp_1(esk293_0)
| ~ v8_vectsp_1(esk293_0)
| ~ v7_vectsp_1(esk293_0)
| ~ v6_vectsp_1(esk293_0)
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ m1_subset_1(esk295_0,u1_struct_0(esk294_0))
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[51943,7913,theory(equality)]) ).
cnf(51969,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| ~ v8_vectsp_1(esk293_0)
| ~ v7_vectsp_1(esk293_0)
| ~ v6_vectsp_1(esk293_0)
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ m1_subset_1(esk295_0,u1_struct_0(esk294_0))
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[51968,7919,theory(equality)]) ).
cnf(51970,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| ~ v7_vectsp_1(esk293_0)
| ~ v6_vectsp_1(esk293_0)
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ m1_subset_1(esk295_0,u1_struct_0(esk294_0))
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[51969,7920,theory(equality)]) ).
cnf(51971,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| ~ v6_vectsp_1(esk293_0)
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ m1_subset_1(esk295_0,u1_struct_0(esk294_0))
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[51970,7921,theory(equality)]) ).
cnf(51972,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ m1_subset_1(esk295_0,u1_struct_0(esk294_0))
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[51971,7922,theory(equality)]) ).
cnf(51973,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ m1_subset_1(esk295_0,u1_struct_0(esk294_0))
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[51972,7923,theory(equality)]) ).
cnf(51974,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ m1_subset_1(esk295_0,u1_struct_0(esk294_0))
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[51973,7912,theory(equality)]) ).
cnf(51975,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| $false
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[51974,7911,theory(equality)]) ).
cnf(51976,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| $false
| $false
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[51975,7914,theory(equality)]) ).
cnf(51977,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| $false
| $false
| $false
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[51976,7924,theory(equality)]) ).
cnf(51978,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| $false
| $false
| $false
| $false
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[51977,7915,theory(equality)]) ).
cnf(51979,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| $false
| $false
| $false
| $false
| $false
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[51978,7925,theory(equality)]) ).
cnf(51980,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[51979,7916,theory(equality)]) ).
cnf(51981,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[51980,7926,theory(equality)]) ).
cnf(51982,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[51981,7917,theory(equality)]) ).
cnf(51983,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[51982,7927,theory(equality)]) ).
cnf(51984,negated_conjecture,
( k2_group_1(esk293_0) = k1_rlvect_1(esk293_0)
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0)) ),
inference(cn,[status(thm)],[51983,theory(equality)]) ).
cnf(51985,negated_conjecture,
( v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0)) ),
inference(sr,[status(thm)],[51984,7910,theory(equality)]) ).
cnf(51986,negated_conjecture,
( v3_struct_0(esk294_0)
| ~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0)) ),
inference(sr,[status(thm)],[51985,7928,theory(equality)]) ).
cnf(51987,negated_conjecture,
~ m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0)),
inference(sr,[status(thm)],[51986,7918,theory(equality)]) ).
cnf(52037,negated_conjecture,
( r1_rlvect_1(esk294_0,k1_rlvect_1(esk294_0))
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| ~ v5_vectsp_2(esk294_0,esk293_0)
| ~ l3_vectsp_1(esk293_0)
| ~ v8_vectsp_1(esk293_0)
| ~ v7_vectsp_1(esk293_0)
| ~ v6_vectsp_1(esk293_0)
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(spm,[status(thm)],[3234,32925,theory(equality)]) ).
cnf(52167,negated_conjecture,
( r1_rlvect_1(esk294_0,k1_rlvect_1(esk294_0))
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| ~ l3_vectsp_1(esk293_0)
| ~ v8_vectsp_1(esk293_0)
| ~ v7_vectsp_1(esk293_0)
| ~ v6_vectsp_1(esk293_0)
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[52037,7913,theory(equality)]) ).
cnf(52168,negated_conjecture,
( r1_rlvect_1(esk294_0,k1_rlvect_1(esk294_0))
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| ~ v8_vectsp_1(esk293_0)
| ~ v7_vectsp_1(esk293_0)
| ~ v6_vectsp_1(esk293_0)
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[52167,7919,theory(equality)]) ).
cnf(52169,negated_conjecture,
( r1_rlvect_1(esk294_0,k1_rlvect_1(esk294_0))
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| ~ v7_vectsp_1(esk293_0)
| ~ v6_vectsp_1(esk293_0)
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[52168,7920,theory(equality)]) ).
cnf(52170,negated_conjecture,
( r1_rlvect_1(esk294_0,k1_rlvect_1(esk294_0))
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| ~ v6_vectsp_1(esk293_0)
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[52169,7921,theory(equality)]) ).
cnf(52171,negated_conjecture,
( r1_rlvect_1(esk294_0,k1_rlvect_1(esk294_0))
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| ~ v4_group_1(esk293_0)
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[52170,7922,theory(equality)]) ).
cnf(52172,negated_conjecture,
( r1_rlvect_1(esk294_0,k1_rlvect_1(esk294_0))
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| ~ l1_vectsp_2(esk294_0,esk293_0)
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[52171,7923,theory(equality)]) ).
cnf(52173,negated_conjecture,
( r1_rlvect_1(esk294_0,k1_rlvect_1(esk294_0))
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v6_rlvect_1(esk294_0)
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[52172,7912,theory(equality)]) ).
cnf(52174,negated_conjecture,
( r1_rlvect_1(esk294_0,k1_rlvect_1(esk294_0))
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v6_rlvect_1(esk293_0)
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[52173,7914,theory(equality)]) ).
cnf(52175,negated_conjecture,
( r1_rlvect_1(esk294_0,k1_rlvect_1(esk294_0))
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v5_rlvect_1(esk294_0)
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[52174,7924,theory(equality)]) ).
cnf(52176,negated_conjecture,
( r1_rlvect_1(esk294_0,k1_rlvect_1(esk294_0))
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v5_rlvect_1(esk293_0)
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[52175,7915,theory(equality)]) ).
cnf(52177,negated_conjecture,
( r1_rlvect_1(esk294_0,k1_rlvect_1(esk294_0))
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v4_rlvect_1(esk294_0)
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[52176,7925,theory(equality)]) ).
cnf(52178,negated_conjecture,
( r1_rlvect_1(esk294_0,k1_rlvect_1(esk294_0))
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v4_rlvect_1(esk293_0)
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[52177,7916,theory(equality)]) ).
cnf(52179,negated_conjecture,
( r1_rlvect_1(esk294_0,k1_rlvect_1(esk294_0))
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v3_rlvect_1(esk294_0)
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[52178,7926,theory(equality)]) ).
cnf(52180,negated_conjecture,
( r1_rlvect_1(esk294_0,k1_rlvect_1(esk294_0))
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ v3_rlvect_1(esk293_0) ),
inference(rw,[status(thm)],[52179,7917,theory(equality)]) ).
cnf(52181,negated_conjecture,
( r1_rlvect_1(esk294_0,k1_rlvect_1(esk294_0))
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[52180,7927,theory(equality)]) ).
cnf(52182,negated_conjecture,
( r1_rlvect_1(esk294_0,k1_rlvect_1(esk294_0))
| v3_struct_0(esk293_0)
| v3_struct_0(esk294_0) ),
inference(cn,[status(thm)],[52181,theory(equality)]) ).
cnf(52183,negated_conjecture,
( r1_rlvect_1(esk294_0,k1_rlvect_1(esk294_0))
| v3_struct_0(esk294_0) ),
inference(sr,[status(thm)],[52182,7928,theory(equality)]) ).
cnf(52184,negated_conjecture,
r1_rlvect_1(esk294_0,k1_rlvect_1(esk294_0)),
inference(sr,[status(thm)],[52183,7918,theory(equality)]) ).
cnf(52379,negated_conjecture,
( r2_hidden(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ l1_struct_0(esk294_0) ),
inference(spm,[status(thm)],[6949,52184,theory(equality)]) ).
cnf(52987,negated_conjecture,
( l1_rlvect_1(esk294_0)
| ~ l1_rlvect_1(esk293_0) ),
inference(spm,[status(thm)],[8503,8396,theory(equality)]) ).
cnf(52988,negated_conjecture,
( r2_hidden(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ l1_rlvect_1(esk294_0) ),
inference(spm,[status(thm)],[52379,8396,theory(equality)]) ).
cnf(52998,negated_conjecture,
( m1_subset_1(k1_rlvect_1(esk294_0),u1_struct_0(esk294_0))
| ~ l1_rlvect_1(esk294_0) ),
inference(spm,[status(thm)],[6923,52988,theory(equality)]) ).
cnf(53009,negated_conjecture,
~ l1_rlvect_1(esk294_0),
inference(sr,[status(thm)],[52998,51987,theory(equality)]) ).
cnf(53012,negated_conjecture,
~ l1_rlvect_1(esk293_0),
inference(spm,[status(thm)],[53009,52987,theory(equality)]) ).
cnf(53013,negated_conjecture,
~ l3_vectsp_1(esk293_0),
inference(spm,[status(thm)],[53012,3797,theory(equality)]) ).
cnf(53015,negated_conjecture,
$false,
inference(rw,[status(thm)],[53013,7919,theory(equality)]) ).
cnf(53016,negated_conjecture,
$false,
inference(cn,[status(thm)],[53015,theory(equality)]) ).
cnf(53017,negated_conjecture,
$false,
53016,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/ALG/ALG216+2.p
% --creating new selector for [SET007+3.ax, SET007+0.ax, SET007+1.ax, SET007+2.ax, SET007+4.ax, SET007+5.ax, SET007+6.ax, SET007+7.ax, SET007+9.ax, SET007+10.ax, SET007+11.ax, SET007+14.ax, SET007+16.ax, SET007+20.ax, SET007+26.ax, SET007+31.ax, SET007+34.ax, SET007+35.ax, SET007+40.ax, SET007+48.ax, SET007+54.ax, SET007+55.ax, SET007+200.ax, SET007+210.ax, SET007+211.ax, SET007+212.ax, SET007+213.ax, SET007+224.ax, SET007+241.ax, SET007+276.ax, SET007+278.ax, SET007+279.ax, SET007+280.ax]
% -running prover on /tmp/tmpsY844r/sel_ALG216+2.p_1 with time limit 29
% -prover status Theorem
% Problem ALG216+2.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/ALG/ALG216+2.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/ALG/ALG216+2.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------