%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : LAT327+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n013.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 : Sun Jul 17 05:42:50 EDT 2022
% Result : Theorem 0.35s 1.42s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : LAT327+1 : TPTP v8.1.0. Released v3.4.0.
% 0.07/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.35 % Computer : n013.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Wed Jun 29 09:12:29 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.35/1.42 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.35/1.43 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.35/1.43
% 0.35/1.43 %-----------------------------------------------------
% 0.35/1.43 fof(t64_filter_2, conjecture, ! [_78920] : (~ v3_struct_0(_78920) & v10_lattices(_78920) & l3_lattices(_78920) => ! [_78951] : (m1_subset_1(_78951, u1_struct_0(_78920)) => ! [_78973] : (m1_subset_1(_78973, u1_struct_0(_78920)) => r3_lattices(_78920, _78951, _78973) => r2_hidden(_78951, k22_filter_2(_78920, _78951, _78973)) & r2_hidden(_78973, k22_filter_2(_78920, _78951, _78973))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t64_filter_2)).
% 0.35/1.43 fof(reflexivity_r3_lattices, axiom, ! [_79465, _79468, _79471] : (~ v3_struct_0(_79465) & v6_lattices(_79465) & v8_lattices(_79465) & v9_lattices(_79465) & l3_lattices(_79465) & m1_subset_1(_79468, u1_struct_0(_79465)) & m1_subset_1(_79471, u1_struct_0(_79465)) => r3_lattices(_79465, _79468, _79468)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity_r3_lattices)).
% 0.35/1.43 fof(cc1_lattices, axiom, ! [_79797] : (l3_lattices(_79797) => ~ v3_struct_0(_79797) & v10_lattices(_79797) => ~ v3_struct_0(_79797) & v4_lattices(_79797) & v5_lattices(_79797) & v6_lattices(_79797) & v7_lattices(_79797) & v8_lattices(_79797) & v9_lattices(_79797)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc1_lattices)).
% 0.35/1.43 fof(t63_filter_2, axiom, ! [_80129] : (~ v3_struct_0(_80129) & v10_lattices(_80129) & l3_lattices(_80129) => ! [_80160] : (m1_subset_1(_80160, u1_struct_0(_80129)) => ! [_80182] : (m1_subset_1(_80182, u1_struct_0(_80129)) => ! [_80204] : (m1_subset_1(_80204, u1_struct_0(_80129)) => r3_lattices(_80129, _80160, _80182) => (r2_hidden(_80204, k22_filter_2(_80129, _80160, _80182)) <=> r3_lattices(_80129, _80160, _80204) & r3_lattices(_80129, _80204, _80182)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t63_filter_2)).
% 0.35/1.43
% 0.35/1.43 cnf(1, plain, [v3_struct_0(14 ^ [])], clausify(t64_filter_2)).
% 0.35/1.43 cnf(2, plain, [-(v10_lattices(14 ^ []))], clausify(t64_filter_2)).
% 0.35/1.43 cnf(3, plain, [-(l3_lattices(14 ^ []))], clausify(t64_filter_2)).
% 0.35/1.43 cnf(4, plain, [-(m1_subset_1(15 ^ [], u1_struct_0(14 ^ [])))], clausify(t64_filter_2)).
% 0.35/1.43 cnf(5, plain, [-(m1_subset_1(16 ^ [], u1_struct_0(14 ^ [])))], clausify(t64_filter_2)).
% 0.35/1.43 cnf(6, plain, [-(r3_lattices(14 ^ [], 15 ^ [], 16 ^ []))], clausify(t64_filter_2)).
% 0.35/1.43 cnf(7, plain, [r2_hidden(15 ^ [], k22_filter_2(14 ^ [], 15 ^ [], 16 ^ [])), r2_hidden(16 ^ [], k22_filter_2(14 ^ [], 15 ^ [], 16 ^ []))], clausify(t64_filter_2)).
% 0.35/1.43 cnf(8, plain, [-(r3_lattices(_41980, _42068, _42068)), -(v3_struct_0(_41980)), v6_lattices(_41980), v8_lattices(_41980), v9_lattices(_41980), l3_lattices(_41980), m1_subset_1(_42068, u1_struct_0(_41980)), m1_subset_1(_42155, u1_struct_0(_41980))], clausify(reflexivity_r3_lattices)).
% 0.35/1.43 cnf(9, plain, [l3_lattices(_45864), -(v6_lattices(_45864)), -(v3_struct_0(_45864)), v10_lattices(_45864)], clausify(cc1_lattices)).
% 0.35/1.43 cnf(10, plain, [l3_lattices(_45864), -(v8_lattices(_45864)), -(v3_struct_0(_45864)), v10_lattices(_45864)], clausify(cc1_lattices)).
% 0.35/1.43 cnf(11, plain, [l3_lattices(_45864), -(v9_lattices(_45864)), -(v3_struct_0(_45864)), v10_lattices(_45864)], clausify(cc1_lattices)).
% 0.35/1.43 cnf(12, plain, [l3_lattices(_47181), v10_lattices(_47181), -(v3_struct_0(_47181)), m1_subset_1(_47456, u1_struct_0(_47181)), m1_subset_1(_47628, u1_struct_0(_47181)), m1_subset_1(_47791, u1_struct_0(_47181)), r3_lattices(_47181, _47456, _47628), -(r2_hidden(_47791, k22_filter_2(_47181, _47456, _47628))), r3_lattices(_47181, _47456, _47791), r3_lattices(_47181, _47791, _47628)], clausify(t63_filter_2)).
% 0.35/1.43
% 0.35/1.43 cnf('1',plain,[r2_hidden(15 ^ [], k22_filter_2(14 ^ [], 15 ^ [], 16 ^ [])), r2_hidden(16 ^ [], k22_filter_2(14 ^ [], 15 ^ [], 16 ^ []))],start(7)).
% 0.35/1.43 cnf('1.1',plain,[-(r2_hidden(15 ^ [], k22_filter_2(14 ^ [], 15 ^ [], 16 ^ []))), l3_lattices(14 ^ []), v10_lattices(14 ^ []), -(v3_struct_0(14 ^ [])), m1_subset_1(15 ^ [], u1_struct_0(14 ^ [])), m1_subset_1(16 ^ [], u1_struct_0(14 ^ [])), m1_subset_1(15 ^ [], u1_struct_0(14 ^ [])), r3_lattices(14 ^ [], 15 ^ [], 16 ^ []), r3_lattices(14 ^ [], 15 ^ [], 15 ^ []), r3_lattices(14 ^ [], 15 ^ [], 16 ^ [])],extension(12,bind([[_47456, _47181, _47791, _47628], [15 ^ [], 14 ^ [], 15 ^ [], 16 ^ []]]))).
% 0.35/1.43 cnf('1.1.1',plain,[-(l3_lattices(14 ^ []))],extension(3)).
% 0.35/1.43 cnf('1.1.2',plain,[-(v10_lattices(14 ^ []))],extension(2)).
% 0.35/1.43 cnf('1.1.3',plain,[v3_struct_0(14 ^ [])],extension(1)).
% 0.35/1.43 cnf('1.1.4',plain,[-(m1_subset_1(15 ^ [], u1_struct_0(14 ^ [])))],extension(4)).
% 0.35/1.43 cnf('1.1.5',plain,[-(m1_subset_1(16 ^ [], u1_struct_0(14 ^ [])))],extension(5)).
% 0.35/1.43 cnf('1.1.6',plain,[-(m1_subset_1(15 ^ [], u1_struct_0(14 ^ [])))],extension(4)).
% 0.35/1.43 cnf('1.1.7',plain,[-(r3_lattices(14 ^ [], 15 ^ [], 16 ^ []))],extension(6)).
% 0.35/1.43 cnf('1.1.8',plain,[-(r3_lattices(14 ^ [], 15 ^ [], 15 ^ [])), -(v3_struct_0(14 ^ [])), v6_lattices(14 ^ []), v8_lattices(14 ^ []), v9_lattices(14 ^ []), l3_lattices(14 ^ []), m1_subset_1(15 ^ [], u1_struct_0(14 ^ [])), m1_subset_1(15 ^ [], u1_struct_0(14 ^ []))],extension(8,bind([[_42068, _42155, _41980], [15 ^ [], 15 ^ [], 14 ^ []]]))).
% 0.35/1.43 cnf('1.1.8.1',plain,[v3_struct_0(14 ^ [])],extension(1)).
% 0.35/1.43 cnf('1.1.8.2',plain,[-(v6_lattices(14 ^ [])), l3_lattices(14 ^ []), -(v3_struct_0(14 ^ [])), v10_lattices(14 ^ [])],extension(9,bind([[_45864], [14 ^ []]]))).
% 0.35/1.43 cnf('1.1.8.2.1',plain,[-(l3_lattices(14 ^ []))],extension(3)).
% 0.35/1.43 cnf('1.1.8.2.2',plain,[v3_struct_0(14 ^ [])],extension(1)).
% 0.35/1.43 cnf('1.1.8.2.3',plain,[-(v10_lattices(14 ^ []))],extension(2)).
% 0.35/1.43 cnf('1.1.8.3',plain,[-(v8_lattices(14 ^ [])), l3_lattices(14 ^ []), -(v3_struct_0(14 ^ [])), v10_lattices(14 ^ [])],extension(10,bind([[_45864], [14 ^ []]]))).
% 0.35/1.43 cnf('1.1.8.3.1',plain,[-(l3_lattices(14 ^ []))],extension(3)).
% 0.35/1.43 cnf('1.1.8.3.2',plain,[v3_struct_0(14 ^ [])],extension(1)).
% 0.35/1.43 cnf('1.1.8.3.3',plain,[-(v10_lattices(14 ^ []))],extension(2)).
% 0.35/1.43 cnf('1.1.8.4',plain,[-(v9_lattices(14 ^ [])), l3_lattices(14 ^ []), -(v3_struct_0(14 ^ [])), v10_lattices(14 ^ [])],extension(11,bind([[_45864], [14 ^ []]]))).
% 0.35/1.43 cnf('1.1.8.4.1',plain,[-(l3_lattices(14 ^ []))],extension(3)).
% 0.35/1.43 cnf('1.1.8.4.2',plain,[v3_struct_0(14 ^ [])],extension(1)).
% 0.35/1.43 cnf('1.1.8.4.3',plain,[-(v10_lattices(14 ^ []))],extension(2)).
% 0.35/1.43 cnf('1.1.8.5',plain,[-(l3_lattices(14 ^ []))],extension(3)).
% 0.35/1.43 cnf('1.1.8.6',plain,[-(m1_subset_1(15 ^ [], u1_struct_0(14 ^ [])))],extension(4)).
% 0.35/1.43 cnf('1.1.8.7',plain,[-(m1_subset_1(15 ^ [], u1_struct_0(14 ^ [])))],extension(4)).
% 0.35/1.43 cnf('1.1.9',plain,[-(r3_lattices(14 ^ [], 15 ^ [], 16 ^ []))],extension(6)).
% 0.35/1.43 cnf('1.2',plain,[-(r2_hidden(16 ^ [], k22_filter_2(14 ^ [], 15 ^ [], 16 ^ []))), l3_lattices(14 ^ []), v10_lattices(14 ^ []), -(v3_struct_0(14 ^ [])), m1_subset_1(15 ^ [], u1_struct_0(14 ^ [])), m1_subset_1(16 ^ [], u1_struct_0(14 ^ [])), m1_subset_1(16 ^ [], u1_struct_0(14 ^ [])), r3_lattices(14 ^ [], 15 ^ [], 16 ^ []), r3_lattices(14 ^ [], 15 ^ [], 16 ^ []), r3_lattices(14 ^ [], 16 ^ [], 16 ^ [])],extension(12,bind([[_47456, _47181, _47791, _47628], [15 ^ [], 14 ^ [], 16 ^ [], 16 ^ []]]))).
% 0.35/1.43 cnf('1.2.1',plain,[-(l3_lattices(14 ^ []))],extension(3)).
% 0.35/1.43 cnf('1.2.2',plain,[-(v10_lattices(14 ^ []))],extension(2)).
% 0.35/1.43 cnf('1.2.3',plain,[v3_struct_0(14 ^ [])],extension(1)).
% 0.35/1.43 cnf('1.2.4',plain,[-(m1_subset_1(15 ^ [], u1_struct_0(14 ^ [])))],extension(4)).
% 0.35/1.43 cnf('1.2.5',plain,[-(m1_subset_1(16 ^ [], u1_struct_0(14 ^ [])))],extension(5)).
% 0.35/1.43 cnf('1.2.6',plain,[-(m1_subset_1(16 ^ [], u1_struct_0(14 ^ [])))],extension(5)).
% 0.35/1.43 cnf('1.2.7',plain,[-(r3_lattices(14 ^ [], 15 ^ [], 16 ^ []))],extension(6)).
% 0.35/1.43 cnf('1.2.8',plain,[-(r3_lattices(14 ^ [], 15 ^ [], 16 ^ []))],extension(6)).
% 0.35/1.43 cnf('1.2.9',plain,[-(r3_lattices(14 ^ [], 16 ^ [], 16 ^ [])), -(v3_struct_0(14 ^ [])), v6_lattices(14 ^ []), v8_lattices(14 ^ []), v9_lattices(14 ^ []), l3_lattices(14 ^ []), m1_subset_1(16 ^ [], u1_struct_0(14 ^ [])), m1_subset_1(15 ^ [], u1_struct_0(14 ^ []))],extension(8,bind([[_42068, _42155, _41980], [16 ^ [], 15 ^ [], 14 ^ []]]))).
% 0.35/1.43 cnf('1.2.9.1',plain,[v3_struct_0(14 ^ [])],extension(1)).
% 0.35/1.43 cnf('1.2.9.2',plain,[-(v6_lattices(14 ^ [])), l3_lattices(14 ^ []), -(v3_struct_0(14 ^ [])), v10_lattices(14 ^ [])],extension(9,bind([[_45864], [14 ^ []]]))).
% 0.35/1.43 cnf('1.2.9.2.1',plain,[-(l3_lattices(14 ^ []))],extension(3)).
% 0.35/1.43 cnf('1.2.9.2.2',plain,[v3_struct_0(14 ^ [])],extension(1)).
% 0.35/1.43 cnf('1.2.9.2.3',plain,[-(v10_lattices(14 ^ []))],extension(2)).
% 0.35/1.43 cnf('1.2.9.3',plain,[-(v8_lattices(14 ^ [])), l3_lattices(14 ^ []), -(v3_struct_0(14 ^ [])), v10_lattices(14 ^ [])],extension(10,bind([[_45864], [14 ^ []]]))).
% 0.35/1.43 cnf('1.2.9.3.1',plain,[-(l3_lattices(14 ^ []))],extension(3)).
% 0.35/1.43 cnf('1.2.9.3.2',plain,[v3_struct_0(14 ^ [])],extension(1)).
% 0.35/1.43 cnf('1.2.9.3.3',plain,[-(v10_lattices(14 ^ []))],extension(2)).
% 0.35/1.43 cnf('1.2.9.4',plain,[-(v9_lattices(14 ^ [])), l3_lattices(14 ^ []), -(v3_struct_0(14 ^ [])), v10_lattices(14 ^ [])],extension(11,bind([[_45864], [14 ^ []]]))).
% 0.35/1.43 cnf('1.2.9.4.1',plain,[-(l3_lattices(14 ^ []))],extension(3)).
% 0.35/1.43 cnf('1.2.9.4.2',plain,[v3_struct_0(14 ^ [])],extension(1)).
% 0.35/1.43 cnf('1.2.9.4.3',plain,[-(v10_lattices(14 ^ []))],extension(2)).
% 0.35/1.43 cnf('1.2.9.5',plain,[-(l3_lattices(14 ^ []))],extension(3)).
% 0.35/1.43 cnf('1.2.9.6',plain,[-(m1_subset_1(16 ^ [], u1_struct_0(14 ^ [])))],extension(5)).
% 0.35/1.43 cnf('1.2.9.7',plain,[-(m1_subset_1(15 ^ [], u1_struct_0(14 ^ [])))],extension(4)).
% 0.35/1.43 %-----------------------------------------------------
% 0.35/1.44
% 0.35/1.44 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------