%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : ALG218+1 : TPTP v5.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art04.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 : Tue Dec 28 21:12:59 EST 2010
% Result : Theorem 1.27s
% Output : Solution 1.27s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP3357/ALG218+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP3357/ALG218+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP3357/ALG218+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 3453
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.029 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(2, axiom,![X1]:?[X2]:m1_subset_1(X2,X1),file('/tmp/SRASS.s.p', existence_m1_subset_1)).
% fof(3, axiom,![X1]:![X2]:((((((((((~(v3_struct_0(X2))&v3_rlvect_1(X2))&v4_rlvect_1(X2))&v5_rlvect_1(X2))&v6_rlvect_1(X2))&v4_group_1(X2))&v6_vectsp_1(X2))&v7_vectsp_1(X2))&v8_vectsp_1(X2))&l3_vectsp_1(X2))=>![X3]:(((((((~(v3_struct_0(X3))&v3_rlvect_1(X3))&v4_rlvect_1(X3))&v5_rlvect_1(X3))&v6_rlvect_1(X3))&v5_vectsp_2(X3,X2))&l1_vectsp_2(X3,X2))=>(r1_rlvect_1(k1_rmod_2(X2,X3),X1)<=>X1=k1_rlvect_1(X3)))),file('/tmp/SRASS.s.p', t46_rmod_2)).
% fof(9, axiom,![X1]:![X2]:(((((((((((((~(v3_struct_0(X2))&v3_rlvect_1(X2))&v4_rlvect_1(X2))&v5_rlvect_1(X2))&v6_rlvect_1(X2))&v4_group_1(X2))&v7_group_1(X2))&v6_vectsp_1(X2))&v7_vectsp_1(X2))&v8_vectsp_1(X2))&~(v10_vectsp_1(X2)))&v2_vectsp_2(X2))&l3_vectsp_1(X2))=>![X3]:(((((((~(v3_struct_0(X3))&v3_rlvect_1(X3))&v4_rlvect_1(X3))&v5_rlvect_1(X3))&v6_rlvect_1(X3))&v5_vectsp_2(X3,X2))&l1_vectsp_2(X3,X2))=>![X4]:(m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X3)))=>(r2_hidden(X1,X4)=>r1_rlvect_1(k1_rmod_5(X2,X3,X4),X1))))),file('/tmp/SRASS.s.p', t10_rmod_5)).
% fof(13, axiom,![X1]:![X2]:(((~(v3_struct_0(X1))&l1_struct_0(X1))&m1_subset_1(X2,u1_struct_0(X1)))=>k7_rlvect_2(X1,X2)=k1_tarski(X2)),file('/tmp/SRASS.s.p', redefinition_k7_rlvect_2)).
% fof(14, axiom,![X1]:(v1_xboole_0(X1)=>X1=k1_xboole_0),file('/tmp/SRASS.s.p', t6_boole)).
% fof(22, axiom,![X1]:![X2]:![X3]:((r2_hidden(X1,X2)&m1_subset_1(X2,k1_zfmisc_1(X3)))=>m1_subset_1(X1,X3)),file('/tmp/SRASS.s.p', t4_subset)).
% fof(36, axiom,?[X1]:v1_xboole_0(X1),file('/tmp/SRASS.s.p', rc1_xboole_0)).
% fof(40, axiom,![X1]:![X2]:(X1=X2<=>(r1_tarski(X1,X2)&r1_tarski(X2,X1))),file('/tmp/SRASS.s.p', d10_xboole_0)).
% fof(47, axiom,![X1]:![X2]:(X2=k1_tarski(X1)<=>![X3]:(r2_hidden(X3,X2)<=>X3=X1)),file('/tmp/SRASS.s.p', d1_tarski)).
% fof(49, axiom,![X1]:![X2]:(m1_subset_1(X1,X2)=>(v1_xboole_0(X2)|r2_hidden(X1,X2))),file('/tmp/SRASS.s.p', t2_subset)).
% fof(53, axiom,![X1]:![X2]:~((r2_hidden(X1,X2)&v1_xboole_0(X2))),file('/tmp/SRASS.s.p', t7_boole)).
% fof(55, axiom,![X1]:(l1_struct_0(X1)=>![X2]:(l1_vectsp_2(X2,X1)=>l1_rlvect_1(X2))),file('/tmp/SRASS.s.p', dt_l1_vectsp_2)).
% fof(56, axiom,![X1]:(l3_vectsp_1(X1)=>(l1_rlvect_1(X1)&l2_vectsp_1(X1))),file('/tmp/SRASS.s.p', dt_l3_vectsp_1)).
% fof(61, axiom,![X1]:(l2_struct_0(X1)=>l1_struct_0(X1)),file('/tmp/SRASS.s.p', dt_l2_struct_0)).
% fof(62, axiom,![X1]:![X2]:(r1_tarski(X1,X2)<=>![X3]:(r2_hidden(X3,X1)=>r2_hidden(X3,X2))),file('/tmp/SRASS.s.p', d3_tarski)).
% fof(63, axiom,![X1]:(l1_rlvect_1(X1)=>l2_struct_0(X1)),file('/tmp/SRASS.s.p', dt_l1_rlvect_1)).
% fof(70, axiom,![X1]:(l2_vectsp_1(X1)=>(l1_vectsp_1(X1)&l2_struct_0(X1))),file('/tmp/SRASS.s.p', dt_l2_vectsp_1)).
% fof(79, 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))&v7_group_1(X1))&v6_vectsp_1(X1))&v7_vectsp_1(X1))&v8_vectsp_1(X1))&~(v10_vectsp_1(X1)))&v2_vectsp_2(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,k1_zfmisc_1(u1_struct_0(X2)))=>~(((k1_rmod_5(X1,X2,X3)=k1_rmod_2(X1,X2)&~(X3=k1_xboole_0))&~(X3=k7_rlvect_2(X2,k1_rlvect_1(X2)))))))),file('/tmp/SRASS.s.p', t12_rmod_5)).
% fof(80, 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))&v7_group_1(X1))&v6_vectsp_1(X1))&v7_vectsp_1(X1))&v8_vectsp_1(X1))&~(v10_vectsp_1(X1)))&v2_vectsp_2(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,k1_zfmisc_1(u1_struct_0(X2)))=>~(((k1_rmod_5(X1,X2,X3)=k1_rmod_2(X1,X2)&~(X3=k1_xboole_0))&~(X3=k7_rlvect_2(X2,k1_rlvect_1(X2))))))))),inference(assume_negation,[status(cth)],[79])).
% fof(81, plain,![X1]:![X2]:((((((((((~(v3_struct_0(X2))&v3_rlvect_1(X2))&v4_rlvect_1(X2))&v5_rlvect_1(X2))&v6_rlvect_1(X2))&v4_group_1(X2))&v6_vectsp_1(X2))&v7_vectsp_1(X2))&v8_vectsp_1(X2))&l3_vectsp_1(X2))=>![X3]:(((((((~(v3_struct_0(X3))&v3_rlvect_1(X3))&v4_rlvect_1(X3))&v5_rlvect_1(X3))&v6_rlvect_1(X3))&v5_vectsp_2(X3,X2))&l1_vectsp_2(X3,X2))=>(r1_rlvect_1(k1_rmod_2(X2,X3),X1)<=>X1=k1_rlvect_1(X3)))),inference(fof_simplification,[status(thm)],[3,theory(equality)])).
% fof(87, plain,![X1]:![X2]:(((((((((((((~(v3_struct_0(X2))&v3_rlvect_1(X2))&v4_rlvect_1(X2))&v5_rlvect_1(X2))&v6_rlvect_1(X2))&v4_group_1(X2))&v7_group_1(X2))&v6_vectsp_1(X2))&v7_vectsp_1(X2))&v8_vectsp_1(X2))&~(v10_vectsp_1(X2)))&v2_vectsp_2(X2))&l3_vectsp_1(X2))=>![X3]:(((((((~(v3_struct_0(X3))&v3_rlvect_1(X3))&v4_rlvect_1(X3))&v5_rlvect_1(X3))&v6_rlvect_1(X3))&v5_vectsp_2(X3,X2))&l1_vectsp_2(X3,X2))=>![X4]:(m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X3)))=>(r2_hidden(X1,X4)=>r1_rlvect_1(k1_rmod_5(X2,X3,X4),X1))))),inference(fof_simplification,[status(thm)],[9,theory(equality)])).
% fof(90, plain,![X1]:![X2]:(((~(v3_struct_0(X1))&l1_struct_0(X1))&m1_subset_1(X2,u1_struct_0(X1)))=>k7_rlvect_2(X1,X2)=k1_tarski(X2)),inference(fof_simplification,[status(thm)],[13,theory(equality)])).
% fof(107, 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))&v7_group_1(X1))&v6_vectsp_1(X1))&v7_vectsp_1(X1))&v8_vectsp_1(X1))&~(v10_vectsp_1(X1)))&v2_vectsp_2(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,k1_zfmisc_1(u1_struct_0(X2)))=>~(((k1_rmod_5(X1,X2,X3)=k1_rmod_2(X1,X2)&~(X3=k1_xboole_0))&~(X3=k7_rlvect_2(X2,k1_rlvect_1(X2))))))))),inference(fof_simplification,[status(thm)],[80,theory(equality)])).
% fof(111, plain,![X3]:?[X4]:m1_subset_1(X4,X3),inference(variable_rename,[status(thm)],[2])).
% fof(112, plain,![X3]:m1_subset_1(esk2_1(X3),X3),inference(skolemize,[status(esa)],[111])).
% cnf(113,plain,(m1_subset_1(esk2_1(X1),X1)),inference(split_conjunct,[status(thm)],[112])).
% fof(114, plain,![X1]:![X2]:((((((((((v3_struct_0(X2)|~(v3_rlvect_1(X2)))|~(v4_rlvect_1(X2)))|~(v5_rlvect_1(X2)))|~(v6_rlvect_1(X2)))|~(v4_group_1(X2)))|~(v6_vectsp_1(X2)))|~(v7_vectsp_1(X2)))|~(v8_vectsp_1(X2)))|~(l3_vectsp_1(X2)))|![X3]:(((((((v3_struct_0(X3)|~(v3_rlvect_1(X3)))|~(v4_rlvect_1(X3)))|~(v5_rlvect_1(X3)))|~(v6_rlvect_1(X3)))|~(v5_vectsp_2(X3,X2)))|~(l1_vectsp_2(X3,X2)))|((~(r1_rlvect_1(k1_rmod_2(X2,X3),X1))|X1=k1_rlvect_1(X3))&(~(X1=k1_rlvect_1(X3))|r1_rlvect_1(k1_rmod_2(X2,X3),X1))))),inference(fof_nnf,[status(thm)],[81])).
% fof(115, plain,![X4]:![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)))|((~(r1_rlvect_1(k1_rmod_2(X5,X6),X4))|X4=k1_rlvect_1(X6))&(~(X4=k1_rlvect_1(X6))|r1_rlvect_1(k1_rmod_2(X5,X6),X4))))),inference(variable_rename,[status(thm)],[114])).
% fof(116, plain,![X4]:![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)))|((~(r1_rlvect_1(k1_rmod_2(X5,X6),X4))|X4=k1_rlvect_1(X6))&(~(X4=k1_rlvect_1(X6))|r1_rlvect_1(k1_rmod_2(X5,X6),X4))))|(((((((((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)],[115])).
% fof(117, plain,![X4]:![X5]:![X6]:((((~(r1_rlvect_1(k1_rmod_2(X5,X6),X4))|X4=k1_rlvect_1(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))))&(((~(X4=k1_rlvect_1(X6))|r1_rlvect_1(k1_rmod_2(X5,X6),X4))|((((((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)],[116])).
% cnf(119,plain,(v3_struct_0(X1)|v3_struct_0(X2)|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)|~r1_rlvect_1(k1_rmod_2(X1,X2),X3)),inference(split_conjunct,[status(thm)],[117])).
% fof(163, plain,![X1]:![X2]:(((((((((((((v3_struct_0(X2)|~(v3_rlvect_1(X2)))|~(v4_rlvect_1(X2)))|~(v5_rlvect_1(X2)))|~(v6_rlvect_1(X2)))|~(v4_group_1(X2)))|~(v7_group_1(X2)))|~(v6_vectsp_1(X2)))|~(v7_vectsp_1(X2)))|~(v8_vectsp_1(X2)))|v10_vectsp_1(X2))|~(v2_vectsp_2(X2)))|~(l3_vectsp_1(X2)))|![X3]:(((((((v3_struct_0(X3)|~(v3_rlvect_1(X3)))|~(v4_rlvect_1(X3)))|~(v5_rlvect_1(X3)))|~(v6_rlvect_1(X3)))|~(v5_vectsp_2(X3,X2)))|~(l1_vectsp_2(X3,X2)))|![X4]:(~(m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X3))))|(~(r2_hidden(X1,X4))|r1_rlvect_1(k1_rmod_5(X2,X3,X4),X1))))),inference(fof_nnf,[status(thm)],[87])).
% fof(164, plain,![X5]:![X6]:(((((((((((((v3_struct_0(X6)|~(v3_rlvect_1(X6)))|~(v4_rlvect_1(X6)))|~(v5_rlvect_1(X6)))|~(v6_rlvect_1(X6)))|~(v4_group_1(X6)))|~(v7_group_1(X6)))|~(v6_vectsp_1(X6)))|~(v7_vectsp_1(X6)))|~(v8_vectsp_1(X6)))|v10_vectsp_1(X6))|~(v2_vectsp_2(X6)))|~(l3_vectsp_1(X6)))|![X7]:(((((((v3_struct_0(X7)|~(v3_rlvect_1(X7)))|~(v4_rlvect_1(X7)))|~(v5_rlvect_1(X7)))|~(v6_rlvect_1(X7)))|~(v5_vectsp_2(X7,X6)))|~(l1_vectsp_2(X7,X6)))|![X8]:(~(m1_subset_1(X8,k1_zfmisc_1(u1_struct_0(X7))))|(~(r2_hidden(X5,X8))|r1_rlvect_1(k1_rmod_5(X6,X7,X8),X5))))),inference(variable_rename,[status(thm)],[163])).
% fof(165, plain,![X5]:![X6]:![X7]:![X8]:(((~(m1_subset_1(X8,k1_zfmisc_1(u1_struct_0(X7))))|(~(r2_hidden(X5,X8))|r1_rlvect_1(k1_rmod_5(X6,X7,X8),X5)))|((((((v3_struct_0(X7)|~(v3_rlvect_1(X7)))|~(v4_rlvect_1(X7)))|~(v5_rlvect_1(X7)))|~(v6_rlvect_1(X7)))|~(v5_vectsp_2(X7,X6)))|~(l1_vectsp_2(X7,X6))))|((((((((((((v3_struct_0(X6)|~(v3_rlvect_1(X6)))|~(v4_rlvect_1(X6)))|~(v5_rlvect_1(X6)))|~(v6_rlvect_1(X6)))|~(v4_group_1(X6)))|~(v7_group_1(X6)))|~(v6_vectsp_1(X6)))|~(v7_vectsp_1(X6)))|~(v8_vectsp_1(X6)))|v10_vectsp_1(X6))|~(v2_vectsp_2(X6)))|~(l3_vectsp_1(X6)))),inference(shift_quantors,[status(thm)],[164])).
% cnf(166,plain,(v10_vectsp_1(X1)|v3_struct_0(X1)|v3_struct_0(X2)|r1_rlvect_1(k1_rmod_5(X1,X2,X3),X4)|~l3_vectsp_1(X1)|~v2_vectsp_2(X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v7_group_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)|~r2_hidden(X4,X3)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))),inference(split_conjunct,[status(thm)],[165])).
% fof(187, plain,![X1]:![X2]:(((v3_struct_0(X1)|~(l1_struct_0(X1)))|~(m1_subset_1(X2,u1_struct_0(X1))))|k7_rlvect_2(X1,X2)=k1_tarski(X2)),inference(fof_nnf,[status(thm)],[90])).
% fof(188, plain,![X3]:![X4]:(((v3_struct_0(X3)|~(l1_struct_0(X3)))|~(m1_subset_1(X4,u1_struct_0(X3))))|k7_rlvect_2(X3,X4)=k1_tarski(X4)),inference(variable_rename,[status(thm)],[187])).
% cnf(189,plain,(k7_rlvect_2(X1,X2)=k1_tarski(X2)|v3_struct_0(X1)|~m1_subset_1(X2,u1_struct_0(X1))|~l1_struct_0(X1)),inference(split_conjunct,[status(thm)],[188])).
% fof(190, plain,![X1]:(~(v1_xboole_0(X1))|X1=k1_xboole_0),inference(fof_nnf,[status(thm)],[14])).
% fof(191, plain,![X2]:(~(v1_xboole_0(X2))|X2=k1_xboole_0),inference(variable_rename,[status(thm)],[190])).
% cnf(192,plain,(X1=k1_xboole_0|~v1_xboole_0(X1)),inference(split_conjunct,[status(thm)],[191])).
% fof(234, plain,![X1]:![X2]:![X3]:((~(r2_hidden(X1,X2))|~(m1_subset_1(X2,k1_zfmisc_1(X3))))|m1_subset_1(X1,X3)),inference(fof_nnf,[status(thm)],[22])).
% fof(235, plain,![X4]:![X5]:![X6]:((~(r2_hidden(X4,X5))|~(m1_subset_1(X5,k1_zfmisc_1(X6))))|m1_subset_1(X4,X6)),inference(variable_rename,[status(thm)],[234])).
% cnf(236,plain,(m1_subset_1(X1,X2)|~m1_subset_1(X3,k1_zfmisc_1(X2))|~r2_hidden(X1,X3)),inference(split_conjunct,[status(thm)],[235])).
% fof(279, plain,?[X2]:v1_xboole_0(X2),inference(variable_rename,[status(thm)],[36])).
% fof(280, plain,v1_xboole_0(esk18_0),inference(skolemize,[status(esa)],[279])).
% cnf(281,plain,(v1_xboole_0(esk18_0)),inference(split_conjunct,[status(thm)],[280])).
% fof(290, plain,![X1]:![X2]:((~(X1=X2)|(r1_tarski(X1,X2)&r1_tarski(X2,X1)))&((~(r1_tarski(X1,X2))|~(r1_tarski(X2,X1)))|X1=X2)),inference(fof_nnf,[status(thm)],[40])).
% fof(291, plain,![X3]:![X4]:((~(X3=X4)|(r1_tarski(X3,X4)&r1_tarski(X4,X3)))&((~(r1_tarski(X3,X4))|~(r1_tarski(X4,X3)))|X3=X4)),inference(variable_rename,[status(thm)],[290])).
% fof(292, plain,![X3]:![X4]:(((r1_tarski(X3,X4)|~(X3=X4))&(r1_tarski(X4,X3)|~(X3=X4)))&((~(r1_tarski(X3,X4))|~(r1_tarski(X4,X3)))|X3=X4)),inference(distribute,[status(thm)],[291])).
% cnf(293,plain,(X1=X2|~r1_tarski(X2,X1)|~r1_tarski(X1,X2)),inference(split_conjunct,[status(thm)],[292])).
% fof(316, plain,![X1]:![X2]:((~(X2=k1_tarski(X1))|![X3]:((~(r2_hidden(X3,X2))|X3=X1)&(~(X3=X1)|r2_hidden(X3,X2))))&(?[X3]:((~(r2_hidden(X3,X2))|~(X3=X1))&(r2_hidden(X3,X2)|X3=X1))|X2=k1_tarski(X1))),inference(fof_nnf,[status(thm)],[47])).
% fof(317, plain,![X4]:![X5]:((~(X5=k1_tarski(X4))|![X6]:((~(r2_hidden(X6,X5))|X6=X4)&(~(X6=X4)|r2_hidden(X6,X5))))&(?[X7]:((~(r2_hidden(X7,X5))|~(X7=X4))&(r2_hidden(X7,X5)|X7=X4))|X5=k1_tarski(X4))),inference(variable_rename,[status(thm)],[316])).
% fof(318, plain,![X4]:![X5]:((~(X5=k1_tarski(X4))|![X6]:((~(r2_hidden(X6,X5))|X6=X4)&(~(X6=X4)|r2_hidden(X6,X5))))&(((~(r2_hidden(esk22_2(X4,X5),X5))|~(esk22_2(X4,X5)=X4))&(r2_hidden(esk22_2(X4,X5),X5)|esk22_2(X4,X5)=X4))|X5=k1_tarski(X4))),inference(skolemize,[status(esa)],[317])).
% fof(319, plain,![X4]:![X5]:![X6]:((((~(r2_hidden(X6,X5))|X6=X4)&(~(X6=X4)|r2_hidden(X6,X5)))|~(X5=k1_tarski(X4)))&(((~(r2_hidden(esk22_2(X4,X5),X5))|~(esk22_2(X4,X5)=X4))&(r2_hidden(esk22_2(X4,X5),X5)|esk22_2(X4,X5)=X4))|X5=k1_tarski(X4))),inference(shift_quantors,[status(thm)],[318])).
% fof(320, plain,![X4]:![X5]:![X6]:((((~(r2_hidden(X6,X5))|X6=X4)|~(X5=k1_tarski(X4)))&((~(X6=X4)|r2_hidden(X6,X5))|~(X5=k1_tarski(X4))))&(((~(r2_hidden(esk22_2(X4,X5),X5))|~(esk22_2(X4,X5)=X4))|X5=k1_tarski(X4))&((r2_hidden(esk22_2(X4,X5),X5)|esk22_2(X4,X5)=X4)|X5=k1_tarski(X4)))),inference(distribute,[status(thm)],[319])).
% cnf(323,plain,(r2_hidden(X3,X1)|X1!=k1_tarski(X2)|X3!=X2),inference(split_conjunct,[status(thm)],[320])).
% cnf(324,plain,(X3=X2|X1!=k1_tarski(X2)|~r2_hidden(X3,X1)),inference(split_conjunct,[status(thm)],[320])).
% fof(331, plain,![X1]:![X2]:(~(m1_subset_1(X1,X2))|(v1_xboole_0(X2)|r2_hidden(X1,X2))),inference(fof_nnf,[status(thm)],[49])).
% fof(332, plain,![X3]:![X4]:(~(m1_subset_1(X3,X4))|(v1_xboole_0(X4)|r2_hidden(X3,X4))),inference(variable_rename,[status(thm)],[331])).
% cnf(333,plain,(r2_hidden(X1,X2)|v1_xboole_0(X2)|~m1_subset_1(X1,X2)),inference(split_conjunct,[status(thm)],[332])).
% fof(343, plain,![X1]:![X2]:(~(r2_hidden(X1,X2))|~(v1_xboole_0(X2))),inference(fof_nnf,[status(thm)],[53])).
% fof(344, plain,![X3]:![X4]:(~(r2_hidden(X3,X4))|~(v1_xboole_0(X4))),inference(variable_rename,[status(thm)],[343])).
% cnf(345,plain,(~v1_xboole_0(X1)|~r2_hidden(X2,X1)),inference(split_conjunct,[status(thm)],[344])).
% fof(349, plain,![X1]:(~(l1_struct_0(X1))|![X2]:(~(l1_vectsp_2(X2,X1))|l1_rlvect_1(X2))),inference(fof_nnf,[status(thm)],[55])).
% fof(350, plain,![X3]:(~(l1_struct_0(X3))|![X4]:(~(l1_vectsp_2(X4,X3))|l1_rlvect_1(X4))),inference(variable_rename,[status(thm)],[349])).
% fof(351, plain,![X3]:![X4]:((~(l1_vectsp_2(X4,X3))|l1_rlvect_1(X4))|~(l1_struct_0(X3))),inference(shift_quantors,[status(thm)],[350])).
% cnf(352,plain,(l1_rlvect_1(X2)|~l1_struct_0(X1)|~l1_vectsp_2(X2,X1)),inference(split_conjunct,[status(thm)],[351])).
% fof(353, plain,![X1]:(~(l3_vectsp_1(X1))|(l1_rlvect_1(X1)&l2_vectsp_1(X1))),inference(fof_nnf,[status(thm)],[56])).
% fof(354, plain,![X2]:(~(l3_vectsp_1(X2))|(l1_rlvect_1(X2)&l2_vectsp_1(X2))),inference(variable_rename,[status(thm)],[353])).
% fof(355, plain,![X2]:((l1_rlvect_1(X2)|~(l3_vectsp_1(X2)))&(l2_vectsp_1(X2)|~(l3_vectsp_1(X2)))),inference(distribute,[status(thm)],[354])).
% cnf(356,plain,(l2_vectsp_1(X1)|~l3_vectsp_1(X1)),inference(split_conjunct,[status(thm)],[355])).
% fof(380, plain,![X1]:(~(l2_struct_0(X1))|l1_struct_0(X1)),inference(fof_nnf,[status(thm)],[61])).
% fof(381, plain,![X2]:(~(l2_struct_0(X2))|l1_struct_0(X2)),inference(variable_rename,[status(thm)],[380])).
% cnf(382,plain,(l1_struct_0(X1)|~l2_struct_0(X1)),inference(split_conjunct,[status(thm)],[381])).
% fof(383, plain,![X1]:![X2]:((~(r1_tarski(X1,X2))|![X3]:(~(r2_hidden(X3,X1))|r2_hidden(X3,X2)))&(?[X3]:(r2_hidden(X3,X1)&~(r2_hidden(X3,X2)))|r1_tarski(X1,X2))),inference(fof_nnf,[status(thm)],[62])).
% fof(384, plain,![X4]:![X5]:((~(r1_tarski(X4,X5))|![X6]:(~(r2_hidden(X6,X4))|r2_hidden(X6,X5)))&(?[X7]:(r2_hidden(X7,X4)&~(r2_hidden(X7,X5)))|r1_tarski(X4,X5))),inference(variable_rename,[status(thm)],[383])).
% fof(385, plain,![X4]:![X5]:((~(r1_tarski(X4,X5))|![X6]:(~(r2_hidden(X6,X4))|r2_hidden(X6,X5)))&((r2_hidden(esk27_2(X4,X5),X4)&~(r2_hidden(esk27_2(X4,X5),X5)))|r1_tarski(X4,X5))),inference(skolemize,[status(esa)],[384])).
% fof(386, plain,![X4]:![X5]:![X6]:(((~(r2_hidden(X6,X4))|r2_hidden(X6,X5))|~(r1_tarski(X4,X5)))&((r2_hidden(esk27_2(X4,X5),X4)&~(r2_hidden(esk27_2(X4,X5),X5)))|r1_tarski(X4,X5))),inference(shift_quantors,[status(thm)],[385])).
% fof(387, plain,![X4]:![X5]:![X6]:(((~(r2_hidden(X6,X4))|r2_hidden(X6,X5))|~(r1_tarski(X4,X5)))&((r2_hidden(esk27_2(X4,X5),X4)|r1_tarski(X4,X5))&(~(r2_hidden(esk27_2(X4,X5),X5))|r1_tarski(X4,X5)))),inference(distribute,[status(thm)],[386])).
% cnf(388,plain,(r1_tarski(X1,X2)|~r2_hidden(esk27_2(X1,X2),X2)),inference(split_conjunct,[status(thm)],[387])).
% cnf(389,plain,(r1_tarski(X1,X2)|r2_hidden(esk27_2(X1,X2),X1)),inference(split_conjunct,[status(thm)],[387])).
% fof(391, plain,![X1]:(~(l1_rlvect_1(X1))|l2_struct_0(X1)),inference(fof_nnf,[status(thm)],[63])).
% fof(392, plain,![X2]:(~(l1_rlvect_1(X2))|l2_struct_0(X2)),inference(variable_rename,[status(thm)],[391])).
% cnf(393,plain,(l2_struct_0(X1)|~l1_rlvect_1(X1)),inference(split_conjunct,[status(thm)],[392])).
% fof(418, plain,![X1]:(~(l2_vectsp_1(X1))|(l1_vectsp_1(X1)&l2_struct_0(X1))),inference(fof_nnf,[status(thm)],[70])).
% fof(419, plain,![X2]:(~(l2_vectsp_1(X2))|(l1_vectsp_1(X2)&l2_struct_0(X2))),inference(variable_rename,[status(thm)],[418])).
% fof(420, plain,![X2]:((l1_vectsp_1(X2)|~(l2_vectsp_1(X2)))&(l2_struct_0(X2)|~(l2_vectsp_1(X2)))),inference(distribute,[status(thm)],[419])).
% cnf(421,plain,(l2_struct_0(X1)|~l2_vectsp_1(X1)),inference(split_conjunct,[status(thm)],[420])).
% fof(431, 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))&v7_group_1(X1))&v6_vectsp_1(X1))&v7_vectsp_1(X1))&v8_vectsp_1(X1))&~(v10_vectsp_1(X1)))&v2_vectsp_2(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,k1_zfmisc_1(u1_struct_0(X2)))&((k1_rmod_5(X1,X2,X3)=k1_rmod_2(X1,X2)&~(X3=k1_xboole_0))&~(X3=k7_rlvect_2(X2,k1_rlvect_1(X2))))))),inference(fof_nnf,[status(thm)],[107])).
% fof(432, 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))&v7_group_1(X4))&v6_vectsp_1(X4))&v7_vectsp_1(X4))&v8_vectsp_1(X4))&~(v10_vectsp_1(X4)))&v2_vectsp_2(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,k1_zfmisc_1(u1_struct_0(X5)))&((k1_rmod_5(X4,X5,X6)=k1_rmod_2(X4,X5)&~(X6=k1_xboole_0))&~(X6=k7_rlvect_2(X5,k1_rlvect_1(X5))))))),inference(variable_rename,[status(thm)],[431])).
% fof(433, negated_conjecture,(((((((((((((~(v3_struct_0(esk28_0))&v3_rlvect_1(esk28_0))&v4_rlvect_1(esk28_0))&v5_rlvect_1(esk28_0))&v6_rlvect_1(esk28_0))&v4_group_1(esk28_0))&v7_group_1(esk28_0))&v6_vectsp_1(esk28_0))&v7_vectsp_1(esk28_0))&v8_vectsp_1(esk28_0))&~(v10_vectsp_1(esk28_0)))&v2_vectsp_2(esk28_0))&l3_vectsp_1(esk28_0))&(((((((~(v3_struct_0(esk29_0))&v3_rlvect_1(esk29_0))&v4_rlvect_1(esk29_0))&v5_rlvect_1(esk29_0))&v6_rlvect_1(esk29_0))&v5_vectsp_2(esk29_0,esk28_0))&l1_vectsp_2(esk29_0,esk28_0))&(m1_subset_1(esk30_0,k1_zfmisc_1(u1_struct_0(esk29_0)))&((k1_rmod_5(esk28_0,esk29_0,esk30_0)=k1_rmod_2(esk28_0,esk29_0)&~(esk30_0=k1_xboole_0))&~(esk30_0=k7_rlvect_2(esk29_0,k1_rlvect_1(esk29_0))))))),inference(skolemize,[status(esa)],[432])).
% cnf(434,negated_conjecture,(esk30_0!=k7_rlvect_2(esk29_0,k1_rlvect_1(esk29_0))),inference(split_conjunct,[status(thm)],[433])).
% cnf(435,negated_conjecture,(esk30_0!=k1_xboole_0),inference(split_conjunct,[status(thm)],[433])).
% cnf(436,negated_conjecture,(k1_rmod_5(esk28_0,esk29_0,esk30_0)=k1_rmod_2(esk28_0,esk29_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(437,negated_conjecture,(m1_subset_1(esk30_0,k1_zfmisc_1(u1_struct_0(esk29_0)))),inference(split_conjunct,[status(thm)],[433])).
% cnf(438,negated_conjecture,(l1_vectsp_2(esk29_0,esk28_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(439,negated_conjecture,(v5_vectsp_2(esk29_0,esk28_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(440,negated_conjecture,(v6_rlvect_1(esk29_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(441,negated_conjecture,(v5_rlvect_1(esk29_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(442,negated_conjecture,(v4_rlvect_1(esk29_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(443,negated_conjecture,(v3_rlvect_1(esk29_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(444,negated_conjecture,(~v3_struct_0(esk29_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(445,negated_conjecture,(l3_vectsp_1(esk28_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(446,negated_conjecture,(v2_vectsp_2(esk28_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(447,negated_conjecture,(~v10_vectsp_1(esk28_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(448,negated_conjecture,(v8_vectsp_1(esk28_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(449,negated_conjecture,(v7_vectsp_1(esk28_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(450,negated_conjecture,(v6_vectsp_1(esk28_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(451,negated_conjecture,(v7_group_1(esk28_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(452,negated_conjecture,(v4_group_1(esk28_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(453,negated_conjecture,(v6_rlvect_1(esk28_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(454,negated_conjecture,(v5_rlvect_1(esk28_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(455,negated_conjecture,(v4_rlvect_1(esk28_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(456,negated_conjecture,(v3_rlvect_1(esk28_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(457,negated_conjecture,(~v3_struct_0(esk28_0)),inference(split_conjunct,[status(thm)],[433])).
% cnf(462,plain,(r2_hidden(X1,X2)|k1_tarski(X1)!=X2),inference(er,[status(thm)],[323,theory(equality)])).
% cnf(464,negated_conjecture,(l2_vectsp_1(esk28_0)),inference(spm,[status(thm)],[356,445,theory(equality)])).
% cnf(468,plain,(k1_xboole_0=esk18_0),inference(spm,[status(thm)],[192,281,theory(equality)])).
% cnf(493,negated_conjecture,(l1_rlvect_1(esk29_0)|~l1_struct_0(esk28_0)),inference(spm,[status(thm)],[352,438,theory(equality)])).
% cnf(509,plain,(v1_xboole_0(X1)|r2_hidden(esk2_1(X1),X1)),inference(spm,[status(thm)],[333,113,theory(equality)])).
% cnf(546,negated_conjecture,(m1_subset_1(X1,u1_struct_0(esk29_0))|~r2_hidden(X1,esk30_0)),inference(spm,[status(thm)],[236,437,theory(equality)])).
% cnf(555,plain,(r1_tarski(X1,X2)|~v1_xboole_0(X1)),inference(spm,[status(thm)],[345,389,theory(equality)])).
% cnf(557,plain,(X1=esk27_2(X2,X3)|r1_tarski(X2,X3)|k1_tarski(X1)!=X2),inference(spm,[status(thm)],[324,389,theory(equality)])).
% cnf(660,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)|~v2_vectsp_2(esk28_0)|~v7_group_1(esk28_0)|~l1_vectsp_2(esk29_0,esk28_0)|~v5_vectsp_2(esk29_0,esk28_0)|~v8_vectsp_1(esk28_0)|~v7_vectsp_1(esk28_0)|~v6_vectsp_1(esk28_0)|~v4_group_1(esk28_0)|~v6_rlvect_1(esk29_0)|~v6_rlvect_1(esk28_0)|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~m1_subset_1(esk30_0,k1_zfmisc_1(u1_struct_0(esk29_0)))|~l3_vectsp_1(esk28_0)),inference(spm,[status(thm)],[166,436,theory(equality)])).
% cnf(661,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)|$false|~v7_group_1(esk28_0)|~l1_vectsp_2(esk29_0,esk28_0)|~v5_vectsp_2(esk29_0,esk28_0)|~v8_vectsp_1(esk28_0)|~v7_vectsp_1(esk28_0)|~v6_vectsp_1(esk28_0)|~v4_group_1(esk28_0)|~v6_rlvect_1(esk29_0)|~v6_rlvect_1(esk28_0)|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~m1_subset_1(esk30_0,k1_zfmisc_1(u1_struct_0(esk29_0)))|~l3_vectsp_1(esk28_0)),inference(rw,[status(thm)],[660,446,theory(equality)])).
% cnf(662,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)|$false|$false|~l1_vectsp_2(esk29_0,esk28_0)|~v5_vectsp_2(esk29_0,esk28_0)|~v8_vectsp_1(esk28_0)|~v7_vectsp_1(esk28_0)|~v6_vectsp_1(esk28_0)|~v4_group_1(esk28_0)|~v6_rlvect_1(esk29_0)|~v6_rlvect_1(esk28_0)|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~m1_subset_1(esk30_0,k1_zfmisc_1(u1_struct_0(esk29_0)))|~l3_vectsp_1(esk28_0)),inference(rw,[status(thm)],[661,451,theory(equality)])).
% cnf(663,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)|$false|$false|$false|~v5_vectsp_2(esk29_0,esk28_0)|~v8_vectsp_1(esk28_0)|~v7_vectsp_1(esk28_0)|~v6_vectsp_1(esk28_0)|~v4_group_1(esk28_0)|~v6_rlvect_1(esk29_0)|~v6_rlvect_1(esk28_0)|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~m1_subset_1(esk30_0,k1_zfmisc_1(u1_struct_0(esk29_0)))|~l3_vectsp_1(esk28_0)),inference(rw,[status(thm)],[662,438,theory(equality)])).
% cnf(664,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)|$false|$false|$false|$false|~v8_vectsp_1(esk28_0)|~v7_vectsp_1(esk28_0)|~v6_vectsp_1(esk28_0)|~v4_group_1(esk28_0)|~v6_rlvect_1(esk29_0)|~v6_rlvect_1(esk28_0)|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~m1_subset_1(esk30_0,k1_zfmisc_1(u1_struct_0(esk29_0)))|~l3_vectsp_1(esk28_0)),inference(rw,[status(thm)],[663,439,theory(equality)])).
% cnf(665,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)|$false|$false|$false|$false|$false|~v7_vectsp_1(esk28_0)|~v6_vectsp_1(esk28_0)|~v4_group_1(esk28_0)|~v6_rlvect_1(esk29_0)|~v6_rlvect_1(esk28_0)|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~m1_subset_1(esk30_0,k1_zfmisc_1(u1_struct_0(esk29_0)))|~l3_vectsp_1(esk28_0)),inference(rw,[status(thm)],[664,448,theory(equality)])).
% cnf(666,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)|$false|$false|$false|$false|$false|$false|~v6_vectsp_1(esk28_0)|~v4_group_1(esk28_0)|~v6_rlvect_1(esk29_0)|~v6_rlvect_1(esk28_0)|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~m1_subset_1(esk30_0,k1_zfmisc_1(u1_struct_0(esk29_0)))|~l3_vectsp_1(esk28_0)),inference(rw,[status(thm)],[665,449,theory(equality)])).
% cnf(667,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)|$false|$false|$false|$false|$false|$false|$false|~v4_group_1(esk28_0)|~v6_rlvect_1(esk29_0)|~v6_rlvect_1(esk28_0)|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~m1_subset_1(esk30_0,k1_zfmisc_1(u1_struct_0(esk29_0)))|~l3_vectsp_1(esk28_0)),inference(rw,[status(thm)],[666,450,theory(equality)])).
% cnf(668,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)|$false|$false|$false|$false|$false|$false|$false|$false|~v6_rlvect_1(esk29_0)|~v6_rlvect_1(esk28_0)|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~m1_subset_1(esk30_0,k1_zfmisc_1(u1_struct_0(esk29_0)))|~l3_vectsp_1(esk28_0)),inference(rw,[status(thm)],[667,452,theory(equality)])).
% cnf(669,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v6_rlvect_1(esk28_0)|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~m1_subset_1(esk30_0,k1_zfmisc_1(u1_struct_0(esk29_0)))|~l3_vectsp_1(esk28_0)),inference(rw,[status(thm)],[668,440,theory(equality)])).
% cnf(670,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~m1_subset_1(esk30_0,k1_zfmisc_1(u1_struct_0(esk29_0)))|~l3_vectsp_1(esk28_0)),inference(rw,[status(thm)],[669,453,theory(equality)])).
% cnf(671,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~m1_subset_1(esk30_0,k1_zfmisc_1(u1_struct_0(esk29_0)))|~l3_vectsp_1(esk28_0)),inference(rw,[status(thm)],[670,441,theory(equality)])).
% cnf(672,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~m1_subset_1(esk30_0,k1_zfmisc_1(u1_struct_0(esk29_0)))|~l3_vectsp_1(esk28_0)),inference(rw,[status(thm)],[671,454,theory(equality)])).
% cnf(673,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~m1_subset_1(esk30_0,k1_zfmisc_1(u1_struct_0(esk29_0)))|~l3_vectsp_1(esk28_0)),inference(rw,[status(thm)],[672,442,theory(equality)])).
% cnf(674,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~m1_subset_1(esk30_0,k1_zfmisc_1(u1_struct_0(esk29_0)))|~l3_vectsp_1(esk28_0)),inference(rw,[status(thm)],[673,455,theory(equality)])).
% cnf(675,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v3_rlvect_1(esk28_0)|~m1_subset_1(esk30_0,k1_zfmisc_1(u1_struct_0(esk29_0)))|~l3_vectsp_1(esk28_0)),inference(rw,[status(thm)],[674,443,theory(equality)])).
% cnf(676,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~m1_subset_1(esk30_0,k1_zfmisc_1(u1_struct_0(esk29_0)))|~l3_vectsp_1(esk28_0)),inference(rw,[status(thm)],[675,456,theory(equality)])).
% cnf(677,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~l3_vectsp_1(esk28_0)),inference(rw,[status(thm)],[676,437,theory(equality)])).
% cnf(678,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[677,445,theory(equality)])).
% cnf(679,negated_conjecture,(v10_vectsp_1(esk28_0)|r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)),inference(cn,[status(thm)],[678,theory(equality)])).
% cnf(680,negated_conjecture,(r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)),inference(sr,[status(thm)],[679,447,theory(equality)])).
% cnf(681,negated_conjecture,(r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)),inference(sr,[status(thm)],[680,444,theory(equality)])).
% cnf(682,negated_conjecture,(r1_rlvect_1(k1_rmod_2(esk28_0,esk29_0),X1)|~r2_hidden(X1,esk30_0)),inference(sr,[status(thm)],[681,457,theory(equality)])).
% cnf(701,negated_conjecture,(esk18_0!=esk30_0),inference(rw,[status(thm)],[435,468,theory(equality)])).
% cnf(702,negated_conjecture,(l2_struct_0(esk28_0)),inference(spm,[status(thm)],[421,464,theory(equality)])).
% cnf(712,negated_conjecture,(l1_struct_0(esk28_0)),inference(spm,[status(thm)],[382,702,theory(equality)])).
% cnf(871,plain,(X1=X2|~r1_tarski(X1,X2)|~v1_xboole_0(X2)),inference(spm,[status(thm)],[293,555,theory(equality)])).
% cnf(908,negated_conjecture,(l1_rlvect_1(esk29_0)|$false),inference(rw,[status(thm)],[493,712,theory(equality)])).
% cnf(909,negated_conjecture,(l1_rlvect_1(esk29_0)),inference(cn,[status(thm)],[908,theory(equality)])).
% cnf(910,negated_conjecture,(l2_struct_0(esk29_0)),inference(spm,[status(thm)],[393,909,theory(equality)])).
% cnf(911,negated_conjecture,(l1_struct_0(esk29_0)),inference(spm,[status(thm)],[382,910,theory(equality)])).
% cnf(924,negated_conjecture,(k7_rlvect_2(esk29_0,X1)=k1_tarski(X1)|v3_struct_0(esk29_0)|~l1_struct_0(esk29_0)|~r2_hidden(X1,esk30_0)),inference(spm,[status(thm)],[189,546,theory(equality)])).
% cnf(926,negated_conjecture,(k7_rlvect_2(esk29_0,X1)=k1_tarski(X1)|v3_struct_0(esk29_0)|$false|~r2_hidden(X1,esk30_0)),inference(rw,[status(thm)],[924,911,theory(equality)])).
% cnf(927,negated_conjecture,(k7_rlvect_2(esk29_0,X1)=k1_tarski(X1)|v3_struct_0(esk29_0)|~r2_hidden(X1,esk30_0)),inference(cn,[status(thm)],[926,theory(equality)])).
% cnf(928,negated_conjecture,(k7_rlvect_2(esk29_0,X1)=k1_tarski(X1)|~r2_hidden(X1,esk30_0)),inference(sr,[status(thm)],[927,444,theory(equality)])).
% cnf(936,negated_conjecture,(k1_tarski(k1_rlvect_1(esk29_0))!=esk30_0|~r2_hidden(k1_rlvect_1(esk29_0),esk30_0)),inference(spm,[status(thm)],[434,928,theory(equality)])).
% cnf(940,negated_conjecture,(k1_tarski(k1_rlvect_1(esk29_0))!=esk30_0),inference(csr,[status(thm)],[936,462])).
% cnf(1012,negated_conjecture,(k1_rlvect_1(esk29_0)=X1|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~l1_vectsp_2(esk29_0,esk28_0)|~v5_vectsp_2(esk29_0,esk28_0)|~v8_vectsp_1(esk28_0)|~v7_vectsp_1(esk28_0)|~v6_vectsp_1(esk28_0)|~v4_group_1(esk28_0)|~v6_rlvect_1(esk29_0)|~v6_rlvect_1(esk28_0)|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~l3_vectsp_1(esk28_0)|~r2_hidden(X1,esk30_0)),inference(spm,[status(thm)],[119,682,theory(equality)])).
% cnf(1013,negated_conjecture,(k1_rlvect_1(esk29_0)=X1|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|$false|~v5_vectsp_2(esk29_0,esk28_0)|~v8_vectsp_1(esk28_0)|~v7_vectsp_1(esk28_0)|~v6_vectsp_1(esk28_0)|~v4_group_1(esk28_0)|~v6_rlvect_1(esk29_0)|~v6_rlvect_1(esk28_0)|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~l3_vectsp_1(esk28_0)|~r2_hidden(X1,esk30_0)),inference(rw,[status(thm)],[1012,438,theory(equality)])).
% cnf(1014,negated_conjecture,(k1_rlvect_1(esk29_0)=X1|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|$false|$false|~v8_vectsp_1(esk28_0)|~v7_vectsp_1(esk28_0)|~v6_vectsp_1(esk28_0)|~v4_group_1(esk28_0)|~v6_rlvect_1(esk29_0)|~v6_rlvect_1(esk28_0)|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~l3_vectsp_1(esk28_0)|~r2_hidden(X1,esk30_0)),inference(rw,[status(thm)],[1013,439,theory(equality)])).
% cnf(1015,negated_conjecture,(k1_rlvect_1(esk29_0)=X1|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|$false|$false|$false|~v7_vectsp_1(esk28_0)|~v6_vectsp_1(esk28_0)|~v4_group_1(esk28_0)|~v6_rlvect_1(esk29_0)|~v6_rlvect_1(esk28_0)|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~l3_vectsp_1(esk28_0)|~r2_hidden(X1,esk30_0)),inference(rw,[status(thm)],[1014,448,theory(equality)])).
% cnf(1016,negated_conjecture,(k1_rlvect_1(esk29_0)=X1|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|$false|$false|$false|$false|~v6_vectsp_1(esk28_0)|~v4_group_1(esk28_0)|~v6_rlvect_1(esk29_0)|~v6_rlvect_1(esk28_0)|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~l3_vectsp_1(esk28_0)|~r2_hidden(X1,esk30_0)),inference(rw,[status(thm)],[1015,449,theory(equality)])).
% cnf(1017,negated_conjecture,(k1_rlvect_1(esk29_0)=X1|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|$false|$false|$false|$false|$false|~v4_group_1(esk28_0)|~v6_rlvect_1(esk29_0)|~v6_rlvect_1(esk28_0)|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~l3_vectsp_1(esk28_0)|~r2_hidden(X1,esk30_0)),inference(rw,[status(thm)],[1016,450,theory(equality)])).
% cnf(1018,negated_conjecture,(k1_rlvect_1(esk29_0)=X1|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|$false|$false|$false|$false|$false|$false|~v6_rlvect_1(esk29_0)|~v6_rlvect_1(esk28_0)|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~l3_vectsp_1(esk28_0)|~r2_hidden(X1,esk30_0)),inference(rw,[status(thm)],[1017,452,theory(equality)])).
% cnf(1019,negated_conjecture,(k1_rlvect_1(esk29_0)=X1|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|$false|$false|$false|$false|$false|$false|$false|~v6_rlvect_1(esk28_0)|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~l3_vectsp_1(esk28_0)|~r2_hidden(X1,esk30_0)),inference(rw,[status(thm)],[1018,440,theory(equality)])).
% cnf(1020,negated_conjecture,(k1_rlvect_1(esk29_0)=X1|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|$false|$false|$false|$false|$false|$false|$false|$false|~v5_rlvect_1(esk29_0)|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~l3_vectsp_1(esk28_0)|~r2_hidden(X1,esk30_0)),inference(rw,[status(thm)],[1019,453,theory(equality)])).
% cnf(1021,negated_conjecture,(k1_rlvect_1(esk29_0)=X1|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v5_rlvect_1(esk28_0)|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~l3_vectsp_1(esk28_0)|~r2_hidden(X1,esk30_0)),inference(rw,[status(thm)],[1020,441,theory(equality)])).
% cnf(1022,negated_conjecture,(k1_rlvect_1(esk29_0)=X1|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v4_rlvect_1(esk29_0)|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~l3_vectsp_1(esk28_0)|~r2_hidden(X1,esk30_0)),inference(rw,[status(thm)],[1021,454,theory(equality)])).
% cnf(1023,negated_conjecture,(k1_rlvect_1(esk29_0)=X1|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v4_rlvect_1(esk28_0)|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~l3_vectsp_1(esk28_0)|~r2_hidden(X1,esk30_0)),inference(rw,[status(thm)],[1022,442,theory(equality)])).
% cnf(1024,negated_conjecture,(k1_rlvect_1(esk29_0)=X1|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v3_rlvect_1(esk29_0)|~v3_rlvect_1(esk28_0)|~l3_vectsp_1(esk28_0)|~r2_hidden(X1,esk30_0)),inference(rw,[status(thm)],[1023,455,theory(equality)])).
% cnf(1025,negated_conjecture,(k1_rlvect_1(esk29_0)=X1|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v3_rlvect_1(esk28_0)|~l3_vectsp_1(esk28_0)|~r2_hidden(X1,esk30_0)),inference(rw,[status(thm)],[1024,443,theory(equality)])).
% cnf(1026,negated_conjecture,(k1_rlvect_1(esk29_0)=X1|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~l3_vectsp_1(esk28_0)|~r2_hidden(X1,esk30_0)),inference(rw,[status(thm)],[1025,456,theory(equality)])).
% cnf(1027,negated_conjecture,(k1_rlvect_1(esk29_0)=X1|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~r2_hidden(X1,esk30_0)),inference(rw,[status(thm)],[1026,445,theory(equality)])).
% cnf(1028,negated_conjecture,(k1_rlvect_1(esk29_0)=X1|v3_struct_0(esk29_0)|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)),inference(cn,[status(thm)],[1027,theory(equality)])).
% cnf(1029,negated_conjecture,(k1_rlvect_1(esk29_0)=X1|v3_struct_0(esk28_0)|~r2_hidden(X1,esk30_0)),inference(sr,[status(thm)],[1028,444,theory(equality)])).
% cnf(1030,negated_conjecture,(k1_rlvect_1(esk29_0)=X1|~r2_hidden(X1,esk30_0)),inference(sr,[status(thm)],[1029,457,theory(equality)])).
% cnf(1031,negated_conjecture,(k1_rlvect_1(esk29_0)=esk27_2(esk30_0,X1)|r1_tarski(esk30_0,X1)),inference(spm,[status(thm)],[1030,389,theory(equality)])).
% cnf(1033,negated_conjecture,(k1_rlvect_1(esk29_0)=esk2_1(esk30_0)|v1_xboole_0(esk30_0)),inference(spm,[status(thm)],[1030,509,theory(equality)])).
% cnf(1050,negated_conjecture,(r1_tarski(esk30_0,X1)|r2_hidden(k1_rlvect_1(esk29_0),esk30_0)),inference(spm,[status(thm)],[389,1031,theory(equality)])).
% cnf(1051,negated_conjecture,(r1_tarski(esk30_0,X1)|~r2_hidden(k1_rlvect_1(esk29_0),X1)),inference(spm,[status(thm)],[388,1031,theory(equality)])).
% cnf(1101,negated_conjecture,(r1_tarski(esk30_0,X1)|k1_tarski(k1_rlvect_1(esk29_0))!=X1),inference(spm,[status(thm)],[1051,462,theory(equality)])).
% cnf(1121,negated_conjecture,(esk30_0=X1|r2_hidden(k1_rlvect_1(esk29_0),esk30_0)|~v1_xboole_0(X1)),inference(spm,[status(thm)],[871,1050,theory(equality)])).
% cnf(1379,negated_conjecture,(r1_tarski(esk30_0,k1_tarski(k1_rlvect_1(esk29_0)))),inference(er,[status(thm)],[1101,theory(equality)])).
% cnf(1381,negated_conjecture,(k1_tarski(k1_rlvect_1(esk29_0))=esk30_0|~r1_tarski(k1_tarski(k1_rlvect_1(esk29_0)),esk30_0)),inference(spm,[status(thm)],[293,1379,theory(equality)])).
% cnf(1385,negated_conjecture,(~r1_tarski(k1_tarski(k1_rlvect_1(esk29_0)),esk30_0)),inference(sr,[status(thm)],[1381,940,theory(equality)])).
% cnf(1397,negated_conjecture,(esk30_0=esk18_0|r2_hidden(k1_rlvect_1(esk29_0),esk30_0)),inference(spm,[status(thm)],[1121,281,theory(equality)])).
% cnf(1399,negated_conjecture,(r2_hidden(k1_rlvect_1(esk29_0),esk30_0)),inference(sr,[status(thm)],[1397,701,theory(equality)])).
% cnf(1400,negated_conjecture,(~v1_xboole_0(esk30_0)),inference(spm,[status(thm)],[345,1399,theory(equality)])).
% cnf(1409,negated_conjecture,(k1_rlvect_1(esk29_0)=esk2_1(esk30_0)),inference(sr,[status(thm)],[1033,1400,theory(equality)])).
% cnf(1419,negated_conjecture,(r2_hidden(esk2_1(esk30_0),esk30_0)),inference(rw,[status(thm)],[1399,1409,theory(equality)])).
% cnf(1424,negated_conjecture,(~r1_tarski(k1_tarski(esk2_1(esk30_0)),esk30_0)),inference(rw,[status(thm)],[1385,1409,theory(equality)])).
% cnf(1812,plain,(X1=esk27_2(k1_tarski(X1),X2)|r1_tarski(k1_tarski(X1),X2)),inference(er,[status(thm)],[557,theory(equality)])).
% cnf(1841,plain,(r1_tarski(k1_tarski(X1),X2)|~r2_hidden(X1,X2)),inference(spm,[status(thm)],[388,1812,theory(equality)])).
% cnf(1876,negated_conjecture,(~r2_hidden(esk2_1(esk30_0),esk30_0)),inference(spm,[status(thm)],[1424,1841,theory(equality)])).
% cnf(1879,negated_conjecture,($false),inference(rw,[status(thm)],[1876,1419,theory(equality)])).
% cnf(1880,negated_conjecture,($false),inference(cn,[status(thm)],[1879,theory(equality)])).
% cnf(1881,negated_conjecture,($false),1880,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 790
% # ...of these trivial : 12
% # ...subsumed : 192
% # ...remaining for further processing: 586
% # Other redundant clauses eliminated : 3
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 5
% # Backward-rewritten : 39
% # Generated clauses : 890
% # ...of the previous two non-trivial : 839
% # Contextual simplify-reflections : 29
% # Paramodulations : 866
% # Factorizations : 2
% # Equation resolutions : 12
% # Current number of processed clauses: 378
% # Positive orientable unit clauses: 95
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 38
% # Non-unit-clauses : 245
% # Current number of unprocessed clauses: 290
% # ...number of literals in the above : 1449
% # Clause-clause subsumption calls (NU) : 5847
% # Rec. Clause-clause subsumption calls : 3052
% # Unit Clause-clause subsumption calls : 732
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 7
% # Indexed BW rewrite successes : 7
% # Backwards rewriting index: 370 leaves, 1.33+/-1.129 terms/leaf
% # Paramod-from index: 205 leaves, 1.03+/-0.169 terms/leaf
% # Paramod-into index: 334 leaves, 1.12+/-0.507 terms/leaf
% # -------------------------------------------------
% # User time : 0.122 s
% # System time : 0.007 s
% # Total time : 0.129 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.26 CPU 0.35 WC
% FINAL PrfWatch: 0.26 CPU 0.35 WC
% SZS output end Solution for /tmp/SystemOnTPTP3357/ALG218+1.tptp
%
%------------------------------------------------------------------------------