%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : ALG214+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Thu Jul 14 17:22:00 EDT 2022
% Result : Theorem 232.62s 224.31s
% Output : Proof 232.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ALG214+1 : TPTP v8.1.0. Released v3.4.0.
% 0.07/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n026.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Wed Jun 8 12:05:17 EDT 2022
% 0.12/0.34 % CPUTime :
% 232.62/224.31 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 232.62/224.32 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 232.68/224.33
% 232.68/224.33 %-----------------------------------------------------
% 232.68/224.33 fof(t2_rmod_5, conjecture, ! [_145472] : (~ v3_struct_0(_145472) & v3_rlvect_1(_145472) & v4_rlvect_1(_145472) & v5_rlvect_1(_145472) & v6_rlvect_1(_145472) & v4_group_1(_145472) & v6_vectsp_1(_145472) & v7_vectsp_1(_145472) & v8_vectsp_1(_145472) & l3_vectsp_1(_145472) => ! [_145552] : (~ v3_struct_0(_145552) & v3_rlvect_1(_145552) & v4_rlvect_1(_145552) & v5_rlvect_1(_145552) & v6_rlvect_1(_145552) & v5_vectsp_2(_145552, _145472) & l1_vectsp_2(_145552, _145472) => ! [_145617] : (m1_subset_1(_145617, k1_zfmisc_1(u1_struct_0(_145552))) => ! [_145643] : (m1_subset_1(_145643, k1_zfmisc_1(u1_struct_0(_145552))) => r1_tarski(_145617, _145643) & v1_rmod_5(_145643, _145472, _145552) => v1_rmod_5(_145617, _145472, _145552))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t2_rmod_5)).
% 232.68/224.33 fof(d1_rmod_5, axiom, ! [_146265] : (~ v3_struct_0(_146265) & v3_rlvect_1(_146265) & v4_rlvect_1(_146265) & v5_rlvect_1(_146265) & v6_rlvect_1(_146265) & v4_group_1(_146265) & v6_vectsp_1(_146265) & v7_vectsp_1(_146265) & v8_vectsp_1(_146265) & l3_vectsp_1(_146265) => ! [_146345] : (~ v3_struct_0(_146345) & v3_rlvect_1(_146345) & v4_rlvect_1(_146345) & v5_rlvect_1(_146345) & v6_rlvect_1(_146345) & v5_vectsp_2(_146345, _146265) & l1_vectsp_2(_146345, _146265) => ! [_146410] : (m1_subset_1(_146410, k1_zfmisc_1(u1_struct_0(_146345))) => (v1_rmod_5(_146410, _146265, _146345) <=> ! [_146449] : (m2_rmod_4(_146449, _146265, _146345, _146410) => k5_rmod_4(_146265, _146345, _146449) = k1_rlvect_1(_146345) => k2_rmod_4(_146265, _146345, _146449) = k1_xboole_0))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_rmod_5)).
% 232.68/224.33 fof(t25_rmod_4, axiom, ! [_147071] : (~ v3_struct_0(_147071) & v3_rlvect_1(_147071) & v4_rlvect_1(_147071) & v5_rlvect_1(_147071) & v6_rlvect_1(_147071) & v4_group_1(_147071) & v6_vectsp_1(_147071) & v7_vectsp_1(_147071) & v8_vectsp_1(_147071) & l3_vectsp_1(_147071) => ! [_147151] : (~ v3_struct_0(_147151) & v3_rlvect_1(_147151) & v4_rlvect_1(_147151) & v5_rlvect_1(_147151) & v6_rlvect_1(_147151) & v5_vectsp_2(_147151, _147071) & l1_vectsp_2(_147151, _147071) => ! [_147216] : (m1_subset_1(_147216, k1_zfmisc_1(u1_struct_0(_147151))) => ! [_147242] : (m1_subset_1(_147242, k1_zfmisc_1(u1_struct_0(_147151))) => ! [_147268] : (m2_rmod_4(_147268, _147071, _147151, _147216) => r1_tarski(_147216, _147242) => m2_rmod_4(_147268, _147071, _147151, _147242)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t25_rmod_4)).
% 232.68/224.33
% 232.68/224.33 cnf(1, plain, [v3_struct_0(45 ^ [])], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(2, plain, [-(v5_rlvect_1(44 ^ []))], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(3, plain, [-(v4_rlvect_1(45 ^ []))], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(4, plain, [-(v8_vectsp_1(44 ^ []))], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(5, plain, [-(3 ^ [_26529, _25987, _25275]), v1_rmod_5(_26529, _25275, _25987), m2_rmod_4(_26807, _25275, _25987, _26529), k5_rmod_4(_25275, _25987, _26807) = k1_rlvect_1(_25987), -(k2_rmod_4(_25275, _25987, _26807) = k1_xboole_0)], clausify(d1_rmod_5)).
% 232.68/224.33 cnf(6, plain, [-(l3_vectsp_1(44 ^ []))], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(7, plain, [-(v7_vectsp_1(44 ^ []))], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(8, plain, [l3_vectsp_1(_59591), v8_vectsp_1(_59591), v7_vectsp_1(_59591), v6_vectsp_1(_59591), v4_group_1(_59591), v6_rlvect_1(_59591), v5_rlvect_1(_59591), v4_rlvect_1(_59591), v3_rlvect_1(_59591), -(v3_struct_0(_59591)), -(m2_rmod_4(_61192, _59591, _60303, _61024)), r1_tarski(_60845, _61024), m2_rmod_4(_61192, _59591, _60303, _60845), m1_subset_1(_61024, k1_zfmisc_1(u1_struct_0(_60303))), m1_subset_1(_60845, k1_zfmisc_1(u1_struct_0(_60303))), -(v3_struct_0(_60303)), v3_rlvect_1(_60303), v4_rlvect_1(_60303), v5_rlvect_1(_60303), v6_rlvect_1(_60303), v5_vectsp_2(_60303, _59591), l1_vectsp_2(_60303, _59591)], clausify(t25_rmod_4)).
% 232.68/224.33 cnf(9, plain, [-(2 ^ [_26529, _25987, _25275]), k2_rmod_4(_25275, _25987, 1 ^ [_26529, _25987, _25275]) = k1_xboole_0], clausify(d1_rmod_5)).
% 232.68/224.33 cnf(10, plain, [-(3 ^ [_26529, _25987, _25275]), -(v1_rmod_5(_26529, _25275, _25987)), 2 ^ [_26529, _25987, _25275]], clausify(d1_rmod_5)).
% 232.68/224.33 cnf(11, plain, [-(v4_rlvect_1(44 ^ []))], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(12, plain, [-(v5_rlvect_1(45 ^ []))], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(13, plain, [-(2 ^ [_26529, _25987, _25275]), -(k5_rmod_4(_25275, _25987, 1 ^ [_26529, _25987, _25275]) = k1_rlvect_1(_25987))], clausify(d1_rmod_5)).
% 232.68/224.33 cnf(14, plain, [-(v6_rlvect_1(44 ^ []))], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(15, plain, [v1_rmod_5(46 ^ [], 44 ^ [], 45 ^ [])], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(16, plain, [-(m1_subset_1(47 ^ [], k1_zfmisc_1(u1_struct_0(45 ^ []))))], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(17, plain, [-(r1_tarski(46 ^ [], 47 ^ []))], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(18, plain, [-(v3_rlvect_1(44 ^ []))], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(19, plain, [-(v5_vectsp_2(45 ^ [], 44 ^ []))], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(20, plain, [-(v6_vectsp_1(44 ^ []))], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(21, plain, [-(v1_rmod_5(47 ^ [], 44 ^ [], 45 ^ []))], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(22, plain, [-(v3_rlvect_1(45 ^ []))], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(23, plain, [-(m1_subset_1(46 ^ [], k1_zfmisc_1(u1_struct_0(45 ^ []))))], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(24, plain, [-(l1_vectsp_2(45 ^ [], 44 ^ []))], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(25, plain, [v3_struct_0(44 ^ [])], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(26, plain, [l3_vectsp_1(_25275), v8_vectsp_1(_25275), v7_vectsp_1(_25275), v6_vectsp_1(_25275), v4_group_1(_25275), v6_rlvect_1(_25275), v5_rlvect_1(_25275), v4_rlvect_1(_25275), v3_rlvect_1(_25275), -(v3_struct_0(_25275)), l1_vectsp_2(_25987, _25275), v5_vectsp_2(_25987, _25275), v6_rlvect_1(_25987), v5_rlvect_1(_25987), v4_rlvect_1(_25987), v3_rlvect_1(_25987), -(v3_struct_0(_25987)), m1_subset_1(_26529, k1_zfmisc_1(u1_struct_0(_25987))), 3 ^ [_26529, _25987, _25275]], clausify(d1_rmod_5)).
% 232.68/224.33 cnf(27, plain, [-(v6_rlvect_1(45 ^ []))], clausify(t2_rmod_5)).
% 232.68/224.33 cnf(28, plain, [-(2 ^ [_26529, _25987, _25275]), -(m2_rmod_4(1 ^ [_26529, _25987, _25275], _25275, _25987, _26529))], clausify(d1_rmod_5)).
% 232.68/224.33 cnf(29, plain, [-(v4_group_1(44 ^ []))], clausify(t2_rmod_5)).
% 232.68/224.33
% 232.68/224.33 cnf('1',plain,[v1_rmod_5(46 ^ [], 44 ^ [], 45 ^ [])],start(15)).
% 232.68/224.33 cnf('1.1',plain,[-(v1_rmod_5(46 ^ [], 44 ^ [], 45 ^ [])), -(3 ^ [46 ^ [], 45 ^ [], 44 ^ []]), 2 ^ [46 ^ [], 45 ^ [], 44 ^ []]],extension(10,bind([[_26529, _25987, _25275], [46 ^ [], 45 ^ [], 44 ^ []]]))).
% 232.68/224.33 cnf('1.1.1',plain,[3 ^ [46 ^ [], 45 ^ [], 44 ^ []], l3_vectsp_1(44 ^ []), v8_vectsp_1(44 ^ []), v7_vectsp_1(44 ^ []), v6_vectsp_1(44 ^ []), v4_group_1(44 ^ []), v6_rlvect_1(44 ^ []), v5_rlvect_1(44 ^ []), v4_rlvect_1(44 ^ []), v3_rlvect_1(44 ^ []), -(v3_struct_0(44 ^ [])), l1_vectsp_2(45 ^ [], 44 ^ []), v5_vectsp_2(45 ^ [], 44 ^ []), v6_rlvect_1(45 ^ []), v5_rlvect_1(45 ^ []), v4_rlvect_1(45 ^ []), v3_rlvect_1(45 ^ []), -(v3_struct_0(45 ^ [])), m1_subset_1(46 ^ [], k1_zfmisc_1(u1_struct_0(45 ^ [])))],extension(26,bind([[_25275, _26529, _25987], [44 ^ [], 46 ^ [], 45 ^ []]]))).
% 232.68/224.33 cnf('1.1.1.1',plain,[-(l3_vectsp_1(44 ^ []))],extension(6)).
% 232.68/224.33 cnf('1.1.1.2',plain,[-(v8_vectsp_1(44 ^ []))],extension(4)).
% 232.68/224.33 cnf('1.1.1.3',plain,[-(v7_vectsp_1(44 ^ []))],extension(7)).
% 232.68/224.33 cnf('1.1.1.4',plain,[-(v6_vectsp_1(44 ^ []))],extension(20)).
% 232.68/224.33 cnf('1.1.1.5',plain,[-(v4_group_1(44 ^ []))],extension(29)).
% 232.68/224.33 cnf('1.1.1.6',plain,[-(v6_rlvect_1(44 ^ []))],extension(14)).
% 232.68/224.33 cnf('1.1.1.7',plain,[-(v5_rlvect_1(44 ^ []))],extension(2)).
% 232.68/224.33 cnf('1.1.1.8',plain,[-(v4_rlvect_1(44 ^ []))],extension(11)).
% 232.68/224.33 cnf('1.1.1.9',plain,[-(v3_rlvect_1(44 ^ []))],extension(18)).
% 232.68/224.33 cnf('1.1.1.10',plain,[v3_struct_0(44 ^ [])],extension(25)).
% 232.68/224.33 cnf('1.1.1.11',plain,[-(l1_vectsp_2(45 ^ [], 44 ^ []))],extension(24)).
% 232.68/224.33 cnf('1.1.1.12',plain,[-(v5_vectsp_2(45 ^ [], 44 ^ []))],extension(19)).
% 232.68/224.33 cnf('1.1.1.13',plain,[-(v6_rlvect_1(45 ^ []))],extension(27)).
% 232.68/224.33 cnf('1.1.1.14',plain,[-(v5_rlvect_1(45 ^ []))],extension(12)).
% 232.68/224.33 cnf('1.1.1.15',plain,[-(v4_rlvect_1(45 ^ []))],extension(3)).
% 232.68/224.33 cnf('1.1.1.16',plain,[-(v3_rlvect_1(45 ^ []))],extension(22)).
% 232.68/224.33 cnf('1.1.1.17',plain,[v3_struct_0(45 ^ [])],extension(1)).
% 232.68/224.33 cnf('1.1.1.18',plain,[-(m1_subset_1(46 ^ [], k1_zfmisc_1(u1_struct_0(45 ^ []))))],extension(23)).
% 232.68/224.33 cnf('1.1.2',plain,[-(2 ^ [46 ^ [], 45 ^ [], 44 ^ []]), -(m2_rmod_4(1 ^ [46 ^ [], 45 ^ [], 44 ^ []], 44 ^ [], 45 ^ [], 46 ^ []))],extension(28,bind([[_25275, _25987, _26529], [44 ^ [], 45 ^ [], 46 ^ []]]))).
% 232.68/224.33 cnf('1.1.2.1',plain,[m2_rmod_4(1 ^ [46 ^ [], 45 ^ [], 44 ^ []], 44 ^ [], 45 ^ [], 46 ^ []), l3_vectsp_1(44 ^ []), v8_vectsp_1(44 ^ []), v7_vectsp_1(44 ^ []), v6_vectsp_1(44 ^ []), v4_group_1(44 ^ []), v6_rlvect_1(44 ^ []), v5_rlvect_1(44 ^ []), v4_rlvect_1(44 ^ []), v3_rlvect_1(44 ^ []), -(v3_struct_0(44 ^ [])), -(m2_rmod_4(1 ^ [46 ^ [], 45 ^ [], 44 ^ []], 44 ^ [], 45 ^ [], 47 ^ [])), r1_tarski(46 ^ [], 47 ^ []), m1_subset_1(47 ^ [], k1_zfmisc_1(u1_struct_0(45 ^ []))), m1_subset_1(46 ^ [], k1_zfmisc_1(u1_struct_0(45 ^ []))), -(v3_struct_0(45 ^ [])), v3_rlvect_1(45 ^ []), v4_rlvect_1(45 ^ []), v5_rlvect_1(45 ^ []), v6_rlvect_1(45 ^ []), v5_vectsp_2(45 ^ [], 44 ^ []), l1_vectsp_2(45 ^ [], 44 ^ [])],extension(8,bind([[_61192, _61024, _60845, _60303, _59591], [1 ^ [46 ^ [], 45 ^ [], 44 ^ []], 47 ^ [], 46 ^ [], 45 ^ [], 44 ^ []]]))).
% 232.68/224.33 cnf('1.1.2.1.1',plain,[-(l3_vectsp_1(44 ^ []))],extension(6)).
% 232.68/224.33 cnf('1.1.2.1.2',plain,[-(v8_vectsp_1(44 ^ []))],extension(4)).
% 232.68/224.33 cnf('1.1.2.1.3',plain,[-(v7_vectsp_1(44 ^ []))],extension(7)).
% 232.68/224.33 cnf('1.1.2.1.4',plain,[-(v6_vectsp_1(44 ^ []))],extension(20)).
% 232.68/224.33 cnf('1.1.2.1.5',plain,[-(v4_group_1(44 ^ []))],extension(29)).
% 232.68/224.33 cnf('1.1.2.1.6',plain,[-(v6_rlvect_1(44 ^ []))],extension(14)).
% 232.68/224.33 cnf('1.1.2.1.7',plain,[-(v5_rlvect_1(44 ^ []))],extension(2)).
% 232.68/224.33 cnf('1.1.2.1.8',plain,[-(v4_rlvect_1(44 ^ []))],extension(11)).
% 232.68/224.33 cnf('1.1.2.1.9',plain,[-(v3_rlvect_1(44 ^ []))],extension(18)).
% 232.68/224.33 cnf('1.1.2.1.10',plain,[v3_struct_0(44 ^ [])],extension(25)).
% 232.68/224.33 cnf('1.1.2.1.11',plain,[m2_rmod_4(1 ^ [46 ^ [], 45 ^ [], 44 ^ []], 44 ^ [], 45 ^ [], 47 ^ []), -(3 ^ [47 ^ [], 45 ^ [], 44 ^ []]), v1_rmod_5(47 ^ [], 44 ^ [], 45 ^ []), k5_rmod_4(44 ^ [], 45 ^ [], 1 ^ [46 ^ [], 45 ^ [], 44 ^ []]) = k1_rlvect_1(45 ^ []), -(k2_rmod_4(44 ^ [], 45 ^ [], 1 ^ [46 ^ [], 45 ^ [], 44 ^ []]) = k1_xboole_0)],extension(5,bind([[_26529, _25275, _25987, _26807], [47 ^ [], 44 ^ [], 45 ^ [], 1 ^ [46 ^ [], 45 ^ [], 44 ^ []]]]))).
% 232.68/224.33 cnf('1.1.2.1.11.1',plain,[3 ^ [47 ^ [], 45 ^ [], 44 ^ []], l3_vectsp_1(44 ^ []), v8_vectsp_1(44 ^ []), v7_vectsp_1(44 ^ []), v6_vectsp_1(44 ^ []), v4_group_1(44 ^ []), v6_rlvect_1(44 ^ []), v5_rlvect_1(44 ^ []), v4_rlvect_1(44 ^ []), v3_rlvect_1(44 ^ []), -(v3_struct_0(44 ^ [])), l1_vectsp_2(45 ^ [], 44 ^ []), v5_vectsp_2(45 ^ [], 44 ^ []), v6_rlvect_1(45 ^ []), v5_rlvect_1(45 ^ []), v4_rlvect_1(45 ^ []), v3_rlvect_1(45 ^ []), -(v3_struct_0(45 ^ [])), m1_subset_1(47 ^ [], k1_zfmisc_1(u1_struct_0(45 ^ [])))],extension(26,bind([[_25275, _26529, _25987], [44 ^ [], 47 ^ [], 45 ^ []]]))).
% 232.68/224.33 cnf('1.1.2.1.11.1.1',plain,[-(l3_vectsp_1(44 ^ []))],extension(6)).
% 232.68/224.33 cnf('1.1.2.1.11.1.2',plain,[-(v8_vectsp_1(44 ^ []))],extension(4)).
% 232.68/224.33 cnf('1.1.2.1.11.1.3',plain,[-(v7_vectsp_1(44 ^ []))],extension(7)).
% 232.68/224.33 cnf('1.1.2.1.11.1.4',plain,[-(v6_vectsp_1(44 ^ []))],extension(20)).
% 232.68/224.33 cnf('1.1.2.1.11.1.5',plain,[-(v4_group_1(44 ^ []))],extension(29)).
% 232.68/224.33 cnf('1.1.2.1.11.1.6',plain,[-(v6_rlvect_1(44 ^ []))],extension(14)).
% 232.68/224.33 cnf('1.1.2.1.11.1.7',plain,[-(v5_rlvect_1(44 ^ []))],extension(2)).
% 232.68/224.33 cnf('1.1.2.1.11.1.8',plain,[-(v4_rlvect_1(44 ^ []))],extension(11)).
% 232.68/224.33 cnf('1.1.2.1.11.1.9',plain,[-(v3_rlvect_1(44 ^ []))],extension(18)).
% 232.68/224.33 cnf('1.1.2.1.11.1.10',plain,[v3_struct_0(44 ^ [])],extension(25)).
% 232.68/224.33 cnf('1.1.2.1.11.1.11',plain,[-(l1_vectsp_2(45 ^ [], 44 ^ []))],extension(24)).
% 232.68/224.33 cnf('1.1.2.1.11.1.12',plain,[-(v5_vectsp_2(45 ^ [], 44 ^ []))],extension(19)).
% 232.68/224.33 cnf('1.1.2.1.11.1.13',plain,[-(v6_rlvect_1(45 ^ []))],extension(27)).
% 232.68/224.33 cnf('1.1.2.1.11.1.14',plain,[-(v5_rlvect_1(45 ^ []))],extension(12)).
% 232.68/224.33 cnf('1.1.2.1.11.1.15',plain,[-(v4_rlvect_1(45 ^ []))],extension(3)).
% 232.68/224.33 cnf('1.1.2.1.11.1.16',plain,[-(v3_rlvect_1(45 ^ []))],extension(22)).
% 232.68/224.33 cnf('1.1.2.1.11.1.17',plain,[v3_struct_0(45 ^ [])],extension(1)).
% 232.68/224.33 cnf('1.1.2.1.11.1.18',plain,[-(m1_subset_1(47 ^ [], k1_zfmisc_1(u1_struct_0(45 ^ []))))],extension(16)).
% 232.68/224.33 cnf('1.1.2.1.11.2',plain,[-(v1_rmod_5(47 ^ [], 44 ^ [], 45 ^ []))],extension(21)).
% 232.68/224.33 cnf('1.1.2.1.11.3',plain,[-(k5_rmod_4(44 ^ [], 45 ^ [], 1 ^ [46 ^ [], 45 ^ [], 44 ^ []]) = k1_rlvect_1(45 ^ [])), -(2 ^ [46 ^ [], 45 ^ [], 44 ^ []])],extension(13,bind([[_26529, _25987, _25275], [46 ^ [], 45 ^ [], 44 ^ []]]))).
% 232.68/224.33 cnf('1.1.2.1.11.3.1',plain,[2 ^ [46 ^ [], 45 ^ [], 44 ^ []]],reduction('1.1')).
% 232.68/224.33 cnf('1.1.2.1.11.4',plain,[k2_rmod_4(44 ^ [], 45 ^ [], 1 ^ [46 ^ [], 45 ^ [], 44 ^ []]) = k1_xboole_0, -(2 ^ [46 ^ [], 45 ^ [], 44 ^ []])],extension(9,bind([[_26529, _25987, _25275], [46 ^ [], 45 ^ [], 44 ^ []]]))).
% 232.68/224.33 cnf('1.1.2.1.11.4.1',plain,[2 ^ [46 ^ [], 45 ^ [], 44 ^ []]],reduction('1.1')).
% 232.68/224.33 cnf('1.1.2.1.12',plain,[-(r1_tarski(46 ^ [], 47 ^ []))],extension(17)).
% 232.68/224.33 cnf('1.1.2.1.13',plain,[-(m1_subset_1(47 ^ [], k1_zfmisc_1(u1_struct_0(45 ^ []))))],extension(16)).
% 232.68/224.33 cnf('1.1.2.1.14',plain,[-(m1_subset_1(46 ^ [], k1_zfmisc_1(u1_struct_0(45 ^ []))))],extension(23)).
% 232.68/224.33 cnf('1.1.2.1.15',plain,[v3_struct_0(45 ^ [])],extension(1)).
% 232.68/224.33 cnf('1.1.2.1.16',plain,[-(v3_rlvect_1(45 ^ []))],extension(22)).
% 232.68/224.33 cnf('1.1.2.1.17',plain,[-(v4_rlvect_1(45 ^ []))],extension(3)).
% 232.68/224.33 cnf('1.1.2.1.18',plain,[-(v5_rlvect_1(45 ^ []))],extension(12)).
% 232.68/224.33 cnf('1.1.2.1.19',plain,[-(v6_rlvect_1(45 ^ []))],extension(27)).
% 232.68/224.33 cnf('1.1.2.1.20',plain,[-(v5_vectsp_2(45 ^ [], 44 ^ []))],extension(19)).
% 232.68/224.33 cnf('1.1.2.1.21',plain,[-(l1_vectsp_2(45 ^ [], 44 ^ []))],extension(24)).
% 232.68/224.33 %-----------------------------------------------------
% 232.68/224.33
% 232.68/224.33 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------