%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : KRS161+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n024.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 03:13:52 EDT 2022
% Result : Theorem 0.63s 1.40s
% Output : Proof 0.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS161+1 : TPTP v8.1.0. Released v3.1.0.
% 0.07/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n024.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Tue Jun 7 08:02:35 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.63/1.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.63/1.41 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.63/1.41
% 0.63/1.41 %-----------------------------------------------------
% 0.63/1.41 fof(the_axiom, conjecture, ! [_206225] : (cowlThing(_206225) & ~ cowlNothing(_206225)) & ! [_206225] : (xsd_string(_206225) <=> ~ xsd_integer(_206225)) & cC130(iV16439) & cC108(iV16439) & cC104(iV16439) & cC106(iV16439) & cC28(iV16439) & cowlThing(iV16439) & cC98(iV16440) & cC80(iV16440) & cC82(iV16440) & cowlThing(iV16440) & cC38(iV16448) & cowlThing(iV16448) & cC76(iV16453) & cC62(iV16453) & cowlThing(iV16453) & cC60(iV16453) & cC56(iV16455) & cC44(iV16455) & cC42(iV16455) & cowlThing(iV16455) & cC38(iV16457) & cowlThing(iV16457) & cC50(iV16459) & cC88(iV16459) & cC34(iV16459) & cC68(iV16459) & cowlThing(iV16459) & cC38(iV16460) & cowlThing(iV16460) & cC42(iV16461) & cC56(iV16461) & cC44(iV16461) & cowlThing(iV16461) & cC38(iV16462) & cowlThing(iV16462) & cC76(iV16463) & cC62(iV16463) & cowlThing(iV16463) & cC60(iV16463) & cC56(iV16464) & cC42(iV16464) & cC44(iV16464) & cowlThing(iV16464) & cC38(iV16465) & cowlThing(iV16465), file('/export/starexec/sandbox/benchmark/theBenchmark.p', the_axiom)).
% 0.63/1.41 fof(axiom_0, axiom, ! [_207420] : (cowlThing(_207420) & ~ cowlNothing(_207420)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 0.63/1.41 fof(axiom_1, axiom, ! [_207560] : (xsd_string(_207560) <=> ~ xsd_integer(_207560)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_1)).
% 0.63/1.41 fof(axiom_11, axiom, ! [_207721] : (cC106(_207721) <=> cC104(_207721) & cC100xcomp(_207721)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_11)).
% 0.63/1.41 fof(axiom_12, axiom, ! [_207876] : (cC108(_207876) <=> cC28(_207876) & cC106(_207876)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_12)).
% 0.63/1.41 fof(axiom_52, axiom, ! [_208129] : (cC34(_208129) <=> cC30xcomp(_208129) & cC32xcomp(_208129)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_52)).
% 0.63/1.41 fof(axiom_57, axiom, ! [_208282] : (cC38(_208282) <=> cTOP(_208282) & cC36xcomp(_208282)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_57)).
% 0.63/1.41 fof(axiom_65, axiom, ! [_208441] : (cC42(_208441) <=> ? [_208456] : (rR1(_208441, _208456) & cC8xcomp(_208456))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_65)).
% 0.63/1.41 fof(axiom_66, axiom, ! [_208622] : (cC44(_208622) <=> cC40xcomp(_208622) & cC42(_208622)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_66)).
% 0.63/1.41 fof(axiom_73, axiom, ! [_208780] : (cC50(_208780) <=> cC46xcomp(_208780) & cC48xcomp(_208780)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_73)).
% 0.63/1.41 fof(axiom_82, axiom, ! [_208942] : (cC56(_208942) <=> cC54xcomp(_208942) & cC44(_208942)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_82)).
% 0.63/1.41 fof(axiom_91, axiom, ! [_209104] : (cC60(_209104) <=> ? [_209119] : (rR1(_209104, _209119) & cC12xcomp(_209119))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_91)).
% 0.63/1.41 fof(axiom_92, axiom, ! [_209285] : (cC62(_209285) <=> cC60(_209285) & cC58xcomp(_209285)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_92)).
% 0.63/1.41 fof(axiom_100, axiom, ! [_209445] : (cC68(_209445) <=> cC64xcomp(_209445) & cC66xcomp(_209445)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_100)).
% 0.63/1.41 fof(axiom_112, axiom, ! [_209614] : (cC76(_209614) <=> cC74xcomp(_209614) & cC62(_209614)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_112)).
% 0.63/1.41 fof(axiom_119, axiom, ! [_209771] : (cC80(_209771) <=> ? [_209786] : (rR1(_209771, _209786) & cC16xcomp(_209786))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_119)).
% 0.63/1.41 fof(axiom_120, axiom, ! [_209952] : (cC82(_209952) <=> cC80(_209952) & cC78xcomp(_209952)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_120)).
% 0.63/1.41 fof(axiom_128, axiom, ! [_210112] : (cC88(_210112) <=> cC84xcomp(_210112) & cC86xcomp(_210112)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_128)).
% 0.63/1.41 fof(axiom_143, axiom, ! [_210288] : (cC98(_210288) <=> cC96xcomp(_210288) & cC82(_210288)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_143)).
% 0.63/1.41 fof(axiom_145, axiom, ! [_210432] : (cTEST(_210432) <=> cC108(_210432) & cC130(_210432)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_145)).
% 0.63/1.41 fof(axiom_148, axiom, cC100xcomp(iV16439), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_148)).
% 0.63/1.41 fof(axiom_149, axiom, cTEST(iV16439), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_149)).
% 0.63/1.41 fof(axiom_154, axiom, cC96xcomp(iV16440), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_154)).
% 0.63/1.41 fof(axiom_158, axiom, cC78xcomp(iV16440), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_158)).
% 0.63/1.41 fof(axiom_159, axiom, rR1(iV16440, iV16463), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_159)).
% 0.63/1.41 fof(axiom_163, axiom, cTOP(iV16448), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_163)).
% 0.63/1.41 fof(axiom_168, axiom, cC36xcomp(iV16448), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_168)).
% 0.63/1.41 fof(axiom_174, axiom, cC74xcomp(iV16453), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_174)).
% 0.63/1.41 fof(axiom_181, axiom, cC58xcomp(iV16453), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_181)).
% 0.63/1.41 fof(axiom_182, axiom, rR1(iV16453, iV16461), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_182)).
% 0.63/1.41 fof(axiom_185, axiom, cC40xcomp(iV16455), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_185)).
% 0.63/1.41 fof(axiom_190, axiom, cC54xcomp(iV16455), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_190)).
% 0.63/1.41 fof(axiom_193, axiom, rR1(iV16455, iV16460), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_193)).
% 0.63/1.41 fof(axiom_197, axiom, cTOP(iV16457), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_197)).
% 0.63/1.41 fof(axiom_201, axiom, cC36xcomp(iV16457), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_201)).
% 0.63/1.41 fof(axiom_209, axiom, cC30xcomp(iV16459), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_209)).
% 0.63/1.41 fof(axiom_210, axiom, cC84xcomp(iV16459), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_210)).
% 0.63/1.41 fof(axiom_212, axiom, cC46xcomp(iV16459), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_212)).
% 0.63/1.41 fof(axiom_213, axiom, cC64xcomp(iV16459), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_213)).
% 0.63/1.41 fof(axiom_215, axiom, cC86xcomp(iV16459), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_215)).
% 0.63/1.41 fof(axiom_216, axiom, cC32xcomp(iV16459), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_216)).
% 0.63/1.41 fof(axiom_217, axiom, cC48xcomp(iV16459), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_217)).
% 0.63/1.41 fof(axiom_221, axiom, cC66xcomp(iV16459), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_221)).
% 0.63/1.41 fof(axiom_225, axiom, cTOP(iV16460), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_225)).
% 0.63/1.41 fof(axiom_227, axiom, cC8xcomp(iV16460), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_227)).
% 0.63/1.41 fof(axiom_228, axiom, cC36xcomp(iV16460), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_228)).
% 0.63/1.41 fof(axiom_234, axiom, cC40xcomp(iV16461), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_234)).
% 0.63/1.41 fof(axiom_237, axiom, cC12xcomp(iV16461), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_237)).
% 0.63/1.41 fof(axiom_240, axiom, cC54xcomp(iV16461), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_240)).
% 0.63/1.41 fof(axiom_243, axiom, rR1(iV16461, iV16462), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_243)).
% 0.63/1.41 fof(axiom_247, axiom, cTOP(iV16462), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_247)).
% 0.63/1.41 fof(axiom_249, axiom, cC8xcomp(iV16462), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_249)).
% 0.63/1.41 fof(axiom_252, axiom, cC36xcomp(iV16462), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_252)).
% 0.63/1.41 fof(axiom_255, axiom, cC74xcomp(iV16463), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_255)).
% 0.63/1.41 fof(axiom_257, axiom, cC16xcomp(iV16463), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_257)).
% 0.63/1.41 fof(axiom_262, axiom, cC58xcomp(iV16463), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_262)).
% 0.63/1.41 fof(axiom_263, axiom, rR1(iV16463, iV16464), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_263)).
% 0.63/1.41 fof(axiom_266, axiom, cC40xcomp(iV16464), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_266)).
% 0.63/1.41 fof(axiom_267, axiom, cC12xcomp(iV16464), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_267)).
% 0.63/1.41 fof(axiom_270, axiom, cC54xcomp(iV16464), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_270)).
% 0.63/1.41 fof(axiom_274, axiom, rR1(iV16464, iV16465), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_274)).
% 0.63/1.41 fof(axiom_277, axiom, cTOP(iV16465), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_277)).
% 0.63/1.41 fof(axiom_280, axiom, cC8xcomp(iV16465), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_280)).
% 0.63/1.41 fof(axiom_282, axiom, cC36xcomp(iV16465), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_282)).
% 0.63/1.41
% 0.63/1.41 cnf(1, plain, [-(118 ^ []), xsd_string(116 ^ [])], clausify(the_axiom)).
% 0.63/1.41 cnf(2, plain, [-(118 ^ []), xsd_integer(116 ^ [])], clausify(the_axiom)).
% 0.63/1.41 cnf(3, plain, [-(117 ^ []), -(xsd_integer(116 ^ []))], clausify(the_axiom)).
% 0.63/1.41 cnf(4, plain, [-(117 ^ []), -(xsd_string(116 ^ []))], clausify(the_axiom)).
% 0.63/1.41 cnf(5, plain, [-(cowlNothing(115 ^ [])), cowlThing(115 ^ []), 118 ^ [], 117 ^ [], cC130(iV16439), cC108(iV16439), cC104(iV16439), cC106(iV16439), cC28(iV16439), cowlThing(iV16439), cC98(iV16440), cC80(iV16440), cC82(iV16440), cowlThing(iV16440), cC38(iV16448), cowlThing(iV16448), cC76(iV16453), cC62(iV16453), cowlThing(iV16453), cC60(iV16453), cC56(iV16455), cC44(iV16455), cC42(iV16455), cowlThing(iV16455), cC38(iV16457), cowlThing(iV16457), cC50(iV16459), cC88(iV16459), cC34(iV16459), cC68(iV16459), cowlThing(iV16459), cC38(iV16460), cowlThing(iV16460), cC42(iV16461), cC56(iV16461), cC44(iV16461), cowlThing(iV16461), cC38(iV16462), cowlThing(iV16462), cC76(iV16463), cC62(iV16463), cowlThing(iV16463), cC60(iV16463), cC56(iV16464), cC42(iV16464), cC44(iV16464), cowlThing(iV16464), cC38(iV16465), cowlThing(iV16465)], clausify(the_axiom)).
% 0.63/1.41 cnf(6, plain, [-(cowlThing(_43084))], clausify(axiom_0)).
% 0.63/1.41 cnf(7, plain, [cowlNothing(_43084)], clausify(axiom_0)).
% 0.63/1.41 cnf(8, plain, [xsd_string(_43312), xsd_integer(_43312)], clausify(axiom_1)).
% 0.63/1.41 cnf(9, plain, [-(xsd_string(_43312)), -(xsd_integer(_43312))], clausify(axiom_1)).
% 0.63/1.41 cnf(10, plain, [cC106(_46252), -(cC104(_46252))], clausify(axiom_11)).
% 0.63/1.41 cnf(11, plain, [-(cC106(_46252)), cC104(_46252), cC100xcomp(_46252)], clausify(axiom_11)).
% 0.63/1.41 cnf(12, plain, [cC108(_46520), -(cC28(_46520))], clausify(axiom_12)).
% 0.63/1.41 cnf(13, plain, [cC108(_46520), -(cC106(_46520))], clausify(axiom_12)).
% 0.63/1.41 cnf(14, plain, [-(cC34(_58515)), cC30xcomp(_58515), cC32xcomp(_58515)], clausify(axiom_52)).
% 0.63/1.41 cnf(15, plain, [-(cC38(_60014)), cTOP(_60014), cC36xcomp(_60014)], clausify(axiom_57)).
% 0.63/1.41 cnf(16, plain, [-(cC42(_62380)), rR1(_62380, _62468), cC8xcomp(_62468)], clausify(axiom_65)).
% 0.63/1.41 cnf(17, plain, [-(cC44(_62726)), cC40xcomp(_62726), cC42(_62726)], clausify(axiom_66)).
% 0.63/1.41 cnf(18, plain, [-(cC50(_64698)), cC46xcomp(_64698), cC48xcomp(_64698)], clausify(axiom_73)).
% 0.63/1.41 cnf(19, plain, [-(cC56(_67410)), cC54xcomp(_67410), cC44(_67410)], clausify(axiom_82)).
% 0.63/1.41 cnf(20, plain, [-(cC60(_70044)), rR1(_70044, _70132), cC12xcomp(_70132)], clausify(axiom_91)).
% 0.63/1.41 cnf(21, plain, [-(cC62(_70390)), cC60(_70390), cC58xcomp(_70390)], clausify(axiom_92)).
% 0.63/1.41 cnf(22, plain, [-(cC68(_72645)), cC64xcomp(_72645), cC66xcomp(_72645)], clausify(axiom_100)).
% 0.63/1.41 cnf(23, plain, [-(cC76(_76287)), cC74xcomp(_76287), cC62(_76287)], clausify(axiom_112)).
% 0.63/1.41 cnf(24, plain, [-(cC80(_78370)), rR1(_78370, _78458), cC16xcomp(_78458)], clausify(axiom_119)).
% 0.63/1.41 cnf(25, plain, [-(cC82(_78716)), cC80(_78716), cC78xcomp(_78716)], clausify(axiom_120)).
% 0.63/1.41 cnf(26, plain, [-(cC88(_80971)), cC84xcomp(_80971), cC86xcomp(_80971)], clausify(axiom_128)).
% 0.63/1.41 cnf(27, plain, [-(cC98(_85543)), cC96xcomp(_85543), cC82(_85543)], clausify(axiom_143)).
% 0.63/1.41 cnf(28, plain, [cTEST(_86112), -(cC108(_86112))], clausify(axiom_145)).
% 0.63/1.41 cnf(29, plain, [cTEST(_86112), -(cC130(_86112))], clausify(axiom_145)).
% 0.63/1.41 cnf(30, plain, [-(cC100xcomp(iV16439))], clausify(axiom_148)).
% 0.63/1.41 cnf(31, plain, [-(cTEST(iV16439))], clausify(axiom_149)).
% 0.63/1.41 cnf(32, plain, [-(cC96xcomp(iV16440))], clausify(axiom_154)).
% 0.63/1.41 cnf(33, plain, [-(cC78xcomp(iV16440))], clausify(axiom_158)).
% 0.63/1.41 cnf(34, plain, [-(rR1(iV16440, iV16463))], clausify(axiom_159)).
% 0.63/1.41 cnf(35, plain, [-(cTOP(iV16448))], clausify(axiom_163)).
% 0.63/1.41 cnf(36, plain, [-(cC36xcomp(iV16448))], clausify(axiom_168)).
% 0.63/1.41 cnf(37, plain, [-(cC74xcomp(iV16453))], clausify(axiom_174)).
% 0.63/1.41 cnf(38, plain, [-(cC58xcomp(iV16453))], clausify(axiom_181)).
% 0.63/1.41 cnf(39, plain, [-(rR1(iV16453, iV16461))], clausify(axiom_182)).
% 0.63/1.41 cnf(40, plain, [-(cC40xcomp(iV16455))], clausify(axiom_185)).
% 0.63/1.41 cnf(41, plain, [-(cC54xcomp(iV16455))], clausify(axiom_190)).
% 0.63/1.41 cnf(42, plain, [-(rR1(iV16455, iV16460))], clausify(axiom_193)).
% 0.63/1.41 cnf(43, plain, [-(cTOP(iV16457))], clausify(axiom_197)).
% 0.63/1.41 cnf(44, plain, [-(cC36xcomp(iV16457))], clausify(axiom_201)).
% 0.63/1.41 cnf(45, plain, [-(cC30xcomp(iV16459))], clausify(axiom_209)).
% 0.63/1.41 cnf(46, plain, [-(cC84xcomp(iV16459))], clausify(axiom_210)).
% 0.63/1.41 cnf(47, plain, [-(cC46xcomp(iV16459))], clausify(axiom_212)).
% 0.63/1.41 cnf(48, plain, [-(cC64xcomp(iV16459))], clausify(axiom_213)).
% 0.63/1.41 cnf(49, plain, [-(cC86xcomp(iV16459))], clausify(axiom_215)).
% 0.63/1.41 cnf(50, plain, [-(cC32xcomp(iV16459))], clausify(axiom_216)).
% 0.63/1.41 cnf(51, plain, [-(cC48xcomp(iV16459))], clausify(axiom_217)).
% 0.63/1.41 cnf(52, plain, [-(cC66xcomp(iV16459))], clausify(axiom_221)).
% 0.63/1.41 cnf(53, plain, [-(cTOP(iV16460))], clausify(axiom_225)).
% 0.63/1.41 cnf(54, plain, [-(cC8xcomp(iV16460))], clausify(axiom_227)).
% 0.63/1.41 cnf(55, plain, [-(cC36xcomp(iV16460))], clausify(axiom_228)).
% 0.63/1.41 cnf(56, plain, [-(cC40xcomp(iV16461))], clausify(axiom_234)).
% 0.63/1.41 cnf(57, plain, [-(cC12xcomp(iV16461))], clausify(axiom_237)).
% 0.63/1.41 cnf(58, plain, [-(cC54xcomp(iV16461))], clausify(axiom_240)).
% 0.63/1.41 cnf(59, plain, [-(rR1(iV16461, iV16462))], clausify(axiom_243)).
% 0.63/1.41 cnf(60, plain, [-(cTOP(iV16462))], clausify(axiom_247)).
% 0.63/1.41 cnf(61, plain, [-(cC8xcomp(iV16462))], clausify(axiom_249)).
% 0.63/1.41 cnf(62, plain, [-(cC36xcomp(iV16462))], clausify(axiom_252)).
% 0.63/1.41 cnf(63, plain, [-(cC74xcomp(iV16463))], clausify(axiom_255)).
% 0.63/1.41 cnf(64, plain, [-(cC16xcomp(iV16463))], clausify(axiom_257)).
% 0.63/1.41 cnf(65, plain, [-(cC58xcomp(iV16463))], clausify(axiom_262)).
% 0.63/1.41 cnf(66, plain, [-(rR1(iV16463, iV16464))], clausify(axiom_263)).
% 0.63/1.41 cnf(67, plain, [-(cC40xcomp(iV16464))], clausify(axiom_266)).
% 0.63/1.41 cnf(68, plain, [-(cC12xcomp(iV16464))], clausify(axiom_267)).
% 0.63/1.41 cnf(69, plain, [-(cC54xcomp(iV16464))], clausify(axiom_270)).
% 0.63/1.41 cnf(70, plain, [-(rR1(iV16464, iV16465))], clausify(axiom_274)).
% 0.63/1.41 cnf(71, plain, [-(cTOP(iV16465))], clausify(axiom_277)).
% 0.63/1.41 cnf(72, plain, [-(cC8xcomp(iV16465))], clausify(axiom_280)).
% 0.63/1.41 cnf(73, plain, [-(cC36xcomp(iV16465))], clausify(axiom_282)).
% 0.63/1.41
% 0.63/1.41 cnf('1',plain,[cowlNothing(115 ^ [])],start(7,bind([[_43084], [115 ^ []]]))).
% 0.63/1.41 cnf('1.1',plain,[-(cowlNothing(115 ^ [])), cowlThing(115 ^ []), 118 ^ [], 117 ^ [], cC130(iV16439), cC108(iV16439), cC104(iV16439), cC106(iV16439), cC28(iV16439), cowlThing(iV16439), cC98(iV16440), cC80(iV16440), cC82(iV16440), cowlThing(iV16440), cC38(iV16448), cowlThing(iV16448), cC76(iV16453), cC62(iV16453), cowlThing(iV16453), cC60(iV16453), cC56(iV16455), cC44(iV16455), cC42(iV16455), cowlThing(iV16455), cC38(iV16457), cowlThing(iV16457), cC50(iV16459), cC88(iV16459), cC34(iV16459), cC68(iV16459), cowlThing(iV16459), cC38(iV16460), cowlThing(iV16460), cC42(iV16461), cC56(iV16461), cC44(iV16461), cowlThing(iV16461), cC38(iV16462), cowlThing(iV16462), cC76(iV16463), cC62(iV16463), cowlThing(iV16463), cC60(iV16463), cC56(iV16464), cC42(iV16464), cC44(iV16464), cowlThing(iV16464), cC38(iV16465), cowlThing(iV16465)],extension(5)).
% 0.63/1.41 cnf('1.1.1',plain,[-(cowlThing(115 ^ []))],extension(6,bind([[_43084], [115 ^ []]]))).
% 0.63/1.41 cnf('1.1.2',plain,[-(118 ^ []), xsd_string(116 ^ [])],extension(1)).
% 0.63/1.41 cnf('1.1.2.1',plain,[-(xsd_string(116 ^ [])), -(xsd_integer(116 ^ []))],extension(9,bind([[_43312], [116 ^ []]]))).
% 0.63/1.41 cnf('1.1.2.1.1',plain,[xsd_integer(116 ^ []), -(118 ^ [])],extension(2)).
% 0.63/1.41 cnf('1.1.2.1.1.1',plain,[118 ^ []],reduction('1.1')).
% 0.63/1.41 cnf('1.1.3',plain,[-(117 ^ []), -(xsd_integer(116 ^ []))],extension(3)).
% 0.63/1.41 cnf('1.1.3.1',plain,[xsd_integer(116 ^ []), xsd_string(116 ^ [])],extension(8,bind([[_43312], [116 ^ []]]))).
% 0.63/1.41 cnf('1.1.3.1.1',plain,[-(xsd_string(116 ^ [])), -(117 ^ [])],extension(4)).
% 0.63/1.41 cnf('1.1.3.1.1.1',plain,[117 ^ []],reduction('1.1')).
% 0.63/1.41 cnf('1.1.4',plain,[-(cC130(iV16439)), cTEST(iV16439)],extension(29,bind([[_86112], [iV16439]]))).
% 0.63/1.41 cnf('1.1.4.1',plain,[-(cTEST(iV16439))],extension(31)).
% 0.63/1.41 cnf('1.1.5',plain,[-(cC108(iV16439)), cTEST(iV16439)],extension(28,bind([[_86112], [iV16439]]))).
% 0.63/1.41 cnf('1.1.5.1',plain,[-(cTEST(iV16439))],extension(31)).
% 0.63/1.41 cnf('1.1.6',plain,[-(cC104(iV16439)), cC106(iV16439)],extension(10,bind([[_46252], [iV16439]]))).
% 0.63/1.41 cnf('1.1.6.1',plain,[-(cC106(iV16439)), cC108(iV16439)],extension(13,bind([[_46520], [iV16439]]))).
% 0.63/1.41 cnf('1.1.6.1.1',plain,[-(cC108(iV16439))],lemmata('1.1')).
% 0.63/1.41 cnf('1.1.7',plain,[-(cC106(iV16439)), cC104(iV16439), cC100xcomp(iV16439)],extension(11,bind([[_46252], [iV16439]]))).
% 0.63/1.41 cnf('1.1.7.1',plain,[-(cC104(iV16439))],lemmata('1.1')).
% 0.63/1.41 cnf('1.1.7.2',plain,[-(cC100xcomp(iV16439))],extension(30)).
% 0.63/1.41 cnf('1.1.8',plain,[-(cC28(iV16439)), cC108(iV16439)],extension(12,bind([[_46520], [iV16439]]))).
% 0.63/1.41 cnf('1.1.8.1',plain,[-(cC108(iV16439))],lemmata('1.1')).
% 0.63/1.41 cnf('1.1.9',plain,[-(cowlThing(iV16439))],extension(6,bind([[_43084], [iV16439]]))).
% 0.63/1.41 cnf('1.1.10',plain,[-(cC98(iV16440)), cC96xcomp(iV16440), cC82(iV16440)],extension(27,bind([[_85543], [iV16440]]))).
% 0.63/1.41 cnf('1.1.10.1',plain,[-(cC96xcomp(iV16440))],extension(32)).
% 0.63/1.41 cnf('1.1.10.2',plain,[-(cC82(iV16440)), cC80(iV16440), cC78xcomp(iV16440)],extension(25,bind([[_78716], [iV16440]]))).
% 0.63/1.41 cnf('1.1.10.2.1',plain,[-(cC80(iV16440)), rR1(iV16440, iV16463), cC16xcomp(iV16463)],extension(24,bind([[_78370, _78458], [iV16440, iV16463]]))).
% 0.63/1.41 cnf('1.1.10.2.1.1',plain,[-(rR1(iV16440, iV16463))],extension(34)).
% 0.63/1.41 cnf('1.1.10.2.1.2',plain,[-(cC16xcomp(iV16463))],extension(64)).
% 0.63/1.41 cnf('1.1.10.2.2',plain,[-(cC78xcomp(iV16440))],extension(33)).
% 0.63/1.41 cnf('1.1.11',plain,[-(cC80(iV16440)), rR1(iV16440, iV16463), cC16xcomp(iV16463)],extension(24,bind([[_78370, _78458], [iV16440, iV16463]]))).
% 0.63/1.41 cnf('1.1.11.1',plain,[-(rR1(iV16440, iV16463))],extension(34)).
% 0.63/1.41 cnf('1.1.11.2',plain,[-(cC16xcomp(iV16463))],extension(64)).
% 0.63/1.41 cnf('1.1.12',plain,[-(cC82(iV16440)), cC80(iV16440), cC78xcomp(iV16440)],extension(25,bind([[_78716], [iV16440]]))).
% 0.63/1.41 cnf('1.1.12.1',plain,[-(cC80(iV16440))],lemmata('1.1')).
% 0.63/1.41 cnf('1.1.12.2',plain,[-(cC78xcomp(iV16440))],extension(33)).
% 0.63/1.41 cnf('1.1.13',plain,[-(cowlThing(iV16440))],extension(6,bind([[_43084], [iV16440]]))).
% 0.63/1.41 cnf('1.1.14',plain,[-(cC38(iV16448)), cTOP(iV16448), cC36xcomp(iV16448)],extension(15,bind([[_60014], [iV16448]]))).
% 0.63/1.41 cnf('1.1.14.1',plain,[-(cTOP(iV16448))],extension(35)).
% 0.63/1.41 cnf('1.1.14.2',plain,[-(cC36xcomp(iV16448))],extension(36)).
% 0.63/1.41 cnf('1.1.15',plain,[-(cowlThing(iV16448))],extension(6,bind([[_43084], [iV16448]]))).
% 0.63/1.41 cnf('1.1.16',plain,[-(cC76(iV16453)), cC74xcomp(iV16453), cC62(iV16453)],extension(23,bind([[_76287], [iV16453]]))).
% 0.63/1.41 cnf('1.1.16.1',plain,[-(cC74xcomp(iV16453))],extension(37)).
% 0.63/1.41 cnf('1.1.16.2',plain,[-(cC62(iV16453)), cC60(iV16453), cC58xcomp(iV16453)],extension(21,bind([[_70390], [iV16453]]))).
% 0.63/1.41 cnf('1.1.16.2.1',plain,[-(cC60(iV16453)), rR1(iV16453, iV16461), cC12xcomp(iV16461)],extension(20,bind([[_70044, _70132], [iV16453, iV16461]]))).
% 0.63/1.41 cnf('1.1.16.2.1.1',plain,[-(rR1(iV16453, iV16461))],extension(39)).
% 0.63/1.41 cnf('1.1.16.2.1.2',plain,[-(cC12xcomp(iV16461))],extension(57)).
% 0.63/1.41 cnf('1.1.16.2.2',plain,[-(cC58xcomp(iV16453))],extension(38)).
% 0.63/1.41 cnf('1.1.17',plain,[-(cC62(iV16453)), cC60(iV16453), cC58xcomp(iV16453)],extension(21,bind([[_70390], [iV16453]]))).
% 0.63/1.41 cnf('1.1.17.1',plain,[-(cC60(iV16453)), rR1(iV16453, iV16461), cC12xcomp(iV16461)],extension(20,bind([[_70044, _70132], [iV16453, iV16461]]))).
% 0.63/1.41 cnf('1.1.17.1.1',plain,[-(rR1(iV16453, iV16461))],extension(39)).
% 0.63/1.41 cnf('1.1.17.1.2',plain,[-(cC12xcomp(iV16461))],extension(57)).
% 0.63/1.41 cnf('1.1.17.2',plain,[-(cC58xcomp(iV16453))],extension(38)).
% 0.63/1.41 cnf('1.1.18',plain,[-(cowlThing(iV16453))],extension(6,bind([[_43084], [iV16453]]))).
% 0.63/1.41 cnf('1.1.19',plain,[-(cC60(iV16453)), rR1(iV16453, iV16461), cC12xcomp(iV16461)],extension(20,bind([[_70044, _70132], [iV16453, iV16461]]))).
% 0.63/1.41 cnf('1.1.19.1',plain,[-(rR1(iV16453, iV16461))],extension(39)).
% 0.63/1.41 cnf('1.1.19.2',plain,[-(cC12xcomp(iV16461))],extension(57)).
% 0.63/1.41 cnf('1.1.20',plain,[-(cC56(iV16455)), cC54xcomp(iV16455), cC44(iV16455)],extension(19,bind([[_67410], [iV16455]]))).
% 0.63/1.41 cnf('1.1.20.1',plain,[-(cC54xcomp(iV16455))],extension(41)).
% 0.63/1.41 cnf('1.1.20.2',plain,[-(cC44(iV16455)), cC40xcomp(iV16455), cC42(iV16455)],extension(17,bind([[_62726], [iV16455]]))).
% 0.63/1.41 cnf('1.1.20.2.1',plain,[-(cC40xcomp(iV16455))],extension(40)).
% 0.63/1.41 cnf('1.1.20.2.2',plain,[-(cC42(iV16455)), rR1(iV16455, iV16460), cC8xcomp(iV16460)],extension(16,bind([[_62380, _62468], [iV16455, iV16460]]))).
% 0.63/1.41 cnf('1.1.20.2.2.1',plain,[-(rR1(iV16455, iV16460))],extension(42)).
% 0.63/1.41 cnf('1.1.20.2.2.2',plain,[-(cC8xcomp(iV16460))],extension(54)).
% 0.63/1.41 cnf('1.1.21',plain,[-(cC44(iV16455)), cC40xcomp(iV16455), cC42(iV16455)],extension(17,bind([[_62726], [iV16455]]))).
% 0.63/1.41 cnf('1.1.21.1',plain,[-(cC40xcomp(iV16455))],extension(40)).
% 0.63/1.41 cnf('1.1.21.2',plain,[-(cC42(iV16455)), rR1(iV16455, iV16460), cC8xcomp(iV16460)],extension(16,bind([[_62380, _62468], [iV16455, iV16460]]))).
% 0.63/1.41 cnf('1.1.21.2.1',plain,[-(rR1(iV16455, iV16460))],extension(42)).
% 0.63/1.41 cnf('1.1.21.2.2',plain,[-(cC8xcomp(iV16460))],extension(54)).
% 0.63/1.41 cnf('1.1.22',plain,[-(cC42(iV16455)), rR1(iV16455, iV16460), cC8xcomp(iV16460)],extension(16,bind([[_62380, _62468], [iV16455, iV16460]]))).
% 0.63/1.41 cnf('1.1.22.1',plain,[-(rR1(iV16455, iV16460))],extension(42)).
% 0.63/1.41 cnf('1.1.22.2',plain,[-(cC8xcomp(iV16460))],extension(54)).
% 0.63/1.41 cnf('1.1.23',plain,[-(cowlThing(iV16455))],extension(6,bind([[_43084], [iV16455]]))).
% 0.63/1.41 cnf('1.1.24',plain,[-(cC38(iV16457)), cTOP(iV16457), cC36xcomp(iV16457)],extension(15,bind([[_60014], [iV16457]]))).
% 0.63/1.41 cnf('1.1.24.1',plain,[-(cTOP(iV16457))],extension(43)).
% 0.63/1.41 cnf('1.1.24.2',plain,[-(cC36xcomp(iV16457))],extension(44)).
% 0.63/1.41 cnf('1.1.25',plain,[-(cowlThing(iV16457))],extension(6,bind([[_43084], [iV16457]]))).
% 0.63/1.41 cnf('1.1.26',plain,[-(cC50(iV16459)), cC46xcomp(iV16459), cC48xcomp(iV16459)],extension(18,bind([[_64698], [iV16459]]))).
% 0.63/1.41 cnf('1.1.26.1',plain,[-(cC46xcomp(iV16459))],extension(47)).
% 0.63/1.41 cnf('1.1.26.2',plain,[-(cC48xcomp(iV16459))],extension(51)).
% 0.63/1.41 cnf('1.1.27',plain,[-(cC88(iV16459)), cC84xcomp(iV16459), cC86xcomp(iV16459)],extension(26,bind([[_80971], [iV16459]]))).
% 0.63/1.41 cnf('1.1.27.1',plain,[-(cC84xcomp(iV16459))],extension(46)).
% 0.63/1.41 cnf('1.1.27.2',plain,[-(cC86xcomp(iV16459))],extension(49)).
% 0.63/1.41 cnf('1.1.28',plain,[-(cC34(iV16459)), cC30xcomp(iV16459), cC32xcomp(iV16459)],extension(14,bind([[_58515], [iV16459]]))).
% 0.63/1.41 cnf('1.1.28.1',plain,[-(cC30xcomp(iV16459))],extension(45)).
% 0.63/1.41 cnf('1.1.28.2',plain,[-(cC32xcomp(iV16459))],extension(50)).
% 0.63/1.41 cnf('1.1.29',plain,[-(cC68(iV16459)), cC64xcomp(iV16459), cC66xcomp(iV16459)],extension(22,bind([[_72645], [iV16459]]))).
% 0.63/1.41 cnf('1.1.29.1',plain,[-(cC64xcomp(iV16459))],extension(48)).
% 0.63/1.41 cnf('1.1.29.2',plain,[-(cC66xcomp(iV16459))],extension(52)).
% 0.63/1.41 cnf('1.1.30',plain,[-(cowlThing(iV16459))],extension(6,bind([[_43084], [iV16459]]))).
% 0.63/1.41 cnf('1.1.31',plain,[-(cC38(iV16460)), cTOP(iV16460), cC36xcomp(iV16460)],extension(15,bind([[_60014], [iV16460]]))).
% 0.63/1.41 cnf('1.1.31.1',plain,[-(cTOP(iV16460))],extension(53)).
% 0.63/1.41 cnf('1.1.31.2',plain,[-(cC36xcomp(iV16460))],extension(55)).
% 0.63/1.41 cnf('1.1.32',plain,[-(cowlThing(iV16460))],extension(6,bind([[_43084], [iV16460]]))).
% 0.63/1.41 cnf('1.1.33',plain,[-(cC42(iV16461)), rR1(iV16461, iV16462), cC8xcomp(iV16462)],extension(16,bind([[_62380, _62468], [iV16461, iV16462]]))).
% 0.63/1.41 cnf('1.1.33.1',plain,[-(rR1(iV16461, iV16462))],extension(59)).
% 0.63/1.41 cnf('1.1.33.2',plain,[-(cC8xcomp(iV16462))],extension(61)).
% 0.63/1.41 cnf('1.1.34',plain,[-(cC56(iV16461)), cC54xcomp(iV16461), cC44(iV16461)],extension(19,bind([[_67410], [iV16461]]))).
% 0.63/1.41 cnf('1.1.34.1',plain,[-(cC54xcomp(iV16461))],extension(58)).
% 0.63/1.41 cnf('1.1.34.2',plain,[-(cC44(iV16461)), cC40xcomp(iV16461), cC42(iV16461)],extension(17,bind([[_62726], [iV16461]]))).
% 0.63/1.41 cnf('1.1.34.2.1',plain,[-(cC40xcomp(iV16461))],extension(56)).
% 0.63/1.41 cnf('1.1.34.2.2',plain,[-(cC42(iV16461))],lemmata('1.1')).
% 0.63/1.41 cnf('1.1.35',plain,[-(cC44(iV16461)), cC40xcomp(iV16461), cC42(iV16461)],extension(17,bind([[_62726], [iV16461]]))).
% 0.63/1.41 cnf('1.1.35.1',plain,[-(cC40xcomp(iV16461))],extension(56)).
% 0.63/1.41 cnf('1.1.35.2',plain,[-(cC42(iV16461))],lemmata('1.1')).
% 0.63/1.41 cnf('1.1.36',plain,[-(cowlThing(iV16461))],extension(6,bind([[_43084], [iV16461]]))).
% 0.63/1.41 cnf('1.1.37',plain,[-(cC38(iV16462)), cTOP(iV16462), cC36xcomp(iV16462)],extension(15,bind([[_60014], [iV16462]]))).
% 0.63/1.41 cnf('1.1.37.1',plain,[-(cTOP(iV16462))],extension(60)).
% 0.63/1.41 cnf('1.1.37.2',plain,[-(cC36xcomp(iV16462))],extension(62)).
% 0.63/1.41 cnf('1.1.38',plain,[-(cowlThing(iV16462))],extension(6,bind([[_43084], [iV16462]]))).
% 0.63/1.41 cnf('1.1.39',plain,[-(cC76(iV16463)), cC74xcomp(iV16463), cC62(iV16463)],extension(23,bind([[_76287], [iV16463]]))).
% 0.63/1.41 cnf('1.1.39.1',plain,[-(cC74xcomp(iV16463))],extension(63)).
% 0.63/1.41 cnf('1.1.39.2',plain,[-(cC62(iV16463)), cC60(iV16463), cC58xcomp(iV16463)],extension(21,bind([[_70390], [iV16463]]))).
% 0.63/1.41 cnf('1.1.39.2.1',plain,[-(cC60(iV16463)), rR1(iV16463, iV16464), cC12xcomp(iV16464)],extension(20,bind([[_70044, _70132], [iV16463, iV16464]]))).
% 0.63/1.41 cnf('1.1.39.2.1.1',plain,[-(rR1(iV16463, iV16464))],extension(66)).
% 0.63/1.41 cnf('1.1.39.2.1.2',plain,[-(cC12xcomp(iV16464))],extension(68)).
% 0.63/1.41 cnf('1.1.39.2.2',plain,[-(cC58xcomp(iV16463))],extension(65)).
% 0.63/1.41 cnf('1.1.40',plain,[-(cC62(iV16463)), cC60(iV16463), cC58xcomp(iV16463)],extension(21,bind([[_70390], [iV16463]]))).
% 0.63/1.41 cnf('1.1.40.1',plain,[-(cC60(iV16463)), rR1(iV16463, iV16464), cC12xcomp(iV16464)],extension(20,bind([[_70044, _70132], [iV16463, iV16464]]))).
% 0.63/1.41 cnf('1.1.40.1.1',plain,[-(rR1(iV16463, iV16464))],extension(66)).
% 0.63/1.41 cnf('1.1.40.1.2',plain,[-(cC12xcomp(iV16464))],extension(68)).
% 0.63/1.41 cnf('1.1.40.2',plain,[-(cC58xcomp(iV16463))],extension(65)).
% 0.63/1.41 cnf('1.1.41',plain,[-(cowlThing(iV16463))],extension(6,bind([[_43084], [iV16463]]))).
% 0.63/1.41 cnf('1.1.42',plain,[-(cC60(iV16463)), rR1(iV16463, iV16464), cC12xcomp(iV16464)],extension(20,bind([[_70044, _70132], [iV16463, iV16464]]))).
% 0.63/1.41 cnf('1.1.42.1',plain,[-(rR1(iV16463, iV16464))],extension(66)).
% 0.63/1.41 cnf('1.1.42.2',plain,[-(cC12xcomp(iV16464))],extension(68)).
% 0.63/1.41 cnf('1.1.43',plain,[-(cC56(iV16464)), cC54xcomp(iV16464), cC44(iV16464)],extension(19,bind([[_67410], [iV16464]]))).
% 0.63/1.41 cnf('1.1.43.1',plain,[-(cC54xcomp(iV16464))],extension(69)).
% 0.63/1.41 cnf('1.1.43.2',plain,[-(cC44(iV16464)), cC40xcomp(iV16464), cC42(iV16464)],extension(17,bind([[_62726], [iV16464]]))).
% 0.63/1.41 cnf('1.1.43.2.1',plain,[-(cC40xcomp(iV16464))],extension(67)).
% 0.63/1.41 cnf('1.1.43.2.2',plain,[-(cC42(iV16464)), rR1(iV16464, iV16465), cC8xcomp(iV16465)],extension(16,bind([[_62380, _62468], [iV16464, iV16465]]))).
% 0.63/1.41 cnf('1.1.43.2.2.1',plain,[-(rR1(iV16464, iV16465))],extension(70)).
% 0.63/1.41 cnf('1.1.43.2.2.2',plain,[-(cC8xcomp(iV16465))],extension(72)).
% 0.63/1.41 cnf('1.1.44',plain,[-(cC42(iV16464)), rR1(iV16464, iV16465), cC8xcomp(iV16465)],extension(16,bind([[_62380, _62468], [iV16464, iV16465]]))).
% 0.63/1.41 cnf('1.1.44.1',plain,[-(rR1(iV16464, iV16465))],extension(70)).
% 0.63/1.41 cnf('1.1.44.2',plain,[-(cC8xcomp(iV16465))],extension(72)).
% 0.63/1.41 cnf('1.1.45',plain,[-(cC44(iV16464)), cC40xcomp(iV16464), cC42(iV16464)],extension(17,bind([[_62726], [iV16464]]))).
% 0.63/1.41 cnf('1.1.45.1',plain,[-(cC40xcomp(iV16464))],extension(67)).
% 0.63/1.41 cnf('1.1.45.2',plain,[-(cC42(iV16464))],lemmata('1.1')).
% 0.63/1.41 cnf('1.1.46',plain,[-(cowlThing(iV16464))],extension(6,bind([[_43084], [iV16464]]))).
% 0.63/1.41 cnf('1.1.47',plain,[-(cC38(iV16465)), cTOP(iV16465), cC36xcomp(iV16465)],extension(15,bind([[_60014], [iV16465]]))).
% 0.63/1.41 cnf('1.1.47.1',plain,[-(cTOP(iV16465))],extension(71)).
% 0.63/1.41 cnf('1.1.47.2',plain,[-(cC36xcomp(iV16465))],extension(73)).
% 0.63/1.41 cnf('1.1.48',plain,[-(cowlThing(iV16465))],extension(6,bind([[_43084], [iV16465]]))).
% 0.63/1.41 %-----------------------------------------------------
% 0.70/1.42
% 0.70/1.42 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------