%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : GRP643+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:26 EDT 2022
% Result : Theorem 0.39s 1.41s
% Output : Proof 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP643+1 : TPTP v8.1.0. Released v3.4.0.
% 0.11/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n026.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % 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 : Mon Jun 13 17:52:51 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.39/1.41 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/1.42 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/1.42
% 0.39/1.42 %-----------------------------------------------------
% 0.39/1.42 fof(t21_latsubgr, conjecture, ! [_97386] : (~ v3_struct_0(_97386) & v3_group_1(_97386) & v4_group_1(_97386) & l1_group_1(_97386) => ! [_97424] : (v1_group_1(_97424) & m1_group_2(_97424, _97386) => ! [_97449] : (m1_subset_1(_97449, u1_struct_0(_97386)) => ! [_97471] : (m1_subset_1(_97471, u1_struct_0(_97386)) => r2_hidden(_97449, k1_funct_1(k1_latsubgr(_97386), _97424)) & r2_hidden(_97471, k1_funct_1(k1_latsubgr(_97386), _97424)) => r2_hidden(k1_group_1(_97386, _97449, _97471), k1_funct_1(k1_latsubgr(_97386), _97424)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t21_latsubgr)).
% 0.39/1.42 fof(dt_k1_group_1, axiom, ! [_98100, _98103, _98106] : (~ v3_struct_0(_98100) & l1_group_1(_98100) & m1_subset_1(_98103, u1_struct_0(_98100)) & m1_subset_1(_98106, u1_struct_0(_98100)) => m1_subset_1(k1_group_1(_98100, _98103, _98106), u1_struct_0(_98100))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', dt_k1_group_1)).
% 0.39/1.42 fof(t18_latsubgr, axiom, ! [_98428] : (~ v3_struct_0(_98428) & v3_group_1(_98428) & v4_group_1(_98428) & l1_group_1(_98428) => ! [_98466] : (v1_group_1(_98466) & m1_group_2(_98466, _98428) => ! [_98491] : (m1_subset_1(_98491, u1_struct_0(_98428)) => (r2_hidden(_98491, k1_funct_1(k1_latsubgr(_98428), _98466)) <=> r1_rlvect_1(_98466, _98491))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t18_latsubgr)).
% 0.39/1.42 fof(t59_group_2, axiom, ! [_98842] : (~ v3_struct_0(_98842) & v3_group_1(_98842) & v4_group_1(_98842) & l1_group_1(_98842) => ! [_98880] : (m1_subset_1(_98880, u1_struct_0(_98842)) => ! [_98902] : (m1_subset_1(_98902, u1_struct_0(_98842)) => ! [_98924] : (m1_group_2(_98924, _98842) => r1_rlvect_1(_98924, _98880) & r1_rlvect_1(_98924, _98902) => r1_rlvect_1(_98924, k1_group_1(_98842, _98880, _98902)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t59_group_2)).
% 0.39/1.42
% 0.39/1.42 cnf(1, plain, [v3_struct_0(15 ^ [])], clausify(t21_latsubgr)).
% 0.39/1.42 cnf(2, plain, [-(v3_group_1(15 ^ []))], clausify(t21_latsubgr)).
% 0.39/1.42 cnf(3, plain, [-(v4_group_1(15 ^ []))], clausify(t21_latsubgr)).
% 0.39/1.42 cnf(4, plain, [-(l1_group_1(15 ^ []))], clausify(t21_latsubgr)).
% 0.39/1.42 cnf(5, plain, [-(v1_group_1(16 ^ []))], clausify(t21_latsubgr)).
% 0.39/1.42 cnf(6, plain, [-(m1_group_2(16 ^ [], 15 ^ []))], clausify(t21_latsubgr)).
% 0.39/1.42 cnf(7, plain, [-(m1_subset_1(17 ^ [], u1_struct_0(15 ^ [])))], clausify(t21_latsubgr)).
% 0.39/1.42 cnf(8, plain, [-(m1_subset_1(18 ^ [], u1_struct_0(15 ^ [])))], clausify(t21_latsubgr)).
% 0.39/1.42 cnf(9, plain, [-(r2_hidden(17 ^ [], k1_funct_1(k1_latsubgr(15 ^ []), 16 ^ [])))], clausify(t21_latsubgr)).
% 0.39/1.42 cnf(10, plain, [-(r2_hidden(18 ^ [], k1_funct_1(k1_latsubgr(15 ^ []), 16 ^ [])))], clausify(t21_latsubgr)).
% 0.39/1.42 cnf(11, plain, [r2_hidden(k1_group_1(15 ^ [], 17 ^ [], 18 ^ []), k1_funct_1(k1_latsubgr(15 ^ []), 16 ^ []))], clausify(t21_latsubgr)).
% 0.39/1.42 cnf(12, plain, [-(m1_subset_1(k1_group_1(_48864, _48942, _49019), u1_struct_0(_48864))), -(v3_struct_0(_48864)), l1_group_1(_48864), m1_subset_1(_48942, u1_struct_0(_48864)), m1_subset_1(_49019, u1_struct_0(_48864))], clausify(dt_k1_group_1)).
% 0.39/1.42 cnf(13, plain, [l1_group_1(_61164), v4_group_1(_61164), v3_group_1(_61164), -(v3_struct_0(_61164)), m1_group_2(_61473, _61164), v1_group_1(_61473), m1_subset_1(_61658, u1_struct_0(_61164)), r2_hidden(_61658, k1_funct_1(k1_latsubgr(_61164), _61473)), -(r1_rlvect_1(_61473, _61658))], clausify(t18_latsubgr)).
% 0.39/1.42 cnf(14, plain, [l1_group_1(_61164), v4_group_1(_61164), v3_group_1(_61164), -(v3_struct_0(_61164)), m1_group_2(_61473, _61164), v1_group_1(_61473), m1_subset_1(_61658, u1_struct_0(_61164)), -(r2_hidden(_61658, k1_funct_1(k1_latsubgr(_61164), _61473))), r1_rlvect_1(_61473, _61658)], clausify(t18_latsubgr)).
% 0.39/1.42 cnf(15, plain, [l1_group_1(_63622), v4_group_1(_63622), v3_group_1(_63622), -(v3_struct_0(_63622)), m1_subset_1(_63944, u1_struct_0(_63622)), m1_subset_1(_64105, u1_struct_0(_63622)), m1_group_2(_64257, _63622), -(r1_rlvect_1(_64257, k1_group_1(_63622, _63944, _64105))), r1_rlvect_1(_64257, _63944), r1_rlvect_1(_64257, _64105)], clausify(t59_group_2)).
% 0.39/1.42
% 0.39/1.42 cnf('1',plain,[r2_hidden(k1_group_1(15 ^ [], 17 ^ [], 18 ^ []), k1_funct_1(k1_latsubgr(15 ^ []), 16 ^ []))],start(11)).
% 0.39/1.42 cnf('1.1',plain,[-(r2_hidden(k1_group_1(15 ^ [], 17 ^ [], 18 ^ []), k1_funct_1(k1_latsubgr(15 ^ []), 16 ^ []))), l1_group_1(15 ^ []), v4_group_1(15 ^ []), v3_group_1(15 ^ []), -(v3_struct_0(15 ^ [])), m1_group_2(16 ^ [], 15 ^ []), v1_group_1(16 ^ []), m1_subset_1(k1_group_1(15 ^ [], 17 ^ [], 18 ^ []), u1_struct_0(15 ^ [])), r1_rlvect_1(16 ^ [], k1_group_1(15 ^ [], 17 ^ [], 18 ^ []))],extension(14,bind([[_61164, _61473, _61658], [15 ^ [], 16 ^ [], k1_group_1(15 ^ [], 17 ^ [], 18 ^ [])]]))).
% 0.39/1.42 cnf('1.1.1',plain,[-(l1_group_1(15 ^ []))],extension(4)).
% 0.39/1.42 cnf('1.1.2',plain,[-(v4_group_1(15 ^ []))],extension(3)).
% 0.39/1.42 cnf('1.1.3',plain,[-(v3_group_1(15 ^ []))],extension(2)).
% 0.39/1.42 cnf('1.1.4',plain,[v3_struct_0(15 ^ [])],extension(1)).
% 0.39/1.42 cnf('1.1.5',plain,[-(m1_group_2(16 ^ [], 15 ^ []))],extension(6)).
% 0.39/1.42 cnf('1.1.6',plain,[-(v1_group_1(16 ^ []))],extension(5)).
% 0.39/1.42 cnf('1.1.7',plain,[-(m1_subset_1(k1_group_1(15 ^ [], 17 ^ [], 18 ^ []), u1_struct_0(15 ^ []))), -(v3_struct_0(15 ^ [])), l1_group_1(15 ^ []), m1_subset_1(17 ^ [], u1_struct_0(15 ^ [])), m1_subset_1(18 ^ [], u1_struct_0(15 ^ []))],extension(12,bind([[_48942, _49019, _48864], [17 ^ [], 18 ^ [], 15 ^ []]]))).
% 0.39/1.42 cnf('1.1.7.1',plain,[v3_struct_0(15 ^ [])],extension(1)).
% 0.39/1.42 cnf('1.1.7.2',plain,[-(l1_group_1(15 ^ []))],extension(4)).
% 0.39/1.42 cnf('1.1.7.3',plain,[-(m1_subset_1(17 ^ [], u1_struct_0(15 ^ [])))],extension(7)).
% 0.39/1.42 cnf('1.1.7.4',plain,[-(m1_subset_1(18 ^ [], u1_struct_0(15 ^ [])))],extension(8)).
% 0.39/1.42 cnf('1.1.8',plain,[-(r1_rlvect_1(16 ^ [], k1_group_1(15 ^ [], 17 ^ [], 18 ^ []))), l1_group_1(15 ^ []), v4_group_1(15 ^ []), v3_group_1(15 ^ []), -(v3_struct_0(15 ^ [])), m1_subset_1(17 ^ [], u1_struct_0(15 ^ [])), m1_subset_1(18 ^ [], u1_struct_0(15 ^ [])), m1_group_2(16 ^ [], 15 ^ []), r1_rlvect_1(16 ^ [], 17 ^ []), r1_rlvect_1(16 ^ [], 18 ^ [])],extension(15,bind([[_63622, _63944, _64257, _64105], [15 ^ [], 17 ^ [], 16 ^ [], 18 ^ []]]))).
% 0.39/1.42 cnf('1.1.8.1',plain,[-(l1_group_1(15 ^ []))],extension(4)).
% 0.39/1.42 cnf('1.1.8.2',plain,[-(v4_group_1(15 ^ []))],extension(3)).
% 0.39/1.42 cnf('1.1.8.3',plain,[-(v3_group_1(15 ^ []))],extension(2)).
% 0.39/1.42 cnf('1.1.8.4',plain,[v3_struct_0(15 ^ [])],extension(1)).
% 0.39/1.42 cnf('1.1.8.5',plain,[-(m1_subset_1(17 ^ [], u1_struct_0(15 ^ [])))],extension(7)).
% 0.39/1.42 cnf('1.1.8.6',plain,[-(m1_subset_1(18 ^ [], u1_struct_0(15 ^ [])))],extension(8)).
% 0.39/1.42 cnf('1.1.8.7',plain,[-(m1_group_2(16 ^ [], 15 ^ []))],extension(6)).
% 0.39/1.42 cnf('1.1.8.8',plain,[-(r1_rlvect_1(16 ^ [], 17 ^ [])), l1_group_1(15 ^ []), v4_group_1(15 ^ []), v3_group_1(15 ^ []), -(v3_struct_0(15 ^ [])), m1_group_2(16 ^ [], 15 ^ []), v1_group_1(16 ^ []), m1_subset_1(17 ^ [], u1_struct_0(15 ^ [])), r2_hidden(17 ^ [], k1_funct_1(k1_latsubgr(15 ^ []), 16 ^ []))],extension(13,bind([[_61658, _61164, _61473], [17 ^ [], 15 ^ [], 16 ^ []]]))).
% 0.39/1.42 cnf('1.1.8.8.1',plain,[-(l1_group_1(15 ^ []))],extension(4)).
% 0.39/1.42 cnf('1.1.8.8.2',plain,[-(v4_group_1(15 ^ []))],extension(3)).
% 0.39/1.42 cnf('1.1.8.8.3',plain,[-(v3_group_1(15 ^ []))],extension(2)).
% 0.39/1.42 cnf('1.1.8.8.4',plain,[v3_struct_0(15 ^ [])],extension(1)).
% 0.39/1.42 cnf('1.1.8.8.5',plain,[-(m1_group_2(16 ^ [], 15 ^ []))],extension(6)).
% 0.39/1.42 cnf('1.1.8.8.6',plain,[-(v1_group_1(16 ^ []))],extension(5)).
% 0.39/1.42 cnf('1.1.8.8.7',plain,[-(m1_subset_1(17 ^ [], u1_struct_0(15 ^ [])))],extension(7)).
% 0.39/1.42 cnf('1.1.8.8.8',plain,[-(r2_hidden(17 ^ [], k1_funct_1(k1_latsubgr(15 ^ []), 16 ^ [])))],extension(9)).
% 0.39/1.42 cnf('1.1.8.9',plain,[-(r1_rlvect_1(16 ^ [], 18 ^ [])), l1_group_1(15 ^ []), v4_group_1(15 ^ []), v3_group_1(15 ^ []), -(v3_struct_0(15 ^ [])), m1_group_2(16 ^ [], 15 ^ []), v1_group_1(16 ^ []), m1_subset_1(18 ^ [], u1_struct_0(15 ^ [])), r2_hidden(18 ^ [], k1_funct_1(k1_latsubgr(15 ^ []), 16 ^ []))],extension(13,bind([[_61658, _61164, _61473], [18 ^ [], 15 ^ [], 16 ^ []]]))).
% 0.39/1.42 cnf('1.1.8.9.1',plain,[-(l1_group_1(15 ^ []))],extension(4)).
% 0.39/1.42 cnf('1.1.8.9.2',plain,[-(v4_group_1(15 ^ []))],extension(3)).
% 0.39/1.42 cnf('1.1.8.9.3',plain,[-(v3_group_1(15 ^ []))],extension(2)).
% 0.39/1.42 cnf('1.1.8.9.4',plain,[v3_struct_0(15 ^ [])],extension(1)).
% 0.39/1.42 cnf('1.1.8.9.5',plain,[-(m1_group_2(16 ^ [], 15 ^ []))],extension(6)).
% 0.39/1.42 cnf('1.1.8.9.6',plain,[-(v1_group_1(16 ^ []))],extension(5)).
% 0.39/1.42 cnf('1.1.8.9.7',plain,[-(m1_subset_1(18 ^ [], u1_struct_0(15 ^ [])))],extension(8)).
% 0.39/1.42 cnf('1.1.8.9.8',plain,[-(r2_hidden(18 ^ [], k1_funct_1(k1_latsubgr(15 ^ []), 16 ^ [])))],extension(10)).
% 0.39/1.42 %-----------------------------------------------------
% 0.39/1.43
% 0.39/1.43 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------