%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : ALG220+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 : art05.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:17:17 EST 2010
% Result : Theorem 1.32s
% Output : Solution 1.32s
% 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/SystemOnTPTP9302/ALG220+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP9302/ALG220+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP9302/ALG220+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 9398
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.027 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(7, axiom,![X1]:![X2]:![X3]:(((((((((((((((((((((~(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))&~(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_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2))))=>(v3_vectsp_2(k1_rmod_5(X1,X2,X3),X1)&m1_rmod_2(k1_rmod_5(X1,X2,X3),X1,X2))),file('/tmp/SRASS.s.p', dt_k1_rmod_5)).
% fof(8, 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))&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)))=>![X4]:(m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2)))=>(r1_tarski(X3,X4)=>m1_rmod_2(k1_rmod_5(X1,X2,X3),X1,k1_rmod_5(X1,X2,X4))))))),file('/tmp/SRASS.s.p', t15_rmod_5)).
% fof(9, 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))&v3_vectsp_2(X2,X1))&v5_vectsp_2(X2,X1))&l1_vectsp_2(X2,X1))=>![X3]:((((((((~(v3_struct_0(X3))&v3_rlvect_1(X3))&v4_rlvect_1(X3))&v5_rlvect_1(X3))&v6_rlvect_1(X3))&v3_vectsp_2(X3,X1))&v5_vectsp_2(X3,X1))&l1_vectsp_2(X3,X1))=>((m1_rmod_2(X3,X1,X2)&m1_rmod_2(X2,X1,X3))=>X3=X2)))),file('/tmp/SRASS.s.p', t33_rmod_2)).
% fof(10, axiom,![X1]:![X2]:(((((((((((((((((~(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))&~(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)=>((((((~(v3_struct_0(X3))&v3_rlvect_1(X3))&v4_rlvect_1(X3))&v5_rlvect_1(X3))&v6_rlvect_1(X3))&v5_vectsp_2(X3,X1))&l1_vectsp_2(X3,X1)))),file('/tmp/SRASS.s.p', dt_m1_rmod_2)).
% fof(69, 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))&v3_vectsp_2(X2,X1))&v5_vectsp_2(X2,X1))&l1_vectsp_2(X2,X1))=>![X3]:(m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))=>![X4]:(m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2)))=>((k1_rmod_5(X1,X2,X3)=X2&r1_tarski(X3,X4))=>k1_rmod_5(X1,X2,X4)=X2))))),file('/tmp/SRASS.s.p', t16_rmod_5)).
% fof(70, 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))&v3_vectsp_2(X2,X1))&v5_vectsp_2(X2,X1))&l1_vectsp_2(X2,X1))=>![X3]:(m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))=>![X4]:(m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2)))=>((k1_rmod_5(X1,X2,X3)=X2&r1_tarski(X3,X4))=>k1_rmod_5(X1,X2,X4)=X2)))))),inference(assume_negation,[status(cth)],[69])).
% fof(73, plain,![X1]:![X2]:![X3]:(((((((((((((((((((((~(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))&~(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_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2))))=>(v3_vectsp_2(k1_rmod_5(X1,X2,X3),X1)&m1_rmod_2(k1_rmod_5(X1,X2,X3),X1,X2))),inference(fof_simplification,[status(thm)],[7,theory(equality)])).
% fof(74, 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))&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)))=>![X4]:(m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2)))=>(r1_tarski(X3,X4)=>m1_rmod_2(k1_rmod_5(X1,X2,X3),X1,k1_rmod_5(X1,X2,X4))))))),inference(fof_simplification,[status(thm)],[8,theory(equality)])).
% fof(75, 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))&v3_vectsp_2(X2,X1))&v5_vectsp_2(X2,X1))&l1_vectsp_2(X2,X1))=>![X3]:((((((((~(v3_struct_0(X3))&v3_rlvect_1(X3))&v4_rlvect_1(X3))&v5_rlvect_1(X3))&v6_rlvect_1(X3))&v3_vectsp_2(X3,X1))&v5_vectsp_2(X3,X1))&l1_vectsp_2(X3,X1))=>((m1_rmod_2(X3,X1,X2)&m1_rmod_2(X2,X1,X3))=>X3=X2)))),inference(fof_simplification,[status(thm)],[9,theory(equality)])).
% fof(76, plain,![X1]:![X2]:(((((((((((((((((~(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))&~(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)=>((((((~(v3_struct_0(X3))&v3_rlvect_1(X3))&v4_rlvect_1(X3))&v5_rlvect_1(X3))&v6_rlvect_1(X3))&v5_vectsp_2(X3,X1))&l1_vectsp_2(X3,X1)))),inference(fof_simplification,[status(thm)],[10,theory(equality)])).
% fof(92, 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))&v3_vectsp_2(X2,X1))&v5_vectsp_2(X2,X1))&l1_vectsp_2(X2,X1))=>![X3]:(m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))=>![X4]:(m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2)))=>((k1_rmod_5(X1,X2,X3)=X2&r1_tarski(X3,X4))=>k1_rmod_5(X1,X2,X4)=X2)))))),inference(fof_simplification,[status(thm)],[70,theory(equality)])).
% fof(128, plain,![X1]:![X2]:![X3]:(((((((((((((((((((((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)))|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_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))))|(v3_vectsp_2(k1_rmod_5(X1,X2,X3),X1)&m1_rmod_2(k1_rmod_5(X1,X2,X3),X1,X2))),inference(fof_nnf,[status(thm)],[73])).
% fof(129, plain,![X4]:![X5]:![X6]:(((((((((((((((((((((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)))|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)))|~(m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X5)))))|(v3_vectsp_2(k1_rmod_5(X4,X5,X6),X4)&m1_rmod_2(k1_rmod_5(X4,X5,X6),X4,X5))),inference(variable_rename,[status(thm)],[128])).
% fof(130, plain,![X4]:![X5]:![X6]:((v3_vectsp_2(k1_rmod_5(X4,X5,X6),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)))|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)))|~(m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X5))))))&(m1_rmod_2(k1_rmod_5(X4,X5,X6),X4,X5)|((((((((((((((((((((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)))|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)))|~(m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X5))))))),inference(distribute,[status(thm)],[129])).
% cnf(131,plain,(v3_struct_0(X2)|v10_vectsp_1(X3)|v3_struct_0(X3)|m1_rmod_2(k1_rmod_5(X3,X2,X1),X3,X2)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X2)))|~l1_vectsp_2(X2,X3)|~v5_vectsp_2(X2,X3)|~v6_rlvect_1(X2)|~v5_rlvect_1(X2)|~v4_rlvect_1(X2)|~v3_rlvect_1(X2)|~l3_vectsp_1(X3)|~v2_vectsp_2(X3)|~v8_vectsp_1(X3)|~v7_vectsp_1(X3)|~v6_vectsp_1(X3)|~v7_group_1(X3)|~v4_group_1(X3)|~v6_rlvect_1(X3)|~v5_rlvect_1(X3)|~v4_rlvect_1(X3)|~v3_rlvect_1(X3)),inference(split_conjunct,[status(thm)],[130])).
% cnf(132,plain,(v3_struct_0(X2)|v10_vectsp_1(X3)|v3_struct_0(X3)|v3_vectsp_2(k1_rmod_5(X3,X2,X1),X3)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X2)))|~l1_vectsp_2(X2,X3)|~v5_vectsp_2(X2,X3)|~v6_rlvect_1(X2)|~v5_rlvect_1(X2)|~v4_rlvect_1(X2)|~v3_rlvect_1(X2)|~l3_vectsp_1(X3)|~v2_vectsp_2(X3)|~v8_vectsp_1(X3)|~v7_vectsp_1(X3)|~v6_vectsp_1(X3)|~v7_group_1(X3)|~v4_group_1(X3)|~v6_rlvect_1(X3)|~v5_rlvect_1(X3)|~v4_rlvect_1(X3)|~v3_rlvect_1(X3)),inference(split_conjunct,[status(thm)],[130])).
% fof(133, 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)))|~(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))))|![X4]:(~(m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2))))|(~(r1_tarski(X3,X4))|m1_rmod_2(k1_rmod_5(X1,X2,X3),X1,k1_rmod_5(X1,X2,X4))))))),inference(fof_nnf,[status(thm)],[74])).
% fof(134, 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)))|~(v7_group_1(X5)))|~(v6_vectsp_1(X5)))|~(v7_vectsp_1(X5)))|~(v8_vectsp_1(X5)))|v10_vectsp_1(X5))|~(v2_vectsp_2(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,k1_zfmisc_1(u1_struct_0(X6))))|![X8]:(~(m1_subset_1(X8,k1_zfmisc_1(u1_struct_0(X6))))|(~(r1_tarski(X7,X8))|m1_rmod_2(k1_rmod_5(X5,X6,X7),X5,k1_rmod_5(X5,X6,X8))))))),inference(variable_rename,[status(thm)],[133])).
% fof(135, plain,![X5]:![X6]:![X7]:![X8]:((((~(m1_subset_1(X8,k1_zfmisc_1(u1_struct_0(X6))))|(~(r1_tarski(X7,X8))|m1_rmod_2(k1_rmod_5(X5,X6,X7),X5,k1_rmod_5(X5,X6,X8))))|~(m1_subset_1(X7,k1_zfmisc_1(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)))|~(v7_group_1(X5)))|~(v6_vectsp_1(X5)))|~(v7_vectsp_1(X5)))|~(v8_vectsp_1(X5)))|v10_vectsp_1(X5))|~(v2_vectsp_2(X5)))|~(l3_vectsp_1(X5)))),inference(shift_quantors,[status(thm)],[134])).
% cnf(136,plain,(v10_vectsp_1(X1)|v3_struct_0(X1)|v3_struct_0(X2)|m1_rmod_2(k1_rmod_5(X1,X2,X3),X1,k1_rmod_5(X1,X2,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)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))|~r1_tarski(X3,X4)|~m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2)))),inference(split_conjunct,[status(thm)],[135])).
% fof(137, 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)))|~(v3_vectsp_2(X2,X1)))|~(v5_vectsp_2(X2,X1)))|~(l1_vectsp_2(X2,X1)))|![X3]:((((((((v3_struct_0(X3)|~(v3_rlvect_1(X3)))|~(v4_rlvect_1(X3)))|~(v5_rlvect_1(X3)))|~(v6_rlvect_1(X3)))|~(v3_vectsp_2(X3,X1)))|~(v5_vectsp_2(X3,X1)))|~(l1_vectsp_2(X3,X1)))|((~(m1_rmod_2(X3,X1,X2))|~(m1_rmod_2(X2,X1,X3)))|X3=X2)))),inference(fof_nnf,[status(thm)],[75])).
% fof(138, 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)))|~(v3_vectsp_2(X5,X4)))|~(v5_vectsp_2(X5,X4)))|~(l1_vectsp_2(X5,X4)))|![X6]:((((((((v3_struct_0(X6)|~(v3_rlvect_1(X6)))|~(v4_rlvect_1(X6)))|~(v5_rlvect_1(X6)))|~(v6_rlvect_1(X6)))|~(v3_vectsp_2(X6,X4)))|~(v5_vectsp_2(X6,X4)))|~(l1_vectsp_2(X6,X4)))|((~(m1_rmod_2(X6,X4,X5))|~(m1_rmod_2(X5,X4,X6)))|X6=X5)))),inference(variable_rename,[status(thm)],[137])).
% fof(139, plain,![X4]:![X5]:![X6]:((((((((((v3_struct_0(X6)|~(v3_rlvect_1(X6)))|~(v4_rlvect_1(X6)))|~(v5_rlvect_1(X6)))|~(v6_rlvect_1(X6)))|~(v3_vectsp_2(X6,X4)))|~(v5_vectsp_2(X6,X4)))|~(l1_vectsp_2(X6,X4)))|((~(m1_rmod_2(X6,X4,X5))|~(m1_rmod_2(X5,X4,X6)))|X6=X5))|(((((((v3_struct_0(X5)|~(v3_rlvect_1(X5)))|~(v4_rlvect_1(X5)))|~(v5_rlvect_1(X5)))|~(v6_rlvect_1(X5)))|~(v3_vectsp_2(X5,X4)))|~(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)],[138])).
% cnf(140,plain,(v3_struct_0(X1)|v3_struct_0(X2)|X3=X2|v3_struct_0(X3)|~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)|~v3_vectsp_2(X2,X1)|~v6_rlvect_1(X2)|~v5_rlvect_1(X2)|~v4_rlvect_1(X2)|~v3_rlvect_1(X2)|~m1_rmod_2(X2,X1,X3)|~m1_rmod_2(X3,X1,X2)|~l1_vectsp_2(X3,X1)|~v5_vectsp_2(X3,X1)|~v3_vectsp_2(X3,X1)|~v6_rlvect_1(X3)|~v5_rlvect_1(X3)|~v4_rlvect_1(X3)|~v3_rlvect_1(X3)),inference(split_conjunct,[status(thm)],[139])).
% fof(141, plain,![X1]:![X2]:(((((((((((((((((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)))|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))|((((((~(v3_struct_0(X3))&v3_rlvect_1(X3))&v4_rlvect_1(X3))&v5_rlvect_1(X3))&v6_rlvect_1(X3))&v5_vectsp_2(X3,X1))&l1_vectsp_2(X3,X1)))),inference(fof_nnf,[status(thm)],[76])).
% fof(142, plain,![X4]:![X5]:(((((((((((((((((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)))|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))|((((((~(v3_struct_0(X6))&v3_rlvect_1(X6))&v4_rlvect_1(X6))&v5_rlvect_1(X6))&v6_rlvect_1(X6))&v5_vectsp_2(X6,X4))&l1_vectsp_2(X6,X4)))),inference(variable_rename,[status(thm)],[141])).
% fof(143, plain,![X4]:![X5]:![X6]:((~(m1_rmod_2(X6,X4,X5))|((((((~(v3_struct_0(X6))&v3_rlvect_1(X6))&v4_rlvect_1(X6))&v5_rlvect_1(X6))&v6_rlvect_1(X6))&v5_vectsp_2(X6,X4))&l1_vectsp_2(X6,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)))|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)))),inference(shift_quantors,[status(thm)],[142])).
% fof(144, plain,![X4]:![X5]:![X6]:((((((((~(v3_struct_0(X6))|~(m1_rmod_2(X6,X4,X5)))|((((((((((((((((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)))|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_rlvect_1(X6)|~(m1_rmod_2(X6,X4,X5)))|((((((((((((((((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)))|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)))))&((v4_rlvect_1(X6)|~(m1_rmod_2(X6,X4,X5)))|((((((((((((((((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)))|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)))))&((v5_rlvect_1(X6)|~(m1_rmod_2(X6,X4,X5)))|((((((((((((((((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)))|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)))))&((v6_rlvect_1(X6)|~(m1_rmod_2(X6,X4,X5)))|((((((((((((((((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)))|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)))))&((v5_vectsp_2(X6,X4)|~(m1_rmod_2(X6,X4,X5)))|((((((((((((((((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)))|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)))))&((l1_vectsp_2(X6,X4)|~(m1_rmod_2(X6,X4,X5)))|((((((((((((((((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)))|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))))),inference(distribute,[status(thm)],[143])).
% cnf(145,plain,(v3_struct_0(X1)|v3_struct_0(X2)|l1_vectsp_2(X3,X2)|~l1_vectsp_2(X1,X2)|~v5_vectsp_2(X1,X2)|~v6_rlvect_1(X1)|~v5_rlvect_1(X1)|~v4_rlvect_1(X1)|~v3_rlvect_1(X1)|~l3_vectsp_1(X2)|~v8_vectsp_1(X2)|~v7_vectsp_1(X2)|~v6_vectsp_1(X2)|~v4_group_1(X2)|~v6_rlvect_1(X2)|~v5_rlvect_1(X2)|~v4_rlvect_1(X2)|~v3_rlvect_1(X2)|~m1_rmod_2(X3,X2,X1)),inference(split_conjunct,[status(thm)],[144])).
% cnf(146,plain,(v3_struct_0(X1)|v3_struct_0(X2)|v5_vectsp_2(X3,X2)|~l1_vectsp_2(X1,X2)|~v5_vectsp_2(X1,X2)|~v6_rlvect_1(X1)|~v5_rlvect_1(X1)|~v4_rlvect_1(X1)|~v3_rlvect_1(X1)|~l3_vectsp_1(X2)|~v8_vectsp_1(X2)|~v7_vectsp_1(X2)|~v6_vectsp_1(X2)|~v4_group_1(X2)|~v6_rlvect_1(X2)|~v5_rlvect_1(X2)|~v4_rlvect_1(X2)|~v3_rlvect_1(X2)|~m1_rmod_2(X3,X2,X1)),inference(split_conjunct,[status(thm)],[144])).
% cnf(147,plain,(v3_struct_0(X1)|v3_struct_0(X2)|v6_rlvect_1(X3)|~l1_vectsp_2(X1,X2)|~v5_vectsp_2(X1,X2)|~v6_rlvect_1(X1)|~v5_rlvect_1(X1)|~v4_rlvect_1(X1)|~v3_rlvect_1(X1)|~l3_vectsp_1(X2)|~v8_vectsp_1(X2)|~v7_vectsp_1(X2)|~v6_vectsp_1(X2)|~v4_group_1(X2)|~v6_rlvect_1(X2)|~v5_rlvect_1(X2)|~v4_rlvect_1(X2)|~v3_rlvect_1(X2)|~m1_rmod_2(X3,X2,X1)),inference(split_conjunct,[status(thm)],[144])).
% cnf(148,plain,(v3_struct_0(X1)|v3_struct_0(X2)|v5_rlvect_1(X3)|~l1_vectsp_2(X1,X2)|~v5_vectsp_2(X1,X2)|~v6_rlvect_1(X1)|~v5_rlvect_1(X1)|~v4_rlvect_1(X1)|~v3_rlvect_1(X1)|~l3_vectsp_1(X2)|~v8_vectsp_1(X2)|~v7_vectsp_1(X2)|~v6_vectsp_1(X2)|~v4_group_1(X2)|~v6_rlvect_1(X2)|~v5_rlvect_1(X2)|~v4_rlvect_1(X2)|~v3_rlvect_1(X2)|~m1_rmod_2(X3,X2,X1)),inference(split_conjunct,[status(thm)],[144])).
% cnf(149,plain,(v3_struct_0(X1)|v3_struct_0(X2)|v4_rlvect_1(X3)|~l1_vectsp_2(X1,X2)|~v5_vectsp_2(X1,X2)|~v6_rlvect_1(X1)|~v5_rlvect_1(X1)|~v4_rlvect_1(X1)|~v3_rlvect_1(X1)|~l3_vectsp_1(X2)|~v8_vectsp_1(X2)|~v7_vectsp_1(X2)|~v6_vectsp_1(X2)|~v4_group_1(X2)|~v6_rlvect_1(X2)|~v5_rlvect_1(X2)|~v4_rlvect_1(X2)|~v3_rlvect_1(X2)|~m1_rmod_2(X3,X2,X1)),inference(split_conjunct,[status(thm)],[144])).
% cnf(150,plain,(v3_struct_0(X1)|v3_struct_0(X2)|v3_rlvect_1(X3)|~l1_vectsp_2(X1,X2)|~v5_vectsp_2(X1,X2)|~v6_rlvect_1(X1)|~v5_rlvect_1(X1)|~v4_rlvect_1(X1)|~v3_rlvect_1(X1)|~l3_vectsp_1(X2)|~v8_vectsp_1(X2)|~v7_vectsp_1(X2)|~v6_vectsp_1(X2)|~v4_group_1(X2)|~v6_rlvect_1(X2)|~v5_rlvect_1(X2)|~v4_rlvect_1(X2)|~v3_rlvect_1(X2)|~m1_rmod_2(X3,X2,X1)),inference(split_conjunct,[status(thm)],[144])).
% cnf(151,plain,(v3_struct_0(X1)|v3_struct_0(X2)|~l1_vectsp_2(X1,X2)|~v5_vectsp_2(X1,X2)|~v6_rlvect_1(X1)|~v5_rlvect_1(X1)|~v4_rlvect_1(X1)|~v3_rlvect_1(X1)|~l3_vectsp_1(X2)|~v8_vectsp_1(X2)|~v7_vectsp_1(X2)|~v6_vectsp_1(X2)|~v4_group_1(X2)|~v6_rlvect_1(X2)|~v5_rlvect_1(X2)|~v4_rlvect_1(X2)|~v3_rlvect_1(X2)|~m1_rmod_2(X3,X2,X1)|~v3_struct_0(X3)),inference(split_conjunct,[status(thm)],[144])).
% fof(365, 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))&v3_vectsp_2(X2,X1))&v5_vectsp_2(X2,X1))&l1_vectsp_2(X2,X1))&?[X3]:(m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))&?[X4]:(m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2)))&((k1_rmod_5(X1,X2,X3)=X2&r1_tarski(X3,X4))&~(k1_rmod_5(X1,X2,X4)=X2)))))),inference(fof_nnf,[status(thm)],[92])).
% fof(366, negated_conjecture,?[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))&v7_group_1(X5))&v6_vectsp_1(X5))&v7_vectsp_1(X5))&v8_vectsp_1(X5))&~(v10_vectsp_1(X5)))&v2_vectsp_2(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))&v3_vectsp_2(X6,X5))&v5_vectsp_2(X6,X5))&l1_vectsp_2(X6,X5))&?[X7]:(m1_subset_1(X7,k1_zfmisc_1(u1_struct_0(X6)))&?[X8]:(m1_subset_1(X8,k1_zfmisc_1(u1_struct_0(X6)))&((k1_rmod_5(X5,X6,X7)=X6&r1_tarski(X7,X8))&~(k1_rmod_5(X5,X6,X8)=X6)))))),inference(variable_rename,[status(thm)],[365])).
% fof(367, negated_conjecture,(((((((((((((~(v3_struct_0(esk25_0))&v3_rlvect_1(esk25_0))&v4_rlvect_1(esk25_0))&v5_rlvect_1(esk25_0))&v6_rlvect_1(esk25_0))&v4_group_1(esk25_0))&v7_group_1(esk25_0))&v6_vectsp_1(esk25_0))&v7_vectsp_1(esk25_0))&v8_vectsp_1(esk25_0))&~(v10_vectsp_1(esk25_0)))&v2_vectsp_2(esk25_0))&l3_vectsp_1(esk25_0))&((((((((~(v3_struct_0(esk26_0))&v3_rlvect_1(esk26_0))&v4_rlvect_1(esk26_0))&v5_rlvect_1(esk26_0))&v6_rlvect_1(esk26_0))&v3_vectsp_2(esk26_0,esk25_0))&v5_vectsp_2(esk26_0,esk25_0))&l1_vectsp_2(esk26_0,esk25_0))&(m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))&(m1_subset_1(esk28_0,k1_zfmisc_1(u1_struct_0(esk26_0)))&((k1_rmod_5(esk25_0,esk26_0,esk27_0)=esk26_0&r1_tarski(esk27_0,esk28_0))&~(k1_rmod_5(esk25_0,esk26_0,esk28_0)=esk26_0)))))),inference(skolemize,[status(esa)],[366])).
% cnf(368,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,esk28_0)!=esk26_0),inference(split_conjunct,[status(thm)],[367])).
% cnf(369,negated_conjecture,(r1_tarski(esk27_0,esk28_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(370,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,esk27_0)=esk26_0),inference(split_conjunct,[status(thm)],[367])).
% cnf(371,negated_conjecture,(m1_subset_1(esk28_0,k1_zfmisc_1(u1_struct_0(esk26_0)))),inference(split_conjunct,[status(thm)],[367])).
% cnf(372,negated_conjecture,(m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))),inference(split_conjunct,[status(thm)],[367])).
% cnf(373,negated_conjecture,(l1_vectsp_2(esk26_0,esk25_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(374,negated_conjecture,(v5_vectsp_2(esk26_0,esk25_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(376,negated_conjecture,(v6_rlvect_1(esk26_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(377,negated_conjecture,(v5_rlvect_1(esk26_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(378,negated_conjecture,(v4_rlvect_1(esk26_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(379,negated_conjecture,(v3_rlvect_1(esk26_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(380,negated_conjecture,(~v3_struct_0(esk26_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(381,negated_conjecture,(l3_vectsp_1(esk25_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(382,negated_conjecture,(v2_vectsp_2(esk25_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(383,negated_conjecture,(~v10_vectsp_1(esk25_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(384,negated_conjecture,(v8_vectsp_1(esk25_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(385,negated_conjecture,(v7_vectsp_1(esk25_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(386,negated_conjecture,(v6_vectsp_1(esk25_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(387,negated_conjecture,(v7_group_1(esk25_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(388,negated_conjecture,(v4_group_1(esk25_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(389,negated_conjecture,(v6_rlvect_1(esk25_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(390,negated_conjecture,(v5_rlvect_1(esk25_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(391,negated_conjecture,(v4_rlvect_1(esk25_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(392,negated_conjecture,(v3_rlvect_1(esk25_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(393,negated_conjecture,(~v3_struct_0(esk25_0)),inference(split_conjunct,[status(thm)],[367])).
% cnf(395,plain,(X2=X3|v3_struct_0(X3)|v3_struct_0(X2)|v3_struct_0(X1)|~m1_rmod_2(X3,X1,X2)|~m1_rmod_2(X2,X1,X3)|~v5_vectsp_2(X3,X1)|~v3_vectsp_2(X3,X1)|~v3_vectsp_2(X2,X1)|~l1_vectsp_2(X3,X1)|~l1_vectsp_2(X2,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X3)|~v6_rlvect_1(X2)|~v6_rlvect_1(X1)|~v5_rlvect_1(X3)|~v5_rlvect_1(X2)|~v5_rlvect_1(X1)|~v4_rlvect_1(X3)|~v4_rlvect_1(X2)|~v4_rlvect_1(X1)|~v3_rlvect_1(X3)|~v3_rlvect_1(X2)|~v3_rlvect_1(X1)|~l3_vectsp_1(X1)),inference(csr,[status(thm)],[140,146])).
% cnf(396,plain,(X2=X3|v3_struct_0(X3)|v3_struct_0(X2)|v3_struct_0(X1)|~m1_rmod_2(X3,X1,X2)|~m1_rmod_2(X2,X1,X3)|~v5_vectsp_2(X3,X1)|~v3_vectsp_2(X3,X1)|~v3_vectsp_2(X2,X1)|~l1_vectsp_2(X3,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X3)|~v6_rlvect_1(X2)|~v6_rlvect_1(X1)|~v5_rlvect_1(X3)|~v5_rlvect_1(X2)|~v5_rlvect_1(X1)|~v4_rlvect_1(X3)|~v4_rlvect_1(X2)|~v4_rlvect_1(X1)|~v3_rlvect_1(X3)|~v3_rlvect_1(X2)|~v3_rlvect_1(X1)|~l3_vectsp_1(X1)),inference(csr,[status(thm)],[395,145])).
% cnf(397,plain,(X2=X3|v3_struct_0(X3)|v3_struct_0(X2)|v3_struct_0(X1)|~m1_rmod_2(X3,X1,X2)|~m1_rmod_2(X2,X1,X3)|~v5_vectsp_2(X3,X1)|~v3_vectsp_2(X3,X1)|~v3_vectsp_2(X2,X1)|~l1_vectsp_2(X3,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X1)|~v6_rlvect_1(X3)|~v5_rlvect_1(X3)|~v5_rlvect_1(X2)|~v5_rlvect_1(X1)|~v4_rlvect_1(X3)|~v4_rlvect_1(X2)|~v4_rlvect_1(X1)|~v3_rlvect_1(X3)|~v3_rlvect_1(X2)|~v3_rlvect_1(X1)|~l3_vectsp_1(X1)),inference(csr,[status(thm)],[396,147])).
% cnf(398,plain,(X2=X3|v3_struct_0(X3)|v3_struct_0(X2)|v3_struct_0(X1)|~m1_rmod_2(X3,X1,X2)|~m1_rmod_2(X2,X1,X3)|~v5_vectsp_2(X3,X1)|~v3_vectsp_2(X3,X1)|~v3_vectsp_2(X2,X1)|~l1_vectsp_2(X3,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X3)|~v6_rlvect_1(X1)|~v5_rlvect_1(X1)|~v5_rlvect_1(X3)|~v4_rlvect_1(X3)|~v4_rlvect_1(X2)|~v4_rlvect_1(X1)|~v3_rlvect_1(X3)|~v3_rlvect_1(X2)|~v3_rlvect_1(X1)|~l3_vectsp_1(X1)),inference(csr,[status(thm)],[397,148])).
% cnf(399,plain,(X2=X3|v3_struct_0(X3)|v3_struct_0(X2)|v3_struct_0(X1)|~m1_rmod_2(X3,X1,X2)|~m1_rmod_2(X2,X1,X3)|~v5_vectsp_2(X3,X1)|~v3_vectsp_2(X3,X1)|~v3_vectsp_2(X2,X1)|~l1_vectsp_2(X3,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X3)|~v6_rlvect_1(X1)|~v5_rlvect_1(X3)|~v5_rlvect_1(X1)|~v4_rlvect_1(X1)|~v4_rlvect_1(X3)|~v3_rlvect_1(X3)|~v3_rlvect_1(X2)|~v3_rlvect_1(X1)|~l3_vectsp_1(X1)),inference(csr,[status(thm)],[398,149])).
% cnf(400,plain,(X2=X3|v3_struct_0(X3)|v3_struct_0(X2)|v3_struct_0(X1)|~m1_rmod_2(X3,X1,X2)|~m1_rmod_2(X2,X1,X3)|~v5_vectsp_2(X3,X1)|~v3_vectsp_2(X3,X1)|~v3_vectsp_2(X2,X1)|~l1_vectsp_2(X3,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X3)|~v6_rlvect_1(X1)|~v5_rlvect_1(X3)|~v5_rlvect_1(X1)|~v4_rlvect_1(X3)|~v4_rlvect_1(X1)|~v3_rlvect_1(X1)|~v3_rlvect_1(X3)|~l3_vectsp_1(X1)),inference(csr,[status(thm)],[399,150])).
% cnf(401,plain,(X2=X3|v3_struct_0(X3)|v3_struct_0(X1)|~m1_rmod_2(X3,X1,X2)|~m1_rmod_2(X2,X1,X3)|~v5_vectsp_2(X3,X1)|~v3_vectsp_2(X3,X1)|~v3_vectsp_2(X2,X1)|~l1_vectsp_2(X3,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X3)|~v6_rlvect_1(X1)|~v5_rlvect_1(X3)|~v5_rlvect_1(X1)|~v4_rlvect_1(X3)|~v4_rlvect_1(X1)|~v3_rlvect_1(X3)|~v3_rlvect_1(X1)|~l3_vectsp_1(X1)),inference(csr,[status(thm)],[400,151])).
% cnf(529,plain,(v3_struct_0(X1)|v3_struct_0(X2)|v10_vectsp_1(X1)|~v5_vectsp_2(X2,X1)|~l1_vectsp_2(X2,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X1)|~v6_rlvect_1(X2)|~v5_rlvect_1(X1)|~v5_rlvect_1(X2)|~v4_rlvect_1(X1)|~v4_rlvect_1(X2)|~v3_rlvect_1(X1)|~v3_rlvect_1(X2)|~v3_struct_0(k1_rmod_5(X1,X2,X3))|~l3_vectsp_1(X1)|~v2_vectsp_2(X1)|~v7_group_1(X1)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))),inference(spm,[status(thm)],[151,131,theory(equality)])).
% cnf(530,plain,(v3_rlvect_1(k1_rmod_5(X1,X2,X3))|v3_struct_0(X1)|v3_struct_0(X2)|v10_vectsp_1(X1)|~v5_vectsp_2(X2,X1)|~l1_vectsp_2(X2,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X1)|~v6_rlvect_1(X2)|~v5_rlvect_1(X1)|~v5_rlvect_1(X2)|~v4_rlvect_1(X1)|~v4_rlvect_1(X2)|~v3_rlvect_1(X1)|~v3_rlvect_1(X2)|~l3_vectsp_1(X1)|~v2_vectsp_2(X1)|~v7_group_1(X1)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))),inference(spm,[status(thm)],[150,131,theory(equality)])).
% cnf(531,plain,(v4_rlvect_1(k1_rmod_5(X1,X2,X3))|v3_struct_0(X1)|v3_struct_0(X2)|v10_vectsp_1(X1)|~v5_vectsp_2(X2,X1)|~l1_vectsp_2(X2,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X1)|~v6_rlvect_1(X2)|~v5_rlvect_1(X1)|~v5_rlvect_1(X2)|~v4_rlvect_1(X1)|~v4_rlvect_1(X2)|~v3_rlvect_1(X1)|~v3_rlvect_1(X2)|~l3_vectsp_1(X1)|~v2_vectsp_2(X1)|~v7_group_1(X1)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))),inference(spm,[status(thm)],[149,131,theory(equality)])).
% cnf(532,plain,(v5_rlvect_1(k1_rmod_5(X1,X2,X3))|v3_struct_0(X1)|v3_struct_0(X2)|v10_vectsp_1(X1)|~v5_vectsp_2(X2,X1)|~l1_vectsp_2(X2,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X1)|~v6_rlvect_1(X2)|~v5_rlvect_1(X1)|~v5_rlvect_1(X2)|~v4_rlvect_1(X1)|~v4_rlvect_1(X2)|~v3_rlvect_1(X1)|~v3_rlvect_1(X2)|~l3_vectsp_1(X1)|~v2_vectsp_2(X1)|~v7_group_1(X1)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))),inference(spm,[status(thm)],[148,131,theory(equality)])).
% cnf(533,plain,(v6_rlvect_1(k1_rmod_5(X1,X2,X3))|v3_struct_0(X1)|v3_struct_0(X2)|v10_vectsp_1(X1)|~v5_vectsp_2(X2,X1)|~l1_vectsp_2(X2,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X1)|~v6_rlvect_1(X2)|~v5_rlvect_1(X1)|~v5_rlvect_1(X2)|~v4_rlvect_1(X1)|~v4_rlvect_1(X2)|~v3_rlvect_1(X1)|~v3_rlvect_1(X2)|~l3_vectsp_1(X1)|~v2_vectsp_2(X1)|~v7_group_1(X1)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))),inference(spm,[status(thm)],[147,131,theory(equality)])).
% cnf(534,plain,(l1_vectsp_2(k1_rmod_5(X1,X2,X3),X1)|v3_struct_0(X1)|v3_struct_0(X2)|v10_vectsp_1(X1)|~v5_vectsp_2(X2,X1)|~l1_vectsp_2(X2,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X1)|~v6_rlvect_1(X2)|~v5_rlvect_1(X1)|~v5_rlvect_1(X2)|~v4_rlvect_1(X1)|~v4_rlvect_1(X2)|~v3_rlvect_1(X1)|~v3_rlvect_1(X2)|~l3_vectsp_1(X1)|~v2_vectsp_2(X1)|~v7_group_1(X1)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))),inference(spm,[status(thm)],[145,131,theory(equality)])).
% cnf(535,plain,(v5_vectsp_2(k1_rmod_5(X1,X2,X3),X1)|v3_struct_0(X1)|v3_struct_0(X2)|v10_vectsp_1(X1)|~v5_vectsp_2(X2,X1)|~l1_vectsp_2(X2,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X1)|~v6_rlvect_1(X2)|~v5_rlvect_1(X1)|~v5_rlvect_1(X2)|~v4_rlvect_1(X1)|~v4_rlvect_1(X2)|~v3_rlvect_1(X1)|~v3_rlvect_1(X2)|~l3_vectsp_1(X1)|~v2_vectsp_2(X1)|~v7_group_1(X1)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))),inference(spm,[status(thm)],[146,131,theory(equality)])).
% cnf(573,plain,(k1_rmod_5(X1,X2,X3)=k1_rmod_5(X1,X2,X4)|v3_struct_0(k1_rmod_5(X1,X2,X4))|v3_struct_0(X1)|v10_vectsp_1(X1)|v3_struct_0(X2)|~m1_rmod_2(k1_rmod_5(X1,X2,X3),X1,k1_rmod_5(X1,X2,X4))|~v5_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~v3_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~v3_vectsp_2(k1_rmod_5(X1,X2,X3),X1)|~l1_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(k1_rmod_5(X1,X2,X4))|~v6_rlvect_1(X1)|~v5_rlvect_1(k1_rmod_5(X1,X2,X4))|~v5_rlvect_1(X1)|~v4_rlvect_1(k1_rmod_5(X1,X2,X4))|~v4_rlvect_1(X1)|~v3_rlvect_1(k1_rmod_5(X1,X2,X4))|~v3_rlvect_1(X1)|~l3_vectsp_1(X1)|~v2_vectsp_2(X1)|~v7_group_1(X1)|~r1_tarski(X4,X3)|~v5_vectsp_2(X2,X1)|~l1_vectsp_2(X2,X1)|~v6_rlvect_1(X2)|~v5_rlvect_1(X2)|~v4_rlvect_1(X2)|~v3_rlvect_1(X2)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))|~m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2)))),inference(spm,[status(thm)],[401,136,theory(equality)])).
% cnf(3254,plain,(k1_rmod_5(X1,X2,X3)=k1_rmod_5(X1,X2,X4)|v10_vectsp_1(X1)|v3_struct_0(k1_rmod_5(X1,X2,X4))|v3_struct_0(X1)|v3_struct_0(X2)|~m1_rmod_2(k1_rmod_5(X1,X2,X3),X1,k1_rmod_5(X1,X2,X4))|~v2_vectsp_2(X1)|~v7_group_1(X1)|~r1_tarski(X4,X3)|~v5_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~v5_vectsp_2(X2,X1)|~v3_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~v3_vectsp_2(k1_rmod_5(X1,X2,X3),X1)|~l1_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~l1_vectsp_2(X2,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(k1_rmod_5(X1,X2,X4))|~v6_rlvect_1(X2)|~v6_rlvect_1(X1)|~v5_rlvect_1(k1_rmod_5(X1,X2,X4))|~v5_rlvect_1(X2)|~v5_rlvect_1(X1)|~v4_rlvect_1(k1_rmod_5(X1,X2,X4))|~v4_rlvect_1(X2)|~v4_rlvect_1(X1)|~v3_rlvect_1(X1)|~v3_rlvect_1(X2)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))|~m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2)))|~l3_vectsp_1(X1)),inference(csr,[status(thm)],[573,530])).
% cnf(3255,plain,(k1_rmod_5(X1,X2,X3)=k1_rmod_5(X1,X2,X4)|v10_vectsp_1(X1)|v3_struct_0(k1_rmod_5(X1,X2,X4))|v3_struct_0(X1)|v3_struct_0(X2)|~m1_rmod_2(k1_rmod_5(X1,X2,X3),X1,k1_rmod_5(X1,X2,X4))|~v2_vectsp_2(X1)|~v7_group_1(X1)|~r1_tarski(X4,X3)|~v5_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~v5_vectsp_2(X2,X1)|~v3_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~v3_vectsp_2(k1_rmod_5(X1,X2,X3),X1)|~l1_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~l1_vectsp_2(X2,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(k1_rmod_5(X1,X2,X4))|~v6_rlvect_1(X2)|~v6_rlvect_1(X1)|~v5_rlvect_1(k1_rmod_5(X1,X2,X4))|~v5_rlvect_1(X2)|~v5_rlvect_1(X1)|~v4_rlvect_1(X1)|~v4_rlvect_1(X2)|~v3_rlvect_1(X1)|~v3_rlvect_1(X2)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))|~m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2)))|~l3_vectsp_1(X1)),inference(csr,[status(thm)],[3254,531])).
% cnf(3256,plain,(k1_rmod_5(X1,X2,X3)=k1_rmod_5(X1,X2,X4)|v10_vectsp_1(X1)|v3_struct_0(k1_rmod_5(X1,X2,X4))|v3_struct_0(X1)|v3_struct_0(X2)|~m1_rmod_2(k1_rmod_5(X1,X2,X3),X1,k1_rmod_5(X1,X2,X4))|~v2_vectsp_2(X1)|~v7_group_1(X1)|~r1_tarski(X4,X3)|~v5_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~v5_vectsp_2(X2,X1)|~v3_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~v3_vectsp_2(k1_rmod_5(X1,X2,X3),X1)|~l1_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~l1_vectsp_2(X2,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(k1_rmod_5(X1,X2,X4))|~v6_rlvect_1(X2)|~v6_rlvect_1(X1)|~v5_rlvect_1(X1)|~v5_rlvect_1(X2)|~v4_rlvect_1(X1)|~v4_rlvect_1(X2)|~v3_rlvect_1(X1)|~v3_rlvect_1(X2)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))|~m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2)))|~l3_vectsp_1(X1)),inference(csr,[status(thm)],[3255,532])).
% cnf(3257,plain,(k1_rmod_5(X1,X2,X3)=k1_rmod_5(X1,X2,X4)|v10_vectsp_1(X1)|v3_struct_0(k1_rmod_5(X1,X2,X4))|v3_struct_0(X1)|v3_struct_0(X2)|~m1_rmod_2(k1_rmod_5(X1,X2,X3),X1,k1_rmod_5(X1,X2,X4))|~v2_vectsp_2(X1)|~v7_group_1(X1)|~r1_tarski(X4,X3)|~v5_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~v5_vectsp_2(X2,X1)|~v3_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~v3_vectsp_2(k1_rmod_5(X1,X2,X3),X1)|~l1_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~l1_vectsp_2(X2,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X1)|~v6_rlvect_1(X2)|~v5_rlvect_1(X1)|~v5_rlvect_1(X2)|~v4_rlvect_1(X1)|~v4_rlvect_1(X2)|~v3_rlvect_1(X1)|~v3_rlvect_1(X2)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))|~m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2)))|~l3_vectsp_1(X1)),inference(csr,[status(thm)],[3256,533])).
% cnf(3258,plain,(k1_rmod_5(X1,X2,X3)=k1_rmod_5(X1,X2,X4)|v10_vectsp_1(X1)|v3_struct_0(k1_rmod_5(X1,X2,X4))|v3_struct_0(X1)|v3_struct_0(X2)|~m1_rmod_2(k1_rmod_5(X1,X2,X3),X1,k1_rmod_5(X1,X2,X4))|~v2_vectsp_2(X1)|~v7_group_1(X1)|~r1_tarski(X4,X3)|~v5_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~v5_vectsp_2(X2,X1)|~v3_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~v3_vectsp_2(k1_rmod_5(X1,X2,X3),X1)|~l1_vectsp_2(X2,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X1)|~v6_rlvect_1(X2)|~v5_rlvect_1(X1)|~v5_rlvect_1(X2)|~v4_rlvect_1(X1)|~v4_rlvect_1(X2)|~v3_rlvect_1(X1)|~v3_rlvect_1(X2)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))|~m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2)))|~l3_vectsp_1(X1)),inference(csr,[status(thm)],[3257,534])).
% cnf(3259,plain,(k1_rmod_5(X1,X2,X3)=k1_rmod_5(X1,X2,X4)|v10_vectsp_1(X1)|v3_struct_0(k1_rmod_5(X1,X2,X4))|v3_struct_0(X1)|v3_struct_0(X2)|~m1_rmod_2(k1_rmod_5(X1,X2,X3),X1,k1_rmod_5(X1,X2,X4))|~v2_vectsp_2(X1)|~v7_group_1(X1)|~r1_tarski(X4,X3)|~v5_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~v5_vectsp_2(X2,X1)|~v3_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~l1_vectsp_2(X2,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X1)|~v6_rlvect_1(X2)|~v5_rlvect_1(X1)|~v5_rlvect_1(X2)|~v4_rlvect_1(X1)|~v4_rlvect_1(X2)|~v3_rlvect_1(X1)|~v3_rlvect_1(X2)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))|~m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2)))|~l3_vectsp_1(X1)),inference(csr,[status(thm)],[3258,132])).
% cnf(3260,plain,(k1_rmod_5(X1,X2,X3)=k1_rmod_5(X1,X2,X4)|v10_vectsp_1(X1)|v3_struct_0(k1_rmod_5(X1,X2,X4))|v3_struct_0(X1)|v3_struct_0(X2)|~m1_rmod_2(k1_rmod_5(X1,X2,X3),X1,k1_rmod_5(X1,X2,X4))|~v2_vectsp_2(X1)|~v7_group_1(X1)|~r1_tarski(X4,X3)|~v5_vectsp_2(k1_rmod_5(X1,X2,X4),X1)|~v5_vectsp_2(X2,X1)|~l1_vectsp_2(X2,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X1)|~v6_rlvect_1(X2)|~v5_rlvect_1(X1)|~v5_rlvect_1(X2)|~v4_rlvect_1(X1)|~v4_rlvect_1(X2)|~v3_rlvect_1(X1)|~v3_rlvect_1(X2)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))|~m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2)))|~l3_vectsp_1(X1)),inference(csr,[status(thm)],[3259,132])).
% cnf(3261,plain,(k1_rmod_5(X1,X2,X3)=k1_rmod_5(X1,X2,X4)|v10_vectsp_1(X1)|v3_struct_0(k1_rmod_5(X1,X2,X4))|v3_struct_0(X1)|v3_struct_0(X2)|~m1_rmod_2(k1_rmod_5(X1,X2,X3),X1,k1_rmod_5(X1,X2,X4))|~v2_vectsp_2(X1)|~v7_group_1(X1)|~r1_tarski(X4,X3)|~v5_vectsp_2(X2,X1)|~l1_vectsp_2(X2,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X1)|~v6_rlvect_1(X2)|~v5_rlvect_1(X1)|~v5_rlvect_1(X2)|~v4_rlvect_1(X1)|~v4_rlvect_1(X2)|~v3_rlvect_1(X1)|~v3_rlvect_1(X2)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))|~m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2)))|~l3_vectsp_1(X1)),inference(csr,[status(thm)],[3260,535])).
% cnf(3262,plain,(k1_rmod_5(X1,X2,X3)=k1_rmod_5(X1,X2,X4)|v10_vectsp_1(X1)|v3_struct_0(X2)|v3_struct_0(X1)|~m1_rmod_2(k1_rmod_5(X1,X2,X3),X1,k1_rmod_5(X1,X2,X4))|~v2_vectsp_2(X1)|~v7_group_1(X1)|~r1_tarski(X4,X3)|~v5_vectsp_2(X2,X1)|~l1_vectsp_2(X2,X1)|~v8_vectsp_1(X1)|~v7_vectsp_1(X1)|~v6_vectsp_1(X1)|~v4_group_1(X1)|~v6_rlvect_1(X1)|~v6_rlvect_1(X2)|~v5_rlvect_1(X1)|~v5_rlvect_1(X2)|~v4_rlvect_1(X1)|~v4_rlvect_1(X2)|~v3_rlvect_1(X1)|~v3_rlvect_1(X2)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))|~m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2)))|~l3_vectsp_1(X1)),inference(csr,[status(thm)],[3261,529])).
% cnf(3263,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|~v2_vectsp_2(esk25_0)|~v7_group_1(esk25_0)|~r1_tarski(esk27_0,X1)|~v5_vectsp_2(esk26_0,esk25_0)|~l1_vectsp_2(esk26_0,esk25_0)|~v8_vectsp_1(esk25_0)|~v7_vectsp_1(esk25_0)|~v6_vectsp_1(esk25_0)|~v4_group_1(esk25_0)|~v6_rlvect_1(esk25_0)|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|~m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|~l3_vectsp_1(esk25_0)),inference(spm,[status(thm)],[3262,370,theory(equality)])).
% cnf(3268,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|$false|~v7_group_1(esk25_0)|~r1_tarski(esk27_0,X1)|~v5_vectsp_2(esk26_0,esk25_0)|~l1_vectsp_2(esk26_0,esk25_0)|~v8_vectsp_1(esk25_0)|~v7_vectsp_1(esk25_0)|~v6_vectsp_1(esk25_0)|~v4_group_1(esk25_0)|~v6_rlvect_1(esk25_0)|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|~m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3263,382,theory(equality)])).
% cnf(3269,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|$false|$false|~r1_tarski(esk27_0,X1)|~v5_vectsp_2(esk26_0,esk25_0)|~l1_vectsp_2(esk26_0,esk25_0)|~v8_vectsp_1(esk25_0)|~v7_vectsp_1(esk25_0)|~v6_vectsp_1(esk25_0)|~v4_group_1(esk25_0)|~v6_rlvect_1(esk25_0)|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|~m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3268,387,theory(equality)])).
% cnf(3270,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|$false|$false|~r1_tarski(esk27_0,X1)|$false|~l1_vectsp_2(esk26_0,esk25_0)|~v8_vectsp_1(esk25_0)|~v7_vectsp_1(esk25_0)|~v6_vectsp_1(esk25_0)|~v4_group_1(esk25_0)|~v6_rlvect_1(esk25_0)|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|~m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3269,374,theory(equality)])).
% cnf(3271,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|$false|$false|~r1_tarski(esk27_0,X1)|$false|$false|~v8_vectsp_1(esk25_0)|~v7_vectsp_1(esk25_0)|~v6_vectsp_1(esk25_0)|~v4_group_1(esk25_0)|~v6_rlvect_1(esk25_0)|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|~m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3270,373,theory(equality)])).
% cnf(3272,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|$false|$false|~r1_tarski(esk27_0,X1)|$false|$false|$false|~v7_vectsp_1(esk25_0)|~v6_vectsp_1(esk25_0)|~v4_group_1(esk25_0)|~v6_rlvect_1(esk25_0)|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|~m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3271,384,theory(equality)])).
% cnf(3273,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|$false|$false|~r1_tarski(esk27_0,X1)|$false|$false|$false|$false|~v6_vectsp_1(esk25_0)|~v4_group_1(esk25_0)|~v6_rlvect_1(esk25_0)|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|~m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3272,385,theory(equality)])).
% cnf(3274,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|$false|$false|~r1_tarski(esk27_0,X1)|$false|$false|$false|$false|$false|~v4_group_1(esk25_0)|~v6_rlvect_1(esk25_0)|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|~m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3273,386,theory(equality)])).
% cnf(3275,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|$false|$false|~r1_tarski(esk27_0,X1)|$false|$false|$false|$false|$false|$false|~v6_rlvect_1(esk25_0)|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|~m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3274,388,theory(equality)])).
% cnf(3276,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|$false|$false|~r1_tarski(esk27_0,X1)|$false|$false|$false|$false|$false|$false|$false|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|~m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3275,389,theory(equality)])).
% cnf(3277,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|$false|$false|~r1_tarski(esk27_0,X1)|$false|$false|$false|$false|$false|$false|$false|$false|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|~m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3276,376,theory(equality)])).
% cnf(3278,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|$false|$false|~r1_tarski(esk27_0,X1)|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|~m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3277,390,theory(equality)])).
% cnf(3279,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|$false|$false|~r1_tarski(esk27_0,X1)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|~m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3278,377,theory(equality)])).
% cnf(3280,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|$false|$false|~r1_tarski(esk27_0,X1)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|~m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3279,391,theory(equality)])).
% cnf(3281,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|$false|$false|~r1_tarski(esk27_0,X1)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|~m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3280,378,theory(equality)])).
% cnf(3282,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|$false|$false|~r1_tarski(esk27_0,X1)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v3_rlvect_1(esk26_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|~m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3281,392,theory(equality)])).
% cnf(3283,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|$false|$false|~r1_tarski(esk27_0,X1)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|~m1_subset_1(esk27_0,k1_zfmisc_1(u1_struct_0(esk26_0)))|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3282,379,theory(equality)])).
% cnf(3284,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|$false|$false|~r1_tarski(esk27_0,X1)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3283,372,theory(equality)])).
% cnf(3285,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|$false|$false|~r1_tarski(esk27_0,X1)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false|$false),inference(rw,[status(thm)],[3284,381,theory(equality)])).
% cnf(3286,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))),inference(cn,[status(thm)],[3285,theory(equality)])).
% cnf(3287,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v3_struct_0(esk26_0)|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))),inference(sr,[status(thm)],[3286,383,theory(equality)])).
% cnf(3288,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v3_struct_0(esk25_0)|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))),inference(sr,[status(thm)],[3287,380,theory(equality)])).
% cnf(3289,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|~m1_rmod_2(k1_rmod_5(esk25_0,esk26_0,X1),esk25_0,esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))),inference(sr,[status(thm)],[3288,393,theory(equality)])).
% cnf(3544,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|~v2_vectsp_2(esk25_0)|~v7_group_1(esk25_0)|~v5_vectsp_2(esk26_0,esk25_0)|~l1_vectsp_2(esk26_0,esk25_0)|~v8_vectsp_1(esk25_0)|~v7_vectsp_1(esk25_0)|~v6_vectsp_1(esk25_0)|~v4_group_1(esk25_0)|~v6_rlvect_1(esk25_0)|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~l3_vectsp_1(esk25_0)),inference(spm,[status(thm)],[3289,131,theory(equality)])).
% cnf(3546,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false|~v7_group_1(esk25_0)|~v5_vectsp_2(esk26_0,esk25_0)|~l1_vectsp_2(esk26_0,esk25_0)|~v8_vectsp_1(esk25_0)|~v7_vectsp_1(esk25_0)|~v6_vectsp_1(esk25_0)|~v4_group_1(esk25_0)|~v6_rlvect_1(esk25_0)|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3544,382,theory(equality)])).
% cnf(3547,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false|$false|~v5_vectsp_2(esk26_0,esk25_0)|~l1_vectsp_2(esk26_0,esk25_0)|~v8_vectsp_1(esk25_0)|~v7_vectsp_1(esk25_0)|~v6_vectsp_1(esk25_0)|~v4_group_1(esk25_0)|~v6_rlvect_1(esk25_0)|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3546,387,theory(equality)])).
% cnf(3548,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false|$false|$false|~l1_vectsp_2(esk26_0,esk25_0)|~v8_vectsp_1(esk25_0)|~v7_vectsp_1(esk25_0)|~v6_vectsp_1(esk25_0)|~v4_group_1(esk25_0)|~v6_rlvect_1(esk25_0)|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3547,374,theory(equality)])).
% cnf(3549,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false|$false|$false|$false|~v8_vectsp_1(esk25_0)|~v7_vectsp_1(esk25_0)|~v6_vectsp_1(esk25_0)|~v4_group_1(esk25_0)|~v6_rlvect_1(esk25_0)|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3548,373,theory(equality)])).
% cnf(3550,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false|$false|$false|$false|$false|~v7_vectsp_1(esk25_0)|~v6_vectsp_1(esk25_0)|~v4_group_1(esk25_0)|~v6_rlvect_1(esk25_0)|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3549,384,theory(equality)])).
% cnf(3551,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false|$false|$false|$false|$false|$false|~v6_vectsp_1(esk25_0)|~v4_group_1(esk25_0)|~v6_rlvect_1(esk25_0)|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3550,385,theory(equality)])).
% cnf(3552,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false|$false|$false|$false|$false|$false|$false|~v4_group_1(esk25_0)|~v6_rlvect_1(esk25_0)|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3551,386,theory(equality)])).
% cnf(3553,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false|$false|$false|$false|$false|$false|$false|$false|~v6_rlvect_1(esk25_0)|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3552,388,theory(equality)])).
% cnf(3554,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v6_rlvect_1(esk26_0)|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3553,389,theory(equality)])).
% cnf(3555,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v5_rlvect_1(esk25_0)|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3554,376,theory(equality)])).
% cnf(3556,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v5_rlvect_1(esk26_0)|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3555,390,theory(equality)])).
% cnf(3557,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v4_rlvect_1(esk25_0)|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3556,377,theory(equality)])).
% cnf(3558,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v4_rlvect_1(esk26_0)|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3557,391,theory(equality)])).
% cnf(3559,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v3_rlvect_1(esk25_0)|~v3_rlvect_1(esk26_0)|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3558,378,theory(equality)])).
% cnf(3560,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v3_rlvect_1(esk26_0)|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3559,392,theory(equality)])).
% cnf(3561,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~l3_vectsp_1(esk25_0)),inference(rw,[status(thm)],[3560,379,theory(equality)])).
% cnf(3562,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[3561,381,theory(equality)])).
% cnf(3563,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v10_vectsp_1(esk25_0)|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))),inference(cn,[status(thm)],[3562,theory(equality)])).
% cnf(3564,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v3_struct_0(esk25_0)|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))),inference(sr,[status(thm)],[3563,383,theory(equality)])).
% cnf(3565,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|v3_struct_0(esk26_0)|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))),inference(sr,[status(thm)],[3564,393,theory(equality)])).
% cnf(3566,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,X1)=esk26_0|~r1_tarski(esk27_0,X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk26_0)))),inference(sr,[status(thm)],[3565,380,theory(equality)])).
% cnf(3571,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,esk28_0)=esk26_0|~r1_tarski(esk27_0,esk28_0)),inference(spm,[status(thm)],[3566,371,theory(equality)])).
% cnf(3587,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,esk28_0)=esk26_0|$false),inference(rw,[status(thm)],[3571,369,theory(equality)])).
% cnf(3588,negated_conjecture,(k1_rmod_5(esk25_0,esk26_0,esk28_0)=esk26_0),inference(cn,[status(thm)],[3587,theory(equality)])).
% cnf(3589,negated_conjecture,($false),inference(sr,[status(thm)],[3588,368,theory(equality)])).
% cnf(3590,negated_conjecture,($false),3589,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 847
% # ...of these trivial : 3
% # ...subsumed : 235
% # ...remaining for further processing: 609
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 3
% # Backward-rewritten : 72
% # Generated clauses : 1228
% # ...of the previous two non-trivial : 984
% # Contextual simplify-reflections : 199
% # Paramodulations : 1220
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 395
% # Positive orientable unit clauses: 85
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 20
% # Non-unit-clauses : 290
% # Current number of unprocessed clauses: 285
% # ...number of literals in the above : 2613
% # Clause-clause subsumption calls (NU) : 18873
% # Rec. Clause-clause subsumption calls : 6680
% # Unit Clause-clause subsumption calls : 996
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 12
% # Indexed BW rewrite successes : 5
% # Backwards rewriting index: 365 leaves, 1.58+/-1.427 terms/leaf
% # Paramod-from index: 182 leaves, 1.22+/-0.875 terms/leaf
% # Paramod-into index: 311 leaves, 1.34+/-0.989 terms/leaf
% # -------------------------------------------------
% # User time : 0.180 s
% # System time : 0.011 s
% # Total time : 0.191 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.35 CPU 0.44 WC
% FINAL PrfWatch: 0.35 CPU 0.44 WC
% SZS output end Solution for /tmp/SystemOnTPTP9302/ALG220+1.tptp
%
%------------------------------------------------------------------------------