%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : GRP640+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 : Sat Jul 16 10:14:24 EDT 2022
% Result : Theorem 2.07s 2.43s
% Output : Proof 2.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP640+1 : TPTP v8.1.0. Released v3.4.0.
% 0.03/0.12 % 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.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Mon Jun 13 22:44:36 EDT 2022
% 0.12/0.33 % CPUTime :
% 2.07/2.43 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.07/2.44 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.07/2.45
% 2.07/2.45 %-----------------------------------------------------
% 2.07/2.45 fof(t13_latsubgr, conjecture, ! [_118657] : (~ v3_struct_0(_118657) & v3_group_1(_118657) & v4_group_1(_118657) & l1_group_1(_118657) => ! [_118695] : (~ v3_struct_0(_118695) & v3_group_1(_118695) & v4_group_1(_118695) & l1_group_1(_118695) => ! [_118733] : (m1_group_2(_118733, _118657) => ! [_118751] : (m1_group_2(_118751, _118657) => ! [_118769] : (v1_funct_1(_118769) & v1_funct_2(_118769, u1_struct_0(_118657), u1_struct_0(_118695)) & m2_relset_1(_118769, u1_struct_0(_118657), u1_struct_0(_118695)) => ! [_118826] : (m1_subset_1(_118826, k1_zfmisc_1(u1_struct_0(_118657))) => _118826 = k2_xboole_0(u1_struct_0(_118733), u1_struct_0(_118751)) => k2_funct_2(u1_struct_0(_118657), u1_struct_0(_118695), _118769, u1_struct_0(k8_group_4(_118657, _118733, _118751))) = k2_funct_2(u1_struct_0(_118657), u1_struct_0(_118695), _118769, u1_struct_0(k5_group_4(_118657, _118826))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t13_latsubgr)).
% 2.07/2.45 fof(redefinition_r1_group_2, axiom, ! [_119749, _119752, _119755] : (~ v3_struct_0(_119749) & v3_group_1(_119749) & v4_group_1(_119749) & l1_group_1(_119749) & v1_group_1(_119752) & m1_group_2(_119752, _119749) & v1_group_1(_119755) & m1_group_2(_119755, _119749) => (r1_group_2(_119749, _119752, _119755) <=> _119752 = _119755)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', redefinition_r1_group_2)).
% 2.07/2.45 fof(dt_k5_group_4, axiom, ! [_120100, _120103] : (~ v3_struct_0(_120100) & v3_group_1(_120100) & v4_group_1(_120100) & l1_group_1(_120100) & m1_subset_1(_120103, k1_zfmisc_1(u1_struct_0(_120100))) => v1_group_1(k5_group_4(_120100, _120103)) & m1_group_2(k5_group_4(_120100, _120103), _120100)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_k5_group_4)).
% 2.07/2.45 fof(dt_k8_group_4, axiom, ! [_120420, _120423, _120426] : (~ v3_struct_0(_120420) & v3_group_1(_120420) & v4_group_1(_120420) & l1_group_1(_120420) & m1_group_2(_120423, _120420) & m1_group_2(_120426, _120420) => v1_group_1(k8_group_4(_120420, _120423, _120426)) & m1_group_2(k8_group_4(_120420, _120423, _120426), _120420)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_k8_group_4)).
% 2.07/2.45 fof(t4_latsubgr, axiom, ! [_120783] : (~ v3_struct_0(_120783) & v3_group_1(_120783) & v4_group_1(_120783) & l1_group_1(_120783) => ! [_120821] : (m1_group_2(_120821, _120783) => ! [_120839] : (m1_group_2(_120839, _120783) => ! [_120857] : (m1_subset_1(_120857, k1_zfmisc_1(u1_struct_0(_120783))) => _120857 = k2_xboole_0(u1_struct_0(_120821), u1_struct_0(_120839)) => r1_group_2(_120783, k8_group_4(_120783, _120821, _120839), k5_group_4(_120783, _120857)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t4_latsubgr)).
% 2.07/2.45
% 2.07/2.45 cnf(1, plain, [v3_struct_0(15 ^ [])], clausify(t13_latsubgr)).
% 2.07/2.45 cnf(2, plain, [-(v3_group_1(15 ^ []))], clausify(t13_latsubgr)).
% 2.07/2.45 cnf(3, plain, [-(v4_group_1(15 ^ []))], clausify(t13_latsubgr)).
% 2.07/2.45 cnf(4, plain, [-(l1_group_1(15 ^ []))], clausify(t13_latsubgr)).
% 2.07/2.45 cnf(5, plain, [-(m1_group_2(17 ^ [], 15 ^ []))], clausify(t13_latsubgr)).
% 2.07/2.45 cnf(6, plain, [-(m1_group_2(18 ^ [], 15 ^ []))], clausify(t13_latsubgr)).
% 2.07/2.45 cnf(7, plain, [-(m1_subset_1(20 ^ [], k1_zfmisc_1(u1_struct_0(15 ^ []))))], clausify(t13_latsubgr)).
% 2.07/2.45 cnf(8, plain, [-(20 ^ [] = k2_xboole_0(u1_struct_0(17 ^ []), u1_struct_0(18 ^ [])))], clausify(t13_latsubgr)).
% 2.07/2.45 cnf(9, plain, [k2_funct_2(u1_struct_0(15 ^ []), u1_struct_0(16 ^ []), 19 ^ [], u1_struct_0(k8_group_4(15 ^ [], 17 ^ [], 18 ^ []))) = k2_funct_2(u1_struct_0(15 ^ []), u1_struct_0(16 ^ []), 19 ^ [], u1_struct_0(k5_group_4(15 ^ [], 20 ^ [])))], clausify(t13_latsubgr)).
% 2.07/2.45 cnf(10, plain, [-(k2_funct_2(_46205, _46410, _46611, _46808) = k2_funct_2(_46308, _46511, _46710, _46905)), _46205 = _46308, _46410 = _46511, _46611 = _46710, _46808 = _46905], theory(equality)).
% 2.07/2.45 cnf(11, plain, [_51539 = _51588, -(u1_struct_0(_51539) = u1_struct_0(_51588))], theory(equality)).
% 2.07/2.45 cnf(12, plain, [-(_33502 = _33502)], theory(equality)).
% 2.07/2.45 cnf(13, plain, [-(_72159 = _72253), r1_group_2(_72064, _72159, _72253), -(v3_struct_0(_72064)), v3_group_1(_72064), v4_group_1(_72064), l1_group_1(_72064), v1_group_1(_72159), m1_group_2(_72159, _72064), v1_group_1(_72253), m1_group_2(_72253, _72064)], clausify(redefinition_r1_group_2)).
% 2.07/2.45 cnf(14, plain, [-(v1_group_1(k5_group_4(_74231, _74313))), -(v3_struct_0(_74231)), v3_group_1(_74231), v4_group_1(_74231), l1_group_1(_74231), m1_subset_1(_74313, k1_zfmisc_1(u1_struct_0(_74231)))], clausify(dt_k5_group_4)).
% 2.07/2.45 cnf(15, plain, [-(m1_group_2(k5_group_4(_74231, _74313), _74231)), -(v3_struct_0(_74231)), v3_group_1(_74231), v4_group_1(_74231), l1_group_1(_74231), m1_subset_1(_74313, k1_zfmisc_1(u1_struct_0(_74231)))], clausify(dt_k5_group_4)).
% 2.07/2.45 cnf(16, plain, [-(v1_group_1(k8_group_4(_75002, _75093, _75183))), -(v3_struct_0(_75002)), v3_group_1(_75002), v4_group_1(_75002), l1_group_1(_75002), m1_group_2(_75093, _75002), m1_group_2(_75183, _75002)], clausify(dt_k8_group_4)).
% 2.07/2.45 cnf(17, plain, [-(m1_group_2(k8_group_4(_75002, _75093, _75183), _75002)), -(v3_struct_0(_75002)), v3_group_1(_75002), v4_group_1(_75002), l1_group_1(_75002), m1_group_2(_75093, _75002), m1_group_2(_75183, _75002)], clausify(dt_k8_group_4)).
% 2.07/2.45 cnf(18, plain, [l1_group_1(_78104), v4_group_1(_78104), v3_group_1(_78104), -(v3_struct_0(_78104)), m1_group_2(_78431, _78104), m1_group_2(_78581, _78104), m1_subset_1(_78724, k1_zfmisc_1(u1_struct_0(_78104))), _78724 = k2_xboole_0(u1_struct_0(_78431), u1_struct_0(_78581)), -(r1_group_2(_78104, k8_group_4(_78104, _78431, _78581), k5_group_4(_78104, _78724)))], clausify(t4_latsubgr)).
% 2.07/2.45
% 2.07/2.45 cnf('1',plain,[k2_funct_2(u1_struct_0(15 ^ []), u1_struct_0(16 ^ []), 19 ^ [], u1_struct_0(k8_group_4(15 ^ [], 17 ^ [], 18 ^ []))) = k2_funct_2(u1_struct_0(15 ^ []), u1_struct_0(16 ^ []), 19 ^ [], u1_struct_0(k5_group_4(15 ^ [], 20 ^ [])))],start(9)).
% 2.07/2.45 cnf('1.1',plain,[-(k2_funct_2(u1_struct_0(15 ^ []), u1_struct_0(16 ^ []), 19 ^ [], u1_struct_0(k8_group_4(15 ^ [], 17 ^ [], 18 ^ []))) = k2_funct_2(u1_struct_0(15 ^ []), u1_struct_0(16 ^ []), 19 ^ [], u1_struct_0(k5_group_4(15 ^ [], 20 ^ [])))), u1_struct_0(15 ^ []) = u1_struct_0(15 ^ []), u1_struct_0(16 ^ []) = u1_struct_0(16 ^ []), 19 ^ [] = 19 ^ [], u1_struct_0(k8_group_4(15 ^ [], 17 ^ [], 18 ^ [])) = u1_struct_0(k5_group_4(15 ^ [], 20 ^ []))],extension(10,bind([[_46205, _46308, _46410, _46511, _46611, _46710, _46808, _46905], [u1_struct_0(15 ^ []), u1_struct_0(15 ^ []), u1_struct_0(16 ^ []), u1_struct_0(16 ^ []), 19 ^ [], 19 ^ [], u1_struct_0(k8_group_4(15 ^ [], 17 ^ [], 18 ^ [])), u1_struct_0(k5_group_4(15 ^ [], 20 ^ []))]]))).
% 2.07/2.45 cnf('1.1.1',plain,[-(u1_struct_0(15 ^ []) = u1_struct_0(15 ^ [])), 15 ^ [] = 15 ^ []],extension(11,bind([[_51539, _51588], [15 ^ [], 15 ^ []]]))).
% 2.07/2.45 cnf('1.1.1.1',plain,[-(15 ^ [] = 15 ^ [])],extension(12,bind([[_33502], [15 ^ []]]))).
% 2.07/2.45 cnf('1.1.2',plain,[-(u1_struct_0(16 ^ []) = u1_struct_0(16 ^ [])), 16 ^ [] = 16 ^ []],extension(11,bind([[_51539, _51588], [16 ^ [], 16 ^ []]]))).
% 2.07/2.45 cnf('1.1.2.1',plain,[-(16 ^ [] = 16 ^ [])],extension(12,bind([[_33502], [16 ^ []]]))).
% 2.07/2.45 cnf('1.1.3',plain,[-(19 ^ [] = 19 ^ [])],extension(12,bind([[_33502], [19 ^ []]]))).
% 2.07/2.45 cnf('1.1.4',plain,[-(u1_struct_0(k8_group_4(15 ^ [], 17 ^ [], 18 ^ [])) = u1_struct_0(k5_group_4(15 ^ [], 20 ^ []))), k8_group_4(15 ^ [], 17 ^ [], 18 ^ []) = k5_group_4(15 ^ [], 20 ^ [])],extension(11,bind([[_51539, _51588], [k8_group_4(15 ^ [], 17 ^ [], 18 ^ []), k5_group_4(15 ^ [], 20 ^ [])]]))).
% 2.07/2.45 cnf('1.1.4.1',plain,[-(k8_group_4(15 ^ [], 17 ^ [], 18 ^ []) = k5_group_4(15 ^ [], 20 ^ [])), r1_group_2(15 ^ [], k8_group_4(15 ^ [], 17 ^ [], 18 ^ []), k5_group_4(15 ^ [], 20 ^ [])), -(v3_struct_0(15 ^ [])), v3_group_1(15 ^ []), v4_group_1(15 ^ []), l1_group_1(15 ^ []), v1_group_1(k8_group_4(15 ^ [], 17 ^ [], 18 ^ [])), m1_group_2(k8_group_4(15 ^ [], 17 ^ [], 18 ^ []), 15 ^ []), v1_group_1(k5_group_4(15 ^ [], 20 ^ [])), m1_group_2(k5_group_4(15 ^ [], 20 ^ []), 15 ^ [])],extension(13,bind([[_72159, _72253, _72064], [k8_group_4(15 ^ [], 17 ^ [], 18 ^ []), k5_group_4(15 ^ [], 20 ^ []), 15 ^ []]]))).
% 2.07/2.45 cnf('1.1.4.1.1',plain,[-(r1_group_2(15 ^ [], k8_group_4(15 ^ [], 17 ^ [], 18 ^ []), k5_group_4(15 ^ [], 20 ^ []))), l1_group_1(15 ^ []), v4_group_1(15 ^ []), v3_group_1(15 ^ []), -(v3_struct_0(15 ^ [])), m1_group_2(17 ^ [], 15 ^ []), m1_group_2(18 ^ [], 15 ^ []), m1_subset_1(20 ^ [], k1_zfmisc_1(u1_struct_0(15 ^ []))), 20 ^ [] = k2_xboole_0(u1_struct_0(17 ^ []), u1_struct_0(18 ^ []))],extension(18,bind([[_78104, _78724, _78431, _78581], [15 ^ [], 20 ^ [], 17 ^ [], 18 ^ []]]))).
% 2.07/2.45 cnf('1.1.4.1.1.1',plain,[-(l1_group_1(15 ^ []))],extension(4)).
% 2.07/2.45 cnf('1.1.4.1.1.2',plain,[-(v4_group_1(15 ^ []))],extension(3)).
% 2.07/2.45 cnf('1.1.4.1.1.3',plain,[-(v3_group_1(15 ^ []))],extension(2)).
% 2.07/2.45 cnf('1.1.4.1.1.4',plain,[v3_struct_0(15 ^ [])],extension(1)).
% 2.07/2.45 cnf('1.1.4.1.1.5',plain,[-(m1_group_2(17 ^ [], 15 ^ []))],extension(5)).
% 2.07/2.45 cnf('1.1.4.1.1.6',plain,[-(m1_group_2(18 ^ [], 15 ^ []))],extension(6)).
% 2.07/2.45 cnf('1.1.4.1.1.7',plain,[-(m1_subset_1(20 ^ [], k1_zfmisc_1(u1_struct_0(15 ^ []))))],extension(7)).
% 2.07/2.45 cnf('1.1.4.1.1.8',plain,[-(20 ^ [] = k2_xboole_0(u1_struct_0(17 ^ []), u1_struct_0(18 ^ [])))],extension(8)).
% 2.07/2.45 cnf('1.1.4.1.2',plain,[v3_struct_0(15 ^ [])],extension(1)).
% 2.07/2.45 cnf('1.1.4.1.3',plain,[-(v3_group_1(15 ^ []))],extension(2)).
% 2.07/2.45 cnf('1.1.4.1.4',plain,[-(v4_group_1(15 ^ []))],extension(3)).
% 2.07/2.45 cnf('1.1.4.1.5',plain,[-(l1_group_1(15 ^ []))],extension(4)).
% 2.07/2.45 cnf('1.1.4.1.6',plain,[-(v1_group_1(k8_group_4(15 ^ [], 17 ^ [], 18 ^ []))), -(v3_struct_0(15 ^ [])), v3_group_1(15 ^ []), v4_group_1(15 ^ []), l1_group_1(15 ^ []), m1_group_2(17 ^ [], 15 ^ []), m1_group_2(18 ^ [], 15 ^ [])],extension(16,bind([[_75093, _75183, _75002], [17 ^ [], 18 ^ [], 15 ^ []]]))).
% 2.07/2.45 cnf('1.1.4.1.6.1',plain,[v3_struct_0(15 ^ [])],extension(1)).
% 2.07/2.45 cnf('1.1.4.1.6.2',plain,[-(v3_group_1(15 ^ []))],extension(2)).
% 2.07/2.45 cnf('1.1.4.1.6.3',plain,[-(v4_group_1(15 ^ []))],extension(3)).
% 2.07/2.45 cnf('1.1.4.1.6.4',plain,[-(l1_group_1(15 ^ []))],extension(4)).
% 2.07/2.45 cnf('1.1.4.1.6.5',plain,[-(m1_group_2(17 ^ [], 15 ^ []))],extension(5)).
% 2.07/2.45 cnf('1.1.4.1.6.6',plain,[-(m1_group_2(18 ^ [], 15 ^ []))],extension(6)).
% 2.07/2.45 cnf('1.1.4.1.7',plain,[-(m1_group_2(k8_group_4(15 ^ [], 17 ^ [], 18 ^ []), 15 ^ [])), -(v3_struct_0(15 ^ [])), v3_group_1(15 ^ []), v4_group_1(15 ^ []), l1_group_1(15 ^ []), m1_group_2(17 ^ [], 15 ^ []), m1_group_2(18 ^ [], 15 ^ [])],extension(17,bind([[_75093, _75183, _75002], [17 ^ [], 18 ^ [], 15 ^ []]]))).
% 2.07/2.45 cnf('1.1.4.1.7.1',plain,[v3_struct_0(15 ^ [])],extension(1)).
% 2.07/2.45 cnf('1.1.4.1.7.2',plain,[-(v3_group_1(15 ^ []))],extension(2)).
% 2.07/2.45 cnf('1.1.4.1.7.3',plain,[-(v4_group_1(15 ^ []))],extension(3)).
% 2.07/2.45 cnf('1.1.4.1.7.4',plain,[-(l1_group_1(15 ^ []))],extension(4)).
% 2.07/2.45 cnf('1.1.4.1.7.5',plain,[-(m1_group_2(17 ^ [], 15 ^ []))],extension(5)).
% 2.07/2.45 cnf('1.1.4.1.7.6',plain,[-(m1_group_2(18 ^ [], 15 ^ []))],extension(6)).
% 2.07/2.45 cnf('1.1.4.1.8',plain,[-(v1_group_1(k5_group_4(15 ^ [], 20 ^ []))), -(v3_struct_0(15 ^ [])), v3_group_1(15 ^ []), v4_group_1(15 ^ []), l1_group_1(15 ^ []), m1_subset_1(20 ^ [], k1_zfmisc_1(u1_struct_0(15 ^ [])))],extension(14,bind([[_74313, _74231], [20 ^ [], 15 ^ []]]))).
% 2.07/2.45 cnf('1.1.4.1.8.1',plain,[v3_struct_0(15 ^ [])],extension(1)).
% 2.07/2.45 cnf('1.1.4.1.8.2',plain,[-(v3_group_1(15 ^ []))],extension(2)).
% 2.07/2.45 cnf('1.1.4.1.8.3',plain,[-(v4_group_1(15 ^ []))],extension(3)).
% 2.07/2.45 cnf('1.1.4.1.8.4',plain,[-(l1_group_1(15 ^ []))],extension(4)).
% 2.07/2.45 cnf('1.1.4.1.8.5',plain,[-(m1_subset_1(20 ^ [], k1_zfmisc_1(u1_struct_0(15 ^ []))))],extension(7)).
% 2.07/2.45 cnf('1.1.4.1.9',plain,[-(m1_group_2(k5_group_4(15 ^ [], 20 ^ []), 15 ^ [])), -(v3_struct_0(15 ^ [])), v3_group_1(15 ^ []), v4_group_1(15 ^ []), l1_group_1(15 ^ []), m1_subset_1(20 ^ [], k1_zfmisc_1(u1_struct_0(15 ^ [])))],extension(15,bind([[_74313, _74231], [20 ^ [], 15 ^ []]]))).
% 2.07/2.45 cnf('1.1.4.1.9.1',plain,[v3_struct_0(15 ^ [])],extension(1)).
% 2.07/2.45 cnf('1.1.4.1.9.2',plain,[-(v3_group_1(15 ^ []))],extension(2)).
% 2.07/2.45 cnf('1.1.4.1.9.3',plain,[-(v4_group_1(15 ^ []))],extension(3)).
% 2.07/2.45 cnf('1.1.4.1.9.4',plain,[-(l1_group_1(15 ^ []))],extension(4)).
% 2.07/2.45 cnf('1.1.4.1.9.5',plain,[-(m1_subset_1(20 ^ [], k1_zfmisc_1(u1_struct_0(15 ^ []))))],extension(7)).
% 2.07/2.45 %-----------------------------------------------------
% 2.07/2.45
% 2.07/2.45 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------