%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : LAT319+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n017.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:42 EDT 2022
% Result : Theorem 20.87s 21.01s
% Output : Proof 20.87s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : LAT319+1 : TPTP v8.1.0. Released v3.4.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.13/0.33 % Computer : n017.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Thu Jun 30 01:22:38 EDT 2022
% 0.13/0.34 % CPUTime :
% 20.87/21.01 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.87/21.02 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.87/21.02
% 20.87/21.02 %-----------------------------------------------------
% 20.87/21.02 fof(t54_filter_2, conjecture, ! [_178708] : (~ v3_struct_0(_178708) & v10_lattices(_178708) & l3_lattices(_178708) => (~ v3_struct_0(_178708) & v10_lattices(_178708) & v17_lattices(_178708) & l3_lattices(_178708) <=> ~ v3_struct_0(k1_lattice2(_178708)) & v10_lattices(k1_lattice2(_178708)) & v17_lattices(k1_lattice2(_178708)) & l3_lattices(k1_lattice2(_178708)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t54_filter_2)).
% 20.87/21.02 fof(cc2_lattices, axiom, ! [_179272] : (l3_lattices(_179272) => ~ v3_struct_0(_179272) & v4_lattices(_179272) & v5_lattices(_179272) & v6_lattices(_179272) & v7_lattices(_179272) & v8_lattices(_179272) & v9_lattices(_179272) => ~ v3_struct_0(_179272) & v10_lattices(_179272)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', cc2_lattices)).
% 20.87/21.02 fof(cc5_lattices, axiom, ! [_179578] : (l3_lattices(_179578) => ~ v3_struct_0(_179578) & v17_lattices(_179578) => ~ v3_struct_0(_179578) & v11_lattices(_179578) & v13_lattices(_179578) & v14_lattices(_179578) & v15_lattices(_179578) & v16_lattices(_179578)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', cc5_lattices)).
% 20.87/21.02 fof(cc6_lattices, axiom, ! [_179886] : (l3_lattices(_179886) => ~ v3_struct_0(_179886) & v11_lattices(_179886) & v15_lattices(_179886) & v16_lattices(_179886) => ~ v3_struct_0(_179886) & v17_lattices(_179886)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', cc6_lattices)).
% 20.87/21.02 fof(dt_k1_lattice2, axiom, ! [_180141] : (l3_lattices(_180141) => v3_lattices(k1_lattice2(_180141)) & l3_lattices(k1_lattice2(_180141))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', dt_k1_lattice2)).
% 20.87/21.02 fof(fc1_lattice2, axiom, ! [_180319] : (~ v3_struct_0(_180319) & l3_lattices(_180319) => ~ v3_struct_0(k1_lattice2(_180319)) & v3_lattices(k1_lattice2(_180319))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', fc1_lattice2)).
% 20.87/21.02 fof(fc6_lattice2, axiom, ! [_180543] : (~ v3_struct_0(_180543) & v10_lattices(_180543) & l3_lattices(_180543) => ~ v3_struct_0(k1_lattice2(_180543)) & v3_lattices(k1_lattice2(_180543)) & v4_lattices(k1_lattice2(_180543)) & v5_lattices(k1_lattice2(_180543)) & v6_lattices(k1_lattice2(_180543)) & v7_lattices(k1_lattice2(_180543)) & v8_lattices(k1_lattice2(_180543)) & v9_lattices(k1_lattice2(_180543)) & v10_lattices(k1_lattice2(_180543))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', fc6_lattice2)).
% 20.87/21.02 fof(t53_filter_2, axiom, ! [_181133] : (~ v3_struct_0(_181133) & v10_lattices(_181133) & l3_lattices(_181133) => (~ v3_struct_0(_181133) & v10_lattices(_181133) & v15_lattices(_181133) & v16_lattices(_181133) & l3_lattices(_181133) <=> ~ v3_struct_0(k1_lattice2(_181133)) & v10_lattices(k1_lattice2(_181133)) & v15_lattices(k1_lattice2(_181133)) & v16_lattices(k1_lattice2(_181133)) & l3_lattices(k1_lattice2(_181133)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t53_filter_2)).
% 20.87/21.02 fof(t65_lattice2, axiom, ! [_181594] : (~ v3_struct_0(_181594) & v10_lattices(_181594) & l3_lattices(_181594) => (~ v3_struct_0(_181594) & v10_lattices(_181594) & v11_lattices(_181594) & l3_lattices(_181594) <=> ~ v3_struct_0(k1_lattice2(_181594)) & v10_lattices(k1_lattice2(_181594)) & v11_lattices(k1_lattice2(_181594)) & l3_lattices(k1_lattice2(_181594)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t65_lattice2)).
% 20.87/21.02
% 20.87/21.02 cnf(1, plain, [-(26 ^ []), -(v3_struct_0(24 ^ [])), v10_lattices(24 ^ []), v17_lattices(24 ^ []), l3_lattices(24 ^ [])], clausify(t54_filter_2)).
% 20.87/21.02 cnf(2, plain, [-(26 ^ []), -(l3_lattices(k1_lattice2(24 ^ [])))], clausify(t54_filter_2)).
% 20.87/21.02 cnf(3, plain, [-(26 ^ []), -(v17_lattices(k1_lattice2(24 ^ [])))], clausify(t54_filter_2)).
% 20.87/21.02 cnf(4, plain, [-(26 ^ []), -(v10_lattices(k1_lattice2(24 ^ [])))], clausify(t54_filter_2)).
% 20.87/21.02 cnf(5, plain, [-(26 ^ []), v3_struct_0(k1_lattice2(24 ^ []))], clausify(t54_filter_2)).
% 20.87/21.02 cnf(6, plain, [-(25 ^ []), -(v3_struct_0(k1_lattice2(24 ^ []))), v10_lattices(k1_lattice2(24 ^ [])), v17_lattices(k1_lattice2(24 ^ [])), l3_lattices(k1_lattice2(24 ^ []))], clausify(t54_filter_2)).
% 20.87/21.02 cnf(7, plain, [-(25 ^ []), -(l3_lattices(24 ^ []))], clausify(t54_filter_2)).
% 20.87/21.02 cnf(8, plain, [-(25 ^ []), -(v17_lattices(24 ^ []))], clausify(t54_filter_2)).
% 20.87/21.02 cnf(9, plain, [-(25 ^ []), -(v10_lattices(24 ^ []))], clausify(t54_filter_2)).
% 20.87/21.02 cnf(10, plain, [-(25 ^ []), v3_struct_0(24 ^ [])], clausify(t54_filter_2)).
% 20.87/21.02 cnf(11, plain, [v3_struct_0(24 ^ [])], clausify(t54_filter_2)).
% 20.87/21.02 cnf(12, plain, [-(v10_lattices(24 ^ []))], clausify(t54_filter_2)).
% 20.87/21.02 cnf(13, plain, [-(l3_lattices(24 ^ []))], clausify(t54_filter_2)).
% 20.87/21.02 cnf(14, plain, [25 ^ [], 26 ^ []], clausify(t54_filter_2)).
% 20.87/21.02 cnf(15, plain, [l3_lattices(_71532), -(v10_lattices(_71532)), -(v3_struct_0(_71532)), v4_lattices(_71532), v5_lattices(_71532), v6_lattices(_71532), v7_lattices(_71532), v8_lattices(_71532), v9_lattices(_71532)], clausify(cc2_lattices)).
% 20.87/21.02 cnf(16, plain, [l3_lattices(_73198), -(v11_lattices(_73198)), -(v3_struct_0(_73198)), v17_lattices(_73198)], clausify(cc5_lattices)).
% 20.87/21.02 cnf(17, plain, [l3_lattices(_73198), -(v15_lattices(_73198)), -(v3_struct_0(_73198)), v17_lattices(_73198)], clausify(cc5_lattices)).
% 20.87/21.02 cnf(18, plain, [l3_lattices(_73198), -(v16_lattices(_73198)), -(v3_struct_0(_73198)), v17_lattices(_73198)], clausify(cc5_lattices)).
% 20.87/21.02 cnf(19, plain, [l3_lattices(_73850), -(v17_lattices(_73850)), -(v3_struct_0(_73850)), v11_lattices(_73850), v15_lattices(_73850), v16_lattices(_73850)], clausify(cc6_lattices)).
% 20.87/21.02 cnf(20, plain, [l3_lattices(_77480), -(l3_lattices(k1_lattice2(_77480)))], clausify(dt_k1_lattice2)).
% 20.87/21.02 cnf(21, plain, [v3_struct_0(k1_lattice2(_82768)), -(v3_struct_0(_82768)), l3_lattices(_82768)], clausify(fc1_lattice2)).
% 20.87/21.02 cnf(22, plain, [-(v4_lattices(k1_lattice2(_89775))), -(v3_struct_0(_89775)), v10_lattices(_89775), l3_lattices(_89775)], clausify(fc6_lattice2)).
% 20.87/21.02 cnf(23, plain, [-(v5_lattices(k1_lattice2(_89775))), -(v3_struct_0(_89775)), v10_lattices(_89775), l3_lattices(_89775)], clausify(fc6_lattice2)).
% 20.87/21.02 cnf(24, plain, [-(v6_lattices(k1_lattice2(_89775))), -(v3_struct_0(_89775)), v10_lattices(_89775), l3_lattices(_89775)], clausify(fc6_lattice2)).
% 20.87/21.02 cnf(25, plain, [-(v7_lattices(k1_lattice2(_89775))), -(v3_struct_0(_89775)), v10_lattices(_89775), l3_lattices(_89775)], clausify(fc6_lattice2)).
% 20.87/21.02 cnf(26, plain, [-(v8_lattices(k1_lattice2(_89775))), -(v3_struct_0(_89775)), v10_lattices(_89775), l3_lattices(_89775)], clausify(fc6_lattice2)).
% 20.87/21.02 cnf(27, plain, [-(v9_lattices(k1_lattice2(_89775))), -(v3_struct_0(_89775)), v10_lattices(_89775), l3_lattices(_89775)], clausify(fc6_lattice2)).
% 20.87/21.02 cnf(28, plain, [-(v15_lattices(k1_lattice2(_102301))), -(v3_struct_0(_102301)), v10_lattices(_102301), v15_lattices(_102301), v16_lattices(_102301), l3_lattices(_102301)], clausify(t53_filter_2)).
% 20.87/21.02 cnf(29, plain, [-(v16_lattices(k1_lattice2(_102301))), -(v3_struct_0(_102301)), v10_lattices(_102301), v15_lattices(_102301), v16_lattices(_102301), l3_lattices(_102301)], clausify(t53_filter_2)).
% 20.87/21.02 cnf(30, plain, [l3_lattices(_102301), v10_lattices(_102301), -(v3_struct_0(_102301)), -(v15_lattices(_102301)), -(v3_struct_0(k1_lattice2(_102301))), v10_lattices(k1_lattice2(_102301)), v15_lattices(k1_lattice2(_102301)), v16_lattices(k1_lattice2(_102301)), l3_lattices(k1_lattice2(_102301))], clausify(t53_filter_2)).
% 20.87/21.02 cnf(31, plain, [l3_lattices(_102301), v10_lattices(_102301), -(v3_struct_0(_102301)), -(v16_lattices(_102301)), -(v3_struct_0(k1_lattice2(_102301))), v10_lattices(k1_lattice2(_102301)), v15_lattices(k1_lattice2(_102301)), v16_lattices(k1_lattice2(_102301)), l3_lattices(k1_lattice2(_102301))], clausify(t53_filter_2)).
% 20.87/21.02 cnf(32, plain, [-(v11_lattices(k1_lattice2(_103780))), -(v3_struct_0(_103780)), v10_lattices(_103780), v11_lattices(_103780), l3_lattices(_103780)], clausify(t65_lattice2)).
% 20.87/21.02 cnf(33, plain, [l3_lattices(_103780), v10_lattices(_103780), -(v3_struct_0(_103780)), -(v11_lattices(_103780)), -(v3_struct_0(k1_lattice2(_103780))), v10_lattices(k1_lattice2(_103780)), v11_lattices(k1_lattice2(_103780)), l3_lattices(k1_lattice2(_103780))], clausify(t65_lattice2)).
% 20.87/21.02
% 20.87/21.02 cnf('1',plain,[25 ^ [], 26 ^ []],start(14)).
% 20.87/21.02 cnf('1.1',plain,[-(25 ^ []), -(v3_struct_0(k1_lattice2(24 ^ []))), v10_lattices(k1_lattice2(24 ^ [])), v17_lattices(k1_lattice2(24 ^ [])), l3_lattices(k1_lattice2(24 ^ []))],extension(6)).
% 20.87/21.02 cnf('1.1.1',plain,[v3_struct_0(k1_lattice2(24 ^ [])), -(v3_struct_0(24 ^ [])), l3_lattices(24 ^ [])],extension(21,bind([[_82768], [24 ^ []]]))).
% 20.87/21.02 cnf('1.1.1.1',plain,[v3_struct_0(24 ^ []), -(25 ^ [])],extension(10)).
% 20.87/21.02 cnf('1.1.1.1.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.02 cnf('1.1.1.2',plain,[-(l3_lattices(24 ^ [])), -(25 ^ [])],extension(7)).
% 20.87/21.02 cnf('1.1.1.2.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.02 cnf('1.1.2',plain,[-(v10_lattices(k1_lattice2(24 ^ []))), l3_lattices(k1_lattice2(24 ^ [])), -(v3_struct_0(k1_lattice2(24 ^ []))), v4_lattices(k1_lattice2(24 ^ [])), v5_lattices(k1_lattice2(24 ^ [])), v6_lattices(k1_lattice2(24 ^ [])), v7_lattices(k1_lattice2(24 ^ [])), v8_lattices(k1_lattice2(24 ^ [])), v9_lattices(k1_lattice2(24 ^ []))],extension(15,bind([[_71532], [k1_lattice2(24 ^ [])]]))).
% 20.87/21.02 cnf('1.1.2.1',plain,[-(l3_lattices(k1_lattice2(24 ^ []))), l3_lattices(24 ^ [])],extension(20,bind([[_77480], [24 ^ []]]))).
% 20.87/21.02 cnf('1.1.2.1.1',plain,[-(l3_lattices(24 ^ [])), -(25 ^ [])],extension(7)).
% 20.87/21.02 cnf('1.1.2.1.1.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.02 cnf('1.1.2.2',plain,[v3_struct_0(k1_lattice2(24 ^ []))],lemmata('1.1')).
% 20.87/21.02 cnf('1.1.2.3',plain,[-(v4_lattices(k1_lattice2(24 ^ []))), -(v3_struct_0(24 ^ [])), v10_lattices(24 ^ []), l3_lattices(24 ^ [])],extension(22,bind([[_89775], [24 ^ []]]))).
% 20.87/21.02 cnf('1.1.2.3.1',plain,[v3_struct_0(24 ^ []), -(25 ^ [])],extension(10)).
% 20.87/21.02 cnf('1.1.2.3.1.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.02 cnf('1.1.2.3.2',plain,[-(v10_lattices(24 ^ [])), -(25 ^ [])],extension(9)).
% 20.87/21.02 cnf('1.1.2.3.2.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.02 cnf('1.1.2.3.3',plain,[-(l3_lattices(24 ^ [])), -(25 ^ [])],extension(7)).
% 20.87/21.02 cnf('1.1.2.3.3.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.02 cnf('1.1.2.4',plain,[-(v5_lattices(k1_lattice2(24 ^ []))), -(v3_struct_0(24 ^ [])), v10_lattices(24 ^ []), l3_lattices(24 ^ [])],extension(23,bind([[_89775], [24 ^ []]]))).
% 20.87/21.02 cnf('1.1.2.4.1',plain,[v3_struct_0(24 ^ []), -(25 ^ [])],extension(10)).
% 20.87/21.02 cnf('1.1.2.4.1.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.02 cnf('1.1.2.4.2',plain,[-(v10_lattices(24 ^ [])), -(25 ^ [])],extension(9)).
% 20.87/21.02 cnf('1.1.2.4.2.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.02 cnf('1.1.2.4.3',plain,[-(l3_lattices(24 ^ [])), -(25 ^ [])],extension(7)).
% 20.87/21.02 cnf('1.1.2.4.3.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.02 cnf('1.1.2.5',plain,[-(v6_lattices(k1_lattice2(24 ^ []))), -(v3_struct_0(24 ^ [])), v10_lattices(24 ^ []), l3_lattices(24 ^ [])],extension(24,bind([[_89775], [24 ^ []]]))).
% 20.87/21.02 cnf('1.1.2.5.1',plain,[v3_struct_0(24 ^ []), -(25 ^ [])],extension(10)).
% 20.87/21.02 cnf('1.1.2.5.1.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.02 cnf('1.1.2.5.2',plain,[-(v10_lattices(24 ^ [])), -(25 ^ [])],extension(9)).
% 20.87/21.02 cnf('1.1.2.5.2.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.02 cnf('1.1.2.5.3',plain,[-(l3_lattices(24 ^ [])), -(25 ^ [])],extension(7)).
% 20.87/21.02 cnf('1.1.2.5.3.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.02 cnf('1.1.2.6',plain,[-(v7_lattices(k1_lattice2(24 ^ []))), -(v3_struct_0(24 ^ [])), v10_lattices(24 ^ []), l3_lattices(24 ^ [])],extension(25,bind([[_89775], [24 ^ []]]))).
% 20.87/21.02 cnf('1.1.2.6.1',plain,[v3_struct_0(24 ^ []), -(25 ^ [])],extension(10)).
% 20.87/21.02 cnf('1.1.2.6.1.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.02 cnf('1.1.2.6.2',plain,[-(v10_lattices(24 ^ [])), -(25 ^ [])],extension(9)).
% 20.87/21.02 cnf('1.1.2.6.2.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.02 cnf('1.1.2.6.3',plain,[-(l3_lattices(24 ^ [])), -(25 ^ [])],extension(7)).
% 20.87/21.02 cnf('1.1.2.6.3.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.02 cnf('1.1.2.7',plain,[-(v8_lattices(k1_lattice2(24 ^ []))), -(v3_struct_0(24 ^ [])), v10_lattices(24 ^ []), l3_lattices(24 ^ [])],extension(26,bind([[_89775], [24 ^ []]]))).
% 20.87/21.02 cnf('1.1.2.7.1',plain,[v3_struct_0(24 ^ []), -(25 ^ [])],extension(10)).
% 20.87/21.02 cnf('1.1.2.7.1.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.02 cnf('1.1.2.7.2',plain,[-(v10_lattices(24 ^ [])), -(25 ^ [])],extension(9)).
% 20.87/21.02 cnf('1.1.2.7.2.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.02 cnf('1.1.2.7.3',plain,[-(l3_lattices(24 ^ [])), -(25 ^ [])],extension(7)).
% 20.87/21.02 cnf('1.1.2.7.3.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.02 cnf('1.1.2.8',plain,[-(v9_lattices(k1_lattice2(24 ^ []))), -(v3_struct_0(24 ^ [])), v10_lattices(24 ^ []), l3_lattices(24 ^ [])],extension(27,bind([[_89775], [24 ^ []]]))).
% 20.87/21.03 cnf('1.1.2.8.1',plain,[v3_struct_0(24 ^ []), -(25 ^ [])],extension(10)).
% 20.87/21.03 cnf('1.1.2.8.1.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.2.8.2',plain,[-(v10_lattices(24 ^ [])), -(25 ^ [])],extension(9)).
% 20.87/21.03 cnf('1.1.2.8.2.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.2.8.3',plain,[-(l3_lattices(24 ^ [])), -(25 ^ [])],extension(7)).
% 20.87/21.03 cnf('1.1.2.8.3.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3',plain,[-(v17_lattices(k1_lattice2(24 ^ []))), l3_lattices(k1_lattice2(24 ^ [])), -(v3_struct_0(k1_lattice2(24 ^ []))), v11_lattices(k1_lattice2(24 ^ [])), v15_lattices(k1_lattice2(24 ^ [])), v16_lattices(k1_lattice2(24 ^ []))],extension(19,bind([[_73850], [k1_lattice2(24 ^ [])]]))).
% 20.87/21.03 cnf('1.1.3.1',plain,[-(l3_lattices(k1_lattice2(24 ^ []))), l3_lattices(24 ^ [])],extension(20,bind([[_77480], [24 ^ []]]))).
% 20.87/21.03 cnf('1.1.3.1.1',plain,[-(l3_lattices(24 ^ [])), -(25 ^ [])],extension(7)).
% 20.87/21.03 cnf('1.1.3.1.1.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3.2',plain,[v3_struct_0(k1_lattice2(24 ^ []))],lemmata('1.1')).
% 20.87/21.03 cnf('1.1.3.3',plain,[-(v11_lattices(k1_lattice2(24 ^ []))), -(v3_struct_0(24 ^ [])), v10_lattices(24 ^ []), v11_lattices(24 ^ []), l3_lattices(24 ^ [])],extension(32,bind([[_103780], [24 ^ []]]))).
% 20.87/21.03 cnf('1.1.3.3.1',plain,[v3_struct_0(24 ^ []), -(25 ^ [])],extension(10)).
% 20.87/21.03 cnf('1.1.3.3.1.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3.3.2',plain,[-(v10_lattices(24 ^ [])), -(25 ^ [])],extension(9)).
% 20.87/21.03 cnf('1.1.3.3.2.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3.3.3',plain,[-(v11_lattices(24 ^ [])), l3_lattices(24 ^ []), -(v3_struct_0(24 ^ [])), v17_lattices(24 ^ [])],extension(16,bind([[_73198], [24 ^ []]]))).
% 20.87/21.03 cnf('1.1.3.3.3.1',plain,[-(l3_lattices(24 ^ [])), -(25 ^ [])],extension(7)).
% 20.87/21.03 cnf('1.1.3.3.3.1.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3.3.3.2',plain,[v3_struct_0(24 ^ [])],extension(11)).
% 20.87/21.03 cnf('1.1.3.3.3.3',plain,[-(v17_lattices(24 ^ [])), -(25 ^ [])],extension(8)).
% 20.87/21.03 cnf('1.1.3.3.3.3.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3.3.4',plain,[-(l3_lattices(24 ^ [])), -(25 ^ [])],extension(7)).
% 20.87/21.03 cnf('1.1.3.3.4.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3.4',plain,[-(v15_lattices(k1_lattice2(24 ^ []))), -(v3_struct_0(24 ^ [])), v10_lattices(24 ^ []), v15_lattices(24 ^ []), v16_lattices(24 ^ []), l3_lattices(24 ^ [])],extension(28,bind([[_102301], [24 ^ []]]))).
% 20.87/21.03 cnf('1.1.3.4.1',plain,[v3_struct_0(24 ^ []), -(25 ^ [])],extension(10)).
% 20.87/21.03 cnf('1.1.3.4.1.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3.4.2',plain,[-(v10_lattices(24 ^ [])), -(25 ^ [])],extension(9)).
% 20.87/21.03 cnf('1.1.3.4.2.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3.4.3',plain,[-(v15_lattices(24 ^ [])), l3_lattices(24 ^ []), -(v3_struct_0(24 ^ [])), v17_lattices(24 ^ [])],extension(17,bind([[_73198], [24 ^ []]]))).
% 20.87/21.03 cnf('1.1.3.4.3.1',plain,[-(l3_lattices(24 ^ [])), -(25 ^ [])],extension(7)).
% 20.87/21.03 cnf('1.1.3.4.3.1.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3.4.3.2',plain,[v3_struct_0(24 ^ [])],extension(11)).
% 20.87/21.03 cnf('1.1.3.4.3.3',plain,[-(v17_lattices(24 ^ [])), -(25 ^ [])],extension(8)).
% 20.87/21.03 cnf('1.1.3.4.3.3.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3.4.4',plain,[-(v16_lattices(24 ^ [])), l3_lattices(24 ^ []), -(v3_struct_0(24 ^ [])), v17_lattices(24 ^ [])],extension(18,bind([[_73198], [24 ^ []]]))).
% 20.87/21.03 cnf('1.1.3.4.4.1',plain,[-(l3_lattices(24 ^ [])), -(25 ^ [])],extension(7)).
% 20.87/21.03 cnf('1.1.3.4.4.1.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3.4.4.2',plain,[v3_struct_0(24 ^ [])],extension(11)).
% 20.87/21.03 cnf('1.1.3.4.4.3',plain,[-(v17_lattices(24 ^ [])), -(25 ^ [])],extension(8)).
% 20.87/21.03 cnf('1.1.3.4.4.3.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3.4.5',plain,[-(l3_lattices(24 ^ [])), -(25 ^ [])],extension(7)).
% 20.87/21.03 cnf('1.1.3.4.5.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3.5',plain,[-(v16_lattices(k1_lattice2(24 ^ []))), -(v3_struct_0(24 ^ [])), v10_lattices(24 ^ []), v15_lattices(24 ^ []), v16_lattices(24 ^ []), l3_lattices(24 ^ [])],extension(29,bind([[_102301], [24 ^ []]]))).
% 20.87/21.03 cnf('1.1.3.5.1',plain,[v3_struct_0(24 ^ []), -(25 ^ [])],extension(10)).
% 20.87/21.03 cnf('1.1.3.5.1.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3.5.2',plain,[-(v10_lattices(24 ^ [])), -(25 ^ [])],extension(9)).
% 20.87/21.03 cnf('1.1.3.5.2.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3.5.3',plain,[-(v15_lattices(24 ^ [])), l3_lattices(24 ^ []), -(v3_struct_0(24 ^ [])), v17_lattices(24 ^ [])],extension(17,bind([[_73198], [24 ^ []]]))).
% 20.87/21.03 cnf('1.1.3.5.3.1',plain,[-(l3_lattices(24 ^ [])), -(25 ^ [])],extension(7)).
% 20.87/21.03 cnf('1.1.3.5.3.1.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3.5.3.2',plain,[v3_struct_0(24 ^ [])],extension(11)).
% 20.87/21.03 cnf('1.1.3.5.3.3',plain,[-(v17_lattices(24 ^ [])), -(25 ^ [])],extension(8)).
% 20.87/21.03 cnf('1.1.3.5.3.3.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3.5.4',plain,[-(v16_lattices(24 ^ [])), l3_lattices(24 ^ []), -(v3_struct_0(24 ^ [])), v17_lattices(24 ^ [])],extension(18,bind([[_73198], [24 ^ []]]))).
% 20.87/21.03 cnf('1.1.3.5.4.1',plain,[-(l3_lattices(24 ^ [])), -(25 ^ [])],extension(7)).
% 20.87/21.03 cnf('1.1.3.5.4.1.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3.5.4.2',plain,[v3_struct_0(24 ^ [])],extension(11)).
% 20.87/21.03 cnf('1.1.3.5.4.3',plain,[-(v17_lattices(24 ^ [])), -(25 ^ [])],extension(8)).
% 20.87/21.03 cnf('1.1.3.5.4.3.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.3.5.5',plain,[-(l3_lattices(24 ^ [])), -(25 ^ [])],extension(7)).
% 20.87/21.03 cnf('1.1.3.5.5.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.1.4',plain,[-(l3_lattices(k1_lattice2(24 ^ []))), l3_lattices(24 ^ [])],extension(20,bind([[_77480], [24 ^ []]]))).
% 20.87/21.03 cnf('1.1.4.1',plain,[-(l3_lattices(24 ^ [])), -(25 ^ [])],extension(7)).
% 20.87/21.03 cnf('1.1.4.1.1',plain,[25 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2',plain,[-(26 ^ []), -(v3_struct_0(24 ^ [])), v10_lattices(24 ^ []), v17_lattices(24 ^ []), l3_lattices(24 ^ [])],extension(1)).
% 20.87/21.03 cnf('1.2.1',plain,[v3_struct_0(24 ^ [])],extension(11)).
% 20.87/21.03 cnf('1.2.2',plain,[-(v10_lattices(24 ^ []))],extension(12)).
% 20.87/21.03 cnf('1.2.3',plain,[-(v17_lattices(24 ^ [])), l3_lattices(24 ^ []), -(v3_struct_0(24 ^ [])), v11_lattices(24 ^ []), v15_lattices(24 ^ []), v16_lattices(24 ^ [])],extension(19,bind([[_73850], [24 ^ []]]))).
% 20.87/21.03 cnf('1.2.3.1',plain,[-(l3_lattices(24 ^ []))],extension(13)).
% 20.87/21.03 cnf('1.2.3.2',plain,[v3_struct_0(24 ^ [])],extension(11)).
% 20.87/21.03 cnf('1.2.3.3',plain,[-(v11_lattices(24 ^ [])), l3_lattices(24 ^ []), v10_lattices(24 ^ []), -(v3_struct_0(24 ^ [])), -(v3_struct_0(k1_lattice2(24 ^ []))), v10_lattices(k1_lattice2(24 ^ [])), v11_lattices(k1_lattice2(24 ^ [])), l3_lattices(k1_lattice2(24 ^ []))],extension(33,bind([[_103780], [24 ^ []]]))).
% 20.87/21.03 cnf('1.2.3.3.1',plain,[-(l3_lattices(24 ^ []))],extension(13)).
% 20.87/21.03 cnf('1.2.3.3.2',plain,[-(v10_lattices(24 ^ []))],extension(12)).
% 20.87/21.03 cnf('1.2.3.3.3',plain,[v3_struct_0(24 ^ [])],extension(11)).
% 20.87/21.03 cnf('1.2.3.3.4',plain,[v3_struct_0(k1_lattice2(24 ^ [])), -(26 ^ [])],extension(5)).
% 20.87/21.03 cnf('1.2.3.3.4.1',plain,[26 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2.3.3.5',plain,[-(v10_lattices(k1_lattice2(24 ^ []))), -(26 ^ [])],extension(4)).
% 20.87/21.03 cnf('1.2.3.3.5.1',plain,[26 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2.3.3.6',plain,[-(v11_lattices(k1_lattice2(24 ^ []))), l3_lattices(k1_lattice2(24 ^ [])), -(v3_struct_0(k1_lattice2(24 ^ []))), v17_lattices(k1_lattice2(24 ^ []))],extension(16,bind([[_73198], [k1_lattice2(24 ^ [])]]))).
% 20.87/21.03 cnf('1.2.3.3.6.1',plain,[-(l3_lattices(k1_lattice2(24 ^ []))), -(26 ^ [])],extension(2)).
% 20.87/21.03 cnf('1.2.3.3.6.1.1',plain,[26 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2.3.3.6.2',plain,[v3_struct_0(k1_lattice2(24 ^ []))],lemmata('1.2.3.3')).
% 20.87/21.03 cnf('1.2.3.3.6.3',plain,[-(v17_lattices(k1_lattice2(24 ^ []))), -(26 ^ [])],extension(3)).
% 20.87/21.03 cnf('1.2.3.3.6.3.1',plain,[26 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2.3.3.7',plain,[-(l3_lattices(k1_lattice2(24 ^ []))), -(26 ^ [])],extension(2)).
% 20.87/21.03 cnf('1.2.3.3.7.1',plain,[26 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2.3.4',plain,[-(v15_lattices(24 ^ [])), l3_lattices(24 ^ []), v10_lattices(24 ^ []), -(v3_struct_0(24 ^ [])), -(v3_struct_0(k1_lattice2(24 ^ []))), v10_lattices(k1_lattice2(24 ^ [])), v15_lattices(k1_lattice2(24 ^ [])), v16_lattices(k1_lattice2(24 ^ [])), l3_lattices(k1_lattice2(24 ^ []))],extension(30,bind([[_102301], [24 ^ []]]))).
% 20.87/21.03 cnf('1.2.3.4.1',plain,[-(l3_lattices(24 ^ []))],extension(13)).
% 20.87/21.03 cnf('1.2.3.4.2',plain,[-(v10_lattices(24 ^ []))],extension(12)).
% 20.87/21.03 cnf('1.2.3.4.3',plain,[v3_struct_0(24 ^ [])],extension(11)).
% 20.87/21.03 cnf('1.2.3.4.4',plain,[v3_struct_0(k1_lattice2(24 ^ [])), -(26 ^ [])],extension(5)).
% 20.87/21.03 cnf('1.2.3.4.4.1',plain,[26 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2.3.4.5',plain,[-(v10_lattices(k1_lattice2(24 ^ []))), -(26 ^ [])],extension(4)).
% 20.87/21.03 cnf('1.2.3.4.5.1',plain,[26 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2.3.4.6',plain,[-(v15_lattices(k1_lattice2(24 ^ []))), l3_lattices(k1_lattice2(24 ^ [])), -(v3_struct_0(k1_lattice2(24 ^ []))), v17_lattices(k1_lattice2(24 ^ []))],extension(17,bind([[_73198], [k1_lattice2(24 ^ [])]]))).
% 20.87/21.03 cnf('1.2.3.4.6.1',plain,[-(l3_lattices(k1_lattice2(24 ^ []))), -(26 ^ [])],extension(2)).
% 20.87/21.03 cnf('1.2.3.4.6.1.1',plain,[26 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2.3.4.6.2',plain,[v3_struct_0(k1_lattice2(24 ^ []))],lemmata('1.2.3.4')).
% 20.87/21.03 cnf('1.2.3.4.6.3',plain,[-(v17_lattices(k1_lattice2(24 ^ []))), -(26 ^ [])],extension(3)).
% 20.87/21.03 cnf('1.2.3.4.6.3.1',plain,[26 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2.3.4.7',plain,[-(v16_lattices(k1_lattice2(24 ^ []))), l3_lattices(k1_lattice2(24 ^ [])), -(v3_struct_0(k1_lattice2(24 ^ []))), v17_lattices(k1_lattice2(24 ^ []))],extension(18,bind([[_73198], [k1_lattice2(24 ^ [])]]))).
% 20.87/21.03 cnf('1.2.3.4.7.1',plain,[-(l3_lattices(k1_lattice2(24 ^ []))), -(26 ^ [])],extension(2)).
% 20.87/21.03 cnf('1.2.3.4.7.1.1',plain,[26 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2.3.4.7.2',plain,[v3_struct_0(k1_lattice2(24 ^ []))],lemmata('1.2.3.4')).
% 20.87/21.03 cnf('1.2.3.4.7.3',plain,[-(v17_lattices(k1_lattice2(24 ^ []))), -(26 ^ [])],extension(3)).
% 20.87/21.03 cnf('1.2.3.4.7.3.1',plain,[26 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2.3.4.8',plain,[-(l3_lattices(k1_lattice2(24 ^ []))), -(26 ^ [])],extension(2)).
% 20.87/21.03 cnf('1.2.3.4.8.1',plain,[26 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2.3.5',plain,[-(v16_lattices(24 ^ [])), l3_lattices(24 ^ []), v10_lattices(24 ^ []), -(v3_struct_0(24 ^ [])), -(v3_struct_0(k1_lattice2(24 ^ []))), v10_lattices(k1_lattice2(24 ^ [])), v15_lattices(k1_lattice2(24 ^ [])), v16_lattices(k1_lattice2(24 ^ [])), l3_lattices(k1_lattice2(24 ^ []))],extension(31,bind([[_102301], [24 ^ []]]))).
% 20.87/21.03 cnf('1.2.3.5.1',plain,[-(l3_lattices(24 ^ []))],extension(13)).
% 20.87/21.03 cnf('1.2.3.5.2',plain,[-(v10_lattices(24 ^ []))],extension(12)).
% 20.87/21.03 cnf('1.2.3.5.3',plain,[v3_struct_0(24 ^ [])],extension(11)).
% 20.87/21.03 cnf('1.2.3.5.4',plain,[v3_struct_0(k1_lattice2(24 ^ [])), -(26 ^ [])],extension(5)).
% 20.87/21.03 cnf('1.2.3.5.4.1',plain,[26 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2.3.5.5',plain,[-(v10_lattices(k1_lattice2(24 ^ []))), -(26 ^ [])],extension(4)).
% 20.87/21.03 cnf('1.2.3.5.5.1',plain,[26 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2.3.5.6',plain,[-(v15_lattices(k1_lattice2(24 ^ []))), l3_lattices(k1_lattice2(24 ^ [])), -(v3_struct_0(k1_lattice2(24 ^ []))), v17_lattices(k1_lattice2(24 ^ []))],extension(17,bind([[_73198], [k1_lattice2(24 ^ [])]]))).
% 20.87/21.03 cnf('1.2.3.5.6.1',plain,[-(l3_lattices(k1_lattice2(24 ^ []))), -(26 ^ [])],extension(2)).
% 20.87/21.03 cnf('1.2.3.5.6.1.1',plain,[26 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2.3.5.6.2',plain,[v3_struct_0(k1_lattice2(24 ^ []))],lemmata('1.2.3.5')).
% 20.87/21.03 cnf('1.2.3.5.6.3',plain,[-(v17_lattices(k1_lattice2(24 ^ []))), -(26 ^ [])],extension(3)).
% 20.87/21.03 cnf('1.2.3.5.6.3.1',plain,[26 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2.3.5.7',plain,[-(v16_lattices(k1_lattice2(24 ^ []))), l3_lattices(k1_lattice2(24 ^ [])), -(v3_struct_0(k1_lattice2(24 ^ []))), v17_lattices(k1_lattice2(24 ^ []))],extension(18,bind([[_73198], [k1_lattice2(24 ^ [])]]))).
% 20.87/21.03 cnf('1.2.3.5.7.1',plain,[-(l3_lattices(k1_lattice2(24 ^ []))), -(26 ^ [])],extension(2)).
% 20.87/21.03 cnf('1.2.3.5.7.1.1',plain,[26 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2.3.5.7.2',plain,[v3_struct_0(k1_lattice2(24 ^ []))],lemmata('1.2.3.5')).
% 20.87/21.03 cnf('1.2.3.5.7.3',plain,[-(v17_lattices(k1_lattice2(24 ^ []))), -(26 ^ [])],extension(3)).
% 20.87/21.03 cnf('1.2.3.5.7.3.1',plain,[26 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2.3.5.8',plain,[-(l3_lattices(k1_lattice2(24 ^ []))), -(26 ^ [])],extension(2)).
% 20.87/21.03 cnf('1.2.3.5.8.1',plain,[26 ^ []],reduction('1')).
% 20.87/21.03 cnf('1.2.4',plain,[-(l3_lattices(24 ^ []))],extension(13)).
% 20.87/21.03 %-----------------------------------------------------
% 20.87/21.03
% 20.87/21.03 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------